header {* Semantics *} 

theory Semantics
imports Sequence Intensional
begin

text {* This theory provides a shallow embedding of the
 TLA* semantics. *}

section "Types of Formulas"

types ('a,'b) formfun = "'a seq \<Rightarrow> 'b"
           'a formula = "('a,bool) formfun"
        ('a,'b) stfun = "'a \<Rightarrow> 'b"
	    'a stpred = "('a,bool) stfun"

instance
 "*" :: (type,type) world ..

instance 
 "*" :: (world,world) world ..

instance
  "fun" :: (type,world) world ..

instance 
 "fun" :: (type,type) world ..

instance
 "fun" :: (world,world) world ..

text {* Pair and function are instantiated to be of type class world.
  This allows use of the lifted intensional logic for formulas, and 
  standard logical connectives can therefore be used. *}

section "Semantics of TLA*"

text {* The semantics of TLA* is defined *}

constdefs

always :: "'a formula \<Rightarrow> 'a formula" 
"always F \<equiv> \<lambda> s. \<forall> n. (s |\<^sub>s n) \<Turnstile> F"

nexts :: "('a,'b) formfun \<Rightarrow> ('a,'b) formfun" 
"nexts F \<equiv> \<lambda> s. (tail s) \<Turnstile> F"

before :: "('a,'b) stfun \<Rightarrow> ('a,'b) formfun"
"before f \<equiv> \<lambda> s. (first s) \<Turnstile> f"

after :: "('a,'b) stfun \<Rightarrow> ('a,'b) formfun"
"after f \<equiv> nexts (before f)"

unch  :: "('a,'b) stfun \<Rightarrow> 'a formula" 
"unch v \<equiv> \<lambda> s. s \<Turnstile> (after v) = (before v)"

action :: "'a formula \<Rightarrow> ('a,'b) stfun \<Rightarrow> 'a formula"
"action P v \<equiv> \<lambda> s. \<forall> i. ((s |\<^sub>s i) \<Turnstile> P) \<or> ((s |\<^sub>s i) \<Turnstile> unch v)"

subsection "Concrete Syntax"

text{* This is the concrete syntax for the (abstract) operator above *}

syntax
 "_always" :: "lift \<Rightarrow> lift" ("([]_)" [40] 90)
 "_nexts" :: "lift \<Rightarrow> lift" ("(Next _)" [40] 90)
 "_action" :: "[lift,lift] \<Rightarrow> lift" ("([][_]'_(_))" [20,1000] 90)
 "_before"    :: "lift \<Rightarrow> lift"  ("($_)" [100] 99)
 "_after"     :: "lift \<Rightarrow> lift"  ("(_$)" [100] 99)
 "_prime"     :: "lift \<Rightarrow> lift"  ("(_`)" [100] 99)  
 "_unch"     :: "lift \<Rightarrow> lift"  ("(Unchanged _)" [100] 99) 
 "TEMP"  :: "lift \<Rightarrow> 'b" ("(TEMP _)")

translations
 "_always" \<rightleftharpoons> "always"
 "_nexts" \<rightleftharpoons> "nexts"
 "_action" \<rightleftharpoons> "action"
 "_before"    \<rightleftharpoons> "before" 
 "_after"     \<rightleftharpoons> "after" 
 "_prime"     \<rightharpoonup> "after"
 "_unch"     \<rightleftharpoons> "unch" 
 "TEMP F" \<rightharpoonup> "(F:: (nat \<Rightarrow> _) \<Rightarrow> _)"

syntax (xsymbols)
 "_always" :: "lift \<Rightarrow> lift" ("(\<box>_)" [40] 90) 
 "_nexts" :: "lift \<Rightarrow> lift" ("(\<circ>_)" [40] 90) 
 "_action" :: "[lift,lift] \<Rightarrow> lift" ("(\<box>[_]'_(_))" [20,1000] 90)

section "Abbreviations"

text {* Some normal temporal abbreviations are given, with their
 concrete syntax. *}

constdefs

actrans :: "'a formula \<Rightarrow> ('a,'b) stfun \<Rightarrow> 'a formula"
"actrans P v \<equiv> TEMP(P \<or> unch v)"

eventually :: "'a formula \<Rightarrow> 'a formula"
"eventually F \<equiv> LIFT(\<not>\<box>\<not>F)"

angle_action :: "'a formula \<Rightarrow> ('a,'b) stfun \<Rightarrow> 'a formula"
"angle_action P v \<equiv> LIFT(\<not>\<box>[\<not>P]_v)"

angle_actrans :: "'a formula \<Rightarrow> ('a,'b) stfun \<Rightarrow> 'a formula"
"angle_actrans P v \<equiv> TEMP(\<not> actrans LIFT(\<not>P) v)"

leadsto :: "'a formula \<Rightarrow> 'a formula \<Rightarrow> 'a formula"
"leadsto P Q \<equiv> LIFT \<box>(P \<longrightarrow> eventually Q)"


subsection "Concrete Syntax"

syntax
  "_actrans" :: "[lift,lift] \<Rightarrow> lift" ("([_]'_(_))" [20] 90)
  "_eventually" :: "lift \<Rightarrow> lift" ("(<>_)" [40] 90)
  "_angle_action" :: "[lift,lift] \<Rightarrow> lift" ("(<><_>'_(_))" [20,1000] 90)
  "_angle_actrans" :: "[lift,lift] \<Rightarrow> lift" ("(<_>'_(_))" [20,1000] 90)
  "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ ~> _)" [40,40] 90)

