author  paulson 
Thu, 13 Aug 1998 18:14:26 +0200  
changeset 5316  7a8975451a89 
parent 5278  a903b66822e2 
child 5788  e3a98a7c0634 
permissions  rwrr 
2935  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 

5069  13 
Goalw [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 

5316  17 
val [major,minor] = Goal 
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 

5316  30 
Goalw [Push_def] "Push i f = Push j g ==> i=j"; 
31 
by (etac (fun_cong RS box_equals RS Suc_inject) 1); 

923  32 
by (rtac nat_case_0 1); 
33 
by (rtac nat_case_0 1); 

34 
qed "Push_inject1"; 

35 

5316  36 
Goalw [Push_def] "Push i f = Push j g ==> f=g"; 
37 
by (rtac (ext RS box_equals) 1); 

38 
by (etac fun_cong 1); 

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

41 
qed "Push_inject2"; 

42 

5316  43 
val [major,minor] = Goal 
923  44 
"[ Push i f =Push j g; [ i=j; f=g ] ==> P \ 
45 
\ ] ==> P"; 

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

47 
qed "Push_inject"; 

48 

5316  49 
Goalw [Push_def] "Push k f =(%z.0) ==> P"; 
50 
by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1); 

923  51 
by (rtac nat_case_0 1); 
52 
by (rtac refl 1); 

53 
qed "Push_neq_K0"; 

54 

55 
(*** Isomorphisms ***) 

56 

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

61 

5069  62 
Goal "inj_on Abs_Node Node"; 
4830  63 
by (rtac inj_on_inverseI 1); 
923  64 
by (etac Abs_Node_inverse 1); 
4830  65 
qed "inj_on_Abs_Node"; 
923  66 

4830  67 
val Abs_Node_inject = inj_on_Abs_Node RS inj_onD; 
923  68 

69 

70 
(*** Introduction rules for Node ***) 

71 

5069  72 
Goalw [Node_def] "(%k. 0,a) : Node"; 
2891  73 
by (Blast_tac 1); 
923  74 
qed "Node_K0_I"; 
75 

5069  76 
Goalw [Node_def,Push_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

77 
"p: Node ==> apfst (Push i) p : Node"; 
4089  78 
by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); 
923  79 
qed "Node_Push_I"; 
80 

81 

82 
(*** Distinctness of constructors ***) 

83 

84 
(** Scons vs Atom **) 

85 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

86 
Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)"; 
923  87 
by (rtac notI 1); 
88 
by (etac (equalityD2 RS subsetD RS UnE) 1); 

89 
by (rtac singletonI 1); 

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

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

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

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

96 

97 
(*** Injectiveness ***) 

98 

99 
(** Atomic nodes **) 

100 

5069  101 
Goalw [Atom_def, inj_def] "inj(Atom)"; 
4089  102 
by (blast_tac (claset() addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1); 
923  103 
qed "inj_Atom"; 
104 
val Atom_inject = inj_Atom RS injD; 

105 

5069  106 
Goal "(Atom(a)=Atom(b)) = (a=b)"; 
4089  107 
by (blast_tac (claset() addSDs [Atom_inject]) 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

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

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

110 

5069  111 
Goalw [Leaf_def,o_def] "inj(Leaf)"; 
923  112 
by (rtac injI 1); 
113 
by (etac (Atom_inject RS Inl_inject) 1); 

114 
qed "inj_Leaf"; 

115 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

116 
bind_thm ("Leaf_inject", inj_Leaf RS injD); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

117 
AddSDs [Leaf_inject]; 
923  118 

5069  119 
Goalw [Numb_def,o_def] "inj(Numb)"; 
923  120 
by (rtac injI 1); 
121 
by (etac (Atom_inject RS Inr_inject) 1); 

122 
qed "inj_Numb"; 

123 

124 
val Numb_inject = inj_Numb RS injD; 

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

125 
AddSDs [Numb_inject]; 
923  126 

127 
(** Injectiveness of Push_Node **) 

128 

5316  129 
val [major,minor] = Goalw [Push_Node_def] 
923  130 
"[ Push_Node i m =Push_Node j n; [ i=j; m=n ] ==> P \ 
131 
\ ] ==> P"; 

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

132 
by (rtac (major RS Abs_Node_inject RS apfst_convE) 1); 
923  133 
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

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

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

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

139 
by (etac trans 1); 

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

143 

144 
(** Injectiveness of Scons **) 

145 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

146 
Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'"; 
4089  147 
by (blast_tac (claset() addSDs [Push_Node_inject]) 1); 
923  148 
qed "Scons_inject_lemma1"; 
149 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

150 
Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'"; 
4089  151 
by (blast_tac (claset() addSDs [Push_Node_inject]) 1); 
923  152 
qed "Scons_inject_lemma2"; 
153 

5316  154 
Goal "Scons M N = Scons M' N' ==> M=M'"; 
155 
by (etac equalityE 1); 

923  156 
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1)); 
157 
qed "Scons_inject1"; 

