src/Pure/Isar/object_logic.ML
author haftmann
Sat, 20 Aug 2011 01:21:22 +0200
changeset 44323 4b5b430eb00e
parent 42375 774df7c59508
child 45375 7fe19930dfc9
permissions -rw-r--r--
merged
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
    Author:     Markus Wenzel, TU Muenchen
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     3
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     4
Specifics about common object-logics.
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     5
*)
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
signature OBJECT_LOGIC =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     8
sig
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
     9
  val get_base_sort: theory -> sort option
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    10
  val add_base_sort: sort -> theory -> theory
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    11
  val add_judgment: binding * typ * mixfix -> theory -> theory
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    12
  val add_judgment_cmd: binding * string * mixfix -> theory -> theory
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    13
  val judgment_name: theory -> string
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    14
  val is_judgment: theory -> term -> bool
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    15
  val drop_judgment: theory -> term -> term
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    16
  val fixed_judgment: theory -> string -> term
18121
77b6d06ad99d renamed assert_prop to ensure_prop;
wenzelm
parents: 17902
diff changeset
    17
  val ensure_propT: theory -> term -> term
23586
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
    18
  val dest_judgment: cterm -> cterm
23566
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
    19
  val judgment_conv: conv -> conv
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
    20
  val elim_concl: thm -> term option
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    21
  val declare_atomize: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    22
  val declare_rulify: attribute
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    23
  val atomize_term: theory -> term -> term
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
    24
  val atomize: conv
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
    25
  val atomize_prems: conv
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
    26
  val atomize_prems_tac: int -> tactic
12829
c92128238f85 full_atomize;
wenzelm
parents: 12807
diff changeset
    27
  val full_atomize_tac: int -> tactic
18807
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
    28
  val rulify_term: theory -> term -> term
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
    29
  val rulify_tac: int -> tactic
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    30
  val rulify: thm -> thm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    31
  val rulify_no_asm: thm -> thm
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    32
  val rule_format: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    33
  val rule_format_no_asm: attribute
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    34
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    35
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35129
diff changeset
    36
structure Object_Logic: OBJECT_LOGIC =
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    37
struct
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    38
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    39
(** theory data **)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    40
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    41
datatype data = Data of
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    42
 {base_sort: sort option,
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    43
  judgment: string option,
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    44
  atomize_rulify: thm list * thm list};
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    45
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    46
fun make_data (base_sort, judgment, atomize_rulify) =
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    47
  Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    48
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36610
diff changeset
    49
structure Data = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
    50
