# HG changeset patch
# User oheimb
# Date 997267008 -7200
# Node ID 06c1998340a8ba9b8fa90330f7d5d84b9b2c9814
# Parent  11402be6e4b0fcf642c94c602bd7f61d1a0f2af4
changed to full expressions with side effects

diff -r 11402be6e4b0 -r 06c1998340a8 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Tue Aug 07 22:42:22 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Wed Aug 08 12:36:48 2001 +0200
@@ -9,102 +9,150 @@
 theory AxSem = State:
 
 types assn   = "state => bool"
-      triple = "assn \<times> stmt \<times> assn"
+     vassn   = "val \<Rightarrow> assn"
+      triple = "assn \<times> stmt \<times>  assn"
+     etriple = "assn \<times> expr \<times> vassn"
 translations
   "assn"   \<leftharpoondown> (type)"state => bool"
-  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
+ "vassn"   \<leftharpoondown> (type)"val => assn"
+  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times>  assn"
+ "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
 
-consts   hoare   :: "(triple set \<times> triple set) set"
+consts   hoare   :: "(triple set \<times>  triple set) set"
+consts  ehoare   :: "(triple set \<times> etriple    ) set"
 syntax (xsymbols)
  "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
  "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
                                    ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
+"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ |\<turnstile>e/ _"[61,61]60)
+"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
+                                  ("_ \<turnstile>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
 syntax
  "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
  "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
                                   ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
+"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ ||-e/ _"[61,61] 60)
+"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
+                                 ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
 
-translations "A |\<turnstile> C"       \<rightleftharpoons> "(A,C) \<in> hoare"
-             "A  \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
+translations "A |\<turnstile> C"        \<rightleftharpoons> "(A,C) \<in> hoare"
+             "A  \<turnstile> {P}c{Q}"  \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
+             "A |\<turnstile>e t"       \<rightleftharpoons> "(A,t) \<in> ehoare"
+             "A |\<turnstile>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
+             "A  \<turnstile>e{P}e{Q}"  \<rightleftharpoons> "A |\<turnstile>e (P,e,Q)"
 
-inductive hoare
+
+inductive hoare ehoare
 intros
 
   Skip:  "A |- {P} Skip {P}"
 
   Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
 
-  Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q}; 
-            A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q}  |] ==>
-            A |- {P} If(e) c1 Else c2 {Q}"
+  Cond: "[| A |-e {P} e {Q}; 
+            \<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
+            A |- {P} If(e) c1 Else c2 {R}"
+
+  Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
+         A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
 
-  Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
-         A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
+  LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
 
-  NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
-              x:=new C {P}"
+  LAss: "A |-e {P} e {\<lambda>v s.  Q (lupd(x\<mapsto>v) s)} ==>
+         A |-  {P} x:==e {Q}"
+
+  FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
+         A |-e {P} e..f {Q}"
 
-  Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
-              P (lupd(x|->s<y>) s)} x:=(C)y {P}"
+  FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
+        \<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
+            A |-  {P} e1..f:==e2 {R}"
 
-  FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
+  NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
+                new C {P}"
 
-  FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
+  Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True 
+                                 | Addr a => obj_class s a <=C C) --> Q v s} ==>
+         A |-e {P} Cast C e {Q}"
 
