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