author  paulson 
Fri, 04 Apr 1997 11:18:52 +0200  
changeset 2891  d8f254ad1ab9 
parent 1985  84cf16192e03 
child 2935  998cb95fdd43 
permissions  rwrr 
1465  1 
(* Title: HOL/univ 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1991 University of Cambridge 
5 

6 
For univ.thy 

7 
*) 

8 

9 
open Univ; 

10 

11 
(** apfst  can be used in similar type definitions **) 

12 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

13 
goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)"; 
923  14 
by (rtac split 1); 
976
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

15 
qed "apfst_conv"; 
923  16 

17 
val [major,minor] = goal Univ.thy 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

18 
"[ q = apfst f p; !!x y. [ p = (x,y); q = (f(x),y) ] ==> R \ 
923  19 
\ ] ==> R"; 
20 
by (rtac PairE 1); 

21 
by (rtac minor 1); 

22 
by (assume_tac 1); 

23 
by (rtac (major RS trans) 1); 

24 
by (etac ssubst 1); 

976
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

25 
by (rtac apfst_conv 1); 
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

26 
qed "apfst_convE"; 
923  27 

28 
(** Push  an injection, analogous to Cons on lists **) 

29 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

30 
val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g ==> i=j"; 
923  31 
by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1); 
32 
by (rtac nat_case_0 1); 

33 
by (rtac nat_case_0 1); 

34 
qed "Push_inject1"; 

35 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

36 
val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g ==> f=g"; 
923  37 
by (rtac (major RS fun_cong RS ext RS box_equals) 1); 
38 
by (rtac (nat_case_Suc RS ext) 1); 

39 
by (rtac (nat_case_Suc RS ext) 1); 

40 
qed "Push_inject2"; 

41 

42 
val [major,minor] = goal Univ.thy 

43 
"[ Push i f =Push j g; [ i=j; f=g ] ==> P \ 

44 
\ ] ==> P"; 

45 
by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1); 

46 
qed "Push_inject"; 

47 

48 
val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P"; 

49 
by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1); 

50 
by (rtac nat_case_0 1); 

51 
by (rtac refl 1); 

52 
qed "Push_neq_K0"; 

53 

54 
(*** Isomorphisms ***) 

55 

56 
goal Univ.thy "inj(Rep_Node)"; 

1465  57 
by (rtac inj_inverseI 1); (*cannot combine by RS: multiple unifiers*) 
923  58 
by (rtac Rep_Node_inverse 1); 
59 
qed "inj_Rep_Node"; 

60 

61 
goal Univ.thy "inj_onto Abs_Node Node"; 

62 
by (rtac inj_onto_inverseI 1); 

63 
by (etac Abs_Node_inverse 1); 

64 
qed "inj_onto_Abs_Node"; 

65 

66 
val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD; 

67 

68 

69 
(*** Introduction rules for Node ***) 

70 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

71 
goalw Univ.thy [Node_def] "(%k. 0,a) : Node"; 
2891  72 
by (Blast_tac 1); 
923  73 
qed "Node_K0_I"; 
74 

75 
goalw Univ.thy [Node_def,Push_def] 

76 
"!!p. p: Node ==> apfst (Push i) p : Node"; 

2891  77 
by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1); 
923  78 
qed "Node_Push_I"; 
79 

80 

81 
(*** Distinctness of constructors ***) 

82 

83 
(** Scons vs Atom **) 

84 

85 
goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)"; 

86 
by (rtac notI 1); 

87 
by (etac (equalityD2 RS subsetD RS UnE) 1); 

88 
by (rtac singletonI 1); 

976
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

89 
by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, 
1465  90 
Pair_inject, sym RS Push_neq_K0] 1 
923  91 
ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1)); 
92 
qed "Scons_not_Atom"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

93 
bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym); 
923  94 

95 

96 
(*** Injectiveness ***) 

97 

98 
(** Atomic nodes **) 

