src/HOL/NanoJava/Equivalence.thy

 theory Equivalence = OpSem + AxSem:
 
 subsection "Validity"
 
 constdefs
-  valid   :: "[assn,stmt,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c-n-> t) --> Q t"
-
- nvalid   :: "[nat,       triple    ] => bool" ("|=_: _"  [61,61] 60)
- "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c-n-> t --> P s --> Q t"
-
- nvalids  :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
+  valid   :: "[assn,stmt, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+ "|=  {P} c {Q} \<equiv> \<forall>s   t. P s --> (\<exists>n. s -c  -n-> t) --> Q   t"
+
+ evalid   :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+ "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e>v-n-> t) --> Q v t"
+
+
+ nvalid   :: "[nat, triple    ] => bool" ("|=_: _"  [61,61] 60)
+ "|=n:  t \<equiv> let (P,c,Q) = t in \<forall>s   t. s -c  -n-> t --> P s --> Q   t"
+
+envalid   :: "[nat,etriple    ] => bool" ("|=_:e _" [61,61] 60)
+ "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e>v-n-> t --> P s --> Q v t"
+
+  nvalids :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
  "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
 
- cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"[61,61] 60)
- "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
+ cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"  [61,61] 60)
+ "A ||=  C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
+
+cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60)
+ "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
 
 syntax (xsymbols)
-  valid   :: "[assn,stmt,assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- nvalid   :: "[nat,       triple    ] => bool" ("\<Turnstile>_: _"   [61,61] 60)
- nvalids  :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
+   valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+  evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+  nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
+ envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:e _" [61,61] 60)
+  nvalids :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
  cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
-
-syntax
-  nvalid1::"[nat,        assn,stmt,assn] => bool" ( "|=_:.{(1_)}/ (_)/ {(1_)}"
-                                                         [61,3,90,3] 60)
- cnvalid1::"[triple set, assn,stmt,assn] => bool" ("_ ||=.{(1_)}/ (_)/ {(1_)}"
-                                                         [61,3,90,3] 60)
-syntax (xsymbols)
-  nvalid1::"[nat,        assn,stmt,assn] => bool" (  "\<Turnstile>_:.{(1_)}/ (_)/ {(1_)}"
-                                                         [61,3,90,3] 60)
- cnvalid1::"[triple set, assn,stmt,assn] => bool" ( "_ |\<Turnstile>.{(1_)}/ (_)/ {(1_)}"
-                                                         [61,3,90,3] 60)
-translations
- " \<Turnstile>n:.{P} c {Q}" \<rightleftharpoons> " \<Turnstile>n:  (P,c,Q)"
- "A |\<Turnstile>.{P} c {Q}" \<rightleftharpoons> "A |\<Turnstile> {(P,c,Q)}"
-
-lemma nvalid1_def2: "\<Turnstile>n:.{P} c {Q} \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
+cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>e/ _"[61,61] 60)
+
+
+lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
 by (simp add: nvalid_def Let_def)
 
-lemma cnvalid1_def2: 
-  "A |\<Turnstile>.{P} c {Q} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
-by(simp add: nvalid1_def2 nvalids_def cnvalids_def)
-
-lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n:.{P} c {Q})"
-apply (simp add: valid_def nvalid1_def2)
-apply blast
-done
+lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))"
+apply (simp add: valid_def nvalid_def2)
+apply blast
+done
+
+lemma envalid_def2: "\<Turnstile>n:e (P,e,Q) \<equiv> \<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t"
+by (simp add: envalid_def Let_def)
+
+lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (\<forall>n. \<Turnstile>n:e (P,e,Q))"
+apply (simp add: evalid_def envalid_def2)
+apply blast
+done
+
+lemma cenvalid_def2: 
+  "A|\<Turnstile>e (P,e,Q) = (\<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))"
+by(simp add: cenvalid_def envalid_def2) 
 
 
 subsection "Soundness"
 
-declare exec_elim_cases [elim!]
-
-lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
-by (clarsimp simp add: nvalid1_def2)
-
-lemma Impl_nvalid_Suc: "\<Turnstile>n:.{P} body C m {Q} \<Longrightarrow> \<Turnstile>Suc n:.{P} Impl C m {Q}"
-by (clarsimp simp add: nvalid1_def2)
+declare exec_elim_cases [elim!] eval_elim_cases [elim!]
+
+lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)"
+by (clarsimp simp add: nvalid_def2)
+
+lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)"
+by (clarsimp simp add: nvalid_def2)
 
 lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
-by (force simp add: split_paired_all nvalid1_def2 intro: exec_mono)
+by (force simp add: split_paired_all nvalid_def2 intro: exec_mono)
 
 lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow>  Ball A (nvalid n)"
 by (fast intro: nvalid_SucD)
 
 lemma Loop_sound_lemma [rule_format (no_asm)]: 
