equal
deleted
inserted
replaced
151 |
151 |
152 subsection {* Fixed point induction *} |
152 subsection {* Fixed point induction *} |
153 |
153 |
154 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" |
154 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" |
155 apply (subst fix_def2) |
155 apply (subst fix_def2) |
156 apply (erule admD [rule_format]) |
156 apply (erule admD) |
157 apply (rule chain_iterate) |
157 apply (rule chain_iterate) |
158 apply (induct_tac "i", simp_all) |
158 apply (induct_tac "i", simp_all) |
159 done |
159 done |
160 |
160 |
161 lemma def_fix_ind: |
161 lemma def_fix_ind: |
231 lemma adm_impl_admw: "adm P \<Longrightarrow> admw P" |
231 lemma adm_impl_admw: "adm P \<Longrightarrow> admw P" |
232 apply (unfold admw_def) |
232 apply (unfold admw_def) |
233 apply (intro strip) |
233 apply (intro strip) |
234 apply (erule admD) |
234 apply (erule admD) |
235 apply (rule chain_iterate) |
235 apply (rule chain_iterate) |
236 apply assumption |
236 apply (erule spec) |
237 done |
237 done |
238 |
238 |
239 text {* computational induction for weak admissible formulae *} |
239 text {* computational induction for weak admissible formulae *} |
240 |
240 |
241 lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" |
241 lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)" |