src/Pure/Isar/auto_bind.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 19075 12833c7e0fa6
child 21448 09c953c07008
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     1 (*  Title:      Pure/Isar/auto_bind.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Automatic bindings of Isar text elements.
     6 *)
     7 
     8 signature AUTO_BIND =
     9 sig
    10   val rule_contextN: string
    11   val thesisN: string
    12   val thisN: string
    13   val premsN: string
    14   val goal: theory -> term list -> (indexname * term option) list
    15   val cases: theory -> term list -> (string * RuleCases.T option) list
    16   val facts: theory -> term list -> (indexname * term option) list
    17   val no_facts: (indexname * term option) list
    18 end;
    19 
    20 structure AutoBind: AUTO_BIND =
    21 struct
    22 
    23 (** bindings **)
    24 
    25 val rule_contextN = "rule_context";
    26 val thesisN = "thesis";
    27 val thisN = "this";
    28 val premsN = "prems";
    29 
    30 fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
    31 
    32 fun statement_binds thy name prop =
    33   [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
    34 
    35 
    36 (* goal *)
    37 
    38 fun goal thy [prop] = statement_binds thy thesisN prop
    39   | goal _ _ = [((thesisN, 0), NONE)];
    40 
    41 fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
    42   | cases _ _ = [(rule_contextN, NONE)];
    43 
    44 
    45 (* facts *)
    46 
    47 fun get_arg thy prop =
    48   (case strip_judgment thy prop of
    49     _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
    50   | _ => NONE);
    51 
    52 fun facts _ [] = []
    53   | facts thy props =
    54       let val prop = Library.last_elem props
    55       in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
    56 
    57 val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
    58 
    59 end;