src/Pure/Isar/auto_bind.ML
author wenzelm
Thu Feb 10 13:34:38 2000 +0100 (2000-02-10 ago)
changeset 8227 d67db92897df
parent 7675 c859160e78b0
child 8612 e8ef58d6d6eb
permissions -rw-r--r--
add_judgment;
     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 Note: the current implementation is not quite 'generic', but works
     8 fine with the more common object-logics (HOL, FOL, ZF etc.).
     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   val add_judgment: bstring * string * mixfix -> theory -> theory
    17   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
    18 end;
    19 
    20 structure AutoBind: AUTO_BIND =
    21 struct
    22 
    23 val thesisN = "thesis";
    24 val thisN = "this";
    25 
    26 
    27 (** bindings **)
    28 
    29 (* goal *)
    30 
    31 fun statement_binds (name, prop) =
    32   let
    33     val concl = Logic.strip_assums_concl prop;
    34     val parms = Logic.strip_params prop;
    35     fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
    36 
    37     val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
    38       (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
    39   in map (fn (s, t) => ((s, 0), t)) env end;
    40 
    41 fun goal prop = statement_binds (thesisN, prop);
    42 
    43 
    44 (* facts *)
    45 
    46 fun dddot_bind prop =
    47   [(Syntax.dddot_indexname,
    48       case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
    49 
    50 fun facts _ [] = []
    51   | facts name props =
    52       let val prop = Library.last_elem props
    53       in dddot_bind prop @ statement_binds (thisN, prop) end;
    54 
    55 
    56 (* atomic_thesis *)
    57 
    58 fun mk_free t = Free (thesisN, Term.fastype_of t);
    59 
    60 fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
    61   | atomic_thesis t = ((thesisN, t), mk_free t);
    62 
    63 
    64 (** judgment **)
    65 
    66 fun gen_add_judgment add args = PureThy.local_path o add [args] o PureThy.global_path;
    67 
    68 val add_judgment = gen_add_judgment Theory.add_consts;
    69 val add_judgment_i = gen_add_judgment Theory.add_consts_i;
    70 
    71 
    72 end;