author paulson Wed, 21 Mar 2012 13:05:40 +0000 changeset 47071 2884ee1ffbf0 parent 47059 8e1b14bf0190 child 47072 777549486d44
More structured proofs for infinite cardinalities
 src/ZF/Cardinal_AC.thy file | annotate | diff | comparison | revisions src/ZF/InfDatatype.thy file | annotate | diff | comparison | revisions
```--- 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```
```--- 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) |]```