author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46821  ff6b0c1087f2 
child 58871  c399ae4b836f 
permissions  rwrr 
6093  1 
(* Title: ZF/QUniv.thy 
1478  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

13356  6 
header{*A Small Universe for Lazy Recursive Types*} 
13285  7 

16417  8 
theory QUniv imports Univ QPair begin 
3923  9 

6112  10 
(*Disjoint sums as a datatype*) 
46820  11 
rep_datatype 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

12 
elimination sumE 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

13 
induction TrueI 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

14 
case_eqns case_Inl case_Inr 
6112  15 

16 
(*Variant disjoint sums as a datatype*) 

46820  17 
rep_datatype 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

18 
elimination qsumE 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

19 
induction TrueI 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

20 
case_eqns qcase_QInl qcase_QInr 
6112  21 

24893  22 
definition 
23 
quniv :: "i => i" where 

6112  24 
"quniv(A) == Pow(univ(eclose(A)))" 
0  25 

13285  26 

13356  27 
subsection{*Properties involving Transset and Sum*} 
28 

13285  29 
lemma Transset_includes_summands: 
46820  30 
"[ Transset(C); A+B \<subseteq> C ] ==> A \<subseteq> C & B \<subseteq> C" 
31 
apply (simp add: sum_def Un_subset_iff) 

13285  32 
apply (blast dest: Transset_includes_range) 
33 
done 

34 

35 
lemma Transset_sum_Int_subset: 

46820  36 
"Transset(C) ==> (A+B) \<inter> C \<subseteq> (A \<inter> C) + (B \<inter> C)" 
37 
apply (simp add: sum_def Int_Un_distrib2) 

13285  38 
apply (blast dest: Transset_Pair_D) 
39 
done 

40 

13356  41 
subsection{*Introduction and Elimination Rules*} 
13285  42 

46820  43 
lemma qunivI: "X \<subseteq> univ(eclose(A)) ==> X \<in> quniv(A)" 
13285  44 
by (simp add: quniv_def) 
45 

46820  46 
lemma qunivD: "X \<in> quniv(A) ==> X \<subseteq> univ(eclose(A))" 
13285  47 
by (simp add: quniv_def) 
48 

46820  49 
lemma quniv_mono: "A<=B ==> quniv(A) \<subseteq> quniv(B)" 
13285  50 
apply (unfold quniv_def) 
51 
apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono]) 

52 
done 

53 

13356  54 
subsection{*Closure Properties*} 
13285  55 

46820  56 
lemma univ_eclose_subset_quniv: "univ(eclose(A)) \<subseteq> quniv(A)" 
57 
apply (simp add: quniv_def Transset_iff_Pow [symmetric]) 

13285  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*) 

46820  62 
lemma univ_subset_quniv: "univ(A) \<subseteq> quniv(A)" 
13285  63 
apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans]) 
64 
apply (rule univ_eclose_subset_quniv) 

65 
done 

66 

45602  67 
lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD] 
13285  68 

46820  69 
lemma Pow_univ_subset_quniv: "Pow(univ(A)) \<subseteq> quniv(A)" 
13285  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 = 

45602  75 
PowI [THEN Pow_univ_subset_quniv [THEN subsetD]] 
13285  76 

45602  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] 

13285  80 

81 
lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv] 

82 

45602  83 
lemmas A_into_quniv = A_subset_quniv [THEN subsetD] 
13285  84 

85 
(*** univ(A) closure for Quineinspired pairs and injections ***) 

86 

87 
(*Quine ordered pairs*) 

46820  88 
lemma QPair_subset_univ: 
89 
"[ a \<subseteq> univ(A); b \<subseteq> univ(A) ] ==> <a;b> \<subseteq> univ(A)" 

13285  90 
by (simp add: QPair_def sum_subset_univ) 
91 

13356  92 
subsection{*Quine Disjoint Sum*} 
13285  93 

