# HG changeset patch
# User paulson
# Date 1331833085 0
# Node ID d8b3412cdb999b13ce89c4a64877a996977b3078
# Parent  2b6e55924af31a67534de3a5b1e2f238a324a64c
beautification and structured proofs

diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/AC/HH.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -98,7 +98,7 @@
 done
 
 lemma HH_subset_x_imp_lepoll: 
-     "[| HH(f, x, i) \<in> Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"
+     "[| HH(f, x, i) \<in> Pow(x)-{0}; Ord(i) |] ==> i \<lesssim> Pow(x)-{0}"
 apply (unfold lepoll_def inj_def)
 apply (rule_tac x = "\<lambda>j \<in> i. HH (f, x, j) " in exI)
 apply (simp (no_asm_simp))
diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/AC/WO2_AC16.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -177,7 +177,7 @@
 done
 
 lemma Union_lesspoll:
-     "[| \<forall>x \<in> X. x lepoll n & x \<subseteq> T; well_ord(T, R); X lepoll b;   
+     "[| \<forall>x \<in> X. x \<lesssim> n & x \<subseteq> T; well_ord(T, R); X \<lesssim> b;   
          b<a; ~Finite(a); Card(a); n \<in> nat |]   
       ==> \<Union>(X)\<prec>a"
 apply (case_tac "Finite (X)")
@@ -203,7 +203,7 @@
 lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)"
 by fast
 
-lemma Un_lepoll_succ: "A lepoll B ==> A \<union> {a} lepoll succ(B)"
+lemma Un_lepoll_succ: "A \<lesssim> B ==> A \<union> {a} \<lesssim> succ(B)"
 apply (simp add: Un_sing_eq_cons succ_def)
 apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
 done
@@ -216,7 +216,7 @@
 
 lemma recfunAC16_Diff_lepoll_1:
      "Ord(x) 
-      ==> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) lepoll 1"
+      ==> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) \<lesssim> 1"
 apply (erule Ord_cases)
   apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll])
 (*Limit case*)
@@ -247,13 +247,13 @@
 done
 
 
-lemma two_in_lepoll_1: "[| A lepoll 1; a \<in> A; b \<in> A |] ==> a=b"
+lemma two_in_lepoll_1: "[| A \<lesssim> 1; a \<in> A; b \<in> A |] ==> a=b"
 by (fast dest!: lepoll_1_is_sing)
 
 
 lemma UN_lepoll_index:
-     "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) lepoll 1; Limit(a) |]   
-      ==> (\<Union>x<a. F(x)) lepoll a"
+     "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a) |]   
+      ==> (\<Union>x<a. F(x)) \<lesssim> a"
 apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
 apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). LEAST i. z \<in> F (i) " in exI)
 apply (unfold inj_def)
@@ -271,7 +271,7 @@
 done
 
 
-lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) lepoll y"
+lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) \<lesssim> y"
 apply (erule trans_induct3)
 (*0 case*)
 apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl)
@@ -369,7 +369,7 @@
 
 
 lemma subset_imp_eq_lemma:
-     "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m lepoll A & B lepoll m \<longrightarrow> A=B"
+     "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m \<lesssim> A & B \<lesssim> m \<longrightarrow> A=B"
 apply (induct_tac "m")
 apply (fast dest!: lepoll_0_is_0)
 apply (intro allI impI)
@@ -385,7 +385,7 @@
 done
 
 
-lemma subset_imp_eq: "[| A \<subseteq> B; m lepoll A; B lepoll m; m \<in> nat |] ==> A=B"
+lemma subset_imp_eq: "[| A \<subseteq> B; m \<lesssim> A; B \<lesssim> m; m \<in> nat |] ==> A=B"
 by (blast dest!: subset_imp_eq_lemma)
 
 
diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Cardinal_AC.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -11,7 +11,7 @@
 
 subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
 
-lemma cardinal_eqpoll: "|A| eqpoll A"
+lemma cardinal_eqpoll: "|A| \<approx> A"
 apply (rule AC_well_ord [THEN exE])
 apply (erule well_ord_cardinal_eqpoll)
 done
@@ -19,13 +19,13 @@
 text{*The theorem @{term "||A|| = |A|"} *}
 lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
 
-lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
+lemma cardinal_eqE: "|X| = |Y| ==> X \<approx> Y"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule well_ord_cardinal_eqE, assumption+)
 done
 
-lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X eqpoll Y"
+lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X \<approx> Y"
 by (blast intro: cardinal_cong cardinal_eqE)
 
 lemma cardinal_disjoint_Un:
@@ -33,7 +33,7 @@
       ==> |A \<union> C| = |B \<union> D|"
 by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
 
