equal
deleted
inserted
replaced
87 apply clarsimp+ |
87 apply clarsimp+ |
88 done |
88 done |
89 |
89 |
90 lemma Impl_sound_lemma: |
90 lemma Impl_sound_lemma: |
91 "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); |
91 "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); |
92 M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)" |
92 Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)" |
93 by blast |
93 by blast |
94 |
94 |
95 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" |
95 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" |
96 by fast |
96 by fast |
97 |
97 |