1.1 --- a/src/ZF/Cardinal.thy Wed Mar 14 17:40:00 2012 +0100
1.2 +++ b/src/ZF/Cardinal.thy Wed Mar 14 17:19:30 2012 +0000
1.3 @@ -540,15 +540,21 @@
1.4 done
1.5
1.6
1.7 -lemma nat_lepoll_imp_le [rule_format]:
1.8 - "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n"
1.9 -apply (induct_tac m)
1.10 -apply (blast intro!: nat_0_le)
1.11 -apply (rule ballI)
1.12 -apply (erule_tac n = n in natE)
1.13 -apply (simp (no_asm_simp) add: lepoll_def inj_def)
1.14 -apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
1.15 -done
1.16 +lemma nat_lepoll_imp_le:
1.17 + "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
1.18 +proof (induct m arbitrary: n rule: nat_induct)
1.19 + case 0 thus ?case by (blast intro!: nat_0_le)
1.20 +next
1.21 + case (succ m)
1.22 + show ?case using `n \<in> nat`
1.23 + proof (cases rule: natE)
1.24 + case 0 thus ?thesis using succ
1.25 + by (simp add: lepoll_def inj_def)
1.26 + next
1.27 + case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n`
1.28 + by (blast intro!: succ_leI dest!: succ_lepoll_succD)
1.29 + qed
1.30 +qed
1.31
1.32 lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
1.33 apply (rule iffI)
2.1 --- a/src/ZF/CardinalArith.thy Wed Mar 14 17:40:00 2012 +0100
2.2 +++ b/src/ZF/CardinalArith.thy Wed Mar 14 17:19:30 2012 +0000
2.3 @@ -628,28 +628,25 @@
2.4 assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
2.5 proof -
2.6 have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card)
2.7 - have "InfCard(K) \<longrightarrow> K \<otimes> K = K"
2.8 - proof (rule trans_induct [OF OK], rule impI)
2.9 - fix i
2.10 - assume i: "Ord(i)" "InfCard(i)"
2.11 - and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y"
2.12 - show "i \<otimes> i = i"
2.13 - proof (rule le_anti_sym)
2.14 - have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|"
2.15 - by (rule cardinal_cong,
2.16 - simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
2.17 - hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i
2.18 - by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
2.19 - moreover
2.20 - have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i
2.21 - by (simp add: ordertype_csquare_le)
2.22 - ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
2.23 - next
2.24 - show "i \<le> i \<otimes> i" using i
2.25 - by (blast intro: cmult_square_le InfCard_is_Card)
2.26 - qed
2.27 + show "InfCard(K) ==> K \<otimes> K = K" using OK
2.28 + proof (induct rule: trans_induct)
2.29 + case (step i)
2.30 + show "i \<otimes> i = i"
2.31 + proof (rule le_anti_sym)
2.32 + have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|"
2.33 + by (rule cardinal_cong,
2.34 + simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
2.35 + hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))"
2.36 + by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
2.37 + moreover
2.38 + have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step
2.39 + by (simp add: ordertype_csquare_le)
2.40 + ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
2.41 + next
2.42 + show "i \<le> i \<otimes> i" using step
2.43 + by (blast intro: cmult_square_le InfCard_is_Card)
2.44 qed
2.45 - thus ?thesis using IK ..
2.46 + qed
2.47 qed
2.48
2.49 (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
2.50 @@ -910,10 +907,15 @@
2.51 finally show ?thesis .
2.52 qed
2.53
2.54 -lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat"
2.55 -apply (erule trans_induct3, auto)
2.56 -apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
2.57 -done
2.58 +lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat | i=nat"
2.59 +proof (induct i rule: trans_induct3)
2.60 + case 0 thus ?case by auto
2.61 +next
2.62 + case (succ i) thus ?case by auto
2.63 +next
2.64 + case (limit l) thus ?case
2.65 + by (blast dest: nat_le_Limit le_imp_subset)
2.66 +qed
2.67
2.68 lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
2.69 by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
3.1 --- a/src/ZF/Nat_ZF.thy Wed Mar 14 17:40:00 2012 +0100
3.2 +++ b/src/ZF/Nat_ZF.thy Wed Mar 14 17:19:30 2012 +0000
3.3 @@ -87,14 +87,16 @@
3.4
3.5 (*Mathematical induction*)
3.6 lemma nat_induct [case_names 0 succ, induct set: nat]:
3.7 - "[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
3.8 + "[| n \<in> nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
3.9 by (erule def_induct [OF nat_def nat_bnd_mono], blast)
3.10
3.11 lemma natE:
3.12 - "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
3.13 -by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
3.14 + assumes "n \<in> nat"
3.15 + obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
3.16 +using assms
3.17 +by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
3.18
3.19 -lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
3.20 +lemma nat_into_Ord [simp]: "n \<in> nat ==> Ord(n)"
3.21 by (erule nat_induct, auto)
3.22
3.23 (* @{term"i: nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"} *)
3.24 @@ -123,7 +125,7 @@
3.25 lemma succ_natD: "succ(i): nat ==> i: nat"
3.26 by (rule Ord_trans [OF succI1], auto)
3.27
3.28 -lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
3.29 +lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n \<in> nat"
3.30 by (blast dest!: succ_natD)
3.31
3.32 lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
3.33 @@ -138,7 +140,7 @@
3.34 (* [| succ(i): k; k: nat |] ==> i: k *)
3.35 lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
3.36
3.37 -lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat"
3.38 +lemma lt_nat_in_nat: "[| m<n; n \<in> nat |] ==> m: nat"
3.39 apply (erule ltE)
3.40 apply (erule Ord_trans, assumption, simp)
3.41 done
3.42 @@ -158,7 +160,7 @@
3.43
3.44
3.45 lemma nat_induct_from_lemma [rule_format]:
3.46 - "[| n: nat; m: nat;
3.47 + "[| n \<in> nat; m: nat;
3.48 !!x. [| x: nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
3.49 ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
3.50 apply (erule nat_induct)
3.51 @@ -167,7 +169,7 @@
3.52
3.53 (*Induction starting from m rather than 0*)
3.54 lemma nat_induct_from:
3.55 - "[| m \<le> n; m: nat; n: nat;
3.56 + "[| m \<le> n; m: nat; n \<in> nat;
3.57 P(m);
3.58 !!x. [| x: nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
3.59 ==> P(n)"
3.60 @@ -176,7 +178,7 @@
3.61
3.62 (*Induction suitable for subtraction and less-than*)
3.63 lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
3.64 - "[| m: nat; n: nat;
3.65 + "[| m: nat; n \<in> nat;
3.66 !!x. x: nat ==> P(x,0);
3.67 !!y. y: nat ==> P(0,succ(y));
3.68 !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |]
3.69 @@ -201,7 +203,7 @@
3.70 done
3.71
3.72 lemma succ_lt_induct:
3.73 - "[| m<n; n: nat;
3.74 + "[| m<n; n \<in> nat;
3.75 P(m,succ(m));
3.76 !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) |]
3.77 ==> P(m,n)"
3.78 @@ -241,7 +243,7 @@
3.79 by (simp add: nat_case_def)
3.80
3.81 lemma nat_case_type [TC]:
3.82 - "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
3.83 + "[| n \<in> nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
3.84 ==> nat_case(a,b,n) \<in> C(n)";
3.85 by (erule nat_induct, auto)
3.86
4.1 --- a/src/ZF/Ordinal.thy Wed Mar 14 17:40:00 2012 +0100
4.2 +++ b/src/ZF/Ordinal.thy Wed Mar 14 17:19:30 2012 +0000
4.3 @@ -236,7 +236,7 @@
4.4 done
4.5
4.6
4.7 -(** Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! **)
4.8 +text{* Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! *}
4.9
4.10 lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))"
4.11 by (unfold lt_def, blast)
4.12 @@ -335,12 +335,11 @@
4.13 done
4.14
4.15 (*Induction over an ordinal*)
4.16 -lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
4.17 -lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
4.18 +lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
4.19
4.20 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
4.21
4.22 -lemma trans_induct [consumes 1]:
4.23 +lemma trans_induct [rule_format, consumes 1, case_names step]:
4.24 "[| Ord(i);
4.25 !!x.[| Ord(x); \<forall>y\<in>x. P(y) |] ==> P(x) |]
4.26 ==> P(i)"
4.27 @@ -348,10 +347,8 @@
4.28 apply (blast intro: Ord_succ [THEN Ord_in_Ord])
4.29 done
4.30
4.31 -lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
4.32
4.33 -
4.34 -(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
4.35 +section{*Fundamental properties of the epsilon ordering (< on ordinals)*}
4.36
4.37
4.38 subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
4.39 @@ -364,23 +361,27 @@
4.40 apply (blast dest: Ord_trans)
4.41 done
4.42
4.43 -(*The trichotomy law for ordinals!*)
4.44 +text{*The trichotomy law for ordinals*}
4.45 lemma Ord_linear_lt:
4.46 - "[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P"
4.47 + assumes o: "Ord(i)" "Ord(j)"
4.48 + obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i"
4.49 apply (simp add: lt_def)
4.50 -apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+)
4.51 +apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE])
4.52 +apply (blast intro: o)+
4.53 done
4.54
4.55 lemma Ord_linear2:
4.56 - "[| Ord(i); Ord(j); i<j ==> P; j \<le> i ==> P |] ==> P"
4.57 + assumes o: "Ord(i)" "Ord(j)"
4.58 + obtains (lt) "i<j" | (ge) "j \<le> i"
4.59 apply (rule_tac i = i and j = j in Ord_linear_lt)
4.60 -apply (blast intro: leI le_eqI sym ) +
4.61 +apply (blast intro: leI le_eqI sym o) +
4.62 done
4.63
4.64 lemma Ord_linear_le:
4.65 - "[| Ord(i); Ord(j); i \<le> j ==> P; j \<le> i ==> P |] ==> P"
4.66 + assumes o: "Ord(i)" "Ord(j)"
4.67 + obtains (le) "i \<le> j" | (ge) "j \<le> i"
4.68 apply (rule_tac i = i and j = j in Ord_linear_lt)
4.69 -apply (blast intro: leI le_eqI ) +
4.70 +apply (blast intro: leI le_eqI o) +
4.71 done
4.72
4.73 lemma le_imp_not_lt: "j \<le> i ==> ~ i<j"
4.74 @@ -701,12 +702,9 @@
4.75 by (blast intro!: non_succ_LimitI Ord_0_lt)
4.76
4.77 lemma Ord_cases:
4.78 - "[| Ord(i);
4.79 - i=0 ==> P;
4.80 - !!j. [| Ord(j); i=succ(j) |] ==> P;
4.81 - Limit(i) ==> P
4.82 - |] ==> P"
4.83 -by (drule Ord_cases_disj, blast)
4.84 + assumes i: "Ord(i)"
4.85 + obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
4.86 +by (insert Ord_cases_disj [OF i], auto)
4.87
4.88 lemma trans_induct3_raw:
4.89 "[| Ord(i);
5.1 --- a/src/ZF/ex/LList.thy Wed Mar 14 17:40:00 2012 +0100
5.2 +++ b/src/ZF/ex/LList.thy Wed Mar 14 17:19:30 2012 +0000
5.3 @@ -106,15 +106,22 @@
5.4 declare qunivD [dest!]
5.5 declare Ord_in_Ord [elim!]
5.6
5.7 -lemma llist_quniv_lemma [rule_format]:
5.8 - "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
5.9 -apply (erule trans_induct)
5.10 -apply (rule ballI)
5.11 -apply (erule llist.cases)
5.12 -apply (simp_all add: QInl_def QInr_def llist.con_defs)
5.13 -(*LCons case: I simply can't get rid of the deepen_tac*)
5.14 -apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
5.15 -done
5.16 +lemma llist_quniv_lemma:
5.17 + "Ord(i) ==> l \<in> llist(quniv(A)) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
5.18 +proof (induct i arbitrary: l rule: trans_induct)
5.19 + case (step i l)
5.20 + show ?case using `l \<in> llist(quniv(A))`
5.21 + proof (cases l rule: llist.cases)
5.22 + case LNil thus ?thesis
5.23 + by (simp add: QInl_def QInr_def llist.con_defs)
5.24 + next
5.25 + case (LCons a l) thus ?thesis using step.hyps
5.26 + proof (simp add: QInl_def QInr_def llist.con_defs)
5.27 + show "<1; <a; l>> \<inter> Vset(i) \<subseteq> univ(eclose(A))" using LCons `Ord(i)`
5.28 + by (fast intro: step Ord_trans Int_lower1 [THEN subset_trans])
5.29 + qed
5.30 + qed
5.31 +qed
5.32
5.33 lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)"
5.34 apply (rule qunivI [THEN subsetI])
5.35 @@ -134,14 +141,19 @@
5.36 declare Ord_in_Ord [elim!]
5.37
5.38 (*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
5.39 -lemma lleq_Int_Vset_subset [rule_format]:
5.40 - "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
5.41 -apply (erule trans_induct)
5.42 -apply (intro allI impI)
5.43 -apply (erule lleq.cases)
5.44 -apply (unfold QInr_def llist.con_defs, safe)
5.45 -apply (fast elim!: Ord_trans bspec [elim_format])
5.46 -done
5.47 +lemma lleq_Int_Vset_subset:
5.48 + "Ord(i) ==> <l,l'> \<in> lleq(A) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
5.49 +proof (induct i arbitrary: l l' rule: trans_induct)
5.50 + case (step i l l')
5.51 + show ?case using `\<langle>l, l'\<rangle> \<in> lleq(A)`
5.52 + proof (cases rule: lleq.cases)
5.53 + case LNil thus ?thesis
5.54 + by (auto simp add: QInr_def llist.con_defs)
5.55 + next
5.56 + case (LCons a l l') thus ?thesis using step.hyps
5.57 + by (auto simp add: QInr_def llist.con_defs intro: Ord_trans)
5.58 + qed
5.59 +qed
5.60
5.61 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
5.62 lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)"
5.63 @@ -208,15 +220,22 @@
5.64
5.65 (*Reasoning borrowed from lleq.ML; a similar proof works for all
5.66 "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
5.67 -lemma flip_llist_quniv_lemma [rule_format]:
5.68 - "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
5.69 -apply (erule trans_induct)
5.70 -apply (rule ballI)
5.71 -apply (erule llist.cases, simp_all)
5.72 -apply (simp_all add: QInl_def QInr_def llist.con_defs)
5.73 -(*LCons case: I simply can't get rid of the deepen_tac*)
5.74 -apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
5.75 -done
5.76 +lemma flip_llist_quniv_lemma:
5.77 + "Ord(i) ==> l \<in> llist(bool) \<Longrightarrow> flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
5.78 +proof (induct i arbitrary: l rule: trans_induct)
5.79 + case (step i l)
5.80 + show ?case using `l \<in> llist(bool)`
5.81 + proof (cases l rule: llist.cases)
5.82 + case LNil thus ?thesis
5.83 + by (simp, simp add: QInl_def QInr_def llist.con_defs)
5.84 + next
5.85 + case (LCons a l) thus ?thesis using step.hyps
5.86 + proof (simp, simp add: QInl_def QInr_def llist.con_defs)
5.87 + show "<1; <not(a); flip(l)>> \<inter> Vset(i) \<subseteq> univ(eclose(bool))" using LCons step.hyps
5.88 + by (auto intro: Ord_trans)
5.89 + qed
5.90 + qed
5.91 +qed
5.92
5.93 lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"
5.94 by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)