0
|
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;
|