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