src/Pure/Isar/auto_bind.ML
author wenzelm
Mon Jul 19 21:26:33 1999 +0200 (1999-07-19 ago)
changeset 7048 3535eec33c50
parent 6796 c2e5cb8cd50d
child 7331 aee8f76fe54c
permissions -rw-r--r--
facts: no statement_binds;
     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 
     8 signature AUTO_BIND =
     9 sig
    10   val goal: term -> (indexname * term) list
    11   val facts: string -> term list -> (indexname * term) list
    12 end;
    13 
    14 structure AutoBind: AUTO_BIND =
    15 struct
    16 
    17 
    18 (* goals *)
    19 
    20 fun statement_binds (name, prop) =
    21   let
    22     val concl = Logic.strip_imp_concl prop;
    23     val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
    24       (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => []);
    25   in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
    26 
    27 fun goal prop = statement_binds ("thesis", prop);
    28 
    29 
    30 (* facts *)
    31 
    32 fun dddot_bind prop =
    33   (case Logic.strip_imp_concl prop of
    34     Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    35   | _ => []);
    36 
    37 fun facts _ [] = []
    38   | facts name [prop] = dddot_bind prop
    39   | facts name props =  dddot_bind (Library.last_elem props);
    40       
    41 
    42 end;