158 

5316  159 
Goal "Scons M N = Scons M' N' ==> N=N'"; 
160 
by (etac equalityE 1); 

923  161 
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1)); 
162 
qed "Scons_inject2"; 

163 

5316  164 
val [major,minor] = Goal 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

165 
"[ Scons M N = Scons M' N'; [ M=M'; N=N' ] ==> P \ 
923  166 
\ ] ==> P"; 
167 
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1); 

168 
qed "Scons_inject"; 

169 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

170 
Goal "(Scons M N = Scons M' N') = (M=M' & N=N')"; 
4089  171 
by (blast_tac (claset() addSEs [Scons_inject]) 1); 
923  172 
qed "Scons_Scons_eq"; 
173 

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

175 

176 
(** Scons vs Leaf **) 

177 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

178 
Goalw [Leaf_def,o_def] "Scons M N ~= Leaf(a)"; 
923  179 
by (rtac Scons_not_Atom 1); 
180 
qed "Scons_not_Leaf"; 

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

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

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

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

184 

923  185 

186 
(** Scons vs Numb **) 

187 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

188 
Goalw [Numb_def,o_def] "Scons M N ~= Numb(k)"; 
923  189 
by (rtac Scons_not_Atom 1); 
190 
qed "Scons_not_Numb"; 

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

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

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

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

194 

923  195 

196 
(** Leaf vs Numb **) 

197 

5069  198 
Goalw [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)"; 
4089  199 
by (simp_tac (simpset() addsimps [Inl_not_Inr]) 1); 
923  200 
qed "Leaf_not_Numb"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1786
diff
changeset

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

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

203 
AddIffs [Leaf_not_Numb, Numb_not_Leaf]; 
923  204 

205 

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

207 

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

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

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

211 

5069  212 
Goalw [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

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

216 
by (etac less_zeroE 1); 

217 
qed "ndepth_K0"; 

218 

5069  219 
Goal "k < Suc(LEAST x. f(x)=0) > 0 < nat_case (Suc i) f k"; 
923  220 
by (nat_ind_tac "k" 1); 
1264  221 
by (ALLGOALS Simp_tac); 
923  222 
by (rtac impI 1); 
4356  223 
by (dtac not_less_Least 1); 
224 
by (Asm_full_simp_tac 1); 

225 
val lemma = result(); 

923  226 

5069  227 
Goalw [ndepth_def,Push_Node_def] 
923  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); 

4153  231 
by Safe_tac; 
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); 

4356  238 
by (asm_simp_tac (simpset() addsimps [lemma]) 1); 
923  239 
qed "ndepth_Push_Node"; 
240 

241 

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

243 

5069  244 
Goalw [ntrunc_def] "ntrunc 0 M = {}"; 
2891  245 
by (Blast_tac 1); 
923  246 
qed "ntrunc_0"; 
247 

5069  248 
Goalw [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)"; 
4089  249 
by (fast_tac (claset() addss (simpset() addsimps [ndepth_K0])) 1); 
923  250 
qed "ntrunc_Atom"; 
251 

5069  252 
Goalw [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)"; 
923  253 
by (rtac ntrunc_Atom 1); 
254 
qed "ntrunc_Leaf"; 

