text:
(* Author: Stefan Merz *)
header {* $\omega$-words *}
theory Words
imports "~~/src/HOL/Library/Infinite_Set"
begin
text {* Note: This theory is copied from Stefan Merz's work. *}

text {*
  Automata recognize languages, which are sets of words. For the
  theory of $\omega$-automata, we are mostly interested in
  $\omega$-words, but it is sometimes useful to reason about
  finite words, too. We are modeling finite words as lists; this
  lets us benefit from the existing library. Other formalizations
  could be investigated, such as representing words as functions
  whose domains are initial intervals of the natural numbers.
*}

subsection {* Type declaration and elementary operations *}

text {*
  We represent $\omega$-words as functions from the natural numbers
  to the alphabet type. Other possible formalizations include
  a coinductive definition or a uniform encoding of finite and
  infinite words, as studied by M\"uller et al.
*}

type_synonym
  'a word = "nat \<Rightarrow> 'a"

definition
  suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
  where "suffix k x \<equiv> \<lambda>n. x (k+n)"

lemma suffix_nth [simp]:
  "(suffix k x) n = x (k+n)"
by (simp add: suffix_def)

lemma suffix_0 [simp]:
  "suffix 0 x = x"
by (simp add: suffix_def)

lemma suffix_suffix [simp]:
  "suffix m (suffix k x) = suffix (k+m) x"
by (rule ext, simp add: suffix_def add.assoc)

(*
text {*
  A finite part of an infinite word can be obtained as the
  result of mapping the word over the desired index interval.
  For now, we do not define a separate constant for this
  construction, as it does not occur very often, and we prefer
  to rely on the proof machinery provided by the standard library.
  However, the standard rewriting rules include the theorem @{text upt_Suc},
  which tends to convert, say, $[i..j]$ into $[i..j(] @ [j]$.
  Since this is (almost) never what we want, we remove the theorem
  from the rule base in effect for this session.
*}
declare upt_Suc [simp del]
*)

text {*
  We can prefix a finite word to an $\omega$-word, and a way
  to obtain an $\omega$-word from a finite, non-empty word is by
  $\omega$-iteration.
*}

definition
  conc :: "['a list, 'a word] \<Rightarrow> 'a word"    ("_/ conc _" [66,65] 65)
  where "w conc x == \<lambda>n. if n < length w then w!n else x (n - length w)"

definition
  iter :: "'a list \<Rightarrow> 'a word"
  where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"

syntax (xsymbols)
  conc :: "['a list, 'a word] \<Rightarrow> 'a word"    ("_/ \<frown> _" [66,65] 65)
  iter :: "'a list \<Rightarrow> 'a word"               ("(_\<^sup>\<omega>)" [1000])

lemma conc_empty[simp]: "[] \<frown> w = w"
  unfolding conc_def by auto

lemma conc_fst:
  "n < length w \<Longrightarrow> (w \<frown> x) n = w!n"
by (simp add: conc_def)

lemma conc_snd:
  "\<not>(n < length w) \<Longrightarrow> (w \<frown> x) n = x (n - length w)"
by (simp add: conc_def)

lemma iter_nth [simp]:
  "0 < length w \<Longrightarrow> w\<^sup>\<omega> n = w!(n mod (length w))"
by (simp add: iter_def)

lemma conc_conc:
  "u \<frown> v \<frown> w = (u @ v) \<frown> w" (is "?lhs = ?rhs")
proof
  fix n
  have u: "n < length u \<Longrightarrow> ?lhs n = ?rhs n"
    by (simp add: conc_def nth_append)
  have v: "\<lbrakk> \<not>(n < length u); n < length u + length v \<rbrakk> \<Longrightarrow> ?lhs n = ?rhs n"
    by (simp add: conc_def nth_append, arith)
  have w: "\<not>(n < length u + length v) \<Longrightarrow> ?lhs n = ?rhs n"
    by (simp add: conc_def nth_append, arith)
  from u v w show "?lhs n = ?rhs n" by auto
qed

lemma prefix_suffix:
  "x = (map x [0..<n] ) \<frown> (suffix n x)"
by (rule ext, simp add: conc_def)

lemma iter_unroll:
  "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>"
by (rule ext, simp add: conc_def mod_geq)

subsection {* The limit set of an $\omega$-word *}

text {*
  The limit set (also called infinity set) of an $\omega$-word
  is the set of letters that appear infinitely often in the word.
  This set plays an important role in defining acceptance conditions
  of $\omega$-automata.
*}

definition
  limit :: "'a word \<Rightarrow> 'a set"
  where "limit x \<equiv> { a . \<exists>\<^sub>\<infinity>n . x n = a }"

lemma limit_iff_frequent:
  "(a \<in> limit x) = (\<exists>\<^sub>\<infinity>n . x n = a)"
by (simp add: limit_def)

text {*
  The following is a different way to define the limit,
  using the reverse image, making the laws about reverse
  image applicable to the limit set.
  (Might want to change the definition above?)
*}

lemma limit_vimage:
  "(a \<in> limit x) = infinite (x -` {a})"
by (simp add: limit_def Inf_many_def vimage_def)

lemma two_in_limit_iff:
  "({a,b} \<subseteq> limit x) =
   ((\<exists>n. x n =a ) \<and> (\<forall>n. x n = a \<longrightarrow> (\<exists>m>n. x m = b)) \<and> (\<forall>m. x m = b \<longrightarrow> (\<exists>n>m. x n = a)))"
  (is "?lhs = (?r1 \<and> ?r2 \<and> ?r3)")
proof
  assume lhs: "?lhs"
  hence 1: "?r1" by (auto simp: limit_def elim: INFM_EX)
  from lhs have "\<forall>n. \<exists>m>n. x m = b" by (auto simp: limit_def INFM_nat)
  hence 2: "?r2" by simp
  from lhs have "\<forall>m. \<exists>n>m. x n = a" by (auto simp: limit_def INFM_nat)
  hence 3: "?r3" by simp
  from 1 2 3 show "?r1 \<and> ?r2 \<and> ?r3" by simp
next
  assume "?r1 \<and> ?r2 \<and> ?r3"
  hence 1: "?r1" and 2: "?r2" and 3: "?r3" by simp+
  have infa: "\<forall>m. \<exists>n\<ge>m. x n = a"
  proof
    fix m
    show "\<exists>n\<ge>m. x n = a" (is "?A m")
    proof (induct m)
      from 1 show "?A 0" by simp
    next
      fix m
      assume ih: "?A m"
      then obtain n where n: "n \<ge> m" "x n = a" by auto
      with 2 obtain k where k: "k>n" "x k = b" by auto
      with 3 obtain l where l: "l>k" "x l = a" by auto
      from n k l have "l \<ge> Suc m" by auto
      with l show "?A (Suc m)" by auto
    qed
  qed
  hence infa': "\<exists>\<^sub>\<infinity>n. x n = a" by (simp add: INFM_nat_le)
  have "\<forall>n. \<exists>m>n. x m = b"
  proof
    fix n
    from infa obtain k where k1: "k\<ge>n" and k2: "x k = a" by auto
    from 2 k2 obtain l where l1: "l>k" and l2: "x l = b" by auto
    from k1 l1 have "l > n" by auto
    with l2 show "\<exists>m>n. x m = b" by auto
  qed
  hence "\<exists>\<^sub>\<infinity>m. x m = b" by (simp add: INFM_nat)
  with infa' show "?lhs" by (auto simp: limit_def)
qed

text {*
  For $\omega$-words over a finite alphabet, the limit set is
  non-empty. Moreover, from some position onward, any such word
  contains only letters from its limit set.
*}

lemma limit_nonempty:
  assumes fin: "finite (range x)"
  shows "\<exists>a. a \<in> limit x"
proof -
  from fin obtain a where "a \<in> range x \<and> infinite (x -` {a})"
    by (rule inf_img_fin_domE, auto)
  hence "a \<in> limit x"
    by (auto simp add: limit_vimage)
  thus ?thesis ..
qed

lemmas limit_nonemptyE = limit_nonempty[THEN exE]

lemma limit_inter_INF:
  assumes hyp: "limit w \<inter> S \<noteq> {}"
  shows "\<exists>\<^sub>\<infinity> n. w n \<in> S"
proof -
  from hyp obtain x where "\<exists>\<^sub>\<infinity> n. w n = x" and "x \<in> S"
    by (auto simp add: limit_def)
  thus ?thesis
    by (auto elim: INFM_mono)
qed

text {*
  The reverse implication is true only if $S$ is finite.
*}

lemma INF_limit_inter:
  assumes hyp: "\<exists>\<^sub>\<infinity> n. w n \<in>  S" and fin: "finite (S \<inter> range w)"
  shows  "\<exists>a. a \<in> limit w \<inter> S"
proof (rule ccontr)
  assume contra: "\<not>(\<exists>a. a \<in> limit w \<inter> S)"
  hence "\<forall>a\<in>S. finite {n. w n = a}"
    by (auto simp add: limit_def Inf_many_def)
  with fin have "finite (UN a:S \<inter> range w. {n. w n = a})"
    by auto
  moreover
  have "(UN a:S \<inter> range w. {n. w n = a}) = {n. w n \<in> S}"
    by auto
  moreover
  note hyp
  ultimately show "False"
    by (simp add: Inf_many_def)
qed

lemma fin_ex_inf_eq_limit: "finite A \<Longrightarrow> (\<exists>\<^sub>\<infinity>i. w i \<in> A) \<longleftrightarrow> limit w \<inter> A \<noteq> {}"
  by (metis INF_limit_inter equals0D finite_Int limit_inter_INF)

lemma limit_in_range_suffix:
  "limit x \<subseteq> range (suffix k x)"
proof
  fix a
  assume "a \<in> limit x"
  then obtain l where
    kl: "k < l" and xl: "x l = a"
    by (auto simp add: limit_def INFM_nat)
  from kl obtain m where "l = k+m"
    by (auto simp add:  less_iff_Suc_add)
  with xl show "a \<in> range (suffix k x)"
    by auto
qed

lemma limit_in_range: "limit r \<subseteq> range r"
  using limit_in_range_suffix[of r 0] by simp

lemmas limit_in_range_suffixD = limit_in_range_suffix[THEN subsetD]

theorem limit_is_suffix:
  assumes fin: "finite (range x)"
  shows "\<exists>k. limit x = range (suffix k x)"
proof -
  have "\<exists>k. range (suffix k x) \<subseteq> limit x"
  proof -
    -- "The set of letters that are not in the limit is certainly finite."
    from fin have "finite (range x - limit x)"
      by simp
    -- "Moreover, any such letter occurs only finitely often"
    moreover
    have "\<forall>a \<in> range x - limit x. finite (x -` {a})"
      by (auto simp add: limit_vimage)
    -- "Thus, there are only finitely many occurrences of such letters."
    ultimately have "finite (UN a : range x - limit x. x -` {a})"
      by (blast intro: finite_UN_I)
    -- "Therefore these occurrences are within some initial interval."
    then obtain k where "(UN a : range x - limit x. x -` {a}) \<subseteq> {..<k}"
      by (blast dest: finite_nat_bounded)
    -- "This is just the bound we are looking for."
    hence "\<forall>m. k \<le> m \<longrightarrow> x m \<in> limit x"
      by (auto simp add: limit_vimage)
    hence "range (suffix k x) \<subseteq> limit x"
      by auto
    thus ?thesis ..
  qed
  then obtain k where "range (suffix k x) \<subseteq> limit x" ..
  with limit_in_range_suffix
  have "limit x = range (suffix k x)"
    by (rule subset_antisym)
  thus ?thesis ..
qed

theorems limit_is_suffixE = limit_is_suffix[THEN exE]

text {*
  The limit set enjoys some simple algebraic laws with respect
  to concatenation, suffixes, iteration, and renaming.
*}

theorem limit_conc [simp]:
  "limit (w \<frown> x) = limit x"
proof (auto)
  fix a assume a: "a \<in> limit (w \<frown> x)"
  have "\<forall>m. \<exists>n. m<n \<and> x n = a"
  proof
    fix m
    from a obtain n where "m + length w < n \<and> (w \<frown> x) n = a"
      by (auto simp add: limit_def Inf_many_def infinite_nat_iff_unbounded)
    hence "m < n - length w \<and> x (n - length w) = a"
      by (auto simp add: conc_def)
    thus "\<exists>n. m<n \<and> x n = a" ..
  qed
  hence "infinite {n . x n = a}"
    by (simp add: infinite_nat_iff_unbounded)
  thus "a \<in> limit x"
    by (simp add: limit_def Inf_many_def)
next
  fix a assume a: "a \<in> limit x"
  have "\<forall>m. length w < m \<longrightarrow> (\<exists>n. m<n \<and> (w \<frown> x) n = a)"
  proof (clarify)
    fix m
    assume m: "length w < m"
    with a obtain n where "m - length w < n \<and> x n = a"
      by (auto simp add: limit_def Inf_many_def infinite_nat_iff_unbounded)
    with m have "m < n + length w \<and> (w \<frown> x) (n + length w) = a"
      by (simp add: conc_def, arith)
    thus "\<exists>n. m<n \<and> (w \<frown> x) n = a" ..
  qed
  hence "infinite {n . (w \<frown> x) n = a}"
    by (simp add: unbounded_k_infinite)
  thus "a \<in> limit (w \<frown> x)"
    by (simp add: limit_def Inf_many_def)
qed

theorem limit_suffix [simp]:
  "limit (suffix n x) = limit x"
proof -
  have "x = (map x [0..<n]) \<frown> (suffix n x)"
    by (simp add: prefix_suffix)
  hence "limit x = limit ((map x [0..<n]) \<frown> suffix n x)"
    by simp
  also have "\<dots> = limit (suffix n x)"
    by (rule limit_conc)
  finally show ?thesis
    by (rule sym)
qed

theorem limit_iter [simp]:
  assumes nempty: "0 < length w"
  shows "limit w\<^sup>\<omega> = set w"
proof
  have "limit w\<^sup>\<omega> \<subseteq> range w\<^sup>\<omega>"
    by (auto simp add: limit_def dest: INFM_EX)
  also from nempty have "\<dots> \<subseteq> set w"
    by auto
  finally show "limit w\<^sup>\<omega> \<subseteq> set w" .
next
  {
    fix a assume a: "a \<in> set w"
    then obtain k where k: "k < length w \<and> w!k = a"
      by (auto simp add: set_conv_nth)
    -- "the following bound is terrible, but it simplifies the proof"
    from nempty k
    have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
      by (simp add: mod_add_left_eq)
    moreover
    -- "why is the following so hard to prove??"
    have "\<forall>m. m < (Suc m)*(length w) + k"
    proof
      fix m
      from nempty have "1 \<le> length w" by arith
      hence "m*1 \<le> m*length w" by simp
      hence "m \<le> m*length w" by simp
      with nempty have "m < length w + (m*length w) + k" by arith
      thus "m < (Suc m)*(length w) + k" by simp
    qed
    moreover note nempty
    ultimately have "a \<in> limit w\<^sup>\<omega>"
      by (auto simp add: limit_iff_frequent INFM_nat)
  }
  then show "set w \<subseteq> limit w\<^sup>\<omega>" by auto
qed

lemma limit_o [simp]:
  assumes a: "a \<in> limit w"
  shows "f a \<in> limit (f \<circ> w)"
proof -
  from a
  have "\<exists>\<^sub>\<infinity>n. w n = a"
    by (simp add: limit_iff_frequent)
  hence "\<exists>\<^sub>\<infinity>n. f (w n) = f a"
    by (rule INFM_mono, simp)
  thus "f a \<in> limit (f \<circ> w)"
    by (simp add: limit_iff_frequent)
qed

text {*
  The converse relation is not true in general: $f(a)$ can be in the
  limit of $f \circ w$ even though $a$ is not in the limit of $w$.
  However, @{text limit} commutes with renaming if the function is
  injective. More generally, if $f(a)$ is the image of only finitely
  many elements, some of these must be in the limit of $w$.
*}

lemma limit_o_inv:
  assumes fin: "finite (f -` {x})" and x: "x \<in> limit (f \<circ> w)"
  shows "\<exists>a \<in> (f -` {x}). a \<in> limit w"
proof (rule ccontr)
  assume contra: "\<not>(\<exists>a \<in> (f -` {x}). a \<in> limit w)"
  -- "hence, every element in the pre-image occurs only finitely often"
  then have "\<forall>a \<in> (f -` {x}). finite {n. w n = a}"
    by (simp add: limit_def Inf_many_def)
  -- "so there are only finitely many occurrences of any such element"
  with fin have "finite (\<Union> a \<in> (f -` {x}). {n. w n = a})"
    by auto
  -- {* these are precisely those positions where $x$ occurs in $f \circ w$ *}
  moreover
  have "(\<Union> a \<in> (f -` {x}). {n. w n = a}) = {n. f(w n) = x}"
    by auto
  ultimately
  -- "so $x$ can occur only finitely often in the translated word"
  have "finite {n. f(w n) = x}"
    by simp
  -- {* \ldots\ which yields a contradiction *}
  with x show "False"
    by (simp add: limit_def Inf_many_def)
qed

theorem limit_inj [simp]:
  assumes inj: "inj f"
  shows "limit (f \<circ> w) = f ` (limit w)"
proof
  show "f ` limit w \<subseteq> limit (f \<circ> w)"
    by auto
next
  show "limit (f \<circ> w) \<subseteq> f ` limit w"
  proof
    fix x
    assume x: "x \<in> limit (f \<circ> w)"
    from inj have "finite (f -` {x})"
      by (blast intro: finite_vimageI)
    with x obtain a where a: "a \<in> (f -` {x}) \<and> a \<in> limit w"
      by (blast dest: limit_o_inv)
    thus "x \<in> f ` (limit w)"
      by auto
  qed
qed

subsection {* Index sequences and piecewise definitions *}

text {*
  A word can be defined piecewise: given a sequence of words $w_0, w_1, \ldots$
  and a strictly increasing sequence of integers $i_0, i_1, \ldots$ where $i_0=0$,
  a single word is obtained by concatenating subwords of the $w_n$ as given by
  the integers: the resulting word is
  \[
    (w_0)_{i_0} \ldots (w_0)_{i_1-1} (w_1)_{i_1} \ldots (w_1)_{i_2-1} \ldots
  \]
  We prepare the field by proving some trivial facts about such sequences of
  indexes.
*}

definition
  idx_sequence :: "nat word \<Rightarrow> bool"
  where "idx_sequence idx \<equiv> (idx 0 = 0) \<and> (\<forall>n. idx n < idx (Suc n))"

lemma idx_sequence_less:
  assumes iseq: "idx_sequence idx"
  shows "idx n < idx (Suc(n+k))"
proof (induct k)
  from iseq show "idx n < idx (Suc (n + 0))"
    by (simp add: idx_sequence_def)
next
  fix k
  assume ih: "idx n < idx (Suc(n+k))"
  from iseq have "idx (Suc(n+k)) < idx (Suc(n + Suc k))"
    by (simp add: idx_sequence_def)
  with ih show "idx n < idx (Suc(n + Suc k))"
    by (rule less_trans)
qed

lemma idx_sequence_inj:
  assumes iseq: "idx_sequence idx"
  and eq: "idx m = idx n"
  shows "m = n"
proof (rule nat_less_cases)
  assume "n<m"
  then obtain k where "m = Suc(n+k)"
    by (auto simp add: less_iff_Suc_add)
  with iseq have "idx n < idx m"
    by (simp add: idx_sequence_less)
  with eq show ?thesis
    by simp
next
  assume "m<n"
  then obtain k where "n = Suc(m+k)"
    by (auto simp add: less_iff_Suc_add)
  with iseq have "idx m < idx n"
    by (simp add: idx_sequence_less)
  with eq show ?thesis
    by simp
qed (simp)

lemma idx_sequence_mono:
  assumes iseq: "idx_sequence idx"
  and m: "m \<le> n"
  shows "idx m \<le> idx n"
proof (cases "m=n")
  case True
  thus ?thesis by simp
next
  case False
  with m have "m < n" by simp
  then obtain k where "n = Suc(m+k)"
    by (auto simp add: less_iff_Suc_add)
  with iseq have "idx m < idx n"
    by (simp add: idx_sequence_less)
  thus ?thesis by simp
qed

text {*
  Given an index sequence, every natural number is contained in the
  interval defined by two adjacent indexes, and in fact this interval
  is determined uniquely.
*}

lemma idx_sequence_idx:
  assumes "idx_sequence idx"
  shows "idx k \<in> {idx k ..< idx (Suc k)}"
using assms by (auto simp add: idx_sequence_def)

lemma idx_sequence_interval:
  assumes iseq: "idx_sequence idx"
  shows "\<exists>k. n \<in> {idx k ..< idx (Suc k) }"
    (is "?P n" is "\<exists>k. ?in n k")
proof (induct n)
  from iseq have "0 = idx 0"
    by (simp add: idx_sequence_def)
  moreover
  from iseq have "idx 0 \<in> {idx 0 ..< idx (Suc 0) }"
    by (rule idx_sequence_idx)
  ultimately
  show "?P 0" by auto
next
  fix n
  assume "?P n"
  then obtain k where k: "?in n k" ..
  show "?P (Suc n)"
  proof (cases "Suc n < idx (Suc k)")
    case True
    with k have "?in (Suc n) k"
      by simp
    thus ?thesis ..
  next
    case False
    with k have "Suc n = idx (Suc k)"
      by auto
    with iseq have "?in (Suc n) (Suc k)"
      by (simp add: idx_sequence_def)
    thus ?thesis ..
  qed
qed

lemma idx_sequence_interval_unique:
  assumes iseq: "idx_sequence idx"
  and k: "n \<in> {idx k ..< idx (Suc k) }"
  and m: "n \<in> {idx m ..< idx (Suc m) }"
  shows "k = m"
proof (rule nat_less_cases)
  assume "k < m"
  hence "Suc k \<le> m" by simp
  with iseq have "idx (Suc k) \<le> idx m"
    by (rule idx_sequence_mono)
  with m have "idx (Suc k) \<le> n"
    by auto
  with k have "False"
    by simp
  thus ?thesis ..
next
  assume "m < k"
  hence "Suc m \<le> k" by simp
  with iseq have "idx (Suc m) \<le> idx k"
    by (rule idx_sequence_mono)
  with k have "idx (Suc m) \<le> n"
    by auto
  with m have "False"
    by simp
  thus ?thesis ..
qed (simp)

lemma idx_sequence_unique_interval:
  assumes iseq: "idx_sequence idx"
  shows "\<exists>! k. n \<in> {idx k ..< idx (Suc k) }"
proof (rule ex_ex1I)
  from iseq show "\<exists>k. n \<in> {idx k ..< idx (Suc k)}"
    by (rule idx_sequence_interval)
next
  fix k y
  assume "n \<in> {idx k..<idx (Suc k)}" and "n \<in> {idx y..<idx (Suc y)}"
  with iseq show "k = y" by (auto elim: idx_sequence_interval_unique)
qed

text {*
  Now we can define the piecewise construction of a word using
  an index sequence.
*}

definition
  merge :: "['a word word, nat word] \<Rightarrow> 'a word"
  where "merge ws idx \<equiv>
           \<lambda> n. let i = THE i. n \<in> {idx i ..< idx (Suc i) } in ws i n"

lemma merge:
  assumes idx: "idx_sequence idx"
  and n: "n \<in> {idx i ..< idx (Suc i) }"
  shows "merge ws idx n = ws i n"
proof -
  from n have "(THE k. n \<in> {idx k ..< idx (Suc k) }) = i"
    by (rule the_equality[OF _ sym[OF idx_sequence_interval_unique[OF idx n]]]) simp
  thus ?thesis
    by (simp add: merge_def Let_def)
qed

lemma merge0:
  assumes idx: "idx_sequence idx"
  shows "merge ws idx 0 = ws 0 0"
proof (rule merge[OF idx])
  from idx have "idx 0 < idx (Suc 0)"
    by (unfold idx_sequence_def, blast)
  with idx show "0 \<in> {idx 0 ..< idx (Suc 0)}"
    by (simp add: idx_sequence_def)
qed

lemma merge_Suc:
  assumes idx: "idx_sequence idx"
  and n: "n \<in> {idx i ..< idx (Suc i) }"
  shows "merge ws idx (Suc n) =
         (if Suc n = idx (Suc i) then ws (Suc i) else ws i) (Suc n)"
proof (auto)
  assume eq: "Suc n = idx (Suc i)"
  from idx have "idx (Suc i) < idx (Suc(Suc i))"
    by (unfold idx_sequence_def, blast)
  with eq idx show "merge ws idx (idx (Suc i)) = ws (Suc i) (idx (Suc i))"
    by (simp add: merge)
next
  assume neq: "Suc n \<noteq> idx (Suc i)"
  with n have "Suc n \<in> {idx i ..< idx (Suc i) }"
    by auto
  with idx show "merge ws idx (Suc n) = ws i (Suc n)"
    by (rule merge)
qed

end


text:
(*
   Title: Psi-calculi
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Simulation
  imports Semantics
begin

context env begin

definition
  "simulation" :: "'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
                   ('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set \<Rightarrow>
                   ('a, 'b, 'c) psi \<Rightarrow> bool" ("_ \<rhd> _ \<leadsto>[_] _" [80, 80, 80, 80] 80)
where
  "\<Psi> \<rhd> P \<leadsto>[Rel] Q \<equiv> \<forall>\<alpha> Q'. \<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q' \<longrightarrow> bn \<alpha> \<sharp>* \<Psi> \<longrightarrow> bn \<alpha> \<sharp>* P \<longrightarrow> (\<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel)"

abbreviation
  simulationNilJudge ("_ \<leadsto>[_] _" [80, 80, 80] 80) where "P \<leadsto>[Rel] Q \<equiv> SBottom' \<rhd> P \<leadsto>[Rel] Q"

lemma simI[consumes 1, case_names cSim]:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   C   :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     Sim: "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha>  \<sharp>* \<Psi>; distinct(bn \<alpha>);
                         bn \<alpha> \<sharp>* (subject \<alpha>); bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
proof(auto simp add: simulation_def)
  fix \<alpha> Q'
  assume "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" and "bn \<alpha> \<sharp>* \<Psi>" and "bn \<alpha> \<sharp>* P"
  thus "\<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"
  proof(nominal_induct \<alpha> rule: action.strong_induct)
    case(In M N)
    thus ?case by(rule_tac Sim) auto
  next
    case(Out M xvec N)
    moreover {
      fix M xvec N Q'
      assume "(xvec::name list) \<sharp>* \<Psi>" and "xvec \<sharp>* P"
      obtain p where xvecFreshPsi: "((p::name prm) \<bullet> (xvec::name list)) \<sharp>* \<Psi>"
                 and xvecFreshM: "(p \<bullet> xvec) \<sharp>* (M::'a)"
                 and xvecFreshN: "(p \<bullet> xvec) \<sharp>* (N::'a)"
                 and xvecFreshP: "(p \<bullet> xvec) \<sharp>* P"
                 and xvecFreshQ: "(p \<bullet> xvec) \<sharp>* Q"
                 and xvecFreshQ': "(p \<bullet> xvec) \<sharp>* (Q'::('a, 'b, 'c) psi)"
                 and xvecFreshC: "(p \<bullet> xvec) \<sharp>* C"
                 and xvecFreshxvec: "(p \<bullet> xvec) \<sharp>* xvec"
                 and S: "(set p) \<subseteq> (set xvec) \<times> (set(p \<bullet> xvec))"
                 and dpr: "distinctPerm p"
        by(rule_tac xvec=xvec and c="(\<Psi>, M, Q, N, P, Q', xvec, C)" in name_list_avoiding)
          (auto simp add: eqvts fresh_star_prod)

      from \<open>(p \<bullet> xvec) \<sharp>* M\<close> \<open>distinctPerm p\<close> have "xvec \<sharp>* (p \<bullet> M)"
        by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, where pi=p, symmetric]) simp

      assume Trans: "\<Psi> \<rhd> Q \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'"
      with xvecFreshN xvecFreshQ' S
      have "\<Psi> \<rhd> Q \<longmapsto>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> Q')"
        by(simp add: boundOutputChainAlpha'' residualInject)
      moreover hence "distinct(p \<bullet> xvec)"  by(auto dest: boundOutputDistinct)

      moreover note xvecFreshPsi xvecFreshP xvecFreshQ xvecFreshM xvecFreshC
      ultimately obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'"
                            and P'RelQ': "(\<Psi>, P', p \<bullet> Q') \<in> Rel"
        by(drule_tac Sim) auto
      hence "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto>(p \<bullet> (M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'))"
        by(rule_tac semantics.eqvt)
      with \<open>xvec \<sharp>* \<Psi>\<close> xvecFreshPsi \<open>xvec \<sharp>* P\<close> xvecFreshP S dpr
      have "\<Psi> \<rhd> P \<longmapsto>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')"
        by(simp add: eqvts name_set_fresh_fresh)
      with \<open>xvec \<sharp>* \<Psi>\<close> xvecFreshPsi \<open>xvec \<sharp>* P\<close> xvecFreshP S \<open>xvec \<sharp>* (p \<bullet> M)\<close>
      have "\<Psi> \<rhd> P \<longmapsto>(p \<bullet> p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')"
       by(rule_tac outputPermSubject)
         (simp add: fresh_star_def | assumption)+

      with dpr have "\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')"
        by simp

      moreover from P'RelQ' Eqvt have "(p \<bullet> \<Psi>, p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel"
        apply(simp add: eqvt_def eqvts)
        apply(erule_tac x="(\<Psi>, P', p \<bullet> Q')" in ballE)
        apply(erule_tac x="p" in allE)
        by(auto simp add: eqvts)

      with \<open>xvec \<sharp>* \<Psi>\<close> xvecFreshPsi S dpr have "(\<Psi>, p \<bullet> P', Q') \<in> Rel" by simp
      ultimately have "\<exists>P'. \<Psi> \<rhd> P \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"
        by blast
    }
    ultimately show ?case by force
  next
    case Tau
    thus ?case by(rule_tac Sim) auto
  qed
qed

lemma simI2[case_names cSim]:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   C   :: "'d::fs_name"

  assumes Sim: "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* P; bn \<alpha>  \<sharp>* \<Psi>; distinct(bn \<alpha>)\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
using assms
by(auto simp add: simulation_def dest: boundOutputDistinct)

lemma simIChainFresh[consumes 4, case_names cSim]:
  fixes \<Psi>    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"
  and   C    :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     "xvec \<sharp>* \<Psi>"
  and     "xvec \<sharp>* P"
  and     "xvec \<sharp>* Q"
  and     Sim: "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* \<Psi>;
                         bn \<alpha> \<sharp>* subject \<alpha>; distinct(bn \<alpha>); bn \<alpha> \<sharp>* C; xvec \<sharp>* \<alpha>; xvec \<sharp>* Q'\<rbrakk> \<Longrightarrow>
                         \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"
  shows "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
using \<open>eqvt Rel\<close>
proof(induct rule: simI[where C="(xvec, C)"])
  case(cSim \<alpha> Q')
  from \<open>bn \<alpha> \<sharp>* (xvec, C)\<close> have "bn \<alpha> \<sharp>* xvec" and "bn \<alpha> \<sharp>* C" by(simp add: freshChainSym)+
  obtain p::"name prm" where "(p \<bullet> xvec) \<sharp>* \<Psi>" and  "(p \<bullet> xvec) \<sharp>* P" and  "(p \<bullet> xvec) \<sharp>* Q"
                         and  "(p \<bullet> xvec) \<sharp>* \<alpha>" and S: "set p \<subseteq> set xvec \<times> set(p \<bullet> xvec)"
                         and "distinctPerm p"
    by(rule_tac c="(\<Psi>, P, Q, \<alpha>)" and xvec=xvec in name_list_avoiding) auto
  show ?case
  proof(cases rule: actionCases[where \<alpha>=\<alpha>])
    case(cInput M N)
    from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha>=M\<lparr>N\<rparr>\<close> have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> Q) \<longmapsto>(p \<bullet> (M\<lparr>N\<rparr> \<prec> Q'))"
      by(fastforce intro: semantics.eqvt)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* Q\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close> S
    have QTrans: "\<Psi> \<rhd> Q \<longmapsto>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> (p \<bullet> Q')"
      by(simp add: eqvts)
    moreover from \<open>(p \<bullet> xvec) \<sharp>* \<alpha>\<close> have "(p \<bullet> (p \<bullet> xvec)) \<sharp>* (p \<bullet> \<alpha>)"
      by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with \<open>distinctPerm p\<close> \<open>\<alpha>=M\<lparr>N\<rparr>\<close> have "xvec \<sharp>* (p \<bullet> M)" and "xvec \<sharp>* (p \<bullet> N)" by simp+
    moreover with QTrans \<open>xvec \<sharp>* Q\<close> have "xvec \<sharp>* (p \<bullet> Q')" by(rule_tac inputFreshChainDerivative)
    ultimately have "\<exists>P'. \<Psi> \<rhd> P \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P' \<and> (\<Psi>, P', (p \<bullet> Q')) \<in> Rel"
      by(rule_tac Sim) (assumption | simp)+
    then obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P'" and P'RelQ': "(\<Psi>, P', (p \<bullet> Q')) \<in> Rel"
      by blast
    from PTrans have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto> (p \<bullet> ((p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P'))"
      by(rule semantics.eqvt)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> S \<open>distinctPerm p\<close>
    have "\<Psi> \<rhd> P \<longmapsto> M\<lparr>N\<rparr> \<prec> (p \<bullet> P')" by(simp add: eqvts)
    moreover from P'RelQ' \<open>eqvt Rel\<close> have "(p \<bullet> \<Psi>, p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel"
      by(auto simp add: eqvt_def)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> S \<open>distinctPerm p\<close>
    have "(\<Psi>, p \<bullet> P', Q') \<in> Rel" by simp
    ultimately show ?thesis using \<open>\<alpha>=M\<lparr>N\<rparr>\<close> by blast
  next
    case(cOutput M yvec N)
    from \<open>distinct(bn \<alpha>)\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> have "distinct yvec" and "yvec \<sharp>* M" by simp+
    from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> Q) \<longmapsto>(p \<bullet> (M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle> \<prec> Q'))"
      by(fastforce intro: semantics.eqvt)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* Q\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close> S
    have QTrans: "\<Psi> \<rhd> Q \<longmapsto>(p \<bullet> M)\<lparr>\<nu>*(p \<bullet> yvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> Q')"
      by(simp add: eqvts)
    with S \<open>bn \<alpha> \<sharp>* xvec\<close> \<open>(p \<bullet> xvec) \<sharp>* \<alpha>\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> have "\<Psi> \<rhd> Q \<longmapsto>(p \<bullet> M)\<lparr>\<nu>*yvec\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> Q')"
      by simp
    moreover from \<open>(p \<bullet> xvec) \<sharp>* \<alpha>\<close> have "(p \<bullet> (p \<bullet> xvec)) \<sharp>* (p \<bullet> \<alpha>)"
      by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with \<open>distinctPerm p\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> have "xvec \<sharp>* (p \<bullet> M)" and "xvec \<sharp>* (p \<bullet> N)" and "xvec \<sharp>* (p \<bullet> yvec)" by simp+
    moreover with QTrans \<open>xvec \<sharp>* Q\<close> \<open>distinct yvec\<close> \<open>yvec \<sharp>* M\<close> have "xvec \<sharp>* (p \<bullet> Q')"
      by(drule_tac outputFreshChainDerivative(2)) (auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    moreover from \<open>yvec \<sharp>* M\<close> S \<open>bn \<alpha> \<sharp>* xvec\<close> \<open>(p \<bullet> xvec) \<sharp>* \<alpha>\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> \<open>distinctPerm p\<close>
    have "yvec \<sharp>* (p \<bullet> M)" by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, where pi=p]) simp
    ultimately have "\<exists>P'. \<Psi> \<rhd> P \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*yvec\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P' \<and> (\<Psi>, P', (p \<bullet> Q')) \<in> Rel"
      using \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* Q\<close>\<open>bn \<alpha> \<sharp>* xvec\<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>yvec \<sharp>* M\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> \<open>distinct yvec\<close>
      by(rule_tac Sim) auto
    then obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*yvec\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'" and P'RelQ': "(\<Psi>, P', (p \<bullet> Q')) \<in> Rel"
      by blast
    from PTrans have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto> (p \<bullet> ((p \<bullet> M)\<lparr>\<nu>*yvec\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'))"
      by(rule semantics.eqvt)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> S \<open>distinctPerm p\<close> \<open>bn \<alpha> \<sharp>* xvec\<close> \<open>(p \<bullet> xvec) \<sharp>* \<alpha>\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close>
    have "\<Psi> \<rhd> P \<longmapsto> M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')" by(simp add: eqvts)
    moreover from P'RelQ' \<open>eqvt Rel\<close> have "(p \<bullet> \<Psi>, p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel"
      by(auto simp add: eqvt_def)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> S \<open>distinctPerm p\<close>
    have "(\<Psi>, p \<bullet> P', Q') \<in> Rel" by simp
    ultimately show ?thesis using \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> by blast
  next
    case cTau
    from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha> = \<tau>\<close> \<open>xvec \<sharp>* Q\<close> have "xvec \<sharp>* Q'"
      by(blast dest: tauFreshChainDerivative)
    with \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha> = \<tau>\<close>
    show ?thesis by(drule_tac Sim) auto
  qed
qed

lemma simIFresh[consumes 4, case_names cSim]:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   x   :: name
  and   C   :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     "x \<sharp> \<Psi>"
  and     "x \<sharp> P"
  and     "x \<sharp> Q"
  and     "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* \<Psi>;
                    bn \<alpha> \<sharp>* subject \<alpha>; distinct(bn \<alpha>); bn \<alpha> \<sharp>* C; x \<sharp> \<alpha>; x \<sharp> Q'\<rbrakk> \<Longrightarrow>
                    \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
using assms
by(rule_tac xvec="[x]" and C=C in simIChainFresh) auto

lemma simE:
  fixes F   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<leadsto>[Rel] Q"

  shows "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"
using assms
by(auto simp add: simulation_def)

lemma simClosedAux:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"
  and     PSimQ: "\<Psi> \<rhd> P \<leadsto>[Rel] Q"

  shows "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<leadsto>[Rel] (p \<bullet> Q)"
using EqvtRel
proof(induct rule: simI[of _ _ _ _ "(\<Psi>, P, p)"])
  case(cSim \<alpha> Q')
  from \<open>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto>\<alpha> \<prec> Q'\<close>
  have "(rev p \<bullet> p \<bullet> \<Psi>) \<rhd> (rev p \<bullet> p \<bullet> Q) \<longmapsto>(rev p \<bullet> (\<alpha> \<prec> Q'))"
    by(blast dest: semantics.eqvt)
  hence "\<Psi> \<rhd> Q \<longmapsto>(rev p \<bullet> \<alpha>) \<prec> (rev p \<bullet> Q')"
    by(simp add: eqvts)
  moreover with \<open>bn \<alpha> \<sharp>* (\<Psi>, P, p)\<close> have "bn \<alpha> \<sharp>* \<Psi>" and "bn \<alpha> \<sharp>* P" and "bn \<alpha> \<sharp>* p" by simp+
  ultimately obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>(rev p \<bullet> \<alpha>) \<prec> P'"
                         and P'RelQ': "(\<Psi>, P', rev p \<bullet> Q') \<in> Rel"
    using PSimQ
    by(force dest: simE freshChainPermSimp simp add: eqvts)
  from PTrans have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto>(p \<bullet> ((rev p \<bullet> \<alpha>) \<prec> P'))"
    by(rule semantics.eqvt)
  with \<open>bn \<alpha> \<sharp>* p\<close> have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto>\<alpha> \<prec> (p \<bullet> P')"
    by(simp add: eqvts freshChainPermSimp)
  moreover from P'RelQ' EqvtRel have "(p \<bullet> (\<Psi>, P', rev p \<bullet> Q')) \<in> Rel"
    by(simp only: eqvt_def)
  hence "(p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel" by simp
  ultimately show ?case by blast
qed

lemma simClosed:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] Q \<Longrightarrow> (p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<leadsto>[Rel] (p \<bullet> Q)"
  and   "P \<leadsto>[Rel] Q \<Longrightarrow> (p \<bullet> P) \<leadsto>[Rel] (p \<bullet> Q)"
using EqvtRel
by(force dest: simClosedAux simp add: permBottom)+

lemma reflexive:
  fixes Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"

  assumes "{(\<Psi>, P, P) | \<Psi> P. True} \<subseteq> Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] P"
using assms
by(auto simp add: simulation_def)

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
  and     QSimR: "\<Psi> \<rhd> Q \<leadsto>[Rel'] R"
  and     Eqvt: "eqvt Rel''"
  and     Set: "{(\<Psi>, P, R) | \<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel''] R"
using \<open>eqvt Rel''\<close>
proof(induct rule: simI[where C=Q])
  case(cSim \<alpha> R')
  from QSimR \<open>\<Psi> \<rhd> R \<longmapsto>\<alpha> \<prec> R'\<close> \<open>(bn \<alpha>) \<sharp>* \<Psi>\<close> \<open>(bn \<alpha>) \<sharp>* Q\<close>
  obtain Q' where QTrans: "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" and Q'Rel'R': "(\<Psi>, Q', R') \<in> Rel'"
    by(blast dest: simE)
  from PSimQ QTrans \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close>
  obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
    by(blast dest: simE)
  with PTrans Q'Rel'R' P'RelQ' Set
  show ?case by blast
qed

lemma statEqSim:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   \<Psi>'  :: 'b

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
  and     "eqvt Rel'"
  and     "\<Psi> \<simeq> \<Psi>'"
  and     C1: "\<And>\<Psi>'' R S \<Psi>'''. \<lbrakk>(\<Psi>'', R, S) \<in> Rel; \<Psi>'' \<simeq> \<Psi>'''\<rbrakk> \<Longrightarrow> (\<Psi>''', R, S) \<in> Rel'"

  shows "\<Psi>' \<rhd> P \<leadsto>[Rel'] Q"
using \<open>eqvt Rel'\<close>
proof(induct rule: simI[of _ _ _ _ \<Psi>])
  case(cSim \<alpha> Q')
  from \<open>\<Psi>' \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
  have "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" by(metis statEqTransition AssertionStatEqSym)
  with PSimQ \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close>
  obtain P' where "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'" and "(\<Psi>, P', Q') \<in> Rel"
    by(blast dest: simE)

  from \<open>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close> have "\<Psi>' \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
    by(rule statEqTransition)
  moreover from \<open>(\<Psi>, P', Q') \<in> Rel\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close> have "(\<Psi>', P', Q') \<in> Rel'"
    by(rule C1)
  ultimately show ?case by blast
qed

  assumes "\<Psi> \<rhd> P \<leadsto>[A] Q"
  and     "A \<subseteq> B"

  shows "\<Psi> \<rhd> P \<leadsto>[B] Q"
using assms
by(simp (no_asm) add: simulation_def) (auto dest: simE)

end

end

repo: PSL


text:
section "A Typed Language"

theory Types imports Star Complex_Main begin

text {* We build on @{theory Complex_Main} instead of @{theory Main} to access
the real numbers. *}

subsection "Arithmetic Expressions"

datatype val = Iv int | Rv real

type_synonym vname = string
type_synonym state = "vname \<Rightarrow> val"

text_raw{*\snip{aexptDef}{0}{2}{% *}
datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
text_raw{*}%endsnip*}

inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
"taval (Ic i) s (Iv i)" |
"taval (Rc r) s (Rv r)" |
"taval (V x) s (s x)" |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
 \<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
 \<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"

inductive_cases [elim!]:
  "taval (Ic i) s v"  "taval (Rc i) s v"
  "taval (V x) s v"
  "taval (Plus a1 a2) s v"

subsection "Boolean Expressions"

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (Bc v) s v" |
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"

subsection "Syntax of Commands"
(* a copy of Com.thy - keep in sync! *)

datatype
  com = SKIP
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;; _"  [60, 61] 60)
      | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
      | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)

subsection "Small-Step Semantics of Commands"

inductive
  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
where
Assign:  "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |

Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
Seq2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow> (c1';;c2,s')" |

IfTrue:  "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |

While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"

lemmas small_step_induct = small_step.induct[split_format(complete)]

subsection "The Type System"

datatype ty = Ity | Rty

type_synonym tyenv = "vname \<Rightarrow> ty"

inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
  ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
where
Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" |
Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"

declare atyping.intros [intro!]
inductive_cases [elim!]:
  "\<Gamma> \<turnstile> V x : \<tau>" "\<Gamma> \<turnstile> Ic i : \<tau>" "\<Gamma> \<turnstile> Rc r : \<tau>" "\<Gamma> \<turnstile> Plus a1 a2 : \<tau>"

text{* Warning: the ``:'' notation leads to syntactic ambiguities,
i.e. multiple parse trees, because ``:'' also stands for set membership.
In most situations Isabelle's type system will reject all but one parse tree,
but will still inform you of the potential ambiguity. *}

inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
where
B_ty: "\<Gamma> \<turnstile> Bc v" |
Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"

declare btyping.intros [intro!]
inductive_cases [elim!]: "\<Gamma> \<turnstile> Not b" "\<Gamma> \<turnstile> And b1 b2" "\<Gamma> \<turnstile> Less a1 a2"

inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;;c2" |
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"

declare ctyping.intros [intro!]
inductive_cases [elim!]:
  "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;;c2"
  "\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
  "\<Gamma> \<turnstile> WHILE b DO c"

subsection "Well-typed Programs Do Not Get Stuck"

fun type :: "val \<Rightarrow> ty" where
"type (Iv i) = Ity" |
"type (Rv r) = Rty"

lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
by (cases v) simp_all

lemma type_eq_Rty[simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
by (cases v) simp_all

definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)
where "\<Gamma> \<turnstile> s  \<longleftrightarrow>  (\<forall>x. type (s x) = \<Gamma> x)"

lemma apreservation:
  "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
apply(induction arbitrary: v rule: atyping.induct)
apply (fastforce simp: styping_def)+
done

lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
proof(induction rule: atyping.induct)
  case (Plus_ty \<Gamma> a1 t a2)
  then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
  show ?case
  proof (cases v1)
    case Iv
    with Plus_ty v show ?thesis
      by(fastforce intro: taval.intros(4) dest!: apreservation)
  next
    case Rv
    with Plus_ty v show ?thesis
      by(fastforce intro: taval.intros(5) dest!: apreservation)
  qed
qed (auto intro: taval.intros)

lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
proof(induction rule: btyping.induct)
  case (Less_ty \<Gamma> a1 t a2)
  then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
    by (metis aprogress)
  show ?case
  proof (cases v1)
    case Iv
    with Less_ty v show ?thesis
      by (fastforce intro!: tbval.intros(4) dest!:apreservation)
  next
    case Rv
    with Less_ty v show ?thesis
      by (fastforce intro!: tbval.intros(5) dest!:apreservation)
  qed
qed (auto intro: tbval.intros)

theorem progress:
  "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
proof(induction rule: ctyping.induct)
  case Skip_ty thus ?case by simp
next
  case Assign_ty
  thus ?case by (metis Assign aprogress)
next
  case Seq_ty thus ?case by simp (metis Seq1 Seq2)
next
  case (If_ty \<Gamma> b c1 c2)
  then obtain bv where "tbval b s bv" by (metis bprogress)
  show ?case
  proof(cases bv)
    assume "bv"
    with `tbval b s bv` show ?case by simp (metis IfTrue)
  next
    assume "\<not>bv"
    with `tbval b s bv` show ?case by simp (metis IfFalse)
  qed
next
  case While_ty show ?case by (metis While)
qed

theorem styping_preservation:
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
proof(induction rule: small_step_induct)
  case Assign thus ?case
    by (auto simp: styping_def) (metis Assign(1,3) apreservation)
qed auto

theorem ctyping_preservation:
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'"
by (induct rule: small_step_induct) (auto simp: ctyping.intros)

abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"

theorem type_sound:
  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
apply(induction rule:star_induct)
apply (metis progress)
by (metis styping_preservation ctyping_preservation)

end

repo: jormungand


text:
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
(* instead, see the skeleton file ArchStateData_H.thy *)
(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(GD_GPL)
 *)

(*
	Kernel state and kernel monads, imports everything that SEL4.Model needs.
*)

chapter "Architecture Specific Kernel State and Monads"

theory ArchStateData_H
imports
  Arch_Structs_B
  ArchTypes_H
  ArchStructures_H
begin
context Arch begin global_naming ARM_H

datatype kernel_state =
    ARMKernelState "asid \<Rightarrow> ((machine_word) option)" "hardware_asid \<Rightarrow> (asid option)" hardware_asid "asid \<Rightarrow> ((hardware_asid * machine_word) option)" machine_word "machine_word list" "machine_word \<Rightarrow> arm_vspace_region_use"

primrec
  armKSKernelVSpace :: "kernel_state \<Rightarrow> machine_word \<Rightarrow> arm_vspace_region_use"
where
  "armKSKernelVSpace (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v6"

primrec
  armKSASIDTable :: "kernel_state \<Rightarrow> asid \<Rightarrow> ((machine_word) option)"
where
  "armKSASIDTable (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v0"

primrec
  armKSGlobalPD :: "kernel_state \<Rightarrow> machine_word"
where
  "armKSGlobalPD (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v4"

primrec
  armKSHWASIDTable :: "kernel_state \<Rightarrow> hardware_asid \<Rightarrow> (asid option)"
where
  "armKSHWASIDTable (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v1"

primrec
  armKSGlobalPTs :: "kernel_state \<Rightarrow> machine_word list"
where
  "armKSGlobalPTs (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v5"

primrec
  armKSNextASID :: "kernel_state \<Rightarrow> hardware_asid"
where
  "armKSNextASID (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v2"

primrec
  armKSASIDMap :: "kernel_state \<Rightarrow> asid \<Rightarrow> ((hardware_asid * machine_word) option)"
where
  "armKSASIDMap (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = v3"

primrec
  armKSKernelVSpace_update :: "((machine_word \<Rightarrow> arm_vspace_region_use) \<Rightarrow> (machine_word \<Rightarrow> arm_vspace_region_use)) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSKernelVSpace_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState v0 v1 v2 v3 v4 v5 (f v6)"

primrec
  armKSASIDTable_update :: "((asid \<Rightarrow> ((machine_word) option)) \<Rightarrow> (asid \<Rightarrow> ((machine_word) option))) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSASIDTable_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState (f v0) v1 v2 v3 v4 v5 v6"

primrec
  armKSGlobalPD_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSGlobalPD_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState v0 v1 v2 v3 (f v4) v5 v6"

primrec
  armKSHWASIDTable_update :: "((hardware_asid \<Rightarrow> (asid option)) \<Rightarrow> (hardware_asid \<Rightarrow> (asid option))) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSHWASIDTable_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState v0 (f v1) v2 v3 v4 v5 v6"

primrec
  armKSGlobalPTs_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSGlobalPTs_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState v0 v1 v2 v3 v4 (f v5) v6"

primrec
  armKSNextASID_update :: "(hardware_asid \<Rightarrow> hardware_asid) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSNextASID_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState v0 v1 (f v2) v3 v4 v5 v6"

primrec
  armKSASIDMap_update :: "((asid \<Rightarrow> ((hardware_asid * machine_word) option)) \<Rightarrow> (asid \<Rightarrow> ((hardware_asid * machine_word) option))) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
where
  "armKSASIDMap_update f (ARMKernelState v0 v1 v2 v3 v4 v5 v6) = ARMKernelState v0 v1 v2 (f v3) v4 v5 v6"

abbreviation (input)
  ARMKernelState_trans :: "(asid \<Rightarrow> ((machine_word) option)) \<Rightarrow> (hardware_asid \<Rightarrow> (asid option)) \<Rightarrow> (hardware_asid) \<Rightarrow> (asid \<Rightarrow> ((hardware_asid * machine_word) option)) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word \<Rightarrow> arm_vspace_region_use) \<Rightarrow> kernel_state" ("ARMKernelState'_ \<lparr> armKSASIDTable= _, armKSHWASIDTable= _, armKSNextASID= _, armKSASIDMap= _, armKSGlobalPD= _, armKSGlobalPTs= _, armKSKernelVSpace= _ \<rparr>")
where
  "ARMKernelState_ \<lparr> armKSASIDTable= v0, armKSHWASIDTable= v1, armKSNextASID= v2, armKSASIDMap= v3, armKSGlobalPD= v4, armKSGlobalPTs= v5, armKSKernelVSpace= v6 \<rparr> == ARMKernelState v0 v1 v2 v3 v4 v5 v6"

lemma armKSKernelVSpace_armKSKernelVSpace_update [simp]:
  "armKSKernelVSpace (armKSKernelVSpace_update f v) = f (armKSKernelVSpace v)"
  by (cases v) simp

lemma armKSKernelVSpace_armKSASIDTable_update [simp]:
  "armKSKernelVSpace (armKSASIDTable_update f v) = armKSKernelVSpace v"
  by (cases v) simp

lemma armKSKernelVSpace_armKSGlobalPD_update [simp]:
  "armKSKernelVSpace (armKSGlobalPD_update f v) = armKSKernelVSpace v"
  by (cases v) simp

lemma armKSKernelVSpace_armKSHWASIDTable_update [simp]:
  "armKSKernelVSpace (armKSHWASIDTable_update f v) = armKSKernelVSpace v"
  by (cases v) simp

lemma armKSKernelVSpace_armKSGlobalPTs_update [simp]:
  "armKSKernelVSpace (armKSGlobalPTs_update f v) = armKSKernelVSpace v"
  by (cases v) simp

lemma armKSKernelVSpace_armKSNextASID_update [simp]:
  "armKSKernelVSpace (armKSNextASID_update f v) = armKSKernelVSpace v"
  by (cases v) simp

lemma armKSKernelVSpace_armKSASIDMap_update [simp]:
  "armKSKernelVSpace (armKSASIDMap_update f v) = armKSKernelVSpace v"
  by (cases v) simp

lemma armKSASIDTable_armKSKernelVSpace_update [simp]:
  "armKSASIDTable (armKSKernelVSpace_update f v) = armKSASIDTable v"
  by (cases v) simp

lemma armKSASIDTable_armKSASIDTable_update [simp]:
  "armKSASIDTable (armKSASIDTable_update f v) = f (armKSASIDTable v)"
  by (cases v) simp

lemma armKSASIDTable_armKSGlobalPD_update [simp]:
  "armKSASIDTable (armKSGlobalPD_update f v) = armKSASIDTable v"
  by (cases v) simp

lemma armKSASIDTable_armKSHWASIDTable_update [simp]:
  "armKSASIDTable (armKSHWASIDTable_update f v) = armKSASIDTable v"
  by (cases v) simp

lemma armKSASIDTable_armKSGlobalPTs_update [simp]:
  "armKSASIDTable (armKSGlobalPTs_update f v) = armKSASIDTable v"
  by (cases v) simp

lemma armKSASIDTable_armKSNextASID_update [simp]:
  "armKSASIDTable (armKSNextASID_update f v) = armKSASIDTable v"
  by (cases v) simp

lemma armKSASIDTable_armKSASIDMap_update [simp]:
  "armKSASIDTable (armKSASIDMap_update f v) = armKSASIDTable v"
  by (cases v) simp

lemma armKSGlobalPD_armKSKernelVSpace_update [simp]:
  "armKSGlobalPD (armKSKernelVSpace_update f v) = armKSGlobalPD v"
  by (cases v) simp

lemma armKSGlobalPD_armKSASIDTable_update [simp]:
  "armKSGlobalPD (armKSASIDTable_update f v) = armKSGlobalPD v"
  by (cases v) simp

lemma armKSGlobalPD_armKSGlobalPD_update [simp]:
  "armKSGlobalPD (armKSGlobalPD_update f v) = f (armKSGlobalPD v)"
  by (cases v) simp

lemma armKSGlobalPD_armKSHWASIDTable_update [simp]:
  "armKSGlobalPD (armKSHWASIDTable_update f v) = armKSGlobalPD v"
  by (cases v) simp

lemma armKSGlobalPD_armKSGlobalPTs_update [simp]:
  "armKSGlobalPD (armKSGlobalPTs_update f v) = armKSGlobalPD v"
  by (cases v) simp

lemma armKSGlobalPD_armKSNextASID_update [simp]:
  "armKSGlobalPD (armKSNextASID_update f v) = armKSGlobalPD v"
  by (cases v) simp

lemma armKSGlobalPD_armKSASIDMap_update [simp]:
  "armKSGlobalPD (armKSASIDMap_update f v) = armKSGlobalPD v"
  by (cases v) simp

lemma armKSHWASIDTable_armKSKernelVSpace_update [simp]:
  "armKSHWASIDTable (armKSKernelVSpace_update f v) = armKSHWASIDTable v"
  by (cases v) simp

lemma armKSHWASIDTable_armKSASIDTable_update [simp]:
  "armKSHWASIDTable (armKSASIDTable_update f v) = armKSHWASIDTable v"
  by (cases v) simp

lemma armKSHWASIDTable_armKSGlobalPD_update [simp]:
  "armKSHWASIDTable (armKSGlobalPD_update f v) = armKSHWASIDTable v"
  by (cases v) simp

lemma armKSHWASIDTable_armKSHWASIDTable_update [simp]:
  "armKSHWASIDTable (armKSHWASIDTable_update f v) = f (armKSHWASIDTable v)"
  by (cases v) simp

lemma armKSHWASIDTable_armKSGlobalPTs_update [simp]:
  "armKSHWASIDTable (armKSGlobalPTs_update f v) = armKSHWASIDTable v"
  by (cases v) simp

lemma armKSHWASIDTable_armKSNextASID_update [simp]:
  "armKSHWASIDTable (armKSNextASID_update f v) = armKSHWASIDTable v"
  by (cases v) simp

lemma armKSHWASIDTable_armKSASIDMap_update [simp]:
  "armKSHWASIDTable (armKSASIDMap_update f v) = armKSHWASIDTable v"
  by (cases v) simp

lemma armKSGlobalPTs_armKSKernelVSpace_update [simp]:
  "armKSGlobalPTs (armKSKernelVSpace_update f v) = armKSGlobalPTs v"
  by (cases v) simp

lemma armKSGlobalPTs_armKSASIDTable_update [simp]:
  "armKSGlobalPTs (armKSASIDTable_update f v) = armKSGlobalPTs v"
  by (cases v) simp

lemma armKSGlobalPTs_armKSGlobalPD_update [simp]:
  "armKSGlobalPTs (armKSGlobalPD_update f v) = armKSGlobalPTs v"
  by (cases v) simp

lemma armKSGlobalPTs_armKSHWASIDTable_update [simp]:
  "armKSGlobalPTs (armKSHWASIDTable_update f v) = armKSGlobalPTs v"
  by (cases v) simp

lemma armKSGlobalPTs_armKSGlobalPTs_update [simp]:
  "armKSGlobalPTs (armKSGlobalPTs_update f v) = f (armKSGlobalPTs v)"
  by (cases v) simp

lemma armKSGlobalPTs_armKSNextASID_update [simp]:
  "armKSGlobalPTs (armKSNextASID_update f v) = armKSGlobalPTs v"
  by (cases v) simp

lemma armKSGlobalPTs_armKSASIDMap_update [simp]:
  "armKSGlobalPTs (armKSASIDMap_update f v) = armKSGlobalPTs v"
  by (cases v) simp

lemma armKSNextASID_armKSKernelVSpace_update [simp]:
  "armKSNextASID (armKSKernelVSpace_update f v) = armKSNextASID v"
  by (cases v) simp

lemma armKSNextASID_armKSASIDTable_update [simp]:
  "armKSNextASID (armKSASIDTable_update f v) = armKSNextASID v"
  by (cases v) simp

lemma armKSNextASID_armKSGlobalPD_update [simp]:
  "armKSNextASID (armKSGlobalPD_update f v) = armKSNextASID v"
  by (cases v) simp

lemma armKSNextASID_armKSHWASIDTable_update [simp]:
  "armKSNextASID (armKSHWASIDTable_update f v) = armKSNextASID v"
  by (cases v) simp

lemma armKSNextASID_armKSGlobalPTs_update [simp]:
  "armKSNextASID (armKSGlobalPTs_update f v) = armKSNextASID v"
  by (cases v) simp

lemma armKSNextASID_armKSNextASID_update [simp]:
  "armKSNextASID (armKSNextASID_update f v) = f (armKSNextASID v)"
  by (cases v) simp

lemma armKSNextASID_armKSASIDMap_update [simp]:
  "armKSNextASID (armKSASIDMap_update f v) = armKSNextASID v"
  by (cases v) simp

lemma armKSASIDMap_armKSKernelVSpace_update [simp]:
  "armKSASIDMap (armKSKernelVSpace_update f v) = armKSASIDMap v"
  by (cases v) simp

lemma armKSASIDMap_armKSASIDTable_update [simp]:
  "armKSASIDMap (armKSASIDTable_update f v) = armKSASIDMap v"
  by (cases v) simp

lemma armKSASIDMap_armKSGlobalPD_update [simp]:
  "armKSASIDMap (armKSGlobalPD_update f v) = armKSASIDMap v"
  by (cases v) simp

lemma armKSASIDMap_armKSHWASIDTable_update [simp]:
  "armKSASIDMap (armKSHWASIDTable_update f v) = armKSASIDMap v"
  by (cases v) simp

lemma armKSASIDMap_armKSGlobalPTs_update [simp]:
  "armKSASIDMap (armKSGlobalPTs_update f v) = armKSASIDMap v"
  by (cases v) simp

lemma armKSASIDMap_armKSNextASID_update [simp]:
  "armKSASIDMap (armKSNextASID_update f v) = armKSASIDMap v"
  by (cases v) simp

lemma armKSASIDMap_armKSASIDMap_update [simp]:
  "armKSASIDMap (armKSASIDMap_update f v) = f (armKSASIDMap v)"
  by (cases v) simp

definition
newKernelState :: "paddr \<Rightarrow> (kernel_state * paddr list)"
where
"newKernelState data_start \<equiv>
    let
        alignToBits = (\<lambda>  addr b. (((addr - 1) `~shiftR~` b) + 1) `~shiftL~` b);
        globalsFrame = data_start `~alignToBits~` pageBits;
        globalsFrameTop = globalsFrame + bit pageBits;
        globalPTs = globalsFrameTop `~alignToBits~` pageBits;
        globalPTsTop = globalPTs + bit pageBits;
        globalPD = globalPTsTop `~alignToBits~` pdBits;
        globalPDTop = globalPD + bit pdBits;
        frames = globalsFrame #
            [globalPTs, globalPTs + bit pageBits  .e.  globalPTsTop - 1] @
            [globalPD, globalPD + bit pageBits  .e.  globalPDTop - 1];
        state = ARMKernelState_ \<lparr>
            armKSASIDTable= funPartialArray (const Nothing) (0, (1 `~shiftL~` asidHighBits) - 1),
            armKSHWASIDTable= funArray (const Nothing),
            armKSNextASID= minBound,
            armKSASIDMap= funPartialArray (const Nothing) asidRange,
            armKSGlobalPD= ptrFromPAddr globalPD,
            armKSGlobalPTs= map ptrFromPAddr
                [globalPTs, globalPTs + bit ptBits  .e.  globalPTsTop- 1],
            armKSKernelVSpace=
                (\<lambda> vref. if vref < mask 20 then ArmVSpaceKernelWindow
                                            else ArmVSpaceInvalidRegion) \<rparr>
    in
                                   (state, frames)"

end

end


text:
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_step
imports CSP_F_domain CSP_T_law_step
begin

(*****************************************************************

         1. step laws
         2.
         3.
         4.

 *****************************************************************)

(*********************************************************
                    stop expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_STOP_step: "STOP =F[M1,M2] ? :{} -> Pf"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_STOP_step)
apply (simp add: failures_iff)
done

(* to avoide producing free variables in tactics *)

lemma cspF_STOP_step_DIV: "STOP =F[M1,M2] ? x:{} -> DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_STOP_step)
apply (simp add: failures_iff)
done

(*********************************************************
                    Act_prefix expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Act_prefix_step: "a -> P =F[M,M] ? x:{a} -> P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Act_prefix_step)
apply (simp add: failures_iff)
done

(*********************************************************
                    Ext choice expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Ext_choice_step:
  "(? :X -> Pf) [+] (? :Y -> Qf) =F[M,M]
      ? x:(X Un Y) ->
                (IF (x : X & x : Y) THEN (Pf x |~| Qf x)
                 ELSE IF (x : X) THEN Pf x
                 ELSE Qf x)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_step)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all)
 apply (force)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI)
 apply (simp)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI)
 apply (simp)
 apply (simp add: in_traces)
 apply (simp add: in_traces)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all)
 apply (force)

 apply (case_tac "a : Y")
 apply (simp_all add: in_failures)

 apply (case_tac "a : X")
 apply (simp_all add: in_failures)
done

(*********************************************************
                    Parallel expansion
 *********************************************************)

(* set 1 *)

lemma cspF_Parallel_step_set1:
  "[| Ya - insert Tick (Ev ` X) = Za - insert Tick (Ev ` X) ;
       Ev ` Y Int Ya = {}; Ev ` Z Int Za = {} |]
   ==> Ev ` (X Int Y Int Z) Int (Ya Un Za) = {}"
by (auto)

(* set 2 *)

lemma cspF_Parallel_step_set2:
  "[| Ya - insert Tick (Ev ` X) = Za - insert Tick (Ev ` X) ;
       Ev ` Y Int Ya = {}; Ev ` Z Int Za = {} |]
   ==> Ev ` (Y - X) Int (Ya Un Za) = {}"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: inj_image_diff_dist)
 apply (simp add: in_Ev_set)
 apply (elim conjE exE)

 apply (erule disjE)
  apply (fast)
    (* *)
  apply (simp)
   apply (case_tac "Ev a : Ya")
   apply (fast)
   apply (rotate_tac 1)
   apply (erule equalityE)
   apply (rotate_tac -1)
   apply (erule subsetE)
   apply (drule_tac x="Ev a" in bspec, fast)
   apply (simp)
  apply (fast)
done

(* set 3 *)

lemma cspF_Parallel_step_set3:
  "[| Ya - insert Tick (Ev ` X) = Za - insert Tick (Ev ` X) ;
       Ev ` Y Int Ya = {}; Ev ` Z Int Za = {} |]
   ==> Ev ` (Z - X) Int (Ya Un Za) = {}"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: inj_image_diff_dist)
 apply (simp add: in_Ev_set)
 apply (elim conjE exE)
 apply (erule disjE)
  apply (simp)
   apply (case_tac "Ev a : Za")
   apply (fast)
   apply (rotate_tac 1)
   apply (erule equalityE)
   apply (erule subsetE)
   apply (drule_tac x="Ev a" in bspec, fast)
   apply (simp)
  apply (fast)
    (* *)
  apply (simp)
done

(* set 4 *)

lemma cspF_Parallel_step_set4:
  "Ev ` (X Int Y Int Z Un (Y - X) Un (Z - X)) Int Xa = {}
   ==> Xa =
       Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Y) Un
      (Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Z))"
by (auto)

(* set 5 *)

lemma cspF_Parallel_step_set5:
  "Ev ` (X Int Y Int Z Un (Y - X) Un (Z - X)) Int Xa = {}
   ==> Ev ` Y Int
      (Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Y)) = {} &
       Ev ` Z Int
      (Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Z)) = {}"
by (auto)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Parallel_step:
  "(? :Y -> Pf) |[X]| (? :Z -> Qf) =F[M,M]
      ? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ? x:Z -> Qf x)
                                     |~| (? x:Y -> Pf x |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ? x:Z -> Qf x)
               ELSE (? x:Y -> Pf x |[X]| Qf x)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_step)
apply (rule order_antisym)

(* => *)
apply (rule)
apply (simp add: in_failures)
apply (elim disjE conjE exE)

 (* (nil,nil) *)
 apply (simp add: image_Un Int_Un_distrib2)
 apply (simp add: cspF_Parallel_step_set1
                  cspF_Parallel_step_set2
                  cspF_Parallel_step_set3)

 (* (nil,Ev) *)
 apply (simp)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="s" in spec)

 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: par_tr_head)

 apply (rule_tac x="aa" in exI)
 apply (rule_tac x="sc" in exI)
 apply (simp)

 apply (case_tac "aa : Y")
  apply (simp)
  apply (rule disjI2)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="sb" in exI)
  apply (simp)
  (* "aa ~: Y" *)
  apply (simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="sb" in exI)
  apply (simp)

 (* (Ev,nil) *)
 apply (simp)
 apply (drule_tac x="s" in spec)

 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: par_tr_head)

 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sc" in exI)
 apply (simp)

 apply (case_tac "a : Z")
  apply (simp)
  apply (rule disjI1)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp)
  (* "a ~: Z" *)
  apply (simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp)

 (* (Ev,Ev) *)
 apply (drule_tac x="s" in spec)
 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: par_tr_head)
 apply (elim disjE conjE exE, simp)

  (* sync *)
  apply (rule_tac x="aa" in exI)
  apply (rule_tac x="sd" in exI)
  apply (simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="sc" in exI)
  apply (simp)

  (* left *)
  apply (simp)
  apply (rule_tac x="a" in exI)
  apply (rule_tac x="sd" in exI)
  apply (simp)

  apply (case_tac "a : Z")
   apply (simp)
   apply (rule disjI1)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="<Ev aa> ^^^ sc" in exI)
   apply (simp)
   (* "a ~: Z" *)
   apply (simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="<Ev aa> ^^^ sc" in exI)
   apply (simp)

  (* right *)
  apply (simp)
  apply (rule_tac x="aa" in exI)
  apply (rule_tac x="sd" in exI)
  apply (simp)

  apply (case_tac "aa : Y")
   apply (simp)
   apply (rule disjI2)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="<Ev a> ^^^ sb" in exI)
   apply (rule_tac x="sc" in exI)
   apply (simp)
   (* "aa ~: Y" *)
   apply (simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="<Ev a> ^^^ sb" in exI)
   apply (rule_tac x="sc" in exI)
   apply (simp)