translations 
  "_actrans" \<rightleftharpoons> "actrans"
  "_eventually" \<rightleftharpoons> "eventually"
  "_angle_action" \<rightleftharpoons> "angle_action"
  "_angle_actrans" \<rightleftharpoons> "angle_actrans"
  "_leadsto" \<rightleftharpoons> "leadsto"

syntax (xsymbols)
  "_eventually" :: "lift \<Rightarrow> lift" ("(\<diamond>_)" [40] 90)
  "_angle_action" :: "[lift,lift] \<Rightarrow> lift" ("(\<diamond>\<langle>_\<rangle>'_(_))" [20,1000] 90)
  "_angle_actrans" :: "[lift,lift] \<Rightarrow> lift" ("(\<langle>_\<rangle>'_(_))" [20,1000] 90)
  "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ \<leadsto> _)" [40,40] 90)

section "Properties of Operators"

text {* The following two lemmas shows that these operators has the obvious semantics. *}

lemma eventually_defs: "(w \<Turnstile> \<diamond> F) = (\<exists> n. (w |\<^sub>s n) \<Turnstile> F)"
proof
  assume a1: "(w \<Turnstile> \<diamond> F)"
  hence "w \<Turnstile> \<not>\<box>\<not>F" by (unfold eventually_def)
  hence "\<not>(w \<Turnstile> \<box>\<not>F)" by auto
  hence "\<not>(\<forall> n. (w |\<^sub>s n) \<Turnstile> \<not>F)" by (auto simp add: always_def)
  hence  "\<not>(\<forall> n. \<not>((w |\<^sub>s n) \<Turnstile> F))" by auto
  thus "(\<exists> n. (w |\<^sub>s n) \<Turnstile> F)" by auto
next
  assume a1: "(\<exists> n. (w |\<^sub>s n) \<Turnstile> F)"
  show "w \<Turnstile> \<diamond> F" by (simp add: eventually_def always_def)
qed


lemma angle_action_defs: "(w \<Turnstile> \<diamond>\<langle>P\<rangle>_v) = (\<exists> i. ((w |\<^sub>s i) \<Turnstile> P) \<and> ((w |\<^sub>s i) \<Turnstile> v$ \<noteq> $v))"
proof
  assume "w \<Turnstile> \<diamond>\<langle>P\<rangle>_v"
  hence "w \<Turnstile> \<not>\<box>[\<not>P]_v" by (unfold angle_action_def)
  hence "\<not>(w \<Turnstile> \<box>[\<not>P]_v)" by auto
  hence "\<not>(\<forall> i. ((w |\<^sub>s i) \<Turnstile> \<not>P) \<or> ((w |\<^sub>s i) \<Turnstile> Unchanged v))"
    by (unfold action_def)
  hence  "\<exists> i. \<not>(((w |\<^sub>s i) \<Turnstile> \<not>P) \<or> ((w |\<^sub>s i) \<Turnstile> Unchanged v))"
    by auto
  thus  "\<exists> i. ((w |\<^sub>s i) \<Turnstile> P) \<and> ((w |\<^sub>s i) \<Turnstile> v$ \<noteq> $v)"
    by (auto simp add: unch_def)
next
  assume a1: "\<exists> i. ((w |\<^sub>s i) \<Turnstile> P) \<and> ((w |\<^sub>s i) \<Turnstile> v$ \<noteq> $v)"
  thus "w \<Turnstile> \<diamond>\<langle>P\<rangle>_v" by (simp add: angle_action_def action_def unch_def)
qed

lemma unch_defs: "(w \<Turnstile> Unchanged v) = (((second w) \<Turnstile> v) = ((first w) \<Turnstile> v))"
  by (auto simp add: unch_def before_def nexts_def after_def 
    tail_def suffix_def first_def second_def)

section "Invariance Under Stuttering"

text {* This section formalises stuttering invariance for the defined
 operators. *}

constdefs
stutinv :: "('a,'b) formfun \<Rightarrow> bool"
"stutinv F \<equiv> \<forall> \<sigma> \<tau>. \<sigma> \<approx> \<tau> \<longrightarrow> (\<sigma> \<Turnstile> F) = (\<tau> \<Turnstile> F)"

nstutinv :: "('a,'b) formfun \<Rightarrow> bool"
"nstutinv P \<equiv> \<forall> \<sigma> \<tau>. (first \<sigma> = first \<tau>) \<and> (tail \<sigma>) \<approx> (tail \<tau>) \<longrightarrow> (\<sigma> \<Turnstile> P) = (\<tau> \<Turnstile> P)"

syntax
  "_stutinv" :: "lift \<Rightarrow> bool" ("(STUTINV _)" [40] 40)
  "_nstutinv" :: "lift \<Rightarrow> bool" ("(NSTUTINV _)" [40] 40)

translations
  "_stutinv" \<rightleftharpoons> "stutinv"
  "_nstutinv" \<rightleftharpoons> "nstutinv"


text {* Predicate @{term "stutinv F"} formalises stuttering invariance for
  formula @{term F}. That is if two sequences are similar @{term "s \<approx> t"} (equal up
  to stuttering) then the validity of @{term F} under both @{term s} and @{term t}
  are equivalent. Predicate @{term "nstutinv P"} should be read as \emph{nearly
  stuttering invariant} -- and is required for some stuttering invariance proofs. *}

