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