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;
     1 (*  Title:      Pure/Isar/auto_bind.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Automatic term bindings -- logic specific patterns.
     6 
     7 TODO:
     8   - logic specific theory data instead of hardwired operations (!!);
     9 *)
    10 
    11 signature AUTO_BIND =
    12 sig
    13   val goal: term -> (indexname * term) list
    14   val facts: term list -> (indexname * term) list
    15 end;
    16 
    17 structure AutoBind: AUTO_BIND =
    18 struct
    19 
    20 val thesisN = "thesis";
    21 fun thesis_name sfx = (Syntax.binding (thesisN ^ sfx), 0);
    22 
    23 fun goal prop =
    24   let val concl = Logic.strip_imp_concl prop in
    25     [(thesis_name "_prop", prop), (thesis_name "_concl", concl)] @
    26       (case concl of Const ("Trueprop", _) $ t => [(thesis_name "", t)] | _ => [])
    27   end;
    28 
    29 fun facts [] = []
    30   | facts props =
    31       (case Logic.strip_imp_concl (Library.last_elem props) of
    32         Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    33       | _ => []);
    34 
    35 
    36 end;