-lemma lepoll_imp_Card_le: "A lepoll B ==> |A| \<le> |B|"
+lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| \<le> |B|"
 apply (rule AC_well_ord [THEN exE])
 apply (erule well_ord_lepoll_imp_Card_le, assumption)
 done
@@ -59,7 +59,7 @@
 apply (rule well_ord_cadd_cmult_distrib, assumption+)
 done
 
-lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
+lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \<approx> A"
 apply (rule AC_well_ord [THEN exE])
 apply (erule well_ord_InfCard_square_eq, assumption)
 done
@@ -67,36 +67,50 @@
 
 subsection {*The relationship between cardinality and le-pollence*}
 
-lemma Card_le_imp_lepoll: "|A| \<le> |B| ==> A lepoll B"
-apply (rule cardinal_eqpoll
-              [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])
-apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])
-apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
-done
+lemma Card_le_imp_lepoll:
+  assumes "|A| \<le> |B|" shows "A \<lesssim> B"
+proof -
+  have "A \<approx> |A|" 
+    by (rule cardinal_eqpoll [THEN eqpoll_sym])
+  also have "... \<lesssim> |B|"
+    by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)
+  also have "... \<approx> B" 
+    by (rule cardinal_eqpoll)
+  finally show ?thesis .
+qed
 
-lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A lepoll K"
+lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
 apply (erule Card_cardinal_eq [THEN subst], rule iffI,
        erule Card_le_imp_lepoll)
 apply (erule lepoll_imp_Card_le)
 done
 
-lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0";
+lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
 apply auto
 apply (drule cardinal_0 [THEN ssubst])
 apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
 done
 
-lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| \<longleftrightarrow> i lesspoll A"
-apply (cut_tac A = "A" in cardinal_eqpoll)
-apply (auto simp add: eqpoll_iff)
-apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
-apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2
-             simp add: cardinal_idem)
-done
+lemma cardinal_lt_iff_lesspoll:
+  assumes i: "Ord(i)" shows "i < |A| \<longleftrightarrow> i \<prec> A"
+proof
+  assume "i < |A|"
+  hence  "i \<prec> |A|" 
+    by (blast intro: lt_Card_imp_lesspoll Card_cardinal) 
+  also have "...  \<approx> A" 
+    by (rule cardinal_eqpoll)
+  finally show "i \<prec> A" .
+next
+  assume "i \<prec> A"
+  also have "...  \<approx> |A|" 
+    by (blast intro: cardinal_eqpoll eqpoll_sym) 
+  finally have "i \<prec> |A|" .
+  thus  "i < |A|" using i
+    by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
+qed
 
 lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
-apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
-done
+  by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
 
 
 subsection{*Other Applications of AC*}
@@ -164,15 +178,21 @@
     set need not be a cardinal.  Surprisingly complicated proof!
 **)
 
-(*Work backwards along the injection from W into K, given that @{term"W\<noteq>0"}.*)
+text{*Work backwards along the injection from @{term W} into @{term K}, given that @{term"W\<noteq>0"}.*}
+
 lemma inj_UN_subset:
-     "[| f: inj(A,B);  a:A |] ==>
-      (\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
-apply (rule UN_least)
-apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
- apply (simp add: inj_is_fun [THEN apply_rangeI])
-apply (blast intro: inj_is_fun [THEN apply_type])
-done
+  assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
+  shows "(\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))"
+proof (rule UN_least)
+  fix x
+  assume x: "x \<in> A"
+  hence fx: "f ` x \<in> B" by (blast intro: f inj_is_fun [THEN apply_type])
+  have "C(x) \<subseteq> C(if f ` x \<in> range(f) then converse(f) ` (f ` x) else a)" 
+    using f x by (simp add: inj_is_fun [THEN apply_rangeI])
+  also have "... \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f) ` y else a))"
+    by (rule UN_upper [OF fx]) 
+  finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
+qed
 
 (*Simpler to require |W|=K; we'd have a bijection; but the theorem would
   be weaker.*)
diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Nat_ZF.thy
--- a/src/ZF/Nat_ZF.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Nat_ZF.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -92,7 +92,7 @@
 
 lemma natE:
  assumes "n \<in> nat"
- obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
+ obtains ("0") "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
 using assms
 by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
 
diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Ordinal.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -703,7 +703,7 @@
 
 lemma Ord_cases:
  assumes i: "Ord(i)"
- obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
+ obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
 by (insert Ord_cases_disj [OF i], auto)
 
 lemma trans_induct3_raw:
diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/UNITY/AllocBase.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -342,7 +342,7 @@
 apply (simp add: length_nat_list_inj)
 done
 
-lemma nat_lepoll_var: "nat lepoll var"
+lemma nat_lepoll_var: "nat \<lesssim> var"
 apply (unfold lepoll_def)
 apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
 apply (rule var_infinite_lemma)