src/Pure/Thy/thm_database.ML
author wenzelm
Wed, 03 Feb 1999 17:23:35 +0100
changeset 6204 c7ad5b27894f
parent 5744 9e73738f2307
child 6327 c6abb5884fed
permissions -rw-r--r--
open BasicThmDatabase; Present.thm;
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$
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
     3
    Author:     Carsten Clasohm and Tobias Nipkow and Markus Wenzel, TU Muenchen
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     4
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
     5
User level interface to thm database (see also Pure/pure_thy.ML).
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
     6
*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
     7
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
     8
signature BASIC_THM_DATABASE =
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
     9
sig
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    10
  val store_thm: string * thm -> thm
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    11
  val qed_thm: thm option ref
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    12
  val bind_thm: string * thm -> unit
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    13
  val qed: string -> unit
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    14
  val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    15
  val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    16
  (*these peek at the proof state!*)
4287
227a9e786c35 fixed type of thms_containing;
wenzelm
parents: 4037
diff changeset
    17
  val thms_containing: xstring list -> (string * thm) list
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    18
  val findI: int -> (string * thm) list
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    19
  val findEs: int -> (string * thm) list
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    20
  val findE: int -> int -> (string * thm) list
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    21
end;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    22
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    23
signature THM_DATABASE =
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    24
sig
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    25
  include BASIC_THM_DATABASE
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    26
  val ml_store_thm: string * thm -> unit
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    27
  val is_ml_identifier: string -> bool
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    28
end;
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    29
3627
3d0d5f2a2e33 tuned names;
wenzelm
parents: 3601
diff changeset
    30
