|
1 (* Title: CCL/ccl |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 For ccl.thy. |
|
7 *) |
|
8 |
|
9 open CCL; |
|
10 |
|
11 val ccl_data_defs = [apply_def,fix_def]; |
|
12 |
|
13 (*** Simplifier for pre-order and equality ***) |
|
14 |
|
15 structure CCL_SimpData : SIMP_DATA = |
|
16 struct |
|
17 val refl_thms = [refl, po_refl, iff_refl] |
|
18 val trans_thms = [trans, iff_trans, po_trans] |
|
19 val red1 = iffD1 |
|
20 val red2 = iffD2 |
|
21 val mk_rew_rules = mk_rew_rules |
|
22 val case_splits = [] (*NO IF'S!*) |
|
23 val norm_thms = norm_thms |
|
24 val subst_thms = [subst]; |
|
25 val dest_red = dest_red |
|
26 end; |
|
27 |
|
28 structure CCL_Simp = SimpFun(CCL_SimpData); |
|
29 open CCL_Simp; |
|
30 |
|
31 val auto_ss = empty_ss setauto (fn hyps => ares_tac (TrueI::hyps)); |
|
32 |
|
33 val po_refl_iff_T = make_iff_T po_refl; |
|
34 |
|
35 val CCL_ss = auto_ss addcongs (FOL_congs @ set_congs) |
|
36 addrews ([po_refl_iff_T] @ FOL_rews @ mem_rews); |
|
37 |
|
38 (*** Congruence Rules ***) |
|
39 |
|
40 (*similar to AP_THM in Gordon's HOL*) |
|
41 val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" |
|
42 (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); |
|
43 |
|
44 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) |
|
45 val arg_cong = prove_goal CCL.thy "x=y ==> f(x)=f(y)" |
|
46 (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); |
|
47 |
|
48 goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))"; |
|
49 by (SIMP_TAC (CCL_ss addrews [eq_iff]) 1); |
|
50 by (fast_tac (set_cs addIs [po_abstractn]) 1); |
|
51 val abstractn = standard (allI RS (result() RS mp)); |
|
52 |
|
53 fun type_of_terms (Const("Trueprop",_) $ |
|
54 (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t; |
|
55 |
|
56 fun abs_prems thm = |
|
57 let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t |
|
58 | do_abs n thm _ = thm |
|
59 fun do_prems n [] thm = thm |
|
60 | do_prems n (x::xs) thm = do_prems (n+1) xs (do_abs n thm (type_of_terms x)); |
|
61 in do_prems 1 (prems_of thm) thm |
|
62 end; |
|
63 |
|
64 fun ccl_mk_congs thy cs = map abs_prems (mk_congs thy cs); |
|
65 |
|
66 val ccl_congs = ccl_mk_congs CCL.thy |
|
67 ["op [=","SIM","POgen","EQgen","pair","lambda","case","op `","fix"]; |
|
68 |
|
69 val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot]; |
|
70 |
|
71 (*** Termination and Divergence ***) |
|
72 |
|
73 goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot"; |
|
74 br iff_refl 1; |
|
75 val Trm_iff = result(); |
|
76 |
|
77 goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot"; |
|
78 br iff_refl 1; |
|
79 val Dvg_iff = result(); |
|
80 |
|
81 (*** Constructors are injective ***) |
|
82 |
|
83 val prems = goal CCL.thy |
|
84 "[| x=a; y=b; x=y |] ==> a=b"; |
|
85 by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals])))); |
|
86 val eq_lemma = result(); |
|
87 |
|
88 fun mk_inj_rl thy rews congs s = |
|
89 let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]); |
|
90 val inj_lemmas = flat (map mk_inj_lemmas rews); |
|
91 val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE |
|
92 eresolve_tac inj_lemmas 1 ORELSE |
|
93 ASM_SIMP_TAC (CCL_ss addrews rews |
|
94 addcongs congs) 1) |
|
95 in prove_goal thy s (fn _ => [tac]) |
|
96 end; |
|
97 |
|
98 val ccl_injs = map (mk_inj_rl CCL.thy caseBs ccl_congs) |
|
99 ["<a,b> = <a',b'> <-> (a=a' & b=b')", |
|
100 "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"]; |
|
101 |
|
102 val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE; |
|
103 |
|
104 (*** Constructors are distinct ***) |
|
105 |
|
106 local |
|
107 fun pairs_of f x [] = [] |
|
108 | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys); |
|
109 |
|
110 fun mk_combs ff [] = [] |
|
111 | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs; |
|
112 |
|
113 (* Doesn't handle binder types correctly *) |
|
114 fun saturate thy sy name = |
|
115 let fun arg_str 0 a s = s |
|
116 | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")" |
|
117 | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s); |
|
118 val sg = sign_of thy; |
|
119 val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),sy) of |
|
120 None => error(sy^" not declared") | Some(T) => T; |
|
121 val arity = length (fst (strip_type T)); |
|
122 in sy ^ (arg_str arity name "") end; |
|
123 |
|
124 fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b"); |
|
125 |
|
126 val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)" |
|
127 (fn _ => [SIMP_TAC (CCL_ss addcongs ccl_congs) 1]) RS mp; |
|
128 fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL |
|
129 [distinctness RS notE,sym RS (distinctness RS notE)]; |
|
130 in |
|
131 fun mk_lemmas rls = flat (map mk_lemma (mk_combs pair rls)); |
|
132 fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs; |
|
133 end; |
|
134 |
|
135 |
|
136 val caseB_lemmas = mk_lemmas caseBs; |
|
137 |
|
138 val ccl_dstncts = |
|
139 let fun mk_raw_dstnct_thm rls s = |
|
140 prove_goal CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1]) |
|
141 in map (mk_raw_dstnct_thm caseB_lemmas) |
|
142 (mk_dstnct_rls CCL.thy ["bot","true","false","pair","lambda"]) end; |
|
143 |
|
144 fun mk_dstnct_thms thy defs inj_rls xs = |
|
145 let fun mk_dstnct_thm rls s = prove_goalw thy defs s |
|
146 (fn _ => [SIMP_TAC (CCL_ss addrews (rls@inj_rls)) 1]) |
|
147 in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end; |
|
148 |
|
149 fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss); |
|
150 |
|
151 (*** Rewriting and Proving ***) |
|
152 |
|
153 fun XH_to_I rl = rl RS iffD2; |
|
154 fun XH_to_D rl = rl RS iffD1; |
|
155 val XH_to_E = make_elim o XH_to_D; |
|
156 val XH_to_Is = map XH_to_I; |
|
157 val XH_to_Ds = map XH_to_D; |
|
158 val XH_to_Es = map XH_to_E; |
|
159 |
|
160 val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts; |
|
161 val ccl_ss = CCL_ss addrews ccl_rews addcongs ccl_congs; |
|
162 |
|
163 val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) |
|
164 addSDs (XH_to_Ds ccl_injs); |
|
165 |
|
166 (****** Facts from gfp Definition of [= and = ******) |
|
167 |
|
168 val major::prems = goal Set.thy "[| A=B; a:B <-> P |] ==> a:A <-> P"; |
|
169 brs (prems RL [major RS ssubst]) 1; |
|
170 val XHlemma1 = result(); |
|
171 |
|
172 goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> & P(t,t')} <-> Q)"; |
|
173 by (fast_tac ccl_cs 1); |
|
174 val XHlemma2 = result() RS mp; |
|
175 |
|
176 (*** Pre-Order ***) |
|
177 |
|
178 goalw CCL.thy [POgen_def,SIM_def] "mono(%X.POgen(X))"; |
|
179 br monoI 1; |
|
180 by (safe_tac ccl_cs); |
|
181 by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); |
|
182 by (ALLGOALS (SIMP_TAC ccl_ss)); |
|
183 by (ALLGOALS (fast_tac set_cs)); |
|
184 val POgen_mono = result(); |
|
185 |
|
186 goalw CCL.thy [POgen_def,SIM_def] |
|
187 "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | \ |
|
188 \ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \ |
|
189 \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"; |
|
190 br (iff_refl RS XHlemma2) 1; |
|
191 val POgenXH = result(); |
|
192 |
|
193 goal CCL.thy |
|
194 "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \ |
|
195 \ (EX a a' b b'.t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \ |
|
196 \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))"; |
|
197 by (SIMP_TAC (ccl_ss addrews [PO_iff]) 1); |
|
198 br (rewrite_rule [POgen_def,SIM_def] |
|
199 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1; |
|
200 br (iff_refl RS XHlemma2) 1; |
|
201 val poXH = result(); |
|
202 |
|
203 goal CCL.thy "bot [= b"; |
|
204 br (poXH RS iffD2) 1; |
|
205 by (SIMP_TAC ccl_ss 1); |
|
206 val po_bot = result(); |
|
207 |
|
208 goal CCL.thy "a [= bot --> a=bot"; |
|
209 br impI 1; |
|
210 bd (poXH RS iffD1) 1; |
|
211 be rev_mp 1; |
|
212 by (SIMP_TAC ccl_ss 1); |
|
213 val bot_poleast = result() RS mp; |
|
214 |
|
215 goal CCL.thy "<a,b> [= <a',b'> <-> a [= a' & b [= b'"; |
|
216 br (poXH RS iff_trans) 1; |
|
217 by (SIMP_TAC ccl_ss 1); |
|
218 by (fast_tac ccl_cs 1); |
|
219 val po_pair = result(); |
|
220 |
|
221 goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))"; |
|
222 br (poXH RS iff_trans) 1; |
|
223 by (SIMP_TAC ccl_ss 1); |
|
224 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1)); |
|
225 by (ASM_SIMP_TAC ccl_ss 1); |
|
226 by (fast_tac ccl_cs 1); |
|
227 val po_lam = result(); |
|
228 |
|
229 val ccl_porews = [po_bot,po_pair,po_lam]; |
|
230 |
|
231 val [p1,p2,p3,p4,p5] = goal CCL.thy |
|
232 "[| t [= t'; a [= a'; b [= b'; !!x y.c(x,y) [= c'(x,y); \ |
|
233 \ !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')"; |
|
234 br (p1 RS po_cong RS po_trans) 1; |
|
235 br (p2 RS po_cong RS po_trans) 1; |
|
236 br (p3 RS po_cong RS po_trans) 1; |
|
237 br (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1; |
|
238 by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] |
|
239 (p5 RS po_abstractn RS po_cong RS po_trans) 1); |
|
240 br po_refl 1; |
|
241 val case_pocong = result(); |
|
242 |
|
243 val [p1,p2] = goalw CCL.thy ccl_data_defs |
|
244 "[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'"; |
|
245 by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1)); |
|
246 val apply_pocong = result(); |
|
247 |
|
248 |
|
249 val prems = goal CCL.thy "~ lam x.b(x) [= bot"; |
|
250 br notI 1; |
|
251 bd bot_poleast 1; |
|
252 be (distinctness RS notE) 1; |
|
253 val npo_lam_bot = result(); |
|
254 |
|
255 val eq1::eq2::prems = goal CCL.thy |
|
256 "[| x=a; y=b; x[=y |] ==> a[=b"; |
|
257 br (eq1 RS subst) 1; |
|
258 br (eq2 RS subst) 1; |
|
259 brs prems 1; |
|
260 val po_lemma = result(); |
|
261 |
|
262 goal CCL.thy "~ <a,b> [= lam x.f(x)"; |
|
263 br notI 1; |
|
264 br (npo_lam_bot RS notE) 1; |
|
265 be (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1; |
|
266 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); |
|
267 val npo_pair_lam = result(); |
|
268 |
|
269 goal CCL.thy "~ lam x.f(x) [= <a,b>"; |
|
270 br notI 1; |
|
271 br (npo_lam_bot RS notE) 1; |
|
272 be (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1; |
|
273 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); |
|
274 val npo_lam_pair = result(); |
|
275 |
|
276 fun mk_thm s = prove_goal CCL.thy s (fn _ => |
|
277 [rtac notI 1,dtac case_pocong 1,etac rev_mp 5, |
|
278 ALLGOALS (SIMP_TAC ccl_ss), |
|
279 REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]); |
|
280 |
|
281 val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm |
|
282 ["~ true [= false", "~ false [= true", |
|
283 "~ true [= <a,b>", "~ <a,b> [= true", |
|
284 "~ true [= lam x.f(x)","~ lam x.f(x) [= true", |
|
285 "~ false [= <a,b>", "~ <a,b> [= false", |
|
286 "~ false [= lam x.f(x)","~ lam x.f(x) [= false"]; |
|
287 |
|
288 (* Coinduction for [= *) |
|
289 |
|
290 val prems = goal CCL.thy "[| <t,u> : R; R <= POgen(R) |] ==> t [= u"; |
|
291 br (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1; |
|
292 by (REPEAT (ares_tac prems 1)); |
|
293 val po_coinduct = result(); |
|
294 |
|
295 fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i; |
|
296 |
|
297 (*************** EQUALITY *******************) |
|
298 |
|
299 goalw CCL.thy [EQgen_def,SIM_def] "mono(%X.EQgen(X))"; |
|
300 br monoI 1; |
|
301 by (safe_tac set_cs); |
|
302 by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); |
|
303 by (ALLGOALS (SIMP_TAC ccl_ss)); |
|
304 by (ALLGOALS (fast_tac set_cs)); |
|
305 val EQgen_mono = result(); |
|
306 |
|
307 goalw CCL.thy [EQgen_def,SIM_def] |
|
308 "<t,t'> : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | \ |
|
309 \ (t=false & t'=false) | \ |
|
310 \ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \ |
|
311 \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"; |
|
312 br (iff_refl RS XHlemma2) 1; |
|
313 val EQgenXH = result(); |
|
314 |
|
315 goal CCL.thy |
|
316 "t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \ |
|
317 \ (EX a a' b b'.t=<a,b> & t'=<a',b'> & a=a' & b=b') | \ |
|
318 \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))"; |
|
319 by (subgoal_tac |
|
320 "<t,t'> : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \ |
|
321 \ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | \ |
|
322 \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1); |
|
323 be rev_mp 1; |
|
324 by (SIMP_TAC (CCL_ss addrews [EQ_iff RS iff_sym]) 1); |
|
325 br (rewrite_rule [EQgen_def,SIM_def] |
|
326 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1; |
|
327 br (iff_refl RS XHlemma2) 1; |
|
328 val eqXH = result(); |
|
329 |
|
330 val prems = goal CCL.thy "[| <t,u> : R; R <= EQgen(R) |] ==> t = u"; |
|
331 br (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1; |
|
332 by (REPEAT (ares_tac prems 1)); |
|
333 val eq_coinduct = result(); |
|
334 |
|
335 val prems = goal CCL.thy |
|
336 "[| <t,u> : R; R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u"; |
|
337 br (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1; |
|
338 by (REPEAT (ares_tac (EQgen_mono::prems) 1)); |
|
339 val eq_coinduct3 = result(); |
|
340 |
|
341 fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i; |
|
342 fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i; |
|
343 |
|
344 (*** Untyped Case Analysis and Other Facts ***) |
|
345 |
|
346 goalw CCL.thy [apply_def] "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)"; |
|
347 by (safe_tac ccl_cs); |
|
348 by (SIMP_TAC ccl_ss 1); |
|
349 val cond_eta = result() RS mp; |
|
350 |
|
351 goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))"; |
|
352 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1); |
|
353 by (fast_tac set_cs 1); |
|
354 val exhaustion = result(); |
|
355 |
|
356 val prems = goal CCL.thy |
|
357 "[| P(bot); P(true); P(false); !!x y.P(<x,y>); !!b.P(lam x.b(x)) |] ==> P(t)"; |
|
358 by (cut_facts_tac [exhaustion] 1); |
|
359 by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst])); |
|
360 val term_case = result(); |
|
361 |
|
362 fun term_case_tac a i = res_inst_tac [("t",a)] term_case i; |