# HG changeset patch # User wenzelm # Date 852888477 -3600 # Node ID 7590fd5ce3c7aa819493f01c118c52f618a40bdf # Parent dcf9288052732b23485e566ac15881411ae29152 cleaned up (real changes next time); diff -r dcf928805273 -r 7590fd5ce3c7 src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Thu Jan 09 17:16:50 1997 +0100 +++ b/src/Provers/simplifier.ML Fri Jan 10 10:27:57 1997 +0100 @@ -4,159 +4,148 @@ Copyright 1993 TU Munich Generic simplifier, suitable for most logics. - + +TODO: + - stamps to identify funs / tacs + - merge: fail if incompatible funs *) infix 4 addsimps addeqcongs addsolver delsimps - setsolver setloop setmksimps setsubgoaler; + setsolver setloop setmksimps setsubgoaler; signature SIMPLIFIER = sig type simpset - val addeqcongs: simpset * thm list -> simpset + val empty_ss: simpset + val rep_ss: simpset -> {simps: thm list, congs: thm list} + val prems_of_ss: simpset -> thm list + val setloop: 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 addsimps: simpset * thm list -> simpset - val addsolver: simpset * (thm list -> int -> tactic) -> simpset val delsimps: simpset * thm list -> simpset - val asm_full_simp_tac: simpset -> int -> tactic - val full_simp_tac: simpset -> int -> tactic - val asm_simp_tac: simpset -> int -> tactic - val empty_ss: simpset + val addeqcongs: simpset * thm list -> simpset val merge_ss: simpset * simpset -> simpset - val prems_of_ss: simpset -> thm list - val rep_ss: simpset -> {simps: thm list, congs: thm list} - val setsolver: simpset * (thm list -> int -> tactic) -> simpset - val setloop: simpset * (int -> tactic) -> simpset - val setmksimps: simpset * (thm -> thm list) -> simpset - val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset - val simp_tac: simpset -> int -> tactic - val simpset: simpset ref val Addsimps: thm list -> unit val Delsimps: thm list -> unit - val 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 Simp_tac: int -> tactic val Asm_simp_tac: int -> tactic val Full_simp_tac: int -> tactic val Asm_full_simp_tac: int -> tactic end; -structure Simplifier :SIMPLIFIER = + +structure Simplifier: SIMPLIFIER = struct +(** simplification sets **) + +(* type simpset *) + datatype simpset = - Simpset of {mss: meta_simpset, - simps: thm list, - congs: thm list, - subgoal_tac: simpset -> int -> tactic, - finish_tac: thm list -> int -> tactic, - loop_tac: int -> tactic}; + Simpset of { + mss: meta_simpset, + simps: thm list, + congs: thm list, + subgoal_tac: simpset -> int -> tactic, + finish_tac: thm list -> int -> tactic, + loop_tac: int -> tactic}; + +fun make_ss (mss, simps, congs, subgoal_tac, finish_tac, loop_tac) = + Simpset {mss = mss, simps = simps, congs = congs, + subgoal_tac = subgoal_tac, finish_tac = finish_tac, + loop_tac = loop_tac}; val empty_ss = - Simpset{mss=empty_mss, - simps= [], - congs= [], - subgoal_tac= K(K no_tac), - finish_tac= K(K no_tac), - loop_tac= K no_tac}; + make_ss (Thm.empty_mss, [], [], K (K no_tac), K (K no_tac), K no_tac); + +fun rep_ss (Simpset {simps, congs, ...}) = {simps = simps, congs = congs}; + +fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss; + + +(* extend simpsets *) + +fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac = _}) + setloop loop_tac = + make_ss (mss, simps, congs, subgoal_tac, finish_tac, DETERM o loop_tac); + +fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac = _, loop_tac}) + setsolver finish_tac = + make_ss (mss, simps, congs, subgoal_tac, finish_tac, loop_tac); + +fun (Simpset {mss, simps, congs, subgoal_tac, loop_tac, finish_tac}) + addsolver tac = + make_ss (mss, simps, congs, subgoal_tac, + fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac); + +fun (Simpset {mss, simps, congs, subgoal_tac = _, finish_tac, loop_tac}) + setsubgoaler subgoal_tac = + make_ss (mss, simps, congs, subgoal_tac, finish_tac, loop_tac); + +fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) + setmksimps mk_simps = + make_ss (Thm.set_mk_rews (mss, mk_simps), simps, congs, + subgoal_tac, finish_tac, loop_tac); + +fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) + addsimps rews = + let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in + make_ss (Thm.add_simps (mss, rews'), rews' @ simps, + congs, subgoal_tac, finish_tac, loop_tac) + end; + +fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_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'), + congs, subgoal_tac, finish_tac, loop_tac) + end; + +fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) + addeqcongs newcongs = + make_ss (Thm.add_congs (mss, newcongs), + simps, newcongs @ congs, subgoal_tac, finish_tac, loop_tac); + + +(* merge simpsets *) + +(*prefers first simpset*) +fun merge_ss (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}, + Simpset {simps = simps2, congs = congs2, ...}) = + let + val simps' = gen_union eq_thm (simps, simps2); + val congs' = gen_union eq_thm (congs, congs2); + val mss' = Thm.set_mk_rews (empty_mss, Thm.mk_rews_of_mss mss); + val mss' = Thm.add_simps (mss', simps'); + val mss' = Thm.add_congs (mss', congs'); + in + make_ss (mss', simps', congs', subgoal_tac, finish_tac, loop_tac) + end; + + +(* the current simpset *) val simpset = ref empty_ss; -fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac = - Simpset{mss=mss, - simps= simps, - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac= DETERM o loop_tac}; - -fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac = - Simpset{mss=mss, - simps= simps, - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac=loop_tac}; - -fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,finish_tac}) addsolver tac = - Simpset{mss=mss, - simps= simps, - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=fn hyps => finish_tac hyps ORELSE' tac hyps, - loop_tac=loop_tac}; - -fun (Simpset{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler - subgoal_tac = - Simpset{mss=mss, - simps= simps, - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac=loop_tac}; - -fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps - mk_simps = - Simpset{mss=Thm.set_mk_rews(mss,mk_simps), - simps= simps, - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac=loop_tac}; +fun Addsimps rews = (simpset := ! simpset addsimps rews); +fun Delsimps rews = (simpset := ! simpset delsimps rews); -fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews = - let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in - Simpset{mss= Thm.add_simps(mss,rews'), - simps= rews' @ simps, - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac=loop_tac} - end; -fun Addsimps rews = (simpset := !simpset addsimps rews); - -fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews = - let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in - Simpset{mss= Thm.del_simps(mss,rews'), - simps= foldl (gen_rem eq_thm) (simps,rews'), - congs= congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac=loop_tac} - end; - -fun Delsimps rews = (simpset := !simpset delsimps rews); -fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs - newcongs = - Simpset{mss= Thm.add_congs(mss,newcongs), - simps= simps, - congs= newcongs @ congs, - subgoal_tac= subgoal_tac, - finish_tac=finish_tac, - loop_tac=loop_tac}; - -fun merge_ss(Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}, - Simpset{simps=simps2,congs=congs2,...}) = - let val simps' = gen_union eq_thm (simps,simps2) - val congs' = gen_union eq_thm (congs,congs2) - val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss) - val mss' = Thm.add_simps(mss',simps') - val mss' = Thm.add_congs(mss',congs') - in Simpset{mss= mss', - simps= simps', - congs= congs', - subgoal_tac= subgoal_tac, - finish_tac= finish_tac, - loop_tac= loop_tac} - end; - -fun prems_of_ss(Simpset{mss,...}) = prems_of_mss mss; - -fun rep_ss(Simpset{simps,congs,...}) = {simps=simps,congs=congs}; +(** simplification tactics **) fun NEWSUBGOALS tac tacf = - STATE(fn state0 => - tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0))); + STATE (fn state0 => + tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0))); fun gen_simp_tac mode = fn (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) => @@ -170,20 +159,20 @@ 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 + (asm_rewrite_goal_tac mode solve_all_tac mss i THEN + (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0)) and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) in simp_loop_tac end; -val asm_full_simp_tac = gen_simp_tac (true ,true ); -val full_simp_tac = gen_simp_tac (true ,false); -val asm_simp_tac = gen_simp_tac (false,true ); -val simp_tac = gen_simp_tac (false,false); +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); -fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i; -fun Full_simp_tac i = full_simp_tac (!simpset) i; -fun Asm_simp_tac i = asm_simp_tac (!simpset) i; -fun Simp_tac i = simp_tac (!simpset) i; +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; +fun Asm_full_simp_tac i = asm_full_simp_tac (! simpset) i; end;