lemma stutinv_strictly_stronger: assumes h: "STUTINV F"
                                   shows    "NSTUTINV F"
proof (unfold nstutinv_def,(rule allI)+,intro impI,elim conjE)
  fix s t :: "nat \<Rightarrow> 'a"
  assume a1: "first s = first t"
    and  a2: "(tail s) \<approx> (tail t)"
  from h have "\<forall> \<sigma> \<tau>. \<sigma> \<approx> \<tau> \<longrightarrow> (\<sigma> \<Turnstile> F) = (\<tau> \<Turnstile> F)"
    by (simp add: stutinv_def)
  hence g1: "s \<approx> t \<longrightarrow> (s \<Turnstile> F) = (t \<Turnstile> F)"
    by blast
  have "s \<approx> t"
  proof -
    have tg1: "(first s) ## (tail s) = s" by (rule seq_app_first_tail)
    have tg2: "(first t) ## (tail t) = t" by (rule seq_app_first_tail)
    with tg2 a1 have tg2': "(first s) ## (tail t) = t" by simp
    from a2 have "(first s) ## (tail s) \<approx> (first s) ## (tail t)"
      by (rule app_seqsimilar)
    with tg1 tg2' show ?thesis by auto
  qed
  with g1 show "(s \<Turnstile> F) = (t \<Turnstile> F)" by auto
qed

subsection "Properties of @{term stutinv}"

text {* This section proof stuttering invariance, preservation of stuttering invariance
 and introduction of stuttering invariance for different formulas. First, state predicates
 are stuttering invariant. *}

theorem stut_before: "STUTINV $F"
proof (unfold stutinv_def,(rule allI)+,rule impI)
  fix s t :: "'a seq"
  assume a1: "s \<approx> t"
  hence "(first s) = (first t)"
    by (rule sim_first)
  thus "(s \<Turnstile> $F) = (t \<Turnstile> $F)"
    by (auto simp add: before_def)
qed

text{* Invariants preserves stuttering invariance. *}

theorem stut_always: assumes H:"stutinv F" shows "STUTINV \<box>F"
proof (unfold stutinv_def,(rule allI)+,rule impI)
  fix s t
  from H have h':"\<forall> \<sigma> \<tau>. \<sigma> \<approx> \<tau> \<longrightarrow> (\<sigma> \<Turnstile> F) = (\<tau> \<Turnstile> F)" by (unfold stutinv_def)
  hence a1: "s \<approx> t \<longrightarrow> (s \<Turnstile> F) = (t \<Turnstile> F)" by simp
  assume a2: "s \<approx> t"
  with a1 have a1': "(s \<Turnstile> F) = (t \<Turnstile> F)" by auto
  show "(s \<Turnstile> (\<box> F)) = (t \<Turnstile> (\<box> F))"
  proof 
    assume a1: "t \<Turnstile> (\<box> F)"
    show "s \<Turnstile> (\<box> F)" 
    proof (unfold always_def,rule allI)
      fix n
      from a2 have "\<forall> n. \<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) 
	\<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))"
	by (rule sim_step)
      hence "\<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))" ..
      then obtain m where "((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> 
	((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))" ..
      hence "(s |\<^sub>s n \<approx> t |\<^sub>s m)" by auto
      with h' have g1: "(s |\<^sub>s n \<Turnstile> F) = (t |\<^sub>s m \<Turnstile> F)" by auto
      from a1 have "\<forall>n. (t |\<^sub>s n) \<Turnstile> F" by (auto simp add: always_def)
      hence "(t |\<^sub>s m) \<Turnstile> F" ..
      with g1 show "(s |\<^sub>s n) \<Turnstile> F" by auto
    qed
  next
    assume a1: "s \<Turnstile> (\<box> F)"
    show "t \<Turnstile> (\<box> F)" 
    proof (unfold always_def,rule allI)
      fix n
      from a2 have "\<forall> n. \<exists> m. ((t |\<^sub>s n) \<approx> (s |\<^sub>s m)) \<and> (((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s Suc m))
	\<or> ((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s m)))" 
	by (rule sim_step[OF seqsim_sym])
      hence "\<exists> m. ((t |\<^sub>s n) \<approx> (s |\<^sub>s m)) \<and> (((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s Suc m)) \<or> ((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s m)))" ..
      then obtain m where "((t |\<^sub>s n) \<approx> (s |\<^sub>s m)) \<and> (((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s Suc m))
	\<or> ((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s m)))" ..
      hence "(t |\<^sub>s n \<approx> s |\<^sub>s m)" by auto
      with h' have g1: "(t |\<^sub>s n \<Turnstile> F) = (s |\<^sub>s m \<Turnstile> F)" by auto
      from a1 have "\<forall>n. (s |\<^sub>s n) \<Turnstile> F" by (auto simp add: always_def)
      hence "(s |\<^sub>s m) \<Turnstile> F" ..
      with g1 show "(t |\<^sub>s n) \<Turnstile> F" by auto   
    qed
  qed
qed

text{* If we can assume that a formula @{term P} is nearly suttering invariant
 then wrapping it in @{text "\<box>[-]_v"} will introduce stuttering invariance. *}

