src/ZF/QUniv.thy
 changeset 13285 28d1823ce0f2 parent 13220 62c899c77151 child 13356 c9cfe1638bf2
```     1.1 --- a/src/ZF/QUniv.thy	Tue Jul 02 17:44:13 2002 +0200
1.2 +++ b/src/ZF/QUniv.thy	Tue Jul 02 22:46:23 2002 +0200
1.3 @@ -3,25 +3,242 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1993  University of Cambridge
1.6
1.7 -A small universe for lazy recursive types.
1.8 +A small universe for lazy recursive types
1.9  *)
1.10
1.11 -QUniv = Univ + QPair + mono + equalities +
1.12 +(** Properties involving Transset and Sum **)
1.13 +
1.14 +theory QUniv = Univ + QPair + mono + equalities:
1.15
1.16  (*Disjoint sums as a datatype*)
1.17  rep_datatype
1.18 -  elim		sumE
1.19 -  induct	TrueI
1.20 -  case_eqns	case_Inl, case_Inr
1.21 +  elimination	sumE
1.22 +  induction	TrueI
1.23 +  case_eqns	case_Inl case_Inr
1.24
1.25  (*Variant disjoint sums as a datatype*)
1.26  rep_datatype
1.27 -  elim		qsumE
1.28 -  induct	TrueI
1.29 -  case_eqns	qcase_QInl, qcase_QInr
1.30 +  elimination	qsumE
1.31 +  induction	TrueI
1.32 +  case_eqns	qcase_QInl qcase_QInr
1.33
1.34  constdefs
1.35    quniv :: "i => i"
1.36     "quniv(A) == Pow(univ(eclose(A)))"
1.37
1.38 +
1.39 +lemma Transset_includes_summands:
1.40 +     "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"
1.41 +apply (simp add: sum_def Un_subset_iff)
1.42 +apply (blast dest: Transset_includes_range)
1.43 +done
1.44 +
1.45 +lemma Transset_sum_Int_subset:
1.46 +     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"
1.47 +apply (simp add: sum_def Int_Un_distrib2)
1.48 +apply (blast dest: Transset_Pair_D)
1.49 +done
1.50 +
1.51 +(** Introduction and elimination rules avoid tiresome folding/unfolding **)
1.52 +
1.53 +lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)"
1.54 +by (simp add: quniv_def)
1.55 +
1.56 +lemma qunivD: "X : quniv(A) ==> X <= univ(eclose(A))"
1.57 +by (simp add: quniv_def)
1.58 +
1.59 +lemma quniv_mono: "A<=B ==> quniv(A) <= quniv(B)"
1.60 +apply (unfold quniv_def)
1.61 +apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
1.62 +done
1.63 +
1.64 +(*** Closure properties ***)
1.65 +
1.66 +lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)"
1.67 +apply (simp add: quniv_def Transset_iff_Pow [symmetric])
1.68 +apply (rule Transset_eclose [THEN Transset_univ])
1.69 +done
1.70 +
1.71 +(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
1.72 +lemma univ_subset_quniv: "univ(A) <= quniv(A)"
1.73 +apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
1.74 +apply (rule univ_eclose_subset_quniv)
1.75 +done
1.76 +
1.77 +lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
1.78 +
1.79 +lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
1.80 +apply (unfold quniv_def)
1.81 +apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
1.82 +done
1.83 +
1.84 +lemmas univ_subset_into_quniv =
1.85 +    PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
1.86 +
1.87 +lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
1.88 +lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
1.89 +lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
1.90 +
1.91 +lemmas A_subset_quniv =  subset_trans [OF A_subset_univ univ_subset_quniv]
1.92 +
1.93 +lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
1.94 +
1.95 +(*** univ(A) closure for Quine-inspired pairs and injections ***)
1.96 +
1.97 +(*Quine ordered pairs*)
1.98 +lemma QPair_subset_univ:
1.99 +    "[| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)"
1.100 +by (simp add: QPair_def sum_subset_univ)
1.101 +
1.102 +(** Quine disjoint sum **)
1.103 +
1.104 +lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)"
1.105 +apply (unfold QInl_def)
1.106 +apply (erule empty_subsetI [THEN QPair_subset_univ])
1.107 +done
1.108 +
1.109 +lemmas naturals_subset_nat =
1.110 +    Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
1.111 +
1.112 +lemmas naturals_subset_univ =
1.113 +    subset_trans [OF naturals_subset_nat nat_subset_univ]
1.114 +
1.115 +lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)"
1.116 +apply (unfold QInr_def)
1.117 +apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
1.118 +done
1.119 +
1.120 +(*** Closure for Quine-inspired products and sums ***)
1.121 +
1.122 +(*Quine ordered pairs*)
1.123 +lemma QPair_in_quniv:
1.124 +    "[| a: quniv(A);  b: quniv(A) |] ==> <a;b> : quniv(A)"
1.125 +by (simp add: quniv_def QPair_def sum_subset_univ)
1.126 +
1.127 +lemma QSigma_quniv: "quniv(A) <*> quniv(A) <= quniv(A)"
1.128 +by (blast intro: QPair_in_quniv)
1.129 +
1.130 +lemmas QSigma_subset_quniv =  subset_trans [OF QSigma_mono QSigma_quniv]
1.131 +
1.132 +(*The opposite inclusion*)
1.133 +lemma quniv_QPair_D:
1.134 +    "<a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"
1.135 +apply (unfold quniv_def QPair_def)
1.136 +apply (rule Transset_includes_summands [THEN conjE])
1.137 +apply (rule Transset_eclose [THEN Transset_univ])
1.138 +apply (erule PowD, blast)
1.139 +done
1.140 +
1.141 +lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
1.142 +
1.143 +lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
1.144 +by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
1.145 +
1.146 +
1.147 +(** Quine disjoint sum **)
1.148 +
1.149 +lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)"
1.150 +by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
1.151 +
1.152 +lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) : quniv(A)"
1.153 +by (simp add: QInr_def one_in_quniv QPair_in_quniv)
1.154 +
1.155 +lemma qsum_quniv: "quniv(C) <+> quniv(C) <= quniv(C)"
1.156 +by (blast intro: QInl_in_quniv QInr_in_quniv)
1.157 +
1.158 +lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
1.159 +
1.160 +
1.161 +(*** The natural numbers ***)
1.162 +
1.163 +lemmas nat_subset_quniv =  subset_trans [OF nat_subset_univ univ_subset_quniv]
1.164 +
1.165 +(* n:nat ==> n:quniv(A) *)
1.166 +lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
1.167 +
1.168 +lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
1.169 +
1.170 +lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
1.171 +
1.172 +
1.173 +(*** Intersecting <a;b> with Vfrom... ***)
1.174 +
1.175 +lemma QPair_Int_Vfrom_succ_subset:
1.176 + "Transset(X) ==>
1.177 +       <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>"
1.178 +by (simp add: QPair_def sum_def Int_Un_distrib2 Un_mono
1.179 +              product_Int_Vfrom_subset [THEN subset_trans]
1.180 +              Sigma_mono [OF Int_lower1 subset_refl])
1.181 +
1.182 +(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****)
1.183 +
1.184 +(*Rule for level i -- preserving the level, not decreasing it*)
1.185 +
1.186 +lemma QPair_Int_Vfrom_subset:
1.187 + "Transset(X) ==>
1.188 +       <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>"
1.189 +apply (unfold QPair_def)
1.190 +apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
1.191 +done
1.192 +
1.193 +(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
1.194 +lemmas QPair_Int_Vset_subset_trans =
1.195 +     subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
1.196 +
1.197 +lemma QPair_Int_Vset_subset_UN:
1.198 +     "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
1.199 +apply (erule Ord_cases)
1.200 +(*0 case*)
1.201 +apply (simp add: Vfrom_0)
1.202 +(*succ(j) case*)
1.203 +apply (erule ssubst)
1.204 +apply (rule Transset_0 [THEN QPair_Int_Vfrom_succ_subset, THEN subset_trans])
1.205 +apply (rule succI1 [THEN UN_upper])
1.206 +(*Limit(i) case*)
1.207 +apply (simp del: UN_simps
1.208 +        add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans)
1.209 +done
1.210 +
1.211 +ML
1.212 +{*
1.213 +val Transset_includes_summands = thm "Transset_includes_summands";
1.214 +val Transset_sum_Int_subset = thm "Transset_sum_Int_subset";
1.215 +val qunivI = thm "qunivI";
1.216 +val qunivD = thm "qunivD";
1.217 +val quniv_mono = thm "quniv_mono";
1.218 +val univ_eclose_subset_quniv = thm "univ_eclose_subset_quniv";
1.219 +val univ_subset_quniv = thm "univ_subset_quniv";
1.220 +val univ_into_quniv = thm "univ_into_quniv";
1.221 +val Pow_univ_subset_quniv = thm "Pow_univ_subset_quniv";
1.222 +val univ_subset_into_quniv = thm "univ_subset_into_quniv";
1.223 +val zero_in_quniv = thm "zero_in_quniv";
1.224 +val one_in_quniv = thm "one_in_quniv";
1.225 +val two_in_quniv = thm "two_in_quniv";
1.226 +val A_subset_quniv = thm "A_subset_quniv";
1.227 +val A_into_quniv = thm "A_into_quniv";
1.228 +val QPair_subset_univ = thm "QPair_subset_univ";
1.229 +val QInl_subset_univ = thm "QInl_subset_univ";
1.230 +val naturals_subset_nat = thm "naturals_subset_nat";
1.231 +val naturals_subset_univ = thm "naturals_subset_univ";
1.232 +val QInr_subset_univ = thm "QInr_subset_univ";
1.233 +val QPair_in_quniv = thm "QPair_in_quniv";
1.234 +val QSigma_quniv = thm "QSigma_quniv";
1.235 +val QSigma_subset_quniv = thm "QSigma_subset_quniv";
1.236 +val quniv_QPair_D = thm "quniv_QPair_D";
1.237 +val quniv_QPair_E = thm "quniv_QPair_E";
1.238 +val quniv_QPair_iff = thm "quniv_QPair_iff";
1.239 +val QInl_in_quniv = thm "QInl_in_quniv";
1.240 +val QInr_in_quniv = thm "QInr_in_quniv";
1.241 +val qsum_quniv = thm "qsum_quniv";
1.242 +val qsum_subset_quniv = thm "qsum_subset_quniv";
1.243 +val nat_subset_quniv = thm "nat_subset_quniv";
1.244 +val nat_into_quniv = thm "nat_into_quniv";
1.245 +val bool_subset_quniv = thm "bool_subset_quniv";
1.246 +val bool_into_quniv = thm "bool_into_quniv";
1.247 +val QPair_Int_Vfrom_succ_subset = thm "QPair_Int_Vfrom_succ_subset";
1.248 +val QPair_Int_Vfrom_subset = thm "QPair_Int_Vfrom_subset";
1.249 +val QPair_Int_Vset_subset_trans = thm "QPair_Int_Vset_subset_trans";
1.250 +val QPair_Int_Vset_subset_UN = thm "QPair_Int_Vset_subset_UN";
1.251 +*}
1.252 +
1.253  end
```