src/Pure/Isar/auto_bind.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 12241 c4a2a0686238
child 14981 e73f8140af78
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/auto_bind.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Logic specific patterns and automatic term bindings.
     7 *)
     8 
     9 signature AUTO_BIND =
    10 sig
    11   val goal: Sign.sg -> term list -> (indexname * term option) list
    12   val facts: Sign.sg -> term list -> (indexname * term option) list
    13   val thesisN: string
    14 end;
    15 
    16 structure AutoBind: AUTO_BIND =
    17 struct
    18 
    19 (** bindings **)
    20 
    21 val thesisN = "thesis";
    22 val thisN = "this";
    23 
    24 fun strip_judgment sg = ObjectLogic.drop_judgment sg o Logic.strip_assums_concl;
    25 
    26 fun statement_binds sg name prop =
    27   [((name, 0), Some (Term.list_abs (Logic.strip_params prop, strip_judgment sg prop)))];
    28 
    29 
    30 (* goal *)
    31 
    32 fun goal sg [prop] = statement_binds sg thesisN prop
    33   | goal _ _ = [((thesisN, 0), None)];
    34 
    35 
    36 (* facts *)
    37 
    38 fun get_arg sg prop =
    39   (case strip_judgment sg prop of
    40     _ $ t => Some (Term.list_abs (Logic.strip_params prop, t))
    41   | _ => None);
    42 
    43 fun facts _ [] = []
    44   | facts sg props =
    45       let val prop = Library.last_elem props
    46       in [(Syntax.dddot_indexname, get_arg sg prop)] @ statement_binds sg thisN prop end;
    47 
    48 
    49 end;