author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8790  c4aaa5936e0c 
child 9108  9fff97d29837 
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 

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

8 

5069  9 
Goalw [apfst_def] "apfst f (a,b) = (f(a),b)"; 
923  10 
by (rtac split 1); 
976
14b55f7fbf15
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
clasohm
parents:
972
diff
changeset

11 
qed "apfst_conv"; 
923  12 

5316  13 
val [major,minor] = Goal 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

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

17 
by (rtac minor 1); 

18 
by (assume_tac 1); 

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

20 
by (etac ssubst 1); 

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

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

22 
qed "apfst_convE"; 
923  23 

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

25 

5316  26 
Goalw [Push_def] "Push i f = Push j g ==> i=j"; 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

27 
by (etac (fun_cong RS box_equals) 1); 
923  28 
by (rtac nat_case_0 1); 
29 
by (rtac nat_case_0 1); 

30 
qed "Push_inject1"; 

31 

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

34 
by (etac fun_cong 1); 

923  35 
by (rtac (nat_case_Suc RS ext) 1); 
36 
by (rtac (nat_case_Suc RS ext) 1); 

37 
qed "Push_inject2"; 

38 

5316  39 
val [major,minor] = Goal 
923  40 
"[ Push i f =Push j g; [ i=j; f=g ] ==> P \ 
41 
\ ] ==> P"; 

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

43 
qed "Push_inject"; 

44 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

45 
Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

46 
by (rtac Suc_neq_Zero 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

47 
by (etac (fun_cong RS box_equals RS Inr_inject) 1); 
923  48 
by (rtac nat_case_0 1); 
49 
by (rtac refl 1); 

50 
qed "Push_neq_K0"; 

51 

52 
(*** Isomorphisms ***) 

53 

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

58 

5069  59 
Goal "inj_on Abs_Node Node"; 
4830  60 
by (rtac inj_on_inverseI 1); 
923  61 
by (etac Abs_Node_inverse 1); 
4830  62 
qed "inj_on_Abs_Node"; 
923  63 

4830  64 
val Abs_Node_inject = inj_on_Abs_Node RS inj_onD; 
923  65 

66 

67 
(*** Introduction rules for Node ***) 

68 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

69 
Goalw [Node_def] "(%k. Inr 0, a) : Node"; 
2891  70 
by (Blast_tac 1); 
923  71 
qed "Node_K0_I"; 
72 

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

74 
"p: Node ==> apfst (Push i) p : Node"; 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

75 
by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); 
923  76 
qed "Node_Push_I"; 
77 

78 

79 
(*** Distinctness of constructors ***) 

80 

81 
(** Scons vs Atom **) 

82 

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

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

86 
by (rtac singletonI 1); 

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

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

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

91 
bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym); 
923  92 

93 

94 
(*** Injectiveness ***) 

95 

96 
(** Atomic nodes **) 

97 

6171  98 
Goalw [Atom_def] "inj(Atom)"; 
99 
by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1); 

923  100 
qed "inj_Atom"; 
101 
val Atom_inject = inj_Atom RS injD; 

102 

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

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

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

107 

5069  108 
Goalw [Leaf_def,o_def] "inj(Leaf)"; 
923  109 
by (rtac injI 1); 
110 
by (etac (Atom_inject RS Inl_inject) 1); 

111 
qed "inj_Leaf"; 

112 

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

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

114 
AddSDs [Leaf_inject]; 
923  115 

5069  116 
Goalw [Numb_def,o_def] "inj(Numb)"; 
923  117 
by (rtac injI 1); 
118 
by (etac (Atom_inject RS Inr_inject) 1); 

119 
qed "inj_Numb"; 

120 

121 
val Numb_inject = inj_Numb RS injD; 

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

122 
AddSDs [Numb_inject]; 
923  123 

124 
(** Injectiveness of Push_Node **) 

125 

5316  126 
val [major,minor] = Goalw [Push_Node_def] 
923  127 
"[ Push_Node i m =Push_Node j n; [ i=j; m=n ] ==> P \ 
128 
\ ] ==> P"; 

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

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

