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\<open>The Cumulative Hierarchy and a Small Universe for Recursive Types\<close>
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 \<union> (\<Union>y\<in>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. \<lambda>z\<in>Vset(succ(x)).
paulson@46820
    28
                           H(z, \<lambda>w\<in>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. \<lambda>z\<in>Vset(succ(x)).
paulson@46820
    33
                                H(\<lambda>w\<in>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\<open>Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}\<close>
paulson@13356
    41
wenzelm@60770
    42
text\<open>NOT SUITABLE FOR REWRITING -- RECURSIVE!\<close>
paulson@46820
    43
lemma Vfrom: "Vfrom(A,i) = A \<union> (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
paulson@13269
    44
by (subst Vfrom_def [THEN def_transrec], simp)
paulson@13163
    45
wenzelm@60770
    46
subsubsection\<open>Monotonicity\<close>
paulson@13163
    47
paulson@13163
    48
lemma Vfrom_mono [rule_format]:
paulson@46820
    49
     "A<=B ==> \<forall>j. i<=j \<longrightarrow> Vfrom(A,i) \<subseteq> 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 \<in> Vfrom(A,j);  j<i |] ==> a \<in> 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\<open>A fundamental equality: Vfrom does not require ordinals!\<close>
paulson@13163
    63
paulson@15481
    64
paulson@15481
    65
paulson@46820
    66
lemma Vfrom_rank_subset1: "Vfrom(A,x) \<subseteq> Vfrom(A,rank(x))"
paulson@15481
    67
proof (induct x rule: eps_induct)
paulson@15481
    68
  fix x
paulson@15481
    69
  assume "\<forall>y\<in>x. Vfrom(A,y) \<subseteq> Vfrom(A,rank(y))"
paulson@15481
    70
  thus "Vfrom(A, x) \<subseteq> 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)) \<subseteq> 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\<open>expand @{text "rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))"} in assumptions\<close>
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\<open>Basic Closure Properties\<close>
paulson@13163
    98
paulson@13220
    99
lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
paulson@13163
   100
by (subst Vfrom, blast)
paulson@13163
   101
paulson@46820
   102
lemma i_subset_Vfrom: "i \<subseteq> 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 \<subseteq> 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 \<subseteq> Vfrom(A,i) ==> a \<in> Vfrom(A,succ(i))"
paulson@13163
   115
by (subst Vfrom, blast)
paulson@13163
   116
wenzelm@60770
   117
subsubsection\<open>Finite sets and ordered pairs\<close>
paulson@13163
   118
paulson@13220
   119
lemma singleton_in_Vfrom: "a \<in> Vfrom(A,i) ==> {a} \<in> 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 \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> {a,b} \<in> 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 \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> <a,b> \<in> 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 \<subseteq> Vfrom(A,i) ==> succ(a) \<in> 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\<open>0, Successor and Limit Equations for @{term Vfrom}\<close>
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 \<union> 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 \<union> 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,\<Union>(X)) = A \<union> (\<Union>y\<in>X. Vfrom(A,y)) *)
paulson@46820
   162
lemma Vfrom_Union: "y:X ==> Vfrom(A,\<Union>(X)) = (\<Union>y\<in>X. Vfrom(A,y))"
paulson@13163
   163
apply (subst Vfrom)
paulson@13163
   164
apply (rule equalityI)
wenzelm@60770
   165
txt\<open>first inclusion\<close>
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\<open>opposite inclusion\<close>
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\<open>@{term Vfrom} applied to Limit Ordinals\<close>
paulson@13163
   180
paulson@13163
   181
(*NB. limit ordinals are non-empty:
paulson@46820
   182
      Vfrom(A,0) = A = A \<union> (\<Union>y\<in>0. Vfrom(A,y)) *)
paulson@13163
   183
lemma Limit_Vfrom_eq:
paulson@13220
   184
    "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>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 \<in> Vfrom(A,i);  ~R ==> Limit(i);
