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