131 
by (etac (sym RS apfst_convE) 1); 
923  132 
by (rtac minor 1); 
133 
by (etac Pair_inject 1); 

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

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

136 
by (etac trans 1); 

4089  137 
by (safe_tac (claset() addSEs [Push_inject,sym])); 
923  138 
qed "Push_Node_inject"; 
139 

140 

141 
(** Injectiveness of Scons **) 

142 

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

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

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

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

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

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

155 

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

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

160 

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

162 
"[ Scons M N = Scons M' N'; [ M=M'; N=N' ] ==> P \ 
923  163 
\ ] ==> P"; 
164 
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1); 

165 
qed "Scons_inject"; 

166 

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

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

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

172 

173 
(** Scons vs Leaf **) 

174 

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

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

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

178 
bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym); 
923  179 

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

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

181 

923  182 

183 
(** Scons vs Numb **) 

184 

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

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

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

188 
bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym); 
923  189 

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

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

191 

923  192 

193 
(** Leaf vs Numb **) 

194 

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

198 
bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym); 
923  199 

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

200 
AddIffs [Leaf_not_Numb, Numb_not_Leaf]; 
923  201 

202 

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

204 

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

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

206 
AddIffs [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq]; 
923  207 

208 

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

210 
by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]); 
923  211 
by (rtac Least_equality 1); 
212 
by (rtac refl 1); 

213 
by (etac less_zeroE 1); 

214 
qed "ndepth_K0"; 

215 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

216 
Goal "k < Suc(LEAST x. f x = Inr 0) > nat_case (Inr (Suc i)) f k ~= Inr 0"; 
8709  217 
by (induct_tac "k" 1); 
1264  218 
by (ALLGOALS Simp_tac); 
923  219 
by (rtac impI 1); 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

220 
by (etac not_less_Least 1); 
4356  221 
val lemma = result(); 
923  222 

5069  223 
Goalw [ndepth_def,Push_Node_def] 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

224 
"ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"; 
923  225 
by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); 
226 
by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); 

4153  227 
by Safe_tac; 
1465  228 
by (etac ssubst 1); (*instantiates type variables!*) 
1264  229 
by (Simp_tac 1); 
923  230 
by (rtac Least_equality 1); 
231 
by (rewtac Push_def); 

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

233 
by (etac LeastI 1); 

4356  234 
by (asm_simp_tac (simpset() addsimps [lemma]) 1); 
923  235 
qed "ndepth_Push_Node"; 
236 

237 

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

239 

5069  240 
Goalw [ntrunc_def] "ntrunc 0 M = {}"; 
2891  241 
by (Blast_tac 1); 
923  242 
qed "ntrunc_0"; 
243 

5069  244 
Goalw [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)"; 
4089  245 
by (fast_tac (claset() addss (simpset() addsimps [ndepth_K0])) 1); 
923  246 
qed "ntrunc_Atom"; 
247 

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

251 

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

255 

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

257 
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"; 
4089  258 
by (safe_tac (claset() addSIs [imageI])); 
923  259 
by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); 
260 
by (REPEAT (rtac Suc_less_SucD 1 THEN 

1465  261 
rtac (ndepth_Push_Node RS subst) 1 THEN 
262 
assume_tac 1)); 

923  263 
qed "ntrunc_Scons"; 
264 

4521  265 
Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons]; 
266 

267 

923  268 
(** Injection nodes **) 
269 

8790  270 
Goalw [In0_def] "ntrunc 1 (In0 M) = {}"; 
4521  271 
by (Simp_tac 1); 
923  272 
by (rewtac Scons_def); 
2891  273 
by (Blast_tac 1); 
923  274 
qed "ntrunc_one_In0"; 
275 

5069  276 
Goalw [In0_def] 
923  277 
"ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; 
4521  278 
by (Simp_tac 1); 
923  279 
qed "ntrunc_In0"; 
280 