paulson@13220
   191
        !!x. [| x<i;  a \<in> 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 \<in> Vfrom(A,i);  Limit(i) |] ==> {a} \<in> 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\<open>Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)\<close>
paulson@13163
   213
lemma doubleton_in_VLimit:
paulson@13220
   214
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> {a,b} \<in> 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 \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> <a,b> \<in> Vfrom(A,i)"
wenzelm@60770
   223
txt\<open>Infer that a, b occur at ordinals x,xa < i.\<close>
paulson@13163
   224
apply (erule Limit_VfromE, assumption)
paulson@13163
   225
apply (erule Limit_VfromE, assumption)
wenzelm@60770
   226
txt\<open>Infer that @{term"succ(succ(x \<union> xa)) < i"}\<close>
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) \<subseteq> 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 \<in> Vfrom(A,i)"
paulson@13163
   241
by (blast intro: nat_subset_VLimit [THEN subsetD])
paulson@13163
   242
wenzelm@60770
   243
subsubsection\<open>Closure under Disjoint Union\<close>
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 \<in> 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 \<in> Vfrom(A,i); Limit(i) |] ==> Inl(a) \<in> 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 \<in> Vfrom(A,i); Limit(i) |] ==> Inr(b) \<in> 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) \<subseteq> 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\<open>Properties assuming @{term "Transset(A)"}\<close>
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: "[| <a,b> \<subseteq> 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
     "[| <a,b> \<subseteq> Vfrom(A,i);  Transset(A);  Limit(i) |]
paulson@13220
   291
      ==> <a,b> \<in> 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 \<in> Vfrom(A,j);  Transset(A) |] ==> \<Union>(X) \<in> 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 \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \<Union>(X) \<in> 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\<open>General theorem for membership in Vfrom(A,i) when i is a limit ordinal\<close>
paulson@13163
   317
lemma in_VLimit:
paulson@13220
   318
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);
paulson@13220
   319
      !!x y j. [| j<i; 1:j; x \<in> Vfrom(A,j); y \<in> Vfrom(A,j) |]
paulson@46820
   320
               ==> \<exists>k. h(x,y) \<in> Vfrom(A,k) & k<i |]
paulson@13220
   321
   ==> h(a,b) \<in> Vfrom(A,i)"
wenzelm@60770
   322
txt\<open>Infer that a, b occur at ordinals x,xa < i.\<close>
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 \<union> xa \<union> 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\<open>Products\<close>
paulson@13163
   333
paulson@13163
   334
lemma prod_in_Vfrom:
paulson@13220
   335
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
paulson@13220
   336
     ==> a*b \<in> 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 \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
paulson@13220
   345
   ==> a*b \<in> 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\<open>Disjoint Sums, or Quine Ordered Pairs\<close>
paulson@13163
   351
paulson@13163
   352
lemma sum_in_Vfrom:
paulson@13220
   353
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
paulson@13220
   354
     ==> a+b \<in> 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 \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
paulson@13220
   364
   ==> a+b \<in> 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\<open>Function Space!\<close>
paulson@13163
   370
paulson@13163
   371
lemma fun_in_Vfrom:
paulson@13220
   372
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
paulson@13220
   373
          a->b \<in> 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 \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
paulson@13220
   389
   ==> a->b \<in> 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 \<in> Vfrom(A,j);  Transset(A) |] ==> Pow(a) \<in> 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 \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) \<in> 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\<open>The Set @{term "Vset(i)"}\<close>
paulson@13163
   408
paulson@13220
   409
lemma Vset: "Vset(i) = (\<Union>j\<in>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\<open>Characterisation of the elements of @{term "Vset(i)"}\<close>
paulson@13163
   416
paulson@46820
   417
lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) \<longrightarrow> 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) ==> \<forall>b. rank(b) \<in> i \<longrightarrow> b \<in> 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)<i ==> x \<in> Vset(i)"
paulson@13163
   433
by (blast intro: VsetI_lemma elim: ltE)
paulson@13163
   434
