Quelle bires.ML Sprache: SML

(*  Title:      Pure/bires.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Makarius

Biresolution and resolution using nets.
*)

signature BIRES =
sig
  type rule = bool * thm
  val subgoals_of: rule -> int
  val subgoals_ord: rule ord
  val no_subgoals: rule -> bool

  type tag = {weight: int, index: int}
  val tag_weight_ord: tag ord
  val tag_index_ord: tag ord
  val tag_ord: tag ord
  val weighted_tag_ord: bool -> tag ord
  val tag_order: (tag * 'a) list -> 'a list
  val weight_tag: int -> tag

  eqtype kind
  val intro_bang_kind: kind
  val elim_bang_kind: kind
  val dest_bang_kind: kind
  val intro_kind: kind
  val elim_kind: kind
  val dest_kind: kind
  val intro_query_kind: kind
  val elim_query_kind: kind
  val dest_query_kind: kind
  val kind_safe: kind -> bool
  val kind_unsafe: kind -> bool
  val kind_extra: kind -> bool
  val kind_index: kind -> int
  val kind_is_elim: kind -> bool
  val kind_make_elim: kind -> thm -> thm
  val kind_domain: kind list
  val kind_values: 'a -> 'a list
  val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list
  val kind_rule: kind -> thm -> rule
  val kind_description: kind -> string
  val kind_title: kind -> string
  val kind_name: kind -> string

  type 'a decl = {kind: kind, tag: tag, info: 'a}
  val decl_ord: 'a decl ord
  type 'a decls
  val has_decls: 'a decls -> thm -> bool
  val get_decls: 'a decls -> thm -> 'a decl list
  val dest_decls: 'a decls -> (thm * 'a decl -> bool) -> (thm * 'a decl) list
  val pretty_decls: Proof.context -> 'a decls -> Pretty.T list
  val merge_decls: 'a decls * 'a decls -> 'a decl list * 'a decls
  val extend_decls: thm * 'a decl -> 'a decls -> 'a decl option * 'a decls
  val remove_decls: thm -> 'a decls -> 'a decl list * 'a decls
  val empty_decls: 'a decls

  type netpair = (tag * rule) Net.net * (tag * rule) Net.net
  val empty_netpair: netpair
  val pretty_netpair: Proof.context -> string -> netpair -> Pretty.T list
  val insert_tagged_rule: tag * rule -> netpair -> netpair
  val delete_tagged_rule: int * thm -> netpair -> netpair

  val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option ->
    bool -> netpair -> int -> tactic
  val biresolve_from_nets_tac: Proof.context -> netpair -> int -> tactic
  val bimatch_from_nets_tac: Proof.context -> netpair -> int -> tactic

  type net = (int * thm) Net.net
  val build_net: thm list -> net
  val filt_resolve_from_net_tac: Proof.context -> int -> net -> int -> tactic
  val resolve_from_net_tac: Proof.context -> net -> int -> tactic
  val match_from_net_tac: Proof.context -> net -> int -> tactic
end

structure Bires: BIRES =
struct

(** Rule kinds and declarations **)

(* type rule *)

type rule = bool * thm;  (*see Thm.biresolution*)

fun subgoals_of (true, thm) = Thm.nprems_of thm - 1
  | subgoals_of (false, thm) = Thm.nprems_of thm;

val subgoals_ord = int_ord o apply2 subgoals_of;

fun no_subgoals (true, thm) = Thm.one_prem thm
  | no_subgoals (false, thm) = Thm.no_prems thm;

(* tagged rules *)

type tag = {weight: int, index: int};

val tag_weight_ord: tag ord = int_ord o apply2 #weight;
val tag_index_ord: tag ord = int_ord o apply2 #index;

val tag_ord: tag ord = tag_weight_ord ||| tag_index_ord;

fun weighted_tag_ord weighted = if weighted then tag_ord else tag_index_ord;

fun tag_order list = make_order_list tag_ord NONE list;

fun weight_tag weight : tag = {weight = weight, index = 0};

fun next_tag next ({weight, ...}: tag) = {weight = weight, index = next};

(* kind: intro/elim/dest *)

datatype kind = Kind of {index: int, is_elim: bool, make_elim: bool};

fun make_intro_kind i = Kind {index = i, is_elim = false, make_elim = false};
fun make_elim_kind i = Kind {index = i, is_elim = true, make_elim = false};
fun make_dest_kind i = Kind {index = i, is_elim = true, make_elim = true};

val intro_bang_kind = make_intro_kind 0;
val elim_bang_kind = make_elim_kind 0;
val dest_bang_kind = make_dest_kind 0;

val intro_kind = make_intro_kind 1;
val elim_kind = make_elim_kind 1;
val dest_kind = make_dest_kind 1;

val intro_query_kind = make_intro_kind 2;
val elim_query_kind = make_elim_kind 2;
val dest_query_kind = make_dest_kind 2;

val kind_infos =
[(intro_bang_kind, ("safe introduction", "(intro!)")),
  (elim_bang_kind, ("safe elimination", "(elim!)")),
  (dest_bang_kind, ("safe destruction", "(dest!)")),
  (intro_kind, ("unsafe introduction", "(intro)")),
  (elim_kind, ("unsafe elimination", "(elim)")),
  (dest_kind, ("unsafe destruction", "(dest)")),
  (intro_query_kind, ("extra introduction", "(intro?)")),
  (elim_query_kind, ("extra elimination", "(elim?)")),
  (dest_query_kind, ("extra destruction", "(dest?)"))];

fun kind_safe (Kind {index, ...}) = index = 0;
fun kind_unsafe (Kind {index, ...}) = index = 1;
fun kind_extra (Kind {index, ...}) = index = 2;
fun kind_index (Kind {index, ...}) = index;
fun kind_is_elim (Kind {is_elim, ...}) = is_elim;
fun kind_make_elim (Kind {make_elim, ...}) = make_elim ? Tactic.make_elim;

val kind_index_ord = int_ord o apply2 kind_index;
val kind_elim_ord = bool_ord o apply2 kind_is_elim;

val kind_domain = map #1 kind_infos;

fun kind_values x =
  replicate (length (distinct (op =) (map kind_index kind_domain))) x;

fun kind_map kind f = nth_map (kind_index kind) f;
fun kind_rule kind thm : rule = (kind_is_elim kind, thm);

val the_kind_info = the o AList.lookup (op =) kind_infos;

fun kind_description kind =
  let val (a, b) = the_kind_info kind
  in a ^ " " ^ b end;

fun kind_title kind =
  let val (a, b) = the_kind_info kind
  in a ^ " rules " ^ b end;

fun kind_name (Kind {is_elim, make_elim, ...}) =
  if is_elim andalso make_elim then "destruction rule"
  else if is_elim then "elimination rule"
  else "introduction rule";

(* rule declarations in canonical order *)

type 'a decl = {kind: kind, tag: tag, info: 'a};

