src/Pure/Isar/auto_bind.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 35625 9c818cab0dd0
child 41489 8e2b8649507d
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     1 (*  Title:      Pure/Isar/auto_bind.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Automatic bindings of Isar text elements.
     5 *)
     6 
     7 signature AUTO_BIND =
     8 sig
     9   val thesisN: string
    10   val thisN: string
    11   val assmsN: string
    12   val goal: theory -> term list -> (indexname * term option) list
    13   val facts: theory -> term list -> (indexname * term option) list
    14   val no_facts: (indexname * term option) list
    15 end;
    16 
    17 structure Auto_Bind: AUTO_BIND =
    18 struct
    19 
    20 (** bindings **)
    21 
    22 val thesisN = "thesis";
    23 val thisN = "this";
    24 val assmsN = "assms";
    25 
    26 fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
    27 
    28 fun statement_binds thy name prop =
    29   [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
    30 
    31 
    32 (* goal *)
    33 
    34 fun goal thy [prop] = statement_binds thy thesisN prop
    35   | goal _ _ = [((thesisN, 0), NONE)];
    36 
    37 
    38 (* facts *)
    39 
    40 fun get_arg thy prop =
    41   (case strip_judgment thy prop of
    42     _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
    43   | _ => NONE);
    44 
    45 fun facts _ [] = []
    46   | facts thy props =
    47       let val prop = Library.last_elem props
    48       in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
    49 
    50 val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
    51 
    52 end;