|
1 signature QUOTIENT_TACS = |
|
2 sig |
|
3 val regularize_tac: Proof.context -> int -> tactic |
|
4 val all_inj_repabs_tac: Proof.context -> int -> tactic |
|
5 val clean_tac: Proof.context -> int -> tactic |
|
6 val procedure_tac: Proof.context -> thm -> int -> tactic |
|
7 val lift_tac: Proof.context ->thm -> int -> tactic |
|
8 val quotient_tac: Proof.context -> int -> tactic |
|
9 end; |
|
10 |
|
11 structure Quotient_Tacs: QUOTIENT_TACS = |
|
12 struct |
|
13 |
|
14 (* Since HOL_basic_ss is too "big" for us, *) |
|
15 (* we need to set up our own minimal simpset. *) |
|
16 fun mk_minimal_ss ctxt = |
|
17 Simplifier.context ctxt empty_ss |
|
18 setsubgoaler asm_simp_tac |
|
19 setmksimps (mksimps []) |
|
20 |
|
21 |
|
22 |
|
23 (* various helper functions *) |
|
24 fun OF1 thm1 thm2 = thm2 RS thm1 |
|
25 |
|
26 (* makes sure a subgoal is solved *) |
|
27 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
|
28 |
|
29 (* prints warning, if goal is unsolved *) |
|
30 fun WARN (tac, msg) i st = |
|
31 case Seq.pull ((SOLVES' tac) i st) of |
|
32 NONE => (warning msg; Seq.single st) |
|
33 | seqcell => Seq.make (fn () => seqcell) |
|
34 |
|
35 fun RANGE_WARN xs = RANGE (map WARN xs) |
|
36 |
|
37 fun atomize_thm thm = |
|
38 let |
|
39 val thm' = Thm.freezeT (forall_intr_vars thm) |
|
40 val thm'' = ObjectLogic.atomize (cprop_of thm') |
|
41 in |
|
42 @{thm equal_elim_rule1} OF [thm'', thm'] |
|
43 end |
|
44 |
|
45 |
|
46 |
|
47 |
|
48 (* Regularize Tactic *) |
|
49 |
|
50 fun equiv_tac ctxt = |
|
51 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
|
52 |
|
53 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
|
54 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
|
55 |
|
56 fun prep_trm thy (x, (T, t)) = |
|
57 (cterm_of thy (Var (x, T)), cterm_of thy t) |
|
58 |
|
59 fun prep_ty thy (x, (S, ty)) = |
|
60 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
|
61 |
|
62 fun matching_prs thy pat trm = |
|
63 let |
|
64 val univ = Unify.matchers thy [(pat, trm)] |
|
65 val SOME (env, _) = Seq.pull univ |
|
66 val tenv = Vartab.dest (Envir.term_env env) |
|
67 val tyenv = Vartab.dest (Envir.type_env env) |
|
68 in |
|
69 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
|
70 end |
|
71 |
|
72 fun calculate_instance ctxt thm redex R1 R2 = |
|
73 let |
|
74 val thy = ProofContext.theory_of ctxt |
|
75 val goal = Const (@{const_name "equivp"}, dummyT) $ R2 |
|
76 |> Syntax.check_term ctxt |
|
77 |> HOLogic.mk_Trueprop |
|
78 val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) |
|
79 val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) |
|
80 val R1c = cterm_of thy R1 |
|
81 val thmi = Drule.instantiate' [] [SOME R1c] thm |
|
82 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
|
83 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) |
|
84 in |
|
85 SOME thm2 |
|
86 end |
|
87 handle _ => NONE |
|
88 (* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) |
|
89 |
|
90 fun ball_bex_range_simproc ss redex = |
|
91 let |
|
92 val ctxt = Simplifier.the_context ss |
|
93 in |
|
94 case redex of |
|
95 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
|
96 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
|
97 calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 |
|
98 |
|
99 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
|
100 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
|
101 calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 |
|
102 | _ => NONE |
|
103 end |
|
104 |
|
105 (* test whether DETERM makes any difference *) |
|
106 fun quotient_tac ctxt = SOLVES' |
|
107 (REPEAT_ALL_NEW (FIRST' |
|
108 [rtac @{thm identity_quotient}, |
|
109 resolve_tac (quotient_rules_get ctxt)])) |
|
110 |
|
111 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
112 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
113 |
|
114 fun solve_quotient_assum ctxt thm = |
|
115 case Seq.pull (quotient_tac ctxt 1 thm) of |
|
116 SOME (t, _) => t |
|
117 | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" |
|
118 |
|
119 |
|
120 (* 0. preliminary simplification step according to *) |
|
121 (* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) |
|
122 (* ball_reg_eqv_range bex_reg_eqv_range *) |
|
123 (* *) |
|
124 (* 1. eliminating simple Ball/Bex instances *) |
|
125 (* thm ball_reg_right bex_reg_left *) |
|
126 (* *) |
|
127 (* 2. monos *) |
|
128 (* 3. commutation rules for ball and bex *) |
|
129 (* thm ball_all_comm bex_ex_comm *) |
|
130 (* *) |
|
131 (* 4. then rel-equality (which need to be *) |
|
132 (* instantiated to avoid loops) *) |
|
133 (* thm eq_imp_rel *) |
|
134 (* *) |
|
135 (* 5. then simplification like 0 *) |
|
136 (* *) |
|
137 (* finally jump back to 1 *) |
|
138 |
|
139 fun regularize_tac ctxt = |
|
140 let |
|
141 val thy = ProofContext.theory_of ctxt |
|
142 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
|
143 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
|
144 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
|
145 val simpset = (mk_minimal_ss ctxt) |
|
146 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
|
147 addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver |
|
148 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
|
149 in |
|
150 simp_tac simpset THEN' |
|
151 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
|
152 resolve_tac @{thms ball_reg_right bex_reg_left}, |
|
153 resolve_tac (Inductive.get_monos ctxt), |
|
154 resolve_tac @{thms ball_all_comm bex_ex_comm}, |
|
155 resolve_tac eq_eqvs, |
|
156 simp_tac simpset]) |
|
157 end |
|
158 |
|
159 |
|
160 |
|
161 (* Injection Tactic *) |
|
162 |
|
163 (* looks for QUOT_TRUE assumtions, and in case its parameter *) |
|
164 (* is an application, it returns the function and the argument *) |
|
165 fun find_qt_asm asms = |
|
166 let |
|
167 fun find_fun trm = |
|
168 case trm of |
|
169 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
|
170 | _ => false |
|
171 in |
|
172 case find_first find_fun asms of |
|
173 SOME (_ $ (_ $ (f $ a))) => SOME (f, a) |
|
174 | _ => NONE |
|
175 end |
|
176 |
|
177 fun quot_true_simple_conv ctxt fnctn ctrm = |
|
178 case (term_of ctrm) of |
|
179 (Const (@{const_name QUOT_TRUE}, _) $ x) => |
|
180 let |
|
181 val fx = fnctn x; |
|
182 val thy = ProofContext.theory_of ctxt; |
|
183 val cx = cterm_of thy x; |
|
184 val cfx = cterm_of thy fx; |
|
185 val cxt = ctyp_of thy (fastype_of x); |
|
186 val cfxt = ctyp_of thy (fastype_of fx); |
|
187 val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} |
|
188 in |
|
189 Conv.rewr_conv thm ctrm |
|
190 end |
|
191 |
|
192 fun quot_true_conv ctxt fnctn ctrm = |
|
193 case (term_of ctrm) of |
|
194 (Const (@{const_name QUOT_TRUE}, _) $ _) => |
|
195 quot_true_simple_conv ctxt fnctn ctrm |
|
196 | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
|
197 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
|
198 | _ => Conv.all_conv ctrm |
|
199 |
|
200 fun quot_true_tac ctxt fnctn = |
|
201 CONVERSION |
|
202 ((Conv.params_conv ~1 (fn ctxt => |
|
203 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
|
204 |
|
205 fun dest_comb (f $ a) = (f, a) |
|
206 fun dest_bcomb ((_ $ l) $ r) = (l, r) |
|
207 |
|
208 (* TODO: Can this be done easier? *) |
|
209 fun unlam t = |
|
210 case t of |
|
211 (Abs a) => snd (Term.dest_abs a) |
|
212 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) |
|
213 |
|
214 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
|
215 | dest_fun_type _ = error "dest_fun_type" |
|
216 |
|
217 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
|
218 |
|
219 |
|
220 (* we apply apply_rsp only in case if the type needs lifting, *) |
|
221 (* which is the case if the type of the data in the QUOT_TRUE *) |
|
222 (* assumption is different from the corresponding type in the goal *) |
|
223 val apply_rsp_tac = |
|
224 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
225 let |
|
226 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
|
227 val qt_asm = find_qt_asm (map term_of asms) |
|
228 in |
|
229 case (bare_concl, qt_asm) of |
|
230 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
|
231 if (fastype_of qt_fun) = (fastype_of f) |
|
232 then no_tac |
|
233 else |
|
234 let |
|
235 val ty_x = fastype_of x |
|
236 val ty_b = fastype_of qt_arg |
|
237 val ty_f = range_type (fastype_of f) |
|
238 val thy = ProofContext.theory_of context |
|
239 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
|
240 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
|
241 val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
|
242 in |
|
243 (rtac inst_thm THEN' quotient_tac context) 1 |
|
244 end |
|
245 | _ => no_tac |
|
246 end) |
|
247 |
|
248 fun equals_rsp_tac R ctxt = |
|
249 let |
|
250 val ty = domain_type (fastype_of R); |
|
251 val thy = ProofContext.theory_of ctxt |
|
252 val thm = Drule.instantiate' |
|
253 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
|
254 in |
|
255 rtac thm THEN' quotient_tac ctxt |
|
256 end |
|
257 (* raised by instantiate' *) |
|
258 handle THM _ => K no_tac |
|
259 | TYPE _ => K no_tac |
|
260 | TERM _ => K no_tac |
|
261 |
|
262 |
|
263 fun rep_abs_rsp_tac ctxt = |
|
264 SUBGOAL (fn (goal, i) => |
|
265 case (bare_concl goal) of |
|
266 (rel $ _ $ (rep $ (abs $ _))) => |
|
267 (let |
|
268 val thy = ProofContext.theory_of ctxt; |
|
269 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
|
270 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
|
271 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
|
272 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
|
273 in |
|
274 (rtac inst_thm THEN' quotient_tac ctxt) i |
|
275 end |
|
276 handle THM _ => no_tac | TYPE _ => no_tac) |
|
277 | _ => no_tac) |
|
278 |
|
279 |
|
280 (* FIXME /TODO needs to be adapted *) |
|
281 (* |
|
282 To prove that the regularised theorem implies the abs/rep injected, |
|
283 we try: |
|
284 |
|
285 1) theorems 'trans2' from the appropriate QUOT_TYPE |
|
286 2) remove lambdas from both sides: lambda_rsp_tac |
|
287 3) remove Ball/Bex from the right hand side |
|
288 4) use user-supplied RSP theorems |
|
289 5) remove rep_abs from the right side |
|
290 6) reflexivity of equality |
|
291 7) split applications of lifted type (apply_rsp) |
|
292 8) split applications of non-lifted type (cong_tac) |
|
293 9) apply extentionality |
|
294 A) reflexivity of the relation |
|
295 B) assumption |
|
296 (Lambdas under respects may have left us some assumptions) |
|
297 C) proving obvious higher order equalities by simplifying fun_rel |
|
298 (not sure if it is still needed?) |
|
299 D) unfolding lambda on one side |
|
300 E) simplifying (= ===> =) for simpler respectfulness |
|
301 *) |
|
302 |
|
303 |
|
304 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
|
305 (case (bare_concl goal) of |
|
306 (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) |
|
307 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
|
308 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
309 |
|
310 (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) |
|
311 | (Const (@{const_name "op ="},_) $ |
|
312 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
313 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
314 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
|
315 |
|
316 (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) |
|
317 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
318 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
319 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
320 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
321 |
|
322 (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) |
|
323 | Const (@{const_name "op ="},_) $ |
|
324 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
325 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
326 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
|
327 |
|
328 (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) |
|
329 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
330 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
331 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
332 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
333 |
|
334 | (_ $ |
|
335 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
336 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
337 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
|
338 |
|
339 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => |
|
340 (rtac @{thm refl} ORELSE' |
|
341 (equals_rsp_tac R ctxt THEN' RANGE [ |
|
342 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
|
343 |
|
344 (* reflexivity of operators arising from Cong_tac *) |
|
345 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} |
|
346 |
|
347 (* respectfulness of constants; in particular of a simple relation *) |
|
348 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
|
349 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
|
350 |
|
351 (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) |
|
352 (* observe fun_map *) |
|
353 | _ $ _ $ _ |
|
354 => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) |
|
355 ORELSE' rep_abs_rsp_tac ctxt |
|
356 |
|
357 | _ => K no_tac |
|
358 ) i) |
|
359 |
|
360 fun inj_repabs_step_tac ctxt rel_refl = |
|
361 FIRST' [ |
|
362 inj_repabs_tac_match ctxt, |
|
363 (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) |
|
364 |
|
365 apply_rsp_tac ctxt THEN' |
|
366 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
|
367 |
|
368 (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) |
|
369 (* merge with previous tactic *) |
|
370 Cong_Tac.cong_tac @{thm cong} THEN' |
|
371 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
|
372 |
|
373 (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) |
|
374 rtac @{thm ext} THEN' quot_true_tac ctxt unlam, |
|
375 |
|
376 (* resolving with R x y assumptions *) |
|
377 atac, |
|
378 |
|
379 (* reflexivity of the basic relations *) |
|
380 (* R ... ... *) |
|
381 resolve_tac rel_refl] |
|
382 |
|
383 fun inj_repabs_tac ctxt = |
|
384 let |
|
385 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
|
386 in |
|
387 inj_repabs_step_tac ctxt rel_refl |
|
388 end |
|
389 |
|
390 fun all_inj_repabs_tac ctxt = |
|
391 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
|
392 |
|
393 |
|
394 (* Cleaning of the Theorem *) |
|
395 |
|
396 |
|
397 (* expands all fun_maps, except in front of bound variables *) |
|
398 fun fun_map_simple_conv xs ctrm = |
|
399 case (term_of ctrm) of |
|
400 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
401 if (member (op=) xs h) |
|
402 then Conv.all_conv ctrm |
|
403 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
|
404 | _ => Conv.all_conv ctrm |
|
405 |
|
406 fun fun_map_conv xs ctxt ctrm = |
|
407 case (term_of ctrm) of |
|
408 _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv |
|
409 fun_map_simple_conv xs) ctrm |
|
410 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
411 | _ => Conv.all_conv ctrm |
|
412 |
|
413 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
414 |
|
415 fun mk_abs u i t = |
|
416 if incr_boundvars i u aconv t then Bound i |
|
417 else (case t of |
|
418 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
|
419 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
|
420 | Bound j => if i = j then error "make_inst" else t |
|
421 | _ => t) |
|
422 |
|
423 fun make_inst lhs t = |
|
424 let |
|
425 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
426 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
427 in |
|
428 (f, Abs ("x", T, mk_abs u 0 g)) |
|
429 end |
|
430 |
|
431 fun make_inst_id lhs t = |
|
432 let |
|
433 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
|
434 val _ $ (Abs (_, _, g)) = t; |
|
435 in |
|
436 (f, Abs ("x", T, mk_abs u 0 g)) |
|
437 end |
|
438 |
|
439 (* Simplifies a redex using the 'lambda_prs' theorem. *) |
|
440 (* First instantiates the types and known subterms. *) |
|
441 (* Then solves the quotient assumptions to get Rep2 and Abs1 *) |
|
442 (* Finally instantiates the function f using make_inst *) |
|
443 (* If Rep2 is identity then the pattern is simpler and *) |
|
444 (* make_inst_id is used *) |
|
445 fun lambda_prs_simple_conv ctxt ctrm = |
|
446 case (term_of ctrm) of |
|
447 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
|
448 (let |
|
449 val thy = ProofContext.theory_of ctxt |
|
450 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
|
451 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
|
452 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
|
453 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
|
454 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
|
455 val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] |
|
456 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
|
457 val make_inst = if ty_c = ty_d then make_inst_id else make_inst |
|
458 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
459 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
460 in |
|
461 Conv.rewr_conv ti ctrm |
|
462 end |
|
463 handle _ => Conv.all_conv ctrm) |
|
464 | _ => Conv.all_conv ctrm |
|
465 |
|
466 val lambda_prs_conv = |
|
467 More_Conv.top_conv lambda_prs_simple_conv |
|
468 |
|
469 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
|
470 |
|
471 |
|
472 (* 1. folding of definitions and preservation lemmas; *) |
|
473 (* and simplification with *) |
|
474 (* thm babs_prs all_prs ex_prs *) |
|
475 (* *) |
|
476 (* 2. unfolding of ---> in front of everything, except *) |
|
477 (* bound variables (this prevents lambda_prs from *) |
|
478 (* becoming stuck *) |
|
479 (* thm fun_map.simps *) |
|
480 (* *) |
|
481 (* 3. simplification with *) |
|
482 (* thm lambda_prs *) |
|
483 (* *) |
|
484 (* 4. simplification with *) |
|
485 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
|
486 (* *) |
|
487 (* 5. Test for refl *) |
|
488 |
|
489 fun clean_tac lthy = |
|
490 let |
|
491 val thy = ProofContext.theory_of lthy; |
|
492 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
|
493 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
|
494 |
|
495 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
|
496 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
|
497 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
|
498 in |
|
499 EVERY' [simp_tac (simps thms1), |
|
500 fun_map_tac lthy, |
|
501 lambda_prs_tac lthy, |
|
502 simp_tac (simps thms2), |
|
503 TRY o rtac refl] |
|
504 end |
|
505 |
|
506 |
|
507 |
|
508 (* Tactic for Genralisation of Free Variables in a Goal *) |
|
509 |
|
510 fun inst_spec ctrm = |
|
511 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
|
512 |
|
513 fun inst_spec_tac ctrms = |
|
514 EVERY' (map (dtac o inst_spec) ctrms) |
|
515 |
|
516 fun all_list xs trm = |
|
517 fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
|
518 |
|
519 fun apply_under_Trueprop f = |
|
520 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
|
521 |
|
522 fun gen_frees_tac ctxt = |
|
523 SUBGOAL (fn (concl, i) => |
|
524 let |
|
525 val thy = ProofContext.theory_of ctxt |
|
526 val vrs = Term.add_frees concl [] |
|
527 val cvrs = map (cterm_of thy o Free) vrs |
|
528 val concl' = apply_under_Trueprop (all_list vrs) concl |
|
529 val goal = Logic.mk_implies (concl', concl) |
|
530 val rule = Goal.prove ctxt [] [] goal |
|
531 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
|
532 in |
|
533 rtac rule i |
|
534 end) |
|
535 |
|
536 |
|
537 (* The General Shape of the Lifting Procedure *) |
|
538 |
|
539 (* - A is the original raw theorem *) |
|
540 (* - B is the regularized theorem *) |
|
541 (* - C is the rep/abs injected version of B *) |
|
542 (* - D is the lifted theorem *) |
|
543 (* *) |
|
544 (* - 1st prem is the regularization step *) |
|
545 (* - 2nd prem is the rep/abs injection step *) |
|
546 (* - 3rd prem is the cleaning part *) |
|
547 (* *) |
|
548 (* the QUOT_TRUE premise in 2 records the lifted theorem *) |
|
549 |
|
550 val lifting_procedure = |
|
551 @{lemma "[|A; |
|
552 A --> B; |
|
553 QUOT_TRUE D ==> B = C; |
|
554 C = D|] ==> D" |
|
555 by (simp add: QUOT_TRUE_def)} |
|
556 |
|
557 fun lift_match_error ctxt fun_str rtrm qtrm = |
|
558 let |
|
559 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
560 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
561 val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
|
562 "", "does not match with original theorem", rtrm_str] |
|
563 in |
|
564 error msg |
|
565 end |
|
566 |
|
567 |
|
568 fun procedure_inst ctxt rtrm qtrm = |
|
569 let |
|
570 val thy = ProofContext.theory_of ctxt |
|
571 val rtrm' = HOLogic.dest_Trueprop rtrm |
|
572 val qtrm' = HOLogic.dest_Trueprop qtrm |
|
573 val reg_goal = |
|
574 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
|
575 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
576 val inj_goal = |
|
577 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
|
578 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
579 in |
|
580 Drule.instantiate' [] |
|
581 [SOME (cterm_of thy rtrm'), |
|
582 SOME (cterm_of thy reg_goal), |
|
583 NONE, |
|
584 SOME (cterm_of thy inj_goal)] lifting_procedure |
|
585 end |
|
586 |
|
587 |
|
588 (* the tactic leaves three subgoals to be proved *) |
|
589 fun procedure_tac ctxt rthm = |
|
590 ObjectLogic.full_atomize_tac |
|
591 THEN' gen_frees_tac ctxt |
|
592 THEN' CSUBGOAL (fn (goal, i) => |
|
593 let |
|
594 val rthm' = atomize_thm rthm |
|
595 val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) |
|
596 in |
|
597 (rtac rule THEN' rtac rthm') i |
|
598 end) |
|
599 |
|
600 |
|
601 (* Automatic Proofs *) |
|
602 |
|
603 val msg1 = "Regularize proof failed." |
|
604 val msg2 = cat_lines ["Injection proof failed.", |
|
605 "This is probably due to missing respects lemmas.", |
|
606 "Try invoking the injection method manually to see", |
|
607 "which lemmas are missing."] |
|
608 val msg3 = "Cleaning proof failed." |
|
609 |
|
610 fun lift_tac ctxt rthm = |
|
611 procedure_tac ctxt rthm |
|
612 THEN' RANGE_WARN |
|
613 [(regularize_tac ctxt, msg1), |
|
614 (all_inj_repabs_tac ctxt, msg2), |
|
615 (clean_tac ctxt, msg3)] |
|
616 |
|
617 |
|
618 |
|
619 end; |