# HG changeset patch # User oheimb # Date 934817625 -7200 # Node ID 381d6987f68d4a4229ff21d0547dc26391a59714 # Parent 08a354bbc34ccdc99a2373307df59fe14db10765 exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset basic_gen_simp_tac now takes a looper as _explicit_ argument removed superfluous argument of solve_all_tac corrected safe_asm_full_simp_tac: now also with mutual simplification of prems diff -r 08a354bbc34c -r 381d6987f68d src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Mon Aug 16 17:24:28 1999 +0200 +++ b/src/Provers/simplifier.ML Mon Aug 16 17:33:45 1999 +0200 @@ -22,8 +22,8 @@ {mss: meta_simpset, subgoal_tac: simpset -> int -> tactic, loop_tacs: (string * (int -> tactic))list, - finish_tac: thm list -> int -> tactic, - unsafe_finish_tac: thm list -> int -> tactic}; + unsafe_finish_tac: thm list -> int -> tactic, + finish_tac: thm list -> int -> tactic}; val print_ss: simpset -> unit val print_simpset: theory -> unit val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset @@ -123,12 +123,12 @@ mss: meta_simpset, subgoal_tac: simpset -> int -> tactic, loop_tacs: (string * (int -> tactic))list, - finish_tac: thm list -> int -> tactic, - unsafe_finish_tac: thm list -> int -> tactic}; + unsafe_finish_tac: thm list -> int -> tactic, + finish_tac: thm list -> int -> tactic}; -fun make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) = +fun make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac) = Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, - finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac}; + unsafe_finish_tac = unsafe_finish_tac, finish_tac = finish_tac}; val empty_ss = let val mss = Thm.set_mk_sym (Thm.empty_mss, Some o symmetric_fun) @@ -157,91 +157,95 @@ (* extend simpsets *) -fun (Simpset {mss, subgoal_tac = _, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac = _, loop_tacs, unsafe_finish_tac, finish_tac}) setsubgoaler subgoal_tac = - make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs = _, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_finish_tac, finish_tac}) setloop tac = - make_ss (mss, subgoal_tac, [("",tac)], finish_tac, unsafe_finish_tac); + make_ss (mss, subgoal_tac, [("",tac)], unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) addloop tac = make_ss (mss, subgoal_tac, (case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)), - finish_tac, unsafe_finish_tac); + unsafe_finish_tac, finish_tac); -fun (ss as Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) delloop name = +fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) + delloop name = let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in if null del then (warning ("No such looper in simpset: " ^ name); ss) - else make_ss (mss, subgoal_tac, rest, finish_tac, unsafe_finish_tac) + else make_ss (mss, subgoal_tac, rest, unsafe_finish_tac, finish_tac) end; +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) + setSSolver finish_tac = + make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac = _, unsafe_finish_tac}) - setSSolver finish_tac = - make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); - -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) addSSolver tac = - make_ss (mss, subgoal_tac, loop_tacs, fn hyps => finish_tac hyps ORELSE' tac hyps, - unsafe_finish_tac); + make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, + fn hyps => finish_tac hyps ORELSE' tac hyps); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac = _}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac = _, finish_tac}) setSolver unsafe_finish_tac = - make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) addSolver tac = - make_ss (mss, subgoal_tac, loop_tacs, finish_tac, - fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps); + make_ss (mss, subgoal_tac, loop_tacs, + fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) setmksimps mk_simps = make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps), - subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) setmkeqTrue mk_eq_True = make_ss (Thm.set_mk_eq_True (mss, mk_eq_True), - subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) setmksym mksym = make_ss (Thm.set_mk_sym (mss, mksym), - subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) settermless termless = make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs, - finish_tac, unsafe_finish_tac); + unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) addsimps rews = - make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs, + unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) delsimps rews = - make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs, + unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) addeqcongs newcongs = - make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs, + unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) deleqcongs oldcongs = - make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs, + unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) addsimprocs simprocs = make_ss (Thm.add_simprocs (mss, map rep_simproc simprocs), - subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); -fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) delsimprocs simprocs = make_ss (Thm.del_simprocs (mss, map rep_simproc simprocs), - subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac); fun onlysimps (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}, rews) = make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) @@ -251,10 +255,10 @@ (* merge simpsets *) (*NOTE: ignores tactics of 2nd simpset (except loopers)*) fun merge_ss - (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac, finish_tac, unsafe_finish_tac}, + (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac, unsafe_finish_tac, finish_tac}, Simpset {mss = mss2, loop_tacs = loop_tacs2, ...}) = make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac, - merge_alists loop_tacs1 loop_tacs2, finish_tac, unsafe_finish_tac); + merge_alists loop_tacs1 loop_tacs2, unsafe_finish_tac, finish_tac); @@ -343,29 +347,30 @@ (** simplification tactics **) -fun solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) mss = +fun solve_all_tac (subgoal_tac, loop_tacs, unsafe_finish_tac) mss = let val ss = - make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, unsafe_finish_tac); + make_ss (mss, subgoal_tac, loop_tacs,unsafe_finish_tac,unsafe_finish_tac); val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1 in DEPTH_SOLVE solve1_tac end; fun loop_tac loop_tacs = FIRST'(map snd loop_tacs); -(*not totally safe: may instantiate unknowns that appear also in other subgoals*) -fun basic_gen_simp_tac mode = - fn (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) => +(*unsafe: may instantiate unknowns that appear also in other subgoals*) +fun basic_gen_simp_tac mode finish_tac = + fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) => let fun simp_loop_tac i = asm_rewrite_goal_tac mode - (solve_all_tac (subgoal_tac,loop_tacs,finish_tac,unsafe_finish_tac)) + (solve_all_tac (subgoal_tac,loop_tacs,unsafe_finish_tac)) mss i THEN (finish_tac (prems_of_mss mss) i ORELSE TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i)) in simp_loop_tac end; -fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) = - basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac); +fun gen_simp_tac mode + (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) = + basic_gen_simp_tac mode unsafe_finish_tac ss; val simp_tac = gen_simp_tac (false, false, false); val asm_simp_tac = gen_simp_tac (false, true, false); @@ -374,7 +379,9 @@ val asm_full_simp_tac = gen_simp_tac (true, 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, false); +fun safe_asm_full_simp_tac (ss as Simpset {mss, subgoal_tac, loop_tacs, + unsafe_finish_tac, finish_tac}) = + basic_gen_simp_tac (true, true, true) finish_tac ss; (*the abstraction over the proof state delays the dereferencing*) fun Simp_tac i st = simp_tac (simpset ()) i st; @@ -387,9 +394,10 @@ (** simplification rules and conversions **) -fun simp rew mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm = +fun simp rew mode + (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) thm = let - val tacf = solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); + val tacf = solve_all_tac (subgoal_tac, loop_tacs, unsafe_finish_tac); fun prover m th = apsome fst (Seq.pull (tacf m th)); in rew mode prover mss thm end;