theorem stut_action: assumes H: "NSTUTINV P" shows "STUTINV \<box>[P]_v"
proof (unfold stutinv_def,(rule allI)+,rule impI)
  fix s t  
  from H have h':"\<forall> \<sigma> \<tau>. (first \<sigma> = first \<tau>) \<and> (tail \<sigma>) \<approx> (tail \<tau>) \<longrightarrow> (\<sigma> \<Turnstile> P) = (\<tau> \<Turnstile> P)"
    by (simp add: nstutinv_def)
  hence a1:"(first s = first t) \<and> (tail s) \<approx> (tail t) \<longrightarrow> (s \<Turnstile> P) = (t \<Turnstile> P)" by simp
  assume a2: "s \<approx> t"
  hence a2': "t \<approx> s" by (rule seqsim_sym)
  show "(s \<Turnstile> \<box>[P]_v) = (t \<Turnstile> \<box>[P]_v)"
  proof 
    assume a1: "t \<Turnstile> \<box>[P]_v"
    show "s \<Turnstile> \<box>[P]_v"
    proof (unfold action_def,rule allI)
      fix n
      from a2 have "\<forall> n. \<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) 
	\<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))"
	by (rule sim_step)
      hence "\<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))" ..
      then obtain m where a2': "((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) 
	\<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))" ..
      from a2' have g1: "(s |\<^sub>s n \<approx> t |\<^sub>s m)" by auto
      hence  "first (s |\<^sub>s n) = first (t |\<^sub>s m) " by (simp add: sim_first)
      hence g1': "s n = t m" by (simp add: suffix_def first_def)
      hence g1'': "first (s |\<^sub>s n) = first (t |\<^sub>s m)" 
	      by (simp add: suffix_first)
      from a2' have g2: "(s |\<^sub>s (Suc n) \<approx> t |\<^sub>s (Suc m)) \<or> (s |\<^sub>s (Suc n) \<approx> t |\<^sub>s m)" by auto
      hence "(first (s |\<^sub>s (Suc n)) = first (t |\<^sub>s (Suc m))) \<or> (first (s |\<^sub>s (Suc n)) = first (t |\<^sub>s m))"
	by (auto simp add: sim_first)
      hence g2':"(s (Suc n) = t (Suc m)) \<or> (s (Suc n) = t m)" by (simp add: suffix_def first_def)
      thm action_def
      from a1 have "\<forall>i. ((t |\<^sub>s i) \<Turnstile> P) \<or> ((t |\<^sub>s i) \<Turnstile> (Unchanged v))" by (simp add: action_def)
      hence a1': "((t |\<^sub>s m) \<Turnstile> P) \<or> ((t |\<^sub>s m) \<Turnstile> (Unchanged v))" ..
      thus "((s |\<^sub>s n) \<Turnstile> P) \<or> ((s |\<^sub>s n) \<Turnstile> (Unchanged v))"
      proof
	assume a3: "(t |\<^sub>s m) \<Turnstile> Unchanged v"
	hence a3': "((second (t |\<^sub>s m)) \<Turnstile> v) = ((first (t |\<^sub>s m)) \<Turnstile> v)"
	  by (simp add: unch_defs)
	from g2' show ?thesis
	proof
	  assume a4: "s (Suc n) = t (Suc m)"
	  show ?thesis
	  proof (rule disjI2)
	    from a4 have G2: "second (s |\<^sub>s n) = second (t |\<^sub>s m)"
	      by (simp add: suffix_second)
	    from g1'' G2 a3' have "((second (s |\<^sub>s n)) \<Turnstile> v) = ((first (s |\<^sub>s n)) \<Turnstile> v)"
	      by auto
	    thus "(s |\<^sub>s n) \<Turnstile> (Unchanged v)" by (simp add: unch_defs)
	  qed
	next
	  assume a4: "s (Suc n) = t m"
	  hence a4': "second (s |\<^sub>s n) = first (t |\<^sub>s m)"
	    by (simp add: suffix_first suffix_second)
	  show ?thesis
	  proof (rule disjI2)
	    from a3' g1'' a4' have "((second (s |\<^sub>s n)) \<Turnstile> v) = ((first (s |\<^sub>s n)) \<Turnstile> v)"
	      by auto
	    thus "(s |\<^sub>s n) \<Turnstile> (Unchanged v)" by (simp add: unch_defs)
	  qed
	qed
      next
	assume a3: "((t |\<^sub>s m) \<Turnstile> P)"
	from g2 show ?thesis
	proof
	  from H have h':"\<forall> \<sigma> \<tau>. (first \<sigma> = first \<tau>) \<and> (tail \<sigma>) \<approx> (tail \<tau>) \<longrightarrow> (\<sigma> \<Turnstile> P) = (\<tau> \<Turnstile> P)"
	    by (simp add: nstutinv_def)
	  hence g3: "(first (s |\<^sub>s n) = first (t |\<^sub>s m)) 
	    \<and> (tail (s |\<^sub>s n) \<approx> tail (t |\<^sub>s m)) \<longrightarrow>  (((s |\<^sub>s n) \<Turnstile> P) = ((t |\<^sub>s m) \<Turnstile> P))" by auto
	  assume a4: "s |\<^sub>s Suc n \<approx> t |\<^sub>s Suc m"
	  hence g4: "tail (s |\<^sub>s n) \<approx> tail (t |\<^sub>s m)"
	    by (simp add: tail_suffix_suc)
	  from g1 have "first (s |\<^sub>s n) = first (t |\<^sub>s m)" by (simp add: sim_first)
	  with g3 g4 have "((s |\<^sub>s n) \<Turnstile> P) = ((t |\<^sub>s m) \<Turnstile> P)" by auto
	  with a3 show ?thesis by auto
	next
	  assume a3: "s |\<^sub>s Suc n \<approx> t |\<^sub>s m"
	  hence "first (s |\<^sub>s Suc n) = first (t |\<^sub>s m)" by (simp add: sim_first)
	  hence "s (Suc n) = (t m)" by (simp add: suffix_def first_def)
	  hence g3: "second (s |\<^sub>s n) = first (t |\<^sub>s m)" 
	    by (simp add: suffix_first suffix_second)
	  have "((first (t |\<^sub>s m)) \<Turnstile> v) = ((first (t |\<^sub>s m)) \<Turnstile> v)"
	    by auto
	  with g1'' g3 have "((second (s |\<^sub>s n)) \<Turnstile> v) = ((first (s |\<^sub>s n)) \<Turnstile> v)"
	    by auto
	  thus ?thesis by (simp add: unch_defs)
	qed
      qed
    qed
  next
    assume a1: "s \<Turnstile> \<box>[P]_v"
    show "t \<Turnstile> \<box>[P]_v"
    proof (unfold action_def,rule allI)
      fix n
      from a2' have "\<forall> n. \<exists> m. ((t |\<^sub>s n) \<approx> (s |\<^sub>s m)) \<and> (((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s Suc m)) 
	\<or> ((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s m)))"
	by (rule sim_step)
      hence "\<exists> m. ((t |\<^sub>s n) \<approx> (s |\<^sub>s m)) \<and> (((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s Suc m)) \<or> ((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s m)))" ..
      then obtain m where a2'': "((t |\<^sub>s n) \<approx> (s |\<^sub>s m)) \<and> (((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s Suc m)) 
	\<or> ((t |\<^sub>s Suc n) \<approx> (s |\<^sub>s m)))" ..
      from a2'' have g1: "(t |\<^sub>s n \<approx> s |\<^sub>s m)" by auto
      hence  "first (t |\<^sub>s n) = first (s |\<^sub>s m) " by (simp add: sim_first)
      hence g1': "t n = s m" by (simp add: suffix_def first_def)
      hence g1'': "first (t |\<^sub>s n) = first (s |\<^sub>s m)" 
	      by (simp add: suffix_first)
      from a2'' have g2: "(t |\<^sub>s (Suc n) \<approx> s |\<^sub>s (Suc m)) \<or> (t |\<^sub>s (Suc n) \<approx> s |\<^sub>s m)" by auto
      hence "(first (t |\<^sub>s (Suc n)) = first (s |\<^sub>s (Suc m))) \<or> (first (t |\<^sub>s (Suc n)) = first (s |\<^sub>s m))"
	by (auto simp add: sim_first)
      hence g2':"(t (Suc n) = s (Suc m)) \<or> (t (Suc n) = s m)" by (simp add: suffix_def first_def)
      from a1 have "\<forall>i. ((s |\<^sub>s i) \<Turnstile> P) \<or> ((s |\<^sub>s i) \<Turnstile> (Unchanged v))" by (simp add: action_def)
      hence a1': "((s |\<^sub>s m) \<Turnstile> P) \<or> ((s |\<^sub>s m) \<Turnstile> (Unchanged v))" ..
      thus "((t |\<^sub>s n) \<Turnstile> P) \<or> ((t |\<^sub>s n) \<Turnstile> (Unchanged v))"
      proof
	assume a3: "(s |\<^sub>s m) \<Turnstile> Unchanged v"
	hence a3': "((second (s |\<^sub>s m)) \<Turnstile> v) = ((first (s |\<^sub>s m)) \<Turnstile> v)"
	  by (simp add: unch_defs)
	from g2' show ?thesis
	proof
	  assume a4: "t (Suc n) = s (Suc m)"
	  show ?thesis
	  proof (rule disjI2)
	    from a4 have G2: "second (t |\<^sub>s n) = second (s |\<^sub>s m)"
	      by (simp add: suffix_second)
	    from g1'' G2 a3' have "((second (t |\<^sub>s n)) \<Turnstile> v) = ((first (t |\<^sub>s n)) \<Turnstile> v)"
	      by auto
	    thus "(t |\<^sub>s n) \<Turnstile> (Unchanged v)" by (simp add: unch_defs)
	  qed
	next
	  assume a4: "t (Suc n) = s m"
	  hence a4': "second (t |\<^sub>s n) = first (s |\<^sub>s m)"
	    by (simp add: suffix_first suffix_second)
	  show ?thesis
	  proof (rule disjI2)
	    from a3' g1'' a4' have "((second (t |\<^sub>s n)) \<Turnstile> v) = ((first (t |\<^sub>s n)) \<Turnstile> v)"
	      by auto
	    thus "(t |\<^sub>s n) \<Turnstile> (Unchanged v)" by (simp add: unch_defs)
	  qed
	qed
      next
	assume a3: "((s |\<^sub>s m) \<Turnstile> P)"
	from g2 show ?thesis
	proof
	  from H have h':"\<forall> \<sigma> \<tau>. (first \<sigma> = first \<tau>) \<and> (tail \<sigma>) \<approx> (tail \<tau>) \<longrightarrow> (\<sigma> \<Turnstile> P) = (\<tau> \<Turnstile> P)"
	    by (simp add: nstutinv_def)
	  hence g3: "(first (t |\<^sub>s n) = first (s |\<^sub>s m)) 
	    \<and> (tail (t |\<^sub>s n) \<approx> tail (s |\<^sub>s m)) \<longrightarrow>  (((t |\<^sub>s n) \<Turnstile> P) = ((s |\<^sub>s m) \<Turnstile> P))" by auto
	  assume a4: "t |\<^sub>s Suc n \<approx> s |\<^sub>s Suc m"
	  hence g4: "tail (t |\<^sub>s n) \<approx> tail (s |\<^sub>s m)"
	    by (simp add: tail_suffix_suc)
	  from g1 have "first (t |\<^sub>s n) = first (s |\<^sub>s m)" by (simp add: sim_first)
	  with g3 g4 have "((t |\<^sub>s n) \<Turnstile> P) = ((s |\<^sub>s m) \<Turnstile> P)" by auto
	  with a3 show ?thesis by auto
	next
	  assume a3: "t |\<^sub>s Suc n \<approx> s |\<^sub>s m"
	  hence "first (t |\<^sub>s Suc n) = first (s |\<^sub>s m)" by (simp add: sim_first)
	  hence "t (Suc n) = (s m)" by (simp add: suffix_def first_def)
	  hence g3: "second (t |\<^sub>s n) = first (s |\<^sub>s m)" 
	    by (simp add: suffix_first suffix_second)
	  have "((first (s |\<^sub>s m)) \<Turnstile> v) = ((first (s |\<^sub>s m)) \<Turnstile> v)"
	    by auto
	  with g1'' g3 have "((second (t |\<^sub>s n)) \<Turnstile> v) = ((first (t |\<^sub>s n)) \<Turnstile> v)"
	    by auto
	  thus ?thesis by (simp add: unch_defs)
	qed
      qed
    qed
  qed