-  Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and> 
-                    s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
-                  Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
-             A |- {P} x:={C}y..m(p) {Q}"
+  Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
+    \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> 
+                    s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s))}
+                  Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
+             A |-e {P} {C}e1..m(e2) {S}"
 
   Meth: "\<forall>D. A |- {\<lambda>s. \<exists>a. s<This> = Addr a \<and> D=obj_class s a \<and> D <=C C \<and> P s}
                   Impl D m {Q} ==>
              A |- {P} Meth C m {Q}"
 
   (*\<Union>z instead of \<forall>z in the conclusion and
-      z restricted to type state due to limitations of the inductive paackage *)
+      z restricted to type state due to limitations of the inductive package *)
   Impl: "A\<union>   (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||- 
                (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
          A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
 
 (* structural rules *)
 
-  (* z restricted to type state due to limitations of the inductive paackage *)
+  Asm:  "   a \<in> A ==> A ||- {a}"
+
+  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
+
+  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
+
+  (* z restricted to type state due to limitations of the inductive package *)
   Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
              \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
             A |- {P} c {Q }"
 
-  Asm:  "   a \<in> A ==> A ||- {a}"
-
-  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
-
-  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
+  (* z restricted to type state due to limitations of the inductive package *)
+ eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
+             \<forall>s v t. (\<forall>z::state. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
+            A |-e {P} c {Q }"
 
 
 subsection "Derived Rules"
 
 lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
-apply (rule hoare.Conseq)
+apply (rule hoare_ehoare.Conseq)
+apply  (rule allI, assumption)
+apply fast
+done
+
+lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
+apply (rule hoare_ehoare.Conseq)
+apply  (rule allI, assumption)
+apply fast
+done
+
+lemma eConseq1: "\<lbrakk>A \<turnstile>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
+apply (rule hoare_ehoare.eConseq)
+apply  (rule allI, assumption)
+apply fast
+done
+
+lemma eConseq2: "\<lbrakk>A \<turnstile>e {P} e {Q'}; \<forall>v t. Q' v t \<longrightarrow> Q v t\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
+apply (rule hoare_ehoare.eConseq)
 apply  (rule allI, assumption)
 apply fast
 done
 
 lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
-apply (rule hoare.ConjI)
+apply (rule hoare_ehoare.ConjI)
 apply clarify
-apply (drule hoare.ConjE)
+apply (drule hoare_ehoare.ConjE)
 apply  fast
 apply assumption
 done
 
 lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
-by (auto intro: hoare.ConjI hoare.ConjE)
+by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
 
 lemma Impl': 
   "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
                 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
        A    ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
 apply (drule Union[THEN iffD2])
-apply (drule hoare.Impl)
+apply (drule hoare_ehoare.Impl)
 apply (drule Union[THEN iffD1])
 apply (erule spec)
 done
diff -r 11402be6e4b0 -r 06c1998340a8 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Tue Aug 07 22:42:22 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Wed Aug 08 12:36:48 2001 +0200
@@ -11,71 +11,79 @@
 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"
+  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"
+ 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)
+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)
+cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>e/ _"[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"
+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)
+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!]
+declare exec_elim_cases [elim!] eval_elim_cases [elim!]
 
-lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
-by (clarsimp simp add: nvalid1_def2)
+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: 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: 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
 
@@ -84,27 +92,47 @@
           (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)
@@ -116,35 +144,51 @@
 
 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)
+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.intros[intro!]
+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)
@@ -154,62 +198,85 @@
 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")
+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.Skip])
+apply (rule Conseq1 [OF hoare_ehoare.Skip])
 apply blast
 
-apply (rule hoare.Comp)
+apply (rule hoare_ehoare.Comp)
 apply  (erule spec)
-apply (erule hoare.Conseq)
-apply (erule thin_rl, erule thin_rl)
+apply (erule hoare_ehoare.Conseq)
 apply clarsimp
-apply (drule (1) exec_max2)
+apply (drule (1) exec_exec_max)
 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 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 (rule Conseq1 [OF hoare.NewC])
-apply blast
+apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
+apply fast
 
-apply (rule Conseq1 [OF hoare.Cast])
-apply blast
-
-apply (rule Conseq1 [OF hoare.FAcc])
+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 Conseq1 [OF hoare.FAss])
-apply blast
-
-apply (rule hoare.Call)
-apply (rule allI)
-apply (rule hoare.Meth)
+apply (rule hoare_ehoare.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 (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 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}"
@@ -217,12 +284,12 @@
 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
 
@@ -230,7 +297,15 @@
 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
 
diff -r 11402be6e4b0 -r 06c1998340a8 src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Tue Aug 07 22:42:22 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Wed Aug 08 12:36:48 2001 +0200
@@ -9,81 +9,116 @@
 theory OpSem = State:
 
 consts
-  exec :: "(state \<times> stmt \<times> nat \<times> state) set"
+ exec :: "(state \<times> stmt       \<times> nat \<times> state) set"
+ eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
 syntax (xsymbols)
-  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_\<rightarrow> _" [98,90,99,98] 89)
+ exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   99,98] 89)
+ eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,99,98] 89)
 syntax
