src/Pure/Thy/thm_database.ML
author clasohm
Wed, 04 Oct 1995 12:59:52 +0100
changeset 1262 8f40ff1299d8
parent 1245 934183dfc786
child 1272 dd877dc7c1f4
permissions -rw-r--r--
added removal of theorems if theory is to be reloaded; changed functions for local simpsets
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thm_database.ML
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
     3
    Author:     Carsten Clasohm and Tobias Nipkow
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     4
    Copyright   1995 TU Muenchen
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     5
*)
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     6
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
     7
datatype thm_db_type =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
     8
  ThmDB of {count: int,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
     9
            thy_idx: (Sign.sg * (string list * int list)) list,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    10
            const_idx: ((int * (string * thm)) list) Symtab.table};
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    11
    (*count: number of theorems in database (used as unique ID for next thm)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    12
      thy_idx: constants and IDs of theorems
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    13
               indexed by the theory's signature they belong to
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    14
      const_idx: named theorems tagged by numbers and
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    15
                 indexed by the constants they contain*)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    16
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    17
signature THMDB =
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    18
sig
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    19
  val thm_db: thm_db_type ref
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    20
  val store_thm_db: string * thm -> thm
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    21
  val delete_thm_db: theory -> unit
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    22
  val thms_containing: string list -> (string * thm) list
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    23
  val findI:         int -> (string * thm)list
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    24
  val findEs:        int -> (string * thm)list
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    25
  val findE:  int -> int -> (string * thm)list
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    26
end;
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    27
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    28
functor ThmDBFun(): THMDB =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    29
struct
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    30
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    31
(*** ignore and top_const could be turned into functor-parameters, but are
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    32
currently identical for all object logics ***)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    33
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    34
(* Constants not to be used for theorem indexing *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    35
val ignore = ["Trueprop", "all", "==>", "=="];
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    36
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    37
(* top_const: main constant, ignoring Trueprop *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    38
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    39
                                         | _          => None);
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    40
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    41
(*Symtab which associates a constant with a list of theorems that contain the
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    42
  constant (theorems are tagged with numbers)*)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    43
val thm_db = ref (ThmDB
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    44
 {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    45
  const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    46
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    47
(*list all relevant constants a term contains*)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    48
fun list_consts t =
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    49
  let fun consts (Const (c, _)) = if c mem ignore then [] else [c]
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    50
        | consts (Free _) = []
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    51
        | consts (Var _) = []
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    52
        | consts (Bound _) = []
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    53
        | consts (Abs (_, _, t)) = consts t
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    54
        | consts (t1$t2) = (consts t1) union (consts t2);
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    55
  in distinct (consts t) end;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    56
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    57
(*store a theorem in database*)
1236
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1230
diff changeset
    58
fun store_thm_db (named_thm as (name, thm)) =
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    59
  let val {prop, hyps, sign, ...} = rep_thm thm;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    60
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    61
      val consts = distinct (flat (map list_consts (prop :: hyps)));
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    62
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    63
      val ThmDB {count, thy_idx, const_idx} = !thm_db;
1141
a94c0ab9a3ed commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents: 1137
diff changeset
    64
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    65
      fun update_thys [] = [(sign, (consts, [count]))]
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    66
        | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    67
            if Sign.eq_sg (sign, thy_sign) then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    68
              (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    69
            else thy :: update_thys ts;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    70
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    71
      val tagged_thm = (count, named_thm);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    72
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    73
      fun update_db _ [] result = Some result
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    74
        | update_db checked (c :: cs) result =
1236
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1230
diff changeset
    75
            let
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1230
diff changeset
    76
              val old_thms = Symtab.lookup_multi (result, c);
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1230
diff changeset
    77
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    78
              val duplicate =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    79
                if checked then false
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    80
                else case find_first (fn (_, (n, _)) => n = name) old_thms of
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    81
                       Some (_, (_, t)) => eq_thm (t, thm)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    82
                     | None => false
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    83
            in if duplicate then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    84
                 (writeln ("Warning: Theorem database already contains copy of\
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    85
                           \ theorem " ^ quote name);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    86
                  None)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    87
               else update_db true
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    88
                      cs (Symtab.update ((c, tagged_thm :: old_thms), result))
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    89
            end;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    90
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    91
      val const_idx' = update_db false consts const_idx;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    92
  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    93
                                  " cannot be stored in ThmDB\n\t because it \
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    94
                                  \contains no or only ignored constants.")
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    95
     else if is_some const_idx' then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    96
       thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    97
                        const_idx = the const_idx'}
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    98
     else ();
1236
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1230
diff changeset
    99
     thm
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   100
  end;
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   101
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   102
(*remove all theorems with given signature from database*)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   103
fun delete_thm_db thy =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   104
  let
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   105
    val sign = sign_of thy;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   106
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   107
    val ThmDB {count, thy_idx, const_idx} = !thm_db;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   108
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   109
    fun update_thys [] result = (result, [], [])
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   110
      | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   111
                    result =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   112
          if Sign.eq_sg (sign, thy_sign) then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   113
            (result @ ts, thy_consts, thy_nums)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   114
          else update_thys ts (thy :: result);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   115
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   116
    val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   117
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   118
    fun update_db [] result = result
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   119
      | update_db (c :: cs) result =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   120
        let val thms' = filter_out (fn (num, _) => num mem thy_nums)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   121
                                   (Symtab.lookup_multi (result, c));
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   122
        in update_db cs (Symtab.update ((c, thms'), result)) end;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   123
  in thm_db := ThmDB {count = count, thy_idx = thy_idx',
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   124
                      const_idx = update_db thy_consts const_idx}
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   125
  end;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   126
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   127
(*intersection of two theorem lists with descending tags*)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   128
infix desc_inter;
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   129
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   130
  | xs desc_inter [] = []
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   131
  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   132
      if xi = yi then x :: (xs desc_inter ys)
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   133
      else if xi > yi then xs desc_inter yss
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   134
      else xss desc_inter ys;
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   135
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   136
(*get all theorems from database that contain a list of constants*)
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   137
fun thms_containing constants =
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   138
  let fun collect [] _ result = map snd result
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   139
        | collect (c :: cs) first result =
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   140
            let val ThmDB {const_idx, ...} = !thm_db;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   141
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   142
                val new_thms = Symtab.lookup_multi (const_idx, c);
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   143
            in collect cs false (if first then new_thms
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   144
                                          else (result desc_inter new_thms))
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   145
            end;
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   146
1134
5e9775c196e8 changed error message in thms_containing
clasohm
parents: 1132
diff changeset
   147
      val look_for = constants \\ ignore;
5e9775c196e8 changed error message in thms_containing
clasohm
parents: 1132
diff changeset
   148
  in if null look_for then
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   149
       error ("No or only ignored constants were specified for theorem \
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   150
              \database search:\n  " ^ commas (map quote ignore))
1134
5e9775c196e8 changed error message in thms_containing
clasohm
parents: 1132
diff changeset
   151
     else ();
5e9775c196e8 changed error message in thms_containing
clasohm
parents: 1132
diff changeset
   152
     collect look_for true [] end;
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   153
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   154
val intro_const = top_const o concl_of;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   155
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   156
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   157
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   158
(* In case faster access is necessary, the thm db should provide special
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   159
functions
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   160
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   161
index_intros, index_elims: string -> (string * thm) list
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   162
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   163
where thm [| A1 ; ...; An |] ==> B is returned by
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   164
- index_intros c if B  is of the form c t1 ... tn
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   165
- index_elims c  if A1 is of the form c t1 ... tn
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   166
*)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   167
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   168
(* could be provided by thm db *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   169
fun index_intros c =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   170
  let fun topc(_,thm) = intro_const thm = Some(c);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   171
      val named_thms = thms_containing [c]
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   172
  in filter topc named_thms end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   173
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   174
(* could be provided by thm db *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   175
fun index_elims c =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   176
  let fun topc(_,thm) = elim_const thm = Some(c);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   177
      val named_thms = thms_containing [c]
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   178
  in filter topc named_thms end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   179
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   180
(*assume that parameters have unique names*)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   181
fun goal_params i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   182
  let val gi = getgoal i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   183
      val frees = map Free (Logic.strip_params gi)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   184
  in (gi,frees) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   185
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   186
fun concl_of_goal i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   187
  let val (gi,frees) = goal_params i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   188
      val B = Logic.strip_assums_concl gi
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   189
  in subst_bounds(frees,B) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   190
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   191
fun prems_of_goal i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   192
  let val (gi,frees) = goal_params i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   193
      val As = Logic.strip_assums_hyp gi
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   194
  in map (fn A => subst_bounds(frees,A)) As end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   195
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   196
fun select_match(obj, signobj, named_thms, extract) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   197
  let fun matches(prop, tsig) =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   198
            case extract prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   199
              None => false
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   200
            | Some pat => Pattern.matches tsig (pat, obj);
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   201
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   202
      fun select((p as (_,thm))::named_thms, sels) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   203
            let val {prop, sign, ...} = rep_thm thm
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   204
            in select(named_thms,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   205
                      if Sign.subsig(sign, signobj) andalso
1230
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   206
                         matches(prop,#tsig(Sign.rep_sg signobj))
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   207
                      then p::sels else sels)
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   208
            end
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   209
        | select([],sels) = sels
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   210
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   211
  in select(named_thms, []) end;
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   212
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   213
fun find_matching(prop,sign,index,extract) =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   214
  (case top_const prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   215
     Some c => select_match(prop,sign,index c,extract)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   216
   | _      => []);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   217
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   218
fun find_intros(prop,sign) =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   219
  find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   220
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   221
fun find_elims sign prop =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   222
  let fun major prop = case Logic.strip_imp_prems prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   223
                         [] => None | p::_ => Some p
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   224
  in find_matching(prop,sign,index_elims,major) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   225
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   226
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   227
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   228
fun findEs i =
1230
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   229
  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   230
      val sign = #sign(rep_thm(topthm()))
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   231
      val thmss = map (find_elims sign) (prems_of_goal i)
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   232
  in foldl (gen_union eq_nth) ([],thmss) end;
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   233
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   234
fun findE i j =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   235
  let val sign = #sign(rep_thm(topthm()))
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   236
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   237
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   238
end;