qed

text{* The lemmas below shows that propositional and predicate operators 
  preserves stuttering invariance. *}

lemma stut_and: "\<lbrakk>STUTINV F;STUTINV G\<rbrakk> \<Longrightarrow> STUTINV (F \<and> G)"
by (auto simp add: stutinv_def)

lemma stut_or: "\<lbrakk>STUTINV F;STUTINV G\<rbrakk> \<Longrightarrow> STUTINV (F \<or> G)"
by (auto simp add: stutinv_def)

lemma stut_imp: "\<lbrakk>STUTINV F;STUTINV G\<rbrakk> \<Longrightarrow> STUTINV (F \<longrightarrow> G)"
by (auto simp add: stutinv_def)

lemma stut_eq: "\<lbrakk>STUTINV F;STUTINV G\<rbrakk> \<Longrightarrow> STUTINV (F = G)"
by (auto simp add: stutinv_def)

lemma stut_noteq: "\<lbrakk>STUTINV F;STUTINV G\<rbrakk> \<Longrightarrow> STUTINV (F \<noteq> G)"
by (auto simp add: stutinv_def)

lemma stut_not: "STUTINV F \<Longrightarrow> STUTINV (\<not> F)"
by (auto simp add: stutinv_def)

lemma stut_all: "STUTINV F \<Longrightarrow> STUTINV (\<forall> x. F)"
by (auto simp add: stutinv_def)

