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