src/Pure/Isar/object_logic.ML
author wenzelm
Tue, 14 Mar 2006 16:29:38 +0100
changeset 19261 9f8e56d1dbf6
parent 18939 18e2a2676d80
child 20912 380663e636a8
permissions -rw-r--r--
added is_elim (from Provers/classical.ML);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/object_logic.ML
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     4
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     5
Specifics about common object-logics.
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     6
*)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     7
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     8
signature OBJECT_LOGIC =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     9
sig
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    10
  val add_judgment: bstring * string * mixfix -> theory -> theory
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    11
  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    12
  val judgment_name: theory -> string
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    13
  val is_judgment: theory -> term -> bool
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    14
  val drop_judgment: theory -> term -> term
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    15
  val fixed_judgment: theory -> string -> term
18121
77b6d06ad99d renamed assert_prop to ensure_prop;
wenzelm
parents: 17902
diff changeset
    16
  val ensure_propT: theory -> term -> term
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
    17
  val is_elim: thm -> bool
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    18
  val declare_atomize: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    19
  val declare_rulify: attribute
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    20
  val atomize_term: theory -> term -> term
18783
628e57610536 tuned atomize_cterm;
wenzelm
parents: 18728
diff changeset
    21
  val atomize_cterm: cterm -> thm
14743
81001d6cb8c0 conversion of theorems to atomic form
paulson
parents: 14226
diff changeset
    22
  val atomize_thm: thm -> thm
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    23
  val atomize_tac: int -> tactic
12829
c92128238f85 full_atomize;
wenzelm
parents: 12807
diff changeset
    24
  val full_atomize_tac: int -> tactic
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    25
  val atomize_goal: int -> thm -> thm
18807
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
    26
  val rulify_term: theory -> term -> term
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
    27
  val rulify_tac: int -> tactic
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    28
  val rulify: thm -> thm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    29
  val rulify_no_asm: thm -> thm
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    30
  val rule_format: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    31
  val rule_format_no_asm: attribute
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    32
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    33
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    34
structure ObjectLogic: OBJECT_LOGIC =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    35
struct
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    36
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    37
18825
c13136d648e2 removed unatomize;
wenzelm
parents: 18807
diff changeset
    38