lemma stut_ex: "STUTINV F \<Longrightarrow> STUTINV (\<exists> x. F)"
by (auto simp add: stutinv_def)

lemma stut_const: "STUTINV #c"
by (auto simp add: stutinv_def)

lemma stut_fun1: "STUTINV X \<Longrightarrow> STUTINV (f <X>)"
  by (auto simp add: stutinv_def)

lemma stut_fun2: "\<lbrakk>STUTINV X;STUTINV Y\<rbrakk> \<Longrightarrow> STUTINV (f <X,Y>)"
  by (auto simp add: stutinv_def)

lemma stut_fun3: "\<lbrakk>STUTINV X;STUTINV Y;STUTINV Z\<rbrakk> \<Longrightarrow> STUTINV (f <X,Y,Z>)"
  by (auto simp add: stutinv_def)

lemma stut_plus: "\<lbrakk>STUTINV x;STUTINV y\<rbrakk> \<Longrightarrow> STUTINV (x+y)"
  by (auto simp add: stutinv_def)

(* FIXME: add stut for all operators! *)

subsection "Properties of @{term nstutinv}"

text {* This section shows nearly stuttering invariance properties
  for some operators. Firstly, a transition is nearly stuttering
  invariant *}

text{* If a formula @{term F} is stuttering invariant then @{text "\<circ>F"} is
  nearly stuttering invariant. *}

lemma nstut_nexts: assumes H: "STUTINV F" shows "NSTUTINV \<circ>F"
proof (unfold nstutinv_def,(rule allI)+,rule impI)
  fix s :: "nat \<Rightarrow> 'a"
  fix t :: "nat \<Rightarrow> 'a"
  from H have h':"\<forall> \<sigma> \<tau>. \<sigma> \<approx> \<tau> \<longrightarrow> (\<sigma> \<Turnstile> F) = (\<tau> \<Turnstile> F)" by (unfold stutinv_def)
  hence a1: "(tail s) \<approx> (tail t) \<longrightarrow> ((tail s) \<Turnstile> F) = ((tail t) \<Turnstile> F)" by simp
  assume a2: "first s = first t \<and> tail s \<approx> tail t"
  show "(s \<Turnstile> \<circ>F) = (t \<Turnstile> \<circ>F)" 
  proof (unfold nexts_def)
    from a1 a2 show "((tail s) \<Turnstile> F) = ((tail t) \<Turnstile> F)"
      by auto
  qed
