src/Pure/Isar/auto_bind.ML
author wenzelm
Sat Sep 25 13:07:48 1999 +0200 (1999-09-25)
changeset 7599 40b7f7f51208
parent 7474 43cedde6d52a
child 7675 c859160e78b0
permissions -rw-r--r--
admit unbinding;
     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 option) list
    11   val facts: string -> term list -> (indexname * term option) 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_assums_concl prop;
    23     val parms = Logic.strip_params prop;
    24     fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
    25 
    26     val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
    27       (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
    28   in map (fn (s, t) => ((s, 0), t)) env end;
    29 
    30 fun goal prop = statement_binds ("thesis", prop);
    31 
    32 
    33 (* facts *)
    34 
    35 fun dddot_bind prop =
    36   [(Syntax.dddot_indexname,
    37       case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
    38 
    39 fun facts _ [] = []
    40   | facts name props =
    41       let val prop = Library.last_elem props
    42       in dddot_bind prop @ statement_binds ("this", prop) end;
    43       
    44 
    45 end;