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