src/Provers/classical.ML
changeset 982 4fe0b642b7d5
parent 747 bdc066781063
child 1010 a7693f30065d
--- 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. ***)