export low-level addXXs;
authorwenzelm
Wed Dec 05 03:15:15 2001 +0100 (2001-12-05 ago)
changeset 123803402d300f5ef
parent 12379 c74d160ff0c5
child 12381 5177845a34f5
export low-level addXXs;
find_rules interface;
src/Pure/Isar/context_rules.ML
     1.1 --- a/src/Pure/Isar/context_rules.ML	Wed Dec 05 03:14:22 2001 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Dec 05 03:15:15 2001 +0100
     1.3 @@ -13,9 +13,8 @@
     1.4    type T
     1.5    val netpair_bang: Proof.context -> netpair
     1.6    val netpair: Proof.context -> netpair
     1.7 -  val netpairs: Proof.context -> netpair list
     1.8    val orderlist: ((int * int) * 'a) list -> 'a list
     1.9 -  val orderlist_no_weight: ((int * int) * 'a) list -> 'a list
    1.10 +  val find_rules: Proof.context -> thm list -> term -> thm list list
    1.11    val print_global_rules: theory -> unit
    1.12    val print_local_rules: Proof.context -> unit
    1.13    val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.14 @@ -42,6 +41,14 @@
    1.15    val elim_query_local: int option -> Proof.context attribute
    1.16    val dest_query_local: int option -> Proof.context attribute
    1.17    val rule_del_local: Proof.context attribute
    1.18 +  val addXIs_global: theory * thm list -> theory
    1.19 +  val addXEs_global: theory * thm list -> theory
    1.20 +  val addXDs_global: theory * thm list -> theory
    1.21 +  val delrules_global: theory * thm list -> theory
    1.22 +  val addXIs_local: Proof.context * thm list -> Proof.context
    1.23 +  val addXEs_local: Proof.context * thm list -> Proof.context
    1.24 +  val addXDs_local: Proof.context * thm list -> Proof.context
    1.25 +  val delrules_local: Proof.context * thm list -> Proof.context
    1.26    val setup: (theory -> theory) list
    1.27  end;
    1.28  
    1.29 @@ -167,6 +174,14 @@
    1.30  
    1.31  fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    1.32  fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
    1.33 +fun may_unify t net = map snd (orderlist_no_weight (Net.unify_term net t));
    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 +
    1.39 +fun find_rules ctxt facts goal =
    1.40 +  map (fn (inet, enet) => find_erules facts enet @ find_irules goal inet) (netpairs ctxt);
    1.41  
    1.42  
    1.43  fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    1.44 @@ -224,11 +239,27 @@
    1.45  end;
    1.46  
    1.47  
    1.48 +(* low-level modifiers *)
    1.49 +
    1.50 +fun modifier att (x, ths) =
    1.51 +  #1 (Thm.applys_attributes ((x, rev ths), [att]));
    1.52 +
    1.53 +val addXIs_global = modifier (intro_query_global None);
    1.54 +val addXEs_global = modifier (elim_query_global None);
    1.55 +val addXDs_global = modifier (dest_query_global None);
    1.56 +val delrules_global = modifier rule_del_global;
    1.57 +
    1.58 +val addXIs_local = modifier (intro_query_local None);
    1.59 +val addXEs_local = modifier (elim_query_local None);
    1.60 +val addXDs_local = modifier (dest_query_local None);
    1.61 +val delrules_local = modifier rule_del_local;
    1.62 +
    1.63 +
    1.64  (* concrete syntax *)
    1.65  
    1.66  fun add_args a b c x = Attrib.syntax
    1.67 -  (Scan.lift (Scan.option Args.nat --
    1.68 -    (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
    1.69 +  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
    1.70 +    >> (fn (f, n) => f n)) x;
    1.71  
    1.72  fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
    1.73