--- a/src/ZF/Cardinal.thy Wed Mar 07 23:21:00 2012 +0100
+++ b/src/ZF/Cardinal.thy Thu Mar 08 16:49:24 2012 +0000
@@ -101,7 +101,7 @@
apply (blast intro: bij_converse_bij)
done
-lemma eqpoll_trans:
+lemma eqpoll_trans [trans]:
"[| X \<approx> Y; Y \<approx> Z |] ==> X \<approx> Z"
apply (unfold eqpoll_def)
apply (blast intro: comp_bij)
@@ -122,11 +122,17 @@
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
by (unfold eqpoll_def bij_def lepoll_def, blast)
-lemma lepoll_trans: "[| X \<lesssim> Y; Y \<lesssim> Z |] ==> X \<lesssim> Z"
+lemma lepoll_trans [trans]: "[| X \<lesssim> Y; Y \<lesssim> Z |] ==> X \<lesssim> Z"
apply (unfold lepoll_def)
apply (blast intro: comp_inj)
done
+lemma eq_lepoll_trans [trans]: "[| X \<approx> Y; Y \<lesssim> Z |] ==> X \<lesssim> Z"
+ by (blast intro: eqpoll_imp_lepoll lepoll_trans)
+
+lemma lepoll_eq_trans [trans]: "[| X \<lesssim> Y; Y \<approx> Z |] ==> X \<lesssim> Z"
+ by (blast intro: eqpoll_imp_lepoll lepoll_trans)
+
(*Asymmetry law*)
lemma eqpollI: "[| X \<lesssim> Y; Y \<lesssim> X |] ==> X \<approx> Y"
apply (unfold lepoll_def eqpoll_def)
@@ -194,7 +200,7 @@
done
lemma inj_not_surj_succ:
- "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f:inj(A,m)"
+ "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f \<in> inj(A,m)"
apply (unfold inj_def surj_def)
apply (safe del: succE)
apply (erule swap, rule exI)
@@ -208,24 +214,32 @@
(** Variations on transitivity **)
-lemma lesspoll_trans:
+lemma lesspoll_trans [trans]:
"[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
apply (unfold lesspoll_def)
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
-lemma lesspoll_trans1:
+lemma lesspoll_trans1 [trans]:
"[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
apply (unfold lesspoll_def)
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
-lemma lesspoll_trans2:
+lemma lesspoll_trans2 [trans]:
"[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
apply (unfold lesspoll_def)
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
+lemma eq_lesspoll_trans [trans]:
+ "[| X \<approx> Y; Y \<prec> Z |] ==> X \<prec> Z"
+ by (blast intro: eqpoll_imp_lepoll lesspoll_trans1)
+
+lemma lesspoll_eq_trans [trans]:
+ "[| X \<prec> Y; Y \<approx> Z |] ==> X \<prec> Z"
+ by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
+
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
@@ -311,6 +325,9 @@
(* @{term"Ord(A) ==> |A| \<approx> A"} *)
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
+lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> ||A|| = |A|"
+ by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])
+
lemma well_ord_cardinal_eqE:
"[| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X \<approx> Y"
apply (rule eqpoll_sym [THEN eqpoll_trans])
@@ -335,7 +352,7 @@
apply (erule sym)
done
-(* Could replace the @{term"~(j \<approx> i)"} by @{term"~(i \<lesssim> j)"}. *)
+(* Could replace the @{term"~(j \<approx> i)"} by @{term"~(i \<preceq> j)"}. *)
lemma CardI: "[| Ord(i); !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
apply (unfold Card_def cardinal_def)
apply (subst Least_equality)
@@ -399,15 +416,18 @@
done
(*Kunen's Lemma 10.5*)
-lemma cardinal_eq_lemma: "[| |i| \<le> j; j \<le> i |] ==> |j| = |i|"
-apply (rule eqpollI [THEN cardinal_cong])
-apply (erule le_imp_lepoll)
-apply (rule lepoll_trans)
-apply (erule_tac [2] le_imp_lepoll)
-apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
-apply (rule Ord_cardinal_eqpoll)
-apply (elim ltE Ord_succD)
-done
+lemma cardinal_eq_lemma:
+ assumes i:"|i| \<le> j" and j: "j \<le> i" shows "|j| = |i|"
+proof (rule eqpollI [THEN cardinal_cong])
+ show "j \<lesssim> i" by (rule le_imp_lepoll [OF j])
+next
+ have Oi: "Ord(i)" using j by (rule le_Ord2)
+ hence "i \<approx> |i|"
+ by (blast intro: Ord_cardinal_eqpoll eqpoll_sym)
+ also have "... \<lesssim> j"
+ by (blast intro: le_imp_lepoll i)
+ finally show "i \<lesssim> j" .
+qed
lemma cardinal_mono: "i \<le> j ==> |i| \<le> |j|"
apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
@@ -438,19 +458,20 @@
(*Can use AC or finiteness to discharge first premise*)
lemma well_ord_lepoll_imp_Card_le:
- "[| well_ord(B,r); A \<lesssim> B |] ==> |A| \<le> |B|"
-apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
-apply (safe intro!: Ord_cardinal le_eqI)
-apply (rule eqpollI [THEN cardinal_cong], assumption)
-apply (rule lepoll_trans)
-apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
-apply (erule le_imp_lepoll [THEN lepoll_trans])
-apply (rule eqpoll_imp_lepoll)
-apply (unfold lepoll_def)
-apply (erule exE)
-apply (rule well_ord_cardinal_eqpoll)
-apply (erule well_ord_rvimage, assumption)
-done
+ assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
+ shows "|A| \<le> |B|"
+proof (rule Ord_linear_le [of "|A|" "|B|", OF Ord_cardinal Ord_cardinal], assumption)
+ assume BA: "|B| \<le> |A|"
+ from lepoll_well_ord [OF AB wB]
+ obtain s where s: "well_ord(A, s)" by blast
+ have "B \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
+ also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF BA])
+ also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
+ finally have "B \<lesssim> A" .
+ hence "A \<approx> B" by (blast intro: eqpollI AB)
+ hence "|A| = |B|" by (rule cardinal_cong)
+ thus ?thesis by simp
+qed
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
apply (rule le_trans)
@@ -535,14 +556,6 @@
lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n; n:nat |] ==> P"
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
-lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
-apply (unfold lesspoll_def)
-apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
- eqpoll_sym [THEN eqpoll_imp_lepoll]
- intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI,
- THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
-done
-
lemma nat_lepoll_imp_ex_eqpoll_n:
"[| n \<in> nat; nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
apply (unfold lepoll_def eqpoll_def)
@@ -627,6 +640,9 @@
apply (erule cardinal_mono)
done
+lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
+ by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
+
subsection{*Towards Cardinal Arithmetic *}
(** Congruence laws for successor, cardinal addition and multiplication **)
--- a/src/ZF/CardinalArith.thy Wed Mar 07 23:21:00 2012 +0100
+++ b/src/ZF/CardinalArith.thy Thu Mar 08 16:49:24 2012 +0000
@@ -48,36 +48,38 @@
cmult (infixl "\<otimes>" 70)
-lemma Card_Union [simp,intro,TC]: "(\<forall>x\<in>A. Card(x)) ==> Card(\<Union>(A))"
-apply (rule CardI)
- apply (simp add: Card_is_Ord)
-apply (clarify dest!: ltD)
-apply (drule bspec, assumption)
-apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord)
-apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
-apply (drule lesspoll_trans1, assumption)
-apply (subgoal_tac "B \<lesssim> \<Union>A")
- apply (drule lesspoll_trans1, assumption, blast)
-apply (blast intro: subset_imp_lepoll)
-done
+lemma Card_Union [simp,intro,TC]:
+ assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
+proof (rule CardI)
+ show "Ord(\<Union>A)" using A
+ by (simp add: Card_is_Ord)
+next
+ fix j
+ assume j: "j < \<Union>A"
+ hence "\<exists>c\<in>A. j < c & Card(c)" using A
+ by (auto simp add: lt_def intro: Card_is_Ord)
+ then obtain c where c: "c\<in>A" "j < c" "Card(c)"
+ by blast
+ hence jls: "j \<prec> c"
+ by (simp add: lt_Card_imp_lesspoll)
+ { assume eqp: "j \<approx> \<Union>A"
+ hence Uls: "\<Union>A \<prec> c" using jls
+ by (blast intro: eqpoll_sym eqpoll_imp_lepoll lesspoll_trans1)
+ moreover have "c \<lesssim> \<Union>A" using c
+ by (blast intro: subset_imp_lepoll)
+ ultimately have "c \<prec> c"
+ by (blast intro: lesspoll_trans1)
+ hence False
+ by auto
+ } thus "\<not> j \<approx> \<Union>A" by blast
+qed
lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
-by (blast intro: Card_Union)
+ by blast
lemma Card_OUN [simp,intro,TC]:
"(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
-by (simp add: OUnion_def Card_0)
-
-lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
-apply (unfold lesspoll_def)
-apply (rule conjI)
-apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
-apply (rule notI)
-apply (erule eqpollE)
-apply (rule succ_lepoll_natE)
-apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll]
- lepoll_trans, assumption)
-done
+ by (auto simp add: OUnion_def Card_0)
lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
apply (unfold lesspoll_def)
@@ -103,11 +105,10 @@
subsubsection{*Cardinal addition is commutative*}
lemma sum_commute_eqpoll: "A+B \<approx> B+A"
-apply (unfold eqpoll_def)
-apply (rule exI)
-apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective)
-apply auto
-done
+proof (unfold eqpoll_def, rule exI)
+ show "(\<lambda>z\<in>A+B. case(Inr,Inl,z)) \<in> bij(A+B, B+A)"
+ by (auto intro: lam_bijective [where d = "case(Inr,Inl)"])
+qed
lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
apply (unfold cadd_def)
@@ -153,10 +154,10 @@
subsubsection{*Addition by another cardinal*}
lemma sum_lepoll_self: "A \<lesssim> A+B"
-apply (unfold lepoll_def inj_def)
-apply (rule_tac x = "\<lambda>x\<in>A. Inl (x) " in exI)
-apply simp
-done
+proof (unfold lepoll_def, rule exI)
+ show "(\<lambda>x\<in>A. Inl (x)) \<in> inj(A, A + B)"
+ by (simp add: inj_def)
+qed
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
--- a/src/ZF/Int_ZF.thy Wed Mar 07 23:21:00 2012 +0100
+++ b/src/ZF/Int_ZF.thy Thu Mar 08 16:49:24 2012 +0000
@@ -707,7 +707,7 @@
apply auto
done
-lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
+lemma zless_trans [trans]: "[| x $< y; y $< z |] ==> x $< z"
apply (subgoal_tac "intify (x) $< intify (z) ")
apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
apply auto
@@ -750,19 +750,19 @@
apply (blast intro: zless_trans)
done
-lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
+lemma zle_trans [trans]: "[| x $<= y; y $<= z |] ==> x $<= z"
apply (subgoal_tac "intify (x) $<= intify (z) ")
apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
apply auto
done
-lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
+lemma zle_zless_trans [trans]: "[| i $<= j; j $< k |] ==> i $< k"
apply (auto simp add: zle_def)
apply (blast intro: zless_trans)
apply (simp add: zless_def zdiff_def zadd_def)
done
-lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
+lemma zless_zle_trans [trans]: "[| i $< j; j $<= k |] ==> i $< k"
apply (auto simp add: zle_def)
apply (blast intro: zless_trans)
apply (simp add: zless_def zdiff_def zminus_def)
--- a/src/ZF/OrderType.thy Wed Mar 07 23:21:00 2012 +0100
+++ b/src/ZF/OrderType.thy Thu Mar 08 16:49:24 2012 +0000
@@ -74,8 +74,7 @@
The smaller ordinal is an initial segment of the larger *)
lemma lt_pred_Memrel:
"j<i ==> pred(i, j, Memrel(i)) = j"
-apply (unfold pred_def lt_def)
-apply (simp (no_asm_simp))
+apply (simp add: pred_def lt_def)
apply (blast intro: Ord_trans)
done
--- a/src/ZF/Ordinal.thy Wed Mar 07 23:21:00 2012 +0100
+++ b/src/ZF/Ordinal.thy Thu Mar 08 16:49:24 2012 +0000
@@ -9,7 +9,7 @@
definition
Memrel :: "i=>i" where
- "Memrel(A) == {z: A*A . \<exists>x y. z=<x,y> & x:y }"
+ "Memrel(A) == {z\<in>A*A . \<exists>x y. z=<x,y> & x\<in>y }"
definition
Transset :: "i=>o" where
@@ -21,7 +21,7 @@
definition
lt :: "[i,i] => o" (infixl "<" 50) (*less-than on ordinals*) where
- "i<j == i:j & Ord(j)"
+ "i<j == i\<in>j & Ord(j)"
definition
Limit :: "i=>o" where
@@ -56,11 +56,11 @@
subsubsection{*Consequences of Downwards Closure*}
lemma Transset_doubleton_D:
- "[| Transset(C); {a,b}: C |] ==> a:C & b: C"
+ "[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C"
by (unfold Transset_def, blast)
lemma Transset_Pair_D:
- "[| Transset(C); <a,b>: C |] ==> a:C & b: C"
+ "[| Transset(C); <a,b>\<in>C |] ==> a\<in>C & b\<in>C"
apply (simp add: Pair_def)
apply (blast dest: Transset_doubleton_D)
done
@@ -96,11 +96,11 @@
by (unfold Transset_def, blast)
lemma Transset_Union_family:
- "[| !!i. i:A ==> Transset(i) |] ==> Transset(\<Union>(A))"
+ "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Union>(A))"
by (unfold Transset_def, blast)
lemma Transset_Inter_family:
- "[| !!i. i:A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
+ "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
by (unfold Inter_def Transset_def, blast)
lemma Transset_UN:
@@ -115,22 +115,22 @@
subsection{*Lemmas for Ordinals*}
lemma OrdI:
- "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)"
+ "[| Transset(i); !!x. x\<in>i ==> Transset(x) |] ==> Ord(i)"
by (simp add: Ord_def)
lemma Ord_is_Transset: "Ord(i) ==> Transset(i)"
by (simp add: Ord_def)
lemma Ord_contains_Transset:
- "[| Ord(i); j:i |] ==> Transset(j) "
+ "[| Ord(i); j\<in>i |] ==> Transset(j) "
by (unfold Ord_def, blast)
-lemma Ord_in_Ord: "[| Ord(i); j:i |] ==> Ord(j)"
+lemma Ord_in_Ord: "[| Ord(i); j\<in>i |] ==> Ord(j)"
by (unfold Ord_def Transset_def, blast)
(*suitable for rewriting PROVIDED i has been fixed*)
-lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
+lemma Ord_in_Ord': "[| j\<in>i; Ord(i) |] ==> Ord(j)"
by (blast intro: Ord_in_Ord)
(* Ord(succ(j)) ==> Ord(j) *)
@@ -139,13 +139,13 @@
lemma Ord_subset_Ord: "[| Ord(i); Transset(j); j<=i |] ==> Ord(j)"
by (simp add: Ord_def Transset_def, blast)
-lemma OrdmemD: "[| j:i; Ord(i) |] ==> j<=i"
+lemma OrdmemD: "[| j\<in>i; Ord(i) |] ==> j<=i"
by (unfold Ord_def Transset_def, blast)
-lemma Ord_trans: "[| i:j; j:k; Ord(k) |] ==> i:k"
+lemma Ord_trans: "[| i\<in>j; j\<in>k; Ord(k) |] ==> i\<in>k"
by (blast dest: OrdmemD)
-lemma Ord_succ_subsetI: "[| i:j; Ord(j) |] ==> succ(i) \<subseteq> j"
+lemma Ord_succ_subsetI: "[| i\<in>j; Ord(j) |] ==> succ(i) \<subseteq> j"
by (blast dest: OrdmemD)
@@ -172,28 +172,33 @@
apply (blast intro!: Transset_Int)
done
-(*There is no set of all ordinals, for then it would contain itself*)
-lemma ON_class: "~ (\<forall>i. i:X <-> Ord(i))"
-apply (rule notI)
-apply (frule_tac x = X in spec)
-apply (safe elim!: mem_irrefl)
-apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
-apply (simp add: Transset_def)
-apply (blast intro: Ord_in_Ord)+
-done
+text{*There is no set of all ordinals, for then it would contain itself*}
+lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))"
+proof (rule notI)
+ assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)"
+ have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X"
+ by (simp add: X, blast intro: Ord_in_Ord)
+ hence "Transset(X)"
+ by (auto simp add: Transset_def)
+ moreover have "\<And>x. x \<in> X \<Longrightarrow> Transset(x)"
+ by (simp add: X Ord_def)
+ ultimately have "Ord(X)" by (rule OrdI)
+ hence "X \<in> X" by (simp add: X)
+ thus "False" by (rule mem_irrefl)
+qed
subsection{*< is 'less Than' for Ordinals*}
-lemma ltI: "[| i:j; Ord(j) |] ==> i<j"
+lemma ltI: "[| i\<in>j; Ord(j) |] ==> i<j"
by (unfold lt_def, blast)
lemma ltE:
- "[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P"
+ "[| i<j; [| i\<in>j; Ord(i); Ord(j) |] ==> P |] ==> P"
apply (unfold lt_def)
apply (blast intro: Ord_in_Ord)
done
-lemma ltD: "i<j ==> i:j"
+lemma ltD: "i<j ==> i\<in>j"
by (erule ltE, assumption)
lemma not_lt0 [simp]: "~ i<0"
@@ -211,7 +216,7 @@
(* i<0 ==> R *)
lemmas lt0E = not_lt0 [THEN notE, elim!]
-lemma lt_trans: "[| i<j; j<k |] ==> i<k"
+lemma lt_trans [trans]: "[| i<j; j<k |] ==> i<k"
by (blast intro!: ltI elim!: ltE intro: Ord_trans)
lemma lt_not_sym: "i<j ==> ~ (j<i)"
@@ -238,10 +243,10 @@
(*Equivalently, i<j ==> i < succ(j)*)
lemma leI: "i<j ==> i \<le> j"
-by (simp (no_asm_simp) add: le_iff)
+by (simp add: le_iff)
lemma le_eqI: "[| i=j; Ord(j) |] ==> i \<le> j"
-by (simp (no_asm_simp) add: le_iff)
+by (simp add: le_iff)
lemmas le_refl = refl [THEN le_eqI]
@@ -268,7 +273,7 @@
subsection{*Natural Deduction Rules for Memrel*}
(*The lemmas MemrelI/E give better speed than [iff] here*)
-lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a:b & a:A & b:A"
+lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A"
by (unfold Memrel_def, blast)
lemma MemrelI [intro!]: "[| a: b; a: A; b: A |] ==> <a,b> \<in> Memrel(A)"
@@ -276,7 +281,7 @@
lemma MemrelE [elim!]:
"[| <a,b> \<in> Memrel(A);
- [| a: A; b: A; a:b |] ==> P |]
+ [| a: A; b: A; a\<in>b |] ==> P |]
==> P"
by auto
@@ -314,7 +319,7 @@
(*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
lemma Transset_Memrel_iff:
- "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a:b & b:A"
+ "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A"
by (unfold Transset_def, blast)
@@ -352,7 +357,7 @@
subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
lemma Ord_linear [rule_format]:
- "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i:j | i=j | j:i)"
+ "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i\<in>j | i=j | j\<in>i)"
apply (erule trans_induct)
apply (rule impI [THEN allI])
apply (erule_tac i=j in trans_induct)
@@ -386,7 +391,7 @@
subsubsection{*Some Rewrite Rules for <, le*}
-lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i<j"
+lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
by (unfold lt_def, blast)
lemma not_lt_iff_le: "[| Ord(i); Ord(j) |] ==> ~ i<j <-> j \<le> i"
@@ -508,7 +513,7 @@
done
lemma Un_least_mem_iff:
- "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k <-> i:k & j:k"
+ "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k <-> i\<in>k & j\<in>k"
apply (insert Un_least_lt_iff [of i j k])
apply (simp add: lt_def)
done
@@ -529,13 +534,13 @@
by (simp add: Ord_Un_if lt_Ord le_Ord2)
lemma lt_Un_iff:
- "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j";
+ "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j"
apply (simp add: Ord_Un_if not_lt_iff_le)
apply (blast intro: leI lt_trans2)+
done
lemma le_Un_iff:
- "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j";
+ "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"
by (simp add: succ_Un_distrib lt_Un_iff [symmetric])
lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i \<union> j"
@@ -551,17 +556,17 @@
subsection{*Results about Limits*}
-lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(\<Union>(A))"
+lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))"
apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
apply (blast intro: Ord_contains_Transset)+
done
lemma Ord_UN [intro,simp,TC]:
- "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
+ "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
by (rule Ord_Union, blast)
lemma Ord_Inter [intro,simp,TC]:
- "[| !!i. i:A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
+ "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
apply (rule Transset_Inter_family [THEN OrdI])
apply (blast intro: Ord_is_Transset)
apply (simp add: Inter_def)
@@ -569,19 +574,19 @@
done
lemma Ord_INT [intro,simp,TC]:
- "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
+ "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
by (rule Ord_Inter, blast)
(* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
lemma UN_least_le:
- "[| Ord(i); !!x. x:A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
+ "[| Ord(i); !!x. x\<in>A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
apply (blast intro: Ord_UN elim: ltE)+
done
lemma UN_succ_least_lt:
- "[| j<i; !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
+ "[| j<i; !!x. x\<in>A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
apply (rule ltE, assumption)
apply (rule UN_least_le [THEN lt_trans2])
apply (blast intro: succ_leI)+
@@ -608,7 +613,7 @@
done
lemma le_implies_UN_le_UN:
- "[| !!x. x:A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
+ "[| !!x. x\<in>A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
apply (rule UN_least_le)
apply (rule_tac [2] UN_upper_le)
apply (blast intro: Ord_UN le_Ord2)+
@@ -664,13 +669,18 @@
done
lemma non_succ_LimitI:
- "[| 0<i; \<forall>y. succ(y) \<noteq> i |] ==> Limit(i)"
-apply (unfold Limit_def)
-apply (safe del: subsetI)
-apply (rule_tac [2] not_le_iff_lt [THEN iffD1])
-apply (simp_all add: lt_Ord lt_Ord2)
-apply (blast elim: leE lt_asym)
-done
+ assumes i: "0<i" and nsucc: "\<And>y. succ(y) \<noteq> i"
+ shows "Limit(i)"
+proof -
+ have Oi: "Ord(i)" using i by (simp add: lt_def)
+ { fix y
+ assume yi: "y<i"
+ hence Osy: "Ord(succ(y))" by (simp add: lt_Ord Ord_succ)
+ have "~ i \<le> y" using yi by (blast dest: le_imp_not_lt)
+ hence "succ(y) < i" using nsucc [of y]
+ by (blast intro: Ord_linear_lt [OF Osy Oi]) }
+ thus ?thesis using i Oi by (auto simp add: Limit_def)
+qed
lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P"
apply (rule lt_irrefl)
@@ -712,25 +722,41 @@
text{*A set of ordinals is either empty, contains its own union, or its
union is a limit ordinal.*}
+
+lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j"
+ by (auto simp add: le_subset_iff Union_least)
+
lemma Ord_set_cases:
- "\<forall>i\<in>I. Ord(i) ==> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
-apply (clarify elim!: not_emptyE)
-apply (cases "\<Union>(I)" rule: Ord_cases)
- apply (blast intro: Ord_Union)
- apply (blast intro: subst_elem)
- apply auto
-apply (clarify elim!: equalityE succ_subsetE)
-apply (simp add: Union_subset_iff)
-apply (subgoal_tac "B = succ(j)", blast)
-apply (rule le_anti_sym)
- apply (simp add: le_subset_iff)
-apply (simp add: ltI)
-done
+ assumes I: "\<forall>i\<in>I. Ord(i)"
+ shows "I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
+proof (cases "\<Union>(I)" rule: Ord_cases)
+ show "Ord(\<Union>I)" using I by (blast intro: Ord_Union)
+next
+ assume "\<Union>I = 0" thus ?thesis by (simp, blast intro: subst_elem)
+next
+ fix j
+ assume j: "Ord(j)" and UIj:"\<Union>(I) = succ(j)"
+ { assume "\<forall>i\<in>I. i\<le>j"
+ hence "\<Union>(I) \<le> j"
+ by (simp add: Union_le j)
+ hence False
+ by (simp add: UIj lt_not_refl) }
+ then obtain i where i: "i \<in> I" "succ(j) \<le> i" using I j
+ by (atomize, auto simp add: not_le_iff_lt)
+ have "\<Union>(I) \<le> succ(j)" using UIj j by auto
+ hence "i \<le> succ(j)" using i
+ by (simp add: le_subset_iff Union_subset_iff)
+ hence "succ(j) = i" using i
+ by (blast intro: le_anti_sym)
+ hence "succ(j) \<in> I" by (simp add: i)
+ thus ?thesis by (simp add: UIj)
+next
+ assume "Limit(\<Union>I)" thus ?thesis by auto
+qed
-text{*If the union of a set of ordinals is a successor, then it is
-an element of that set.*}
+text{*If the union of a set of ordinals is a successor, then it is an element of that set.*}
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X"
-by (drule Ord_set_cases, auto)
+ by (drule Ord_set_cases, auto)
lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
apply (simp add: Limit_def lt_def)
--- a/src/ZF/pair.thy Wed Mar 07 23:21:00 2012 +0100
+++ b/src/ZF/pair.thy Thu Mar 08 16:49:24 2012 +0000
@@ -58,18 +58,22 @@
declare sym [THEN Pair_neq_0, elim!]
lemma Pair_neq_fst: "<a,b>=a ==> P"
-apply (unfold Pair_def)
-apply (rule consI1 [THEN mem_asym, THEN FalseE])
-apply (erule subst)
-apply (rule consI1)
-done
+proof (unfold Pair_def)
+ assume eq: "{{a, a}, {a, b}} = a"
+ have "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
+ hence "{a, a} \<in> a" by (simp add: eq)
+ moreover have "a \<in> {a, a}" by (rule consI1)
+ ultimately show "P" by (rule mem_asym)
+qed
lemma Pair_neq_snd: "<a,b>=b ==> P"
-apply (unfold Pair_def)
-apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
-apply (erule subst)
-apply (rule consI1 [THEN consI2])
-done
+proof (unfold Pair_def)
+ assume eq: "{{a, a}, {a, b}} = b"
+ have "{a, b} \<in> {{a, a}, {a, b}}" by blast
+ hence "{a, b} \<in> b" by (simp add: eq)
+ moreover have "b \<in> {a, b}" by blast
+ ultimately show "P" by (rule mem_asym)
+qed
subsection{*Sigma: Disjoint Union of a Family of Sets*}
@@ -145,15 +149,12 @@
"[| p:Sigma(A,B);
!!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)
|] ==> split(%x y. c(x,y), p) \<in> C(p)"
-apply (erule SigmaE, auto)
-done
+by (erule SigmaE, auto)
lemma expand_split:
"u: A*B ==>
R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
-apply (simp add: split_def)
-apply auto
-done
+by (auto simp add: split_def)
subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
@@ -165,9 +166,7 @@
"[| split(R,z); z:Sigma(A,B);
!!x y. [| z = <x,y>; R(x,y) |] ==> P
|] ==> P"
-apply (simp add: split_def)
-apply (erule SigmaE, force)
-done
+by (auto simp add: split_def)
lemma splitD: "split(R,<a,b>) ==> R(a,b)"
by (simp add: split_def)