-"\<lbrakk>\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<e> \<noteq> Null \<longrightarrow> P t; s -c0-n0\<rightarrow> t\<rbrakk> \<Longrightarrow> 
-  P s \<longrightarrow> c0 = While (e) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<e> = Null"
-apply (erule exec.induct)
+"\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
+  (s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
+apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
 apply clarsimp+
 done
 
 lemma Impl_sound_lemma: 
 "\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
           (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
 by blast
 
-lemma hoare_sound_main: "A |\<turnstile> C \<Longrightarrow> A |\<Turnstile> C"
-apply (erule hoare.induct)
-apply (simp_all only: cnvalid1_def2)
-apply clarsimp
-apply clarsimp
-apply (clarsimp split add: split_if_asm)
-apply (clarsimp,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
-apply clarsimp
-apply clarsimp
-apply clarsimp
-apply clarsimp
+lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
+by fast
+
+lemma all3_conjunct2: 
+  "\<forall>a p l. (P' a p l \<and> P a p l) \<Longrightarrow> \<forall>a p l. P a p l"
+by fast
+
+lemma cnvalid1_eq: 
+  "A |\<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
+by(simp add: cnvalids_def nvalids_def nvalid_def2)
+
+lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>e t \<longrightarrow> A |\<Turnstile>e t)"
+apply (tactic "split_all_tac 1", rename_tac P e Q)
+apply (rule hoare_ehoare.induct)
+apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
+apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x :  hoare") *})
+apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
+apply (simp_all only: cnvalid1_eq cenvalid_def2)
+apply fast
+apply fast
+apply fast
+apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
+apply fast
+apply fast
+apply fast
+apply fast
+apply fast
+apply fast
 apply (clarsimp del: Meth_elim_cases) (* Call *)
+apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
+apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
+apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
 apply (clarsimp del: Impl_elim_cases) (* Meth *)
 defer
-apply blast (* Conseq *)
+prefer 4 apply blast (*  Conseq *)
+prefer 4 apply blast (* eConseq *)
 apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
 apply blast
 apply blast
 apply blast
 (* Impl *)
-apply (erule thin_rl)
 apply (rule allI)
 apply (induct_tac "n")
 apply  (clarify intro!: Impl_nvalid_0)
 apply (clarify  intro!: Impl_nvalid_Suc)
 apply (drule nvalids_SucD)

 apply (drule (4) Impl_sound_lemma)
 done
 
 theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
 apply (simp only: valid_def2)
-apply (drule hoare_sound_main)
+apply (drule hoare_sound_main [THEN conjunct1, rule_format])
 apply (unfold cnvalids_def nvalids_def)
 apply fast
 done
 
+theorem ehoare_sound: "{} \<turnstile>e {P} e {Q} \<Longrightarrow> \<Turnstile>e {P} e {Q}"
+apply (simp only: evalid_def2)
+apply (drule hoare_sound_main [THEN conjunct2, rule_format])
+apply (unfold cenvalid_def nvalids_def)
+apply fast
+done
+
 
 subsection "(Relative) Completeness"
 
-constdefs MGT    :: "stmt => state => triple"
-         "MGT c z \<equiv> (\<lambda> s. z = s, c, %t. \<exists>n. z -c-n-> t)"
+constdefs MGT    :: "stmt => state =>  triple"
+         "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda>  t. \<exists>n. z -c-  n-> t)"
+         eMGT    :: "expr => state => etriple"
+        "eMGT e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
 
 lemma MGF_implies_complete:
- "\<forall>z. {} |\<turnstile> {MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
+ "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
 apply (simp only: valid_def2)
 apply (unfold MGT_def)
-apply (erule hoare.Conseq)
-apply (clarsimp simp add: nvalid1_def2)
-done
-
-
-declare exec.intros[intro!]
+apply (erule hoare_ehoare.Conseq)
+apply (clarsimp simp add: nvalid_def2)
+done
+
+lemma eMGF_implies_complete:
+ "\<forall>z. {} |\<turnstile>e eMGT e z \<Longrightarrow> \<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
+apply (simp only: evalid_def2)
+apply (unfold eMGT_def)
+apply (erule hoare_ehoare.eConseq)
+apply (clarsimp simp add: envalid_def2)
+done
+
+declare exec_eval.intros[intro!]
 
 lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
   A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
 apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
-       in hoare.Conseq)
+       in hoare_ehoare.Conseq)
 apply  (rule allI)
-apply  (rule hoare.Loop)
-apply  (erule hoare.Conseq)
+apply  (rule hoare_ehoare.Loop)
+apply  (erule hoare_ehoare.Conseq)
 apply  clarsimp
 apply  (blast intro:rtrancl_into_rtrancl)
 apply (erule thin_rl)
 apply clarsimp
 apply (erule_tac x = z in allE)
 apply clarsimp
 apply (erule converse_rtrancl_induct)
 apply  blast
 apply clarsimp
-apply (drule (1) exec_max2)
+apply (drule (1) exec_exec_max)
 apply (blast del: exec_elim_cases)
 done
 