46820  94 
lemma QInl_subset_univ: "a \<subseteq> univ(A) ==> QInl(a) \<subseteq> univ(A)" 
13285  95 
apply (unfold QInl_def) 
96 
apply (erule empty_subsetI [THEN QPair_subset_univ]) 

97 
done 

98 

46820  99 
lemmas naturals_subset_nat = 
45602  100 
Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec] 
13285  101 

102 
lemmas naturals_subset_univ = 

103 
subset_trans [OF naturals_subset_nat nat_subset_univ] 

104 

46820  105 
lemma QInr_subset_univ: "a \<subseteq> univ(A) ==> QInr(a) \<subseteq> univ(A)" 
13285  106 
apply (unfold QInr_def) 
107 
apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ]) 

108 
done 

109 

13356  110 
subsection{*Closure for QuineInspired Products and Sums*} 
13285  111 

112 
(*Quine ordered pairs*) 

46820  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) 

13285  116 

46820  117 
lemma QSigma_quniv: "quniv(A) <*> quniv(A) \<subseteq> quniv(A)" 
13285  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*) 

46820  123 
lemma quniv_QPair_D: 
124 
"<a;b> \<in> quniv(A) ==> a: quniv(A) & b: quniv(A)" 

13285  125 
apply (unfold quniv_def QPair_def) 
46820  126 
apply (rule Transset_includes_summands [THEN conjE]) 
13285  127 
apply (rule Transset_eclose [THEN Transset_univ]) 
46820  128 
apply (erule PowD, blast) 
13285  129 
done 
130 

45602  131 
lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE] 
13285  132 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

133 
lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) \<longleftrightarrow> a: quniv(A) & b: quniv(A)" 
13285  134 
by (blast intro: QPair_in_quniv dest: quniv_QPair_D) 
135 

136 

13356  137 
subsection{*Quine Disjoint Sum*} 
13285  138 

46820  139 
lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) \<in> quniv(A)" 
13285  140 
by (simp add: QInl_def zero_in_quniv QPair_in_quniv) 
141 

46820  142 
lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) \<in> quniv(A)" 
13285  143 
by (simp add: QInr_def one_in_quniv QPair_in_quniv) 
144 

46820  145 
lemma qsum_quniv: "quniv(C) <+> quniv(C) \<subseteq> quniv(C)" 
13285  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 

13356  151 
subsection{*The Natural Numbers*} 
13285  152 

153 
lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv] 

154 

155 
(* n:nat ==> n:quniv(A) *) 

45602  156 
lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD] 
13285  157 

158 
lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv] 

159 

45602  160 
lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD] 
13285  161 

162 

13356  163 
(*Intersecting <a;b> with Vfrom...*) 
13285  164 

46820  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)>" 

13285  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 

13356  172 
subsection{*"TakeLemma" Rules*} 
173 

174 
(*for proving a=b by coinduction and c: quniv(A)*) 

13285  175 

176 
(*Rule for level i  preserving the level, not decreasing it*) 

177 

46820  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)>" 

13285  181 
apply (unfold QPair_def) 
182 
apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset]) 

183 
done 

184 

46820  185 
(*@{term"[ a \<inter> Vset(i) \<subseteq> c; b \<inter> Vset(i) \<subseteq> d ] ==> <a;b> \<inter> Vset(i) \<subseteq> <c;d>"}*) 
13285  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: 

46820  190 
"Ord(i) ==> <a;b> \<inter> Vset(i) \<subseteq> (\<Union>j\<in>i. <a \<inter> Vset(j); b \<inter> Vset(j)>)" 
13285  191 
apply (erule Ord_cases) 
192 
(*0 case*) 

193 
apply (simp add: Vfrom_0) 

194 
(*succ(j) case*) 

46820  195 
apply (erule ssubst) 
13285  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*) 

46820  199 
apply (simp del: UN_simps 
13285  200 
add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans) 
201 
done 

202 

0  203 
end 