src/Pure/Isar/auto_bind.ML
author wenzelm
Sat Sep 04 21:05:01 1999 +0200 (1999-09-04 ago)
changeset 7474 43cedde6d52a
parent 7452 c2289eabf706
child 7599 40b7f7f51208
permissions -rw-r--r--
removed Syntax.binding;
     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_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", prop), (name ^ "_concl", list_abs concl)] @
    27       (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
    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   (case Logic.strip_imp_concl prop of
    37     Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    38   | _ => []);
    39 
    40 fun facts _ [] = []
    41   | facts name props =
    42       let val prop = Library.last_elem props
    43       in dddot_bind prop @ statement_binds ("this", prop) end;
    44       
    45 
    46 end;