qed

text{* The @{text "[-]_v"} operator is not part of the semantics of 
  TLA*, but is used in the axioms of it. However, it is alwasy wrapped
  inside @{text "\<box>[-]_v"} so we only require that it preserves nearly
  stuttering invariance. I am not sure if it introduces stuttering invariance
  with the same assumption. It might be a problem that the formulas it wraps
  can be temporal, while  @{text "[-]_v"} is not. *}

text{* The lemmas below shows that propositional and predicate operators 
  preserves nearly stuttering invariance. *}

lemma nstut_and: "\<lbrakk>NSTUTINV F;NSTUTINV G\<rbrakk> \<Longrightarrow> NSTUTINV (F \<and> G)"
by (auto simp add: nstutinv_def)

lemma nstut_or: "\<lbrakk>NSTUTINV F;NSTUTINV G\<rbrakk> \<Longrightarrow> NSTUTINV (F \<or> G)"
by (auto simp add: nstutinv_def)

lemma nstut_imp: "\<lbrakk>NSTUTINV F;NSTUTINV G\<rbrakk> \<Longrightarrow> NSTUTINV (F \<longrightarrow> G)"
by (auto simp add: nstutinv_def)

lemma nstut_eq: assumes h1: "NSTUTINV F"
                  and   h2: "NSTUTINV G"
                 shows      "NSTUTINV (F = G)"
proof (unfold nstutinv_def,(rule allI)+)
  fix s t
  from h1 have "\<forall> \<sigma> \<tau>. (first \<sigma> = first \<tau>) \<and> (tail \<sigma>) \<approx> (tail \<tau>) \<longrightarrow> (\<sigma> \<Turnstile> F) = (\<tau> \<Turnstile> F)"
    by (unfold nstutinv_def)
  hence g1: "(first s = first t) \<and> (tail s) \<approx> (tail t) \<longrightarrow> (s \<Turnstile> F) = (t \<Turnstile> F)" by blast
  from h2 have "\<forall> \<sigma> \<tau>. (first \<sigma> = first \<tau>) \<and> (tail \<sigma>) \<approx> (tail \<tau>) \<longrightarrow> (\<sigma> \<Turnstile> G) = (\<tau> \<Turnstile> G)"
    by (unfold nstutinv_def)
  hence g2: "(first s = first t) \<and> (tail s) \<approx> (tail t) \<longrightarrow> (s \<Turnstile> G) = (t \<Turnstile> G)" by blast
  with g1 show "(first s = first t) \<and> (tail s) \<approx> (tail t) \<longrightarrow> (s \<Turnstile> F = G) = (t \<Turnstile> F = G)" 
    by auto
qed

lemma nstut_not: "NSTUTINV F \<Longrightarrow> NSTUTINV (\<not> F)"
by (auto simp add: nstutinv_def)

lemma nstut_noteq: assumes h1: "NSTUTINV F"
                  and   h2: "NSTUTINV G"
                 shows      "NSTUTINV (F \<noteq> G)"
proof -
  from h1 h2 have "NSTUTINV (F=G)" by (rule nstut_eq)
  thus "NSTUTINV \<not>(F=G)" by (rule nstut_not)
qed

lemma nstut_all: "NSTUTINV F \<Longrightarrow> NSTUTINV (\<forall> x. F)"
by (auto simp add: nstutinv_def)

lemma nstut_ex: "NSTUTINV F \<Longrightarrow> NSTUTINV (\<exists> x. F)"
by (auto simp add: nstutinv_def)

lemma nstut_const: "NSTUTINV #c"
by (auto simp add: nstutinv_def)

lemma nstut_fun1: assumes h1: "NSTUTINV X"
                 shows      "NSTUTINV (f <X>)"
proof (unfold nstutinv_def,(rule allI)+,rule impI) 
  fix s t :: "nat \<Rightarrow> 'a"
  assume a1: "first s = first t \<and> tail s \<approx> tail t"
  from h1 have "\<forall> s t. first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> X)=(t \<Turnstile> X)"
    by (unfold nstutinv_def)
  hence "first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> X)=(t \<Turnstile> X)"
    by blast
  with a1 have "(s \<Turnstile> X)=(t \<Turnstile> X)" by simp
  thus "(s \<Turnstile> f<X>) = (t \<Turnstile> f<X>)"
    by auto
qed

lemma nstut_fun2: assumes h1: "NSTUTINV X"
                    and   h2: "NSTUTINV Y"
                   shows      "NSTUTINV (f <X,Y>)"
proof (unfold nstutinv_def,(rule allI)+,rule impI) 
  fix s t :: "nat \<Rightarrow> 'a"
  assume a1: "first s = first t \<and> tail s \<approx> tail t"
  from h1 have "\<forall> s t. first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> X)=(t \<Turnstile> X)"
    by (unfold nstutinv_def)
  hence "first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> X)=(t \<Turnstile> X)"
    by blast
  with a1 have g1: "(s \<Turnstile> X)=(t \<Turnstile> X)" by simp
  from h2 have "\<forall> s t. first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> Y)=(t \<Turnstile> Y)"
    by (unfold nstutinv_def)
  hence "first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> Y)=(t \<Turnstile> Y)"
    by blast
  with a1 have "(s \<Turnstile> Y)=(t \<Turnstile> Y)" by simp
  with g1 show "(s \<Turnstile> f<X,Y>) = (t \<Turnstile> f<X,Y>)"
    by auto
