proper context for "net" tactics;
authorwenzelm
Sat Dec 20 22:23:37 2014 +0100 (2014-12-20)
changeset 59164ff40c53d1af9
parent 59163 857a600f0c94
child 59165 115965966e15
proper context for "net" tactics;
avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
src/CTT/CTT.thy
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/record.ML
src/Provers/classical.ML
src/Provers/typedsimp.ML
src/Pure/tactic.ML
src/Sequents/modal.ML
src/Tools/intuitionistic.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/CTT/CTT.thy	Sat Dec 20 19:12:41 2014 +0100
     1.2 +++ b/src/CTT/CTT.thy	Sat Dec 20 22:23:37 2014 +0100
     1.3 @@ -348,26 +348,34 @@
     1.4      @{thms elimL_rls} @ @{thms refl_elem}
     1.5  in
     1.6  
     1.7 -fun routine_tac rls ctxt prems = ASSUME ctxt (filt_resolve_tac (prems @ rls) 4);
     1.8 +fun routine_tac rls ctxt prems =
     1.9 +  ASSUME ctxt (filt_resolve_from_net_tac ctxt 4 (Tactic.build_net (prems @ rls)));
    1.10  
    1.11  (*Solve all subgoals "A type" using formation rules. *)
    1.12 -fun form_tac ctxt = REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac @{thms form_rls} 1));
    1.13 +val form_net = Tactic.build_net @{thms form_rls};
    1.14 +fun form_tac ctxt =
    1.15 +  REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net));
    1.16  
    1.17  (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    1.18  fun typechk_tac ctxt thms =
    1.19 -  let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
    1.20 +  let val tac =
    1.21 +    filt_resolve_from_net_tac ctxt 3
    1.22 +      (Tactic.build_net (thms @ @{thms form_rls} @ @{thms element_rls}))
    1.23    in  REPEAT_FIRST (ASSUME ctxt tac)  end
    1.24  
    1.25  (*Solve a:A (a flexible, A rigid) by introduction rules.
    1.26    Cannot use stringtrees (filt_resolve_tac) since
    1.27    goals like ?a:SUM(A,B) have a trivial head-string *)
    1.28  fun intr_tac ctxt thms =
    1.29 -  let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
    1.30 +  let val tac =
    1.31 +    filt_resolve_from_net_tac ctxt 1
    1.32 +      (Tactic.build_net (thms @ @{thms form_rls} @ @{thms intr_rls}))
    1.33    in  REPEAT_FIRST (ASSUME ctxt tac)  end
    1.34  
    1.35  (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
    1.36  fun equal_tac ctxt thms =
    1.37 -  REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3))
    1.38 +  REPEAT_FIRST
    1.39 +    (ASSUME ctxt (filt_resolve_from_net_tac ctxt 3 (Tactic.build_net (thms @ equal_rls))))
    1.40  
    1.41  end
    1.42  *}
    1.43 @@ -404,8 +412,9 @@
    1.44  ML {*
    1.45  (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
    1.46    Uses other intro rules to avoid changing flexible goals.*)
    1.47 +val eqintr_net = Tactic.build_net @{thms EqI intr_rls}
    1.48  fun eqintr_tac ctxt =
    1.49 -  REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
    1.50 +  REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 eqintr_net))
    1.51  
    1.52  (** Tactics that instantiate CTT-rules.
    1.53      Vars in the given terms will be incremented!
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Dec 20 19:12:41 2014 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Dec 20 22:23:37 2014 +0100
     2.3 @@ -502,7 +502,7 @@
     2.4    then  Seq.empty  else  Seq.single st;
     2.5  
     2.6  
     2.7 -(* net_resolve_tac actually made it slower... *)
     2.8 +(* resolve_from_net_tac actually made it slower... *)
     2.9  fun prolog_step_tac ctxt horns i =
    2.10      (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
    2.11      TRYALL_eq_assume_tac;
    2.12 @@ -744,7 +744,7 @@
    2.13  fun prolog_step_tac' ctxt horns =
    2.14      let val (horn0s, _) = (*0 subgoals vs 1 or more*)
    2.15              take_prefix Thm.no_prems horns
    2.16 -        val nrtac = net_resolve_tac horns
    2.17 +        val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
    2.18      in  fn i => eq_assume_tac i ORELSE
    2.19                  match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
    2.20                  ((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
     3.1 --- a/src/HOL/Tools/record.ML	Sat Dec 20 19:12:41 2014 +0100
     3.2 +++ b/src/HOL/Tools/record.ML	Sat Dec 20 22:23:37 2014 +0100
     3.3 @@ -59,7 +59,7 @@
     3.4      typ * typ -> theory -> (term * term) * theory
     3.5    val mk_cons_tuple: term * term -> term
     3.6    val dest_cons_tuple: term -> term * term
     3.7 -  val iso_tuple_intros_tac: int -> tactic
     3.8 +  val iso_tuple_intros_tac: Proof.context -> int -> tactic
     3.9    val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    3.10  end;
    3.11  
    3.12 @@ -165,8 +165,8 @@
    3.13      ((isom, cons $ isom), thm_thy)
    3.14    end;
    3.15  
    3.16 -val iso_tuple_intros_tac =
    3.17 -  resolve_from_net_tac iso_tuple_intros THEN'
    3.18 +fun iso_tuple_intros_tac ctxt =
    3.19 +  resolve_from_net_tac ctxt iso_tuple_intros THEN'
    3.20    CSUBGOAL (fn (cgoal, i) =>
    3.21      let
    3.22        val thy = Thm.theory_of_cterm cgoal;
    3.23 @@ -968,7 +968,7 @@
    3.24            Goal.prove (Proof_Context.init_global thy) [] [] prop
    3.25              (fn {context = ctxt, ...} =>
    3.26                simp_tac (put_simpset defset ctxt) 1 THEN
    3.27 -              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
    3.28 +              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN
    3.29                TRY (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms id_apply id_o o_id}) 1));
    3.30          val dest =
    3.31            if is_sel_upd_pair thy acc upd
    3.32 @@ -992,7 +992,7 @@
    3.33        Goal.prove (Proof_Context.init_global thy) [] [] prop
    3.34          (fn {context = ctxt, ...} =>
    3.35            simp_tac (put_simpset defset ctxt) 1 THEN
    3.36 -          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
    3.37 +          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN
    3.38            TRY (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms id_apply}) 1));
    3.39      val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
    3.40    in Drule.export_without_context (othm RS dest) end;
    3.41 @@ -1127,7 +1127,7 @@
    3.42      Goal.prove (Proof_Context.init_global thy) [] [] prop
    3.43        (fn {context = ctxt, ...} =>
    3.44          simp_tac (put_simpset ss ctxt) 1 THEN
    3.45 -        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
    3.46 +        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN
    3.47          TRY (resolve_tac [updacc_cong_idI] 1))
    3.48    end;
    3.49  
    3.50 @@ -1595,7 +1595,7 @@
    3.51              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
    3.52              REPEAT_DETERM
    3.53                (rtac @{thm refl_conj_eq} 1 ORELSE
    3.54 -                Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
    3.55 +                Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
    3.56                  rtac refl 1))));
    3.57  
    3.58  
    3.59 @@ -1612,7 +1612,7 @@
    3.60          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
    3.61          val tactic1 =
    3.62            simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
    3.63 -          REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
    3.64 +          REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1;
    3.65          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
    3.66          val [halfway] = Seq.list_of (tactic1 start);
    3.67          val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
    3.68 @@ -1952,7 +1952,7 @@
    3.69            val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
    3.70            val tactic =
    3.71              simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
    3.72 -            REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
    3.73 +            REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ext_ctxt 1 ORELSE terminal);
    3.74            val updaccs = Seq.list_of (tactic init_thm);
    3.75          in
    3.76            (updaccs RL [updacc_accessor_eqE],
    3.77 @@ -2137,7 +2137,7 @@
    3.78             [rtac surject_assist_idE 1,
    3.79              simp_tac (put_simpset HOL_basic_ss ctxt addsimps ext_defs) 1,
    3.80              REPEAT
    3.81 -              (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
    3.82 +              (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
    3.83                  (rtac surject_assistI 1 THEN
    3.84                    simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt
    3.85                      addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
     4.1 --- a/src/Provers/classical.ML	Sat Dec 20 19:12:41 2014 +0100
     4.2 +++ b/src/Provers/classical.ML	Sat Dec 20 22:23:37 2014 +0100
     4.3 @@ -234,20 +234,6 @@
     4.4      dup_netpair    : netpair,                 (*nets for duplication*)
     4.5      xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
     4.6  
     4.7 -(*Desired invariants are
     4.8 -        safe0_netpair = build safe0_brls,
     4.9 -        safep_netpair = build safep_brls,
    4.10 -        haz_netpair = build (joinrules(hazIs, hazEs)),
    4.11 -        dup_netpair = build (joinrules(map dup_intr hazIs,
    4.12 -                                       map dup_elim hazEs))
    4.13 -
    4.14 -where build = build_netpair(Net.empty,Net.empty),
    4.15 -      safe0_brls contains all brules that solve the subgoal, and
    4.16 -      safep_brls contains all brules that generate 1 or more new subgoals.
    4.17 -The theorem lists are largely comments, though they are used in merge_cs and print_cs.
    4.18 -Nets must be built incrementally, to save space and time.
    4.19 -*)
    4.20 -
    4.21  val empty_netpair = (Net.empty, Net.empty);
    4.22  
    4.23  val empty_cs =
    4.24 @@ -712,9 +698,9 @@
    4.25        (FIRST'
    4.26         [eq_assume_tac,
    4.27          eq_mp_tac ctxt,
    4.28 -        bimatch_from_nets_tac safe0_netpair,
    4.29 +        bimatch_from_nets_tac ctxt safe0_netpair,
    4.30          FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
    4.31 -        bimatch_from_nets_tac safep_netpair])
    4.32 +        bimatch_from_nets_tac ctxt safep_netpair])
    4.33    end;
    4.34  
    4.35  (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
    4.36 @@ -731,15 +717,15 @@
    4.37  
    4.38  (*version of bimatch_from_nets_tac that only applies rules that
    4.39    create precisely n subgoals.*)
    4.40 -fun n_bimatch_from_nets_tac n =
    4.41 -  biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
    4.42 +fun n_bimatch_from_nets_tac ctxt n =
    4.43 +  biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true;
    4.44  
    4.45  fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
    4.46  fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
    4.47  
    4.48  (*Two-way branching is allowed only if one of the branches immediately closes*)
    4.49  fun bimatch2_tac ctxt netpair i =
    4.50 -  n_bimatch_from_nets_tac 2 netpair i THEN
    4.51 +  n_bimatch_from_nets_tac ctxt 2 netpair i THEN
    4.52    (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
    4.53  
    4.54  (*Attack subgoals using safe inferences -- matching, not resolution*)
    4.55 @@ -748,9 +734,9 @@
    4.56      appSWrappers ctxt
    4.57       (FIRST'
    4.58         [eq_assume_contr_tac ctxt,
    4.59 -        bimatch_from_nets_tac safe0_netpair,
    4.60 +        bimatch_from_nets_tac ctxt safe0_netpair,
    4.61          FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
    4.62 -        n_bimatch_from_nets_tac 1 safep_netpair,
    4.63 +        n_bimatch_from_nets_tac ctxt 1 safep_netpair,
    4.64          bimatch2_tac ctxt safep_netpair])
    4.65    end;
    4.66  
    4.67 @@ -764,17 +750,17 @@
    4.68  fun inst0_step_tac ctxt =
    4.69    assume_tac ctxt APPEND'
    4.70    contr_tac ctxt APPEND'
    4.71 -  biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
    4.72 +  biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt));
    4.73  
    4.74  (*These unsafe steps could generate more subgoals.*)
    4.75  fun instp_step_tac ctxt =
    4.76 -  biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
    4.77 +  biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt));
    4.78  
    4.79  (*These steps could instantiate variables and are therefore unsafe.*)
    4.80  fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
    4.81  
    4.82  fun haz_step_tac ctxt =
    4.83 -  biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
    4.84 +  biresolve_from_nets_tac ctxt (#haz_netpair (rep_claset_of ctxt));
    4.85  
    4.86  (*Single step for the prover.  FAILS unless it makes progress. *)
    4.87  fun step_tac ctxt i =
    4.88 @@ -837,7 +823,7 @@
    4.89    That's hard to implement and did not perform better in experiments, due to
    4.90    greater search depth required.*)
    4.91  fun dup_step_tac ctxt =
    4.92 -  biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
    4.93 +  biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt));
    4.94  
    4.95  (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
    4.96  local
     5.1 --- a/src/Provers/typedsimp.ML	Sat Dec 20 19:12:41 2014 +0100
     5.2 +++ b/src/Provers/typedsimp.ML	Sat Dec 20 22:23:37 2014 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  *)
     5.5  
     5.6  signature TSIMP_DATA =
     5.7 -  sig
     5.8 +sig
     5.9    val refl: thm         (*Reflexive law*)
    5.10    val sym: thm          (*Symmetric law*)
    5.11    val trans: thm        (*Transitive law*)
    5.12 @@ -19,23 +19,22 @@
    5.13    val default_rls: thm list
    5.14    (*Type checking or similar -- solution of routine conditions*)
    5.15    val routine_tac: Proof.context -> thm list -> int -> tactic
    5.16 -  end;
    5.17 +end;
    5.18  
    5.19  signature TSIMP =
    5.20 -  sig
    5.21 -  val asm_res_tac: Proof.context -> thm list -> int -> tactic   
    5.22 +sig
    5.23 +  val asm_res_tac: Proof.context -> thm list -> int -> tactic
    5.24    val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic
    5.25    val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic
    5.26    val norm_tac: Proof.context -> (thm list * thm list) -> tactic
    5.27    val process_rules: thm list -> thm list * thm list
    5.28 -  val rewrite_res_tac: int -> tactic   
    5.29 +  val rewrite_res_tac: Proof.context -> int -> tactic
    5.30    val split_eqn: thm
    5.31    val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic
    5.32 -  val subconv_res_tac: thm list -> int -> tactic   
    5.33 -  end;
    5.34 +  val subconv_res_tac: Proof.context -> thm list -> int -> tactic
    5.35 +end;
    5.36  
    5.37 -
    5.38 -functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = 
    5.39 +functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =
    5.40  struct
    5.41  local open TSimp_data
    5.42  in
    5.43 @@ -72,45 +71,46 @@
    5.44  fun process_rules rls = fold_rev add_rule rls ([], []);
    5.45  
    5.46  (*Given list of rewrite rules, return list of both forms, reject others*)
    5.47 -fun process_rewrites rls = 
    5.48 +fun process_rewrites rls =
    5.49    case process_rules rls of
    5.50        (simp_rls,[])  =>  simp_rls
    5.51 -    | (_,others) => raise THM 
    5.52 +    | (_,others) => raise THM
    5.53          ("process_rewrites: Ill-formed rewrite", 0, others);
    5.54  
    5.55  (*Process the default rewrite rules*)
    5.56  val simp_rls = process_rewrites default_rls;
    5.57 +val simp_net = Tactic.build_net simp_rls;
    5.58  
    5.59  (*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
    5.60    will fail!  The filter will pass all the rules, and the bound permits
    5.61    no ambiguity.*)
    5.62  
    5.63  (*Resolution with rewrite/sub rules.  Builds the tree for filt_resolve_tac.*)
    5.64 -val rewrite_res_tac = filt_resolve_tac simp_rls 2;
    5.65 +fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net;
    5.66  
    5.67  (*The congruence rules for simplifying subterms.  If subgoal is too flexible
    5.68      then only refl,refl_red will be used (if even them!). *)
    5.69 -fun subconv_res_tac congr_rls =
    5.70 -  filt_resolve_tac (map subconv_rule congr_rls) 2
    5.71 -  ORELSE'  filt_resolve_tac [refl,refl_red] 1;
    5.72 +fun subconv_res_tac ctxt congr_rls =
    5.73 +  filt_resolve_from_net_tac ctxt 2 (Tactic.build_net (map subconv_rule congr_rls))
    5.74 +  ORELSE'  filt_resolve_from_net_tac ctxt 1 (Tactic.build_net [refl, refl_red]);
    5.75  
    5.76  (*Resolve with asms, whether rewrites or not*)
    5.77  fun asm_res_tac ctxt asms =
    5.78 -    let val (xsimp_rls,xother_rls) = process_rules asms
    5.79 -    in  routine_tac ctxt xother_rls  ORELSE'  
    5.80 -        filt_resolve_tac xsimp_rls 2
    5.81 +    let val (xsimp_rls, xother_rls) = process_rules asms
    5.82 +    in  routine_tac ctxt xother_rls  ORELSE'
    5.83 +        filt_resolve_from_net_tac ctxt 2 (Tactic.build_net xsimp_rls)
    5.84      end;
    5.85  
    5.86  (*Single step for simple rewriting*)
    5.87 -fun step_tac ctxt (congr_rls,asms) =
    5.88 -    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac  ORELSE'  
    5.89 -    subconv_res_tac congr_rls;
    5.90 +fun step_tac ctxt (congr_rls, asms) =
    5.91 +    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac ctxt  ORELSE'
    5.92 +    subconv_res_tac ctxt congr_rls;
    5.93  
    5.94  (*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
    5.95  fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
    5.96 -    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac  ORELSE'  
    5.97 -    (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'  
    5.98 -    subconv_res_tac congr_rls;
    5.99 +    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac ctxt  ORELSE'
   5.100 +    (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'
   5.101 +    subconv_res_tac ctxt congr_rls;
   5.102  
   5.103  (*Unconditional normalization tactic*)
   5.104  fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg)  THEN
   5.105 @@ -123,4 +123,3 @@
   5.106  end;
   5.107  end;
   5.108  
   5.109 -
     6.1 --- a/src/Pure/tactic.ML	Sat Dec 20 19:12:41 2014 +0100
     6.2 +++ b/src/Pure/tactic.ML	Sat Dec 20 22:23:37 2014 +0100
     6.3 @@ -35,19 +35,15 @@
     6.4    val cut_rules_tac: thm list -> int -> tactic
     6.5    val cut_facts_tac: thm list -> int -> tactic
     6.6    val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
     6.7 -  val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
     6.8 -    bool -> 'a Net.net * 'a Net.net -> int -> tactic
     6.9 -  val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    6.10 -    int -> tactic
    6.11 -  val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    6.12 -    int -> tactic
    6.13 -  val net_biresolve_tac: (bool * thm) list -> int -> tactic
    6.14 -  val net_bimatch_tac: (bool * thm) list -> int -> tactic
    6.15 -  val filt_resolve_tac: thm list -> int -> int -> tactic
    6.16 -  val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
    6.17 -  val match_from_net_tac: (int * thm) Net.net -> int -> tactic
    6.18 -  val net_resolve_tac: thm list -> int -> tactic
    6.19 -  val net_match_tac: thm list -> int -> tactic
    6.20 +  val biresolution_from_nets_tac: Proof.context ->
    6.21 +    ('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
    6.22 +  val biresolve_from_nets_tac: Proof.context ->
    6.23 +    (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
    6.24 +  val bimatch_from_nets_tac: Proof.context ->
    6.25 +    (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
    6.26 +  val filt_resolve_from_net_tac: Proof.context -> int -> (int * thm) Net.net -> int -> tactic
    6.27 +  val resolve_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
    6.28 +  val match_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
    6.29    val subgoals_of_brl: bool * thm -> int
    6.30    val lessb: (bool * thm) * (bool * thm) -> bool
    6.31    val rename_tac: string list -> int -> tactic
    6.32 @@ -63,8 +59,6 @@
    6.33    val insert_tagged_brl: 'a * (bool * thm) ->
    6.34      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    6.35        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    6.36 -  val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    6.37 -    (bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
    6.38    val delete_tagged_brl: bool * thm ->
    6.39      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    6.40        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    6.41 @@ -219,10 +213,6 @@
    6.42      | NONE => error "insert_tagged_brl: elimination rule with no premises")
    6.43    else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
    6.44  
    6.45 -(*build a pair of nets for biresolution*)
    6.46 -fun build_netpair netpair brls =
    6.47 -    fold_rev insert_tagged_brl (tag_list 1 brls) netpair;
    6.48 -
    6.49  (*delete one kbrl from the pair of nets*)
    6.50  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
    6.51  
    6.52 @@ -238,24 +228,19 @@
    6.53  (*biresolution using a pair of nets rather than rules.
    6.54      function "order" must sort and possibly filter the list of brls.
    6.55      boolean "match" indicates matching or unification.*)
    6.56 -fun biresolution_from_nets_tac order match (inet,enet) =
    6.57 +fun biresolution_from_nets_tac ctxt order match (inet, enet) =
    6.58    SUBGOAL
    6.59 -    (fn (prem,i) =>
    6.60 -      let val hyps = Logic.strip_assums_hyp prem
    6.61 -          and concl = Logic.strip_assums_concl prem
    6.62 -          val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
    6.63 -      in PRIMSEQ (Thm.biresolution NONE match (order kbrls) i) end);
    6.64 +    (fn (prem, i) =>
    6.65 +      let
    6.66 +        val hyps = Logic.strip_assums_hyp prem;
    6.67 +        val concl = Logic.strip_assums_concl prem;
    6.68 +        val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
    6.69 +      in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order kbrls) i) end);
    6.70  
    6.71  (*versions taking pre-built nets.  No filtering of brls*)
    6.72 -val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
    6.73 -val bimatch_from_nets_tac   = biresolution_from_nets_tac order_list true;
    6.74 +fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list false;
    6.75 +fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list true;
    6.76  
    6.77 -(*fast versions using nets internally*)
    6.78 -val net_biresolve_tac =
    6.79 -    biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
    6.80 -
    6.81 -val net_bimatch_tac =
    6.82 -    bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
    6.83  
    6.84  (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
    6.85  
    6.86 @@ -268,27 +253,23 @@
    6.87    fold_rev insert_krl (tag_list 1 rls) Net.empty;
    6.88  
    6.89  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
    6.90 -fun filt_resolution_from_net_tac match pred net =
    6.91 -  SUBGOAL (fn (prem,i) =>
    6.92 +fun filt_resolution_from_net_tac ctxt match pred net =
    6.93 +  SUBGOAL (fn (prem, i) =>
    6.94      let val krls = Net.unify_term net (Logic.strip_assums_concl prem) in
    6.95        if pred krls then
    6.96 -        PRIMSEQ (Thm.biresolution NONE match (map (pair false) (order_list krls)) i)
    6.97 +        PRIMSEQ (Thm.biresolution (SOME ctxt) match (map (pair false) (order_list krls)) i)
    6.98        else no_tac
    6.99      end);
   6.100  
   6.101  (*Resolve the subgoal using the rules (making a net) unless too flexible,
   6.102     which means more than maxr rules are unifiable.      *)
   6.103 -fun filt_resolve_tac rules maxr =
   6.104 -    let fun pred krls = length krls <= maxr
   6.105 -    in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   6.106 +fun filt_resolve_from_net_tac ctxt maxr net =
   6.107 +  let fun pred krls = length krls <= maxr
   6.108 +  in filt_resolution_from_net_tac ctxt false pred net end;
   6.109  
   6.110  (*versions taking pre-built nets*)
   6.111 -val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   6.112 -val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   6.113 -
   6.114 -(*fast versions using nets internally*)
   6.115 -val net_resolve_tac = resolve_from_net_tac o build_net;
   6.116 -val net_match_tac = match_from_net_tac o build_net;
   6.117 +fun resolve_from_net_tac ctxt = filt_resolution_from_net_tac ctxt false (K true);
   6.118 +fun match_from_net_tac ctxt = filt_resolution_from_net_tac ctxt true (K true);
   6.119  
   6.120  
   6.121  (*** For Natural Deduction using (bires_flg, rule) pairs ***)
     7.1 --- a/src/Sequents/modal.ML	Sat Dec 20 19:12:41 2014 +0100
     7.2 +++ b/src/Sequents/modal.ML	Sat Dec 20 22:23:37 2014 +0100
     7.3 @@ -7,22 +7,22 @@
     7.4  
     7.5  signature MODAL_PROVER_RULE =
     7.6  sig
     7.7 -    val rewrite_rls      : thm list
     7.8 -    val safe_rls         : thm list
     7.9 -    val unsafe_rls       : thm list
    7.10 -    val bound_rls        : thm list
    7.11 -    val aside_rls        : thm list
    7.12 +  val rewrite_rls      : thm list
    7.13 +  val safe_rls         : thm list
    7.14 +  val unsafe_rls       : thm list
    7.15 +  val bound_rls        : thm list
    7.16 +  val aside_rls        : thm list
    7.17  end;
    7.18  
    7.19 -signature MODAL_PROVER = 
    7.20 +signature MODAL_PROVER =
    7.21  sig
    7.22 -    val rule_tac   : thm list -> int ->tactic
    7.23 -    val step_tac   : int -> tactic
    7.24 -    val solven_tac : int -> int -> tactic
    7.25 -    val solve_tac  : Proof.context -> int -> tactic
    7.26 +  val rule_tac   : Proof.context -> thm list -> int ->tactic
    7.27 +  val step_tac   : Proof.context -> int -> tactic
    7.28 +  val solven_tac : Proof.context -> int -> int -> tactic
    7.29 +  val solve_tac  : Proof.context -> int -> tactic
    7.30  end;
    7.31  
    7.32 -functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
    7.33 +functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER =
    7.34  struct
    7.35  
    7.36  (*Returns the list of all formulas in the sequent*)
    7.37 @@ -35,7 +35,7 @@
    7.38    Assumes each formula in seqc is surrounded by sequence variables
    7.39    -- checks that each concl formula looks like some subgoal formula.*)
    7.40  fun could_res (seqp,seqc) =
    7.41 -      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
    7.42 +      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
    7.43                                (forms_of_seq seqp))
    7.44               (forms_of_seq seqc);
    7.45  
    7.46 @@ -59,11 +59,12 @@
    7.47  
    7.48  (* NB No back tracking possible with aside rules *)
    7.49  
    7.50 -fun aside_tac n = DETERM(REPEAT (filt_resolve_tac Modal_Rule.aside_rls 999 n));
    7.51 -fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
    7.52 +val aside_net = Tactic.build_net Modal_Rule.aside_rls;
    7.53 +fun aside_tac ctxt n = DETERM (REPEAT (filt_resolve_from_net_tac ctxt 999 aside_net n));
    7.54 +fun rule_tac ctxt rls n = fresolve_tac rls n THEN aside_tac ctxt n;
    7.55  
    7.56  val fres_safe_tac = fresolve_tac Modal_Rule.safe_rls;
    7.57 -val fres_unsafe_tac = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac;
    7.58 +fun fres_unsafe_tac ctxt = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac ctxt;
    7.59  val fres_bound_tac = fresolve_tac Modal_Rule.bound_rls;
    7.60  
    7.61  fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
    7.62 @@ -71,18 +72,19 @@
    7.63                      in fn st => tac (nprems_of st) st end;
    7.64  
    7.65  (* Depth first search bounded by d *)
    7.66 -fun solven_tac d n state = state |>
    7.67 -       (if d<0 then no_tac
    7.68 -        else if (nprems_of state = 0) then all_tac 
    7.69 -        else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
    7.70 -                 ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
    7.71 -                   (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
    7.72 +fun solven_tac ctxt d n st = st |>
    7.73 + (if d < 0 then no_tac
    7.74 +  else if nprems_of st = 0 then all_tac
    7.75 +  else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE
    7.76 +           ((fres_unsafe_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt d)) APPEND
    7.77 +             (fres_bound_tac n  THEN UPTOGOAL n (solven_tac ctxt (d - 1)))));
    7.78  
    7.79 -fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
    7.80 +fun solve_tac ctxt d =
    7.81 +  rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1;
    7.82  
    7.83 -fun step_tac n = 
    7.84 -    COND (has_fewer_prems 1) all_tac 
    7.85 -         (DETERM(fres_safe_tac n) ORELSE 
    7.86 -          (fres_unsafe_tac n APPEND fres_bound_tac n));
    7.87 +fun step_tac ctxt n =
    7.88 +  COND (has_fewer_prems 1) all_tac
    7.89 +       (DETERM(fres_safe_tac n) ORELSE
    7.90 +        (fres_unsafe_tac ctxt n APPEND fres_bound_tac n));
    7.91  
    7.92  end;
     8.1 --- a/src/Tools/intuitionistic.ML	Sat Dec 20 19:12:41 2014 +0100
     8.2 +++ b/src/Tools/intuitionistic.ML	Sat Dec 20 22:23:37 2014 +0100
     8.3 @@ -25,18 +25,18 @@
     8.4  
     8.5  fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
     8.6  
     8.7 -val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
     8.8 +fun bires_tac ctxt = Tactic.biresolution_from_nets_tac ctxt Context_Rules.orderlist;
     8.9  
    8.10  fun safe_step_tac ctxt =
    8.11    Context_Rules.Swrap ctxt
    8.12     (eq_assume_tac ORELSE'
    8.13 -    bires_tac true (Context_Rules.netpair_bang ctxt));
    8.14 +    bires_tac ctxt true (Context_Rules.netpair_bang ctxt));
    8.15  
    8.16  fun unsafe_step_tac ctxt =
    8.17    Context_Rules.wrap ctxt
    8.18     (assume_tac ctxt APPEND'
    8.19 -    bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
    8.20 -    bires_tac false (Context_Rules.netpair ctxt));
    8.21 +    bires_tac ctxt false (Context_Rules.netpair_bang ctxt) APPEND'
    8.22 +    bires_tac ctxt false (Context_Rules.netpair ctxt));
    8.23  
    8.24  fun step_tac ctxt i =
    8.25    REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
     9.1 --- a/src/ZF/Tools/typechk.ML	Sat Dec 20 19:12:41 2014 +0100
     9.2 +++ b/src/ZF/Tools/typechk.ML	Sat Dec 20 22:23:37 2014 +0100
     9.3 @@ -93,15 +93,15 @@
     9.4  
     9.5  fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt);
     9.6  
     9.7 -(*Compiles a term-net for speed*)
     9.8 -val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
     9.9 -                                     @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}];
    9.10 +(*Compile a term-net for speed*)
    9.11 +val basic_net =
    9.12 +  Tactic.build_net @{thms TrueI refl reflexive iff_refl ballI allI conjI impI};
    9.13  
    9.14  (*Instantiates variables in typing conditions.
    9.15    drawback: does not simplify conjunctions*)
    9.16  fun type_solver_tac ctxt hyps = SELECT_GOAL
    9.17      (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
    9.18 -                  ORELSE basic_res_tac 1
    9.19 +                  ORELSE resolve_from_net_tac ctxt basic_net 1
    9.20                    ORELSE (ares_tac hyps 1
    9.21                            APPEND typecheck_step_tac ctxt)));
    9.22