-  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_-> _" [98,90,99,98] 89)
+ exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   99,98]89)
+ eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,99,98]89)
 translations
-  "s -c-n-> s'" == "(s, c, n, s') \<in> exec"
+ "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
+ "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
 
-inductive exec intros
+inductive exec eval intros
 
   Skip: "   s -Skip-n-> s"
 
   Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
             s0 -c1;; c2-n-> s2"
 
-  Cond: "[| s -(if s<e> \<noteq> Null then c1 else c2)-n-> s' |] ==>
-            s -If(e) c1 Else c2-n-> s'"
+  Cond: "[| s0 -e>v-n-> s1; s1 -(if v\<noteq>Null then c1 else c2)-n-> s2 |] ==>
+            s0 -If(e) c1 Else c2-n-> s2"
+
+  LoopF:"   s0<x> = Null ==>
+            s0 -While(x) c-n-> s0"
+  LoopT:"[| s0<x> \<noteq> Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==>
+            s0 -While(x) c-n-> s2"
 
-  LoopF:"   s0<e> = Null ==>
-            s0 -While(e) c-n-> s0"
-  LoopT:"[| s0<e> \<noteq> Null; s0 -c-n-> s1; s1 -While(e) c-n-> s2 |] ==>
-            s0 -While(e) c-n-> s2"
+  LAcc: "   s -LAcc x>s<x>-n-> s"
+
+  LAss: "   s -e>v-n-> s' ==>
+            s -x:==e-n-> lupd(x\<mapsto>v) s'"
+
+  FAcc: "   s -e>Addr a-n-> s' ==>
+            s -e..f>get_field s' a f-n-> s'"
+
+  FAss: "[| s0 -e1>Addr a-n-> s1;  s1 -e2>v-n-> s2 |] ==>
+            s0 -e1..f:==e2-n-> upd_obj a f v s2"
 
   NewC: "   new_Addr s = Addr a ==>
-            s -x:=new C-n-> lupd(x\<mapsto>Addr a)(new_obj a C s)"
-
-  Cast: "  (case s<y> of Null => True | Addr a => obj_class s a \<preceq>C C) ==>
-            s -x:=(C)y-n-> lupd(x\<mapsto>s<y>) s"
+            s -new C>Addr a-n-> new_obj a C s"
 
-  FAcc: "   s<y> = Addr a ==>
-            s -x:=y..f-n-> lupd(x\<mapsto>get_field s a f) s"
+  Cast: "[| s -e>v-n-> s';
+            case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
+            s -Cast C e>v-n-> s'"
 
-  FAss: "   s<y> = Addr a ==>
-            s -y..f:=x-n-> upd_obj a f (s<x>) s"
-
-  Call: "lupd(This\<mapsto>s<y>)(lupd(Param\<mapsto>s<p>)(init_locs C m s))-Meth C m -n-> s'==>
-            s -x:={C}y..m(p)-n-> lupd(x\<mapsto>s'<Res>)(set_locs s s')"
+  Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
+            lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s2)) -Meth C m-n-> s3
+     |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
 
   Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
             s -Impl (obj_class s a) m-n-> s' |] ==>
             s -Meth C m-n-> s'"
 
-  Impl: "   s -body C m-    n-> s' ==>
+  Impl: "   s -body C m-n-> s' ==>
             s -Impl C m-Suc n-> s'"
 
+
 inductive_cases exec_elim_cases':
-	"s -Skip            -n-> t"
-	"s -c1;; c2         -n-> t"
-	"s -If(e) c1 Else c2-n-> t"
-	"s -While(e) c      -n-> t"
-	"s -x:=new C        -n-> t"
-	"s -x:=(C)y         -n-> t"
-	"s -x:=y..f         -n-> t"
-	"s -y..f:=x         -n-> t"
-	"s -x:={C}y..m(p)   -n-> t"
-inductive_cases Meth_elim_cases: "s -Meth C m -n-> t"
-inductive_cases Impl_elim_cases: "s -Impl C m -n-> t"
+	"s -Skip            -n\<rightarrow> t"
+	"s -c1;; c2         -n\<rightarrow> t"
+	"s -If(e) c1 Else c2-n\<rightarrow> t"
+	"s -While(x) c      -n\<rightarrow> t"
+	"s -x:==e           -n\<rightarrow> t"
+	"s -e1..f:==e2      -n\<rightarrow> t"
+inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t"
+inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t"
 lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
