corrected initialization of locals, streamlined Impl
authoroheimb
Thu Aug 09 20:48:57 2001 +0200 (2001-08-09)
changeset 114970e66e0114d9a
parent 11496 fa8d12b789e1
child 11498 681aa3dfab4b
corrected initialization of locals, streamlined Impl
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/OpSem.thy
src/HOL/NanoJava/State.thy
src/HOL/NanoJava/Term.thy
     1.1 --- a/src/HOL/NanoJava/AxSem.thy	Thu Aug 09 19:33:22 2001 +0200
     1.2 +++ b/src/HOL/NanoJava/AxSem.thy	Thu Aug 09 20:48:57 2001 +0200
     1.3 @@ -77,19 +77,20 @@
     1.4  
     1.5    Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
     1.6      \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> 
     1.7 -                    s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s))}
     1.8 +                    s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s))}
     1.9                    Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
    1.10               A |-e {P} {C}e1..m(e2) {S}"
    1.11  
    1.12 -  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.13 -                  Impl D m {Q} ==>
    1.14 +  Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> 
    1.15 +                        P s \<and> s' = init_locs D m s}
    1.16 +                  Impl (D,m) {Q} ==>
    1.17               A |- {P} Meth C m {Q}"
    1.18  
    1.19    (*\<Union>z instead of \<forall>z in the conclusion and
    1.20        z restricted to type state due to limitations of the inductive package *)
    1.21 -  Impl: "A\<union>   (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||- 
    1.22 -               (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
    1.23 -         A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
    1.24 +  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||- 
    1.25 +                            (\<lambda>M. (P z M, body M, Q z M))`Ms ==>
    1.26 +                      A ||- (\<lambda>M. (P z M, Impl M, Q z M))`Ms"
    1.27  
    1.28  (* structural rules *)
    1.29  
    1.30 @@ -99,14 +100,13 @@
    1.31  
    1.32    ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
    1.33  
    1.34 -  (* z restricted to type state due to limitations of the inductive package *)
    1.35    Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
    1.36 -             \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
    1.37 +             \<forall>s t. (\<forall>z. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
    1.38              A |- {P} c {Q }"
    1.39  
    1.40    (* z restricted to type state due to limitations of the inductive package *)
    1.41   eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
    1.42 -             \<forall>s v t. (\<forall>z::state. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
    1.43 +             \<forall>s v t. (\<forall>z. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
    1.44              A |-e {P} c {Q }"
    1.45  
    1.46  
    1.47 @@ -147,22 +147,12 @@
    1.48  lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
    1.49  by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
    1.50  
    1.51 -lemma Impl': 
    1.52 -  "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
    1.53 -                (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
    1.54 -       A    ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
    1.55 -apply (drule Union[THEN iffD2])
    1.56 +lemma Impl1: 
    1.57 +   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) |\<turnstile> 
    1.58 +                        (\<lambda>M. (P z M, body M, Q z M))`Ms; 
    1.59 +    M \<in> Ms\<rbrakk> \<Longrightarrow> 
    1.60 +                A         \<turnstile>  {P z M} Impl M {Q z M}"
    1.61  apply (drule hoare_ehoare.Impl)
    1.62 -apply (drule Union[THEN iffD1])
    1.63 -apply (erule spec)
    1.64 -done
    1.65 -
    1.66 -lemma Impl1: 
    1.67 -   "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
    1.68 -                 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; 
    1.69 -    (C,m)\<in> ms\<rbrakk> \<Longrightarrow> 
    1.70 -         A             |- {P z C m} Impl C m {Q (z::state) C m}"
    1.71 -apply (drule Impl')
    1.72  apply (erule Weaken)
    1.73  apply (auto del: image_eqI intro: rev_image_eqI)
    1.74  done
     2.1 --- a/src/HOL/NanoJava/Equivalence.thy	Thu Aug 09 19:33:22 2001 +0200
     2.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Thu Aug 09 20:48:57 2001 +0200
     2.3 @@ -68,10 +68,10 @@
     2.4  
     2.5  declare exec_elim_cases [elim!] eval_elim_cases [elim!]
     2.6  
     2.7 -lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)"
     2.8 +lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl M,Q)"
     2.9  by (clarsimp simp add: nvalid_def2)
    2.10  
    2.11 -lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)"
    2.12 +lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body M,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl M,Q)"
    2.13  by (clarsimp simp add: nvalid_def2)
    2.14  
    2.15  lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
    2.16 @@ -88,8 +88,8 @@
    2.17  done
    2.18  
    2.19  lemma Impl_sound_lemma: 
    2.20 -"\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
    2.21 -          (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
    2.22 +"\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); 
    2.23 +M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)"
    2.24  by blast
    2.25  
    2.26  lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
    2.27 @@ -124,7 +124,7 @@
    2.28  apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
    2.29  apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
    2.30  apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
    2.31 -apply (clarsimp del: Impl_elim_cases) (* Meth *)
    2.32 +apply (force del: Impl_elim_cases) (* Meth *)
    2.33  defer
    2.34  prefer 4 apply blast (*  Conseq *)
    2.35  prefer 4 apply blast (* eConseq *)
    2.36 @@ -134,12 +134,16 @@
    2.37  apply blast
    2.38  (* Impl *)
    2.39  apply (rule allI)
    2.40 +apply (rule_tac x=z in spec)
    2.41  apply (induct_tac "n")
    2.42  apply  (clarify intro!: Impl_nvalid_0)
    2.43  apply (clarify  intro!: Impl_nvalid_Suc)
    2.44  apply (drule nvalids_SucD)
    2.45 +apply (simp only: all_simps)
    2.46  apply (erule (1) impE)
    2.47 -apply (drule (4) Impl_sound_lemma)
    2.48 +apply (drule (2) Impl_sound_lemma)
    2.49 +apply  blast
    2.50 +apply assumption
    2.51  done
    2.52  
    2.53  theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
    2.54 @@ -204,7 +208,7 @@
    2.55  apply (blast del: exec_elim_cases)
    2.56  done
    2.57  
    2.58 -lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> 
    2.59 +lemma MGF_lemma: "\<forall>M z. A |\<turnstile> {MGT (Impl M) z} \<Longrightarrow> 
    2.60   (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)"
    2.61  apply (simp add: MGT_def MGTe_def)
    2.62  apply (rule stmt_expr.induct)
    2.63 @@ -250,7 +254,7 @@
    2.64  apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
    2.65  apply blast
    2.66  
    2.67 -apply blast
    2.68 +apply (simp add: split_paired_all)
    2.69  
    2.70  apply (rule eConseq1 [OF hoare_ehoare.NewC])
    2.71  apply blast
    2.72 @@ -281,7 +285,7 @@
    2.73  apply (fast del: Impl_elim_cases)
    2.74  done
    2.75  
    2.76 -lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
    2.77 +lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) z}"
    2.78  apply (unfold MGT_def)
    2.79  apply (rule Impl1)
    2.80  apply  (rule_tac [2] UNIV_I)
     3.1 --- a/src/HOL/NanoJava/OpSem.thy	Thu Aug 09 19:33:22 2001 +0200
     3.2 +++ b/src/HOL/NanoJava/OpSem.thy	Thu Aug 09 20:48:57 2001 +0200
     3.3 @@ -54,15 +54,15 @@
     3.4              s -Cast C e>v-n-> s'"
     3.5  
     3.6    Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
     3.7 -            lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s2)) -Meth C m-n-> s3
     3.8 +            lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s2)) -Meth C m-n-> s3
     3.9       |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
    3.10  
    3.11 -  Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
    3.12 -            s -Impl (obj_class s a) m-n-> s' |] ==>
    3.13 +  Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
    3.14 +            init_locs D m s -Impl (D,m)-n-> s' |] ==>
    3.15              s -Meth C m-n-> s'"
    3.16  
    3.17 -  Impl: "   s -body C m-n-> s' ==>
    3.18 -            s -Impl C m-Suc n-> s'"
    3.19 +  Impl: "   s -body M-n-> s' ==>
    3.20 +            s -Impl M-Suc n-> s'"
    3.21  
    3.22  
    3.23  inductive_cases exec_elim_cases':
    3.24 @@ -73,7 +73,7 @@
    3.25  				  "s -x:==e           -n\<rightarrow> t"
    3.26  				  "s -e1..f:==e2      -n\<rightarrow> t"
    3.27  inductive_cases Meth_elim_cases:  "s -Meth C m-n\<rightarrow> t"
    3.28 -inductive_cases Impl_elim_cases:  "s -Impl C m-n\<rightarrow> t"
    3.29 +inductive_cases Impl_elim_cases:  "s -Impl   M-n\<rightarrow> t"
    3.30  lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
    3.31  inductive_cases eval_elim_cases:
    3.32  				  "s -new C         \<succ>v-n\<rightarrow> t"
    3.33 @@ -115,7 +115,7 @@
    3.34  apply (drule (1) eval_eval_max, erule thin_rl)
    3.35  by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
    3.36  
    3.37 -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.38 +lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body M-n\<rightarrow> t)"
    3.39  apply (rule ext)
    3.40  apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
    3.41  done
     4.1 --- a/src/HOL/NanoJava/State.thy	Thu Aug 09 19:33:22 2001 +0200
     4.2 +++ b/src/HOL/NanoJava/State.thy	Thu Aug 09 20:48:57 2001 +0200
     4.3 @@ -10,8 +10,8 @@
     4.4  
     4.5  constdefs
     4.6  
     4.7 -  body :: "cname => mname => stmt"
     4.8 - "body C m \<equiv> bdy (the (method C m))"
     4.9 +  body :: "imname => stmt"
    4.10 + "body \<equiv> \<lambda>(C,m). bdy (the (method C m))"
    4.11  
    4.12  text {* locations, i.e.\ abstract references to objects *}
    4.13  typedecl loc 
    4.14 @@ -53,8 +53,11 @@
    4.15  
    4.16  constdefs
    4.17  
    4.18 +  reset_locs     :: "state => state"
    4.19 + "reset_locs s \<equiv> s (| locals := empty |)"
    4.20 +
    4.21    init_locs     :: "cname => mname => state => state"
    4.22 - "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m))))|)"
    4.23 + "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)"
    4.24  
    4.25  text {* The first parameter of @{term set_locs} is of type @{typ state} 
    4.26          rather than @{typ locals} in order to keep @{typ locals} private.*}
     5.1 --- a/src/HOL/NanoJava/Term.thy	Thu Aug 09 19:33:22 2001 +0200
     5.2 +++ b/src/HOL/NanoJava/Term.thy	Thu Aug 09 20:48:57 2001 +0200
     5.3 @@ -14,6 +14,7 @@
     5.4  arities  cname :: "term"
     5.5           vnam  :: "term"
     5.6           mname :: "term"
     5.7 +types   imname = "cname \<times> mname"
     5.8  
     5.9  datatype vname  (* variable for special names *)
    5.10    = This        (* This pointer *)
    5.11 @@ -29,7 +30,7 @@
    5.12    | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
    5.13    | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
    5.14    | Meth cname mname       (* virtual method *)
    5.15 -  | Impl cname mname       (* method implementation *)
    5.16 +  | Impl      imname       (* method implementation *)
    5.17  and expr
    5.18    = NewC cname       ("new _"        [   99] 95) (* object creation  *)
    5.19    | Cast cname expr                              (* type cast        *)