src/Pure/Isar/auto_bind.ML
author wenzelm
Sat Jun 05 20:27:53 1999 +0200 (1999-06-05)
changeset 6783 9cf9c17d9e35
child 6796 c2e5cb8cd50d
permissions -rw-r--r--
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm@6783
     1
(*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783
     2
    ID:         $Id$
wenzelm@6783
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6783
     4
wenzelm@6783
     5
Automatic term bindings -- logic specific patterns.
wenzelm@6783
     6
wenzelm@6783
     7
TODO:
wenzelm@6783
     8
  - logic specific theory data instead of hardwired operations (!!);
wenzelm@6783
     9
*)
wenzelm@6783
    10
wenzelm@6783
    11
signature AUTO_BIND =
wenzelm@6783
    12
sig
wenzelm@6783
    13
  val goal: term -> (indexname * term) list
wenzelm@6783
    14
  val facts: term list -> (indexname * term) list
wenzelm@6783
    15
end;
wenzelm@6783
    16
wenzelm@6783
    17
structure AutoBind: AUTO_BIND =
wenzelm@6783
    18
struct
wenzelm@6783
    19
wenzelm@6783
    20
val thesisN = "thesis";
wenzelm@6783
    21
fun thesis_name sfx = (Syntax.binding (thesisN ^ sfx), 0);
wenzelm@6783
    22
wenzelm@6783
    23
fun goal prop =
wenzelm@6783
    24
  let val concl = Logic.strip_imp_concl prop in
wenzelm@6783
    25
    [(thesis_name "_prop", prop), (thesis_name "_concl", concl)] @
wenzelm@6783
    26
      (case concl of Const ("Trueprop", _) $ t => [(thesis_name "", t)] | _ => [])
wenzelm@6783
    27
  end;
wenzelm@6783
    28
wenzelm@6783
    29
fun facts [] = []
wenzelm@6783
    30
  | facts props =
wenzelm@6783
    31
      (case Logic.strip_imp_concl (Library.last_elem props) of
wenzelm@6783
    32
        Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
wenzelm@6783
    33
      | _ => []);
wenzelm@6783
    34
wenzelm@6783
    35
wenzelm@6783
    36
end;