src/Pure/Isar/object_logic.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35129 ed24ba6f69aa
child 35626 06197484c6ad
permissions -rw-r--r--
modernized structure Object_Logic;
wenzelm@11897
     1
(*  Title:      Pure/Isar/object_logic.ML
wenzelm@11897
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@11897
     3
wenzelm@11897
     4
Specifics about common object-logics.
wenzelm@11897
     5
*)
wenzelm@11897
     6
wenzelm@11897
     7
signature OBJECT_LOGIC =
wenzelm@11897
     8
sig
wenzelm@25497
     9
  val get_base_sort: theory -> sort option
wenzelm@25497
    10
  val add_base_sort: sort -> theory -> theory
wenzelm@30344
    11
  val typedecl: binding * string list * mixfix -> theory -> typ * theory
wenzelm@30344
    12
  val add_judgment: binding * typ * mixfix -> theory -> theory
wenzelm@30344
    13
  val add_judgment_cmd: binding * string * mixfix -> theory -> theory
wenzelm@16449
    14
  val judgment_name: theory -> string
wenzelm@16449
    15
  val is_judgment: theory -> term -> bool
wenzelm@16449
    16
  val drop_judgment: theory -> term -> term
wenzelm@16449
    17
  val fixed_judgment: theory -> string -> term
wenzelm@18121
    18
  val ensure_propT: theory -> term -> term
wenzelm@23586
    19
  val dest_judgment: cterm -> cterm
wenzelm@23566
    20
  val judgment_conv: conv -> conv
wenzelm@19261
    21
  val is_elim: thm -> bool
wenzelm@18728
    22
  val declare_atomize: attribute
wenzelm@18728
    23
  val declare_rulify: attribute
wenzelm@16449
    24
  val atomize_term: theory -> term -> term
wenzelm@23602
    25
  val atomize: conv
wenzelm@23602
    26
  val atomize_prems: conv
wenzelm@23602
    27
  val atomize_prems_tac: int -> tactic
wenzelm@12829
    28
  val full_atomize_tac: int -> tactic
wenzelm@18807
    29
  val rulify_term: theory -> term -> term
wenzelm@18807
    30
  val rulify_tac: int -> tactic
wenzelm@11897
    31
  val rulify: thm -> thm
wenzelm@11897
    32
  val rulify_no_asm: thm -> thm
wenzelm@18728
    33
  val rule_format: attribute
wenzelm@18728
    34
  val rule_format_no_asm: attribute
wenzelm@11897
    35
end;
wenzelm@11897
    36
wenzelm@35625
    37
structure Object_Logic: OBJECT_LOGIC =
wenzelm@11897
    38
struct
wenzelm@11897
    39
wenzelm@25497
    40
(** theory data **)
wenzelm@11897
    41
wenzelm@25497
    42
datatype data = Data of
wenzelm@25497
    43
 {base_sort: sort option,
wenzelm@25497
    44
  judgment: string option,
wenzelm@25497
    45
  atomize_rulify: thm list * thm list};
wenzelm@25497
    46
wenzelm@25497
    47
fun make_data (base_sort, judgment, atomize_rulify) =
wenzelm@25497
    48
  Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
wenzelm@11897
    49
wenzelm@33522
    50
structure ObjectLogicData = Theory_Data
wenzelm@22846
    51
(
wenzelm@25497
    52
  type T = data;
wenzelm@25497
    53
  val empty = make_data (NONE, NONE, ([], []));
wenzelm@16449
    54
  val extend = I;
wenzelm@11897
    55
wenzelm@25497
    56
  fun merge_opt eq (SOME x, SOME y) =
wenzelm@25497
    57
        if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
wenzelm@25497
    58
    | merge_opt _ (x, y) = if is_some x then x else y;
wenzelm@11897
    59
wenzelm@33522
    60
  fun merge
wenzelm@25497
    61
     (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
wenzelm@25497
    62
      Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
wenzelm@25497
    63
    make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
wenzelm@24039
    64
      (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
wenzelm@22846
    65
);
wenzelm@15801
    66
wenzelm@25497
    67
fun map_data f = ObjectLogicData.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
wenzelm@25497
    68
  make_data (f (base_sort, judgment, atomize_rulify)));
wenzelm@25497
    69
wenzelm@25497
    70
fun get_data thy = ObjectLogicData.get thy |> (fn Data args => args);
wenzelm@25497
    71
wenzelm@11897
    72
wenzelm@11897
    73
wenzelm@11897
    74
(** generic treatment of judgments -- with a single argument only **)
wenzelm@11897
    75
wenzelm@25497
    76
(* base_sort *)
wenzelm@25497
    77
wenzelm@25497
    78
val get_base_sort = #base_sort o get_data;
wenzelm@25497
    79
wenzelm@25497
    80
fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
wenzelm@25497
    81
  if is_some base_sort then error "Attempt to redeclare object-logic base sort"
wenzelm@25497
    82
  else (SOME S, judgment, atomize_rulify));