(
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    51
  type T = data;
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    52
  val empty = make_data (NONE, NONE, ([], []));
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    53
  val extend = I;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    54
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    55
  fun merge_opt eq (SOME x, SOME y) =
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    56
        if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
41493
f05976d69141 added merge_options convenience;
wenzelm
parents: 41228
diff changeset
    57
    | merge_opt _ data = merge_options data;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    58
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33090
diff changeset
    59
  fun merge
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    60
     (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    61
      Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    62
    make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 23602
diff changeset
    63
      (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
    64
);
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
    65
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36610
diff changeset
    66
fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    67
  make_data (f (base_sort, judgment, atomize_rulify)));
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    68
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36610
diff changeset
    69
fun get_data thy = Data.get thy |> (fn Data args => args);
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    70
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    71
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    72
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    73
(** generic treatment of judgments -- with a single argument only **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    74
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    75
(* base_sort *)
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    76
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    77
val get_base_sort = #base_sort o get_data;
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    78
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    79
fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    80
  if is_some base_sort then error "Attempt to redeclare object-logic base sort"
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    81
  else (SOME S, judgment, atomize_rulify));
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    82
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    83
18825
c13136d648e2 removed unatomize;
wenzelm
parents: 18807
diff changeset
    84
(* add judgment *)
11897
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
local
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    87
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    88
fun gen_add_judgment add_consts (b, T, mx) thy =
35129
ed24ba6f69aa discontinued unnamed infix syntax;
wenzelm
parents: 33522
diff changeset
    89
  let val c = Sign.full_name thy b in
14226
7afe0e5bcc83 Made judgments automatically declared final.
skalberg
parents: 13376
diff changeset
    90
    thy
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    91
    |> add_consts [(b, T, mx)]
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
    92
    |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    93
    |> map_data (fn (base_sort, judgment, atomize_rulify) =>
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    94
        if is_some judgment then error "Attempt to redeclare object-logic judgment"
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    95
        else (base_sort, SOME c, atomize_rulify))
14226
7afe0e5bcc83 Made judgments automatically declared final.
skalberg
parents: 13376
diff changeset
    96
  end;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    97
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    98
in
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    99
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
   100
val add_judgment = gen_add_judgment Sign.add_consts_i;
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
   101
val add_judgment_cmd = gen_add_judgment Sign.add_consts;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   102
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   103
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   104
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   105
23566
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   106
(* judgments *)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   107
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   108
fun judgment_name thy =
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   109
  (case #judgment (get_data thy) of
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   110
    SOME name => name
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   111
  | _ => raise TERM ("Unknown object-logic judgment", []));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   112
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   113
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
   114
  | is_judgment _ _ = false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   115
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   116
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
   117
  | drop_judgment thy (tm as (Const (c, _) $ t)) =
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   118
      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
   119
  | drop_judgment _ tm = tm;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   120
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   121
fun fixed_judgment thy x =
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   122
  let  (*be robust wrt. low-level errors*)
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   123
    val c = judgment_name thy;
24848
5dbbd33c3236 replaced literal 'a by Name.aT;
wenzelm
parents: 24832
diff changeset
   124
    val aT = TFree (Name.aT, []);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   125
    val T =
18939
wenzelm
parents: 18842
diff changeset
   126
      the_default (aT --> propT) (Sign.const_type thy c)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   127
      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   128
    val U = Term.domain_type T handle Match => aT;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   129
  in Const (c, T) $ Free (x, U) end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   130
18121
77b6d06ad99d renamed assert_prop to ensure_prop;
wenzelm
parents: 17902
diff changeset
   131
fun ensure_propT thy t =
13376
59975b8417e2 assert_propT;
wenzelm
parents: 13334
diff changeset
   132
  let val T = Term.fastype_of t
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   133
  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
13376
59975b8417e2 assert_propT;
wenzelm
parents: 13334
diff changeset
   134
23586
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   135
fun dest_judgment ct =
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   136
  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   137
  then Thm.dest_arg ct
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   138
  else raise CTERM ("dest_judgment", [ct]);
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   139
23566
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   140
fun judgment_conv cv ct =
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   141
  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   142
  then Conv.arg_conv cv ct
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   143
  else raise CTERM ("judgment_conv", [ct]);
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   144
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   145
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   146
(* elimination rules *)
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   147
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
   148
fun elim_concl rule =
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   149
  let
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   150
    val thy = Thm.theory_of_thm rule;
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   151
    val concl = Thm.concl_of rule;
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
   152
    val C = drop_judgment thy concl;
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   153
  in
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
   154
    if Term.is_Var C andalso
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   155
      exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
   156
    then SOME C else NONE
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   157
  end;
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   158
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   159
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   160
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   161
(** treatment of meta-level connectives **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   162
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   163
(* maintain rules *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   164
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   165
val get_atomize = #1 o #atomize_rulify o get_data;
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   166
val get_rulify = #2 o #atomize_rulify o get_data;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   167
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   168
fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   169
  (base_sort, judgment, (Thm.add_thm th atomize, rulify)));
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   170
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   171
fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   172
  (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   173
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
   174
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
   175
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
   176
28620
9846d772b306 Drule.norm_hhf_eqs;
wenzelm
parents: 26568
diff changeset
   177
val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   178
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   179
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   180
(* atomize *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   181
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
   182
fun atomize_term thy =
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   183
  drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
12729
46808b5ec985 added atomize_cterm;
wenzelm
parents: 12725
diff changeset
   184
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   185
fun atomize ct =
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   186
  Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
14743
81001d6cb8c0 conversion of theorems to atomic form
paulson
parents: 14226
diff changeset
   187
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   188
fun atomize_prems ct =
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   189
  if Logic.has_meta_prems (Thm.term_of ct) then
26568
3a3a83493f00 renamed iterated forall_conv to params_conv;
wenzelm
parents: 26463
diff changeset
   190
    Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41581
diff changeset
   191
      (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   192
  else Conv.all_conv ct;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   193
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   194
val atomize_prems_tac = CONVERSION atomize_prems;
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   195
val full_atomize_tac = CONVERSION atomize;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   196
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   197
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   198
(* rulify *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   199
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   200
fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   201
fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
18807
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
   202
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   203
fun gen_rulify full thm =
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   204
  Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
20912
380663e636a8 attribute: Context.mapping;
wenzelm
parents: 19261
diff changeset
   205
  |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   206
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   207
val rulify = gen_rulify true;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   208
val rulify_no_asm = gen_rulify false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   209
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   210
fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   211
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
   212
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   213
end;