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