equal
deleted
inserted
replaced
456 apply (erule (1) Finite_cons_a [rule_format]) |
456 apply (erule (1) Finite_cons_a [rule_format]) |
457 apply fast |
457 apply fast |
458 apply simp |
458 apply simp |
459 done |
459 done |
460 |
460 |
|
461 lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y" |
|
462 apply (induct arbitrary: y set: Finite) |
|
463 apply (rule_tac x=y in seq.casedist, simp, simp, simp) |
|
464 apply (rule_tac x=y in seq.casedist, simp, simp) |
|
465 apply (simp add: seq.inverts) |
|
466 done |
|
467 |
|
468 lemma adm_Finite [simp]: "adm Finite" |
|
469 by (rule adm_upward, rule Finite_upward) |
|
470 |
461 |
471 |
462 subsection "induction" |
472 subsection "induction" |
463 |
473 |
464 |
474 |
465 (*-------------------------------- *) |
475 (*-------------------------------- *) |