+inductive_cases eval_elim_cases:
+	"s -new C         \<succ>v-n\<rightarrow> t"
+	"s -Cast C e      \<succ>v-n\<rightarrow> t"
+	"s -LAcc x        \<succ>v-n\<rightarrow> t"
+	"s -e..f          \<succ>v-n\<rightarrow> t"
+	"s -{C}e1..m(e2)  \<succ>v-n\<rightarrow> t"
 
-lemma exec_mono [rule_format]: "s -c-n\<rightarrow> t \<Longrightarrow> \<forall>m. n \<le> m \<longrightarrow> s -c-m\<rightarrow> t"
-apply (erule exec.induct)
-prefer 12 (* Impl *)
+lemma exec_eval_mono [rule_format]: 
+  "(s -c  -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c  -m\<rightarrow> t)) \<and>
+   (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))"
+apply (rule exec_eval.induct)
+prefer 14 (* Impl *)
 apply clarify
 apply (rename_tac n)
 apply (case_tac n)
-apply (blast intro:exec.intros)+
+apply  (blast intro:exec_eval.intros)+
 done
+lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
+lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]
+
+lemma exec_exec_max: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
+                       s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
+by (fast intro: exec_mono le_maxI1 le_maxI2)
 
-lemma exec_max2: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-        n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
-                   s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
-by (fast intro: exec_mono le_maxI1 le_maxI2)
+lemma eval_exec_max: "\<lbrakk>s1 -c-    n1   \<rightarrow> t1 ; s2 -e\<succ>v-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
+                       s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
+by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
+
+lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1-    n1   \<rightarrow> t1 ; s2 -e2\<succ>v2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
+                       s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
+by (fast intro: eval_mono le_maxI1 le_maxI2)
+
+lemma eval_eval_exec_max: 
+ "\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 
+   s1 -e1\<succ>v1-max (max n1 n2) n3\<rightarrow> t1 \<and> 
+   s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
+   s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
+apply (drule (1) eval_eval_max, erule thin_rl)
+by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
 
 lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl C m-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body C m-n\<rightarrow> t)"
 apply (rule ext)
-apply (fast elim: exec_elim_cases intro: exec.Impl)
+apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
 done
 
 end
\ No newline at end of file
diff -r 11402be6e4b0 -r 06c1998340a8 src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Tue Aug 07 22:42:22 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy	Wed Aug 08 12:36:48 2001 +0200
@@ -23,20 +23,22 @@
 
 datatype stmt
   = Skip                   (* empty statement *)
-  | Comp       stmt stmt   ("_;; _"             [91,90]    90)
-  | Cond vname stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
+  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
+  | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
   | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
-
-  | NewC vname cname       ("_:=new _"  [99,   99] 95) (* object creation  *)
-  | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
-  | FAcc vname vname vnam  ("_:=_.._"   [99,99,99] 95) (* field access     *)
-  | FAss vname vnam  vname ("_.._:=_"   [99,99,99] 95) (* field assigment  *)
-  | Call vname cname vname mname vname                 (* method call      *)
-                           ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
+  | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
+  | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
   | Meth cname mname       (* virtual method *)
   | Impl cname mname       (* method implementation *)
+and expr
+  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
+  | Cast cname expr                              (* type cast        *)
+  | LAcc vname                                   (* local access     *)
+  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
+  | Call cname expr mname expr                   (* method call      *)
+                     ("{_}_.._'(_')" [99,95,99,95] 95)
 
-(*###TO Product_Type_lemmas.ML*)
+
 lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
 apply (rule_tac x = "(a,b)" in image_eqI)
 apply  auto