src/Pure/Isar/auto_bind.ML
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 8612 e8ef58d6d6eb
child 8807 0046be1769f9
permissions -rw-r--r--
apply etc.: comments;
     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 fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
    30 
    31 
    32 (* goal *)
    33 
    34 fun statement_binds (name, prop) =
    35   let
    36     val concl = Logic.strip_assums_concl prop;
    37     val parms = Logic.strip_params prop;
    38 
    39     val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs parms concl)),
    40       (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs parms t) | _ => None)];
    41   in map (fn (s, t) => ((s, 0), t)) env end;
    42 
    43 fun goal prop = statement_binds (thesisN, prop);
    44 
    45 
    46 (* facts *)
    47 
    48 fun get_subject prop =
    49   (case (Logic.strip_assums_concl prop) of
    50     Const ("Trueprop", _) $ (_ $ t) => Some (list_abs (Logic.strip_params prop) t)
    51   | _ => None);
    52 
    53 fun facts _ [] = []
    54   | facts name props =
    55       let val prop = Library.last_elem props
    56       in [(Syntax.dddot_indexname, get_subject prop)] @ statement_binds (thisN, prop) end;
    57 
    58 
    59 (* atomic_thesis *)
    60 
    61 fun mk_free t = Free (thesisN, Term.fastype_of t);
    62 
    63 fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
    64   | atomic_thesis t = ((thesisN, t), mk_free t);
    65 
    66 
    67 (** judgment **)
    68 
    69 fun gen_add_judgment add args = PureThy.local_path o add [args] o PureThy.global_path;
    70 
    71 val add_judgment = gen_add_judgment Theory.add_consts;
    72 val add_judgment_i = gen_add_judgment Theory.add_consts_i;
    73 
    74 
    75 end;