diff -r 1fe7c9f599c2 -r b442786d4469 src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Sat Feb 15 16:10:00 1997 +0100 +++ b/src/Provers/simplifier.ML Sat Feb 15 16:14:35 1997 +0100 @@ -11,9 +11,8 @@ - improve merge *) -infix 4 setloop addloop setsolver addsolver - setsubgoaler setmksimps - addsimps addeqcongs delsimps +infix 4 setsubgoaler setloop addloop setSSolver addSSolver setSolver addSolver + setmksimps addsimps delsimps addeqcongs deleqcongs settermless addsimprocs delsimprocs; @@ -26,34 +25,42 @@ -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm (* FIXME move?, rename? *) type simpset val empty_ss: simpset - val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list} - val prems_of_ss: simpset -> thm list - val setloop: simpset * (int -> tactic) -> simpset - val addloop: simpset * (int -> tactic) -> simpset - val setsolver: simpset * (thm list -> int -> tactic) -> simpset - val addsolver: simpset * (thm list -> int -> tactic) -> simpset - val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset - val setmksimps: simpset * (thm -> thm list) -> simpset + val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list, + subgoal_tac: simpset -> int -> tactic, + loop_tac: int -> tactic, + finish_tac: thm list -> int -> tactic, + unsafe_finish_tac: thm list -> int -> tactic} + val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset + val setloop: simpset * (int -> tactic) -> simpset + val addloop: simpset * (int -> tactic) -> simpset + val setSSolver: simpset * (thm list -> int -> tactic) -> simpset + val addSSolver: simpset * (thm list -> int -> tactic) -> simpset + val setSolver: simpset * (thm list -> int -> tactic) -> simpset + val addSolver: simpset * (thm list -> int -> tactic) -> simpset + val setmksimps: simpset * (thm -> thm list) -> simpset val settermless: simpset * (term * term -> bool) -> simpset - val addsimps: simpset * thm list -> simpset - val delsimps: simpset * thm list -> simpset + val addsimps: simpset * thm list -> simpset + val delsimps: simpset * thm list -> simpset + val addeqcongs: simpset * thm list -> simpset + val deleqcongs: simpset * thm list -> simpset val addsimprocs: simpset * simproc list -> simpset val delsimprocs: simpset * simproc list -> simpset - val addeqcongs: simpset * thm list -> simpset - val merge_ss: simpset * simpset -> simpset - val simpset: simpset ref + val merge_ss: simpset * simpset -> simpset + val prems_of_ss: simpset -> thm list + val simpset: simpset ref val Addsimps: thm list -> unit val Delsimps: thm list -> unit val Addsimprocs: simproc list -> unit val Delsimprocs: simproc list -> unit - val simp_tac: simpset -> int -> tactic - val asm_simp_tac: simpset -> int -> tactic - val full_simp_tac: simpset -> int -> tactic - val asm_full_simp_tac: simpset -> int -> tactic - val Simp_tac: int -> tactic - val Asm_simp_tac: int -> tactic - val Full_simp_tac: int -> tactic - val Asm_full_simp_tac: int -> tactic + val simp_tac: simpset -> int -> tactic + val asm_simp_tac: simpset -> int -> tactic + val full_simp_tac: simpset -> int -> tactic + val asm_full_simp_tac: simpset -> int -> tactic + val safe_asm_full_simp_tac: simpset -> int -> tactic + val Simp_tac: int -> tactic + val Asm_simp_tac: int -> tactic + val Full_simp_tac: int -> tactic + val Asm_full_simp_tac: int -> tactic end; @@ -115,92 +122,118 @@ simps: thm list, procs: simproc list, congs: thm list, - subgoal_tac: simpset -> int -> tactic, - finish_tac: thm list -> int -> tactic, - loop_tac: int -> tactic}; + subgoal_tac: simpset -> int -> tactic, + loop_tac: int -> tactic, + finish_tac: thm list -> int -> tactic, + unsafe_finish_tac: thm list -> int -> tactic}; -fun make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac) = +fun make_ss (mss, simps, procs, congs, + subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) = Simpset {mss = mss, simps = simps, procs = procs, congs = congs, - subgoal_tac = subgoal_tac, finish_tac = finish_tac, - loop_tac = loop_tac}; + subgoal_tac = subgoal_tac, loop_tac = loop_tac, + finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac}; val empty_ss = - make_ss (Thm.empty_mss, [], [], [], K (K no_tac), K (K no_tac), K no_tac); + make_ss (Thm.empty_mss, [], [], [], + K (K no_tac), K no_tac, K (K no_tac), K (K no_tac)); -fun rep_ss (Simpset {simps, procs, congs, ...}) = - {simps = simps, procs = map name_of_simproc procs, congs = congs}; +fun rep_ss (Simpset {simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac, ...}) = + {simps = simps, procs = map name_of_simproc procs, congs = congs, + subgoal_tac = subgoal_tac, loop_tac = loop_tac, + finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac}; fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss; (* extend simpsets *) -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac = _}) - setloop loop_tac = - make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, DETERM o loop_tac); +fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, loop_tac, + finish_tac, unsafe_finish_tac}) setsubgoaler subgoal_tac = + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac); + +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac = _, + finish_tac, unsafe_finish_tac}) setloop loop_tac = + make_ss (mss, simps, procs, congs, subgoal_tac, DETERM o loop_tac, + finish_tac, unsafe_finish_tac); -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - addloop tac = - make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, - loop_tac ORELSE' (DETERM o tac)); +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) addloop tac = + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac ORELSE'(DETERM o tac), + finish_tac, unsafe_finish_tac); -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac = _, loop_tac}) - setsolver finish_tac = - make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac = _, unsafe_finish_tac}) setSSolver finish_tac = + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac); -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - addsolver tac = - make_ss (mss, simps, procs, congs, subgoal_tac, - fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac); +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) addSSolver tac = + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, + fn hyps => finish_tac hyps ORELSE' tac hyps, unsafe_finish_tac); -fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, finish_tac, loop_tac}) - setsubgoaler subgoal_tac = - make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac = _}) setSolver unsafe_finish_tac = + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac); -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - setmksimps mk_simps = - make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs, - subgoal_tac, finish_tac, loop_tac); +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) addSolver tac = + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps); -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - settermless termless = +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) setmksimps mk_simps = + make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs, + subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac); + +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) settermless termless = make_ss (Thm.set_termless (mss, termless), simps, procs, congs, - subgoal_tac, finish_tac, loop_tac); + subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac); -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - addsimps rews = +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) addsimps rews = let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in make_ss (Thm.add_simps (mss, rews'), gen_union eq_thm (rews', simps), - procs, congs, subgoal_tac, finish_tac, loop_tac) + procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) end; -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - delsimps rews = +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) delsimps rews = let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in - make_ss (Thm.del_simps (mss, rews'), - foldl (gen_rem eq_thm) (simps, rews'), - procs, congs, subgoal_tac, finish_tac, loop_tac) + make_ss (Thm.del_simps (mss, rews'), foldl (gen_rem eq_thm) (simps, rews'), + procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) end; -fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) - addeqcongs newcongs = - make_ss (Thm.add_congs (mss, newcongs), - simps, procs, gen_union eq_thm (newcongs, congs), - subgoal_tac, finish_tac, loop_tac); +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) addeqcongs newcongs = + make_ss (Thm.add_congs (mss, newcongs), simps, procs, + gen_union eq_thm (congs, newcongs), subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac); -fun addsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}), - simproc as Simproc {name = _, procs = procs'}) = +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) deleqcongs oldcongs = + make_ss (Thm.del_congs (mss, oldcongs), simps, procs, + foldl (gen_rem eq_thm) (congs, oldcongs), subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac); + +fun addsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}), + simproc as Simproc {name = _, procs = procs'}) = make_ss (Thm.add_simprocs (mss, procs'), simps, gen_ins eq_simproc (simproc, procs), - congs, subgoal_tac, finish_tac, loop_tac); + congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac); val op addsimprocs = foldl addsimproc; -fun delsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}), - simproc as Simproc {name = _, procs = procs'}) = +fun delsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}), + simproc as Simproc {name = _, procs = procs'}) = make_ss (Thm.del_simprocs (mss, procs'), simps, gen_rem eq_simproc (procs, simproc), - congs, subgoal_tac, finish_tac, loop_tac); + congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac); val op delsimprocs = foldl delsimproc; @@ -208,7 +241,8 @@ (* merge simpsets *) (*prefers first simpset (FIXME improve?)*) -fun merge_ss (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}, +fun merge_ss (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}, Simpset {simps = simps2, procs = procs2, congs = congs2, ...}) = let val simps' = gen_union eq_thm (simps, simps2); @@ -218,7 +252,8 @@ val mss' = Thm.add_simps (mss', simps'); val mss' = Thm.add_congs (mss', congs'); in - make_ss (mss', simps', procs', congs', subgoal_tac, finish_tac, loop_tac) + make_ss (mss', simps', procs', congs', subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac) end; @@ -233,23 +268,24 @@ fun Delsimprocs procs = (simpset := ! simpset delsimprocs procs); - (** simplification tactics **) fun NEWSUBGOALS tac tacf = STATE (fn state0 => tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0))); -fun gen_simp_tac mode = - fn (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) => +(*not totally safe: may instantiate unknowns that appear also in other subgoals*) +fun basic_gen_simp_tac mode = + fn (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, + finish_tac, unsafe_finish_tac}) => let fun solve_all_tac mss = let val ss = - make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); + make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, + unsafe_finish_tac, unsafe_finish_tac); val solve1_tac = NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n<0 then all_tac else no_tac) in DEPTH_SOLVE(solve1_tac) end - fun simp_loop_tac i thm = (asm_rewrite_goal_tac mode solve_all_tac mss i THEN (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm @@ -257,11 +293,17 @@ and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) in simp_loop_tac end; +fun gen_simp_tac mode ss = basic_gen_simp_tac mode + (ss setSSolver #unsafe_finish_tac (rep_ss ss)); + val simp_tac = gen_simp_tac (false, false); val asm_simp_tac = gen_simp_tac (false, true); val full_simp_tac = gen_simp_tac (true, false); val asm_full_simp_tac = gen_simp_tac (true, true); +(*not totally safe: may instantiate unknowns that appear also in other subgoals*) +val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true); + fun Simp_tac i = simp_tac (! simpset) i; fun Asm_simp_tac i = asm_simp_tac (! simpset) i; fun Full_simp_tac i = full_simp_tac (! simpset) i;