equal
deleted
inserted
replaced
78 |
78 |
79 (*** Distinctness of constructors ***) |
79 (*** Distinctness of constructors ***) |
80 |
80 |
81 (** Scons vs Atom **) |
81 (** Scons vs Atom **) |
82 |
82 |
83 Goalw [Atom_def,Scons_def,Push_Node_def,One_def] |
83 Goalw [Atom_def,Scons_def,Push_Node_def,One_nat_def] |
84 "Scons M N ~= Atom(a)"; |
84 "Scons M N ~= Atom(a)"; |
85 by (rtac notI 1); |
85 by (rtac notI 1); |
86 by (etac (equalityD2 RS subsetD RS UnE) 1); |
86 by (etac (equalityD2 RS subsetD RS UnE) 1); |
87 by (rtac singletonI 1); |
87 by (rtac singletonI 1); |
88 by (REPEAT (eresolve_tac [imageE, Abs_Node_inj RS apfst_convE, |
88 by (REPEAT (eresolve_tac [imageE, Abs_Node_inj RS apfst_convE, |
139 qed "Push_Node_inject"; |
139 qed "Push_Node_inject"; |
140 |
140 |
141 |
141 |
142 (** Injectiveness of Scons **) |
142 (** Injectiveness of Scons **) |
143 |
143 |
144 Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> M<=M'"; |
144 Goalw [Scons_def,One_nat_def] "Scons M N <= Scons M' N' ==> M<=M'"; |
145 by (blast_tac (claset() addSDs [Push_Node_inject]) 1); |
145 by (blast_tac (claset() addSDs [Push_Node_inject]) 1); |
146 qed "Scons_inject_lemma1"; |
146 qed "Scons_inject_lemma1"; |
147 |
147 |
148 Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> N<=N'"; |
148 Goalw [Scons_def,One_nat_def] "Scons M N <= Scons M' N' ==> N<=N'"; |
149 by (blast_tac (claset() addSDs [Push_Node_inject]) 1); |
149 by (blast_tac (claset() addSDs [Push_Node_inject]) 1); |
150 qed "Scons_inject_lemma2"; |
150 qed "Scons_inject_lemma2"; |
151 |
151 |
152 Goal "Scons M N = Scons M' N' ==> M=M'"; |
152 Goal "Scons M N = Scons M' N' ==> M=M'"; |
153 by (etac equalityE 1); |
153 by (etac equalityE 1); |
250 |
250 |
251 Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)"; |
251 Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)"; |
252 by (rtac ntrunc_Atom 1); |
252 by (rtac ntrunc_Atom 1); |
253 qed "ntrunc_Numb"; |
253 qed "ntrunc_Numb"; |
254 |
254 |
255 Goalw [Scons_def,ntrunc_def,One_def] |
255 Goalw [Scons_def,ntrunc_def,One_nat_def] |
256 "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"; |
256 "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"; |
257 by (safe_tac (claset() addSIs [imageI])); |
257 by (safe_tac (claset() addSIs [imageI])); |
258 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); |
258 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); |
259 by (REPEAT (rtac Suc_less_SucD 1 THEN |
259 by (REPEAT (rtac Suc_less_SucD 1 THEN |
260 rtac (ndepth_Push_Node RS subst) 1 THEN |
260 rtac (ndepth_Push_Node RS subst) 1 THEN |
264 Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons]; |
264 Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons]; |
265 |
265 |
266 |
266 |
267 (** Injection nodes **) |
267 (** Injection nodes **) |
268 |
268 |
269 Goalw [In0_def] "ntrunc 1' (In0 M) = {}"; |
269 Goalw [In0_def] "ntrunc (Suc 0) (In0 M) = {}"; |
270 by (Simp_tac 1); |
270 by (Simp_tac 1); |
271 by (rewtac Scons_def); |
271 by (rewtac Scons_def); |
272 by (Blast_tac 1); |
272 by (Blast_tac 1); |
273 qed "ntrunc_one_In0"; |
273 qed "ntrunc_one_In0"; |
274 |
274 |
275 Goalw [In0_def] |
275 Goalw [In0_def] |
276 "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; |
276 "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; |
277 by (Simp_tac 1); |
277 by (Simp_tac 1); |
278 qed "ntrunc_In0"; |
278 qed "ntrunc_In0"; |
279 |
279 |
280 Goalw [In1_def] "ntrunc 1' (In1 M) = {}"; |
280 Goalw [In1_def] "ntrunc (Suc 0) (In1 M) = {}"; |
281 by (Simp_tac 1); |
281 by (Simp_tac 1); |
282 by (rewtac Scons_def); |
282 by (rewtac Scons_def); |
283 by (Blast_tac 1); |
283 by (Blast_tac 1); |
284 qed "ntrunc_one_In1"; |
284 qed "ntrunc_one_In1"; |
285 |
285 |
337 qed "usumE"; |
337 qed "usumE"; |
338 |
338 |
339 |
339 |
340 (** Injection **) |
340 (** Injection **) |
341 |
341 |
342 Goalw [In0_def,In1_def,One_def] "In0(M) ~= In1(N)"; |
342 Goalw [In0_def,In1_def,One_nat_def] "In0(M) ~= In1(N)"; |
343 by (rtac notI 1); |
343 by (rtac notI 1); |
344 by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1); |
344 by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1); |
345 qed "In0_not_In1"; |
345 qed "In0_not_In1"; |
346 |
346 |
347 bind_thm ("In1_not_In0", In0_not_In1 RS not_sym); |
347 bind_thm ("In1_not_In0", In0_not_In1 RS not_sym); |