99 

1563  100 
goalw Univ.thy [Atom_def, inj_def] "inj(Atom)"; 
2891  101 
by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1); 
923  102 
qed "inj_Atom"; 
103 
val Atom_inject = inj_Atom RS injD; 

104 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

105 
goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)"; 
2891  106 
by (blast_tac (!claset addSDs [Atom_inject]) 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

107 
qed "Atom_Atom_eq"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

108 
AddIffs [Atom_Atom_eq]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

109 

923  110 
goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)"; 
111 
by (rtac injI 1); 

112 
by (etac (Atom_inject RS Inl_inject) 1); 

113 
qed "inj_Leaf"; 

114 

115 
val Leaf_inject = inj_Leaf RS injD; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

116 
AddSDs [Leaf_inject]; 
923  117 

118 
goalw Univ.thy [Numb_def,o_def] "inj(Numb)"; 

119 
by (rtac injI 1); 

120 
by (etac (Atom_inject RS Inr_inject) 1); 

121 
qed "inj_Numb"; 

122 

123 
val Numb_inject = inj_Numb RS injD; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

124 
AddSDs [Numb_inject]; 
923  125 

126 
(** Injectiveness of Push_Node **) 

127 

128 
val [major,minor] = goalw Univ.thy [Push_Node_def] 

129 
"[ Push_Node i m =Push_Node j n; [ i=j; m=n ] ==> P \ 

130 
\ ] ==> P"; 

976
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

131 
by (rtac (major RS Abs_Node_inject RS apfst_convE) 1); 
923  132 
by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1)); 
976
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

133 
by (etac (sym RS apfst_convE) 1); 
923  134 
by (rtac minor 1); 
135 
by (etac Pair_inject 1); 

136 
by (etac (Push_inject1 RS sym) 1); 

137 
by (rtac (inj_Rep_Node RS injD) 1); 

138 
by (etac trans 1); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

139 
by (safe_tac (!claset addSEs [Push_inject,sym])); 
923  140 
qed "Push_Node_inject"; 
141 

142 

143 
(** Injectiveness of Scons **) 

144 

2891  145 
goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'"; 
146 
by (blast_tac (!claset addSDs [Push_Node_inject]) 1); 

923  147 
qed "Scons_inject_lemma1"; 
148 

2891  149 
goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'"; 
150 
by (fast_tac (!claset addSDs [Push_Node_inject]) 1); 

923  151 
qed "Scons_inject_lemma2"; 
152 

153 
val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'"; 

154 
by (rtac (major RS equalityE) 1); 

155 
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1)); 

156 
qed "Scons_inject1"; 

157 

158 
val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'"; 

159 
by (rtac (major RS equalityE) 1); 

160 
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1)); 

161 
qed "Scons_inject2"; 

162 

163 
val [major,minor] = goal Univ.thy 

164 
"[ M$N = M'$N'; [ M=M'; N=N' ] ==> P \ 

165 
\ ] ==> P"; 

166 
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1); 

167 
qed "Scons_inject"; 

168 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

169 
AddSDs [Scons_inject]; 
923  170 

171 
goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')"; 

2891  172 
by (blast_tac (!claset addSEs [Scons_inject]) 1); 
923  173 
qed "Scons_Scons_eq"; 
174 

175 
(*** Distinctness involving Leaf and Numb ***) 

176 

177 
(** Scons vs Leaf **) 

178 

179 
goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)"; 

180 
by (rtac Scons_not_Atom 1); 

181 
qed "Scons_not_Leaf"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

182 
bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym); 
923  183 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

184 
AddIffs [Scons_not_Leaf, Leaf_not_Scons]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

185 

923  186 

187 
(** Scons vs Numb **) 

188 

189 
goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)"; 

190 
by (rtac Scons_not_Atom 1); 

191 
qed "Scons_not_Numb"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

192 
bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym); 
923  193 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

