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