src/ZF/Constructible/Formula.thy
 changeset 13651 ac80e101306a parent 13647 7f6f0ffc45c3 child 13687 22dce9134953
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Thu Oct 17 10:52:59 2002 +0200
1.2 +++ b/src/ZF/Constructible/Formula.thy	Thu Oct 17 10:54:11 2002 +0200
1.3 @@ -453,9 +453,9 @@
1.4  apply (simp add: DPow_def, blast)
1.5  done
1.6
1.7 -lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
1.8 +lemma singleton_in_DPow: "a \<in> A ==> {a} \<in> DPow(A)"
1.10 -apply (rule_tac x="Cons(x,Nil)" in bexI)
1.11 +apply (rule_tac x="Cons(a,Nil)" in bexI)
1.12   apply (rule_tac x="Equal(0,1)" in bexI)
1.13    apply typecheck
1.14  apply (force simp add: succ_Un_distrib [symmetric])
1.15 @@ -473,16 +473,16 @@
1.16  apply (blast intro: cons_in_DPow)
1.17  done
1.18
1.19 -(*DPow is not monotonic.  For example, let A be some non-constructible set
1.20 -  of natural numbers, and let B be nat.  Then A<=B and obviously A : DPow(A)
1.21 -  but A ~: DPow(B).*)
1.22 -lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
1.23 -apply (simp add: DPow_def, auto)
1.24 -(*must use the formula defining A in B to relativize the new formula...*)
1.25 +text{*@{term DPow} is not monotonic.  For example, let @{term A} be some
1.26 +non-constructible set of natural numbers, and let @{term B} be @{term nat}.
1.27 +Then @{term "A<=B"} and obviously @{term "A : DPow(A)"} but @{term "A ~:
1.28 +DPow(B)"}.*}
1.29 +
1.30 +(*This may be true but the proof looks difficult, requiring relativization
1.31 +lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
1.32 +apply (rule equalityI, safe)
1.33  oops
1.34 -
1.35 -lemma DPow_0: "DPow(0) = {0}"
1.36 -by (blast intro: empty_in_DPow dest: DPow_imp_subset)
1.37 +*)
1.38
1.39  lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)"
1.40  by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
1.41 @@ -493,14 +493,16 @@
1.42  apply (erule Finite_Pow_subset_Pow)
1.43  done
1.44
1.45 -(*This may be true but the proof looks difficult, requiring relativization
1.46 -lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
1.47 -apply (rule equalityI, safe)
1.48 -oops
1.49 -*)
1.50 +
1.51 +subsection{*Internalized Formulas for the Ordinals*}
1.52
1.53 -
1.54 -subsection{*Internalized formulas for basic concepts*}
1.55 +text{*The @{text sats} theorems below differ from the usual form in that they
1.56 +include an element of absoluteness.  That is, they relate internalized
1.57 +formulas to real concepts such as the subset relation, rather than to the
1.58 +relativized concepts defined in theory @{text Relative}.  This lets us prove
1.59 +the theorem as @{text Ords_in_DPow} without first having to instantiate the
1.60 +locale @{text M_trivial}.  Note that the present theory does not even take
1.61 +@{text Relative} as a parent.*}
1.62
1.63  subsubsection{*The subset relation*}
1.64
1.65 @@ -563,12 +565,25 @@
1.66  apply (blast intro: nth_type)
1.67  done
1.68
1.69 +text{*The subset consisting of the ordinals is definable.  Essential lemma for
1.70 +@{text Ord_in_Lset}.  This result is the objective of the present subsection.*}
1.71 +theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
1.72 +apply (simp add: DPow_def Collect_subset)
1.73 +apply (rule_tac x=Nil in bexI)
1.74 + apply (rule_tac x="ordinal_fm(0)" in bexI)
1.76 +done
1.77 +
1.78
1.79  subsection{* Constant Lset: Levels of the Constructible Universe *}
1.80
1.81 -constdefs Lset :: "i=>i"
1.82 +constdefs
1.83 +  Lset :: "i=>i"
1.84      "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
1.85
1.86 +  L :: "i=>o" --{*Kunen's definition VI 1.5, page 167*}
1.87 +    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
1.88 +
1.89  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
1.90  lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
1.91  by (subst Lset_def [THEN def_transrec], simp)
1.92 @@ -601,7 +616,7 @@
1.93  apply (blast intro: elem_subset_in_DPow dest: DPowD)
1.94  done
1.95
1.96 -text{*Kunen's VI, 1.6 (a)*}
1.97 +text{*Kunen's VI 1.6 (a)*}
1.98  lemma Transset_Lset: "Transset(Lset(i))"
1.99  apply (rule_tac a=i in eps_induct)
1.100  apply (subst Lset)
1.101 @@ -615,7 +630,7 @@
1.102
1.103  subsubsection{* Monotonicity *}
1.104
1.105 -text{*Kunen's VI, 1.6 (b)*}
1.106 +text{*Kunen's VI 1.6 (b)*}
1.107  lemma Lset_mono [rule_format]:
1.108       "ALL j. i<=j --> Lset(i) <= Lset(j)"
1.109  apply (rule_tac a=i in eps_induct)
1.110 @@ -638,7 +653,7 @@
1.111  lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
1.112  by (blast dest: ltD [THEN Lset_mono_mem])
1.113
1.114 -subsubsection{* 0, successor and limit equations fof Lset *}
1.115 +subsubsection{* 0, successor and limit equations for Lset *}
1.116
1.117  lemma Lset_0 [simp]: "Lset(0) = 0"
1.118  by (subst Lset, blast)
1.119 @@ -705,15 +720,7 @@
1.120  done
1.121
1.122
1.123 -subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
1.124 -
1.125 -text{*The subset consisting of the ordinals is definable.*}
1.126 -lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
1.127 -apply (simp add: DPow_def Collect_subset)
1.128 -apply (rule_tac x=Nil in bexI)
1.129 - apply (rule_tac x="ordinal_fm(0)" in bexI)
1.131 -done
1.132 +subsection{*Constructible Ordinals: Kunen's VI 1.9 (b)*}
1.133
1.134  lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
1.135  apply (erule trans_induct3)
1.136 @@ -744,6 +751,9 @@
1.137         rule Ords_in_DPow [OF Transset_Lset])
1.138  done
1.139
1.140 +lemma Ord_in_L: "Ord(i) ==> L(i)"
1.141 +by (simp add: L_def, blast intro: Ord_in_Lset)
1.142 +
1.143  subsubsection{* Unions *}
1.144
1.145  lemma Union_in_Lset:
1.146 @@ -765,6 +775,12 @@
1.147  apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
1.148  done
1.149
1.150 +theorem Union_in_L: "L(X) ==> L(Union(X))"
1.151 +apply (simp add: L_def, clarify)
1.152 +apply (drule Ord_imp_greater_Limit)
1.153 +apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)
1.154 +done
1.155 +
1.156  subsubsection{* Finite sets and ordered pairs *}
1.157
1.158  lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
1.159 @@ -780,13 +796,6 @@
1.160  apply (blast intro: doubleton_in_Lset)
1.161  done
1.162
1.163 -lemma singleton_in_LLimit:
1.164 -    "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
1.165 -apply (erule Limit_LsetE, assumption)
1.166 -apply (erule singleton_in_Lset [THEN lt_LsetI])
1.167 -apply (blast intro: Limit_has_succ)
1.168 -done
1.169 -
1.170  lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
1.171  lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
1.172
1.173 @@ -799,6 +808,12 @@
1.174                      Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
1.175  done
1.176
1.177 +theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
1.178 +apply (simp add: L_def, clarify)
1.179 +apply (drule Ord2_imp_greater_Limit, assumption)
1.180 +apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
1.181 +done
1.182 +
1.183  lemma Pair_in_LLimit:
1.184      "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> : Lset(i)"
1.185  txt{*Infer that a, b occur at ordinals x,xa < i.*}
1.186 @@ -809,49 +824,11 @@
1.187                      Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
1.188  done
1.189
1.190 -lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
1.191 -by (blast intro: Pair_in_LLimit)
1.192 -
1.193 -lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
1.194 -
1.195 -lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
1.196 -by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
1.197 -
1.198 -lemma nat_into_LLimit: "[| n: nat;  Limit(i) |] ==> n : Lset(i)"
1.199 -by (blast intro: nat_subset_LLimit [THEN subsetD])
1.200
1.201
1.202 -subsubsection{* Closure under disjoint union *}
1.203 -
1.204 -lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
1.205 -
1.206 -lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
1.207 -by (blast intro: nat_into_LLimit)
1.208 -
1.209 -lemma Inl_in_LLimit:
1.210 -    "[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
1.211 -apply (unfold Inl_def)
1.212 -apply (blast intro: zero_in_LLimit Pair_in_LLimit)
1.213 -done
1.214 -
1.215 -lemma Inr_in_LLimit:
1.216 -    "[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
1.217 -apply (unfold Inr_def)
1.218 -apply (blast intro: one_in_LLimit Pair_in_LLimit)
1.219 -done
1.220 -
1.221 -lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
1.222 -by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
1.223 -
1.224 -lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
1.225 -
1.226 -
1.227 -text{*The constructible universe and its rank function*}
1.228 +text{*The rank function for the constructible universe*}
1.229  constdefs
1.230 -  L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
1.231 -    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
1.232 -
1.233 -  lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
1.234 +  lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
1.235      "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
1.236
1.237  lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
1.238 @@ -872,8 +849,9 @@
1.239  apply (blast intro: ltI Limit_is_Ord lt_trans)
1.240  done
1.241
1.242 -text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
1.243 -would suggest.  For a start it need the previous lemma, proved by induction.*}
1.244 +text{*Kunen's VI 1.8.  The proof is much harder than the text would
1.245 +suggest.  For a start, it needs the previous lemma, which is proved by
1.246 +induction.*}
1.247  lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
1.248  apply (simp add: L_def, auto)
1.249   apply (blast intro: Lset_lrank_lt)
1.250 @@ -886,7 +864,7 @@
1.251  lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
1.253
1.254 -text{*Kunen's VI, 1.9 (a)*}
1.255 +text{*Kunen's VI 1.9 (a)*}
1.256  lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
1.257  apply (unfold lrank_def)
1.258  apply (rule Least_equality)
1.259 @@ -897,13 +875,10 @@
1.260  done
1.261
1.262
1.263 -lemma Ord_in_L: "Ord(i) ==> L(i)"
1.264 -by (blast intro: Ord_in_Lset L_I)
1.265 -
1.266  text{*This is lrank(lrank(a)) = lrank(a) *}
1.267  declare Ord_lrank [THEN lrank_of_Ord, simp]
1.268
1.269 -text{*Kunen's VI, 1.10 *}
1.270 +text{*Kunen's VI 1.10 *}
1.271  lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
1.272  apply (simp add: Lset_succ DPow_def)
1.273  apply (rule_tac x=Nil in bexI)
1.274 @@ -922,7 +897,7 @@
1.275  apply (blast intro!: le_imp_subset Lset_mono)
1.276  done
1.277
1.278 -text{*Kunen's VI, 1.11 *}
1.279 +text{*Kunen's VI 1.11 *}
1.280  lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
1.281  apply (erule trans_induct)
1.282  apply (subst Lset)
1.283 @@ -932,7 +907,7 @@
1.284  apply (rule Pow_mono, blast)
1.285  done
1.286
1.287 -text{*Kunen's VI, 1.12 *}
1.288 +text{*Kunen's VI 1.12 *}
1.289  lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
1.290  apply (erule nat_induct)
1.292 @@ -950,21 +925,7 @@
1.293        ==> P"
1.294  by (blast dest: subset_Lset)
1.295
1.296 -subsection{*For L to satisfy the ZF axioms*}
1.297 -
1.298 -theorem Union_in_L: "L(X) ==> L(Union(X))"
1.299 -apply (simp add: L_def, clarify)
1.300 -apply (drule Ord_imp_greater_Limit)
1.301 -apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)
1.302 -done
1.303 -
1.304 -theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
1.305 -apply (simp add: L_def, clarify)
1.306 -apply (drule Ord2_imp_greater_Limit, assumption)
1.307 -apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
1.308 -done
1.309 -
1.310 -subsubsection{*For L to satisfy Powerset *}
1.311 +subsubsection{*For L to satisfy the Powerset axiom *}
1.312
1.313  lemma LPow_env_typing:
1.314      "[| y : Lset(i); Ord(i); y \<subseteq> X |]
1.315 @@ -996,7 +957,6 @@
1.316
1.317  subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
1.318
1.319 -
1.320  lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
1.321  by (induct_tac n, auto)
1.322
1.323 @@ -1046,7 +1006,7 @@
1.324  lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
1.325  apply (drule Transset_0_disj)
1.326  apply (erule disjE)
1.327 - apply (simp add: DPow'_0 DPow_0)
1.328 + apply (simp add: DPow'_0 Finite_DPow_eq_Pow)
1.329  apply (rule equalityI)
1.330   apply (rule DPow_subset_DPow')
1.331  apply (erule DPow'_subset_DPow)
```