qed

lemma nstut_fun3: assumes h1: "NSTUTINV X"
                    and   h2: "NSTUTINV Y"
                    and   h3: "NSTUTINV Z"
                   shows      "NSTUTINV (f <X,Y,Z>)"
proof (unfold nstutinv_def,(rule allI)+,rule impI) 
  fix s t :: "nat \<Rightarrow> 'a"
  assume a1: "first s = first t \<and> tail s \<approx> tail t"
  from h1 have "\<forall> s t. first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> X)=(t \<Turnstile> X)"
    by (unfold nstutinv_def)
  hence "first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> X)=(t \<Turnstile> X)"
    by blast
  with a1 have g1: "(s \<Turnstile> X)=(t \<Turnstile> X)" by simp
  from h2 have "\<forall> s t. first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> Y)=(t \<Turnstile> Y)"
    by (unfold nstutinv_def)
  hence "first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> Y)=(t \<Turnstile> Y)"
    by blast
  with a1 have g2:"(s \<Turnstile> Y)=(t \<Turnstile> Y)" by simp
  from h3 have "\<forall> s t. first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> Z)=(t \<Turnstile> Z)"
    by (unfold nstutinv_def)
  hence "first s = first t \<and> tail s \<approx> tail t \<longrightarrow> (s \<Turnstile> Z)=(t \<Turnstile> Z)"
    by blast
  with a1 have "(s \<Turnstile> Z)=(t \<Turnstile> Z)" by simp
  with g1 g2 show "(s \<Turnstile> f<X,Y,Z>) = (t \<Turnstile> f<X,Y,Z>)"
    by auto
qed

lemma nstut_plus: "\<lbrakk>NSTUTINV x;NSTUTINV y\<rbrakk> \<Longrightarrow> NSTUTINV (x+y)"
  by (auto simp add: nstut_fun2)

(* FIX ME: ADD for other operators: is it necessary? *)

subsection "Abbreviations"

text {* We show the obvious fact that the same properties holds for abbreviated
  operators. *}

lemmas nstut_before = stut_before[THEN stutinv_strictly_stronger]

lemma nstut_after: "NSTUTINV F$"
proof (unfold after_def)
  have "STUTINV $F" by (rule stut_before)
  thus "NSTUTINV \<circ>$F" by (rule nstut_nexts)
qed

lemma nstut_unch: "NSTUTINV (Unchanged v)"
proof (unfold unch_def)
  have g1: "NSTUTINV v$" by (rule nstut_after)
  have "NSTUTINV $v" 
    by (rule stut_before[THEN stutinv_strictly_stronger])
  with g1 show "NSTUTINV (v$ = $v)" by (rule nstut_eq)
qed

lemma nstut_actrans: assumes H: "NSTUTINV P" shows "NSTUTINV [P]_v"
proof(unfold actrans_def)
  from H nstut_unch[of v] show "NSTUTINV (P \<or> Unchanged v)"
    by (rule nstut_or)
qed

lemma stut_eventually: assumes H: "STUTINV F" shows "STUTINV \<diamond>F"
proof (unfold eventually_def)
  from H have "STUTINV \<not>F" by (rule stut_not)
  hence "STUTINV \<box>\<not>F" by (rule stut_always)
  thus "STUTINV \<not>\<box>\<not>F" by (rule stut_not)
qed

lemma stut_angle_action: assumes H: "NSTUTINV P" shows "STUTINV \<diamond>\<langle>P\<rangle>_v"
proof (unfold angle_action_def)
  from H have "NSTUTINV \<not>P" by (rule nstut_not)
  hence "STUTINV \<box>[\<not> P]_v" by (rule stut_action)
  thus  "STUTINV \<not>\<box>[\<not> P]_v" by (rule stut_not)
qed

lemma nstut_angle_acttrans: assumes H: "NSTUTINV P" shows "NSTUTINV \<langle>P\<rangle>_v"
proof (unfold angle_actrans_def)
  from H have "NSTUTINV \<not>P" by (rule nstut_not)
  hence "NSTUTINV [\<not> P]_v" by (rule nstut_actrans)
  thus "NSTUTINV (\<not>[\<not> P]_v)" by (rule nstut_not)
qed

lemmas stutinvs = stut_before (* stut_statepred *) stut_always stut_action
  stut_and stut_or stut_imp stut_eq stut_noteq stut_not
  stut_all stut_ex stut_eventually stut_angle_action stut_const 
  stut_fun1 stut_fun2 stut_fun3 stut_plus

lemmas nstutinvs = nstut_before nstut_after nstut_nexts nstut_actrans
  nstut_unch nstut_and nstut_or nstut_imp nstut_eq nstut_noteq nstut_not
  nstut_all nstut_ex nstut_angle_acttrans stutinv_strictly_stronger nstut_const
  nstut_fun1 nstut_fun2 nstut_fun3
  stutinvs[THEN stutinv_strictly_stronger]

lemmas bothstutinvs = stutinvs nstutinvs

end