27 setmksimps (mksimps []) |
27 setmksimps (mksimps []) |
28 |
28 |
29 (* composition of two theorems, used in maps *) |
29 (* composition of two theorems, used in maps *) |
30 fun OF1 thm1 thm2 = thm2 RS thm1 |
30 fun OF1 thm1 thm2 = thm2 RS thm1 |
31 |
31 |
32 (* makes sure a subgoal is solved *) |
32 (* FIXME --- now in Isabelle *) |
33 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
33 fun SOLVED' tac i st = |
|
34 tac i st |> Seq.filter (fn st' => nprems_of st' < nprems_of st) |
34 |
35 |
35 (* prints a warning, if the subgoal is not solved *) |
36 (* prints a warning, if the subgoal is not solved *) |
36 fun WARN (tac, msg) i st = |
37 fun WARN (tac, msg) i st = |
37 case Seq.pull ((SOLVES' tac) i st) of |
38 case Seq.pull ((SOLVED' tac) i st) of |
38 NONE => (warning msg; Seq.single st) |
39 NONE => (warning msg; Seq.single st) |
39 | seqcell => Seq.make (fn () => seqcell) |
40 | seqcell => Seq.make (fn () => seqcell) |
40 |
41 |
41 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
42 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
42 |
43 |
52 |
53 |
53 (*** Regularize Tactic ***) |
54 (*** Regularize Tactic ***) |
54 |
55 |
55 (** solvers for equivp and quotient assumptions **) |
56 (** solvers for equivp and quotient assumptions **) |
56 |
57 |
57 (* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *) |
58 (* FIXME / TODO: should this SOLVED' the goal, like with quotient_tac? *) |
58 (* FIXME / TODO: none of te examples break if added *) |
59 (* FIXME / TODO: none of te examples break if added *) |
59 fun equiv_tac ctxt = |
60 fun equiv_tac ctxt = |
60 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
61 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
61 |
62 |
62 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
63 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
63 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
64 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
64 |
65 |
65 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
66 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
66 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) |
67 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) |
67 fun quotient_tac ctxt = SOLVES' |
68 fun quotient_tac ctxt = SOLVED' |
68 (REPEAT_ALL_NEW (FIRST' |
69 (REPEAT_ALL_NEW (FIRST' |
69 [rtac @{thm identity_quotient}, |
70 [rtac @{thm identity_quotient}, |
70 resolve_tac (quotient_rules_get ctxt)])) |
71 resolve_tac (quotient_rules_get ctxt)])) |
71 |
72 |
72 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
73 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |