src/HOL/NanoJava/AxSem.thy

   Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True 
                                  | Addr a => obj_class s a <=C C) --> Q v s} ==>
          A |-e {P} Cast C e {Q}"
 
   Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
-    \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> 
+    \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 
                     s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s))}
-                  Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
+                  Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
              A |-e {P} {C}e1..m(e2) {S}"
 
   Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> 
                         P s \<and> s' = init_locs D m s}
                   Impl (D,m) {Q} ==>
              A |- {P} Meth (C,m) {Q}"
 
-  --{* @{text "\<Union>z"} instead of @{text "\<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>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"
+  --{* @{text "\<Union>Z"} instead of @{text "\<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>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 *}
 
   Asm:  "   a \<in> A ==> A ||- {a}"
 
   ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
 
   ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
 
-  Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
-             \<forall>s t. (\<forall>z. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
+  --{* Z restricted to type state due to limitations of the inductive package *}
+  Conseq:"[| \<forall>Z::state. 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 }"
 
-  --{* z restricted to type state due to limitations of the inductive package *}
- eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
-             \<forall>s v t. (\<forall>z. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
-            A |-e {P} c {Q }"
-
+  --{* Z restricted to type state due to limitations of the inductive package *}
+ eConseq:"[| \<forall>Z::state. A |-e {P' Z} e {Q' Z};
+             \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
+            A |-e {P} e {Q }"
+
+
+subsection "Fully polymorphic variants"
+
+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 }"
+
+ eConseq:"[| \<forall>Z. A |-e {P' Z} e {Q' Z};
+             \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
+                 A |-e {P} e {Q }"
+
+ Impl: "\<forall>Z. 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"
 
 subsection "Derived Rules"
 
 lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
 apply (rule hoare_ehoare.Conseq)

 apply (drule hoare_ehoare.ConjE)
 apply  fast
 apply assumption
 done
 
-lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
+lemma Thin_lemma: 
+  "(A' |\<turnstile>  C         \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile>  C       )) \<and> 
+   (A'  \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A  \<turnstile>\<^sub>e {P} e {Q}))"
+apply (rule hoare_ehoare.induct)
+apply (tactic "ALLGOALS(EVERY'[Clarify_tac, REPEAT o smp_tac 1])")
+apply (blast intro: hoare_ehoare.Skip)
+apply (blast intro: hoare_ehoare.Comp)
+apply (blast intro: hoare_ehoare.Cond)
+apply (blast intro: hoare_ehoare.Loop)
+apply (blast intro: hoare_ehoare.LAcc)
+apply (blast intro: hoare_ehoare.LAss)
+apply (blast intro: hoare_ehoare.FAcc)
+apply (blast intro: hoare_ehoare.FAss)
+apply (blast intro: hoare_ehoare.NewC)
+apply (blast intro: hoare_ehoare.Cast)
+apply (erule hoare_ehoare.Call)
+apply   (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption)
+apply  blast
+apply (blast intro!: hoare_ehoare.Meth)
+apply (blast intro!: hoare_ehoare.Impl)
+apply (blast intro!: hoare_ehoare.Asm)
+apply (blast intro: hoare_ehoare.ConjI)
+apply (blast intro: hoare_ehoare.ConjE)
+apply (rule hoare_ehoare.Conseq)
+apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
+apply (rule hoare_ehoare.eConseq)
+apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
+done
+
+lemma cThin: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
+by (erule (1) conjunct1 [OF Thin_lemma, rule_format])
+
+lemma eThin: "\<lbrakk>A' \<turnstile>\<^sub>e {P} e {Q}; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
+by (erule (1) conjunct2 [OF Thin_lemma, rule_format])
+
+
+lemma Union: "A |\<turnstile> (\<Union>Z. C Z) = (\<forall>Z. A |\<turnstile> C Z)"
 by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
 
-lemma Impl1: 
-   "\<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; 
+lemma Impl1': 
+   "\<lbrakk>\<forall>Z. 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)
+                A   \<turnstile>  {P Z Cm} Impl Cm {Q Z Cm}"
+apply (drule Impl)
 apply (erule Weaken)
 apply (auto del: image_eqI intro: rev_image_eqI)
 done
 
+lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard]
+
 end