8790  281 
Goalw [In1_def] "ntrunc 1 (In1 M) = {}"; 
4521  282 
by (Simp_tac 1); 
923  283 
by (rewtac Scons_def); 
2891  284 
by (Blast_tac 1); 
923  285 
qed "ntrunc_one_In1"; 
286 

5069  287 
Goalw [In1_def] 
923  288 
"ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"; 
4521  289 
by (Simp_tac 1); 
923  290 
qed "ntrunc_In1"; 
291 

4521  292 
Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1]; 
293 

923  294 

295 
(*** Cartesian Product ***) 

296 

7255  297 
Goalw [uprod_def] "[ M:A; N:B ] ==> Scons M N : uprod A B"; 
923  298 
by (REPEAT (ares_tac [singletonI,UN_I] 1)); 
299 
qed "uprodI"; 

300 

301 
(*The general elimination rule*) 

5316  302 
val major::prems = Goalw [uprod_def] 
7255  303 
"[ c : uprod A B; \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

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

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

308 
ORELSE resolve_tac prems 1)); 

309 
qed "uprodE"; 

310 

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

5316  312 
val prems = Goal 
7255  313 
"[ Scons M N : uprod A B; [ M:A; N:B ] ==> P \ 
923  314 
\ ] ==> P"; 
315 
by (rtac uprodE 1); 

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

317 
qed "uprodE2"; 

318 

319 

320 
(*** Disjoint Sum ***) 

321 

7255  322 
Goalw [usum_def] "M:A ==> In0(M) : usum A B"; 
2891  323 
by (Blast_tac 1); 
923  324 
qed "usum_In0I"; 
325 

7255  326 
Goalw [usum_def] "N:B ==> In1(N) : usum A B"; 
2891  327 
by (Blast_tac 1); 
923  328 
qed "usum_In1I"; 
329 

5316  330 
val major::prems = Goalw [usum_def] 
7255  331 
"[ u : usum A B; \ 
923  332 
\ !!x. [ x:A; u=In0(x) ] ==> P; \ 
333 
\ !!y. [ y:B; u=In1(y) ] ==> P \ 

334 
\ ] ==> P"; 

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

336 
by (REPEAT (rtac refl 1 

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

338 
qed "usumE"; 

339 

340 

341 
(** Injection **) 

342 

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

346 
qed "In0_not_In1"; 

347 

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

348 
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

349 

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

350 
AddIffs [In0_not_In1, In1_not_In0]; 
923  351 

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

923  354 
qed "In0_inject"; 
355 

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

923  358 
qed "In1_inject"; 
359 

5069  360 
Goal "(In0 M = In0 N) = (M=N)"; 
4089  361 
by (blast_tac (claset() addSDs [In0_inject]) 1); 
3421  362 
qed "In0_eq"; 
363 

5069  364 
Goal "(In1 M = In1 N) = (M=N)"; 
4089  365 
by (blast_tac (claset() addSDs [In1_inject]) 1); 
3421  366 
qed "In1_eq"; 
367 

368 
AddIffs [In0_eq, In1_eq]; 

369 

6171  370 
Goal "inj In0"; 
371 
by (blast_tac (claset() addSIs [injI]) 1); 

3421  372 
qed "inj_In0"; 
373 

6171  374 
Goal "inj In1"; 
375 
by (blast_tac (claset() addSIs [injI]) 1); 

3421  376 
qed "inj_In1"; 
377 

923  378 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

379 
(*** Function spaces ***) 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

380 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

381 
Goalw [Lim_def] "Lim f = Lim g ==> f = g"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

382 
by (rtac ext 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

383 
by (rtac ccontr 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

384 
by (etac equalityE 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

385 
by (subgoal_tac "? y. y : f x & y ~: g x  y ~: f x & y : g x" 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

386 
by (Blast_tac 2); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

387 
by (etac exE 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

388 
by (etac disjE 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

389 
by (REPEAT (EVERY [ 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

390 
dtac subsetD 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

391 
Fast_tac 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

392 
etac UnionE 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

393 
dtac CollectD 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

394 
etac exE 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

395 
hyp_subst_tac 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

396 
etac imageE 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

397 
etac Push_Node_inject 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

398 
Asm_full_simp_tac 1, 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

399 
TRY (thin_tac "?S <= ?T" 1)])); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

400 
qed "Lim_inject"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

401 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

402 
Goalw [Funs_def] "S <= T ==> Funs S <= Funs T"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

403 
by (Blast_tac 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

404 
qed "Funs_mono"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

405 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

406 
val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S"; 
7088  407 
by (rtac CollectI 1); 
408 
by (rtac subsetI 1); 

409 
by (etac rangeE 1); 

410 
by (etac ssubst 1); 

411 
by (rtac p 1); 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

412 
qed "FunsI"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

413 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

414 
Goalw [Funs_def] "f : Funs S ==> f x : S"; 
7088  415 
by (etac CollectE 1); 
416 
by (etac subsetD 1); 

417 
by (rtac rangeI 1); 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

418 
qed "FunsD"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

419 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

420 
val [p1, p2] = goalw thy [o_def] 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

421 
"[ f : Funs R; !!x. x : R ==> r (a x) = x ] ==> r o (a o f) = f"; 
7088  422 
by (rtac (p2 RS ext) 1); 
423 
by (rtac (p1 RS FunsD) 1); 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

424 
qed "Funs_inv"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

425 

7088  426 
val [p1, p2] = Goalw [o_def] 
427 
"[ f : Funs (range g); !!h. f = g o h ==> P ] ==> P"; 

8292
93e125b21220
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
wenzelm
parents:
8114
diff
changeset

428 
by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1); 
7088  429 
by (rtac ext 1); 
430 
by (rtac (p1 RS FunsD RS rangeE) 1); 

431 
by (etac (exI RS (select_eq_Ex RS iffD2)) 1); 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

432 
qed "Funs_rangeE"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

433 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

434 
Goal "a : S ==> (%x. a) : Funs S"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

435 
by (rtac FunsI 1); 
7088  436 
by (assume_tac 1); 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

437 
qed "Funs_nonempty"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

438 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

439 

923  440 
(*** proving equality of sets and functions using ntrunc ***) 
441 

5069  442 
Goalw [ntrunc_def] "ntrunc k M <= M"; 
2891  443 
by (Blast_tac 1); 
923  444 
qed "ntrunc_subsetI"; 
445 

5316  446 
val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N"; 
4089  447 
by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
4521  448 
major RS subsetD]) 1); 
923  449 
qed "ntrunc_subsetD"; 
450 

451 
(*A generalized form of the takelemma*) 

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

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

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

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

458 
qed "ntrunc_equality"; 

459 

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

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

464 
qed "ntrunc_o_equality"; 

465 

466 
(*** Monotonicity ***) 

467 

7255  468 
Goalw [uprod_def] "[ A<=A'; B<=B' ] ==> uprod A B <= uprod A' B'"; 
2891  469 
by (Blast_tac 1); 
923  470 
qed "uprod_mono"; 
471 

7255  472 
Goalw [usum_def] "[ A<=A'; B<=B' ] ==> usum A B <= usum A' B'"; 
2891  473 
by (Blast_tac 1); 
923  474 
qed "usum_mono"; 
475 

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

476 
Goalw [Scons_def] "[ M<=M'; N<=N' ] ==> Scons M N <= Scons M' N'"; 
2891  477 
by (Blast_tac 1); 
923  478 
qed "Scons_mono"; 
479 

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

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

483 

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

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

487 

488 

489 
(*** Split and Case ***) 

490 

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

491 
Goalw [Split_def] "Split c (Scons M N) = c M N"; 
4535  492 
by (Blast_tac 1); 
923  493 
qed "Split"; 
494 

5069  495 
Goalw [Case_def] "Case c d (In0 M) = c(M)"; 
4535  496 
by (Blast_tac 1); 
923  497 
qed "Case_In0"; 
498 

5069  499 
Goalw [Case_def] "Case c d (In1 N) = d(N)"; 
4535  500 
by (Blast_tac 1); 
923  501 
qed "Case_In1"; 
502 

4521  503 
Addsimps [Split, Case_In0, Case_In1]; 
504 

505 

923  506 
(**** UN x. B(x) rules ****) 
507 

5069  508 
Goalw [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"; 
2891  509 
by (Blast_tac 1); 
923  510 
qed "ntrunc_UN1"; 
511 

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

512 
Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)"; 
2891  513 
by (Blast_tac 1); 
923  514 
qed "Scons_UN1_x"; 
515 

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

516 
Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))"; 
2891  517 
by (Blast_tac 1); 
923  518 
qed "Scons_UN1_y"; 
519 

5069  520 
Goalw [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))"; 
1465  521 
by (rtac Scons_UN1_y 1); 
923  522 
qed "In0_UN1"; 
523 

5069  524 
Goalw [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))"; 
1465  525 
by (rtac Scons_UN1_y 1); 
923  526 
qed "In1_UN1"; 
527 

528 

529 
(*** Equality for Cartesian Product ***) 

530 

5069  531 
Goalw [dprod_def] 
7255  532 
"[ (M,M'):r; (N,N'):s ] ==> (Scons M N, Scons M' N') : dprod r s"; 
2891  533 
by (Blast_tac 1); 
923  534 
qed "dprodI"; 
535 

536 
(*The general elimination rule*) 

5316  537 
val major::prems = Goalw [dprod_def] 
7255  538 
"[ c : dprod r s; \ 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

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

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

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

544 
qed "dprodE"; 

545 

546 

547 
(*** Equality for Disjoint Sum ***) 

548 

7255  549 
Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"; 
2891  550 
by (Blast_tac 1); 
923  551 
qed "dsum_In0I"; 
552 

7255  553 
Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"; 
2891  554 
by (Blast_tac 1); 
923  555 
qed "dsum_In1I"; 
556 

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

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

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

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

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

565 
qed "dsumE"; 

566 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5809
diff
changeset

567 
AddSIs [uprodI, dprodI]; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5809
diff
changeset

568 
AddIs [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5809
diff
changeset

569 
AddSEs [uprodE, dprodE, usumE, dsumE]; 
923  570 

571 

572 
(*** Monotonicity ***) 

573 

7255  574 
Goal "[ r<=r'; s<=s' ] ==> dprod r s <= dprod r' s'"; 
2891  575 
by (Blast_tac 1); 
923  576 
qed "dprod_mono"; 
577 

7255  578 
Goal "[ r<=r'; s<=s' ] ==> dsum r s <= dsum r' s'"; 
2891  579 
by (Blast_tac 1); 
923  580 
qed "dsum_mono"; 
581 

582 

583 
(*** Bounding theorems ***) 

584 

8703  585 
Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"; 
2891  586 
by (Blast_tac 1); 
923  587 
qed "dprod_Sigma"; 
588 

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

590 

591 
(*Dependent version*) 

7255  592 
Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"; 
4153  593 
by Safe_tac; 
923  594 
by (stac Split 1); 
2891  595 
by (Blast_tac 1); 
923  596 
qed "dprod_subset_Sigma2"; 
597 

8703  598 
Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"; 
2891  599 
by (Blast_tac 1); 
923  600 
qed "dsum_Sigma"; 
601 

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

603 

604 

605 
(*** Domain ***) 

606 

7255  607 
Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)"; 
4521  608 
by Auto_tac; 
5788  609 
qed "Domain_dprod"; 
923  610 

7255  611 
Goal "Domain (dsum r s) = usum (Domain r) (Domain s)"; 
4521  612 
by Auto_tac; 
5788  613 
qed "Domain_dsum"; 
923  614 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5809
diff
changeset

615 
Addsimps [Domain_dprod, Domain_dsum]; 