wenzelm@60770
   435
text\<open>Merely a lemma for the next result\<close>
paulson@46821
   436
lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) \<longleftrightarrow> rank(b) < i"
paulson@13163
   437
by (blast intro: VsetD VsetI)
paulson@13163
   438
paulson@46821
   439
lemma Vset_rank_iff [simp]: "b \<in> Vset(a) \<longleftrightarrow> 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\<open>This is rank(rank(a)) = rank(a)\<close>
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 \<in> 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\<open>Reasoning about Sets in Terms of Their Elements' Ranks\<close>
clasohm@0
   463
paulson@46820
   464
lemma arg_subset_Vset_rank: "a \<subseteq> 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 \<inter> Vset(i) \<subseteq> b |] ==> a \<subseteq> 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\<open>Set Up an Environment for Simplification\<close>
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\<open>Recursion over Vset Levels!\<close>
paulson@13163
   491
wenzelm@60770
   492
text\<open>NOT SUITABLE FOR REWRITING: recursive!\<close>
paulson@46820
   493
lemma Vrec: "Vrec(a,H) = H(a, \<lambda>x\<in>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\<open>This form avoids giant explosions in proofs.  NOTE USE OF ==\<close>
paulson@13163
   500
lemma def_Vrec:
paulson@13163
   501
    "[| !!x. h(x)==Vrec(x,H) |] ==>
paulson@46820
   502
     h(a) = H(a, \<lambda>x\<in>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\<open>NOT SUITABLE FOR REWRITING: recursive!\<close>
paulson@13163
   508
lemma Vrecursor:
paulson@46820
   509
     "Vrecursor(H,a) = H(\<lambda>x\<in>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\<open>This form avoids giant explosions in proofs.  NOTE USE OF ==\<close>
paulson@13163
   516
lemma def_Vrecursor:
paulson@46820
   517
     "h == Vrecursor(H) ==> h(a) = H(\<lambda>x\<in>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\<open>The Datatype Universe: @{term "univ(A)"}\<close>
paulson@13163
   524
paulson@46820
   525
lemma univ_mono: "A<=B ==> univ(A) \<subseteq> 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\<open>The Set @{term"univ(A)"} as a Limit\<close>
paulson@13163
   537
paulson@13220
   538
lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>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 \<subseteq> univ(A) ==> c = (\<Union>i\<in>nat. c \<inter> 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 \<subseteq> univ(X);
paulson@46820
   550
        !!i. i:nat ==> a \<inter> Vfrom(X,i) \<subseteq> b |]
paulson@46820
   551
     ==> a \<subseteq> 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 \<subseteq> univ(X);   b \<subseteq> univ(X);
paulson@46820
   558
        !!i. i:nat ==> a \<inter> Vfrom(X,i) = b \<inter> 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\<open>Closure Properties for @{term "univ(A)"}\<close>
paulson@13163
   568
paulson@13220
   569
lemma zero_in_univ: "0 \<in> 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} \<subseteq> univ(A)"
paulson@13255
   575
by (blast intro: zero_in_univ)
paulson@13255
   576
paulson@46820
   577
lemma A_subset_univ: "A \<subseteq> 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\<open>Closure under Unordered and Ordered Pairs\<close>
paulson@13163
   585
paulson@13220
   586
lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> 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} \<in> 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) |] ==> <a,b> \<in> 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) |] ==> \<Union>(X) \<in> 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) \<subseteq> 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\<open>The Natural Numbers\<close>
paulson@13163
   616
paulson@46820
   617
lemma nat_subset_univ: "nat \<subseteq> 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\<open>n:nat ==> n:univ(A)\<close>
wenzelm@45602
   623
lemmas nat_into_univ = nat_subset_univ [THEN subsetD]
paulson@13163
   624
wenzelm@60770
   625
subsubsection\<open>Instances for 1 and 2\<close>
paulson@13163
   626
paulson@13220
   627
lemma one_in_univ: "1 \<in> 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\<open>unused!\<close>
paulson@13220
   633
