# HG changeset patch
# User oheimb
# Date 999186586 -7200
# Node ID 168dbdaedb71ecd958ae62c6a2d518514cb29787
# Parent  4b32a46ffd2923fc7d76a4d600a74a750d165488
cosmetics

diff -r 4b32a46ffd29 -r 168dbdaedb71 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 15:47:30 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 17:49:46 2001 +0200
@@ -88,9 +88,9 @@
 
   (*\<Union>z instead of \<forall>z in the conclusion and
       z restricted to type state due to limitations of the inductive package *)
-  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||- 
-                            (\<lambda>M. (P z M, body M, Q z M))`Ms ==>
-                      A ||- (\<lambda>M. (P z M, Impl M, Q z M))`Ms"
+  Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- 
+                            (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
+                      A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"
 
 (* structural rules *)
 
@@ -148,10 +148,10 @@
 by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
 
 lemma Impl1: 
-   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) |\<turnstile> 
-                        (\<lambda>M. (P z M, body M, Q z M))`Ms; 
-    M \<in> Ms\<rbrakk> \<Longrightarrow> 
-                A         \<turnstile>  {P z M} Impl M {Q z M}"
+   "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) |\<turnstile> 
+                        (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms; 
+    Cm \<in> Ms\<rbrakk> \<Longrightarrow> 
+                A         \<turnstile>  {P z Cm} Impl Cm {Q z Cm}"
 apply (drule hoare_ehoare.Impl)
 apply (erule Weaken)
 apply (auto del: image_eqI intro: rev_image_eqI)
diff -r 4b32a46ffd29 -r 168dbdaedb71 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 15:47:30 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 17:49:46 2001 +0200
@@ -89,7 +89,7 @@
 
 lemma Impl_sound_lemma: 
 "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); 
-M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)"
+Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)"
 by blast
 
 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
diff -r 4b32a46ffd29 -r 168dbdaedb71 src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Thu Aug 30 15:47:30 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Thu Aug 30 17:49:46 2001 +0200
@@ -12,11 +12,11 @@
  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)
- eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,99,98] 89)
+ exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
+ eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
 syntax
- exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   99,98]89)
- eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,99,98]89)
+ exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   65,98]89)
+ eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89)
 translations
  "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
  "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
@@ -61,8 +61,8 @@
             init_locs D m s -Impl (D,m)-n-> s' |] ==>
             s -Meth (C,m)-n-> s'"
 
-  Impl: "   s -body M-n-> s' ==>
-            s -Impl M-Suc n-> s'"
+  Impl: "   s -body Cm-    n-> s' ==>
+            s -Impl Cm-Suc n-> s'"
 
 
 inductive_cases exec_elim_cases':
@@ -72,8 +72,8 @@
 				  "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 Cm-n\<rightarrow> t"
-inductive_cases Impl_elim_cases:  "s -Impl Cm-n\<rightarrow> t"
+inductive_cases Meth_elim_cases:  "s -Meth Cm         -n\<rightarrow> t"
+inductive_cases Impl_elim_cases:  "s -Impl Cm         -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"
@@ -90,7 +90,7 @@
 apply clarify
 apply (rename_tac n)
 apply (case_tac n)
-apply  (blast intro:exec_eval.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]