src/Pure/Isar/net_rules.ML
author wenzelm
Thu, 04 Oct 2001 23:27:42 +0200
changeset 11693 63b0b2ec5830
parent 8807 0046be1769f9
child 11776 d4f9de0bde28
permissions -rw-r--r--
Thm.major_prem_of part of Logic.strip_assums_concl;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/net_rules.ML
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
8807
wenzelm
parents: 8635
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     5
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     6
Efficient storage of rules: preserves order, prefers later entries.
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     7
*)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     8
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     9
signature NET_RULES =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    10
sig
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    11
  type 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    12
  val rules: 'a T -> 'a list
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    13
  val may_unify: 'a T -> term -> 'a list
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    14
  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    15
  val merge: 'a T * 'a T -> 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    16
  val delete: 'a -> 'a T -> 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    17
  val insert: 'a -> 'a T -> 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    18
  val deletes: 'a list -> 'a T -> 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    19
  val inserts: 'a list -> 'a T -> 'a T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    20
  val init_intro: thm T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    21
  val init_elim: thm T
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    22
end;
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    23
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    24
structure NetRules: NET_RULES =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    25
struct
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    26
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    27
(* datatype rules *)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    28
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    29
datatype 'a T =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    30
  Rules of {
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    31
    eq: 'a * 'a -> bool,
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    32
    index: 'a -> term,
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    33
    rules: 'a list,
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    34
    next: int,
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    35
    net: (int * 'a) Net.net};
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    36
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    37
fun mk_rules eq index rules next net =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    38
  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    39
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    40
fun rules (Rules {rules = rs, ...}) = rs;
8635
2f699cd7b8d7 fixed indexing of elim rules;
wenzelm
parents: 8298
diff changeset
    41
fun may_unify (Rules {rules, net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    42
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    43
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    44
(* build rules *)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    45
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    46
fun init eq index = mk_rules eq index [] ~1 Net.empty;
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    47
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    48
fun add rule (Rules {eq, index, rules, next, net}) =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    49
  mk_rules eq index (rule :: rules) (next - 1)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    50
    (Net.insert_term ((index rule, (next, rule)), net, K false));
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    51
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    52
fun make eq index rules = foldr (uncurry add) (rules, init eq index);
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    53
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    54
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    55
fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    56
  make eq index (Library.generic_merge eq I I rules1 rules2);
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    57
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    58
fun delete rule (rs as Rules {eq, index, rules, next, net}) =
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    59
  if not (Library.gen_mem eq (rule, rules)) then rs
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    60
  else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    61
    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    62
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    63
fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    64
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    65
fun deletes rules rs = foldr (uncurry delete) (rules, rs);
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    66
fun inserts rules rs = foldr (uncurry insert) (rules, rs);
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    67
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    68
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    69
(* intro/elim rules *)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    70
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    71
val init_intro = init Thm.eq_thm Thm.concl_of;
11693
63b0b2ec5830 Thm.major_prem_of part of Logic.strip_assums_concl;
wenzelm
parents: 8807
diff changeset
    72
val init_elim = init Thm.eq_thm Thm.major_prem_of;
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    73
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    74
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    75
end;