lemma two_in_univ: "2 \<in> univ(A)"
paulson@13163
   634
by (blast intro: nat_into_univ)
paulson@13163
   635
paulson@46820
   636
lemma bool_subset_univ: "bool \<subseteq> 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\<open>Closure under Disjoint Union\<close>
paulson@13163
   645
paulson@13220
   646
lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> 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) \<in> 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) \<subseteq> 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 \<subseteq> univ(D); \<And>x. x \<in> A \<Longrightarrow> B(x) \<subseteq> univ(D)|] ==> Sigma(A,B) \<subseteq> 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\<open>Finite Branching Closure Properties\<close>
paulson@13163
   676
wenzelm@60770
   677
subsubsection\<open>Closure under Finite Powerset\<close>
paulson@13163
   678
paulson@13163
   679
lemma Fin_Vfrom_lemma:
paulson@46820
   680
     "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> \<exists>j. b \<subseteq> Vfrom(A,j) & j<i"
paulson@13163
   681
apply (erule Fin_induct)
paulson@13163
   682
apply (blast dest!: Limit_has_0, safe)
paulson@13163
   683
apply (erule Limit_VfromE, assumption)
paulson@13163
   684
apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2)
paulson@13163
   685
done
clasohm@0
   686
paulson@46820
   687
lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) \<subseteq> 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)) \<subseteq> 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\<open>Closure under Finite Powers: Functions from a Natural Number\<close>
paulson@13163
   702
paulson@13163
   703
lemma nat_fun_VLimit:
paulson@46820
   704
     "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) \<subseteq> 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) \<subseteq> 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\<open>Closure under Finite Function Space\<close>
paulson@13163
   719
wenzelm@60770
   720
text\<open>General but seldom-used version; normally the domain is fixed\<close>
paulson@13163
   721
lemma FiniteFun_VLimit1:
paulson@46820
   722
     "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) \<subseteq> 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) \<subseteq> 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\<open>Version for a fixed domain\<close>
paulson@13163
   734
lemma FiniteFun_VLimit:
paulson@46820
   735
     "[| W \<subseteq> Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) \<subseteq> 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 \<subseteq> univ(A) ==> W -||> univ(A) \<subseteq> 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 \<subseteq> univ(A) |] ==> f \<in> univ(A)"
paulson@13163
   749
by (erule FiniteFun_univ [THEN subsetD], assumption)
paulson@13163
   750
wenzelm@60770
   751
text\<open>Remove @{text "\<subseteq>"} from the rule above\<close>
paulson@13163
   752
lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
paulson@13163
   753
paulson@13163
   754
wenzelm@60770
   755
subsection\<open>* For QUniv.  Properties of Vfrom analogous to the "take-lemma" *\<close>
paulson@13163
   756
wenzelm@60770
   757
text\<open>Intersecting a*b with Vfrom...\<close>
paulson@13163
   758
wenzelm@60770
   759
text\<open>This version says a, b exist one level down, in the smaller set Vfrom(X,i)\<close>
paulson@13163
   760
lemma doubleton_in_Vfrom_D:
paulson@13220
   761
     "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
paulson@13220
   762
      ==> a \<in> Vfrom(X,i)  &  b \<in> 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\<open>This weaker version says a, b exist at the same level\<close>
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 <a,b> \<in> Vfrom(X,i)
paulson@46821
   770
      implies a, b \<in> Vfrom(X,i), which is useless for induction.
paulson@46821
   771
    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
paulson@46821
   772
      implies a, b \<in> 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
    "[| <a,b> \<in> Vfrom(X,succ(i));  Transset(X) |]
paulson@13220
   779
     ==> a \<in> Vfrom(X,i)  &  b \<in> 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) \<inter> Vfrom(X, succ(i)) \<subseteq> (a \<inter> Vfrom(X,i)) * (b \<inter> 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
\<open>
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
\<close>
clasohm@0
   796
clasohm@0
   797
end