wenzelm@25497
    83
wenzelm@25497
    84
wenzelm@25497
    85
(* typedecl *)
wenzelm@25497
    86
wenzelm@35129
    87
fun typedecl (b, vs, mx) thy =
wenzelm@25497
    88
  let
wenzelm@25497
    89
    val base_sort = get_base_sort thy;
wenzelm@25497
    90
    val _ = has_duplicates (op =) vs andalso
wenzelm@33090
    91
      error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
wenzelm@30344
    92
    val name = Sign.full_name thy b;
wenzelm@25497
    93
    val n = length vs;
wenzelm@25497
    94
    val T = Type (name, map (fn v => TFree (v, [])) vs);
wenzelm@25497
    95
  in
wenzelm@25497
    96
    thy
wenzelm@35129
    97
    |> Sign.add_types [(b, n, mx)]
wenzelm@25497
    98
    |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
wenzelm@25497
    99
    |> pair T
wenzelm@25497
   100
  end;
wenzelm@25497
   101
wenzelm@25497
   102
wenzelm@18825
   103
(* add judgment *)
wenzelm@11897
   104
wenzelm@11897
   105
local
wenzelm@11897
   106
wenzelm@30344
   107
fun gen_add_judgment add_consts (b, T, mx) thy =
wenzelm@35129
   108
  let val c = Sign.full_name thy b in
skalberg@14226
   109
    thy
wenzelm@30344
   110
    |> add_consts [(b, T, mx)]
wenzelm@25018
   111
    |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
wenzelm@25497
   112
    |> map_data (fn (base_sort, judgment, atomize_rulify) =>
wenzelm@25497
   113
        if is_some judgment then error "Attempt to redeclare object-logic judgment"
wenzelm@25497
   114
        else (base_sort, SOME c, atomize_rulify))
skalberg@14226
   115
  end;
wenzelm@11897
   116
wenzelm@11897
   117
in
wenzelm@11897
   118
wenzelm@30344
   119
val add_judgment = gen_add_judgment Sign.add_consts_i;
wenzelm@30344
   120
val add_judgment_cmd = gen_add_judgment Sign.add_consts;
wenzelm@11897
   121
wenzelm@11897
   122
end;
wenzelm@11897
   123
wenzelm@11897
   124
wenzelm@23566
   125
(* judgments *)
wenzelm@11897
   126
wenzelm@16449
   127
fun judgment_name thy =
wenzelm@25497
   128
  (case #judgment (get_data thy) of
wenzelm@25497
   129
    SOME name => name
wenzelm@11897
   130
  | _ => raise TERM ("Unknown object-logic judgment", []));
wenzelm@11897
   131
wenzelm@16449
   132
fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
wenzelm@11897
   133
  | is_judgment _ _ = false;
wenzelm@11897
   134
wenzelm@16449
   135
fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
wenzelm@16449
   136
  | drop_judgment thy (tm as (Const (c, _) $ t)) =
wenzelm@16449
   137
      if (c = judgment_name thy handle TERM _ => false) then t else tm
wenzelm@11897
   138
  | drop_judgment _ tm = tm;
wenzelm@11897
   139
wenzelm@16449
   140
fun fixed_judgment thy x =
wenzelm@11897
   141
  let  (*be robust wrt. low-level errors*)
wenzelm@16449
   142
    val c = judgment_name thy;
wenzelm@24848
   143
    val aT = TFree (Name.aT, []);
wenzelm@11897
   144
    val T =
wenzelm@18939
   145
      the_default (aT --> propT) (Sign.const_type thy c)