255 

5069  256 
Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)"; 
923  257 
by (rtac ntrunc_Atom 1); 
258 
qed "ntrunc_Numb"; 

259 

5069  260 
Goalw [Scons_def,ntrunc_def] 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

261 
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"; 
4089  262 
by (safe_tac (claset() addSIs [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 

4521  269 
Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons]; 
270 

271 

923  272 
(** Injection nodes **) 
273 

5069  274 
Goalw [In0_def] "ntrunc (Suc 0) (In0 M) = {}"; 
4521  275 
by (Simp_tac 1); 
923  276 
by (rewtac Scons_def); 
2891  277 
by (Blast_tac 1); 
923  278 
qed "ntrunc_one_In0"; 
279 

5069  280 
Goalw [In0_def] 
923  281 
"ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; 
4521  282 
by (Simp_tac 1); 
923  283 
qed "ntrunc_In0"; 
284 

5069  285 
Goalw [In1_def] "ntrunc (Suc 0) (In1 M) = {}"; 
4521  286 
by (Simp_tac 1); 
923  287 
by (rewtac Scons_def); 
2891  288 
by (Blast_tac 1); 
923  289 
qed "ntrunc_one_In1"; 
290 

5069  291 
Goalw [In1_def] 
923  292 
"ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"; 
4521  293 
by (Simp_tac 1); 
923  294 
qed "ntrunc_In1"; 
295 

4521  296 
Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1]; 
297 

923  298 

299 
(*** Cartesian Product ***) 

300 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

301 
Goalw [uprod_def] "[ M:A; N:B ] ==> Scons M N : A<*>B"; 
923  302 
by (REPEAT (ares_tac [singletonI,UN_I] 1)); 
303 
qed "uprodI"; 

304 

305 
(*The general elimination rule*) 

5316  306 
val major::prems = Goalw [uprod_def] 
923  307 
"[ c : A<*>B; \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

308 
\ !!x y. [ x:A; y:B; c = Scons x y ] ==> P \ 
923  309 
\ ] ==> P"; 
310 
by (cut_facts_tac [major] 1); 

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

312 
ORELSE resolve_tac prems 1)); 

313 
qed "uprodE"; 

314 

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

5316  316 
val prems = Goal 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

317 
"[ Scons M N : A<*>B; [ M:A; N:B ] ==> P \ 
923  318 
\ ] ==> P"; 
319 
by (rtac uprodE 1); 

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

321 
qed "uprodE2"; 

322 

323 

324 
(*** Disjoint Sum ***) 

325 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

326 
Goalw [usum_def] "M:A ==> In0(M) : A<+>B"; 
2891  327 
by (Blast_tac 1); 
923  328 
qed "usum_In0I"; 
329 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

330 
Goalw [usum_def] "N:B ==> In1(N) : A<+>B"; 
2891  331 
by (Blast_tac 1); 
923  332 
qed "usum_In1I"; 
333 

5316  334 
val major::prems = Goalw [usum_def] 
923  335 
"[ u : A<+>B; \ 
336 
\ !!x. [ x:A; u=In0(x) ] ==> P; \ 

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

338 
\ ] ==> P"; 

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

