src/ZF/QUniv.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 63040 eb4ddd18d635
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      ZF/QUniv.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 section\<open>A Small Universe for Lazy Recursive Types\<close>
     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\<open>Properties involving Transset and Sum\<close>
    28 
    29 lemma Transset_includes_summands:
    30      "[| Transset(C); A+B \<subseteq> C |] ==> A \<subseteq> C & B \<subseteq> 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) \<inter> C \<subseteq> (A \<inter> C) + (B \<inter> C)"
    37 apply (simp add: sum_def Int_Un_distrib2)
    38 apply (blast dest: Transset_Pair_D)
    39 done
    40 
    41 subsection\<open>Introduction and Elimination Rules\<close>
    42 
    43 lemma qunivI: "X \<subseteq> univ(eclose(A)) ==> X \<in> quniv(A)"
    44 by (simp add: quniv_def)
    45 
    46 lemma qunivD: "X \<in> quniv(A) ==> X \<subseteq> univ(eclose(A))"
    47 by (simp add: quniv_def)
    48 
    49 lemma quniv_mono: "A<=B ==> quniv(A) \<subseteq> quniv(B)"
    50 apply (unfold quniv_def)
    51 apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
    52 done
    53 
    54 subsection\<open>Closure Properties\<close>
    55 
    56 lemma univ_eclose_subset_quniv: "univ(eclose(A)) \<subseteq> 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 definition of quniv*)
    62 lemma univ_subset_quniv: "univ(A) \<subseteq> 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]
    68 
    69 lemma Pow_univ_subset_quniv: "Pow(univ(A)) \<subseteq> 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]]
    76 
    77 lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv]
    78 lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv]
    79 lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv]
    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]
    84 
    85 (*** univ(A) closure for Quine-inspired pairs and injections ***)
    86 
    87 (*Quine ordered pairs*)
    88 lemma QPair_subset_univ:
    89     "[| a \<subseteq> univ(A);  b \<subseteq> univ(A) |] ==> <a;b> \<subseteq> univ(A)"
    90 by (simp add: QPair_def sum_subset_univ)
    91 
    92 subsection\<open>Quine Disjoint Sum\<close>
    93 
    94 lemma QInl_subset_univ: "a \<subseteq> univ(A) ==> QInl(a) \<subseteq> 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]
   101 
   102 lemmas naturals_subset_univ =
   103     subset_trans [OF naturals_subset_nat nat_subset_univ]
   104 
   105 lemma QInr_subset_univ: "a \<subseteq> univ(A) ==> QInr(a) \<subseteq> 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\<open>Closure for Quine-Inspired Products and Sums\<close>
   111 
   112 (*Quine ordered pairs*)
   113 lemma QPair_in_quniv:
   114     "[| a: quniv(A);  b: quniv(A) |] ==> <a;b> \<in> quniv(A)"
   115 by (simp add: quniv_def QPair_def sum_subset_univ)
   116 
   117 lemma QSigma_quniv: "quniv(A) <*> quniv(A) \<subseteq> 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> \<in> 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]
   132 
   133 lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) \<longleftrightarrow> a: quniv(A) & b: quniv(A)"
   134 by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
   135 
   136 
   137 subsection\<open>Quine Disjoint Sum\<close>
   138 
   139 lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) \<in> 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) \<in> quniv(A)"
   143 by (simp add: QInr_def one_in_quniv QPair_in_quniv)
   144 
   145 lemma qsum_quniv: "quniv(C) <+> quniv(C) \<subseteq> 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\<open>The Natural Numbers\<close>
   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]
   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]
   161 
   162 
   163 (*Intersecting <a;b> with Vfrom...*)
   164 
   165 lemma QPair_Int_Vfrom_succ_subset:
   166  "Transset(X) ==>
   167        <a;b> \<inter> Vfrom(X, succ(i))  \<subseteq>  <a \<inter> Vfrom(X,i);  b \<inter> 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\<open>"Take-Lemma" Rules\<close>
   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> \<inter> Vfrom(X,i)  \<subseteq>  <a \<inter> Vfrom(X,i);  b \<inter> Vfrom(X,i)>"
   181 apply (unfold QPair_def)
   182 apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
   183 done
   184 
   185 (*@{term"[| a \<inter> Vset(i) \<subseteq> c; b \<inter> Vset(i) \<subseteq> d |] ==> <a;b> \<inter> Vset(i) \<subseteq> <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> \<inter> Vset(i) \<subseteq> (\<Union>j\<in>i. <a \<inter> Vset(j); b \<inter> 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