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