src/Pure/Isar/auto_bind.ML
author wenzelm
Fri Oct 01 20:37:38 1999 +0200 (1999-10-01 ago)
changeset 7675 c859160e78b0
parent 7599 40b7f7f51208
child 8227 d67db92897df
permissions -rw-r--r--
added atomic_thesis;
     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 The implementation below works fine with the more common
     8 object-logics, such as HOL, ZF.
     9 *)
    10 
    11 signature AUTO_BIND =
    12 sig
    13   val goal: term -> (indexname * term option) list
    14   val facts: string -> term list -> (indexname * term option) list
    15   val atomic_thesis: term -> (string * term) * term
    16 end;
    17 
    18 structure AutoBind: AUTO_BIND =
    19 struct
    20 
    21 val thesisN = "thesis";
    22 val thisN = "this";
    23 
    24 
    25 (* goal *)
    26 
    27 fun statement_binds (name, prop) =
    28   let
    29     val concl = Logic.strip_assums_concl prop;
    30     val parms = Logic.strip_params prop;
    31     fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
    32 
    33     val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
    34       (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
    35   in map (fn (s, t) => ((s, 0), t)) env end;
    36 
    37 fun goal prop = statement_binds (thesisN, prop);
    38 
    39 
    40 (* facts *)
    41 
    42 fun dddot_bind prop =
    43   [(Syntax.dddot_indexname,
    44       case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
    45 
    46 fun facts _ [] = []
    47   | facts name props =
    48       let val prop = Library.last_elem props
    49       in dddot_bind prop @ statement_binds (thisN, prop) end;
    50 
    51 
    52 (* atomic_thesis *)
    53 
    54 fun mk_free t = Free (thesisN, Term.fastype_of t);
    55 
    56 fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
    57   | atomic_thesis t = ((thesisN, t), mk_free t);
    58       
    59 
    60 end;