src/Pure/Isar/auto_bind.ML
author wenzelm
Mon Jun 07 22:16:56 1999 +0200 (1999-06-07)
changeset 6796 c2e5cb8cd50d
parent 6783 9cf9c17d9e35
child 7048 3535eec33c50
permissions -rw-r--r--
facts: bind named props (from proof.ML/let_thms);
     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] = statement_binds (name, prop) @ dddot_bind prop
    39   | facts name props =
    40       flat (map statement_binds
    41         (map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props))) @
    42       dddot_bind (Library.last_elem props);
    43       
    44 
    45 end;