src/ZF/QUniv.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 13615 449a70d88b38
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
migrated theory headers to new format
wenzelm@6093
     1
(*  Title:      ZF/QUniv.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
*)
clasohm@0
     7
paulson@13356
     8
header{*A Small Universe for Lazy Recursive Types*}
paulson@13285
     9
haftmann@16417
    10
theory QUniv imports Univ QPair begin
wenzelm@3923
    11
paulson@6112
    12
(*Disjoint sums as a datatype*)
paulson@6112
    13
rep_datatype 
paulson@13285
    14
  elimination	sumE
paulson@13285
    15
  induction	TrueI
paulson@13285
    16
  case_eqns	case_Inl case_Inr
paulson@6112
    17
paulson@6112
    18
(*Variant disjoint sums as a datatype*)
paulson@6112
    19
rep_datatype 
paulson@13285
    20
  elimination	qsumE
paulson@13285
    21
  induction	TrueI
paulson@13285
    22
  case_eqns	qcase_QInl qcase_QInr
paulson@6112
    23
wenzelm@6093
    24
constdefs
paulson@13220
    25
  quniv :: "i => i"
paulson@6112
    26
   "quniv(A) == Pow(univ(eclose(A)))"
clasohm@0
    27
paulson@13285
    28
paulson@13356
    29
subsection{*Properties involving Transset and Sum*}
paulson@13356
    30
paulson@13285
    31
lemma Transset_includes_summands:
paulson@13285
    32
     "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"
paulson@13285
    33
apply (simp add: sum_def Un_subset_iff) 
paulson@13285
    34
apply (blast dest: Transset_includes_range)
paulson@13285
    35
done
paulson@13285
    36
paulson@13285
    37
lemma Transset_sum_Int_subset:
paulson@13285
    38
     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"
paulson@13285
    39
apply (simp add: sum_def Int_Un_distrib2) 
paulson@13285
    40
apply (blast dest: Transset_Pair_D)
paulson@13285
    41
done
paulson@13285
    42
paulson@13356
    43
subsection{*Introduction and Elimination Rules*}
paulson@13285
    44
paulson@13285
    45
lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)"
paulson@13285
    46
by (simp add: quniv_def)
paulson@13285
    47
paulson@13285
    48
lemma qunivD: "X : quniv(A) ==> X <= univ(eclose(A))"
paulson@13285
    49
by (simp add: quniv_def)
paulson@13285
    50
paulson@13285
    51
lemma quniv_mono: "A<=B ==> quniv(A) <= quniv(B)"
paulson@13285
    52
apply (unfold quniv_def)
paulson@13285
    53
apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
paulson@13285
    54
done
paulson@13285
    55
paulson@13356
    56
subsection{*Closure Properties*}
paulson@13285
    57
paulson@13285
    58
lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)"
paulson@13285
    59
apply (simp add: quniv_def Transset_iff_Pow [symmetric]) 
paulson@13285
    60
apply (rule Transset_eclose [THEN Transset_univ])
paulson@13285
    61
done
paulson@13285
    62
paulson@13285
    63
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
paulson@13285
    64
lemma univ_subset_quniv: "univ(A) <= quniv(A)"
paulson@13285
    65
apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
paulson@13285
    66
apply (rule univ_eclose_subset_quniv)
paulson@13285
    67
done
paulson@13285
    68
paulson@13285
    69
lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
paulson@13285
    70
paulson@13285
    71
lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
paulson@13285
    72
apply (unfold quniv_def)
paulson@13285
    73
apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
paulson@13285
    74
done
paulson@13285
    75
paulson@13285
    76
lemmas univ_subset_into_quniv =
paulson@13285
    77
    PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
paulson@13285
    78
paulson@13285
    79
lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
paulson@13285
    80
lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
paulson@13285
    81
lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
paulson@13285
    82
paulson@13285
    83
lemmas A_subset_quniv =  subset_trans [OF A_subset_univ univ_subset_quniv]
paulson@13285
    84
paulson@13285
    85
lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
paulson@13285
    86
paulson@13285
    87
(*** univ(A) closure for Quine-inspired pairs and injections ***)
paulson@13285
    88
paulson@13285
    89
(*Quine ordered pairs*)
paulson@13285
    90
lemma QPair_subset_univ: 
paulson@13285
    91
    "[| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)"
paulson@13285
    92
by (simp add: QPair_def sum_subset_univ)
paulson@13285
    93
paulson@13356
    94
subsection{*Quine Disjoint Sum*}
paulson@13285
    95
paulson@13285
    96
lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)"
paulson@13285
    97
apply (unfold QInl_def)
paulson@13285
    98