wenzelm@11897
   146
      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
wenzelm@11897
   147
    val U = Term.domain_type T handle Match => aT;
wenzelm@11897
   148
  in Const (c, T) $ Free (x, U) end;
wenzelm@11897
   149
wenzelm@18121
   150
fun ensure_propT thy t =
wenzelm@13376
   151
  let val T = Term.fastype_of t
wenzelm@16449
   152
  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
wenzelm@13376
   153
wenzelm@23586
   154
fun dest_judgment ct =
wenzelm@23586
   155
  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
wenzelm@23586
   156
  then Thm.dest_arg ct
wenzelm@23586
   157
  else raise CTERM ("dest_judgment", [ct]);
wenzelm@23586
   158
wenzelm@23566
   159
fun judgment_conv cv ct =
wenzelm@23566
   160
  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
wenzelm@23566
   161
  then Conv.arg_conv cv ct
wenzelm@23566
   162
  else raise CTERM ("judgment_conv", [ct]);
wenzelm@23566
   163
wenzelm@11897
   164
wenzelm@19261
   165
(* elimination rules *)
wenzelm@19261
   166
wenzelm@19261
   167
fun is_elim rule =
wenzelm@19261
   168
  let
wenzelm@19261
   169
    val thy = Thm.theory_of_thm rule;
wenzelm@19261
   170
    val concl = Thm.concl_of rule;
wenzelm@19261
   171
  in
wenzelm@19261
   172
    Term.is_Var (drop_judgment thy concl) andalso
wenzelm@19261
   173
      exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
wenzelm@19261
   174
  end;
wenzelm@19261
   175
wenzelm@19261
   176
wenzelm@11897
   177
wenzelm@11897
   178
(** treatment of meta-level connectives **)
wenzelm@11897
   179
wenzelm@11897
   180
(* maintain rules *)
wenzelm@11897
   181
wenzelm@25497
   182
val get_atomize = #1 o #atomize_rulify o get_data;
wenzelm@25497
   183
val get_rulify = #2 o #atomize_rulify o get_data;
wenzelm@11897
   184
wenzelm@25497
   185
fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
wenzelm@25497
   186
  (base_sort, judgment, (Thm.add_thm th atomize, rulify)));
wenzelm@25497
   187
wenzelm@25497
   188
fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
wenzelm@25497
   189
  (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
wenzelm@11897
   190
wenzelm@22846
   191
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
wenzelm@22846
   192
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
wenzelm@22846
   193
wenzelm@28620
   194
val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
wenzelm@11897
   195
wenzelm@11897
   196
wenzelm@11897
   197
(* atomize *)
wenzelm@11897
   198
wenzelm@16449
   199
fun atomize_term thy =
wenzelm@16449
   200
  drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
wenzelm@12729
   201
wenzelm@23602
   202
fun atomize ct =
wenzelm@23602
   203
  MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
paulson@14743
   204
wenzelm@23602
   205
fun atomize_prems ct =
wenzelm@23602
   206
  if Logic.has_meta_prems (Thm.term_of ct) then
wenzelm@26568
   207
    Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
wenzelm@24832
   208
      (ProofContext.init (Thm.theory_of_cterm ct)) ct
wenzelm@23602
   209
  else Conv.all_conv ct;
wenzelm@11897
   210
wenzelm@23602
   211
val atomize_prems_tac = CONVERSION atomize_prems;
wenzelm@23602
   212
val full_atomize_tac = CONVERSION atomize;
wenzelm@11897
   213
wenzelm@11897
   214
wenzelm@11897
   215
(* rulify *)
wenzelm@11897
   216
wenzelm@18807
   217
fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
wenzelm@23540
   218
fun rulify_tac i st = MetaSimplifier.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
wenzelm@18807
   219
wenzelm@11897
   220
fun gen_rulify full thm =
wenzelm@21708
   221
  MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
wenzelm@20912
   222
  |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
wenzelm@11897
   223
wenzelm@11897
   224
val rulify = gen_rulify true;
wenzelm@11897
   225
val rulify_no_asm = gen_rulify false;
wenzelm@11897
   226
wenzelm@18728
   227
fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
wenzelm@18728
   228
fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
wenzelm@11897
   229
wenzelm@11897
   230
end;