173 apply (induct_tac "n") |
173 apply (induct_tac "n") |
174 apply (drule apply_type [OF _ nat_1I]) |
174 apply (drule apply_type [OF _ nat_1I]) |
175 apply (drule bspec [OF _ nat_0I]) |
175 apply (drule bspec [OF _ nat_0I]) |
176 apply (simp add: XX_def, safe) |
176 apply (simp add: XX_def, safe) |
177 apply (rule rev_bexI, assumption) |
177 apply (rule rev_bexI, assumption) |
178 apply (subgoal_tac "0 \<in> x", force) |
178 apply (subgoal_tac "0 \<in> y", force) |
179 apply (force simp add: RR_def |
179 apply (force simp add: RR_def |
180 intro: ltD elim!: nat_0_le [THEN leE]) |
180 intro: ltD elim!: nat_0_le [THEN leE]) |
181 (** LEVEL 7, other subgoal **) |
181 (** LEVEL 7, other subgoal **) |
182 apply (drule bspec [OF _ nat_succI], assumption) |
182 apply (drule bspec [OF _ nat_succI], assumption) |
183 apply (subgoal_tac "f ` succ (succ (x)) \<in> succ (k) ->X") |
183 apply (subgoal_tac "f ` succ (succ (x)) \<in> succ (k) ->X") |
184 apply (drule apply_type [OF _ nat_succI [THEN nat_succI]], assumption) |
184 apply (drule apply_type [OF _ nat_succI [THEN nat_succI]], assumption) |
185 apply (simp (no_asm_use) add: XX_def RR_def) |
185 apply (simp (no_asm_use) add: XX_def RR_def) |
186 apply safe |
186 apply safe |
187 apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans], |
187 apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans], |
188 assumption) |
188 assumption) |
189 apply (frule_tac a="xa" in domain_of_fun [symmetric, THEN trans], |
189 apply (frule_tac a=y in domain_of_fun [symmetric, THEN trans], |
190 assumption) |
190 assumption) |
191 apply (fast elim!: nat_into_Ord [THEN succ_in_succ] |
191 apply (fast elim!: nat_into_Ord [THEN succ_in_succ] |
192 dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]]) |
192 dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]]) |
193 apply (drule domain_of_fun) |
193 apply (drule domain_of_fun) |
194 apply (simp add: XX_def RR_def, clarify) |
194 apply (simp add: XX_def RR_def, clarify) |
206 apply (rule restrict_eq_imp_val_eq) |
206 apply (rule restrict_eq_imp_val_eq) |
207 apply (drule bspec [OF _ nat_succI], assumption) |
207 apply (drule bspec [OF _ nat_succI], assumption) |
208 apply (simp add: RR_def) |
208 apply (simp add: RR_def) |
209 apply (drule lemma2, assumption+) |
209 apply (drule lemma2, assumption+) |
210 apply (fast dest!: domain_of_fun) |
210 apply (fast dest!: domain_of_fun) |
211 apply (drule_tac x = "xa" in bspec, assumption) |
211 apply (drule_tac x = xa in bspec, assumption) |
212 apply (erule sym [THEN trans, symmetric]) |
212 apply (erule sym [THEN trans, symmetric]) |
213 apply (rule restrict_eq_imp_val_eq [symmetric]) |
213 apply (rule restrict_eq_imp_val_eq [symmetric]) |
214 apply (drule bspec [OF _ nat_succI], assumption) |
214 apply (drule bspec [OF _ nat_succI], assumption) |
215 apply (simp add: RR_def) |
215 apply (simp add: RR_def) |
216 apply (drule lemma2, assumption+) |
216 apply (drule lemma2, assumption+) |
390 f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)|] |
390 f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)|] |
391 ==> allRR" |
391 ==> allRR" |
392 apply (unfold RR_def allRR_def) |
392 apply (unfold RR_def allRR_def) |
393 apply (rule oallI, drule ltD) |
393 apply (rule oallI, drule ltD) |
394 apply (erule nat_induct) |
394 apply (erule nat_induct) |
395 apply (drule_tac x="0" in ospec, blast intro: Limit_has_0) |
395 apply (drule_tac x=0 in ospec, blast intro: Limit_has_0) |
396 apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) |
396 apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) |
397 (*induction step*) (** LEVEL 5 **) |
397 (*induction step*) (** LEVEL 5 **) |
398 (*prevent simplification of ~\<exists> to \<forall>~ *) |
398 (*prevent simplification of ~\<exists> to \<forall>~ *) |
399 apply (simp only: separation split) |
399 apply (simp only: separation split) |
400 apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI) |
400 apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI) |
407 apply (drule apply_domain_type, assumption+) |
407 apply (drule apply_domain_type, assumption+) |
408 apply (erule domainE)+ |
408 apply (erule domainE)+ |
409 apply (frule f_n_type) |
409 apply (frule f_n_type) |
410 apply (simp add: XX_def, assumption+) |
410 apply (simp add: XX_def, assumption+) |
411 apply (rule rev_bexI, erule nat_succI) |
411 apply (rule rev_bexI, erule nat_succI) |
412 apply (rule_tac x = "cons (<succ (xa), ya>, f`xa) " in bexI) |
412 apply (rename_tac m i j y z) |
|
413 apply (rule_tac x = "cons(<succ(m), z>, f`m)" in bexI) |
413 prefer 2 apply (blast intro: cons_fun_type2) |
414 prefer 2 apply (blast intro: cons_fun_type2) |
414 apply (rule conjI) |
415 apply (rule conjI) |
415 prefer 2 apply (fast del: ballI subsetI |
416 prefer 2 apply (fast del: ballI subsetI |
416 elim: trans [OF _ subst_context, THEN domain_cons_eq_succ] |
417 elim: trans [OF _ subst_context, THEN domain_cons_eq_succ] |
417 subst_context |
418 subst_context |
495 apply (case_tac "A \<prec> Hartog (A)") |
496 apply (case_tac "A \<prec> Hartog (A)") |
496 apply (fast dest!: lesspoll_imp_ex_lt_eqpoll |
497 apply (fast dest!: lesspoll_imp_ex_lt_eqpoll |
497 intro!: Ord_Hartog leI [THEN le_imp_subset]) |
498 intro!: Ord_Hartog leI [THEN le_imp_subset]) |
498 apply (erule allE impE)+ |
499 apply (erule allE impE)+ |
499 apply (rule Card_Hartog) |
500 apply (rule Card_Hartog) |
500 apply (erule_tac x = "A" in allE) |
501 apply (erule_tac x = A in allE) |
501 apply (erule_tac x = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) & z2 \<notin> z1}" |
502 apply (erule_tac x = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) & z2 \<notin> z1}" |
502 in allE) |
503 in allE) |
503 apply simp |
504 apply simp |
504 apply (erule impE, fast elim: lesspoll_lemma [THEN not_emptyE]) |
505 apply (erule impE, fast elim: lesspoll_lemma [THEN not_emptyE]) |
505 apply (erule bexE) |
506 apply (erule bexE) |