src/ZF/Univ.thy
 author wenzelm Tue Sep 01 22:32:58 2015 +0200 (2015-09-01) changeset 61076 bdc1e2f0a86a parent 60770 240563fbf41d child 61798 27f3c10b0b50 permissions -rw-r--r--
eliminated \<Colon>;
 wenzelm@32960 ` 1` ```(* Title: ZF/Univ.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 3` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 4` wenzelm@32960 ` 5` ```Standard notation for Vset(i) is V(i), but users might want V for a ``` wenzelm@32960 ` 6` ```variable. ``` lcp@516 ` 7` lcp@516 ` 8` ```NOTE: univ(A) could be a translation; would simplify many proofs! ``` wenzelm@6093 ` 9` ``` But Ind_Syntax.univ refers to the constant "Univ.univ" ``` clasohm@0 ` 10` ```*) ``` clasohm@0 ` 11` wenzelm@60770 ` 12` ```section\The Cumulative Hierarchy and a Small Universe for Recursive Types\ ``` paulson@13356 ` 13` haftmann@16417 ` 14` ```theory Univ imports Epsilon Cardinal begin ``` wenzelm@3923 ` 15` wenzelm@24893 ` 16` ```definition ``` wenzelm@24893 ` 17` ``` Vfrom :: "[i,i]=>i" where ``` paulson@46820 ` 18` ``` "Vfrom(A,i) == transrec(i, %x f. A \ (\y\x. Pow(f`y)))" ``` clasohm@0 ` 19` wenzelm@24892 ` 20` ```abbreviation ``` wenzelm@24892 ` 21` ``` Vset :: "i=>i" where ``` wenzelm@24892 ` 22` ``` "Vset(x) == Vfrom(0,x)" ``` clasohm@0 ` 23` wenzelm@3923 ` 24` wenzelm@24893 ` 25` ```definition ``` wenzelm@24893 ` 26` ``` Vrec :: "[i, [i,i]=>i] =>i" where ``` paulson@46820 ` 27` ``` "Vrec(a,H) == transrec(rank(a), %x g. \z\Vset(succ(x)). ``` paulson@46820 ` 28` ``` H(z, \w\Vset(x). g`rank(w)`w)) ` a" ``` paulson@13163 ` 29` wenzelm@24893 ` 30` ```definition ``` wenzelm@24893 ` 31` ``` Vrecursor :: "[[i,i]=>i, i] =>i" where ``` paulson@46820 ` 32` ``` "Vrecursor(H,a) == transrec(rank(a), %x g. \z\Vset(succ(x)). ``` paulson@46820 ` 33` ``` H(\w\Vset(x). g`rank(w)`w, z)) ` a" ``` paulson@13163 ` 34` wenzelm@24893 ` 35` ```definition ``` wenzelm@24893 ` 36` ``` univ :: "i=>i" where ``` paulson@13163 ` 37` ``` "univ(A) == Vfrom(A,nat)" ``` paulson@13163 ` 38` paulson@13163 ` 39` wenzelm@60770 ` 40` ```subsection\Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}\ ``` paulson@13356 ` 41` wenzelm@60770 ` 42` ```text\NOT SUITABLE FOR REWRITING -- RECURSIVE!\ ``` paulson@46820 ` 43` ```lemma Vfrom: "Vfrom(A,i) = A \ (\j\i. Pow(Vfrom(A,j)))" ``` paulson@13269 ` 44` ```by (subst Vfrom_def [THEN def_transrec], simp) ``` paulson@13163 ` 45` wenzelm@60770 ` 46` ```subsubsection\Monotonicity\ ``` paulson@13163 ` 47` paulson@13163 ` 48` ```lemma Vfrom_mono [rule_format]: ``` paulson@46820 ` 49` ``` "A<=B ==> \j. i<=j \ Vfrom(A,i) \ Vfrom(B,j)" ``` paulson@13163 ` 50` ```apply (rule_tac a=i in eps_induct) ``` paulson@13163 ` 51` ```apply (rule impI [THEN allI]) ``` paulson@15481 ` 52` ```apply (subst Vfrom [of A]) ``` paulson@15481 ` 53` ```apply (subst Vfrom [of B]) ``` paulson@13163 ` 54` ```apply (erule Un_mono) ``` paulson@46820 ` 55` ```apply (erule UN_mono, blast) ``` paulson@13163 ` 56` ```done ``` paulson@13163 ` 57` paulson@13220 ` 58` ```lemma VfromI: "[| a \ Vfrom(A,j); j a \ Vfrom(A,i)" ``` paulson@46820 ` 59` ```by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) ``` paulson@13203 ` 60` paulson@13163 ` 61` wenzelm@60770 ` 62` ```subsubsection\A fundamental equality: Vfrom does not require ordinals!\ ``` paulson@13163 ` 63` paulson@15481 ` 64` paulson@15481 ` 65` paulson@46820 ` 66` ```lemma Vfrom_rank_subset1: "Vfrom(A,x) \ Vfrom(A,rank(x))" ``` paulson@15481 ` 67` ```proof (induct x rule: eps_induct) ``` paulson@15481 ` 68` ``` fix x ``` paulson@15481 ` 69` ``` assume "\y\x. Vfrom(A,y) \ Vfrom(A,rank(y))" ``` paulson@15481 ` 70` ``` thus "Vfrom(A, x) \ Vfrom(A, rank(x))" ``` paulson@15481 ` 71` ``` by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"], ``` paulson@15481 ` 72` ``` blast intro!: rank_lt [THEN ltD]) ``` paulson@15481 ` 73` ```qed ``` paulson@13163 ` 74` paulson@46820 ` 75` ```lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) \ Vfrom(A,x)" ``` paulson@13163 ` 76` ```apply (rule_tac a=x in eps_induct) ``` paulson@13163 ` 77` ```apply (subst Vfrom) ``` paulson@15481 ` 78` ```apply (subst Vfrom, rule subset_refl [THEN Un_mono]) ``` paulson@13163 ` 79` ```apply (rule UN_least) ``` wenzelm@60770 ` 80` ```txt\expand @{text "rank(x1) = (\y\x1. succ(rank(y)))"} in assumptions\ ``` paulson@13163 ` 81` ```apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E]) ``` paulson@13163 ` 82` ```apply (rule subset_trans) ``` paulson@13163 ` 83` ```apply (erule_tac [2] UN_upper) ``` paulson@13163 ` 84` ```apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono]) ``` paulson@13163 ` 85` ```apply (erule ltI [THEN le_imp_subset]) ``` paulson@13163 ` 86` ```apply (rule Ord_rank [THEN Ord_succ]) ``` paulson@13163 ` 87` ```apply (erule bspec, assumption) ``` paulson@13163 ` 88` ```done ``` paulson@13163 ` 89` paulson@13163 ` 90` ```lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)" ``` paulson@13163 ` 91` ```apply (rule equalityI) ``` paulson@13163 ` 92` ```apply (rule Vfrom_rank_subset2) ``` paulson@13163 ` 93` ```apply (rule Vfrom_rank_subset1) ``` paulson@13163 ` 94` ```done ``` paulson@13163 ` 95` paulson@13163 ` 96` wenzelm@60770 ` 97` ```subsection\Basic Closure Properties\ ``` paulson@13163 ` 98` paulson@13220 ` 99` ```lemma zero_in_Vfrom: "y:x ==> 0 \ Vfrom(A,x)" ``` paulson@13163 ` 100` ```by (subst Vfrom, blast) ``` paulson@13163 ` 101` paulson@46820 ` 102` ```lemma i_subset_Vfrom: "i \ Vfrom(A,i)" ``` paulson@13163 ` 103` ```apply (rule_tac a=i in eps_induct) ``` paulson@13163 ` 104` ```apply (subst Vfrom, blast) ``` paulson@13163 ` 105` ```done ``` paulson@13163 ` 106` paulson@46820 ` 107` ```lemma A_subset_Vfrom: "A \ Vfrom(A,i)" ``` paulson@13163 ` 108` ```apply (subst Vfrom) ``` paulson@13163 ` 109` ```apply (rule Un_upper1) ``` paulson@13163 ` 110` ```done ``` paulson@13163 ` 111` paulson@13163 ` 112` ```lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD] ``` paulson@13163 ` 113` paulson@46820 ` 114` ```lemma subset_mem_Vfrom: "a \ Vfrom(A,i) ==> a \ Vfrom(A,succ(i))" ``` paulson@13163 ` 115` ```by (subst Vfrom, blast) ``` paulson@13163 ` 116` wenzelm@60770 ` 117` ```subsubsection\Finite sets and ordered pairs\ ``` paulson@13163 ` 118` paulson@13220 ` 119` ```lemma singleton_in_Vfrom: "a \ Vfrom(A,i) ==> {a} \ Vfrom(A,succ(i))" ``` paulson@13163 ` 120` ```by (rule subset_mem_Vfrom, safe) ``` paulson@13163 ` 121` paulson@13163 ` 122` ```lemma doubleton_in_Vfrom: ``` paulson@13220 ` 123` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i) |] ==> {a,b} \ Vfrom(A,succ(i))" ``` paulson@13163 ` 124` ```by (rule subset_mem_Vfrom, safe) ``` paulson@13163 ` 125` paulson@13163 ` 126` ```lemma Pair_in_Vfrom: ``` paulson@13220 ` 127` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i) |] ==> \ Vfrom(A,succ(succ(i)))" ``` paulson@13163 ` 128` ```apply (unfold Pair_def) ``` paulson@46820 ` 129` ```apply (blast intro: doubleton_in_Vfrom) ``` paulson@13163 ` 130` ```done ``` paulson@13163 ` 131` paulson@46820 ` 132` ```lemma succ_in_Vfrom: "a \ Vfrom(A,i) ==> succ(a) \ Vfrom(A,succ(succ(i)))" ``` paulson@13163 ` 133` ```apply (intro subset_mem_Vfrom succ_subsetI, assumption) ``` paulson@46820 ` 134` ```apply (erule subset_trans) ``` paulson@46820 ` 135` ```apply (rule Vfrom_mono [OF subset_refl subset_succI]) ``` paulson@13163 ` 136` ```done ``` paulson@13163 ` 137` wenzelm@60770 ` 138` ```subsection\0, Successor and Limit Equations for @{term Vfrom}\ ``` paulson@13163 ` 139` paulson@13163 ` 140` ```lemma Vfrom_0: "Vfrom(A,0) = A" ``` paulson@13163 ` 141` ```by (subst Vfrom, blast) ``` paulson@13163 ` 142` paulson@46820 ` 143` ```lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A \ Pow(Vfrom(A,i))" ``` paulson@13163 ` 144` ```apply (rule Vfrom [THEN trans]) ``` paulson@46820 ` 145` ```apply (rule equalityI [THEN subst_context, ``` paulson@13163 ` 146` ``` OF _ succI1 [THEN RepFunI, THEN Union_upper]]) ``` paulson@13163 ` 147` ```apply (rule UN_least) ``` paulson@13163 ` 148` ```apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono]) ``` paulson@13163 ` 149` ```apply (erule ltI [THEN le_imp_subset]) ``` paulson@13163 ` 150` ```apply (erule Ord_succ) ``` paulson@13163 ` 151` ```done ``` paulson@13163 ` 152` paulson@46820 ` 153` ```lemma Vfrom_succ: "Vfrom(A,succ(i)) = A \ Pow(Vfrom(A,i))" ``` paulson@13163 ` 154` ```apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst]) ``` paulson@13784 ` 155` ```apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst]) ``` paulson@13163 ` 156` ```apply (subst rank_succ) ``` paulson@13163 ` 157` ```apply (rule Ord_rank [THEN Vfrom_succ_lemma]) ``` paulson@13163 ` 158` ```done ``` paulson@13163 ` 159` paulson@13163 ` 160` ```(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces ``` paulson@46820 ` 161` ``` the conclusion to be Vfrom(A,\(X)) = A \ (\y\X. Vfrom(A,y)) *) ``` paulson@46820 ` 162` ```lemma Vfrom_Union: "y:X ==> Vfrom(A,\(X)) = (\y\X. Vfrom(A,y))" ``` paulson@13163 ` 163` ```apply (subst Vfrom) ``` paulson@13163 ` 164` ```apply (rule equalityI) ``` wenzelm@60770 ` 165` ```txt\first inclusion\ ``` paulson@13163 ` 166` ```apply (rule Un_least) ``` paulson@13163 ` 167` ```apply (rule A_subset_Vfrom [THEN subset_trans]) ``` paulson@13163 ` 168` ```apply (rule UN_upper, assumption) ``` paulson@13163 ` 169` ```apply (rule UN_least) ``` paulson@13163 ` 170` ```apply (erule UnionE) ``` paulson@13163 ` 171` ```apply (rule subset_trans) ``` paulson@13163 ` 172` ```apply (erule_tac [2] UN_upper, ``` paulson@13163 ` 173` ``` subst Vfrom, erule subset_trans [OF UN_upper Un_upper2]) ``` wenzelm@60770 ` 174` ```txt\opposite inclusion\ ``` paulson@13163 ` 175` ```apply (rule UN_least) ``` paulson@13163 ` 176` ```apply (subst Vfrom, blast) ``` paulson@13163 ` 177` ```done ``` paulson@13163 ` 178` wenzelm@60770 ` 179` ```subsection\@{term Vfrom} applied to Limit Ordinals\ ``` paulson@13163 ` 180` paulson@13163 ` 181` ```(*NB. limit ordinals are non-empty: ``` paulson@46820 ` 182` ``` Vfrom(A,0) = A = A \ (\y\0. Vfrom(A,y)) *) ``` paulson@13163 ` 183` ```lemma Limit_Vfrom_eq: ``` paulson@13220 ` 184` ``` "Limit(i) ==> Vfrom(A,i) = (\y\i. Vfrom(A,y))" ``` paulson@13163 ` 185` ```apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption) ``` paulson@46820 ` 186` ```apply (simp add: Limit_Union_eq) ``` paulson@13163 ` 187` ```done ``` paulson@13163 ` 188` paulson@13163 ` 189` ```lemma Limit_VfromE: ``` paulson@13220 ` 190` ``` "[| a \ Vfrom(A,i); ~R ==> Limit(i); ``` paulson@13220 ` 191` ``` !!x. [| x Vfrom(A,x) |] ==> R ``` paulson@13163 ` 192` ``` |] ==> R" ``` paulson@13163 ` 193` ```apply (rule classical) ``` paulson@13163 ` 194` ```apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) ``` paulson@13203 ` 195` ``` prefer 2 apply assumption ``` paulson@46820 ` 196` ``` apply blast ``` paulson@13203 ` 197` ```apply (blast intro: ltI Limit_is_Ord) ``` paulson@13163 ` 198` ```done ``` paulson@13163 ` 199` paulson@13163 ` 200` ```lemma singleton_in_VLimit: ``` paulson@13220 ` 201` ``` "[| a \ Vfrom(A,i); Limit(i) |] ==> {a} \ Vfrom(A,i)" ``` paulson@13163 ` 202` ```apply (erule Limit_VfromE, assumption) ``` paulson@13203 ` 203` ```apply (erule singleton_in_Vfrom [THEN VfromI]) ``` paulson@46820 ` 204` ```apply (blast intro: Limit_has_succ) ``` paulson@13163 ` 205` ```done ``` paulson@13163 ` 206` paulson@46820 ` 207` ```lemmas Vfrom_UnI1 = ``` wenzelm@45602 ` 208` ``` Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]] ``` paulson@46820 ` 209` ```lemmas Vfrom_UnI2 = ``` wenzelm@45602 ` 210` ``` Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]] ``` paulson@13163 ` 211` wenzelm@60770 ` 212` ```text\Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)\ ``` paulson@13163 ` 213` ```lemma doubleton_in_VLimit: ``` paulson@13220 ` 214` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i); Limit(i) |] ==> {a,b} \ Vfrom(A,i)" ``` paulson@13163 ` 215` ```apply (erule Limit_VfromE, assumption) ``` paulson@13163 ` 216` ```apply (erule Limit_VfromE, assumption) ``` paulson@13203 ` 217` ```apply (blast intro: VfromI [OF doubleton_in_Vfrom] ``` paulson@13163 ` 218` ``` Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) ``` paulson@13163 ` 219` ```done ``` paulson@13163 ` 220` paulson@13163 ` 221` ```lemma Pair_in_VLimit: ``` paulson@13220 ` 222` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i); Limit(i) |] ==> \ Vfrom(A,i)" ``` wenzelm@60770 ` 223` ```txt\Infer that a, b occur at ordinals x,xa < i.\ ``` paulson@13163 ` 224` ```apply (erule Limit_VfromE, assumption) ``` paulson@13163 ` 225` ```apply (erule Limit_VfromE, assumption) ``` wenzelm@60770 ` 226` ```txt\Infer that @{term"succ(succ(x \ xa)) < i"}\ ``` paulson@13203 ` 227` ```apply (blast intro: VfromI [OF Pair_in_Vfrom] ``` paulson@13203 ` 228` ``` Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) ``` paulson@13163 ` 229` ```done ``` paulson@13163 ` 230` paulson@46820 ` 231` ```lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) \ Vfrom(A,i)" ``` paulson@13163 ` 232` ```by (blast intro: Pair_in_VLimit) ``` paulson@13163 ` 233` paulson@13163 ` 234` ```lemmas Sigma_subset_VLimit = ``` paulson@13163 ` 235` ``` subset_trans [OF Sigma_mono product_VLimit] ``` paulson@13163 ` 236` paulson@13163 ` 237` ```lemmas nat_subset_VLimit = ``` paulson@13163 ` 238` ``` subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom] ``` paulson@13163 ` 239` paulson@13220 ` 240` ```lemma nat_into_VLimit: "[| n: nat; Limit(i) |] ==> n \ Vfrom(A,i)" ``` paulson@13163 ` 241` ```by (blast intro: nat_subset_VLimit [THEN subsetD]) ``` paulson@13163 ` 242` wenzelm@60770 ` 243` ```subsubsection\Closure under Disjoint Union\ ``` paulson@13163 ` 244` wenzelm@45602 ` 245` ```lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom] ``` paulson@13163 ` 246` paulson@13220 ` 247` ```lemma one_in_VLimit: "Limit(i) ==> 1 \ Vfrom(A,i)" ``` paulson@13163 ` 248` ```by (blast intro: nat_into_VLimit) ``` paulson@13163 ` 249` paulson@13163 ` 250` ```lemma Inl_in_VLimit: ``` paulson@13220 ` 251` ``` "[| a \ Vfrom(A,i); Limit(i) |] ==> Inl(a) \ Vfrom(A,i)" ``` paulson@13163 ` 252` ```apply (unfold Inl_def) ``` paulson@13163 ` 253` ```apply (blast intro: zero_in_VLimit Pair_in_VLimit) ``` paulson@13163 ` 254` ```done ``` paulson@13163 ` 255` paulson@13163 ` 256` ```lemma Inr_in_VLimit: ``` paulson@13220 ` 257` ``` "[| b \ Vfrom(A,i); Limit(i) |] ==> Inr(b) \ Vfrom(A,i)" ``` paulson@13163 ` 258` ```apply (unfold Inr_def) ``` paulson@13163 ` 259` ```apply (blast intro: one_in_VLimit Pair_in_VLimit) ``` paulson@13163 ` 260` ```done ``` paulson@13163 ` 261` paulson@46820 ` 262` ```lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) \ Vfrom(C,i)" ``` paulson@13163 ` 263` ```by (blast intro!: Inl_in_VLimit Inr_in_VLimit) ``` paulson@13163 ` 264` paulson@13163 ` 265` ```lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit] ``` paulson@13163 ` 266` paulson@13163 ` 267` paulson@13163 ` 268` wenzelm@60770 ` 269` ```subsection\Properties assuming @{term "Transset(A)"}\ ``` paulson@13163 ` 270` paulson@13163 ` 271` ```lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))" ``` paulson@13163 ` 272` ```apply (rule_tac a=i in eps_induct) ``` paulson@13163 ` 273` ```apply (subst Vfrom) ``` paulson@13163 ` 274` ```apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow) ``` paulson@13163 ` 275` ```done ``` paulson@13163 ` 276` paulson@13163 ` 277` ```lemma Transset_Vfrom_succ: ``` paulson@13163 ` 278` ``` "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))" ``` paulson@13163 ` 279` ```apply (rule Vfrom_succ [THEN trans]) ``` paulson@13163 ` 280` ```apply (rule equalityI [OF _ Un_upper2]) ``` paulson@13163 ` 281` ```apply (rule Un_least [OF _ subset_refl]) ``` paulson@13163 ` 282` ```apply (rule A_subset_Vfrom [THEN subset_trans]) ``` paulson@13163 ` 283` ```apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]]) ``` paulson@13163 ` 284` ```done ``` paulson@13163 ` 285` paulson@46820 ` 286` ```lemma Transset_Pair_subset: "[| \ C; Transset(C) |] ==> a: C & b: C" ``` paulson@13163 ` 287` ```by (unfold Pair_def Transset_def, blast) ``` paulson@13163 ` 288` paulson@13163 ` 289` ```lemma Transset_Pair_subset_VLimit: ``` paulson@46820 ` 290` ``` "[| \ Vfrom(A,i); Transset(A); Limit(i) |] ``` paulson@13220 ` 291` ``` ==> \ Vfrom(A,i)" ``` paulson@13163 ` 292` ```apply (erule Transset_Pair_subset [THEN conjE]) ``` paulson@13163 ` 293` ```apply (erule Transset_Vfrom) ``` paulson@13163 ` 294` ```apply (blast intro: Pair_in_VLimit) ``` paulson@13163 ` 295` ```done ``` paulson@13163 ` 296` paulson@13163 ` 297` ```lemma Union_in_Vfrom: ``` paulson@46820 ` 298` ``` "[| X \ Vfrom(A,j); Transset(A) |] ==> \(X) \ Vfrom(A, succ(j))" ``` paulson@13163 ` 299` ```apply (drule Transset_Vfrom) ``` paulson@13163 ` 300` ```apply (rule subset_mem_Vfrom) ``` paulson@13163 ` 301` ```apply (unfold Transset_def, blast) ``` paulson@13163 ` 302` ```done ``` paulson@13163 ` 303` paulson@13163 ` 304` ```lemma Union_in_VLimit: ``` paulson@46820 ` 305` ``` "[| X \ Vfrom(A,i); Limit(i); Transset(A) |] ==> \(X) \ Vfrom(A,i)" ``` paulson@13163 ` 306` ```apply (rule Limit_VfromE, assumption+) ``` paulson@13203 ` 307` ```apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom) ``` paulson@13163 ` 308` ```done ``` paulson@13163 ` 309` paulson@13163 ` 310` paulson@13163 ` 311` ```(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) ``` paulson@13163 ` 312` ``` is a model of simple type theory provided A is a transitive set ``` paulson@13163 ` 313` ``` and i is a limit ordinal ``` paulson@13163 ` 314` ```***) ``` paulson@13163 ` 315` wenzelm@60770 ` 316` ```text\General theorem for membership in Vfrom(A,i) when i is a limit ordinal\ ``` paulson@13163 ` 317` ```lemma in_VLimit: ``` paulson@13220 ` 318` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i); Limit(i); ``` paulson@13220 ` 319` ``` !!x y j. [| j Vfrom(A,j); y \ Vfrom(A,j) |] ``` paulson@46820 ` 320` ``` ==> \k. h(x,y) \ Vfrom(A,k) & k h(a,b) \ Vfrom(A,i)" ``` wenzelm@60770 ` 322` ```txt\Infer that a, b occur at ordinals x,xa < i.\ ``` paulson@13163 ` 323` ```apply (erule Limit_VfromE, assumption) ``` paulson@13163 ` 324` ```apply (erule Limit_VfromE, assumption, atomize) ``` paulson@46820 ` 325` ```apply (drule_tac x=a in spec) ``` paulson@46820 ` 326` ```apply (drule_tac x=b in spec) ``` paulson@46820 ` 327` ```apply (drule_tac x="x \ xa \ 2" in spec) ``` paulson@46820 ` 328` ```apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) ``` paulson@13203 ` 329` ```apply (blast intro: Limit_has_0 Limit_has_succ VfromI) ``` paulson@13163 ` 330` ```done ``` paulson@13163 ` 331` wenzelm@60770 ` 332` ```subsubsection\Products\ ``` paulson@13163 ` 333` paulson@13163 ` 334` ```lemma prod_in_Vfrom: ``` paulson@13220 ` 335` ``` "[| a \ Vfrom(A,j); b \ Vfrom(A,j); Transset(A) |] ``` paulson@13220 ` 336` ``` ==> a*b \ Vfrom(A, succ(succ(succ(j))))" ``` paulson@13163 ` 337` ```apply (drule Transset_Vfrom) ``` paulson@13163 ` 338` ```apply (rule subset_mem_Vfrom) ``` paulson@13163 ` 339` ```apply (unfold Transset_def) ``` paulson@13163 ` 340` ```apply (blast intro: Pair_in_Vfrom) ``` paulson@13163 ` 341` ```done ``` paulson@13163 ` 342` paulson@13163 ` 343` ```lemma prod_in_VLimit: ``` paulson@13220 ` 344` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i); Limit(i); Transset(A) |] ``` paulson@13220 ` 345` ``` ==> a*b \ Vfrom(A,i)" ``` paulson@13163 ` 346` ```apply (erule in_VLimit, assumption+) ``` paulson@13163 ` 347` ```apply (blast intro: prod_in_Vfrom Limit_has_succ) ``` paulson@13163 ` 348` ```done ``` paulson@13163 ` 349` wenzelm@60770 ` 350` ```subsubsection\Disjoint Sums, or Quine Ordered Pairs\ ``` paulson@13163 ` 351` paulson@13163 ` 352` ```lemma sum_in_Vfrom: ``` paulson@13220 ` 353` ``` "[| a \ Vfrom(A,j); b \ Vfrom(A,j); Transset(A); 1:j |] ``` paulson@13220 ` 354` ``` ==> a+b \ Vfrom(A, succ(succ(succ(j))))" ``` paulson@13163 ` 355` ```apply (unfold sum_def) ``` paulson@13163 ` 356` ```apply (drule Transset_Vfrom) ``` paulson@13163 ` 357` ```apply (rule subset_mem_Vfrom) ``` paulson@13163 ` 358` ```apply (unfold Transset_def) ``` paulson@13163 ` 359` ```apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD]) ``` paulson@13163 ` 360` ```done ``` paulson@13163 ` 361` paulson@13163 ` 362` ```lemma sum_in_VLimit: ``` paulson@13220 ` 363` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i); Limit(i); Transset(A) |] ``` paulson@13220 ` 364` ``` ==> a+b \ Vfrom(A,i)" ``` paulson@13163 ` 365` ```apply (erule in_VLimit, assumption+) ``` paulson@13163 ` 366` ```apply (blast intro: sum_in_Vfrom Limit_has_succ) ``` paulson@13163 ` 367` ```done ``` paulson@13163 ` 368` wenzelm@60770 ` 369` ```subsubsection\Function Space!\ ``` paulson@13163 ` 370` paulson@13163 ` 371` ```lemma fun_in_Vfrom: ``` paulson@13220 ` 372` ``` "[| a \ Vfrom(A,j); b \ Vfrom(A,j); Transset(A) |] ==> ``` paulson@13220 ` 373` ``` a->b \ Vfrom(A, succ(succ(succ(succ(j)))))" ``` paulson@13163 ` 374` ```apply (unfold Pi_def) ``` paulson@13163 ` 375` ```apply (drule Transset_Vfrom) ``` paulson@13163 ` 376` ```apply (rule subset_mem_Vfrom) ``` paulson@13163 ` 377` ```apply (rule Collect_subset [THEN subset_trans]) ``` paulson@13163 ` 378` ```apply (subst Vfrom) ``` paulson@13163 ` 379` ```apply (rule subset_trans [THEN subset_trans]) ``` paulson@13163 ` 380` ```apply (rule_tac [3] Un_upper2) ``` paulson@13163 ` 381` ```apply (rule_tac [2] succI1 [THEN UN_upper]) ``` paulson@13163 ` 382` ```apply (rule Pow_mono) ``` paulson@13163 ` 383` ```apply (unfold Transset_def) ``` paulson@13163 ` 384` ```apply (blast intro: Pair_in_Vfrom) ``` paulson@13163 ` 385` ```done ``` paulson@13163 ` 386` paulson@13163 ` 387` ```lemma fun_in_VLimit: ``` paulson@13220 ` 388` ``` "[| a \ Vfrom(A,i); b \ Vfrom(A,i); Limit(i); Transset(A) |] ``` paulson@13220 ` 389` ``` ==> a->b \ Vfrom(A,i)" ``` paulson@13163 ` 390` ```apply (erule in_VLimit, assumption+) ``` paulson@13163 ` 391` ```apply (blast intro: fun_in_Vfrom Limit_has_succ) ``` paulson@13163 ` 392` ```done ``` paulson@13163 ` 393` paulson@13163 ` 394` ```lemma Pow_in_Vfrom: ``` paulson@13220 ` 395` ``` "[| a \ Vfrom(A,j); Transset(A) |] ==> Pow(a) \ Vfrom(A, succ(succ(j)))" ``` paulson@13163 ` 396` ```apply (drule Transset_Vfrom) ``` paulson@13163 ` 397` ```apply (rule subset_mem_Vfrom) ``` paulson@13163 ` 398` ```apply (unfold Transset_def) ``` paulson@13163 ` 399` ```apply (subst Vfrom, blast) ``` paulson@13163 ` 400` ```done ``` paulson@13163 ` 401` paulson@13163 ` 402` ```lemma Pow_in_VLimit: ``` paulson@13220 ` 403` ``` "[| a \ Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) \ Vfrom(A,i)" ``` paulson@13203 ` 404` ```by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI) ``` paulson@13163 ` 405` paulson@13163 ` 406` wenzelm@60770 ` 407` ```subsection\The Set @{term "Vset(i)"}\ ``` paulson@13163 ` 408` paulson@13220 ` 409` ```lemma Vset: "Vset(i) = (\j\i. Pow(Vset(j)))" ``` paulson@13163 ` 410` ```by (subst Vfrom, blast) ``` paulson@13163 ` 411` wenzelm@45602 ` 412` ```lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ] ``` wenzelm@45602 ` 413` ```lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom] ``` paulson@13163 ` 414` wenzelm@60770 ` 415` ```subsubsection\Characterisation of the elements of @{term "Vset(i)"}\ ``` paulson@13163 ` 416` paulson@46820 ` 417` ```lemma VsetD [rule_format]: "Ord(i) ==> \b. b \ Vset(i) \ rank(b) < i" ``` paulson@13163 ` 418` ```apply (erule trans_induct) ``` paulson@13163 ` 419` ```apply (subst Vset, safe) ``` paulson@13163 ` 420` ```apply (subst rank) ``` paulson@46820 ` 421` ```apply (blast intro: ltI UN_succ_least_lt) ``` paulson@13163 ` 422` ```done ``` paulson@13163 ` 423` paulson@13163 ` 424` ```lemma VsetI_lemma [rule_format]: ``` paulson@46820 ` 425` ``` "Ord(i) ==> \b. rank(b) \ i \ b \ Vset(i)" ``` paulson@13163 ` 426` ```apply (erule trans_induct) ``` paulson@13163 ` 427` ```apply (rule allI) ``` paulson@13163 ` 428` ```apply (subst Vset) ``` paulson@13163 ` 429` ```apply (blast intro!: rank_lt [THEN ltD]) ``` paulson@13163 ` 430` ```done ``` paulson@13163 ` 431` paulson@13220 ` 432` ```lemma VsetI: "rank(x) x \ Vset(i)" ``` paulson@13163 ` 433` ```by (blast intro: VsetI_lemma elim: ltE) ``` paulson@13163 ` 434` wenzelm@60770 ` 435` ```text\Merely a lemma for the next result\ ``` paulson@46821 ` 436` ```lemma Vset_Ord_rank_iff: "Ord(i) ==> b \ Vset(i) \ rank(b) < i" ``` paulson@13163 ` 437` ```by (blast intro: VsetD VsetI) ``` paulson@13163 ` 438` paulson@46821 ` 439` ```lemma Vset_rank_iff [simp]: "b \ Vset(a) \ rank(b) < rank(a)" ``` paulson@13163 ` 440` ```apply (rule Vfrom_rank_eq [THEN subst]) ``` paulson@13163 ` 441` ```apply (rule Ord_rank [THEN Vset_Ord_rank_iff]) ``` paulson@13163 ` 442` ```done ``` paulson@13163 ` 443` wenzelm@60770 ` 444` ```text\This is rank(rank(a)) = rank(a)\ ``` paulson@13163 ` 445` ```declare Ord_rank [THEN rank_of_Ord, simp] ``` paulson@13163 ` 446` paulson@13163 ` 447` ```lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i" ``` paulson@13163 ` 448` ```apply (subst rank) ``` paulson@13163 ` 449` ```apply (rule equalityI, safe) ``` paulson@46820 ` 450` ```apply (blast intro: VsetD [THEN ltD]) ``` paulson@46820 ` 451` ```apply (blast intro: VsetD [THEN ltD] Ord_trans) ``` paulson@13163 ` 452` ```apply (blast intro: i_subset_Vfrom [THEN subsetD] ``` paulson@13163 ` 453` ``` Ord_in_Ord [THEN rank_of_Ord, THEN ssubst]) ``` paulson@13163 ` 454` ```done ``` paulson@13163 ` 455` wenzelm@58860 ` 456` ```lemma Finite_Vset: "i \ nat ==> Finite(Vset(i))" ``` paulson@13269 ` 457` ```apply (erule nat_induct) ``` paulson@46820 ` 458` ``` apply (simp add: Vfrom_0) ``` paulson@46820 ` 459` ```apply (simp add: Vset_succ) ``` paulson@13269 ` 460` ```done ``` paulson@13269 ` 461` wenzelm@60770 ` 462` ```subsubsection\Reasoning about Sets in Terms of Their Elements' Ranks\ ``` clasohm@0 ` 463` paulson@46820 ` 464` ```lemma arg_subset_Vset_rank: "a \ Vset(rank(a))" ``` paulson@13163 ` 465` ```apply (rule subsetI) ``` paulson@13163 ` 466` ```apply (erule rank_lt [THEN VsetI]) ``` paulson@13163 ` 467` ```done ``` paulson@13163 ` 468` paulson@13163 ` 469` ```lemma Int_Vset_subset: ``` paulson@46820 ` 470` ``` "[| !!i. Ord(i) ==> a \ Vset(i) \ b |] ==> a \ b" ``` paulson@46820 ` 471` ```apply (rule subset_trans) ``` paulson@13163 ` 472` ```apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank]) ``` paulson@46820 ` 473` ```apply (blast intro: Ord_rank) ``` paulson@13163 ` 474` ```done ``` paulson@13163 ` 475` wenzelm@60770 ` 476` ```subsubsection\Set Up an Environment for Simplification\ ``` paulson@13163 ` 477` paulson@13163 ` 478` ```lemma rank_Inl: "rank(a) < rank(Inl(a))" ``` paulson@13163 ` 479` ```apply (unfold Inl_def) ``` paulson@13163 ` 480` ```apply (rule rank_pair2) ``` paulson@13163 ` 481` ```done ``` paulson@13163 ` 482` paulson@13163 ` 483` ```lemma rank_Inr: "rank(a) < rank(Inr(a))" ``` paulson@13163 ` 484` ```apply (unfold Inr_def) ``` paulson@13163 ` 485` ```apply (rule rank_pair2) ``` paulson@13163 ` 486` ```done ``` paulson@13163 ` 487` paulson@13163 ` 488` ```lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2 ``` paulson@13163 ` 489` wenzelm@60770 ` 490` ```subsubsection\Recursion over Vset Levels!\ ``` paulson@13163 ` 491` wenzelm@60770 ` 492` ```text\NOT SUITABLE FOR REWRITING: recursive!\ ``` paulson@46820 ` 493` ```lemma Vrec: "Vrec(a,H) = H(a, \x\Vset(rank(a)). Vrec(x,H))" ``` paulson@13163 ` 494` ```apply (unfold Vrec_def) ``` paulson@13269 ` 495` ```apply (subst transrec, simp) ``` paulson@13175 ` 496` ```apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def) ``` paulson@13163 ` 497` ```done ``` paulson@13163 ` 498` wenzelm@60770 ` 499` ```text\This form avoids giant explosions in proofs. NOTE USE OF ==\ ``` paulson@13163 ` 500` ```lemma def_Vrec: ``` paulson@13163 ` 501` ``` "[| !!x. h(x)==Vrec(x,H) |] ==> ``` paulson@46820 ` 502` ``` h(a) = H(a, \x\Vset(rank(a)). h(x))" ``` paulson@46820 ` 503` ```apply simp ``` paulson@13163 ` 504` ```apply (rule Vrec) ``` paulson@13163 ` 505` ```done ``` paulson@13163 ` 506` wenzelm@60770 ` 507` ```text\NOT SUITABLE FOR REWRITING: recursive!\ ``` paulson@13163 ` 508` ```lemma Vrecursor: ``` paulson@46820 ` 509` ``` "Vrecursor(H,a) = H(\x\Vset(rank(a)). Vrecursor(H,x), a)" ``` paulson@13163 ` 510` ```apply (unfold Vrecursor_def) ``` paulson@13163 ` 511` ```apply (subst transrec, simp) ``` paulson@13175 ` 512` ```apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def) ``` paulson@13163 ` 513` ```done ``` paulson@13163 ` 514` wenzelm@60770 ` 515` ```text\This form avoids giant explosions in proofs. NOTE USE OF ==\ ``` paulson@13163 ` 516` ```lemma def_Vrecursor: ``` paulson@46820 ` 517` ``` "h == Vrecursor(H) ==> h(a) = H(\x\Vset(rank(a)). h(x), a)" ``` paulson@13163 ` 518` ```apply simp ``` paulson@13163 ` 519` ```apply (rule Vrecursor) ``` paulson@13163 ` 520` ```done ``` paulson@13163 ` 521` paulson@13163 ` 522` wenzelm@60770 ` 523` ```subsection\The Datatype Universe: @{term "univ(A)"}\ ``` paulson@13163 ` 524` paulson@46820 ` 525` ```lemma univ_mono: "A<=B ==> univ(A) \ univ(B)" ``` paulson@13163 ` 526` ```apply (unfold univ_def) ``` paulson@13163 ` 527` ```apply (erule Vfrom_mono) ``` paulson@13163 ` 528` ```apply (rule subset_refl) ``` paulson@13163 ` 529` ```done ``` paulson@13163 ` 530` paulson@13163 ` 531` ```lemma Transset_univ: "Transset(A) ==> Transset(univ(A))" ``` paulson@13163 ` 532` ```apply (unfold univ_def) ``` paulson@13163 ` 533` ```apply (erule Transset_Vfrom) ``` paulson@13163 ` 534` ```done ``` paulson@13163 ` 535` wenzelm@60770 ` 536` ```subsubsection\The Set @{term"univ(A)"} as a Limit\ ``` paulson@13163 ` 537` paulson@13220 ` 538` ```lemma univ_eq_UN: "univ(A) = (\i\nat. Vfrom(A,i))" ``` paulson@13163 ` 539` ```apply (unfold univ_def) ``` paulson@13163 ` 540` ```apply (rule Limit_nat [THEN Limit_Vfrom_eq]) ``` paulson@13163 ` 541` ```done ``` paulson@13163 ` 542` paulson@46820 ` 543` ```lemma subset_univ_eq_Int: "c \ univ(A) ==> c = (\i\nat. c \ Vfrom(A,i))" ``` paulson@13163 ` 544` ```apply (rule subset_UN_iff_eq [THEN iffD1]) ``` paulson@13163 ` 545` ```apply (erule univ_eq_UN [THEN subst]) ``` paulson@13163 ` 546` ```done ``` paulson@13163 ` 547` paulson@13163 ` 548` ```lemma univ_Int_Vfrom_subset: ``` paulson@46820 ` 549` ``` "[| a \ univ(X); ``` paulson@46820 ` 550` ``` !!i. i:nat ==> a \ Vfrom(X,i) \ b |] ``` paulson@46820 ` 551` ``` ==> a \ b" ``` paulson@13163 ` 552` ```apply (subst subset_univ_eq_Int, assumption) ``` paulson@46820 ` 553` ```apply (rule UN_least, simp) ``` paulson@13163 ` 554` ```done ``` paulson@13163 ` 555` paulson@13163 ` 556` ```lemma univ_Int_Vfrom_eq: ``` paulson@46820 ` 557` ``` "[| a \ univ(X); b \ univ(X); ``` paulson@46820 ` 558` ``` !!i. i:nat ==> a \ Vfrom(X,i) = b \ Vfrom(X,i) ``` paulson@13163 ` 559` ``` |] ==> a = b" ``` paulson@13163 ` 560` ```apply (rule equalityI) ``` paulson@13163 ` 561` ```apply (rule univ_Int_Vfrom_subset, assumption) ``` paulson@46820 ` 562` ```apply (blast elim: equalityCE) ``` paulson@13163 ` 563` ```apply (rule univ_Int_Vfrom_subset, assumption) ``` paulson@46820 ` 564` ```apply (blast elim: equalityCE) ``` paulson@13163 ` 565` ```done ``` paulson@13163 ` 566` wenzelm@60770 ` 567` ```subsection\Closure Properties for @{term "univ(A)"}\ ``` paulson@13163 ` 568` paulson@13220 ` 569` ```lemma zero_in_univ: "0 \ univ(A)" ``` paulson@13163 ` 570` ```apply (unfold univ_def) ``` paulson@13163 ` 571` ```apply (rule nat_0I [THEN zero_in_Vfrom]) ``` paulson@13163 ` 572` ```done ``` paulson@13163 ` 573` paulson@46820 ` 574` ```lemma zero_subset_univ: "{0} \ univ(A)" ``` paulson@13255 ` 575` ```by (blast intro: zero_in_univ) ``` paulson@13255 ` 576` paulson@46820 ` 577` ```lemma A_subset_univ: "A \ univ(A)" ``` paulson@13163 ` 578` ```apply (unfold univ_def) ``` paulson@13163 ` 579` ```apply (rule A_subset_Vfrom) ``` paulson@13163 ` 580` ```done ``` paulson@13163 ` 581` wenzelm@45602 ` 582` ```lemmas A_into_univ = A_subset_univ [THEN subsetD] ``` paulson@13163 ` 583` wenzelm@60770 ` 584` ```subsubsection\Closure under Unordered and Ordered Pairs\ ``` paulson@13163 ` 585` paulson@13220 ` 586` ```lemma singleton_in_univ: "a: univ(A) ==> {a} \ univ(A)" ``` paulson@13163 ` 587` ```apply (unfold univ_def) ``` paulson@13163 ` 588` ```apply (blast intro: singleton_in_VLimit Limit_nat) ``` paulson@13163 ` 589` ```done ``` paulson@13163 ` 590` paulson@13163 ` 591` ```lemma doubleton_in_univ: ``` paulson@13220 ` 592` ``` "[| a: univ(A); b: univ(A) |] ==> {a,b} \ univ(A)" ``` paulson@13163 ` 593` ```apply (unfold univ_def) ``` paulson@13163 ` 594` ```apply (blast intro: doubleton_in_VLimit Limit_nat) ``` paulson@13163 ` 595` ```done ``` paulson@13163 ` 596` paulson@13163 ` 597` ```lemma Pair_in_univ: ``` paulson@13220 ` 598` ``` "[| a: univ(A); b: univ(A) |] ==> \ univ(A)" ``` paulson@13163 ` 599` ```apply (unfold univ_def) ``` paulson@13163 ` 600` ```apply (blast intro: Pair_in_VLimit Limit_nat) ``` paulson@13163 ` 601` ```done ``` paulson@13163 ` 602` paulson@13163 ` 603` ```lemma Union_in_univ: ``` paulson@46820 ` 604` ``` "[| X: univ(A); Transset(A) |] ==> \(X) \ univ(A)" ``` paulson@13163 ` 605` ```apply (unfold univ_def) ``` paulson@13163 ` 606` ```apply (blast intro: Union_in_VLimit Limit_nat) ``` paulson@13163 ` 607` ```done ``` paulson@13163 ` 608` paulson@46820 ` 609` ```lemma product_univ: "univ(A)*univ(A) \ univ(A)" ``` paulson@13163 ` 610` ```apply (unfold univ_def) ``` paulson@13163 ` 611` ```apply (rule Limit_nat [THEN product_VLimit]) ``` paulson@13163 ` 612` ```done ``` paulson@13163 ` 613` paulson@13163 ` 614` wenzelm@60770 ` 615` ```subsubsection\The Natural Numbers\ ``` paulson@13163 ` 616` paulson@46820 ` 617` ```lemma nat_subset_univ: "nat \ univ(A)" ``` paulson@13163 ` 618` ```apply (unfold univ_def) ``` paulson@13163 ` 619` ```apply (rule i_subset_Vfrom) ``` paulson@13163 ` 620` ```done ``` paulson@13163 ` 621` wenzelm@60770 ` 622` ```text\n:nat ==> n:univ(A)\ ``` wenzelm@45602 ` 623` ```lemmas nat_into_univ = nat_subset_univ [THEN subsetD] ``` paulson@13163 ` 624` wenzelm@60770 ` 625` ```subsubsection\Instances for 1 and 2\ ``` paulson@13163 ` 626` paulson@13220 ` 627` ```lemma one_in_univ: "1 \ univ(A)" ``` paulson@13163 ` 628` ```apply (unfold univ_def) ``` paulson@13163 ` 629` ```apply (rule Limit_nat [THEN one_in_VLimit]) ``` paulson@13163 ` 630` ```done ``` paulson@13163 ` 631` wenzelm@60770 ` 632` ```text\unused!\ ``` paulson@13220 ` 633` ```lemma two_in_univ: "2 \ univ(A)" ``` paulson@13163 ` 634` ```by (blast intro: nat_into_univ) ``` paulson@13163 ` 635` paulson@46820 ` 636` ```lemma bool_subset_univ: "bool \ univ(A)" ``` paulson@13163 ` 637` ```apply (unfold bool_def) ``` paulson@13163 ` 638` ```apply (blast intro!: zero_in_univ one_in_univ) ``` paulson@13163 ` 639` ```done ``` paulson@13163 ` 640` wenzelm@45602 ` 641` ```lemmas bool_into_univ = bool_subset_univ [THEN subsetD] ``` paulson@13163 ` 642` paulson@13163 ` 643` wenzelm@60770 ` 644` ```subsubsection\Closure under Disjoint Union\ ``` paulson@13163 ` 645` paulson@13220 ` 646` ```lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \ univ(A)" ``` paulson@13163 ` 647` ```apply (unfold univ_def) ``` paulson@13163 ` 648` ```apply (erule Inl_in_VLimit [OF _ Limit_nat]) ``` paulson@13163 ` 649` ```done ``` paulson@13163 ` 650` paulson@13220 ` 651` ```lemma Inr_in_univ: "b: univ(A) ==> Inr(b) \ univ(A)" ``` paulson@13163 ` 652` ```apply (unfold univ_def) ``` paulson@13163 ` 653` ```apply (erule Inr_in_VLimit [OF _ Limit_nat]) ``` paulson@13163 ` 654` ```done ``` paulson@13163 ` 655` paulson@46820 ` 656` ```lemma sum_univ: "univ(C)+univ(C) \ univ(C)" ``` paulson@13163 ` 657` ```apply (unfold univ_def) ``` paulson@13163 ` 658` ```apply (rule Limit_nat [THEN sum_VLimit]) ``` paulson@13163 ` 659` ```done ``` paulson@13163 ` 660` paulson@13163 ` 661` ```lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ] ``` paulson@13163 ` 662` paulson@13255 ` 663` ```lemma Sigma_subset_univ: ``` paulson@13255 ` 664` ``` "[|A \ univ(D); \x. x \ A \ B(x) \ univ(D)|] ==> Sigma(A,B) \ univ(D)" ``` paulson@13255 ` 665` ```apply (simp add: univ_def) ``` paulson@46820 ` 666` ```apply (blast intro: Sigma_subset_VLimit del: subsetI) ``` paulson@13255 ` 667` ```done ``` paulson@13163 ` 668` paulson@13255 ` 669` paulson@13255 ` 670` ```(*Closure under binary union -- use Un_least ``` paulson@13255 ` 671` ``` Closure under Collect -- use Collect_subset [THEN subset_trans] ``` paulson@13255 ` 672` ``` Closure under RepFun -- use RepFun_subset *) ``` paulson@13163 ` 673` paulson@13163 ` 674` wenzelm@60770 ` 675` ```subsection\Finite Branching Closure Properties\ ``` paulson@13163 ` 676` wenzelm@60770 ` 677` ```subsubsection\Closure under Finite Powerset\ ``` paulson@13163 ` 678` paulson@13163 ` 679` ```lemma Fin_Vfrom_lemma: ``` paulson@46820 ` 680` ``` "[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> \j. b \ Vfrom(A,j) & j Fin(Vfrom(A,i)) \ Vfrom(A,i)" ``` paulson@13163 ` 688` ```apply (rule subsetI) ``` paulson@13163 ` 689` ```apply (drule Fin_Vfrom_lemma, safe) ``` paulson@13163 ` 690` ```apply (rule Vfrom [THEN ssubst]) ``` paulson@13163 ` 691` ```apply (blast dest!: ltD) ``` paulson@13163 ` 692` ```done ``` paulson@13163 ` 693` paulson@13163 ` 694` ```lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit] ``` paulson@13163 ` 695` paulson@46820 ` 696` ```lemma Fin_univ: "Fin(univ(A)) \ univ(A)" ``` paulson@13163 ` 697` ```apply (unfold univ_def) ``` paulson@13163 ` 698` ```apply (rule Limit_nat [THEN Fin_VLimit]) ``` paulson@13163 ` 699` ```done ``` paulson@13163 ` 700` wenzelm@60770 ` 701` ```subsubsection\Closure under Finite Powers: Functions from a Natural Number\ ``` paulson@13163 ` 702` paulson@13163 ` 703` ```lemma nat_fun_VLimit: ``` paulson@46820 ` 704` ``` "[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) \ Vfrom(A,i)" ``` paulson@13163 ` 705` ```apply (erule nat_fun_subset_Fin [THEN subset_trans]) ``` paulson@13163 ` 706` ```apply (blast del: subsetI ``` paulson@13163 ` 707` ``` intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit) ``` paulson@13163 ` 708` ```done ``` paulson@13163 ` 709` paulson@13163 ` 710` ```lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit] ``` paulson@13163 ` 711` paulson@46820 ` 712` ```lemma nat_fun_univ: "n: nat ==> n -> univ(A) \ univ(A)" ``` paulson@13163 ` 713` ```apply (unfold univ_def) ``` paulson@13163 ` 714` ```apply (erule nat_fun_VLimit [OF _ Limit_nat]) ``` paulson@13163 ` 715` ```done ``` paulson@13163 ` 716` paulson@13163 ` 717` wenzelm@60770 ` 718` ```subsubsection\Closure under Finite Function Space\ ``` paulson@13163 ` 719` wenzelm@60770 ` 720` ```text\General but seldom-used version; normally the domain is fixed\ ``` paulson@13163 ` 721` ```lemma FiniteFun_VLimit1: ``` paulson@46820 ` 722` ``` "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) \ Vfrom(A,i)" ``` paulson@13163 ` 723` ```apply (rule FiniteFun.dom_subset [THEN subset_trans]) ``` paulson@13163 ` 724` ```apply (blast del: subsetI ``` paulson@13163 ` 725` ``` intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl) ``` paulson@13163 ` 726` ```done ``` paulson@13163 ` 727` paulson@46820 ` 728` ```lemma FiniteFun_univ1: "univ(A) -||> univ(A) \ univ(A)" ``` paulson@13163 ` 729` ```apply (unfold univ_def) ``` paulson@13163 ` 730` ```apply (rule Limit_nat [THEN FiniteFun_VLimit1]) ``` paulson@13163 ` 731` ```done ``` paulson@13163 ` 732` wenzelm@60770 ` 733` ```text\Version for a fixed domain\ ``` paulson@13163 ` 734` ```lemma FiniteFun_VLimit: ``` paulson@46820 ` 735` ``` "[| W \ Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) \ Vfrom(A,i)" ``` paulson@46820 ` 736` ```apply (rule subset_trans) ``` paulson@13163 ` 737` ```apply (erule FiniteFun_mono [OF _ subset_refl]) ``` paulson@13163 ` 738` ```apply (erule FiniteFun_VLimit1) ``` paulson@13163 ` 739` ```done ``` paulson@13163 ` 740` paulson@13163 ` 741` ```lemma FiniteFun_univ: ``` paulson@46820 ` 742` ``` "W \ univ(A) ==> W -||> univ(A) \ univ(A)" ``` paulson@13163 ` 743` ```apply (unfold univ_def) ``` paulson@13163 ` 744` ```apply (erule FiniteFun_VLimit [OF _ Limit_nat]) ``` paulson@13163 ` 745` ```done ``` paulson@13163 ` 746` paulson@13163 ` 747` ```lemma FiniteFun_in_univ: ``` paulson@46820 ` 748` ``` "[| f: W -||> univ(A); W \ univ(A) |] ==> f \ univ(A)" ``` paulson@13163 ` 749` ```by (erule FiniteFun_univ [THEN subsetD], assumption) ``` paulson@13163 ` 750` wenzelm@60770 ` 751` ```text\Remove @{text "\"} from the rule above\ ``` paulson@13163 ` 752` ```lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI] ``` paulson@13163 ` 753` paulson@13163 ` 754` wenzelm@60770 ` 755` ```subsection\* For QUniv. Properties of Vfrom analogous to the "take-lemma" *\ ``` paulson@13163 ` 756` wenzelm@60770 ` 757` ```text\Intersecting a*b with Vfrom...\ ``` paulson@13163 ` 758` wenzelm@60770 ` 759` ```text\This version says a, b exist one level down, in the smaller set Vfrom(X,i)\ ``` paulson@13163 ` 760` ```lemma doubleton_in_Vfrom_D: ``` paulson@13220 ` 761` ``` "[| {a,b} \ Vfrom(X,succ(i)); Transset(X) |] ``` paulson@13220 ` 762` ``` ==> a \ Vfrom(X,i) & b \ Vfrom(X,i)" ``` paulson@46820 ` 763` ```by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], ``` paulson@13163 ` 764` ``` assumption, fast) ``` paulson@13163 ` 765` wenzelm@60770 ` 766` ```text\This weaker version says a, b exist at the same level\ ``` wenzelm@45602 ` 767` ```lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D] ``` paulson@13163 ` 768` paulson@46821 ` 769` ```(** Using only the weaker theorem would prove \ Vfrom(X,i) ``` paulson@46821 ` 770` ``` implies a, b \ Vfrom(X,i), which is useless for induction. ``` paulson@46821 ` 771` ``` Using only the stronger theorem would prove \ Vfrom(X,succ(succ(i))) ``` paulson@46821 ` 772` ``` implies a, b \ Vfrom(X,i), leaving the succ(i) case untreated. ``` paulson@13163 ` 773` ``` The combination gives a reduction by precisely one level, which is ``` paulson@13163 ` 774` ``` most convenient for proofs. ``` paulson@13163 ` 775` ```**) ``` paulson@13163 ` 776` paulson@13163 ` 777` ```lemma Pair_in_Vfrom_D: ``` paulson@13220 ` 778` ``` "[| \ Vfrom(X,succ(i)); Transset(X) |] ``` paulson@13220 ` 779` ``` ==> a \ Vfrom(X,i) & b \ Vfrom(X,i)" ``` paulson@13163 ` 780` ```apply (unfold Pair_def) ``` paulson@13163 ` 781` ```apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D) ``` paulson@13163 ` 782` ```done ``` paulson@13163 ` 783` paulson@13163 ` 784` ```lemma product_Int_Vfrom_subset: ``` paulson@13163 ` 785` ``` "Transset(X) ==> ``` paulson@46820 ` 786` ``` (a*b) \ Vfrom(X, succ(i)) \ (a \ Vfrom(X,i)) * (b \ Vfrom(X,i))" ``` paulson@13163 ` 787` ```by (blast dest!: Pair_in_Vfrom_D) ``` paulson@13163 ` 788` paulson@13163 ` 789` paulson@13163 ` 790` ```ML ``` wenzelm@60770 ` 791` ```\ ``` wenzelm@51717 ` 792` ```val rank_ss = ``` wenzelm@51717 ` 793` ``` simpset_of (@{context} addsimps [@{thm VsetI}] ``` wenzelm@51717 ` 794` ``` addsimps @{thms rank_rls} @ (@{thms rank_rls} RLN (2, [@{thm lt_trans}]))); ``` wenzelm@60770 ` 795` ```\ ``` clasohm@0 ` 796` clasohm@0 ` 797` ```end ```