structure ThmDatabase: THM_DATABASE =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    31
struct
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    32
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    33
(** store theorems **)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    34
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    35
(* store in theory and generate HTML *)
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    36
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    37
fun store_thm (name, thm) =
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    38
  let val thm' = PureThy.smart_store_thm (name, thm)
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    39
  in Present.thm name thm'; thm' end;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    40
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    41
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    42
(* store on ML toplevel *)
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    43
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    44
val qed_thm: thm option ref = ref None;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    45
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    46
val ml_reserved =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    47
 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    48
  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    49
  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    50
  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    51
  "eqtype", "functor", "include", "sharing", "sig", "signature",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    52
  "struct", "structure", "where"];
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    53
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    54
fun is_ml_identifier name =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    55
  Syntax.is_identifier name andalso not (name mem ml_reserved);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    56
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    57
fun ml_store_thm (name, thm) =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    58
  let val thm' = store_thm (name, thm) in
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    59
    if is_ml_identifier name then
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    60
      (qed_thm := Some thm';
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    61
        use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    62
    else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    63
  end;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    64
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    65
fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    66
fun qed name = ml_store_thm (name, result ());
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    67
fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    68
fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    69
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    70
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    71
4037
wenzelm
parents: 4023
diff changeset
    72
(** retrieve theorems **)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    73
4037
wenzelm
parents: 4023
diff changeset
    74
(*get theorems that contain all of given constants*)
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    75
fun thms_containing raw_consts =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    76
  let
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    77
    val sign = sign_of_thm (topthm ());
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    78
    val consts = map (Sign.intern_const sign) raw_consts;
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    79
    val thy = ThyInfo.theory_of_sign sign;
4037
wenzelm
parents: 4023
diff changeset
    80
  in PureThy.thms_containing thy consts end;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    81
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    82
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    83
(*top_const: main constant, ignoring Trueprop*)
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    84
fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    85
  | top_const _ = None;
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    86
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    87
val intro_const = top_const o concl_of;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    88
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    89
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    90
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    91
(* In case faster access is necessary, the thm db should provide special
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    92
functions
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    93
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    94
index_intros, index_elims: string -> (string * thm) list
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    95
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    96
where thm [| A1 ; ...; An |] ==> B is returned by
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    97
- index_intros c if B  is of the form c t1 ... tn
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    98
- index_elims c  if A1 is of the form c t1 ... tn
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    99
*)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   100
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   101
(* could be provided by thm db *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   102
fun index_intros c =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   103
  let fun topc(_,thm) = intro_const thm = Some(c);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   104
      val named_thms = thms_containing [c]
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   105
  in filter topc named_thms end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   106
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   107
(* could be provided by thm db *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   108
fun index_elims c =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   109
  let fun topc(_,thm) = elim_const thm = Some(c);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   110
      val named_thms = thms_containing [c]
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   111
  in filter topc named_thms end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   112
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   113
(*assume that parameters have unique names*)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   114
fun goal_params i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   115
  let val gi = getgoal i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   116
      val frees = map Free (Logic.strip_params gi)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   117
  in (gi,frees) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   118
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   119
fun concl_of_goal i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   120
  let val (gi,frees) = goal_params i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   121
      val B = Logic.strip_assums_concl gi
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   122
  in subst_bounds(frees,B) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   123
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   124
fun prems_of_goal i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   125
  let val (gi,frees) = goal_params i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   126
      val As = Logic.strip_assums_hyp gi
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   127
  in map (fn A => subst_bounds(frees,A)) As end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   128
5155
21177b8a4d7f added comments
paulson
parents: 5090
diff changeset
   129
(*returns all those named_thms whose subterm extracted by extract can be
21177b8a4d7f added comments
paulson
parents: 5090
diff changeset
   130
  instantiated to obj; the list is sorted according to the number of premises
21177b8a4d7f added comments
paulson
parents: 5090
diff changeset
   131
  and the size of the required substitution.*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   132
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
   133
  let fun matches(prop, tsig) =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   134
            case extract prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   135
              None => false
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   136
            | Some pat => Pattern.matches tsig (pat, obj);
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   137
1654
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   138
      fun substsize(prop, tsig) =
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   139
            let val Some pat = extract prop
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   140
                val (_,subst) = Pattern.match tsig (pat,obj)
2150
084218afaf4b Replaced "sum" (only usage?) by foldl op+
paulson
parents: 1749
diff changeset
   141
            in foldl op+
084218afaf4b Replaced "sum" (only usage?) by foldl op+
paulson
parents: 1749
diff changeset
   142
		(0, map (fn (_,t) => size_of_term t) subst)
084218afaf4b Replaced "sum" (only usage?) by foldl op+
paulson
parents: 1749
diff changeset
   143
            end
1654
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   144
4546
271753a7ce24 thm_ord;
wenzelm
parents: 4538
diff changeset
   145
      fun thm_ord ((p0,s0,_),(p1,s1,_)) =
271753a7ce24 thm_ord;
wenzelm
parents: 4538
diff changeset
   146
            prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
1654
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   147
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   148
      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
   149
            let val {prop, sign, ...} = rep_thm thm
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   150
            in select(named_thms,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   151
                      if Sign.subsig(sign, signobj) andalso
1230
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   152
                         matches(prop,#tsig(Sign.rep_sg signobj))
1654
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   153
                      then
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   154
			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   155
                      else sels)
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   156
            end
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   157
        | select([],sels) = sels
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   158
4546
271753a7ce24 thm_ord;
wenzelm
parents: 4538
diff changeset
   159
  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; 
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   160
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   161
fun find_matching(prop,sign,index,extract) =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   162
  (case top_const prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   163
     Some c => select_match(prop,sign,index c,extract)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   164
   | _      => []);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   165
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   166
fun find_intros(prop,sign) =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   167
  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
   168
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   169
fun find_elims sign prop =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   170
  let fun major prop = case Logic.strip_imp_prems prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   171
                         [] => None | p::_ => Some p
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   172
  in find_matching(prop,sign,index_elims,major) 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
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   175
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   176
fun findEs i =
1230
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   177
  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
   178
      val sign = #sign(rep_thm(topthm()))
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   179
      val thmss = map (find_elims sign) (prems_of_goal i)
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   180
  in foldl (gen_union eq_nth) ([],thmss) end;
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   181
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   182
fun findE i j =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   183
  let val sign = #sign(rep_thm(topthm()))
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   184
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   185
3601
43c7912aac8d Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
berghofe
parents: 2150
diff changeset
   186
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   187
end;
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   188
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   189
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   190
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   191
open BasicThmDatabase;