cosmetics
authoroheimb
Thu Aug 30 17:49:46 2001 +0200 (2001-08-30)
changeset 11508168dbdaedb71
parent 11507 4b32a46ffd29
child 11509 d54301357129
cosmetics
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/OpSem.thy
     1.1 --- a/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 15:47:30 2001 +0200
     1.2 +++ b/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 17:49:46 2001 +0200
     1.3 @@ -88,9 +88,9 @@
     1.4  
     1.5    (*\<Union>z instead of \<forall>z in the conclusion and
     1.6        z restricted to type state due to limitations of the inductive package *)
     1.7 -  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||- 
     1.8 -                            (\<lambda>M. (P z M, body M, Q z M))`Ms ==>
     1.9 -                      A ||- (\<lambda>M. (P z M, Impl M, Q z M))`Ms"
    1.10 +  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- 
    1.11 +                            (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
    1.12 +                      A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"
    1.13  
    1.14  (* structural rules *)
    1.15  
    1.16 @@ -148,10 +148,10 @@
    1.17  by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
    1.18  
    1.19  lemma Impl1: 
    1.20 -   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) |\<turnstile> 
    1.21 -                        (\<lambda>M. (P z M, body M, Q z M))`Ms; 
    1.22 -    M \<in> Ms\<rbrakk> \<Longrightarrow> 
    1.23 -                A         \<turnstile>  {P z M} Impl M {Q z M}"
    1.24 +   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) |\<turnstile> 
    1.25 +                        (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms; 
    1.26 +    Cm \<in> Ms\<rbrakk> \<Longrightarrow> 
    1.27 +                A         \<turnstile>  {P z Cm} Impl Cm {Q z Cm}"
    1.28  apply (drule hoare_ehoare.Impl)
    1.29  apply (erule Weaken)
    1.30  apply (auto del: image_eqI intro: rev_image_eqI)
     2.1 --- a/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 15:47:30 2001 +0200
     2.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 17:49:46 2001 +0200
     2.3 @@ -89,7 +89,7 @@
     2.4  
     2.5  lemma Impl_sound_lemma: 
     2.6  "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); 
     2.7 -M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)"
     2.8 +Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)"
     2.9  by blast
    2.10  
    2.11  lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
     3.1 --- a/src/HOL/NanoJava/OpSem.thy	Thu Aug 30 15:47:30 2001 +0200
     3.2 +++ b/src/HOL/NanoJava/OpSem.thy	Thu Aug 30 17:49:46 2001 +0200
     3.3 @@ -12,11 +12,11 @@
     3.4   exec :: "(state \<times> stmt       \<times> nat \<times> state) set"
     3.5   eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
     3.6  syntax (xsymbols)
     3.7 - exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   99,98] 89)
     3.8 - eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,99,98] 89)
     3.9 + exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
    3.10 + eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
    3.11  syntax
    3.12 - exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   99,98]89)
    3.13 - eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,99,98]89)
    3.14 + exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   65,98]89)
    3.15 + eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89)
    3.16  translations
    3.17   "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
    3.18   "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
    3.19 @@ -61,8 +61,8 @@
    3.20              init_locs D m s -Impl (D,m)-n-> s' |] ==>
    3.21              s -Meth (C,m)-n-> s'"
    3.22  
    3.23 -  Impl: "   s -body M-n-> s' ==>
    3.24 -            s -Impl M-Suc n-> s'"
    3.25 +  Impl: "   s -body Cm-    n-> s' ==>
    3.26 +            s -Impl Cm-Suc n-> s'"
    3.27  
    3.28  
    3.29  inductive_cases exec_elim_cases':
    3.30 @@ -72,8 +72,8 @@
    3.31  				  "s -While(x) c      -n\<rightarrow> t"
    3.32  				  "s -x:==e           -n\<rightarrow> t"
    3.33  				  "s -e1..f:==e2      -n\<rightarrow> t"
    3.34 -inductive_cases Meth_elim_cases:  "s -Meth Cm-n\<rightarrow> t"
    3.35 -inductive_cases Impl_elim_cases:  "s -Impl Cm-n\<rightarrow> t"
    3.36 +inductive_cases Meth_elim_cases:  "s -Meth Cm         -n\<rightarrow> t"
    3.37 +inductive_cases Impl_elim_cases:  "s -Impl Cm         -n\<rightarrow> t"
    3.38  lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
    3.39  inductive_cases eval_elim_cases:
    3.40  				  "s -new C         \<succ>v-n\<rightarrow> t"
    3.41 @@ -90,7 +90,7 @@
    3.42  apply clarify
    3.43  apply (rename_tac n)
    3.44  apply (case_tac n)
    3.45 -apply  (blast intro:exec_eval.intros)+
    3.46 +apply (blast intro:exec_eval.intros)+
    3.47  done
    3.48  lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
    3.49  lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]