src/Pure/Isar/context_rules.ML
changeset 12350 5fad0e7129c3
child 12380 3402d300f5ef
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Mon Dec 03 21:31:55 2001 +0100
     1.3 @@ -0,0 +1,260 @@
     1.4 +(*  Title:      Pure/Isar/context_rules.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Declarations of intro/elim/dest rules in Pure; see
    1.10 +Provers/classical.ML for a more specialized version of the same idea.
    1.11 +*)
    1.12 +
    1.13 +signature CONTEXT_RULES =
    1.14 +sig
    1.15 +  type netpair
    1.16 +  type T
    1.17 +  val netpair_bang: Proof.context -> netpair
    1.18 +  val netpair: Proof.context -> netpair
    1.19 +  val netpairs: Proof.context -> netpair list
    1.20 +  val orderlist: ((int * int) * 'a) list -> 'a list
    1.21 +  val orderlist_no_weight: ((int * int) * 'a) list -> 'a list
    1.22 +  val print_global_rules: theory -> unit
    1.23 +  val print_local_rules: Proof.context -> unit
    1.24 +  val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.25 +  val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.26 +  val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
    1.27 +  val wrap: Proof.context -> (int -> tactic) -> int -> tactic
    1.28 +  val intro_bang_global: int option -> theory attribute
    1.29 +  val elim_bang_global: int option -> theory attribute
    1.30 +  val dest_bang_global: int option -> theory attribute
    1.31 +  val intro_global: int option -> theory attribute
    1.32 +  val elim_global: int option -> theory attribute
    1.33 +  val dest_global: int option -> theory attribute
    1.34 +  val intro_query_global: int option -> theory attribute
    1.35 +  val elim_query_global: int option -> theory attribute
    1.36 +  val dest_query_global: int option -> theory attribute
    1.37 +  val rule_del_global: theory attribute
    1.38 +  val intro_bang_local: int option -> Proof.context attribute
    1.39 +  val elim_bang_local: int option -> Proof.context attribute
    1.40 +  val dest_bang_local: int option -> Proof.context attribute
    1.41 +  val intro_local: int option -> Proof.context attribute
    1.42 +  val elim_local: int option -> Proof.context attribute
    1.43 +  val dest_local: int option -> Proof.context attribute
    1.44 +  val intro_query_local: int option -> Proof.context attribute
    1.45 +  val elim_query_local: int option -> Proof.context attribute
    1.46 +  val dest_query_local: int option -> Proof.context attribute
    1.47 +  val rule_del_local: Proof.context attribute
    1.48 +  val setup: (theory -> theory) list
    1.49 +end;
    1.50 +
    1.51 +structure ContextRules: CONTEXT_RULES =
    1.52 +struct
    1.53 +
    1.54 +
    1.55 +(** rule declaration contexts **)
    1.56 +
    1.57 +(* rule kinds *)
    1.58 +
    1.59 +val intro_bangK = (0, false);
    1.60 +val elim_bangK = (0, true);
    1.61 +val introK = (1, false);
    1.62 +val elimK = (1, true);
    1.63 +val intro_queryK = (2, false);
    1.64 +val elim_queryK = (2, true);
    1.65 +
    1.66 +val kind_names =
    1.67 + [(intro_bangK, "safe introduction rules (intro!)"),
    1.68 +  (elim_bangK, "safe elimination rules (elim!)"),
    1.69 +  (introK, "introduction rules (intro)"),
    1.70 +  (elimK, "elimination rules (elim)"),
    1.71 +  (intro_queryK, "extra introduction rules (intro?)"),
    1.72 +  (elim_queryK, "extra elimination rules (elim?)")];
    1.73 +
    1.74 +val rule_kinds = map #1 kind_names;
    1.75 +val rule_indexes = distinct (map #1 rule_kinds);
    1.76 +
    1.77 +
    1.78 +(* raw data *)
    1.79 +
    1.80 +type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
    1.81 +val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
    1.82 +
    1.83 +datatype T = Rules of
    1.84 + {next: int,
    1.85 +  rules: (int * ((int * bool) * thm)) list,
    1.86 +  netpairs: netpair list,
    1.87 +  wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
    1.88 +    (((int -> tactic) -> int -> tactic) * stamp) list};
    1.89 +
    1.90 +fun make_rules next rules netpairs wrappers =
    1.91 +  Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
    1.92 +
    1.93 +fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
    1.94 +  let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
    1.95 +    make_rules (next - 1) ((w, ((i, b), th)) :: rules)
    1.96 +      (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
    1.97 +  end;
    1.98 +
    1.99 +fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
   1.100 +  let
   1.101 +    fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
   1.102 +    fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
   1.103 +  in
   1.104 +    if not (exists eq_th rules) then rs
   1.105 +    else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
   1.106 +  end;
   1.107 +
   1.108 +fun print_rules prt x (Rules {rules, ...}) =
   1.109 +  let
   1.110 +    fun prt_kind (i, b) =
   1.111 +      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
   1.112 +        (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
   1.113 +          (sort (int_ord o pairself fst) rules));
   1.114 +  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   1.115 +
   1.116 +
   1.117 +(* theory and proof data *)
   1.118 +
   1.119 +structure GlobalRulesArgs =
   1.120 +struct
   1.121 +  val name = "Isar/rule_context";
   1.122 +  type T = T;
   1.123 +
   1.124 +  val empty = make_rules ~1 [] empty_netpairs ([], []);
   1.125 +  val copy = I;
   1.126 +  val prep_ext = I;
   1.127 +
   1.128 +  fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
   1.129 +      Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
   1.130 +    let
   1.131 +      val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
   1.132 +      val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
   1.133 +          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
   1.134 +      val next = ~ (length rules);
   1.135 +      val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
   1.136 +          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
   1.137 +        (empty_netpairs, next upto ~1 ~~ rules);
   1.138 +    in make_rules (next - 1) rules netpairs wrappers end;
   1.139 +
   1.140 +  val print = print_rules Display.pretty_thm_sg;
   1.141 +end;
   1.142 +
   1.143 +structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
   1.144 +val print_global_rules = GlobalRules.print;
   1.145 +
   1.146 +structure LocalRulesArgs =
   1.147 +struct
   1.148 +  val name = GlobalRulesArgs.name;
   1.149 +  type T = GlobalRulesArgs.T;
   1.150 +  val init = GlobalRules.get;
   1.151 +  val print = print_rules ProofContext.pretty_thm;
   1.152 +end;
   1.153 +
   1.154 +structure LocalRules = ProofDataFun(LocalRulesArgs);
   1.155 +val print_local_rules = LocalRules.print;
   1.156 +
   1.157 +
   1.158 +(* access data *)
   1.159 +
   1.160 +fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
   1.161 +val netpair_bang = hd o netpairs;
   1.162 +val netpair = hd o tl o netpairs;
   1.163 +
   1.164 +
   1.165 +fun untaglist [] = []
   1.166 +  | untaglist [(k : int * int, x)] = [x]
   1.167 +  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
   1.168 +      if k = k' then untaglist rest
   1.169 +      else x :: untaglist rest;
   1.170 +
   1.171 +fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
   1.172 +fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
   1.173 +
   1.174 +
   1.175 +fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
   1.176 +  make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
   1.177 +
   1.178 +val addSWrapper = gen_add_wrapper Library.apfst;
   1.179 +val addWrapper = gen_add_wrapper Library.apsnd;
   1.180 +
   1.181 +
   1.182 +fun gen_wrap which ctxt =
   1.183 +  let val Rules {wrappers, ...} = LocalRules.get ctxt
   1.184 +  in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
   1.185 +
   1.186 +val Swrap = gen_wrap #1;
   1.187 +val wrap = gen_wrap #2;
   1.188 +
   1.189 +
   1.190 +
   1.191 +(** attributes **)
   1.192 +
   1.193 +(* add and del rules *)
   1.194 +
   1.195 +local
   1.196 +
   1.197 +fun del map_data (x, th) =
   1.198 +  (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
   1.199 +
   1.200 +fun add k view map_data opt_w =
   1.201 +  (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data;
   1.202 +
   1.203 +in
   1.204 +
   1.205 +val intro_bang_global  = add intro_bangK I GlobalRules.map;
   1.206 +val elim_bang_global   = add elim_bangK I GlobalRules.map;
   1.207 +val dest_bang_global   = add elim_bangK Tactic.make_elim GlobalRules.map;
   1.208 +val intro_global       = add introK I GlobalRules.map;
   1.209 +val elim_global        = add elimK I GlobalRules.map;
   1.210 +val dest_global        = add elimK Tactic.make_elim GlobalRules.map;
   1.211 +val intro_query_global = add intro_queryK I GlobalRules.map;
   1.212 +val elim_query_global  = add elim_queryK I GlobalRules.map;
   1.213 +val dest_query_global  = add elim_queryK Tactic.make_elim GlobalRules.map;
   1.214 +val rule_del_global    = del GlobalRules.map;
   1.215 +
   1.216 +val intro_bang_local   = add intro_bangK I LocalRules.map;
   1.217 +val elim_bang_local    = add elim_bangK I LocalRules.map;
   1.218 +val dest_bang_local    = add elim_bangK Tactic.make_elim LocalRules.map;
   1.219 +val intro_local        = add introK I LocalRules.map;
   1.220 +val elim_local         = add elimK I LocalRules.map;
   1.221 +val dest_local         = add elimK Tactic.make_elim LocalRules.map;
   1.222 +val intro_query_local  = add intro_queryK I LocalRules.map;
   1.223 +val elim_query_local   = add elim_queryK I LocalRules.map;
   1.224 +val dest_query_local   = add elim_queryK Tactic.make_elim LocalRules.map;
   1.225 +val rule_del_local     = del LocalRules.map;
   1.226 +
   1.227 +end;
   1.228 +
   1.229 +
   1.230 +(* concrete syntax *)
   1.231 +
   1.232 +fun add_args a b c x = Attrib.syntax
   1.233 +  (Scan.lift (Scan.option Args.nat --
   1.234 +    (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
   1.235 +
   1.236 +fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
   1.237 +
   1.238 +
   1.239 +val rule_atts =
   1.240 + [("intro",
   1.241 +   (add_args intro_bang_global intro_global intro_query_global,
   1.242 +    add_args intro_bang_local intro_local intro_query_local),
   1.243 +    "declaration of introduction rule"),
   1.244 +  ("elim",
   1.245 +   (add_args elim_bang_global elim_global elim_query_global,
   1.246 +    add_args elim_bang_local elim_local elim_query_local),
   1.247 +    "declaration of elimination rule"),
   1.248 +  ("dest",
   1.249 +   (add_args dest_bang_global dest_global dest_query_global,
   1.250 +    add_args dest_bang_local dest_local dest_query_local),
   1.251 +    "declaration of destruction rule"),
   1.252 +  ("rule", (del_args rule_del_global, del_args rule_del_local),
   1.253 +    "remove declaration of intro/elim/dest rule")];
   1.254 +
   1.255 +
   1.256 +
   1.257 +(** theory setup **)
   1.258 +
   1.259 +val setup =
   1.260 + [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
   1.261 +
   1.262 +
   1.263 +end;