equal
deleted
inserted
replaced
430 assumption+) |
430 assumption+) |
431 apply (rule L_new_r_subset) |
431 apply (rule L_new_r_subset) |
432 done |
432 done |
433 |
433 |
434 |
434 |
435 lemma (in Nat_Times_Nat) well_ord_L_new_r: |
435 lemma (in Nat_Times_Nat) well_ord_L_succ_r: |
436 "[|Ord(i); well_ord(Lset(i), r); r \<subseteq> Lset(i) * Lset(i)|] |
436 "[|Ord(i); well_ord(Lset(i), r); r \<subseteq> Lset(i) * Lset(i)|] |
437 ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))" |
437 ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))" |
438 apply (rule well_ordI [OF wf_imp_wf_on]) |
438 apply (rule well_ordI [OF wf_imp_wf_on]) |
439 prefer 2 apply (blast intro: linear_L_succ_r) |
439 prefer 2 apply (blast intro: linear_L_succ_r) |
440 apply (simp add: L_succ_r_def) |
440 apply (simp add: L_succ_r_def) |
494 done |
494 done |
495 |
495 |
496 lemma (in Nat_Times_Nat) L_r_type: |
496 lemma (in Nat_Times_Nat) L_r_type: |
497 "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |
497 "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |
498 apply (induct i rule: trans_induct3_rule) |
498 apply (induct i rule: trans_induct3_rule) |
499 apply (simp_all add: L_succ_r_type well_ord_L_new_r rlimit_def, blast) |
499 apply (simp_all add: L_succ_r_type well_ord_L_succ_r rlimit_def, blast) |
500 done |
500 done |
501 |
501 |
502 lemma (in Nat_Times_Nat) well_ord_L_r: |
502 lemma (in Nat_Times_Nat) well_ord_L_r: |
503 "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" |
503 "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" |
504 apply (induct i rule: trans_induct3_rule) |
504 apply (induct i rule: trans_induct3_rule) |
505 apply (simp_all add: well_ord0 L_r_type well_ord_L_new_r well_ord_rlimit ltD) |
505 apply (simp_all add: well_ord0 L_r_type well_ord_L_succ_r well_ord_rlimit ltD) |
506 done |
506 done |
507 |
507 |
508 lemma well_ord_L_r: |
508 lemma well_ord_L_r: |
509 "Ord(i) ==> \<exists>r. well_ord(Lset(i), r)" |
509 "Ord(i) ==> \<exists>r. well_ord(Lset(i), r)" |
510 apply (insert nat_times_nat_lepoll_nat) |
510 apply (insert nat_times_nat_lepoll_nat) |