(** theory data **)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    39
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    40
structure ObjectLogicData = TheoryDataFun
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    41
(struct
18563
wenzelm
parents: 18254
diff changeset
    42
  val name = "Pure/object_logic";
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    43
  type T = string option * (thm list * thm list);
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    44
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    45
  val empty = (NONE, ([], [Drule.norm_hhf_eq]));
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    46
  val copy = I;
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    47
  val extend = I;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    48
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    49
  fun merge_judgment (SOME x, SOME y) =
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    50
        if x = y then SOME x else error "Attempt to merge different object-logics"
15973
wenzelm
parents: 15801
diff changeset
    51
    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    52
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    53
  fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    54
    (merge_judgment (judgment1, judgment2),
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    55
      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    56
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    57
  fun print _ _ = ();
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    58
end);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    59
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18563
diff changeset
    60
val _ = Context.add_setup ObjectLogicData.init;
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
    61
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    62
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    63
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    64
(** generic treatment of judgments -- with a single argument only **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    65
18825
c13136d648e2 removed unatomize;
wenzelm
parents: 18807
diff changeset
    66
(* add judgment *)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    67
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    68
local
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    69
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    70
fun new_judgment name (NONE, rules) = (SOME name, rules)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    71
  | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment";
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    72
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    73
fun gen_add_judgment add_consts (bname, T, mx) thy =
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    74
  let val c = Sign.full_name thy (Syntax.const_name bname mx) in
14226
7afe0e5bcc83 Made judgments automatically declared final.
skalberg
parents: 13376
diff changeset
    75
    thy
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    76
    |> add_consts [(bname, T, mx)]
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    77
    |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy')
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    78
    |> ObjectLogicData.map (new_judgment c)
14226
7afe0e5bcc83 Made judgments automatically declared final.
skalberg
parents: 13376
diff changeset
    79
  end;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    80
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    81
in
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    82
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    83
val add_judgment = gen_add_judgment Theory.add_consts;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    84
val add_judgment_i = gen_add_judgment Theory.add_consts_i;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    85
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    86
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    87
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    88
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    89
(* term operations *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    90
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    91
fun judgment_name thy =
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    92
  (case ObjectLogicData.get thy of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    93
    (SOME name, _) => name
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    94
  | _ => raise TERM ("Unknown object-logic judgment", []));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    95
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    96
fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    97
  | is_judgment _ _ = false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    98
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    99
fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   100
  | drop_judgment thy (tm as (Const (c, _) $ t)) =
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   101
      if (c = judgment_name thy handle TERM _ => false) then t else tm
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   102
  | drop_judgment _ tm = tm;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   103
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   104
fun fixed_judgment thy x =
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   105
  let  (*be robust wrt. low-level errors*)
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   106
    val c = judgment_name thy;
14854
61bdf2ae4dc5 removed obsolete sort 'logic';
wenzelm
parents: 14743
diff changeset
   107
    val aT = TFree ("'a", []);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   108
    val T =
18939
wenzelm
parents: 18842
diff changeset
   109
      the_default (aT --> propT) (Sign.const_type thy c)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   110
      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   111
    val U = Term.domain_type T handle Match => aT;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   112
  in Const (c, T) $ Free (x, U) end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   113
18121
77b6d06ad99d renamed assert_prop to ensure_prop;
wenzelm
parents: 17902
diff changeset
   114
fun ensure_propT thy t =
13376
59975b8417e2 assert_propT;
wenzelm
parents: 13334
diff changeset
   115
  let val T = Term.fastype_of t
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   116
  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
13376
59975b8417e2 assert_propT;
wenzelm
parents: 13334
diff changeset
   117
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   118
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   119
(* elimination rules *)
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   120
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   121
fun is_elim rule =
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   122
  let
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   123
    val thy = Thm.theory_of_thm rule;
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   124
    val concl = Thm.concl_of rule;
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   125
  in
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   126
    Term.is_Var (drop_judgment thy concl) andalso
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   127
      exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   128
  end;
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   129
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   130
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   131
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   132
(** treatment of meta-level connectives **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   133
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   134
(* maintain rules *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   135
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   136
val get_atomize = #1 o #2 o ObjectLogicData.get;
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   137
val get_rulify = #2 o #2 o ObjectLogicData.get;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   138
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   139
val declare_atomize =
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   140
  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   141
    Library.apsnd o Library.apfst o Drule.add_rule);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   142
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   143
val declare_rulify =
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   144
  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   145
    Library.apsnd o Library.apsnd o Drule.add_rule);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   146
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   147
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   148
(* atomize *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   149
15001
fb2141a9f8c0 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents: 14981
diff changeset
   150
fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule
fb2141a9f8c0 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents: 14981
diff changeset
   151
  (Drule.goals_conv (Library.equal i)
18254
4a081083b06e forall_conv ~1;
wenzelm
parents: 18121
diff changeset
   152
    (Drule.forall_conv ~1
15001
fb2141a9f8c0 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents: 14981
diff changeset
   153
      (Drule.goals_conv (K true) (Tactic.rewrite true rews)))));
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   154
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   155
fun atomize_term thy =
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   156
  drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
12729
46808b5ec985 added atomize_cterm;
wenzelm
parents: 12725
diff changeset
   157
18783
628e57610536 tuned atomize_cterm;
wenzelm
parents: 18728
diff changeset
   158
fun atomize_cterm ct = Tactic.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
17902
7b35ce796a4d renamed atomize_rule to atomize_cterm;
wenzelm
parents: 16449
diff changeset
   159
fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
14743
81001d6cb8c0 conversion of theorems to atomic form
paulson
parents: 14226
diff changeset
   160
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   161
fun atomize_tac i st =
12807
4f2983e39a59 atomize_term replaces atomize_cterm;
wenzelm
parents: 12729
diff changeset
   162
  if Logic.has_meta_prems (Thm.prop_of st) i then
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   163
    (rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   164
  else all_tac st;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   165
12829
c92128238f85 full_atomize;
wenzelm
parents: 12807
diff changeset
   166
fun full_atomize_tac i st =
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   167
  rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
12829
c92128238f85 full_atomize;
wenzelm
parents: 12807
diff changeset
   168
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   169
fun atomize_goal i st =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
   170
  (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   171
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   172
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   173
(* rulify *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   174
18807
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
   175
fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
   176
fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
   177
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   178
fun gen_rulify full thm =
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   179
  Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
12725
7ede865e1fe5 renamed forall_elim_vars_safe to gen_all;
wenzelm
parents: 12479
diff changeset
   180
  |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   181
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   182
val rulify = gen_rulify true;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   183
val rulify_no_asm = gen_rulify false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   184
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   185
fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   186
fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   187
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   188
end;