340 
by (REPEAT (rtac refl 1 

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

342 
qed "usumE"; 

343 

344 

345 
(** Injection **) 

346 

5069  347 
Goalw [In0_def,In1_def] "In0(M) ~= In1(N)"; 
923  348 
by (rtac notI 1); 
349 
by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1); 

350 
qed "In0_not_In1"; 

351 

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

352 
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

353 

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

354 
AddIffs [In0_not_In1, In1_not_In0]; 
923  355 

5316  356 
Goalw [In0_def] "In0(M) = In0(N) ==> M=N"; 
357 
by (etac (Scons_inject2) 1); 

923  358 
qed "In0_inject"; 
359 

5316  360 
Goalw [In1_def] "In1(M) = In1(N) ==> M=N"; 
361 
by (etac (Scons_inject2) 1); 

923  362 
qed "In1_inject"; 
363 

5069  364 
Goal "(In0 M = In0 N) = (M=N)"; 
4089  365 
by (blast_tac (claset() addSDs [In0_inject]) 1); 
3421  366 
qed "In0_eq"; 
367 

5069  368 
Goal "(In1 M = In1 N) = (M=N)"; 
4089  369 
by (blast_tac (claset() addSDs [In1_inject]) 1); 
3421  370 
qed "In1_eq"; 
371 

372 
AddIffs [In0_eq, In1_eq]; 

373 

5069  374 
Goalw [inj_def] "inj In0"; 
3421  375 
by (Blast_tac 1); 
376 
qed "inj_In0"; 

377 

5069  378 
Goalw [inj_def] "inj In1"; 
3421  379 
by (Blast_tac 1); 
380 
qed "inj_In1"; 

381 

923  382 

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

384 

5069  385 
Goalw [ntrunc_def] "ntrunc k M <= M"; 
2891  386 
by (Blast_tac 1); 
923  387 
qed "ntrunc_subsetI"; 
388 

5316  389 
val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N"; 
4089  390 
by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
4521  391 
major RS subsetD]) 1); 
923  392 
qed "ntrunc_subsetD"; 
393 

394 
(*A generalized form of the takelemma*) 

5316  395 
val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N"; 
923  396 
by (rtac equalityI 1); 
397 
by (ALLGOALS (rtac ntrunc_subsetD)); 

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

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

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

401 
qed "ntrunc_equality"; 

402 

5316  403 
val [major] = Goalw [o_def] 
923  404 
"[ !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) ] ==> h1=h2"; 
405 
by (rtac (ntrunc_equality RS ext) 1); 

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

407 
qed "ntrunc_o_equality"; 

408 

409 
(*** Monotonicity ***) 

410 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

411 
Goalw [uprod_def] "[ A<=A'; B<=B' ] ==> A<*>B <= A'<*>B'"; 
2891  412 
by (Blast_tac 1); 
923  413 
qed "uprod_mono"; 
414 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

415 
Goalw [usum_def] "[ A<=A'; B<=B' ] ==> A<+>B <= A'<+>B'"; 
2891  416 
by (Blast_tac 1); 
923  417 
qed "usum_mono"; 
418 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

419 
Goalw [Scons_def] "[ M<=M'; N<=N' ] ==> Scons M N <= Scons M' N'"; 
2891  420 
by (Blast_tac 1); 
923  421 
qed "Scons_mono"; 
422 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

423 
Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)"; 
923  424 
by (REPEAT (ares_tac [subset_refl,Scons_mono] 1)); 
425 
qed "In0_mono"; 

426 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

427 
Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)"; 
923  428 
by (REPEAT (ares_tac [subset_refl,Scons_mono] 1)); 
429 
qed "In1_mono"; 

430 

431 

432 
(*** Split and Case ***) 

433 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

434 
Goalw [Split_def] "Split c (Scons M N) = c M N"; 
4535  435 
by (Blast_tac 1); 
923  436 
qed "Split"; 
437 

5069  438 
Goalw [Case_def] "Case c d (In0 M) = c(M)"; 
4535  439 
by (Blast_tac 1); 
923  440 
qed "Case_In0"; 
441 

5069  442 
Goalw [Case_def] "Case c d (In1 N) = d(N)"; 
4535  443 
by (Blast_tac 1); 
923  444 
qed "Case_In1"; 
445 

4521  446 
Addsimps [Split, Case_In0, Case_In1]; 
447 

448 

923  449 
(**** UN x. B(x) rules ****) 
450 

5069  451 
Goalw [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"; 
2891  452 
by (Blast_tac 1); 
923  453 
qed "ntrunc_UN1"; 
454 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

455 
Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)"; 
2891  456 
by (Blast_tac 1); 
923  457 
qed "Scons_UN1_x"; 
458 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

459 
Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))"; 
2891  460 
by (Blast_tac 1); 
923  461 
qed "Scons_UN1_y"; 
462 

5069  463 
Goalw [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))"; 
1465  464 
by (rtac Scons_UN1_y 1); 
923  465 
qed "In0_UN1"; 
466 