194 
AddIffs [Scons_not_Numb, Numb_not_Scons]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

195 

923  196 

197 
(** Leaf vs Numb **) 

198 

199 
goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

200 
by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1); 
923  201 
qed "Leaf_not_Numb"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

202 
bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym); 
923  203 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

204 
AddIffs [Leaf_not_Numb, Numb_not_Leaf]; 
923  205 

206 

207 
(*** ndepth  the depth of a node ***) 

208 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

209 
Addsimps [apfst_conv]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

210 
AddIffs [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq]; 
923  211 

212 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

213 
goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0"; 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

214 
by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]); 
923  215 
by (rtac Least_equality 1); 
216 
by (rtac refl 1); 

217 
by (etac less_zeroE 1); 

218 
qed "ndepth_K0"; 

219 

220 
goal Univ.thy "k < Suc(LEAST x. f(x)=0) > nat_case (Suc i) f k ~= 0"; 

221 
by (nat_ind_tac "k" 1); 

1264  222 
by (ALLGOALS Simp_tac); 
923  223 
by (rtac impI 1); 
224 
by (etac not_less_Least 1); 

225 
qed "ndepth_Push_lemma"; 

226 

227 
goalw Univ.thy [ndepth_def,Push_Node_def] 

228 
"ndepth (Push_Node i n) = Suc(ndepth(n))"; 

229 
by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); 

230 
by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1761
diff
changeset

231 
by (safe_tac (!claset)); 
1465  232 
by (etac ssubst 1); (*instantiates type variables!*) 
1264  233 
by (Simp_tac 1); 
923  234 
by (rtac Least_equality 1); 
235 
by (rewtac Push_def); 

236 
by (rtac (nat_case_Suc RS trans) 1); 

237 
by (etac LeastI 1); 

238 
by (etac (ndepth_Push_lemma RS mp) 1); 

239 
qed "ndepth_Push_Node"; 

240 

241 

242 
(*** ntrunc applied to the various node sets ***) 

243 

244 
goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}"; 

2891  245 
by (Blast_tac 1); 
923  246 
qed "ntrunc_0"; 
247 

248 
goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

249 
by (fast_tac (!claset addss (!simpset addsimps [ndepth_K0])) 1); 
923  250 
qed "ntrunc_Atom"; 
251 

252 
goalw Univ.thy [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)"; 

253 
by (rtac ntrunc_Atom 1); 

254 
qed "ntrunc_Leaf"; 

255 

256 
goalw Univ.thy [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)"; 

257 
by (rtac ntrunc_Atom 1); 

258 
qed "ntrunc_Numb"; 

259 

260 
goalw Univ.thy [Scons_def,ntrunc_def] 

261 
"ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N"; 

2891  262 
by (safe_tac (!claset addSIs [equalityI, imageI])); 
923  263 
by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); 
264 
by (REPEAT (rtac Suc_less_SucD 1 THEN 

1465  265 
rtac (ndepth_Push_Node RS subst) 1 THEN 
266 
assume_tac 1)); 

923  267 
qed "ntrunc_Scons"; 
268 

269 
(** Injection nodes **) 

270 

271 
goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}"; 

1264  272 
by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1); 
923  273 
by (rewtac Scons_def); 
2891  274 
by (Blast_tac 1); 
923  275 
qed "ntrunc_one_In0"; 
276 

277 
goalw Univ.thy [In0_def] 

278 
"ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; 

1264  279 
by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1); 
923  280 
qed "ntrunc_In0"; 
281 

282 
goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}"; 

1264  283 
by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1); 
923  284 
by (rewtac Scons_def); 
2891  285 
by (Blast_tac 1); 
923  286 
qed "ntrunc_one_In1"; 
287 

288 
goalw Univ.thy [In1_def] 

289 
"ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"; 

1264  290 
by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1); 
923  291 
qed "ntrunc_In1"; 
292 

293 

