src/Provers/classical.ML

--- a/src/Provers/classical.ML	Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Provers/classical.ML	Sat Dec 20 22:23:37 2014 +0100
@@ -234,20 +234,6 @@
     dup_netpair    : netpair,                 (*nets for duplication*)
     xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
 
-(*Desired invariants are
-        safe0_netpair = build safe0_brls,
-        safep_netpair = build safep_brls,
-        haz_netpair = build (joinrules(hazIs, hazEs)),
-        dup_netpair = build (joinrules(map dup_intr hazIs,
-                                       map dup_elim hazEs))
-
-where build = build_netpair(Net.empty,Net.empty),
-      safe0_brls contains all brules that solve the subgoal, and
-      safep_brls contains all brules that generate 1 or more new subgoals.
-The theorem lists are largely comments, though they are used in merge_cs and print_cs.
-Nets must be built incrementally, to save space and time.
-*)
-
 val empty_netpair = (Net.empty, Net.empty);
 
 val empty_cs =
@@ -712,9 +698,9 @@
       (FIRST'
        [eq_assume_tac,
         eq_mp_tac ctxt,
-        bimatch_from_nets_tac safe0_netpair,
+        bimatch_from_nets_tac ctxt safe0_netpair,
         FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
-        bimatch_from_nets_tac safep_netpair])
+        bimatch_from_nets_tac ctxt safep_netpair])
   end;
 
 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
@@ -731,15 +717,15 @@
 
 (*version of bimatch_from_nets_tac that only applies rules that
   create precisely n subgoals.*)
-fun n_bimatch_from_nets_tac n =
-  biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
+fun n_bimatch_from_nets_tac ctxt n =
+  biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true;
 
 fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
 fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
 
 (*Two-way branching is allowed only if one of the branches immediately closes*)
 fun bimatch2_tac ctxt netpair i =
-  n_bimatch_from_nets_tac 2 netpair i THEN
+  n_bimatch_from_nets_tac ctxt 2 netpair i THEN
   (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
@@ -748,9 +734,9 @@
     appSWrappers ctxt
      (FIRST'
        [eq_assume_contr_tac ctxt,
-        bimatch_from_nets_tac safe0_netpair,
+        bimatch_from_nets_tac ctxt safe0_netpair,
         FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
-        n_bimatch_from_nets_tac 1 safep_netpair,
+        n_bimatch_from_nets_tac ctxt 1 safep_netpair,
         bimatch2_tac ctxt safep_netpair])
   end;
 
@@ -764,17 +750,17 @@
 fun inst0_step_tac ctxt =
   assume_tac ctxt APPEND'
   contr_tac ctxt APPEND'
-  biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
+  biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt));
 
 (*These unsafe steps could generate more subgoals.*)
 fun instp_step_tac ctxt =
-  biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
+  biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt));
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
 
 fun haz_step_tac ctxt =
-  biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
+  biresolve_from_nets_tac ctxt (#haz_netpair (rep_claset_of ctxt));
 
 (*Single step for the prover.  FAILS unless it makes progress. *)
 fun step_tac ctxt i =
@@ -837,7 +823,7 @@
   That's hard to implement and did not perform better in experiments, due to
   greater search depth required.*)
 fun dup_step_tac ctxt =
-  biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
+  biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt));
 
 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
 local