9 - stamps to identify funs / tacs |
9 - stamps to identify funs / tacs |
10 - merge: fail if incompatible funs |
10 - merge: fail if incompatible funs |
11 - improve merge |
11 - improve merge |
12 *) |
12 *) |
13 |
13 |
14 infix 4 addsimps addeqcongs addsimprocs delsimprocs addsolver delsimps |
14 infix 4 setloop addloop setsolver addsolver |
15 setsolver setloop setmksimps settermless setsubgoaler; |
15 setsubgoaler setmksimps |
|
16 addsimps addeqcongs delsimps |
|
17 settermless addsimprocs delsimprocs; |
|
18 |
16 |
19 |
17 signature SIMPLIFIER = |
20 signature SIMPLIFIER = |
18 sig |
21 sig |
19 type simproc |
22 type simproc |
20 val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc |
23 val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc |
24 type simpset |
27 type simpset |
25 val empty_ss: simpset |
28 val empty_ss: simpset |
26 val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list} |
29 val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list} |
27 val prems_of_ss: simpset -> thm list |
30 val prems_of_ss: simpset -> thm list |
28 val setloop: simpset * (int -> tactic) -> simpset |
31 val setloop: simpset * (int -> tactic) -> simpset |
|
32 val addloop: simpset * (int -> tactic) -> simpset |
29 val setsolver: simpset * (thm list -> int -> tactic) -> simpset |
33 val setsolver: simpset * (thm list -> int -> tactic) -> simpset |
30 val addsolver: simpset * (thm list -> int -> tactic) -> simpset |
34 val addsolver: simpset * (thm list -> int -> tactic) -> simpset |
31 val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
35 val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
32 val setmksimps: simpset * (thm -> thm list) -> simpset |
36 val setmksimps: simpset * (thm -> thm list) -> simpset |
33 val settermless: simpset * (term * term -> bool) -> simpset |
37 val settermless: simpset * (term * term -> bool) -> simpset |
133 |
137 |
134 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac = _}) |
138 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac = _}) |
135 setloop loop_tac = |
139 setloop loop_tac = |
136 make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, DETERM o loop_tac); |
140 make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, DETERM o loop_tac); |
137 |
141 |
|
142 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
|
143 addloop tac = |
|
144 make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, |
|
145 loop_tac ORELSE' (DETERM o tac)); |
|
146 |
138 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac = _, loop_tac}) |
147 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac = _, loop_tac}) |
139 setsolver finish_tac = |
148 setsolver finish_tac = |
140 make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); |
149 make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); |
141 |
150 |
142 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, finish_tac}) |
151 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
143 addsolver tac = |
152 addsolver tac = |
144 make_ss (mss, simps, procs, congs, subgoal_tac, |
153 make_ss (mss, simps, procs, congs, subgoal_tac, |
145 fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac); |
154 fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac); |
146 |
155 |
147 fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, finish_tac, loop_tac}) |
156 fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, finish_tac, loop_tac}) |