author  berghofe 
Fri, 16 Jul 1999 12:09:48 +0200  
changeset 7014  11ee650edcd2 
parent 6171  cd237a10cbf8 
child 7088  a94c9e226c20 
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 

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

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"; 
923  217 
by (nat_ind_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 

5069  270 
Goalw [In0_def] "ntrunc (Suc 0) (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 

5069  281 
Goalw [In1_def] "ntrunc (Suc 0) (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 

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

297 
Goalw [uprod_def] "[ M:A; N:B ] ==> Scons M N : 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] 
923  303 
"[ c : 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 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
5148
diff
changeset

313 
"[ Scons M N : 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 

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

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

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

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

5316  330 
val major::prems = Goalw [usum_def] 
923  331 
"[ u : A<+>B; \ 
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"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

407 
br CollectI 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

408 
br subsetI 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

409 
be rangeE 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

410 
be ssubst 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

411 
br p 1; 
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"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

415 
be CollectE 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

416 
be subsetD 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

417 
br rangeI 1; 
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"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

422 
br ext 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

423 
br p2 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

424 
br (p1 RS FunsD) 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

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

426 

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

427 
val [p1, p2] = Goalw [o_def] "[ f : Funs (range g); !!h. f = g o h ==> P ] ==> P"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

428 
by (cut_facts_tac [p1] 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

429 
by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

430 
br ext 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

431 
bd FunsD 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

432 
be rangeE 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

433 
be (exI RS (select_eq_Ex RS iffD2)) 1; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6171
diff
changeset

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

435 

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

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

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

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

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

440 

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

441 

923  442 
(*** proving equality of sets and functions using ntrunc ***) 
443 

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

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

453 
(*A generalized form of the takelemma*) 

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

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

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

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

460 
qed "ntrunc_equality"; 

461 

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

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

466 
qed "ntrunc_o_equality"; 

467 

468 
(*** Monotonicity ***) 

469 

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

470 
Goalw [uprod_def] "[ A<=A'; B<=B' ] ==> A<*>B <= A'<*>B'"; 
2891  471 
by (Blast_tac 1); 
923  472 
qed "uprod_mono"; 
473 

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

474 
Goalw [usum_def] "[ A<=A'; B<=B' ] ==> A<+>B <= A'<+>B'"; 
2891  475 
by (Blast_tac 1); 
923  476 
qed "usum_mono"; 
477 

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

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

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

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

485 

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

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

489 

490 

491 
(*** Split and Case ***) 

492 

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

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

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

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

4521  505 
Addsimps [Split, Case_In0, Case_In1]; 
506 

507 

923  508 
(**** UN x. B(x) rules ****) 
509 

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

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

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

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

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

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

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

530 

531 
(*** Equality for Cartesian Product ***) 

532 

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

534 
"[ (M,M'):r; (N,N'):s ] ==> (Scons M N, Scons M' N') : r<**>s"; 
2891  535 
by (Blast_tac 1); 
923  536 
qed "dprodI"; 
537 

538 
(*The general elimination rule*) 

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

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

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

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

546 
qed "dprodE"; 

547 

548 

549 
(*** Equality for Disjoint Sum ***) 

550 

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

551 
Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : r<++>s"; 
2891  552 
by (Blast_tac 1); 
923  553 
qed "dsum_In0I"; 
554 

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

555 
Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : r<++>s"; 
2891  556 
by (Blast_tac 1); 
923  557 
qed "dsum_In1I"; 
558 

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

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

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

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

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

567 
qed "dsumE"; 

568 

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

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

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

571 
AddSEs [uprodE, dprodE, usumE, dsumE]; 
923  572 

573 

574 
(*** Monotonicity ***) 

575 

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

576 
Goal "[ r<=r'; s<=s' ] ==> r<**>s <= r'<**>s'"; 
2891  577 
by (Blast_tac 1); 
923  578 
qed "dprod_mono"; 
579 

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

580 
Goal "[ r<=r'; s<=s' ] ==> r<++>s <= r'<++>s'"; 
2891  581 
by (Blast_tac 1); 
923  582 
qed "dsum_mono"; 
583 

584 

585 
(*** Bounding theorems ***) 

586 

5069  587 
Goal "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)"; 
2891  588 
by (Blast_tac 1); 
923  589 
qed "dprod_Sigma"; 
590 

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

592 

593 
(*Dependent version*) 

5278  594 
Goal "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))"; 
4153  595 
by Safe_tac; 
923  596 
by (stac Split 1); 
2891  597 
by (Blast_tac 1); 
923  598 
qed "dprod_subset_Sigma2"; 
599 

5069  600 
Goal "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)"; 
2891  601 
by (Blast_tac 1); 
923  602 
qed "dsum_Sigma"; 
603 

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

605 

606 

607 
(*** Domain ***) 

608 

5788  609 
Goal "Domain (r<**>s) = (Domain r) <*> (Domain s)"; 
4521  610 
by Auto_tac; 
5788  611 
qed "Domain_dprod"; 
923  612 

5788  613 
Goal "Domain (r<++>s) = (Domain r) <+> (Domain s)"; 
4521  614 
by Auto_tac; 
5788  615 
qed "Domain_dsum"; 
923  616 

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

617 
Addsimps [Domain_dprod, Domain_dsum]; 