5069  467 
Goalw [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))"; 
1465  468 
by (rtac Scons_UN1_y 1); 
923  469 
qed "In1_UN1"; 
470 

471 

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

473 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

474 
Goalw [diag_def] "[ a=b; a:A ] ==> (a,b) : diag(A)"; 
2891  475 
by (Blast_tac 1); 
923  476 
qed "diag_eqI"; 
477 

478 
val diagI = refl RS diag_eqI > standard; 

479 

480 
(*The general elimination rule*) 

5316  481 
val major::prems = Goalw [diag_def] 
923  482 
"[ c : diag(A); \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

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

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

487 
qed "diagE"; 

488 

489 
(*** Equality for Cartesian Product ***) 

490 

5069  491 
Goalw [dprod_def] 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

492 
"[ (M,M'):r; (N,N'):s ] ==> (Scons M N, Scons M' N') : r<**>s"; 
2891  493 
by (Blast_tac 1); 
923  494 
qed "dprodI"; 
495 

496 
(*The general elimination rule*) 

5316  497 
val major::prems = Goalw [dprod_def] 
923  498 
"[ c : r<**>s; \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

499 
\ !!x y x' y'. [ (x,x') : r; (y,y') : s; c = (Scons x y, Scons x' y') ] ==> P \ 
923  500 
\ ] ==> P"; 
501 
by (cut_facts_tac [major] 1); 

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

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

504 
qed "dprodE"; 

505 

506 

507 
(*** Equality for Disjoint Sum ***) 

508 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

509 
Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : r<++>s"; 
2891  510 
by (Blast_tac 1); 
923  511 
qed "dsum_In0I"; 
512 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

513 
Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : r<++>s"; 
2891  514 
by (Blast_tac 1); 
923  515 
qed "dsum_In1I"; 
516 

5316  517 
val major::prems = Goalw [dsum_def] 
923  518 
"[ w : r<++>s; \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

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

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

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

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

525 
qed "dsumE"; 

526 

527 

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

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

529 
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

530 
AddSEs [diagE, uprodE, dprodE, usumE, dsumE]; 
923  531 

532 
(*** Monotonicity ***) 

533 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

534 
Goal "[ r<=r'; s<=s' ] ==> r<**>s <= r'<**>s'"; 
2891  535 
by (Blast_tac 1); 
923  536 
qed "dprod_mono"; 
537 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

538 
Goal "[ r<=r'; s<=s' ] ==> r<++>s <= r'<++>s'"; 
2891  539 
by (Blast_tac 1); 
923  540 
qed "dsum_mono"; 
541 

542 

543 
(*** Bounding theorems ***) 

544 

5069  545 
Goal "diag(A) <= A Times A"; 
2891  546 
by (Blast_tac 1); 
923  547 
qed "diag_subset_Sigma"; 
548 

5069  549 
Goal "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)"; 
2891  550 
by (Blast_tac 1); 
923  551 
qed "dprod_Sigma"; 
552 

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

554 

555 
(*Dependent version*) 

5278  556 
Goal "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))"; 
4153  557 
by Safe_tac; 
923  558 
by (stac Split 1); 
2891  559 
by (Blast_tac 1); 
923  560 
qed "dprod_subset_Sigma2"; 
561 

5069  562 
Goal "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)"; 
2891  563 
by (Blast_tac 1); 
923  564 
qed "dsum_Sigma"; 
565 

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

567 

568 

569 
(*** Domain ***) 

570 

5069  571 
Goal "fst `` diag(A) = A"; 
4521  572 
by Auto_tac; 
923  573 
qed "fst_image_diag"; 
574 

5069  575 
Goal "fst `` (r<**>s) = (fst``r) <*> (fst``s)"; 
4521  576 
by Auto_tac; 
923  577 
qed "fst_image_dprod"; 
578 

5069  579 
Goal "fst `` (r<++>s) = (fst``r) <+> (fst``s)"; 
4521  580 
by Auto_tac; 
923  581 
qed "fst_image_dsum"; 
582 

1264  583 
Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum]; 