294 
(*** Cartesian Product ***) 

295 

296 
goalw Univ.thy [uprod_def] "!!M N. [ M:A; N:B ] ==> (M$N) : A<*>B"; 

297 
by (REPEAT (ares_tac [singletonI,UN_I] 1)); 

298 
qed "uprodI"; 

299 

300 
(*The general elimination rule*) 

301 
val major::prems = goalw Univ.thy [uprod_def] 

302 
"[ c : A<*>B; \ 

303 
\ !!x y. [ x:A; y:B; c=x$y ] ==> P \ 

304 
\ ] ==> P"; 

305 
by (cut_facts_tac [major] 1); 

306 
by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1 

307 
ORELSE resolve_tac prems 1)); 

308 
qed "uprodE"; 

309 

310 
(*Elimination of a pair  introduces no eigenvariables*) 

311 
val prems = goal Univ.thy 

312 
"[ (M$N) : A<*>B; [ M:A; N:B ] ==> P \ 

313 
\ ] ==> P"; 

314 
by (rtac uprodE 1); 

315 
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1)); 

316 
qed "uprodE2"; 

317 

318 

319 
(*** Disjoint Sum ***) 

320 

321 
goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B"; 

2891  322 
by (Blast_tac 1); 
923  323 
qed "usum_In0I"; 
324 

325 
goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B"; 

2891  326 
by (Blast_tac 1); 
923  327 
qed "usum_In1I"; 
328 

329 
val major::prems = goalw Univ.thy [usum_def] 

330 
"[ u : A<+>B; \ 

331 
\ !!x. [ x:A; u=In0(x) ] ==> P; \ 

332 
\ !!y. [ y:B; u=In1(y) ] ==> P \ 

333 
\ ] ==> P"; 

334 
by (rtac (major RS UnE) 1); 

335 
by (REPEAT (rtac refl 1 

336 
ORELSE eresolve_tac (prems@[imageE,ssubst]) 1)); 

337 
qed "usumE"; 

338 

339 

340 
(** Injection **) 

341 

342 
goalw Univ.thy [In0_def,In1_def] "In0(M) ~= In1(N)"; 

343 
by (rtac notI 1); 

344 
by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1); 

345 
qed "In0_not_In1"; 

346 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

347 
bind_thm ("In1_not_In0", In0_not_In1 RS not_sym); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

348 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

349 
AddIffs [In0_not_In1, In1_not_In0]; 
923  350 

351 
val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==> M=N"; 

352 
by (rtac (major RS Scons_inject2) 1); 

353 
qed "In0_inject"; 

354 

355 
val [major] = goalw Univ.thy [In1_def] "In1(M) = In1(N) ==> M=N"; 

356 
by (rtac (major RS Scons_inject2) 1); 

357 
qed "In1_inject"; 

358 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

359 
AddSDs [In0_inject, In1_inject]; 
923  360 

361 
(*** proving equality of sets and functions using ntrunc ***) 

362 

363 
goalw Univ.thy [ntrunc_def] "ntrunc k M <= M"; 

2891  364 
by (Blast_tac 1); 
923  365 
qed "ntrunc_subsetI"; 
366 

367 
val [major] = goalw Univ.thy [ntrunc_def] 

368 
"(!!k. ntrunc k M <= N) ==> M<=N"; 

2891  369 
by (blast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
1465  370 
major RS subsetD]) 1); 
923  371 
qed "ntrunc_subsetD"; 
372 

373 
(*A generalized form of the takelemma*) 

374 
val [major] = goal Univ.thy "(!!k. ntrunc k M = ntrunc k N) ==> M=N"; 

375 
by (rtac equalityI 1); 

376 
by (ALLGOALS (rtac ntrunc_subsetD)); 

377 
by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans)))); 

378 
by (rtac (major RS equalityD1) 1); 

379 
by (rtac (major RS equalityD2) 1); 

