# HG changeset patch
# User oheimb
# Date 1014656542 -3600
# Node ID 6003b4f916c0d5b70aef3c610107e582d9c7e72c
# Parent  b85c62c4e82679b5b5e61997f429c8f1b8aac9e3
Clarification wrt. use of polymorphic variants of Hoare logic rules

diff -r b85c62c4e826 -r 6003b4f916c0 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Mon Feb 25 11:27:07 2002 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Feb 25 18:02:22 2002 +0100
@@ -113,9 +113,10 @@
             A |-e {P} e {Q }"
 
 
-subsection "Fully polymorphic variants"
+subsection "Fully polymorphic variants, required for Example only"
 
 axioms
+
   Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z};
              \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
                  A |- {P} c {Q }"
@@ -202,11 +203,11 @@
 by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
 
 lemma Impl1': 
-   "\<lbrakk>\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
+   "\<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 Impl)
+apply (drule AxSem.Impl)
 apply (erule Weaken)
 apply (auto del: image_eqI intro: rev_image_eqI)
 done
diff -r b85c62c4e826 -r 6003b4f916c0 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Mon Feb 25 11:27:07 2002 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Feb 25 18:02:22 2002 +0100
@@ -285,7 +285,7 @@
 
 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) Z}"
 apply (unfold MGT_def)
-apply (rule_tac 'a = state in Impl1')
+apply (rule Impl1')
 apply  (rule_tac [2] UNIV_I)
 apply clarsimp
 apply (rule hoare_ehoare.ConjI)
diff -r b85c62c4e826 -r 6003b4f916c0 src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Mon Feb 25 11:27:07 2002 +0100
+++ b/src/HOL/NanoJava/Example.thy	Mon Feb 25 18:02:22 2002 +0100
@@ -139,12 +139,12 @@
 apply (rule hoare_ehoare.Meth) (* 1 *)
 apply clarsimp
 apply (rule_tac P'= "\<lambda>Z s. (s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z) \<and> D=Nat" and 
-                Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in Conseq)
+        Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in AxSem.Conseq)
 prefer 2
 apply  (clarsimp simp add: init_locs_def init_vars_def)
 apply rule
 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
-apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in Impl1)
+apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in AxSem.Impl1)
 apply (clarsimp simp add: body_def)  (* 4 *)
 apply (rename_tac n m)
 apply (rule_tac Q = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and> 
@@ -175,7 +175,7 @@
 apply  (rule hoare_ehoare.Meth) (* 17 *)
 apply  clarsimp
 apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
-apply  (rule Conseq)
+apply  (rule AxSem.Conseq)
 apply   rule
 apply   (rule hoare_ehoare.Asm) (* 20 *)
 apply   (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
@@ -189,7 +189,7 @@
 apply (rule hoare_ehoare.Meth) (* 24 *)
 apply clarsimp
 apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
-apply (rule Impl1)
+apply (rule AxSem.Impl1)
 apply (clarsimp simp add: body_def)
 apply (rule hoare_ehoare.Comp) (* 26 *)
 prefer 2