37 (* composition of two theorems, used in maps *) |
37 (* composition of two theorems, used in maps *) |
38 fun OF1 thm1 thm2 = thm2 RS thm1 |
38 fun OF1 thm1 thm2 = thm2 RS thm1 |
39 |
39 |
40 (* prints a warning, if the subgoal is not solved *) |
40 (* prints a warning, if the subgoal is not solved *) |
41 fun WARN (tac, msg) i st = |
41 fun WARN (tac, msg) i st = |
42 case Seq.pull ((SOLVED' tac) i st) of |
42 case Seq.pull (SOLVED' tac i st) of |
43 NONE => (warning msg; Seq.single st) |
43 NONE => (warning msg; Seq.single st) |
44 | seqcell => Seq.make (fn () => seqcell) |
44 | seqcell => Seq.make (fn () => seqcell) |
45 |
45 |
46 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
46 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
47 |
47 |
176 |
176 |
177 |
177 |
178 |
178 |
179 (*** Injection Tactic ***) |
179 (*** Injection Tactic ***) |
180 |
180 |
181 (* Looks for Quot_True assumtions, and in case its parameter |
181 (* Looks for Quot_True assumptions, and in case its parameter |
182 is an application, it returns the function and the argument. |
182 is an application, it returns the function and the argument. |
183 *) |
183 *) |
184 fun find_qt_asm asms = |
184 fun find_qt_asm asms = |
185 let |
185 let |
186 fun find_fun trm = |
186 fun find_fun trm = |
440 |
440 |
441 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
441 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
442 |
442 |
443 (* custom matching functions *) |
443 (* custom matching functions *) |
444 fun mk_abs u i t = |
444 fun mk_abs u i t = |
445 if incr_boundvars i u aconv t then Bound i |
445 if incr_boundvars i u aconv t then Bound i else |
446 else (case t of |
446 case t of |
447 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
447 t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2 |
448 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
448 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
449 | Bound j => if i = j then error "make_inst" else t |
449 | Bound j => if i = j then error "make_inst" else t |
450 | _ => t) |
450 | _ => t |
451 |
451 |
452 fun make_inst lhs t = |
452 fun make_inst lhs t = |
453 let |
453 let |
454 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
454 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
455 val _ $ (Abs (_, _, (_ $ g))) = t; |
455 val _ $ (Abs (_, _, (_ $ g))) = t; |
584 A --> B; |
584 A --> B; |
585 Quot_True D ==> B = C; |
585 Quot_True D ==> B = C; |
586 C = D|] ==> D" |
586 C = D|] ==> D" |
587 by (simp add: Quot_True_def)} |
587 by (simp add: Quot_True_def)} |
588 |
588 |
589 fun lift_match_error ctxt str rtrm qtrm = |
589 fun lift_match_error ctxt msg rtrm qtrm = |
590 let |
590 let |
591 val rtrm_str = Syntax.string_of_term ctxt rtrm |
591 val rtrm_str = Syntax.string_of_term ctxt rtrm |
592 val qtrm_str = Syntax.string_of_term ctxt qtrm |
592 val qtrm_str = Syntax.string_of_term ctxt qtrm |
593 val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, |
593 val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, |
594 "", "does not match with original theorem", rtrm_str] |
594 "", "does not match with original theorem", rtrm_str] |
595 in |
595 in |
596 error msg |
596 error msg |
597 end |
597 end |
598 |
598 |
600 let |
600 let |
601 val thy = ProofContext.theory_of ctxt |
601 val thy = ProofContext.theory_of ctxt |
602 val rtrm' = HOLogic.dest_Trueprop rtrm |
602 val rtrm' = HOLogic.dest_Trueprop rtrm |
603 val qtrm' = HOLogic.dest_Trueprop qtrm |
603 val qtrm' = HOLogic.dest_Trueprop qtrm |
604 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
604 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
605 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
605 handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm |
606 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
606 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
607 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
607 handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm |
608 in |
608 in |
609 Drule.instantiate' [] |
609 Drule.instantiate' [] |
610 [SOME (cterm_of thy rtrm'), |
610 [SOME (cterm_of thy rtrm'), |
611 SOME (cterm_of thy reg_goal), |
611 SOME (cterm_of thy reg_goal), |
612 NONE, |
612 NONE, |