380 
qed "ntrunc_equality"; 

381 

382 
val [major] = goalw Univ.thy [o_def] 

383 
"[ !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) ] ==> h1=h2"; 

384 
by (rtac (ntrunc_equality RS ext) 1); 

385 
by (rtac (major RS fun_cong) 1); 

386 
qed "ntrunc_o_equality"; 

387 

388 
(*** Monotonicity ***) 

389 

390 
goalw Univ.thy [uprod_def] "!!A B. [ A<=A'; B<=B' ] ==> A<*>B <= A'<*>B'"; 

2891  391 
by (Blast_tac 1); 
923  392 
qed "uprod_mono"; 
393 

394 
goalw Univ.thy [usum_def] "!!A B. [ A<=A'; B<=B' ] ==> A<+>B <= A'<+>B'"; 

2891  395 
by (Blast_tac 1); 
923  396 
qed "usum_mono"; 
397 

398 
goalw Univ.thy [Scons_def] "!!M N. [ M<=M'; N<=N' ] ==> M$N <= M'$N'"; 

2891  399 
by (Blast_tac 1); 
923  400 
qed "Scons_mono"; 
401 

402 
goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)"; 

403 
by (REPEAT (ares_tac [subset_refl,Scons_mono] 1)); 

404 
qed "In0_mono"; 

405 

406 
goalw Univ.thy [In1_def] "!!M N. M<=N ==> In1(M) <= In1(N)"; 

407 
by (REPEAT (ares_tac [subset_refl,Scons_mono] 1)); 

408 
qed "In1_mono"; 

409 

410 

411 
(*** Split and Case ***) 

412 

413 
goalw Univ.thy [Split_def] "Split c (M$N) = c M N"; 

2891  414 
by (blast_tac (!claset addIs [select_equality]) 1); 
923  415 
qed "Split"; 
416 

417 
goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)"; 

2891  418 
by (blast_tac (!claset addIs [select_equality]) 1); 
923  419 
qed "Case_In0"; 
420 

421 
goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)"; 

2891  422 
by (blast_tac (!claset addIs [select_equality]) 1); 
923  423 
qed "Case_In1"; 
424 

425 
(**** UN x. B(x) rules ****) 

426 

427 
goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))"; 

2891  428 
by (Blast_tac 1); 
923  429 
qed "ntrunc_UN1"; 
430 

431 
goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)"; 

2891  432 
by (Blast_tac 1); 
923  433 
qed "Scons_UN1_x"; 
434 

435 
goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))"; 

2891  436 
by (Blast_tac 1); 
923  437 
qed "Scons_UN1_y"; 
438 

439 
goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))"; 

1465  440 
by (rtac Scons_UN1_y 1); 
923  441 
qed "In0_UN1"; 
442 

443 
goalw Univ.thy [In1_def] "In1(UN x.f(x)) = (UN x. In1(f(x)))"; 

1465  444 
by (rtac Scons_UN1_y 1); 
923  445 
qed "In1_UN1"; 
446 

447 

448 
(*** Equality : the diagonal relation ***) 

449 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

450 
goalw Univ.thy [diag_def] "!!a A. [ a=b; a:A ] ==> (a,b) : diag(A)"; 
2891  451 
by (Blast_tac 1); 
923  452 
qed "diag_eqI"; 
453 

454 
val diagI = refl RS diag_eqI > standard; 

455 

456 
(*The general elimination rule*) 

457 
val major::prems = goalw Univ.thy [diag_def] 

458 
"[ c : diag(A); \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

459 
\ !!x y. [ x:A; c = (x,x) ] ==> P \ 
923  460 
\ ] ==> P"; 
461 
by (rtac (major RS UN_E) 1); 

462 
by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1)); 

463 
qed "diagE"; 

464 

465 
(*** Equality for Cartesian Product ***) 

466 

467 
goalw Univ.thy [dprod_def] 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

