46 in |
47 in |
47 @{thm equal_elim_rule1} OF [thm'', thm'] |
48 @{thm equal_elim_rule1} OF [thm'', thm'] |
48 end |
49 end |
49 |
50 |
50 |
51 |
51 (*********************) |
52 |
52 (* Regularize Tactic *) |
53 (*** Regularize Tactic ***) |
53 (*********************) |
54 |
54 |
55 (** solvers for equivp and quotient assumptions **) |
55 (* solvers for equivp and quotient assumptions *) |
56 |
56 (* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *) |
57 (* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *) |
57 (* FIXME / TODO: none of te examples break if added *) |
58 (* FIXME / TODO: none of te examples break if added *) |
58 fun equiv_tac ctxt = |
59 fun equiv_tac ctxt = |
59 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
60 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
60 |
61 |
61 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
62 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
62 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
63 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
63 |
64 |
64 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
65 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
65 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) |
66 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) |
66 fun quotient_tac ctxt = SOLVES' |
67 fun quotient_tac ctxt = SOLVES' |
67 (REPEAT_ALL_NEW (FIRST' |
68 (REPEAT_ALL_NEW (FIRST' |
68 [rtac @{thm identity_quotient}, |
69 [rtac @{thm identity_quotient}, |
69 resolve_tac (quotient_rules_get ctxt)])) |
70 resolve_tac (quotient_rules_get ctxt)])) |
70 |
71 |
71 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
72 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
171 resolve_tac eq_eqvs, |
172 resolve_tac eq_eqvs, |
172 simp_tac simpset]) |
173 simp_tac simpset]) |
173 end |
174 end |
174 |
175 |
175 |
176 |
176 (********************) |
177 |
177 (* Injection Tactic *) |
178 (*** Injection Tactic ***) |
178 (********************) |
179 |
179 |
180 (* Looks for Quot_True assumtions, and in case its parameter |
180 (* Looks for Quot_True assumtions, and in case its parameter *) |
181 is an application, it returns the function and the argument. *) |
181 (* is an application, it returns the function and the argument. *) |
|
182 fun find_qt_asm asms = |
182 fun find_qt_asm asms = |
183 let |
183 let |
184 fun find_fun trm = |
184 fun find_fun trm = |
185 case trm of |
185 case trm of |
186 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true |
186 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true |
230 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
230 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
231 | dest_fun_type _ = error "dest_fun_type" |
231 | dest_fun_type _ = error "dest_fun_type" |
232 |
232 |
233 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
233 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
234 |
234 |
235 (* We apply apply_rsp only in case if the type needs lifting. *) |
235 (* We apply apply_rsp only in case if the type needs lifting. |
236 (* This is the case if the type of the data in the Quot_True *) |
236 This is the case if the type of the data in the Quot_True |
237 (* assumption is different from the corresponding type in the goal. *) |
237 assumption is different from the corresponding type in the goal. *) |
238 val apply_rsp_tac = |
238 val apply_rsp_tac = |
239 Subgoal.FOCUS (fn {concl, asms, context,...} => |
239 Subgoal.FOCUS (fn {concl, asms, context,...} => |
240 let |
240 let |
241 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
241 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
242 val qt_asm = find_qt_asm (map term_of asms) |
242 val qt_asm = find_qt_asm (map term_of asms) |
243 in |
243 in |
244 case (bare_concl, qt_asm) of |
244 case (bare_concl, qt_asm) of |
245 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
245 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
246 if (fastype_of qt_fun) = (fastype_of f) |
246 if (fastype_of qt_fun) = (fastype_of f) |
247 then no_tac |
247 then no_tac |
248 else |
248 else |
249 let |
249 let |
250 val ty_x = fastype_of x |
250 val ty_x = fastype_of x |
251 val ty_b = fastype_of qt_arg |
251 val ty_b = fastype_of qt_arg |
252 val ty_f = range_type (fastype_of f) |
252 val ty_f = range_type (fastype_of f) |
253 val thy = ProofContext.theory_of context |
253 val thy = ProofContext.theory_of context |
254 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
254 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
255 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
255 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
256 val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
256 val inst_thm = Drule.instantiate' ty_inst |
|
257 ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
257 in |
258 in |
258 (rtac inst_thm THEN' quotient_tac context) 1 |
259 (rtac inst_thm THEN' quotient_tac context) 1 |
259 end |
260 end |
260 | _ => no_tac |
261 | _ => no_tac |
261 end) |
262 end) |
411 |
412 |
412 fun all_injection_tac ctxt = |
413 fun all_injection_tac ctxt = |
413 REPEAT_ALL_NEW (injection_tac ctxt) |
414 REPEAT_ALL_NEW (injection_tac ctxt) |
414 |
415 |
415 |
416 |
416 (***************************) |
417 |
417 (* Cleaning of the Theorem *) |
418 (** Cleaning of the Theorem **) |
418 (***************************) |
419 |
419 |
420 (* expands all fun_maps, except in front of the bound variables listed in xs *) |
420 (* expands all fun_maps, except in front of the bound *) |
|
421 (* variables listed in xs *) |
|
422 fun fun_map_simple_conv xs ctrm = |
421 fun fun_map_simple_conv xs ctrm = |
423 case (term_of ctrm) of |
422 case (term_of ctrm) of |
424 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
423 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
425 if (member (op=) xs h) |
424 if (member (op=) xs h) |
426 then Conv.all_conv ctrm |
425 then Conv.all_conv ctrm |
427 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
426 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
428 | _ => Conv.all_conv ctrm |
427 | _ => Conv.all_conv ctrm |
429 |
428 |
430 fun fun_map_conv xs ctxt ctrm = |
429 fun fun_map_conv xs ctxt ctrm = |
491 |
490 |
492 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt |
491 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt |
493 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
492 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
494 |
493 |
495 |
494 |
496 (* 1. folding of definitions and preservation lemmas; *) |
495 (* Cleaning consists of: |
497 (* and simplification with *) |
496 1. folding of definitions and preservation lemmas; |
498 (* thm babs_prs all_prs ex_prs *) |
497 and simplification with babs_prs all_prs ex_prs |
499 (* *) |
498 |
500 (* 2. unfolding of ---> in front of everything, except *) |
499 2. unfolding of ---> in front of everything, except |
501 (* bound variables (this prevents lambda_prs from *) |
500 bound variables |
502 (* becoming stuck) *) |
501 (this prevents lambda_prs from becoming stuck) |
503 (* thm fun_map.simps *) |
502 |
504 (* *) |
503 3. simplification with lambda_prs |
505 (* 3. simplification with *) |
504 |
506 (* thm lambda_prs *) |
505 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps |
507 (* *) |
506 |
508 (* 4. simplification with *) |
507 5. test for refl *) |
509 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
|
510 (* *) |
|
511 (* 5. test for refl *) |
|
512 |
|
513 fun clean_tac lthy = |
508 fun clean_tac lthy = |
514 let |
509 let |
515 (* FIXME/TODO produce defs with lthy, like prs and ids *) |
510 (* FIXME/TODO produce defs with lthy, like prs and ids *) |
516 val thy = ProofContext.theory_of lthy; |
511 val thy = ProofContext.theory_of lthy; |
517 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
512 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
559 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
554 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
560 in |
555 in |
561 rtac rule i |
556 rtac rule i |
562 end) |
557 end) |
563 |
558 |
564 (**********************************************) |
559 |
565 (* The General Shape of the Lifting Procedure *) |
560 (** The General Shape of the Lifting Procedure **) |
566 (**********************************************) |
561 |
567 |
562 |
568 (* - A is the original raw theorem *) |
563 (* - A is the original raw theorem |
569 (* - B is the regularized theorem *) |
564 - B is the regularized theorem |
570 (* - C is the rep/abs injected version of B *) |
565 - C is the rep/abs injected version of B |
571 (* - D is the lifted theorem *) |
566 - D is the lifted theorem |
572 (* *) |
567 |
573 (* - 1st prem is the regularization step *) |
568 - 1st prem is the regularization step |
574 (* - 2nd prem is the rep/abs injection step *) |
569 - 2nd prem is the rep/abs injection step |
575 (* - 3rd prem is the cleaning part *) |
570 - 3rd prem is the cleaning part |
576 (* *) |
571 |
577 (* the Quot_True premise in 2nd records the lifted theorem *) |
572 the Quot_True premise in 2nd records the lifted theorem *) |
578 |
|
579 val lifting_procedure_thm = |
573 val lifting_procedure_thm = |
580 @{lemma "[|A; |
574 @{lemma "[|A; |
581 A --> B; |
575 A --> B; |
582 Quot_True D ==> B = C; |
576 Quot_True D ==> B = C; |
583 C = D|] ==> D" |
577 C = D|] ==> D" |
586 fun lift_match_error ctxt str rtrm qtrm = |
580 fun lift_match_error ctxt str rtrm qtrm = |
587 let |
581 let |
588 val rtrm_str = Syntax.string_of_term ctxt rtrm |
582 val rtrm_str = Syntax.string_of_term ctxt rtrm |
589 val qtrm_str = Syntax.string_of_term ctxt qtrm |
583 val qtrm_str = Syntax.string_of_term ctxt qtrm |
590 val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, |
584 val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, |
591 "", "does not match with original theorem", rtrm_str] |
585 "", "does not match with original theorem", rtrm_str] |
592 in |
586 in |
593 error msg |
587 error msg |
594 end |
588 end |
595 |
589 |
596 fun procedure_inst ctxt rtrm qtrm = |
590 fun procedure_inst ctxt rtrm qtrm = |
597 let |
591 let |
598 val thy = ProofContext.theory_of ctxt |
592 val thy = ProofContext.theory_of ctxt |
599 val rtrm' = HOLogic.dest_Trueprop rtrm |
593 val rtrm' = HOLogic.dest_Trueprop rtrm |
600 val qtrm' = HOLogic.dest_Trueprop qtrm |
594 val qtrm' = HOLogic.dest_Trueprop qtrm |
601 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
595 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
602 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
596 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
603 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
597 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
604 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
598 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
605 in |
599 in |
606 Drule.instantiate' [] |
600 Drule.instantiate' [] |
607 [SOME (cterm_of thy rtrm'), |
601 [SOME (cterm_of thy rtrm'), |
608 SOME (cterm_of thy reg_goal), |
602 SOME (cterm_of thy reg_goal), |
609 NONE, |
603 NONE, |