(* <= *)

apply (rule)
apply (simp add: in_failures)
apply (elim disjE conjE exE)

 (* nil *)
 apply (simp)
 apply (rule_tac x="(Xa - insert Tick (Ev ` X)) Un
                   ((Xa Int insert Tick (Ev ` X)) - Ev ` Y)" in exI)
 apply (rule_tac x="(Xa - insert Tick (Ev ` X)) Un
                   ((Xa Int insert Tick (Ev ` X)) - Ev ` Z)" in exI)
 apply (simp add: cspF_Parallel_step_set4)
 apply (rule conjI, force)
 apply (simp add: cspF_Parallel_step_set5)

 (* sync *)
 apply (simp add: in_failures)
 apply (elim conjE exE, simp)
 apply (rule_tac x="Ya" in exI)
 apply (rule_tac x="Za" in exI)
 apply (simp)
 apply (rule_tac x="<Ev a> ^^^ sb" in exI)
 apply (rule_tac x="<Ev a> ^^^ t" in exI)
 apply (simp add: par_tr_head)

 (* left *)
 apply (case_tac "a : Z")
  apply (simp add: in_failures)
  apply (erule disjE)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="<Ev a> ^^^ sb" in exI)
   apply (rule_tac x="t" in exI)
   apply (simp add: par_tr_head)
   (* *)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="<Ev a> ^^^ t" in exI)
   apply (simp add: par_tr_head)
  (* "a ~: Z" *)
  apply (simp add: in_failures)
  apply (elim conjE exE, simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="<Ev a> ^^^ sb" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp add: par_tr_head)

 (* right *)
 apply (case_tac "a : Y")
  apply (simp add: in_failures)
  apply (erule disjE)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="<Ev a> ^^^ sb" in exI)
   apply (rule_tac x="t" in exI)
   apply (simp add: par_tr_head)
   (* *)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="<Ev a> ^^^ t" in exI)
   apply (simp add: par_tr_head)
  (* "a ~: Y" *)
  apply (simp add: in_failures)
  apply (elim conjE exE, simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<Ev a> ^^^ t" in exI)
  apply (simp add: par_tr_head)
done

(*********************************************************
                      Hide expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Hiding_step:
  "(? :Y -> Pf) -- X =F[M,M]
      IF (Y Int X = {}) THEN (? x:Y -> (Pf x -- X))
                         ELSE ((? x:(Y-X) -> (Pf x -- X))
                               [> (! x:(Y Int X) .. (Pf x -- X)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Hiding_step)
apply (rule order_antisym)

 (* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE exE)
 apply (erule disjE)
  (* not hidden *)
  apply (simp)
  apply (case_tac "Y Int X ~= {}", fast)
  apply (simp)
  apply (fast)
  (* hidden *)
  apply (elim conjE exE)
   apply (simp)

  apply (case_tac "a : X")
  apply (case_tac "Y Int X = {}", fast)
   apply (simp)
   apply (case_tac "sb --tr X = <>")
   apply (rule disjI1)
   apply (simp)
   apply (rule_tac x="a" in bexI)
   apply (rule_tac x="sb" in exI)
   apply (simp)
   apply (simp)

   apply (rule disjI2)
   apply (simp)
   apply (rule disjI2)
   apply (rule_tac x="a" in bexI)
   apply (rule_tac x="sb" in exI)
   apply (simp)
   apply (simp)

  (* a ~: X *)
   apply (case_tac "Y Int X = {}")
    apply (simp)
    apply (fast)
   (* Y Int X ~= {} *)
    apply (simp)
    apply (fast)

 (* <= *)
 apply (rule)
 apply (case_tac "Y Int X = {}")
  apply (simp add: in_failures)
  apply (erule disjE)
   apply (rule_tac x="<>" in exI)
   apply (simp)
   apply (fast)
  (* *)
   apply (elim conjE exE)
   apply (case_tac "a : X", fast)
   apply (rule_tac x="<Ev a> ^^^ sb" in exI)
   apply (simp)

 (* Y Int X ~= {} *)
 apply (simp add: in_failures_IF)
 apply (simp add: in_failures_Timeout)
 apply (elim disjE)
  (* 1 *)
  apply (simp add: in_failures)
  apply (elim conjE exE bexE)
  apply (rule_tac x="<Ev a> ^^^ sa" in exI)
  apply (simp)

  (* 2 *)
  apply (simp add: in_failures)
  apply (elim conjE, simp)
  apply (elim conjE exE)
  apply (rule_tac x="<Ev a> ^^^ sb" in exI)
  apply (simp)
  (* 3 *)
  apply (simp add: in_failures)
  apply (simp add: in_traces)
done

(*********************************************************
                    Renaming expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Renaming_step:
  "(? :X -> Pf) [[r]] =F[M,M]
    ? y:(r `` X) -> (! x:{x. x:X & (x,y):r} .. (Pf x)[[r]])"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_step)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
  (* 1 *)
  apply (simp add: ren_inv_def)
  apply (force)
  (* 2 *)
  apply (simp add: ren_tr_decompo)
  apply (elim conjE exE)
  apply (rule disjI2)
  apply (rule_tac x="b" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)
  apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
  (* 1 *)
  apply (simp add: ren_inv_def)
  apply (force)
  (* 2 *)
  apply (rule_tac x="<Ev aa> ^^^ sb" in exI)
  apply (simp)
done

(*********************************************************
            Sequential composition expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Seq_compo_step:
  "(? :X -> Pf) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_step)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE exE disjE)

 apply (simp_all)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="sa" in spec)
 apply (erule disjE)
 apply (simp add: in_traces)
 apply (erule disjE)
 apply (simp)

 apply (elim conjE exE)
 apply (simp)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sb ^^^ t" in exI)
 apply (simp add: appt_assoc)
 apply (simp add: in_traces)
 apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (erule disjE)
 (* 1 *)
  apply (rule disjI1)
  apply (simp)
  apply (fast)

 (* 2 *)
  apply (elim conjE exE disjE)

  (* 2-1 *)
   apply (simp)

  (* 2-2 *)
   apply (rule disjI2)
   apply (simp)
   apply (rule_tac x="<Ev a> ^^^ sb" in exI)
   apply (rule_tac x="t" in exI, simp)
   apply (simp add: appt_assoc)
   apply (simp add: in_traces)
done

(*********************************************************
                    Depth_rest expansion
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Depth_rest_step:
  "(? :X -> Pf) |. (Suc n) =F[M,M] ? x:X -> (Pf x |. n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_step)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sb" in exI)
 apply (simp)
 apply (rule disjI2)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="sa" in spec)
 apply (elim conjE exE disjE)
 apply (simp_all)
 apply (simp add: appt_assoc)
 apply (force)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all)
 apply (rule_tac x="<Ev a> ^^^ sb" in exI)
 apply (simp add: appt_assoc)
done

(*********************************************************)

lemmas cspF_step = cspF_STOP_step       cspF_Act_prefix_step
                   cspF_Ext_choice_step cspF_Parallel_step
                   cspF_Hiding_step     cspF_Renaming_step
                   cspF_Seq_compo_step  cspF_Depth_rest_step

lemmas cspF_light_step = cspF_STOP_step  cspF_Act_prefix_step

lemmas cspF_step_rw = cspF_STOP_step_DIV       cspF_Act_prefix_step
                   cspF_Ext_choice_step cspF_Parallel_step
                   cspF_Hiding_step     cspF_Renaming_step
                   cspF_Seq_compo_step  cspF_Depth_rest_step

lemmas cspF_light_step_rw = cspF_STOP_step_DIV  cspF_Act_prefix_step

end

author: pefribeiro

repo: CSP-Prover


text:
(*  Title:      A locale for and a characterization of maximal normal subgroups
    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
    Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
*)

theory MaximalNormalSubgroups
imports
  SubgroupsAndNormalSubgroups
  SimpleGroups
begin

section \<open>Facts about maximal normal subgroups\<close>

text \<open>A maximal normal subgroup of $G$ is a normal subgroup which is not contained in other any proper
  normal subgroup of $G$.\<close>

locale max_normal_subgroup = normal +
  assumes proper:"H \<noteq> carrier G"
  assumes max_normal:"\<And>J. J \<lhd> G \<Longrightarrow> J \<noteq> H \<Longrightarrow> J \<noteq> carrier G \<Longrightarrow> \<not> (H \<subseteq> J)"

text \<open>Another characterization of maximal normal subgroups: The factor group is simple.\<close>

theorem (in normal) max_normal_simple_quotient:
  assumes finite:"finite (carrier G)"
  shows "max_normal_subgroup H G = simple_group (G Mod H)"
proof
  assume "max_normal_subgroup H G"
  then interpret maxH: max_normal_subgroup H G.
  show "simple_group (G Mod H)" unfolding simple_group_def simple_group_axioms_def
  proof (intro conjI factorgroup_is_group allI impI disjCI)
    from finite factgroup_finite factorgroup_is_group group.finite_pos_order have gt0:"0 < card (rcosets H)"
      unfolding FactGroup_def order_def by force
    from maxH.proper finite have "carrier (G Mod H) \<noteq> {\<one>\<^bsub>G Mod H\<^esub>}" using fact_group_trivial_iff by auto
    hence "1 \<noteq> order (G Mod H)" using factorgroup_is_group group.order_one_triv_iff by metis
    with gt0 show "1 < order (G Mod H)" unfolding order_def FactGroup_def by auto
  next
    fix A'
    assume A'normal:"A' \<lhd> G Mod H" and A'nottriv:"A' \<noteq> {\<one>\<^bsub>G Mod H\<^esub>}"
    define A where "A = \<Union>A'"
    have A2:"A \<lhd> G" using A'normal unfolding A_def by (rule factgroup_subgroup_union_normal)
    have "H \<in> A'" using A'normal normal_imp_subgroup subgroup.one_closed unfolding FactGroup_def by force
    hence "H \<subseteq> A" unfolding A_def by auto
    hence A1:"H \<lhd> (G\<lparr>carrier := A\<rparr>)" using A2 is_normal by (metis is_subgroup maxH.max_normal normal_restrict_supergroup subgroup_self)
    have A3:"A' = rcosets\<^bsub>G\<lparr>carrier := A\<rparr>\<^esub> H"
      unfolding A_def using factgroup_subgroup_union_factor A'normal normal_imp_subgroup by auto
    from A1 interpret normalHA: normal H "(G\<lparr>carrier := A\<rparr>)" by metis
    have "H \<subseteq> A" using normalHA.is_subgroup subgroup.subset by force
    with A2 have "A = H \<or> A = carrier G" using maxH.max_normal by auto
    thus "A' = carrier (G Mod H)"
    proof
      assume "A = H"
      hence "carrier (G\<lparr>carrier := A\<rparr> Mod H) = {\<one>\<^bsub>(G\<lparr>carrier := A\<rparr> Mod H)\<^esub>}" by (metis finite is_group normalHA.fact_group_trivial_iff normalHA.subgroup_self normalHA.subset subgroup_finite subgroup_of_restricted_group subgroup_of_subgroup subset_antisym)
      also have "... = {\<one>\<^bsub>G Mod H\<^esub>}" unfolding FactGroup_def by auto
      finally have "A' = {\<one>\<^bsub>G Mod H\<^esub>}" using A3 unfolding FactGroup_def by simp
      with A'nottriv show ?thesis..
    next
      assume "A = carrier G"
      hence "(G\<lparr>carrier := A\<rparr> Mod H) = G Mod H" by auto
      thus "A' = carrier (G Mod H)" using A3 unfolding FactGroup_def by simp
    qed
  qed
next
  assume simple:"simple_group (G Mod H)"
  show "max_normal_subgroup H G"
  proof
    from simple have "carrier (G Mod H) \<noteq> {\<one>\<^bsub>G Mod H\<^esub>}" unfolding simple_group_def simple_group_axioms_def order_def by auto
    with finite fact_group_trivial_iff show "H \<noteq> carrier G" by auto
  next
    fix A
    assume A:"A \<lhd> G" "A \<noteq> H" "A \<noteq> carrier G"
    show "\<not> H \<subseteq> A"
    proof
      assume HA:"H \<subseteq> A"
      hence "H \<lhd> (G\<lparr>carrier := A\<rparr>)" by (metis A(1) inv_op_closed2 is_subgroup normal_inv_iff normal_restrict_supergroup)
      then interpret normalHA: normal H "(G\<lparr>carrier := A\<rparr>)" by simp
      from finite have finiteA:"finite A" using A(1) normal_imp_subgroup by (metis subgroup_finite)
      have "rcosets\<^bsub>(G\<lparr>carrier := A\<rparr>)\<^esub> H \<lhd> G Mod H" using normality_factorization is_normal HA A(1) by auto
      with simple have "rcosets\<^bsub>(G\<lparr>carrier := A\<rparr>)\<^esub> H = {\<one>\<^bsub>G Mod H\<^esub>} \<or> rcosets\<^bsub>(G\<lparr>carrier := A\<rparr>)\<^esub> H = carrier (G Mod H)"
        unfolding simple_group_def simple_group_axioms_def by auto
      thus "False"
      proof
        assume "rcosets\<^bsub>G\<lparr>carrier := A\<rparr>\<^esub> H = {\<one>\<^bsub>G Mod H\<^esub>}"
        hence "rcosets\<^bsub>G\<lparr>carrier := A\<rparr>\<^esub> H = {\<one>\<^bsub>(G\<lparr>carrier := A\<rparr>) Mod H\<^esub>}" unfolding FactGroup_def by auto
        with finiteA have "H = A" using normalHA.fact_group_trivial_iff unfolding FactGroup_def by auto
        with A(2) show ?thesis by simp
      next
        assume AHGH:"rcosets\<^bsub>G\<lparr>carrier := A\<rparr>\<^esub> H = carrier (G Mod H)"
        have "A = carrier G" unfolding FactGroup_def RCOSETS_def
        proof
          show "A \<subseteq> carrier G" using A(1) normal_imp_subgroup subgroup.subset by metis
        next
          show "carrier G \<subseteq> A"
          proof
            fix x
            assume x:"x \<in> carrier G"
            hence "H #> x \<in> rcosets H" unfolding RCOSETS_def by auto
            with AHGH have "H #> x \<in> rcosets\<^bsub>G\<lparr>carrier := A\<rparr>\<^esub> H" unfolding FactGroup_def by simp
            then obtain x' where x':"x' \<in> A" "H #>x = H #>\<^bsub>G\<lparr>carrier := A\<rparr>\<^esub> x'" unfolding RCOSETS_def by auto
            hence "H #> x = H #> x'" unfolding r_coset_def by auto
            hence "x \<in> H #> x'" by (metis is_subgroup rcos_self x)
            hence "x \<in> A #> x'" using HA unfolding r_coset_def by auto
            thus "x \<in> A" using x'(1) unfolding r_coset_def using subgroup.m_closed A(1) normal_imp_subgroup by force
          qed
        qed
        with A(3) show ?thesis by simp
      qed
    qed
  qed
qed

end