src/Pure/Isar/context_rules.ML
changeset 12399 2ba27248af7f
parent 12380 3402d300f5ef
child 12412 d0857ea70f23
     1.1 --- a/src/Pure/Isar/context_rules.ML	Thu Dec 06 00:40:04 2001 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Dec 06 00:40:19 2001 +0100
     1.3 @@ -14,7 +14,8 @@
     1.4    val netpair_bang: Proof.context -> netpair
     1.5    val netpair: Proof.context -> netpair
     1.6    val orderlist: ((int * int) * 'a) list -> 'a list
     1.7 -  val find_rules: Proof.context -> thm list -> term -> thm list list
     1.8 +  val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
     1.9 +  val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
    1.10    val print_global_rules: theory -> unit
    1.11    val print_local_rules: Proof.context -> unit
    1.12    val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.13 @@ -166,6 +167,8 @@
    1.14  val netpair = hd o tl o netpairs;
    1.15  
    1.16  
    1.17 +(* retrieving rules *)
    1.18 +
    1.19  fun untaglist [] = []
    1.20    | untaglist [(k : int * int, x)] = [x]
    1.21    | untaglist ((k, x) :: (rest as (k', x') :: _)) =
    1.22 @@ -174,16 +177,22 @@
    1.23  
    1.24  fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    1.25  fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
    1.26 -fun may_unify t net = map snd (orderlist_no_weight (Net.unify_term net t));
    1.27 +
    1.28 +fun may_unify weighted t net =
    1.29 +  map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
    1.30 +
    1.31 +fun find_erules _ [] = K []
    1.32 +  | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
    1.33 +fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
    1.34  
    1.35 -fun find_erules [] = K []
    1.36 -  | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
    1.37 -fun find_irules goal = may_unify (Logic.strip_assums_concl goal);
    1.38 +fun find_rules_netpair weighted facts goal (inet, enet) =
    1.39 +  find_erules weighted facts enet @ find_irules weighted goal inet;
    1.40  
    1.41 -fun find_rules ctxt facts goal =
    1.42 -  map (fn (inet, enet) => find_erules facts enet @ find_irules goal inet) (netpairs ctxt);
    1.43 +fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
    1.44  
    1.45  
    1.46 +(* wrappers *)
    1.47 +
    1.48  fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    1.49    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
    1.50