apply (erule empty_subsetI [THEN QPair_subset_univ])
paulson@13285
    99
done
paulson@13285
   100
paulson@13285
   101
lemmas naturals_subset_nat = 
paulson@13285
   102
    Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
paulson@13285
   103
paulson@13285
   104
lemmas naturals_subset_univ =
paulson@13285
   105
    subset_trans [OF naturals_subset_nat nat_subset_univ]
paulson@13285
   106
paulson@13285
   107
lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)"
paulson@13285
   108
apply (unfold QInr_def)
paulson@13285
   109
apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
paulson@13285
   110
done
paulson@13285
   111
paulson@13356
   112
subsection{*Closure for Quine-Inspired Products and Sums*}
paulson@13285
   113
paulson@13285
   114
(*Quine ordered pairs*)
paulson@13285
   115
lemma QPair_in_quniv: 
paulson@13285
   116
    "[| a: quniv(A);  b: quniv(A) |] ==> <a;b> : quniv(A)"
paulson@13285
   117
by (simp add: quniv_def QPair_def sum_subset_univ) 
paulson@13285
   118
paulson@13285
   119
lemma QSigma_quniv: "quniv(A) <*> quniv(A) <= quniv(A)" 
paulson@13285
   120
by (blast intro: QPair_in_quniv)
paulson@13285
   121
paulson@13285
   122
lemmas QSigma_subset_quniv =  subset_trans [OF QSigma_mono QSigma_quniv]
paulson@13285
   123
paulson@13285
   124
(*The opposite inclusion*)
paulson@13285
   125
lemma quniv_QPair_D: 
paulson@13285
   126
    "<a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"
paulson@13285
   127
apply (unfold quniv_def QPair_def)
paulson@13285
   128
apply (rule Transset_includes_summands [THEN conjE]) 
paulson@13285
   129
apply (rule Transset_eclose [THEN Transset_univ])
paulson@13285
   130
apply (erule PowD, blast) 
paulson@13285
   131
done
paulson@13285
   132
paulson@13285
   133
lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
paulson@13285
   134
paulson@13285
   135
lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
paulson@13285
   136
by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
paulson@13285
   137
paulson@13285
   138
paulson@13356
   139
subsection{*Quine Disjoint Sum*}
paulson@13285
   140
paulson@13285
   141
lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)"
paulson@13285
   142
by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
paulson@13285
   143
paulson@13285
   144
lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) : quniv(A)"
paulson@13285
   145
by (simp add: QInr_def one_in_quniv QPair_in_quniv)
paulson@13285
   146
paulson@13285
   147
lemma qsum_quniv: "quniv(C) <+> quniv(C) <= quniv(C)"
paulson@13285
   148
by (blast intro: QInl_in_quniv QInr_in_quniv)
paulson@13285
   149
paulson@13285
   150
lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
paulson@13285
   151
paulson@13285
   152
paulson@13356
   153
subsection{*The Natural Numbers*}
paulson@13285
   154
paulson@13285
   155
lemmas nat_subset_quniv =  subset_trans [OF nat_subset_univ univ_subset_quniv]
paulson@13285
   156
paulson@13285
   157
(* n:nat ==> n:quniv(A) *)
paulson@13285
   158
lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
paulson@13285
   159
paulson@13285
   160
lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
paulson@13285
   161
paulson@13285
   162
lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
paulson@13285
   163
paulson@13285
   164
paulson@13356
   165
(*Intersecting <a;b> with Vfrom...*)
paulson@13285
   166
paulson@13285
   167
lemma QPair_Int_Vfrom_succ_subset: 
paulson@13285
   168
 "Transset(X) ==>           
paulson@13285
   169
       <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>"
paulson@13285
   170
by (simp add: QPair_def sum_def Int_Un_distrib2 Un_mono
paulson@13285
   171
              product_Int_Vfrom_subset [THEN subset_trans]
paulson@13285
   172
              Sigma_mono [OF Int_lower1 subset_refl])
paulson@13285
   173
paulson@13356
   174
subsection{*"Take-Lemma" Rules*}
paulson@13356
   175
paulson@13356
   176
(*for proving a=b by coinduction and c: quniv(A)*)
paulson@13285
   177
paulson@13285
   178
(*Rule for level i -- preserving the level, not decreasing it*)
paulson@13285
   179
paulson@13285
   180
lemma QPair_Int_Vfrom_subset: 
paulson@13285
   181
 "Transset(X) ==>           
paulson@13285
   182
       <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>"
paulson@13285
   183
apply (unfold QPair_def)
paulson@13285
   184
apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
paulson@13285
   185
done
paulson@13285
   186
paulson@13285
   187
