98 |
98 |
99 lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)" |
99 lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)" |
100 by (auto intro: hoare.ConjI hoare.ConjE) |
100 by (auto intro: hoare.ConjI hoare.ConjE) |
101 |
101 |
102 lemma Impl': |
102 lemma Impl': |
103 "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- |
103 "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- |
104 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==> |
104 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==> |
105 A ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms" |
105 A ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms" |
106 apply (drule Union[THEN iffD2]) |
106 apply (drule Union[THEN iffD2]) |
107 apply (drule hoare.Impl) |
107 apply (drule hoare.Impl) |
108 apply (drule Union[THEN iffD1]) |
108 apply (drule Union[THEN iffD1]) |
109 apply (erule spec) |
109 apply (erule spec) |
110 done |
110 done |
111 |
111 |
112 lemma Impl1: |
112 lemma Impl1: |
113 "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- |
113 "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- |
114 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; |
114 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; |
115 (C,m)\<in> ms\<rbrakk> \<Longrightarrow> |
115 (C,m)\<in> ms\<rbrakk> \<Longrightarrow> |
116 A \<turnstile> {P z C m} Impl C m {Q (z::state) C m}" |
116 A |- {P z C m} Impl C m {Q (z::state) C m}" |
117 apply (drule Impl') |
117 apply (drule Impl') |
118 apply (erule Weaken) |
118 apply (erule Weaken) |
119 apply (auto del: image_eqI intro: rev_image_eqI) |
119 apply (auto del: image_eqI intro: rev_image_eqI) |
120 done |
120 done |
121 |
121 |