# HG changeset patch
# User paulson
# Date 1332335140 0
# Node ID 2884ee1ffbf0791f9d4d2384a7e69267f515ab76
# Parent  8e1b14bf01905646f20c8dd47a677b33d2a4c3e9
More structured proofs for infinite cardinalities

diff -r 8e1b14bf0190 -r 2884ee1ffbf0 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/ZF/Cardinal_AC.thy	Wed Mar 21 13:05:40 2012 +0000
@@ -173,14 +173,14 @@
 
 text{*The same again, using @{term csucc}*}
 lemma cardinal_UN_lt_csucc:
-     "[| InfCard(K);  \<forall>i\<in>K. |X(i)| < csucc(K) |]
+     "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> |X(i)| < csucc(K) |]
       ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
 by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
 
 text{*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
   the least ordinal j such that i:Vfrom(A,j). *}
 lemma cardinal_UN_Ord_lt_csucc:
-     "[| InfCard(K);  \<forall>i\<in>K. j(i) < csucc(K) |]
+     "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> j(i) < csucc(K) |]
       ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
 apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
 apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
@@ -189,11 +189,11 @@
 done
 
 
-(** Main result for infinite-branching datatypes.  As above, but the index
-    set need not be a cardinal.  Surprisingly complicated proof!
-**)
+subsection{*The Main Result for Infinite-Branching Datatypes*}
 
-text{*Work backwards along the injection from @{term W} into @{term K}, given that @{term"W\<noteq>0"}.*}
+text{*As above, but the index set need not be a cardinal. Work
+backwards along the injection from @{term W} into @{term K}, given
+that @{term"W\<noteq>0"}.*}
 
 lemma inj_UN_subset:
   assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
@@ -209,20 +209,35 @@
   finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
 qed
 
-text{*Simpler to require |W|=K; we'd have a bijection; but the theorem would
-  be weaker.*}
-lemma le_UN_Ord_lt_csucc:
-     "[| InfCard(K);  |W| \<le> K;  \<forall>w\<in>W. j(w) < csucc(K) |]
-      ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
-apply (case_tac "W=0") --{*solve the easy 0 case*}
- apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]
-                  Card_is_Ord Ord_0_lt_csucc)
-apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
-apply (safe intro!: equalityI)
-apply (erule swap)
-apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
- apply (simp add: inj_converse_fun [THEN apply_type])
-apply (blast intro!: Ord_UN elim: ltE)
-done
+theorem le_UN_Ord_lt_csucc:
+  assumes IK: "InfCard(K)" and WK: "|W| \<le> K" and j: "\<And>w. w\<in>W \<Longrightarrow> j(w) < csucc(K)"
+  shows "(\<Union>w\<in>W. j(w)) < csucc(K)"
+proof -
+  have CK: "Card(K)" 
+    by (simp add: InfCard_is_Card IK)
+  then obtain f where f: "f \<in> inj(W, K)" using WK
+    by(auto simp add: le_Card_iff lepoll_def)
+  have OU: "Ord(\<Union>w\<in>W. j(w))" using j
+    by (blast elim: ltE)
+  note lt_subset_trans [OF _ _ OU, trans]
+  show ?thesis
+    proof (cases "W=0")
+      case True  --{*solve the easy 0 case*}
+      thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
+    next
+      case False
+        then obtain x where x: "x \<in> W" by blast
+        have "(\<Union>x\<in>W. j(x)) \<subseteq> (\<Union>k\<in>K. j(if k \<in> range(f) then converse(f) ` k else x))"
+          by (rule inj_UN_subset [OF f x]) 
+        also have "... < csucc(K)" using IK
+          proof (rule cardinal_UN_Ord_lt_csucc)
+            fix k
+            assume "k \<in> K"
+            thus "j(if k \<in> range(f) then converse(f) ` k else x) < csucc(K)" using f x j
+              by (simp add: inj_converse_fun [THEN apply_type])
+          qed
+        finally show ?thesis .
+    qed
+qed
 
 end
diff -r 8e1b14bf0190 -r 2884ee1ffbf0 src/ZF/InfDatatype.thy
--- a/src/ZF/InfDatatype.thy	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/ZF/InfDatatype.thy	Wed Mar 21 13:05:40 2012 +0000
@@ -11,21 +11,38 @@
     Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]
 
 lemma fun_Vcsucc_lemma:
-     "[| f: D -> Vfrom(A,csucc(K));  |D| \<le> K;  InfCard(K) |]
-      ==> \<exists>j. f: D -> Vfrom(A,j) & j < csucc(K)"
-apply (rule_tac x = "\<Union>d\<in>D. LEAST i. f`d \<in> Vfrom (A,i) " in exI)
-apply (rule conjI)
-apply (rule_tac [2] le_UN_Ord_lt_csucc)
-apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all)
- prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
-apply (rule Pi_type)
-apply (rename_tac [2] d)
-apply (erule_tac [2] fun_Limit_VfromE, simp_all)
-apply (subgoal_tac "f`d \<in> Vfrom (A, LEAST i. f`d \<in> Vfrom (A,i))")
- apply (erule Vfrom_mono [OF subset_refl UN_upper, THEN subsetD])
- apply assumption
-apply (fast elim: LeastI ltE)
-done
+  assumes f: "f \<in> D -> Vfrom(A,csucc(K))" and DK: "|D| \<le> K" and ICK: "InfCard(K)"
+  shows "\<exists>j. f \<in> D -> Vfrom(A,j) & j < csucc(K)"
+proof (rule exI, rule conjI)
+  show "f \<in> D \<rightarrow> Vfrom(A, \<Union>z\<in>D. \<mu> i. f`z \<in> Vfrom (A,i))"
+    proof (rule Pi_type [OF f])
+      fix d
+      assume d: "d \<in> D"
+      show "f ` d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))"
+        proof (rule fun_Limit_VfromE [OF f d ICK]) 
+          fix x
+          assume "x < csucc(K)"  "f ` d \<in> Vfrom(A, x)"
+          hence "f`d \<in> Vfrom(A, \<mu> i. f`d \<in> Vfrom (A,i))" using d
+            by (fast elim: LeastI ltE)
+          also have "... \<subseteq> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" 
+            by (rule Vfrom_mono) (auto intro: d) 
+          finally show "f`d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" .
+        qed
+    qed
+next
+  show "(\<Union>d\<in>D. \<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
+    proof (rule le_UN_Ord_lt_csucc [OF ICK DK])
+      fix d
+      assume d: "d \<in> D"
+      show "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
+        proof (rule fun_Limit_VfromE [OF f d ICK]) 
+          fix x
+          assume "x < csucc(K)"  "f ` d \<in> Vfrom(A, x)"
+          thus "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
+            by (blast intro: Least_le lt_trans1 lt_Ord) 
+        qed
+    qed
+qed
 
 lemma subset_Vcsucc:
      "[| D \<subseteq> Vfrom(A,csucc(K));  |D| \<le> K;  InfCard(K) |]