src/Provers/rulify.ML
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9884 8cc344b3435e
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      Provers/rulify.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Conversion of object-level -->/ALL into meta-level ==>/!!.
     7 *)
     8 
     9 signature BASIC_RULIFY =
    10 sig
    11   val rulify: thm -> thm
    12   val rulify_no_asm: thm -> thm
    13   val qed_spec_mp: string -> unit
    14   val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
    15   val qed_goalw_spec_mp: string -> theory -> thm list -> string
    16     -> (thm list -> tactic list) -> unit
    17 end;
    18 
    19 signature RULIFY =
    20 sig
    21   include BASIC_RULIFY
    22   val rule_format: 'a attribute
    23   val rule_format_no_asm: 'a attribute
    24   val setup: (theory -> theory) list
    25 end;
    26 
    27 functor RulifyFun(val make_meta: thm -> thm val full_make_meta: thm -> thm): RULIFY =
    28 struct
    29 
    30 
    31 (* rulify *)
    32 
    33 val tune = Drule.zero_var_indexes o Drule.strip_shyps_warning o Drule.forall_elim_vars_safe;
    34 
    35 val rulify = tune o full_make_meta;
    36 val rulify_no_asm = tune o make_meta;
    37 
    38 
    39 (* attributes *)
    40 
    41 fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
    42 fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
    43 
    44 fun rule_format_att x = Attrib.syntax
    45   (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rule_format_no_asm || Scan.succeed rule_format)) x;
    46 
    47 
    48 (* qed commands *)
    49 
    50 fun qed_spec_mp name = ThmDatabase.ml_store_thm (name, rulify_no_asm (Goals.result ()));
    51 
    52 fun qed_goal_spec_mp name thy s p =
    53   ThmDatabase.bind_thm (name, rulify_no_asm (Goals.prove_goal thy s p));
    54 
    55 fun qed_goalw_spec_mp name thy defs s p =
    56   ThmDatabase.bind_thm (name, rulify_no_asm (Goals.prove_goalw thy defs s p));
    57 
    58 
    59 (* theory setup *)
    60 
    61 val setup =
    62  [Attrib.add_attributes
    63   [("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")]];
    64 
    65 end;