# HG changeset patch # User paulson # Date 1331728744 0 # Node ID faf4a0b02b7137b8d5ce9b6ce3ec94a79478a9d6 # Parent c2ca2c3d23a689b3d2065068cae9c93dd071b277 rationalising the induction rule trans_induct3 diff -r c2ca2c3d23a6 -r faf4a0b02b71 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Wed Mar 14 00:34:56 2012 +0100 +++ b/src/ZF/Constructible/AC_in_L.thy Wed Mar 14 12:39:04 2012 +0000 @@ -424,14 +424,14 @@ lemma (in Nat_Times_Nat) L_r_type: "Ord(i) ==> L_r(fn,i) \ Lset(i) * Lset(i)" -apply (induct i rule: trans_induct3_rule) +apply (induct i rule: trans_induct3) apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def Transset_subset_DPow [OF Transset_Lset], blast) done lemma (in Nat_Times_Nat) well_ord_L_r: "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" -apply (induct i rule: trans_induct3_rule) +apply (induct i rule: trans_induct3) apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r well_ord_rlimit ltD) done diff -r c2ca2c3d23a6 -r faf4a0b02b71 src/ZF/Constructible/Normal.thy --- a/src/ZF/Constructible/Normal.thy Wed Mar 14 00:34:56 2012 +0100 +++ b/src/ZF/Constructible/Normal.thy Wed Mar 14 12:39:04 2012 +0000 @@ -243,7 +243,7 @@ by (simp add: Normal_def mono_Ord_def) lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\F(i)" -apply (induct i rule: trans_induct3_rule) +apply (induct i rule: trans_induct3) apply (simp add: subset_imp_le) apply (subgoal_tac "F(x) < F(succ(x))") apply (force intro: lt_trans1) @@ -383,7 +383,7 @@ lemma Ord_normalize [simp, intro]: "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))" -apply (induct a rule: trans_induct3_rule) +apply (induct a rule: trans_induct3) apply (simp_all add: ltD def_transrec2 [OF normalize_def]) done diff -r c2ca2c3d23a6 -r faf4a0b02b71 src/ZF/OrderType.thy --- a/src/ZF/OrderType.thy Wed Mar 14 00:34:56 2012 +0100 +++ b/src/ZF/OrderType.thy Wed Mar 14 12:39:04 2012 +0000 @@ -631,16 +631,19 @@ text{*Order/monotonicity properties of ordinal addition *} lemma oadd_le_self2: "Ord(i) ==> i \ j++i" -apply (erule_tac i = i in trans_induct3) -apply (simp (no_asm_simp) add: Ord_0_le) -apply (simp (no_asm_simp) add: oadd_succ succ_leI) -apply (simp (no_asm_simp) add: oadd_Limit) -apply (rule le_trans) -apply (rule_tac [2] le_implies_UN_le_UN) -apply (erule_tac [2] bspec) - prefer 2 apply assumption -apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord) -done +proof (induct i rule: trans_induct3) + case 0 thus ?case by (simp add: Ord_0_le) +next + case (succ i) thus ?case by (simp add: oadd_succ succ_leI) +next + case (limit l) + hence "l = (\x\l. x)" + by (simp add: Union_eq_UN [symmetric] Limit_Union_eq) + also have "... \ (\x\l. j++x)" + by (rule le_implies_UN_le_UN) (rule limit.hyps) + finally have "l \ (\x\l. j++x)" . + thus ?case using limit.hyps by (simp add: oadd_Limit) +qed lemma oadd_le_mono1: "k \ j ==> k++i \ j++i" apply (frule lt_Ord) @@ -925,15 +928,23 @@ lemma omult_le_self: "[| Ord(i); 0 i \ i**j" by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2) -lemma omult_le_mono1: "[| k \ j; Ord(i) |] ==> k**i \ j**i" -apply (frule lt_Ord) -apply (frule le_Ord2) -apply (erule trans_induct3) -apply (simp (no_asm_simp) add: le_refl Ord_0) -apply (simp (no_asm_simp) add: omult_succ oadd_le_mono) -apply (simp (no_asm_simp) add: omult_Limit) -apply (rule le_implies_UN_le_UN, blast) -done +lemma omult_le_mono1: + assumes kj: "k \ j" and i: "Ord(i)" shows "k**i \ j**i" +proof - + have o: "Ord(k)" "Ord(j)" by (rule lt_Ord [OF kj] le_Ord2 [OF kj])+ + show ?thesis using i + proof (induct i rule: trans_induct3) + case 0 thus ?case + by simp + next + case (succ i) thus ?case + by (simp add: o kj omult_succ oadd_le_mono) + next + case (limit l) + thus ?case + by (auto simp add: o kj omult_Limit le_implies_UN_le_UN) + qed +qed lemma omult_lt_mono2: "[| k i**k < i**j" apply (rule ltI) @@ -955,20 +966,30 @@ lemma omult_lt_mono: "[| i' \ i; j' i'**j' < i**j" by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE) -lemma omult_le_self2: "[| Ord(i); 0 i \ j**i" -apply (frule lt_Ord2) -apply (erule_tac i = i in trans_induct3) -apply (simp (no_asm_simp)) -apply (simp (no_asm_simp) add: omult_succ) -apply (erule lt_trans1) -apply (rule_tac b = "j**x" in oadd_0 [THEN subst], rule_tac [2] oadd_lt_mono2) -apply (blast intro: Ord_omult, assumption) -apply (simp (no_asm_simp) add: omult_Limit) -apply (rule le_trans) -apply (rule_tac [2] le_implies_UN_le_UN) -prefer 2 apply blast -apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord) -done +lemma omult_le_self2: + assumes i: "Ord(i)" and j: "0 j**i" +proof - + have oj: "Ord(j)" by (rule lt_Ord2 [OF j]) + show ?thesis using i + proof (induct i rule: trans_induct3) + case 0 thus ?case + by simp + next + case (succ i) + have "j \\ i ++ 0 < j \\ i ++ j" + by (rule oadd_lt_mono2 [OF j]) + with succ.hyps show ?case + by (simp add: oj j omult_succ ) (rule lt_trans1) + next + case (limit l) + hence "l = (\x\l. x)" + by (simp add: Union_eq_UN [symmetric] Limit_Union_eq) + also have "... \ (\x\l. j**x)" + by (rule le_implies_UN_le_UN) (rule limit.hyps) + finally have "l \ (\x\l. j**x)" . + thus ?case using limit.hyps by (simp add: oj omult_Limit) + qed +qed text{*Further properties of ordinal multiplication *} diff -r c2ca2c3d23a6 -r faf4a0b02b71 src/ZF/Ordinal.thy --- a/src/ZF/Ordinal.thy Wed Mar 14 00:34:56 2012 +0100 +++ b/src/ZF/Ordinal.thy Wed Mar 14 12:39:04 2012 +0000 @@ -708,7 +708,7 @@ |] ==> P" by (drule Ord_cases_disj, blast) -lemma trans_induct3 [case_names 0 succ limit, consumes 1]: +lemma trans_induct3_raw: "[| Ord(i); P(0); !!x. [| Ord(x); P(x) |] ==> P(succ(x)); @@ -718,7 +718,7 @@ apply (erule Ord_cases, blast+) done -lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1] +lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1] text{*A set of ordinals is either empty, contains its own union, or its union is a limit ordinal.*}