--- 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) |]