Generalized and exported biresolution_from_nets_tac to allow the declaration
authorpaulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706e57b5902822f
parent 3705 76f3b2803982
child 3707 40856b593501
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Sep 25 12:08:08 1997 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Sep 25 12:09:41 1997 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4    val bimatch_from_nets_tac: 
     1.5        (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
     1.6    val bimatch_tac	: (bool*thm)list -> int -> tactic
     1.7 +  val biresolution_from_nets_tac: 
     1.8 +	('a list -> (bool * thm) list) ->
     1.9 +	bool -> 'a Net.net * 'a Net.net -> int -> tactic
    1.10    val biresolve_from_nets_tac: 
    1.11        (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    1.12    val biresolve_tac	: (bool*thm)list -> int -> tactic
    1.13 @@ -402,19 +405,21 @@
    1.14  end;
    1.15  
    1.16  
    1.17 -(*biresolution using a pair of nets rather than rules*)
    1.18 -fun biresolution_from_nets_tac match (inet,enet) =
    1.19 +(*biresolution using a pair of nets rather than rules.  
    1.20 +    function "order" must sort and possibly filter the list of brls.
    1.21 +    boolean "match" indicates matching or unification.*)
    1.22 +fun biresolution_from_nets_tac order match (inet,enet) =
    1.23    SUBGOAL
    1.24      (fn (prem,i) =>
    1.25        let val hyps = Logic.strip_assums_hyp prem
    1.26            and concl = Logic.strip_assums_concl prem 
    1.27            val kbrls = Net.unify_term inet concl @
    1.28                        List.concat (map (Net.unify_term enet) hyps)
    1.29 -      in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
    1.30 +      in PRIMSEQ (biresolution match (order kbrls) i) end);
    1.31  
    1.32 -(*versions taking pre-built nets*)
    1.33 -val biresolve_from_nets_tac = biresolution_from_nets_tac false;
    1.34 -val bimatch_from_nets_tac = biresolution_from_nets_tac true;
    1.35 +(*versions taking pre-built nets.  No filtering of brls*)
    1.36 +val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
    1.37 +val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
    1.38  
    1.39  (*fast versions using nets internally*)
    1.40  val net_biresolve_tac =