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