-lemma MGF_lemma[rule_format]:
- "(\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z}) \<longrightarrow> (\<forall>z. A |\<turnstile> {MGT c z})"
-apply (simp add: MGT_def)
-apply (induct_tac c)
-apply (tactic "ALLGOALS Clarify_tac")
-
-apply (rule Conseq1 [OF hoare.Skip])
-apply blast
-
-apply (rule hoare.Comp)
+lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> 
+ (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>e eMGT e z)"
+apply (simp add: MGT_def eMGT_def)
+apply (rule stmt_expr.induct)
+apply (rule_tac [!] allI)
+
+apply (rule Conseq1 [OF hoare_ehoare.Skip])
+apply blast
+
+apply (rule hoare_ehoare.Comp)
 apply  (erule spec)
-apply (erule hoare.Conseq)
+apply (erule hoare_ehoare.Conseq)
+apply clarsimp
+apply (drule (1) exec_exec_max)
+apply blast
+
+apply (erule thin_rl)
+apply (rule hoare_ehoare.Cond)
+apply  (erule spec)
+apply (rule allI)
+apply (simp)
+apply (rule conjI)
+apply  (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max,
+        erule thin_rl, erule thin_rl, force)+
+
+apply (erule MGF_Loop)
+
+apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
+apply fast
+
+apply (erule thin_rl)
+apply (rule_tac Q = "\<lambda>a s. \<exists>n. z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
+apply  (drule spec)
+apply  (erule eConseq2)
+apply  fast
+apply (rule allI)
+apply (erule hoare_ehoare.eConseq)
+apply clarsimp
+apply (drule (1) eval_eval_max)
+apply blast
+
+apply (rule hoare_ehoare.Meth)
+apply (rule allI)
+apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
+apply blast
+
+apply blast
+
+apply (rule eConseq1 [OF hoare_ehoare.NewC])
+apply blast
+
+apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast])
+apply fast
+
+apply (rule eConseq1 [OF hoare_ehoare.LAcc])
+apply blast
+
+apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
+apply fast
+
+apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. z -expr1\<succ>a-n1\<rightarrow> t \<and> t -expr2\<succ>v-n2\<rightarrow> s" in
+                hoare_ehoare.Call)
+apply   (erule spec)
+apply  (rule allI)
+apply  (erule hoare_ehoare.eConseq)
+apply  clarsimp
+apply  blast
+apply (rule allI)+
+apply (rule hoare_ehoare.Meth)
+apply (rule allI)
+apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
 apply (erule thin_rl, erule thin_rl)
-apply clarsimp
-apply (drule (1) exec_max2)
-apply blast
-
-apply (rule hoare.Cond)
-apply  (erule hoare.Conseq)
-apply  (erule thin_rl, erule thin_rl)
-apply  force
-apply (erule hoare.Conseq)
-apply (erule thin_rl, erule thin_rl)
-apply force
-
-apply (erule MGF_Loop)
-
-apply (rule Conseq1 [OF hoare.NewC])
-apply blast
-
-apply (rule Conseq1 [OF hoare.Cast])
-apply blast
-
-apply (rule Conseq1 [OF hoare.FAcc])
-apply blast
-
-apply (rule Conseq1 [OF hoare.FAss])
-apply blast
-
-apply (rule hoare.Call)
-apply (rule allI)
-apply (rule hoare.Meth)
-apply (rule allI)
-apply (drule spec, drule spec, erule hoare.Conseq)
-apply blast
-
-apply (rule hoare.Meth)
-apply (rule allI)
-apply (drule spec, drule spec, erule hoare.Conseq)
-apply blast
-
-apply blast
+apply (clarsimp del: Impl_elim_cases)
+apply (drule (2) eval_eval_exec_max)
+apply (fast del: Impl_elim_cases)
 done
 
 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
 apply (unfold MGT_def)
 apply (rule Impl1)
 apply  (rule_tac [2] UNIV_I)
 apply clarsimp
-apply (rule hoare.ConjI)
+apply (rule hoare_ehoare.ConjI)
 apply clarsimp
 apply (rule ssubst [OF Impl_body_eq])
 apply (fold MGT_def)
-apply (rule MGF_lemma)
-apply (rule hoare.Asm)
+apply (rule MGF_lemma [THEN conjunct1, rule_format])
+apply (rule hoare_ehoare.Asm)
 apply force
 done
 
 theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
 apply (rule MGF_implies_complete)
 apply  (erule_tac [2] asm_rl)
 apply (rule allI)
-apply (rule MGF_lemma)
+apply (rule MGF_lemma [THEN conjunct1, rule_format])
 apply (rule MGF_Impl)
 done
 
+theorem ehoare_relative_complete: "\<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
+apply (rule eMGF_implies_complete)
+apply  (erule_tac [2] asm_rl)
+apply (rule allI)
+apply (rule MGF_lemma [THEN conjunct2, rule_format])
+apply (rule MGF_Impl)
+done
+
 end