changed to full expressions with side effects
authoroheimb
Wed Aug 08 12:36:48 2001 +0200 (2001-08-08)
changeset 1147606c1998340a8
parent 11475 11402be6e4b0
child 11477 4d042d3f957d
changed to full expressions with side effects
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/OpSem.thy
src/HOL/NanoJava/Term.thy
     1.1 --- a/src/HOL/NanoJava/AxSem.thy	Tue Aug 07 22:42:22 2001 +0200
     1.2 +++ b/src/HOL/NanoJava/AxSem.thy	Wed Aug 08 12:36:48 2001 +0200
     1.3 @@ -9,102 +9,150 @@
     1.4  theory AxSem = State:
     1.5  
     1.6  types assn   = "state => bool"
     1.7 -      triple = "assn \<times> stmt \<times> assn"
     1.8 +     vassn   = "val \<Rightarrow> assn"
     1.9 +      triple = "assn \<times> stmt \<times>  assn"
    1.10 +     etriple = "assn \<times> expr \<times> vassn"
    1.11  translations
    1.12    "assn"   \<leftharpoondown> (type)"state => bool"
    1.13 -  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
    1.14 + "vassn"   \<leftharpoondown> (type)"val => assn"
    1.15 +  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times>  assn"
    1.16 + "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
    1.17  
    1.18 -consts   hoare   :: "(triple set \<times> triple set) set"
    1.19 +consts   hoare   :: "(triple set \<times>  triple set) set"
    1.20 +consts  ehoare   :: "(triple set \<times> etriple    ) set"
    1.21  syntax (xsymbols)
    1.22   "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
    1.23   "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
    1.24                                     ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    1.25 +"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ |\<turnstile>e/ _"[61,61]60)
    1.26 +"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
    1.27 +                                  ("_ \<turnstile>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    1.28  syntax
    1.29   "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
    1.30   "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
    1.31                                    ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
    1.32 +"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ ||-e/ _"[61,61] 60)
    1.33 +"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
    1.34 +                                 ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
    1.35  
    1.36 -translations "A |\<turnstile> C"       \<rightleftharpoons> "(A,C) \<in> hoare"
    1.37 -             "A  \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
    1.38 +translations "A |\<turnstile> C"        \<rightleftharpoons> "(A,C) \<in> hoare"
    1.39 +             "A  \<turnstile> {P}c{Q}"  \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
    1.40 +             "A |\<turnstile>e t"       \<rightleftharpoons> "(A,t) \<in> ehoare"
    1.41 +             "A |\<turnstile>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
    1.42 +             "A  \<turnstile>e{P}e{Q}"  \<rightleftharpoons> "A |\<turnstile>e (P,e,Q)"
    1.43  
    1.44 -inductive hoare
    1.45 +
    1.46 +inductive hoare ehoare
    1.47  intros
    1.48  
    1.49    Skip:  "A |- {P} Skip {P}"
    1.50  
    1.51    Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
    1.52  
    1.53 -  Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q}; 
    1.54 -            A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q}  |] ==>
    1.55 -            A |- {P} If(e) c1 Else c2 {Q}"
    1.56 +  Cond: "[| A |-e {P} e {Q}; 
    1.57 +            \<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
    1.58 +            A |- {P} If(e) c1 Else c2 {R}"
    1.59 +
    1.60 +  Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
    1.61 +         A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
    1.62  
    1.63 -  Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
    1.64 -         A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
    1.65 +  LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
    1.66  
    1.67 -  NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
    1.68 -              x:=new C {P}"
    1.69 +  LAss: "A |-e {P} e {\<lambda>v s.  Q (lupd(x\<mapsto>v) s)} ==>
    1.70 +         A |-  {P} x:==e {Q}"
    1.71 +
    1.72 +  FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
    1.73 +         A |-e {P} e..f {Q}"
    1.74  
    1.75 -  Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
    1.76 -              P (lupd(x|->s<y>) s)} x:=(C)y {P}"
    1.77 +  FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
    1.78 +        \<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
    1.79 +            A |-  {P} e1..f:==e2 {R}"
    1.80  
    1.81 -  FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
    1.82 +  NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
    1.83 +                new C {P}"
    1.84  
    1.85 -  FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
    1.86 +  Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True 
    1.87 +                                 | Addr a => obj_class s a <=C C) --> Q v s} ==>
    1.88 +         A |-e {P} Cast C e {Q}"
    1.89  
    1.90 -  Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and> 
    1.91 -                    s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
    1.92 -                  Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
    1.93 -             A |- {P} x:={C}y..m(p) {Q}"
    1.94 +  Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
    1.95 +    \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> 
    1.96 +                    s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s))}
    1.97 +                  Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
    1.98 +             A |-e {P} {C}e1..m(e2) {S}"
    1.99  
   1.100    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}
   1.101                    Impl D m {Q} ==>
   1.102               A |- {P} Meth C m {Q}"
   1.103  
   1.104    (*\<Union>z instead of \<forall>z in the conclusion and
   1.105 -      z restricted to type state due to limitations of the inductive paackage *)
   1.106 +      z restricted to type state due to limitations of the inductive package *)
   1.107    Impl: "A\<union>   (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||- 
   1.108                 (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
   1.109           A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
   1.110  
   1.111  (* structural rules *)
   1.112  
   1.113 -  (* z restricted to type state due to limitations of the inductive paackage *)
   1.114 +  Asm:  "   a \<in> A ==> A ||- {a}"
   1.115 +
   1.116 +  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
   1.117 +
   1.118 +  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
   1.119 +
   1.120 +  (* z restricted to type state due to limitations of the inductive package *)
   1.121    Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
   1.122               \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
   1.123              A |- {P} c {Q }"
   1.124  
   1.125 -  Asm:  "   a \<in> A ==> A ||- {a}"
   1.126 -
   1.127 -  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
   1.128 -
   1.129 -  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
   1.130 +  (* z restricted to type state due to limitations of the inductive package *)
   1.131 + eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
   1.132 +             \<forall>s v t. (\<forall>z::state. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
   1.133 +            A |-e {P} c {Q }"
   1.134  
   1.135  
   1.136  subsection "Derived Rules"
   1.137  
   1.138  lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
   1.139 -apply (rule hoare.Conseq)
   1.140 +apply (rule hoare_ehoare.Conseq)
   1.141 +apply  (rule allI, assumption)
   1.142 +apply fast
   1.143 +done
   1.144 +
   1.145 +lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
   1.146 +apply (rule hoare_ehoare.Conseq)
   1.147 +apply  (rule allI, assumption)
   1.148 +apply fast
   1.149 +done
   1.150 +
   1.151 +lemma eConseq1: "\<lbrakk>A \<turnstile>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
   1.152 +apply (rule hoare_ehoare.eConseq)
   1.153 +apply  (rule allI, assumption)
   1.154 +apply fast
   1.155 +done
   1.156 +
   1.157 +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}"
   1.158 +apply (rule hoare_ehoare.eConseq)
   1.159  apply  (rule allI, assumption)
   1.160  apply fast
   1.161  done
   1.162  
   1.163  lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
   1.164 -apply (rule hoare.ConjI)
   1.165 +apply (rule hoare_ehoare.ConjI)
   1.166  apply clarify
   1.167 -apply (drule hoare.ConjE)
   1.168 +apply (drule hoare_ehoare.ConjE)
   1.169  apply  fast
   1.170  apply assumption
   1.171  done
   1.172  
   1.173  lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
   1.174 -by (auto intro: hoare.ConjI hoare.ConjE)
   1.175 +by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
   1.176  
   1.177  lemma Impl': 
   1.178    "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
   1.179                  (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
   1.180         A    ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
   1.181  apply (drule Union[THEN iffD2])
   1.182 -apply (drule hoare.Impl)
   1.183 +apply (drule hoare_ehoare.Impl)
   1.184  apply (drule Union[THEN iffD1])
   1.185  apply (erule spec)
   1.186  done
     2.1 --- a/src/HOL/NanoJava/Equivalence.thy	Tue Aug 07 22:42:22 2001 +0200
     2.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Aug 08 12:36:48 2001 +0200
     2.3 @@ -11,71 +11,79 @@
     2.4  subsection "Validity"
     2.5  
     2.6  constdefs
     2.7 -  valid   :: "[assn,stmt,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
     2.8 - "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c-n-> t) --> Q t"
     2.9 +  valid   :: "[assn,stmt, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    2.10 + "|=  {P} c {Q} \<equiv> \<forall>s   t. P s --> (\<exists>n. s -c  -n-> t) --> Q   t"
    2.11 +
    2.12 + evalid   :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    2.13 + "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e>v-n-> t) --> Q v t"
    2.14 +
    2.15  
    2.16 - nvalid   :: "[nat,       triple    ] => bool" ("|=_: _"  [61,61] 60)
    2.17 - "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c-n-> t --> P s --> Q t"
    2.18 + nvalid   :: "[nat, triple    ] => bool" ("|=_: _"  [61,61] 60)
    2.19 + "|=n:  t \<equiv> let (P,c,Q) = t in \<forall>s   t. s -c  -n-> t --> P s --> Q   t"
    2.20  
    2.21 - nvalids  :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
    2.22 +envalid   :: "[nat,etriple    ] => bool" ("|=_:e _" [61,61] 60)
    2.23 + "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e>v-n-> t --> P s --> Q v t"
    2.24 +
    2.25 +  nvalids :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
    2.26   "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
    2.27  
    2.28 - cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"[61,61] 60)
    2.29 - "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
    2.30 + cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"  [61,61] 60)
    2.31 + "A ||=  C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
    2.32 +
    2.33 +cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60)
    2.34 + "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
    2.35  
    2.36  syntax (xsymbols)
    2.37 -  valid   :: "[assn,stmt,assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    2.38 - nvalid   :: "[nat,       triple    ] => bool" ("\<Turnstile>_: _"   [61,61] 60)
    2.39 - nvalids  :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
    2.40 +   valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    2.41 +  evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    2.42 +  nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
    2.43 + envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:e _" [61,61] 60)
    2.44 +  nvalids :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
    2.45   cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
    2.46 +cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>e/ _"[61,61] 60)
    2.47  
    2.48 -syntax
    2.49 -  nvalid1::"[nat,        assn,stmt,assn] => bool" ( "|=_:.{(1_)}/ (_)/ {(1_)}"
    2.50 -                                                         [61,3,90,3] 60)
    2.51 - cnvalid1::"[triple set, assn,stmt,assn] => bool" ("_ ||=.{(1_)}/ (_)/ {(1_)}"
    2.52 -                                                         [61,3,90,3] 60)
    2.53 -syntax (xsymbols)
    2.54 -  nvalid1::"[nat,        assn,stmt,assn] => bool" (  "\<Turnstile>_:.{(1_)}/ (_)/ {(1_)}"
    2.55 -                                                         [61,3,90,3] 60)
    2.56 - cnvalid1::"[triple set, assn,stmt,assn] => bool" ( "_ |\<Turnstile>.{(1_)}/ (_)/ {(1_)}"
    2.57 -                                                         [61,3,90,3] 60)
    2.58 -translations
    2.59 - " \<Turnstile>n:.{P} c {Q}" \<rightleftharpoons> " \<Turnstile>n:  (P,c,Q)"
    2.60 - "A |\<Turnstile>.{P} c {Q}" \<rightleftharpoons> "A |\<Turnstile> {(P,c,Q)}"
    2.61  
    2.62 -lemma nvalid1_def2: "\<Turnstile>n:.{P} c {Q} \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    2.63 +lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    2.64  by (simp add: nvalid_def Let_def)
    2.65  
    2.66 -lemma cnvalid1_def2: 
    2.67 -  "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)"
    2.68 -by(simp add: nvalid1_def2 nvalids_def cnvalids_def)
    2.69 -
    2.70 -lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n:.{P} c {Q})"
    2.71 -apply (simp add: valid_def nvalid1_def2)
    2.72 +lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))"
    2.73 +apply (simp add: valid_def nvalid_def2)
    2.74  apply blast
    2.75  done
    2.76  
    2.77 +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"
    2.78 +by (simp add: envalid_def Let_def)
    2.79 +
    2.80 +lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (\<forall>n. \<Turnstile>n:e (P,e,Q))"
    2.81 +apply (simp add: evalid_def envalid_def2)
    2.82 +apply blast
    2.83 +done
    2.84 +
    2.85 +lemma cenvalid_def2: 
    2.86 +  "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))"
    2.87 +by(simp add: cenvalid_def envalid_def2) 
    2.88 +
    2.89  
    2.90  subsection "Soundness"
    2.91  
    2.92 -declare exec_elim_cases [elim!]
    2.93 +declare exec_elim_cases [elim!] eval_elim_cases [elim!]
    2.94  
    2.95 -lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
    2.96 -by (clarsimp simp add: nvalid1_def2)
    2.97 +lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)"
    2.98 +by (clarsimp simp add: nvalid_def2)
    2.99  
   2.100 -lemma Impl_nvalid_Suc: "\<Turnstile>n:.{P} body C m {Q} \<Longrightarrow> \<Turnstile>Suc n:.{P} Impl C m {Q}"
   2.101 -by (clarsimp simp add: nvalid1_def2)
   2.102 +lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)"
   2.103 +by (clarsimp simp add: nvalid_def2)
   2.104  
   2.105  lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
   2.106 -by (force simp add: split_paired_all nvalid1_def2 intro: exec_mono)
   2.107 +by (force simp add: split_paired_all nvalid_def2 intro: exec_mono)
   2.108  
   2.109  lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow>  Ball A (nvalid n)"
   2.110  by (fast intro: nvalid_SucD)
   2.111  
   2.112  lemma Loop_sound_lemma [rule_format (no_asm)]: 
   2.113 -"\<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> 
   2.114 -  P s \<longrightarrow> c0 = While (e) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<e> = Null"
   2.115 -apply (erule exec.induct)
   2.116 +"\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
   2.117 +  (s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
   2.118 +apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
   2.119  apply clarsimp+
   2.120  done
   2.121  
   2.122 @@ -84,27 +92,47 @@
   2.123            (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
   2.124  by blast
   2.125  
   2.126 -lemma hoare_sound_main: "A |\<turnstile> C \<Longrightarrow> A |\<Turnstile> C"
   2.127 -apply (erule hoare.induct)
   2.128 -apply (simp_all only: cnvalid1_def2)
   2.129 -apply clarsimp
   2.130 -apply clarsimp
   2.131 -apply (clarsimp split add: split_if_asm)
   2.132 -apply (clarsimp,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
   2.133 -apply clarsimp
   2.134 -apply clarsimp
   2.135 -apply clarsimp
   2.136 -apply clarsimp
   2.137 +lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
   2.138 +by fast
   2.139 +
   2.140 +lemma all3_conjunct2: 
   2.141 +  "\<forall>a p l. (P' a p l \<and> P a p l) \<Longrightarrow> \<forall>a p l. P a p l"
   2.142 +by fast
   2.143 +
   2.144 +lemma cnvalid1_eq: 
   2.145 +  "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)"
   2.146 +by(simp add: cnvalids_def nvalids_def nvalid_def2)
   2.147 +
   2.148 +lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>e t \<longrightarrow> A |\<Turnstile>e t)"
   2.149 +apply (tactic "split_all_tac 1", rename_tac P e Q)
   2.150 +apply (rule hoare_ehoare.induct)
   2.151 +apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
   2.152 +apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x :  hoare") *})
   2.153 +apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
   2.154 +apply (simp_all only: cnvalid1_eq cenvalid_def2)
   2.155 +apply fast
   2.156 +apply fast
   2.157 +apply fast
   2.158 +apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
   2.159 +apply fast
   2.160 +apply fast
   2.161 +apply fast
   2.162 +apply fast
   2.163 +apply fast
   2.164 +apply fast
   2.165  apply (clarsimp del: Meth_elim_cases) (* Call *)
   2.166 +apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
   2.167 +apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
   2.168 +apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
   2.169  apply (clarsimp del: Impl_elim_cases) (* Meth *)
   2.170  defer
   2.171 -apply blast (* Conseq *)
   2.172 +prefer 4 apply blast (*  Conseq *)
   2.173 +prefer 4 apply blast (* eConseq *)
   2.174  apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
   2.175  apply blast
   2.176  apply blast
   2.177  apply blast
   2.178  (* Impl *)
   2.179 -apply (erule thin_rl)
   2.180  apply (rule allI)
   2.181  apply (induct_tac "n")
   2.182  apply  (clarify intro!: Impl_nvalid_0)
   2.183 @@ -116,35 +144,51 @@
   2.184  
   2.185  theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
   2.186  apply (simp only: valid_def2)
   2.187 -apply (drule hoare_sound_main)
   2.188 +apply (drule hoare_sound_main [THEN conjunct1, rule_format])
   2.189  apply (unfold cnvalids_def nvalids_def)
   2.190  apply fast
   2.191  done
   2.192  
   2.193 +theorem ehoare_sound: "{} \<turnstile>e {P} e {Q} \<Longrightarrow> \<Turnstile>e {P} e {Q}"
   2.194 +apply (simp only: evalid_def2)
   2.195 +apply (drule hoare_sound_main [THEN conjunct2, rule_format])
   2.196 +apply (unfold cenvalid_def nvalids_def)
   2.197 +apply fast
   2.198 +done
   2.199 +
   2.200  
   2.201  subsection "(Relative) Completeness"
   2.202  
   2.203 -constdefs MGT    :: "stmt => state => triple"
   2.204 -         "MGT c z \<equiv> (\<lambda> s. z = s, c, %t. \<exists>n. z -c-n-> t)"
   2.205 +constdefs MGT    :: "stmt => state =>  triple"
   2.206 +         "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda>  t. \<exists>n. z -c-  n-> t)"
   2.207 +         eMGT    :: "expr => state => etriple"
   2.208 +        "eMGT e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
   2.209  
   2.210  lemma MGF_implies_complete:
   2.211 - "\<forall>z. {} |\<turnstile> {MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
   2.212 + "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
   2.213  apply (simp only: valid_def2)
   2.214  apply (unfold MGT_def)
   2.215 -apply (erule hoare.Conseq)
   2.216 -apply (clarsimp simp add: nvalid1_def2)
   2.217 +apply (erule hoare_ehoare.Conseq)
   2.218 +apply (clarsimp simp add: nvalid_def2)
   2.219  done
   2.220  
   2.221 +lemma eMGF_implies_complete:
   2.222 + "\<forall>z. {} |\<turnstile>e eMGT e z \<Longrightarrow> \<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
   2.223 +apply (simp only: evalid_def2)
   2.224 +apply (unfold eMGT_def)
   2.225 +apply (erule hoare_ehoare.eConseq)
   2.226 +apply (clarsimp simp add: envalid_def2)
   2.227 +done
   2.228  
   2.229 -declare exec.intros[intro!]
   2.230 +declare exec_eval.intros[intro!]
   2.231  
   2.232  lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
   2.233    A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
   2.234  apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
   2.235 -       in hoare.Conseq)
   2.236 +       in hoare_ehoare.Conseq)
   2.237  apply  (rule allI)
   2.238 -apply  (rule hoare.Loop)
   2.239 -apply  (erule hoare.Conseq)
   2.240 +apply  (rule hoare_ehoare.Loop)
   2.241 +apply  (erule hoare_ehoare.Conseq)
   2.242  apply  clarsimp
   2.243  apply  (blast intro:rtrancl_into_rtrancl)
   2.244  apply (erule thin_rl)
   2.245 @@ -154,62 +198,85 @@
   2.246  apply (erule converse_rtrancl_induct)
   2.247  apply  blast
   2.248  apply clarsimp
   2.249 -apply (drule (1) exec_max2)
   2.250 +apply (drule (1) exec_exec_max)
   2.251  apply (blast del: exec_elim_cases)
   2.252  done
   2.253  
   2.254 -lemma MGF_lemma[rule_format]:
   2.255 - "(\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z}) \<longrightarrow> (\<forall>z. A |\<turnstile> {MGT c z})"
   2.256 -apply (simp add: MGT_def)
   2.257 -apply (induct_tac c)
   2.258 -apply (tactic "ALLGOALS Clarify_tac")
   2.259 +lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> 
   2.260 + (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>e eMGT e z)"
   2.261 +apply (simp add: MGT_def eMGT_def)
   2.262 +apply (rule stmt_expr.induct)
   2.263 +apply (rule_tac [!] allI)
   2.264  
   2.265 -apply (rule Conseq1 [OF hoare.Skip])
   2.266 +apply (rule Conseq1 [OF hoare_ehoare.Skip])
   2.267  apply blast
   2.268  
   2.269 -apply (rule hoare.Comp)
   2.270 +apply (rule hoare_ehoare.Comp)
   2.271  apply  (erule spec)
   2.272 -apply (erule hoare.Conseq)
   2.273 -apply (erule thin_rl, erule thin_rl)
   2.274 +apply (erule hoare_ehoare.Conseq)
   2.275  apply clarsimp
   2.276 -apply (drule (1) exec_max2)
   2.277 +apply (drule (1) exec_exec_max)
   2.278  apply blast
   2.279  
   2.280 -apply (rule hoare.Cond)
   2.281 -apply  (erule hoare.Conseq)
   2.282 -apply  (erule thin_rl, erule thin_rl)
   2.283 -apply  force
   2.284 -apply (erule hoare.Conseq)
   2.285 -apply (erule thin_rl, erule thin_rl)
   2.286 -apply force
   2.287 +apply (erule thin_rl)
   2.288 +apply (rule hoare_ehoare.Cond)
   2.289 +apply  (erule spec)
   2.290 +apply (rule allI)
   2.291 +apply (simp)
   2.292 +apply (rule conjI)
   2.293 +apply  (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max,
   2.294 +        erule thin_rl, erule thin_rl, force)+
   2.295  
   2.296  apply (erule MGF_Loop)
   2.297  
   2.298 -apply (rule Conseq1 [OF hoare.NewC])
   2.299 -apply blast
   2.300 +apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
   2.301 +apply fast
   2.302  
   2.303 -apply (rule Conseq1 [OF hoare.Cast])
   2.304 -apply blast
   2.305 -
   2.306 -apply (rule Conseq1 [OF hoare.FAcc])
   2.307 +apply (erule thin_rl)
   2.308 +apply (rule_tac Q = "\<lambda>a s. \<exists>n. z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
   2.309 +apply  (drule spec)
   2.310 +apply  (erule eConseq2)
   2.311 +apply  fast
   2.312 +apply (rule allI)
   2.313 +apply (erule hoare_ehoare.eConseq)
   2.314 +apply clarsimp
   2.315 +apply (drule (1) eval_eval_max)
   2.316  apply blast
   2.317  
   2.318 -apply (rule Conseq1 [OF hoare.FAss])
   2.319 -apply blast
   2.320 -
   2.321 -apply (rule hoare.Call)
   2.322 -apply (rule allI)
   2.323 -apply (rule hoare.Meth)
   2.324 +apply (rule hoare_ehoare.Meth)
   2.325  apply (rule allI)
   2.326 -apply (drule spec, drule spec, erule hoare.Conseq)
   2.327 -apply blast
   2.328 -
   2.329 -apply (rule hoare.Meth)
   2.330 -apply (rule allI)
   2.331 -apply (drule spec, drule spec, erule hoare.Conseq)
   2.332 +apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
   2.333  apply blast
   2.334  
   2.335  apply blast
   2.336 +
   2.337 +apply (rule eConseq1 [OF hoare_ehoare.NewC])
   2.338 +apply blast
   2.339 +
   2.340 +apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast])
   2.341 +apply fast
   2.342 +
   2.343 +apply (rule eConseq1 [OF hoare_ehoare.LAcc])
   2.344 +apply blast
   2.345 +
   2.346 +apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
   2.347 +apply fast
   2.348 +
   2.349 +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
   2.350 +                hoare_ehoare.Call)
   2.351 +apply   (erule spec)
   2.352 +apply  (rule allI)
   2.353 +apply  (erule hoare_ehoare.eConseq)
   2.354 +apply  clarsimp
   2.355 +apply  blast
   2.356 +apply (rule allI)+
   2.357 +apply (rule hoare_ehoare.Meth)
   2.358 +apply (rule allI)
   2.359 +apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
   2.360 +apply (erule thin_rl, erule thin_rl)
   2.361 +apply (clarsimp del: Impl_elim_cases)
   2.362 +apply (drule (2) eval_eval_exec_max)
   2.363 +apply (fast del: Impl_elim_cases)
   2.364  done
   2.365  
   2.366  lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
   2.367 @@ -217,12 +284,12 @@
   2.368  apply (rule Impl1)
   2.369  apply  (rule_tac [2] UNIV_I)
   2.370  apply clarsimp
   2.371 -apply (rule hoare.ConjI)
   2.372 +apply (rule hoare_ehoare.ConjI)
   2.373  apply clarsimp
   2.374  apply (rule ssubst [OF Impl_body_eq])
   2.375  apply (fold MGT_def)
   2.376 -apply (rule MGF_lemma)
   2.377 -apply (rule hoare.Asm)
   2.378 +apply (rule MGF_lemma [THEN conjunct1, rule_format])
   2.379 +apply (rule hoare_ehoare.Asm)
   2.380  apply force
   2.381  done
   2.382  
   2.383 @@ -230,7 +297,15 @@
   2.384  apply (rule MGF_implies_complete)
   2.385  apply  (erule_tac [2] asm_rl)
   2.386  apply (rule allI)
   2.387 -apply (rule MGF_lemma)
   2.388 +apply (rule MGF_lemma [THEN conjunct1, rule_format])
   2.389 +apply (rule MGF_Impl)
   2.390 +done
   2.391 +
   2.392 +theorem ehoare_relative_complete: "\<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
   2.393 +apply (rule eMGF_implies_complete)
   2.394 +apply  (erule_tac [2] asm_rl)
   2.395 +apply (rule allI)
   2.396 +apply (rule MGF_lemma [THEN conjunct2, rule_format])
   2.397  apply (rule MGF_Impl)
   2.398  done
   2.399  
     3.1 --- a/src/HOL/NanoJava/OpSem.thy	Tue Aug 07 22:42:22 2001 +0200
     3.2 +++ b/src/HOL/NanoJava/OpSem.thy	Wed Aug 08 12:36:48 2001 +0200
     3.3 @@ -9,81 +9,116 @@
     3.4  theory OpSem = State:
     3.5  
     3.6  consts
     3.7 -  exec :: "(state \<times> stmt \<times> nat \<times> state) set"
     3.8 + exec :: "(state \<times> stmt       \<times> nat \<times> state) set"
     3.9 + eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
    3.10  syntax (xsymbols)
    3.11 -  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_\<rightarrow> _" [98,90,99,98] 89)
    3.12 + exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   99,98] 89)
    3.13 + eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,99,98] 89)
    3.14  syntax
    3.15 -  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_-> _" [98,90,99,98] 89)
    3.16 + exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   99,98]89)
    3.17 + eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,99,98]89)
    3.18  translations
    3.19 -  "s -c-n-> s'" == "(s, c, n, s') \<in> exec"
    3.20 + "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
    3.21 + "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
    3.22  
    3.23 -inductive exec intros
    3.24 +inductive exec eval intros
    3.25  
    3.26    Skip: "   s -Skip-n-> s"
    3.27  
    3.28    Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
    3.29              s0 -c1;; c2-n-> s2"
    3.30  
    3.31 -  Cond: "[| s -(if s<e> \<noteq> Null then c1 else c2)-n-> s' |] ==>
    3.32 -            s -If(e) c1 Else c2-n-> s'"
    3.33 +  Cond: "[| s0 -e>v-n-> s1; s1 -(if v\<noteq>Null then c1 else c2)-n-> s2 |] ==>
    3.34 +            s0 -If(e) c1 Else c2-n-> s2"
    3.35 +
    3.36 +  LoopF:"   s0<x> = Null ==>
    3.37 +            s0 -While(x) c-n-> s0"
    3.38 +  LoopT:"[| s0<x> \<noteq> Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==>
    3.39 +            s0 -While(x) c-n-> s2"
    3.40  
    3.41 -  LoopF:"   s0<e> = Null ==>
    3.42 -            s0 -While(e) c-n-> s0"
    3.43 -  LoopT:"[| s0<e> \<noteq> Null; s0 -c-n-> s1; s1 -While(e) c-n-> s2 |] ==>
    3.44 -            s0 -While(e) c-n-> s2"
    3.45 +  LAcc: "   s -LAcc x>s<x>-n-> s"
    3.46 +
    3.47 +  LAss: "   s -e>v-n-> s' ==>
    3.48 +            s -x:==e-n-> lupd(x\<mapsto>v) s'"
    3.49 +
    3.50 +  FAcc: "   s -e>Addr a-n-> s' ==>
    3.51 +            s -e..f>get_field s' a f-n-> s'"
    3.52 +
    3.53 +  FAss: "[| s0 -e1>Addr a-n-> s1;  s1 -e2>v-n-> s2 |] ==>
    3.54 +            s0 -e1..f:==e2-n-> upd_obj a f v s2"
    3.55  
    3.56    NewC: "   new_Addr s = Addr a ==>
    3.57 -            s -x:=new C-n-> lupd(x\<mapsto>Addr a)(new_obj a C s)"
    3.58 -
    3.59 -  Cast: "  (case s<y> of Null => True | Addr a => obj_class s a \<preceq>C C) ==>
    3.60 -            s -x:=(C)y-n-> lupd(x\<mapsto>s<y>) s"
    3.61 +            s -new C>Addr a-n-> new_obj a C s"
    3.62  
    3.63 -  FAcc: "   s<y> = Addr a ==>
    3.64 -            s -x:=y..f-n-> lupd(x\<mapsto>get_field s a f) s"
    3.65 +  Cast: "[| s -e>v-n-> s';
    3.66 +            case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
    3.67 +            s -Cast C e>v-n-> s'"
    3.68  
    3.69 -  FAss: "   s<y> = Addr a ==>
    3.70 -            s -y..f:=x-n-> upd_obj a f (s<x>) s"
    3.71 -
    3.72 -  Call: "lupd(This\<mapsto>s<y>)(lupd(Param\<mapsto>s<p>)(init_locs C m s))-Meth C m -n-> s'==>
    3.73 -            s -x:={C}y..m(p)-n-> lupd(x\<mapsto>s'<Res>)(set_locs s s')"
    3.74 +  Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
    3.75 +            lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s2)) -Meth C m-n-> s3
    3.76 +     |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
    3.77  
    3.78    Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
    3.79              s -Impl (obj_class s a) m-n-> s' |] ==>
    3.80              s -Meth C m-n-> s'"
    3.81  
    3.82 -  Impl: "   s -body C m-    n-> s' ==>
    3.83 +  Impl: "   s -body C m-n-> s' ==>
    3.84              s -Impl C m-Suc n-> s'"
    3.85  
    3.86 +
    3.87  inductive_cases exec_elim_cases':
    3.88 -	"s -Skip            -n-> t"
    3.89 -	"s -c1;; c2         -n-> t"
    3.90 -	"s -If(e) c1 Else c2-n-> t"
    3.91 -	"s -While(e) c      -n-> t"
    3.92 -	"s -x:=new C        -n-> t"
    3.93 -	"s -x:=(C)y         -n-> t"
    3.94 -	"s -x:=y..f         -n-> t"
    3.95 -	"s -y..f:=x         -n-> t"
    3.96 -	"s -x:={C}y..m(p)   -n-> t"
    3.97 -inductive_cases Meth_elim_cases: "s -Meth C m -n-> t"
    3.98 -inductive_cases Impl_elim_cases: "s -Impl C m -n-> t"
    3.99 +	"s -Skip            -n\<rightarrow> t"
   3.100 +	"s -c1;; c2         -n\<rightarrow> t"
   3.101 +	"s -If(e) c1 Else c2-n\<rightarrow> t"
   3.102 +	"s -While(x) c      -n\<rightarrow> t"
   3.103 +	"s -x:==e           -n\<rightarrow> t"
   3.104 +	"s -e1..f:==e2      -n\<rightarrow> t"
   3.105 +inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t"
   3.106 +inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t"
   3.107  lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
   3.108 +inductive_cases eval_elim_cases:
   3.109 +	"s -new C         \<succ>v-n\<rightarrow> t"
   3.110 +	"s -Cast C e      \<succ>v-n\<rightarrow> t"
   3.111 +	"s -LAcc x        \<succ>v-n\<rightarrow> t"
   3.112 +	"s -e..f          \<succ>v-n\<rightarrow> t"
   3.113 +	"s -{C}e1..m(e2)  \<succ>v-n\<rightarrow> t"
   3.114  
   3.115 -lemma exec_mono [rule_format]: "s -c-n\<rightarrow> t \<Longrightarrow> \<forall>m. n \<le> m \<longrightarrow> s -c-m\<rightarrow> t"
   3.116 -apply (erule exec.induct)
   3.117 -prefer 12 (* Impl *)
   3.118 +lemma exec_eval_mono [rule_format]: 
   3.119 +  "(s -c  -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c  -m\<rightarrow> t)) \<and>
   3.120 +   (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))"
   3.121 +apply (rule exec_eval.induct)
   3.122 +prefer 14 (* Impl *)
   3.123  apply clarify
   3.124  apply (rename_tac n)
   3.125  apply (case_tac n)
   3.126 -apply (blast intro:exec.intros)+
   3.127 +apply  (blast intro:exec_eval.intros)+
   3.128  done
   3.129 +lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
   3.130 +lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]
   3.131 +
   3.132 +lemma exec_exec_max: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
   3.133 +                       s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
   3.134 +by (fast intro: exec_mono le_maxI1 le_maxI2)
   3.135  
   3.136 -lemma exec_max2: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-        n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
   3.137 -                   s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
   3.138 -by (fast intro: exec_mono le_maxI1 le_maxI2)
   3.139 +lemma eval_exec_max: "\<lbrakk>s1 -c-    n1   \<rightarrow> t1 ; s2 -e\<succ>v-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
   3.140 +                       s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
   3.141 +by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
   3.142 +
   3.143 +lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1-    n1   \<rightarrow> t1 ; s2 -e2\<succ>v2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
   3.144 +                       s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
   3.145 +by (fast intro: eval_mono le_maxI1 le_maxI2)
   3.146 +
   3.147 +lemma eval_eval_exec_max: 
   3.148 + "\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 
   3.149 +   s1 -e1\<succ>v1-max (max n1 n2) n3\<rightarrow> t1 \<and> 
   3.150 +   s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
   3.151 +   s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
   3.152 +apply (drule (1) eval_eval_max, erule thin_rl)
   3.153 +by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
   3.154  
   3.155  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)"
   3.156  apply (rule ext)
   3.157 -apply (fast elim: exec_elim_cases intro: exec.Impl)
   3.158 +apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
   3.159  done
   3.160  
   3.161  end
   3.162 \ No newline at end of file
     4.1 --- a/src/HOL/NanoJava/Term.thy	Tue Aug 07 22:42:22 2001 +0200
     4.2 +++ b/src/HOL/NanoJava/Term.thy	Wed Aug 08 12:36:48 2001 +0200
     4.3 @@ -23,20 +23,22 @@
     4.4  
     4.5  datatype stmt
     4.6    = Skip                   (* empty statement *)
     4.7 -  | Comp       stmt stmt   ("_;; _"             [91,90]    90)
     4.8 -  | Cond vname stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
     4.9 +  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
    4.10 +  | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
    4.11    | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
    4.12 -
    4.13 -  | NewC vname cname       ("_:=new _"  [99,   99] 95) (* object creation  *)
    4.14 -  | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
    4.15 -  | FAcc vname vname vnam  ("_:=_.._"   [99,99,99] 95) (* field access     *)
    4.16 -  | FAss vname vnam  vname ("_.._:=_"   [99,99,99] 95) (* field assigment  *)
    4.17 -  | Call vname cname vname mname vname                 (* method call      *)
    4.18 -                           ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
    4.19 +  | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
    4.20 +  | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
    4.21    | Meth cname mname       (* virtual method *)
    4.22    | Impl cname mname       (* method implementation *)
    4.23 +and expr
    4.24 +  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
    4.25 +  | Cast cname expr                              (* type cast        *)
    4.26 +  | LAcc vname                                   (* local access     *)
    4.27 +  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
    4.28 +  | Call cname expr mname expr                   (* method call      *)
    4.29 +                     ("{_}_.._'(_')" [99,95,99,95] 95)
    4.30  
    4.31 -(*###TO Product_Type_lemmas.ML*)
    4.32 +
    4.33  lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
    4.34  apply (rule_tac x = "(a,b)" in image_eqI)
    4.35  apply  auto