# HG changeset patch # User lcp # Date 796563874 -7200 # Node ID 4fe0b642b7d503de9190204cc68a25897e6bd0a2 # Parent 864370666a241547dafbd64f936aafdd25632629 Addition of wrappers for integration with the simplifier. New infixes setwrapper compwrapper addbefore addafter. New function getwrapper. The wrapper is a tactical that is applied to the step tactic. By default it is the identity. Using THEN one can cause other tactics to be tried before or after the step tactic. Other effects are possible using ORELSE, etc. diff -r 864370666a24 -r 4fe0b642b7d5 src/Provers/classical.ML --- a/src/Provers/classical.ML Thu Mar 30 13:36:00 1995 +0200 +++ b/src/Provers/classical.ML Thu Mar 30 13:44:34 1995 +0200 @@ -14,6 +14,8 @@ the conclusion. *) +infix 1 THEN_MAYBE; + signature CLASSICAL_DATA = sig val mp : thm (* [| P-->Q; P |] ==> Q *) @@ -24,7 +26,8 @@ end; (*Higher precedence than := facilitates use of references*) -infix 4 addSIs addSEs addSDs addIs addEs addDs; +infix 4 addSIs addSEs addSDs addIs addEs addDs + setwrapper compwrapper addbefore addafter; signature CLASSICAL = @@ -37,9 +40,18 @@ val addSDs : claset * thm list -> claset val addSEs : claset * thm list -> claset val addSIs : 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 print_cs : claset -> unit val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, - hazIs: thm list, hazEs: thm list} + hazIs: thm list, hazEs: thm list, + wrapper: tactic -> tactic} + val getwrapper : claset -> tactic -> tactic + val THEN_MAYBE : tactic * tactic -> tactic + val best_tac : claset -> int -> tactic val contr_tac : int -> tactic val depth_tac : claset -> int -> int -> tactic @@ -111,20 +123,24 @@ type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; datatype claset = - CS of {safeIs : thm list, - safeEs : thm list, - hazIs : thm list, - hazEs : thm list, - safe0_netpair : netpair, - safep_netpair : netpair, - haz_netpair : netpair, - dup_netpair : netpair}; + CS of {safeIs : thm list, (*safe introduction rules*) + 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*) + safe0_netpair : netpair, (*nets for trivial cases*) + safep_netpair : netpair, (*nets for >0 subgoals*) + haz_netpair : netpair, (*nets for unsafe rules*) + dup_netpair : netpair}; (*nets for duplication*) -fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) = - {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; +fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) = + {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper}; -(*For use with biresolve_tac. Combines intrs with swap to catch negated - assumptions; pairs elims with true; sorts. *) +fun getwrapper (CS{wrapper,...}) = wrapper; + +(*For use with biresolve_tac. Combines intr rules with swap to handle negated + assumptions. Pairs elim rules with true. Sorts the list of pairs by + the number of new subgoals generated. *) fun joinrules (intrs,elims) = sort lessb (map (pair true) (elims @ swapify intrs) @ @@ -133,7 +149,7 @@ val build = build_netpair(Net.empty,Net.empty); (*Make a claset from the four kinds of rules*) -fun make_cs {safeIs,safeEs,hazIs,hazEs} = +fun make_cs {safeIs,safeEs,hazIs,hazEs,wrapper} = let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) take_prefix (fn brl => subgoals_of_brl brl=0) (joinrules(safeIs, safeEs)) @@ -141,6 +157,7 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + wrapper = wrapper, safe0_netpair = build safe0_brls, safep_netpair = build safep_brls, haz_netpair = build (joinrules(hazIs, hazEs)), @@ -150,7 +167,7 @@ (*** Manipulation of clasets ***) -val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; +val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[], wrapper=I}; fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = (writeln"Introduction rules"; prths hazIs; @@ -159,22 +176,51 @@ writeln"Safe elimination rules"; prths safeEs; ()); -fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = - make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; +(** Adding new (un)safe introduction or elimination rules **) -fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = - make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs}; +fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSIs ths = + make_cs {safeIs=ths@safeIs, + safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper}; + +fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSEs ths = + make_cs {safeEs=ths@safeEs, + safeIs=safeIs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper}; fun cs addSDs ths = cs addSEs (map make_elim ths); -fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths = - make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs}; +fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addIs ths = + make_cs {hazIs=ths@hazIs, + safeIs=safeIs, safeEs=safeEs, hazEs=hazEs, wrapper=wrapper}; -fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths = - make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs}; +fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addEs ths = + make_cs {hazEs=ths@hazEs, + safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, wrapper=wrapper}; fun cs addDs ths = cs addEs (map make_elim ths); +(** Setting or modifying the wrapper tactical **) + +(*Set a new wrapper*) +fun (CS{safeIs,safeEs,hazIs,hazEs,...}) setwrapper wrapper = + make_cs {wrapper=wrapper, + safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; + +(*Compose a tactical with the existing wrapper*) +fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs); + +(*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); + +(*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); + + + (*** Simple tactics for theorem proving ***) (*Attack subgoals using safe inferences -- matching, not resolution*) @@ -201,17 +247,19 @@ (*These steps could instantiate variables and are therefore unsafe.*) fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; -fun haz_step_tac (cs as (CS{haz_netpair,...})) = +fun haz_step_tac (CS{haz_netpair,...}) = biresolve_from_nets_tac haz_netpair; (*Single step for the prover. FAILS unless it makes progress. *) fun step_tac cs i = - FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]; + getwrapper cs + (FIRST [safe_tac cs, inst_step_tac cs i, 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 = - safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i); + getwrapper cs + (safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i)); (*** The following tactics all fail unless they solve one goal ***) @@ -228,7 +276,7 @@ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); -(*** Complete tactic, loosely based upon LeanTaP This tactic is the outcome +(*** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome of much experimentation! Changing APPEND to ORELSE below would prove easy theorems faster, but loses completeness -- and many of the harder theorems such as 43. ***)