468 
"!!r s. [ (M,M'):r; (N,N'):s ] ==> (M$N, M'$N') : r<**>s"; 
2891  469 
by (Blast_tac 1); 
923  470 
qed "dprodI"; 
471 

472 
(*The general elimination rule*) 

473 
val major::prems = goalw Univ.thy [dprod_def] 

474 
"[ c : r<**>s; \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

475 
\ !!x y x' y'. [ (x,x') : r; (y,y') : s; c = (x$y,x'$y') ] ==> P \ 
923  476 
\ ] ==> P"; 
477 
by (cut_facts_tac [major] 1); 

478 
by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE])); 

479 
by (REPEAT (ares_tac prems 1 ORELSE hyp_subst_tac 1)); 

480 
qed "dprodE"; 

481 

482 

483 
(*** Equality for Disjoint Sum ***) 

484 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

485 
goalw Univ.thy [dsum_def] "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s"; 
2891  486 
by (Blast_tac 1); 
923  487 
qed "dsum_In0I"; 
488 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

489 
goalw Univ.thy [dsum_def] "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s"; 
2891  490 
by (Blast_tac 1); 
923  491 
qed "dsum_In1I"; 
492 

493 
val major::prems = goalw Univ.thy [dsum_def] 

494 
"[ w : r<++>s; \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

495 
\ !!x x'. [ (x,x') : r; w = (In0(x), In0(x')) ] ==> P; \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

496 
\ !!y y'. [ (y,y') : s; w = (In1(y), In1(y')) ] ==> P \ 
923  497 
\ ] ==> P"; 
498 
by (cut_facts_tac [major] 1); 

499 
by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE])); 

500 
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1)); 

501 
qed "dsumE"; 

502 

503 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset

504 
AddSIs [diagI, uprodI, dprodI]; 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset

505 
AddIs [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]; 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset

506 
AddSEs [diagE, uprodE, dprodE, usumE, dsumE]; 
923  507 

508 
(*** Monotonicity ***) 

509 

510 
goal Univ.thy "!!r s. [ r<=r'; s<=s' ] ==> r<**>s <= r'<**>s'"; 

2891  511 
by (Blast_tac 1); 
923  512 
qed "dprod_mono"; 
513 

514 
goal Univ.thy "!!r s. [ r<=r'; s<=s' ] ==> r<++>s <= r'<++>s'"; 

2891  515 
by (Blast_tac 1); 
923  516 
qed "dsum_mono"; 
517 

518 

519 
(*** Bounding theorems ***) 

520 

1642  521 
goal Univ.thy "diag(A) <= A Times A"; 
2891  522 
by (Blast_tac 1); 
923  523 
qed "diag_subset_Sigma"; 
524 

1642  525 
goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)"; 
2891  526 
by (Blast_tac 1); 
923  527 
qed "dprod_Sigma"; 
528 

529 
val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans >standard; 

530 

531 
(*Dependent version*) 

532 
goal Univ.thy 

533 
"(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))"; 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1761
diff
changeset

534 
by (safe_tac (!claset)); 
923  535 
by (stac Split 1); 
2891  536 
by (Blast_tac 1); 
923  537 
qed "dprod_subset_Sigma2"; 
538 

1642  539 
goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)"; 
2891  540 
by (Blast_tac 1); 
923  541 
qed "dsum_Sigma"; 
542 

543 
val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans > standard; 

544 

545 

546 
(*** Domain ***) 

547 

548 
goal Univ.thy "fst `` diag(A) = A"; 

2891  549 
by (Blast_tac 1); 
923  550 
qed "fst_image_diag"; 
551 

552 
goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)"; 

2891  553 
by (Blast_tac 1); 
923  554 
qed "fst_image_dprod"; 
555 

556 
goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)"; 

2891  557 
by (Blast_tac 1); 
923  558 
qed "fst_image_dsum"; 
559 

1264  560 
Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum]; 