src/Pure/Isar/auto_bind.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
child 33386 ff29d1549aca
permissions -rw-r--r--
use long names for old-style fold combinators;
     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 AutoBind: 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 = ObjectLogic.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;