fun decl_ord (args: 'a decl * 'a decl) =
  (case kind_index_ord (apply2 #kind args) of
    EQUAL => tag_index_ord (apply2 #tag args)
  | ord => ord);

fun decl_merge_ord (args: 'a decl * 'a decl) =
  (case kind_elim_ord (apply2 #kind args) of
    EQUAL => rev_order (tag_index_ord (apply2 #tag args))
  | ord => ord);

fun next_decl next ({kind, tag, info}: 'a decl) : 'a decl =
  {kind = kind, tag = next_tag next tag, info = info};

abstype 'a decls = Decls of {next: int, rules: 'a decl list Proptab.table}
with

local

fun dup_decls (Decls {rules, ...}) (thm, {kind, ...}: 'a decl) =
  exists (fn {kind = kind', ...} => kind = kind') (Proptab.lookup_list rules thm);

fun add_decls (thm, decl) (Decls {next, rules}) =
  let
    val decl' = next_decl next decl;
    val decls' = Decls {next = next - 1, rules = Proptab.cons_list (thm, decl') rules};
  in (decl', decls') end;

in

fun has_decls (Decls {rules, ...}) = Proptab.defined rules;

fun get_decls (Decls {rules, ...}) = Proptab.lookup_list rules;

fun dest_decls_ord ord (Decls {rules, ...}) pred =
  build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d))))
  |> sort (ord o apply2 #2);

fun dest_decls decls = dest_decls_ord decl_ord decls;

fun pretty_decls ctxt decls =
  kind_domain |> map_filter (fn kind =>
    (case dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind') of
      [] => NONE
    | ds =>
        SOME (Pretty.big_list (kind_title kind ^ ":")
          (map (Thm.pretty_thm_item ctxt o #1) ds))));

fun merge_decls (decls1, decls2) =
  decls1 |> fold_map add_decls (dest_decls_ord decl_merge_ord decls2 (not o dup_decls decls1));

fun extend_decls (thm, decl) decls =
  if dup_decls decls (thm, decl) then (NONE, decls)
  else add_decls (thm, decl) decls |>> SOME;

fun remove_decls thm (decls as Decls {next, rules}) =
  (case get_decls decls thm of
    [] => ([], decls)
  | old_decls => (old_decls, Decls {next = next, rules = Proptab.delete thm rules}));

val empty_decls = Decls {next = ~1, rules = Proptab.empty};

end;

end;

(* discrimination nets for intr/elim rules *)

type netpair = (tag * rule) Net.net * (tag * rule) Net.net;

val empty_netpair: netpair = (Net.empty, Net.empty);

fun pretty_netpair ctxt title (inet, enet) =
  let
    fun pretty_entry ({weight, ...}: tag, (_, thm): rule) =
      Pretty.item [Pretty.str (string_of_int weight), Pretty.brk 1, Thm.pretty_thm ctxt thm];

    fun pretty_net elim net =
      (case Net.content net |> sort_distinct (tag_ord o apply2 #1) |> map pretty_entry of
        [] => NONE
      | prts => SOME (Pretty.big_list (title ^ " " ^ (if elim then "elim" else "intro")) prts));
  in map_filter I [pretty_net false inet, pretty_net true enet] end;

(** Natural Deduction using (bires_flg, rule) pairs **)

(** To preserve the order of the rules, tag them with decreasing integers **)

fun insert_tagged_rule (tagged_rule as (_, (eres, th))) ((inet, enet): netpair) =
  if eres then
    (case try Thm.major_prem_of th of
      SOME prem => (inet, Net.insert_term (K false) (prem, tagged_rule) enet)
    | NONE => error "insert_tagged_rule: elimination rule with no premises")
  else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet);

fun delete_tagged_rule (index, th) ((inet, enet): netpair) =
  let
    fun eq ((), ({index = index', ...}, _)) = index = index';
    val inet' = Net.delete_term_safe eq (Thm.concl_of th, ()) inet;
    val enet' =
      (case try Thm.major_prem_of th of
        SOME prem => Net.delete_term_safe eq (prem, ()) enet
      | NONE => enet);
  in (inet', enet') end;

(*biresolution using a pair of nets rather than rules:
   boolean "match" indicates matching or unification.*)
fun biresolution_from_nets_tac ctxt ord pred match ((inet, enet): netpair) =
  SUBGOAL
    (fn (prem, i) =>
      let
        val hyps = Logic.strip_assums_hyp prem;
        val concl = Logic.strip_assums_concl prem;
        val tagged_rules = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
        val order = make_order_list ord pred;
      in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order tagged_rules) i) end);

(*versions taking pre-built nets.  No filtering of brls*)
fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE false;
fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE true;

(** Simpler version for resolve_tac -- only one net, and no hyps **)

type net = (int * thm) Net.net;

(*build a net of rules for resolution*)
fun build_net rls : net =
  fold_rev (fn (k, th) => Net.insert_term (K false) (Thm.concl_of th, (k, th)))
    (tag_list 1 rls) Net.empty;

(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
fun filt_resolution_from_net_tac ctxt match pred net =
  SUBGOAL (fn (prem, i) =>
    let val krls = Net.unify_term net (Logic.strip_assums_concl prem) in
      if pred krls then
        PRIMSEQ (Thm.biresolution (SOME ctxt) match (map (pair false) (order_list krls)) i)
      else no_tac
    end);

(*Resolve the subgoal using the rules (making a net) unless too flexible,
   which means more than maxr rules are unifiable.      *)
fun filt_resolve_from_net_tac ctxt maxr net =
  let fun pred krls = length krls <= maxr
  in filt_resolution_from_net_tac ctxt false pred net end;

(*versions taking pre-built nets*)
fun resolve_from_net_tac ctxt = filt_resolution_from_net_tac ctxt false (K true);
fun match_from_net_tac ctxt = filt_resolution_from_net_tac ctxt true (K true);

end;

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.