src/Pure/Thy/thm_database.ML
author wenzelm
Mon, 29 Jun 1998 10:32:06 +0200
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5155 21177b8a4d7f
permissions -rw-r--r--
use_text: verbose flag;
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
3627
3d0d5f2a2e33 tuned names;
wenzelm
parents: 3601
diff changeset
     8
signature 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
3627
3d0d5f2a2e33 tuned names;
wenzelm
parents: 3601
diff changeset
    23
structure ThmDatabase: THM_DATABASE =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    24
struct
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    25
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    26
(** store theorems **)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    27
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    28
(* store in theory and generate HTML *)
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    29
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    30
fun store_thm (name, thm) =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    31
  let val thm' = PureThy.smart_store_thm (name, thm) in
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    32
    BrowserInfo.thm_to_html thm' name; thm'
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    33
  end;
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    34
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    35
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    36
(* store on ML toplevel *)
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    37
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    38
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
    39
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    40
val ml_reserved =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    41
 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    42
  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    43
  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    44
  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    45
  "eqtype", "functor", "include", "sharing", "sig", "signature",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    46
  "struct", "structure", "where"];
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    47
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    48
fun is_ml_identifier name =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    49
  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
    50
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    51
fun ml_store_thm (name, thm) =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    52
  let val thm' = store_thm (name, thm) in
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    53
    if is_ml_identifier name then
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    54
      (qed_thm := Some thm';
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    55
        use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    56
    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
    57
  end;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    58
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    59
fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    60
fun qed name = ml_store_thm (name, result ());
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    61
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
    62
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
    63
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    64
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    65
4037
wenzelm
parents: 4023
diff changeset
    66
(** retrieve theorems **)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    67
4037
wenzelm
parents: 4023
diff changeset
    68
(*get theorems that contain all of given constants*)
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    69
fun thms_containing raw_consts =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    70
  let
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    71
    val sign = sign_of_thm (topthm ());
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    72
    val consts = map (Sign.intern_const sign) raw_consts;
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    73
    val thy = ThyInfo.theory_of_sign sign;
4037
wenzelm
parents: 4023
diff changeset
    74
  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
    75
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    76
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    77
(*top_const: main constant, ignoring Trueprop*)
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    78
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
    79
  | top_const _ = None;
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    80
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    81
val intro_const = top_const o concl_of;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    82
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    83
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
    84
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    85
(* In case faster access is necessary, the thm db should provide special
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    86
functions
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    87
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    88
index_intros, index_elims: string -> (string * thm) list
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    89
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    90
where thm [| A1 ; ...; An |] ==> B is returned by
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    91
- index_intros c if B  is of the form c t1 ... tn
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    92
- index_elims c  if A1 is of the form c t1 ... tn
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    93
*)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    94
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    95
(* could be provided by thm db *)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    96
fun index_intros c =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    97
  let fun topc(_,thm) = intro_const thm = Some(c);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    98
      val named_thms = thms_containing [c]
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    99
  in filter topc named_thms end;
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_elims c =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   103
  let fun topc(_,thm) = elim_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
(*assume that parameters have unique names*)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   108
fun goal_params i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   109
  let val gi = getgoal i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   110
      val frees = map Free (Logic.strip_params gi)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   111
  in (gi,frees) 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
fun concl_of_goal i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   114
  let val (gi,frees) = goal_params i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   115
      val B = Logic.strip_assums_concl gi
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   116
  in subst_bounds(frees,B) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   117
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   118
fun prems_of_goal i =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   119
  let val (gi,frees) = goal_params i
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   120
      val As = Logic.strip_assums_hyp gi
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   121
  in map (fn A => subst_bounds(frees,A)) As end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   122
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   123
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
   124
  let fun matches(prop, tsig) =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   125
            case extract prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   126
              None => false
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   127
            | Some pat => Pattern.matches tsig (pat, obj);
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   128
1654
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   129
      fun substsize(prop, tsig) =
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   130
            let val Some pat = extract prop
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   131
                val (_,subst) = Pattern.match tsig (pat,obj)
2150
084218afaf4b Replaced "sum" (only usage?) by foldl op+
paulson
parents: 1749
diff changeset
   132
            in foldl op+
084218afaf4b Replaced "sum" (only usage?) by foldl op+
paulson
parents: 1749
diff changeset
   133
		(0, map (fn (_,t) => size_of_term t) subst)
084218afaf4b Replaced "sum" (only usage?) by foldl op+
paulson
parents: 1749
diff changeset
   134
            end
1654
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   135
4546
271753a7ce24 thm_ord;
wenzelm
parents: 4538
diff changeset
   136
      fun thm_ord ((p0,s0,_),(p1,s1,_)) =
271753a7ce24 thm_ord;
wenzelm
parents: 4538
diff changeset
   137
            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
   138
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   139
      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
   140
            let val {prop, sign, ...} = rep_thm thm
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   141
            in select(named_thms,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
   142
                      if Sign.subsig(sign, signobj) andalso
1230
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   143
                         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
   144
                      then
faa643c33ee6 select_match now sorts list of matching theorems according to the
berghofe
parents: 1580
diff changeset
   145
			(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
   146
                      else sels)
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   147
            end
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
   148
        | select([],sels) = sels
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   149
4546
271753a7ce24 thm_ord;
wenzelm
parents: 4538
diff changeset
   150
  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; 
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   151
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   152
fun find_matching(prop,sign,index,extract) =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   153
  (case top_const prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   154
     Some c => select_match(prop,sign,index c,extract)
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   155
   | _      => []);
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   156
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   157
fun find_intros(prop,sign) =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   158
  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
   159
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   160
fun find_elims sign prop =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   161
  let fun major prop = case Logic.strip_imp_prems prop of
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   162
                         [] => None | p::_ => Some p
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   163
  in find_matching(prop,sign,index_elims,major) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   164
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   165
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   166
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   167
fun findEs i =
1230
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   168
  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
   169
      val sign = #sign(rep_thm(topthm()))
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   170
      val thmss = map (find_elims sign) (prems_of_goal i)
87e29e18e970 fixed bug in findI
nipkow
parents: 1221
diff changeset
   171
  in foldl (gen_union eq_nth) ([],thmss) end;
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   172
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   173
fun findE i j =
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   174
  let val sign = #sign(rep_thm(topthm()))
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   175
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
   176
3601
43c7912aac8d Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
berghofe
parents: 2150
diff changeset
   177
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   178
end;