# HG changeset patch # User oheimb # Date 856020238 -3600 # Node ID 7a962f6829ca6203d5a22812c029f9c44a7d41b8 # Parent b442786d4469dd0f65afa53e91023fbe57761e50 moved THEN_MAYBE to Pure/tctical.ML better addbefore, addafter (now: addaltern), setwrapper (now: setWrapper) and addwrapper (now addWrapper) added safe wrapper(and functions setSWrapper,compSWrapper,addSbefore,addSaltern) diff -r b442786d4469 -r 7a962f6829ca src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Feb 15 16:14:35 1997 +0100 +++ b/src/Provers/classical.ML Sat Feb 15 16:23:58 1997 +0100 @@ -14,8 +14,6 @@ the conclusion. *) -infix 1 THEN_MAYBE; - signature CLASSICAL_DATA = sig val mp : thm (* [| P-->Q; P |] ==> Q *) @@ -27,7 +25,8 @@ (*Higher precedence than := facilitates use of references*) infix 4 addSIs addSEs addSDs addIs addEs addDs delrules - setwrapper compwrapper addbefore addafter; + setSWrapper compSWrapper setWrapper compWrapper + addSbefore addSaltern addbefore addaltern; signature CLASSICAL = @@ -43,20 +42,25 @@ val addSEs : claset * thm list -> claset val addSIs : claset * thm list -> claset val delrules : claset * thm list -> claset - val setwrapper : claset * (tactic->tactic) -> claset - val compwrapper : claset * (tactic->tactic) -> claset - val addbefore : claset * tactic -> claset - val addafter : claset * tactic -> claset + val setSWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset + val compSWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset + val setWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset + val compWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset + val addSbefore : claset * (int -> tactic) -> claset + val addSaltern : claset * (int -> tactic) -> claset + val addbefore : claset * (int -> tactic) -> claset + val addaltern : claset * (int -> tactic) -> claset val print_cs : claset -> unit val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, - wrapper: tactic -> tactic, + uwrapper: (int -> tactic) -> (int -> tactic), + swrapper: (int -> tactic) -> (int -> tactic), safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair} - val getwrapper : claset -> tactic -> tactic - val THEN_MAYBE : tactic * tactic -> tactic + val getWrapper : claset -> (int -> tactic) -> (int -> tactic) + val getSWrapper : claset -> (int -> tactic) -> (int -> tactic) val fast_tac : claset -> int -> tactic val slow_tac : claset -> int -> tactic @@ -80,6 +84,7 @@ val safe_tac : claset -> tactic val safe_step_tac : claset -> int -> tactic val step_tac : claset -> int -> tactic + val slow_step_tac : claset -> int -> tactic val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) val swapify : thm list -> thm list val swap_res_tac : thm list -> int -> tactic @@ -157,7 +162,10 @@ safeEs : thm list, (*safe elimination rules*) hazIs : thm list, (*unsafe introduction rules*) hazEs : thm list, (*unsafe elimination rules*) - wrapper : tactic->tactic, (*for transforming step_tac*) + uwrapper : (int -> tactic) -> + (int -> tactic), (*for transforming step_tac*) + swrapper : (int -> tactic) -> + (int -> tactic), (*for transform. safe_step_tac*) safe0_netpair : netpair, (*nets for trivial cases*) safep_netpair : netpair, (*nets for >0 subgoals*) haz_netpair : netpair, (*nets for unsafe rules*) @@ -182,7 +190,8 @@ safeEs = [], hazIs = [], hazEs = [], - wrapper = I, + uwrapper = I, + swrapper = I, safe0_netpair = (Net.empty,Net.empty), safep_netpair = (Net.empty,Net.empty), haz_netpair = (Net.empty,Net.empty), @@ -197,7 +206,9 @@ fun rep_claset (CS args) = args; -fun getwrapper (CS{wrapper,...}) = wrapper; +fun getWrapper (CS{uwrapper,...}) = uwrapper; + +fun getSWrapper (CS{swrapper,...}) = swrapper; (*** Adding (un)safe introduction or elimination rules. @@ -244,7 +255,7 @@ (*** Safe rules ***) -fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = if gen_mem eq_thm (th, safeIs) then @@ -262,12 +273,13 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, - wrapper = wrapper, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + uwrapper = uwrapper, + swrapper = swrapper, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} end; -fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = if gen_mem eq_thm (th, safeEs) then @@ -285,9 +297,10 @@ safeIs = safeIs, hazIs = hazIs, hazEs = hazEs, - wrapper = wrapper, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + uwrapper = uwrapper, + swrapper = swrapper, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} end; fun rev_foldl f (e, l) = foldl f (e, rev l); @@ -300,7 +313,7 @@ (*** Hazardous (unsafe) rules ***) -fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th)= if gen_mem eq_thm (th, hazIs) then @@ -316,12 +329,13 @@ safeIs = safeIs, safeEs = safeEs, hazEs = hazEs, - wrapper = wrapper, + uwrapper = uwrapper, + swrapper = swrapper, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair} end; -fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = if gen_mem eq_thm (th, hazEs) then @@ -337,7 +351,8 @@ safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, - wrapper = wrapper, + uwrapper = uwrapper, + swrapper = swrapper, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair} end; @@ -355,7 +370,7 @@ searches in all the lists and chooses the relevant delXX function. ***) -fun delSI (CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun delSI (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] @@ -365,12 +380,13 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, - wrapper = wrapper, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + uwrapper = uwrapper, + swrapper = swrapper, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} end; -fun delSE (CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun delSE (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] @@ -380,13 +396,14 @@ safeIs = safeIs, hazIs = hazIs, hazEs = hazEs, - wrapper = wrapper, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + uwrapper = uwrapper, + swrapper = swrapper, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} end; -fun delI (CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun delI (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = CS{hazIs = gen_rem eq_thm (hazIs,th), @@ -395,11 +412,12 @@ safeIs = safeIs, safeEs = safeEs, hazEs = hazEs, - wrapper = wrapper, + uwrapper = uwrapper, + swrapper = swrapper, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair}; -fun delE (CS{safeIs, safeEs, hazIs, hazEs, wrapper, +fun delE (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = CS{hazEs = gen_rem eq_thm (hazEs,th), @@ -408,7 +426,8 @@ safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, - wrapper = wrapper, + uwrapper = uwrapper, + swrapper = swrapper, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair}; @@ -423,47 +442,62 @@ val op delrules = foldl delrule; -(*** Setting or modifying the wrapper tactical ***) +(*** Setting or modifying the wrapper tacticals ***) -(*Set a new wrapper*) -fun (CS{safeIs, safeEs, hazIs, hazEs, +(*Set a new uwrapper*) +fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) - setwrapper new_wrapper = - CS{wrapper = new_wrapper, - safeIs = safeIs, + setWrapper new_uwrapper = + CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + uwrapper = new_uwrapper, + swrapper = swrapper, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, haz_netpair = haz_netpair, dup_netpair = dup_netpair}; -(*Compose a tactical with the existing wrapper*) -fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs); +(*Set a new swrapper*) +fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) + setSWrapper new_swrapper = + CS{safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + uwrapper = uwrapper, + swrapper = new_swrapper, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair}; -(*Execute tac1, but only execute tac2 if there are at least as many subgoals - as before. This ensures that tac2 is only applied to an outcome of tac1.*) -fun tac1 THEN_MAYBE tac2 = - STATE (fn state => - tac1 THEN - COND (has_fewer_prems (nprems_of state)) all_tac tac2); +(*Compose a tactical with the existing uwrapper*) +fun cs compWrapper uwrapper' = cs setWrapper (uwrapper' o getWrapper cs); + +(*Compose a tactical with the existing swrapper*) +fun cs compSWrapper swrapper' = cs setSWrapper (swrapper' o getSWrapper cs); -(*Cause a tactic to be executed before/after the step tactic*) -fun cs addbefore tac2 = cs compwrapper (fn tac1 => tac2 THEN_MAYBE tac1); -fun cs addafter tac2 = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2); +(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) +fun cs addSbefore tac1 = cs compSWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); +fun cs addSaltern tac2 = cs compSWrapper (fn tac1 => tac1 ORELSE' tac2); +(*compose a tactic sequentially before/alternatively after the step tactic*) +fun cs addbefore tac1 = cs compWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); +fun cs addaltern tac2 = cs compWrapper (fn tac1 => tac1 APPEND' tac2); (*Merge works by adding all new rules of the 2nd claset into the 1st claset. Merging the term nets may look more efficient, but the rather delicate treatment of priority might get muddled up.*) fun merge_cs - (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, ...}, + (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) = let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) val safeEs' = gen_rems eq_thm (safeEs2,safeEs) - val hazIs' = gen_rems eq_thm (hazIs2,hazIs) - val hazEs' = gen_rems eq_thm (hazEs2,hazEs) + val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) + val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) in cs addSIs safeIs' addSEs safeEs' addIs hazIs' @@ -474,15 +508,17 @@ (**** Simple tactics for theorem proving ****) (*Attack subgoals using safe inferences -- matching, not resolution*) -fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = - FIRST' [eq_assume_tac, - eq_mp_tac, - bimatch_from_nets_tac safe0_netpair, - FIRST' hyp_subst_tacs, - bimatch_from_nets_tac safep_netpair] ; +fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = + getSWrapper cs (FIRST' [ + eq_assume_tac, + eq_mp_tac, + bimatch_from_nets_tac safe0_netpair, + FIRST' hyp_subst_tacs, + bimatch_from_nets_tac safep_netpair]); (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) -fun safe_tac cs = REPEAT_DETERM_FIRST (safe_step_tac cs); +fun safe_tac cs = REPEAT_DETERM_FIRST + (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); (*But these unsafe steps at least solve a subgoal!*) fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = @@ -501,15 +537,13 @@ biresolve_from_nets_tac haz_netpair; (*Single step for the prover. FAILS unless it makes progress. *) -fun step_tac cs i = - getwrapper cs - (FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]); +fun step_tac cs i = getWrapper cs + (K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) i; (*Using a "safe" rule to instantiate variables is unsafe. This tactic allows backtracking from "safe" rules to "unsafe" rules here.*) -fun slow_step_tac cs i = - getwrapper cs - (safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i)); +fun slow_step_tac cs i = getWrapper cs + (K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i; (**** The following tactics all fail unless they solve one goal ****) @@ -553,13 +587,13 @@ (*Searching to depth m.*) fun depth_tac cs m i = STATE(fn state => SELECT_GOAL - (getwrapper cs - (REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE - (DEPTH_SOLVE (depth_tac cs m 1), - inst0_step_tac cs 1 APPEND + (getWrapper cs + (fn i => REPEAT_DETERM1 (safe_step_tac cs i) THEN_ELSE + (DEPTH_SOLVE (depth_tac cs m i), + inst0_step_tac cs i APPEND COND (K(m=0)) no_tac - ((instp_step_tac cs 1 APPEND dup_step_tac cs 1) - THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))))) + ((instp_step_tac cs i APPEND dup_step_tac cs i) + THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1) i); (*Iterative deepening tactical. Allows us to "deepen" any search tactic*) @@ -618,3 +652,5 @@ end; end; + +