(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
paulson@13285
   188
lemmas QPair_Int_Vset_subset_trans =
paulson@13285
   189
     subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
paulson@13285
   190
paulson@13285
   191
lemma QPair_Int_Vset_subset_UN:
paulson@13615
   192
     "Ord(i) ==> <a;b> Int Vset(i) <= (\<Union>j\<in>i. <a Int Vset(j); b Int Vset(j)>)"
paulson@13285
   193
apply (erule Ord_cases)
paulson@13285
   194
(*0 case*)
paulson@13285
   195
apply (simp add: Vfrom_0)
paulson@13285
   196
(*succ(j) case*)
paulson@13285
   197
apply (erule ssubst) 
paulson@13285
   198
apply (rule Transset_0 [THEN QPair_Int_Vfrom_succ_subset, THEN subset_trans])
paulson@13285
   199
apply (rule succI1 [THEN UN_upper])
paulson@13285
   200
(*Limit(i) case*)
paulson@13285
   201
apply (simp del: UN_simps 
paulson@13285
   202
        add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans)
paulson@13285
   203
done
paulson@13285
   204
paulson@13285
   205
ML
paulson@13285
   206
{*
paulson@13285
   207
val Transset_includes_summands = thm "Transset_includes_summands";
paulson@13285
   208
val Transset_sum_Int_subset = thm "Transset_sum_Int_subset";
paulson@13285
   209
val qunivI = thm "qunivI";
paulson@13285
   210
val qunivD = thm "qunivD";
paulson@13285
   211
val quniv_mono = thm "quniv_mono";
paulson@13285
   212
val univ_eclose_subset_quniv = thm "univ_eclose_subset_quniv";
paulson@13285
   213
val univ_subset_quniv = thm "univ_subset_quniv";
paulson@13285
   214
val univ_into_quniv = thm "univ_into_quniv";
paulson@13285
   215
val Pow_univ_subset_quniv = thm "Pow_univ_subset_quniv";
paulson@13285
   216
val univ_subset_into_quniv = thm "univ_subset_into_quniv";
paulson@13285
   217
val zero_in_quniv = thm "zero_in_quniv";
paulson@13285
   218
val one_in_quniv = thm "one_in_quniv";
paulson@13285
   219
val two_in_quniv = thm "two_in_quniv";
paulson@13285
   220
val A_subset_quniv = thm "A_subset_quniv";
paulson@13285
   221
val A_into_quniv = thm "A_into_quniv";
paulson@13285
   222
val QPair_subset_univ = thm "QPair_subset_univ";
paulson@13285
   223
val QInl_subset_univ = thm "QInl_subset_univ";
paulson@13285
   224
val naturals_subset_nat = thm "naturals_subset_nat";
paulson@13285
   225
val naturals_subset_univ = thm "naturals_subset_univ";
paulson@13285
   226
val QInr_subset_univ = thm "QInr_subset_univ";
paulson@13285
   227
val QPair_in_quniv = thm "QPair_in_quniv";
paulson@13285
   228
val QSigma_quniv = thm "QSigma_quniv";
paulson@13285
   229
val QSigma_subset_quniv = thm "QSigma_subset_quniv";
paulson@13285
   230
val quniv_QPair_D = thm "quniv_QPair_D";
paulson@13285
   231
val quniv_QPair_E = thm "quniv_QPair_E";
paulson@13285
   232
val quniv_QPair_iff = thm "quniv_QPair_iff";
paulson@13285
   233
val QInl_in_quniv = thm "QInl_in_quniv";
paulson@13285
   234
val QInr_in_quniv = thm "QInr_in_quniv";
paulson@13285
   235
val qsum_quniv = thm "qsum_quniv";
paulson@13285
   236
val qsum_subset_quniv = thm "qsum_subset_quniv";
paulson@13285
   237
val nat_subset_quniv = thm "nat_subset_quniv";
paulson@13285
   238
val nat_into_quniv = thm "nat_into_quniv";
paulson@13285
   239
val bool_subset_quniv = thm "bool_subset_quniv";
paulson@13285
   240
val bool_into_quniv = thm "bool_into_quniv";
paulson@13285
   241
val QPair_Int_Vfrom_succ_subset = thm "QPair_Int_Vfrom_succ_subset";
paulson@13285
   242
val QPair_Int_Vfrom_subset = thm "QPair_Int_Vfrom_subset";
paulson@13285
   243
val QPair_Int_Vset_subset_trans = thm "QPair_Int_Vset_subset_trans";
paulson@13285
   244
val QPair_Int_Vset_subset_UN = thm "QPair_Int_Vset_subset_UN";
paulson@13285
   245
*}
paulson@13285
   246
clasohm@0
   247
end