--- a/src/HOL/NanoJava/AxSem.thy Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Fri Sep 21 18:23:15 2001 +0200
@@ -78,9 +78,9 @@
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>
@@ -88,11 +88,11 @@
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 *}
@@ -102,15 +102,31 @@
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"
@@ -146,17 +162,55 @@
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