equal
deleted
inserted
replaced
49 |
49 |
50 (*** Regularize Tactic ***) |
50 (*** Regularize Tactic ***) |
51 |
51 |
52 (** solvers for equivp and quotient assumptions **) |
52 (** solvers for equivp and quotient assumptions **) |
53 |
53 |
54 (* FIXME / TODO: should this SOLVED' the goal, like with quotient_tac? *) |
|
55 (* FIXME / TODO: none of te examples break if added *) |
|
56 fun equiv_tac ctxt = |
54 fun equiv_tac ctxt = |
57 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
55 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
58 |
56 |
59 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
57 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
60 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
58 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
61 |
59 |
62 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
|
63 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) |
|
64 fun quotient_tac ctxt = SOLVED' |
60 fun quotient_tac ctxt = SOLVED' |
65 (REPEAT_ALL_NEW (FIRST' |
61 (REPEAT_ALL_NEW (FIRST' |
66 [rtac @{thm identity_quotient}, |
62 [rtac @{thm identity_quotient}, |
67 resolve_tac (quotient_rules_get ctxt)])) |
63 resolve_tac (quotient_rules_get ctxt)])) |
68 |
64 |
277 SOME thm => rtac thm THEN' quotient_tac ctxt |
273 SOME thm => rtac thm THEN' quotient_tac ctxt |
278 | NONE => K no_tac |
274 | NONE => K no_tac |
279 end |
275 end |
280 | _ => K no_tac |
276 | _ => K no_tac |
281 end |
277 end |
282 (* TODO: Again, can one specify more concretely *) |
|
283 (* TODO: in terms of R when no_tac should be returned? *) |
|
284 |
278 |
285 fun rep_abs_rsp_tac ctxt = |
279 fun rep_abs_rsp_tac ctxt = |
286 SUBGOAL (fn (goal, i) => |
280 SUBGOAL (fn (goal, i) => |
287 case (try bare_concl goal) of |
281 case (try bare_concl goal) of |
288 SOME (rel $ _ $ (rep $ (abs $ _))) => |
282 SOME (rel $ _ $ (rep $ (abs $ _))) => |