src/Pure/Isar/object_logic.ML
author wenzelm
Tue Jun 01 12:33:50 2004 +0200 (2004-06-01)
changeset 14854 61bdf2ae4dc5
parent 14743 81001d6cb8c0
child 14981 e73f8140af78
permissions -rw-r--r--
removed obsolete sort 'logic';
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
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@11897
     5
wenzelm@11897
     6
Specifics about common object-logics.
wenzelm@11897
     7
*)
wenzelm@11897
     8
wenzelm@11897
     9
signature OBJECT_LOGIC =
wenzelm@11897
    10
sig
wenzelm@11897
    11
  val add_judgment: bstring * string * mixfix -> theory -> theory
wenzelm@11897
    12
  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
wenzelm@11897
    13
  val judgment_name: Sign.sg -> string
wenzelm@11897
    14
  val is_judgment: Sign.sg -> term -> bool
wenzelm@11897
    15
  val drop_judgment: Sign.sg -> term -> term
wenzelm@11897
    16
  val fixed_judgment: Sign.sg -> string -> term
wenzelm@13376
    17
  val assert_propT: Sign.sg -> term -> term
wenzelm@11897
    18
  val declare_atomize: theory attribute
wenzelm@11897
    19
  val declare_rulify: theory attribute
wenzelm@12807
    20
  val atomize_term: Sign.sg -> term -> term
paulson@14743
    21
  val atomize_thm: thm -> thm
wenzelm@13376
    22
  val atomize_rule: Sign.sg -> cterm -> 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@11897
    26
  val rulify: thm -> thm
wenzelm@11897
    27
  val rulify_no_asm: thm -> thm
wenzelm@11897
    28
  val rule_format: 'a attribute
wenzelm@11897
    29
  val rule_format_no_asm: 'a attribute
wenzelm@11897
    30
  val setup: (theory -> theory) list
wenzelm@11897
    31
end;
wenzelm@11897
    32
wenzelm@11897
    33
structure ObjectLogic: OBJECT_LOGIC =
wenzelm@11897
    34
struct
wenzelm@11897
    35
wenzelm@11897
    36
wenzelm@11897
    37
(** object-logic theory data **)
wenzelm@11897
    38
wenzelm@11897
    39
(* data kind 'Pure/object-logic' *)
wenzelm@11897
    40
wenzelm@11897
    41
structure ObjectLogicDataArgs =
wenzelm@11897
    42
struct
wenzelm@11897
    43
  val name = "Pure/object-logic";
wenzelm@11897
    44
  type T = string option * (thm list * thm list);
wenzelm@11897
    45
wenzelm@11897
    46
  val empty = (None, ([], [Drule.norm_hhf_eq]));
wenzelm@11897
    47
  val copy = I;
wenzelm@11897
    48
  val prep_ext = I;
wenzelm@11897
    49
wenzelm@11897
    50
  fun merge_judgment (Some x, Some y) =
wenzelm@11897
    51
        if x = y then Some x else error "Attempt to merge different object-logics"
wenzelm@11897
    52
    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
wenzelm@11897
    53
wenzelm@11897
    54
  fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
wenzelm@11897
    55
    (merge_judgment (judgment1, judgment2),
wenzelm@11897
    56
      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
wenzelm@11897
    57
wenzelm@11897
    58
  fun print _ _ = ();
wenzelm@11897
    59
end;
wenzelm@11897
    60
wenzelm@11897
    61
structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
wenzelm@11897
    62
wenzelm@11897
    63
wenzelm@11897
    64
(** generic treatment of judgments -- with a single argument only **)
wenzelm@11897
    65
wenzelm@11897
    66
(* add_judgment(_i) *)
wenzelm@11897
    67
wenzelm@11897
    68
local
wenzelm@11897
    69
wenzelm@11897
    70
fun new_judgment name (None, rules) = (Some name, rules)
wenzelm@11897
    71
  | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment";
wenzelm@11897
    72
skalberg@14226
    73
fun add_final name thy =
skalberg@14226
    74
  let
skalberg@14226
    75
    val typ = case Sign.const_type (sign_of thy) name of
skalberg@14226
    76
		Some T => T
skalberg@14226
    77
	      | None => error "Internal error in ObjectLogic.gen_add_judgment";
skalberg@14226
    78
  in
skalberg@14226
    79
    Theory.add_finals_i false [Const(name,typ)] thy
skalberg@14226
    80
  end;
skalberg@14226
    81
wenzelm@11897
    82
fun gen_add_judgment add_consts (name, T, syn) thy =
skalberg@14226
    83
  let
skalberg@14226
    84
    val fullname = Sign.full_name (Theory.sign_of thy) name;
skalberg@14226
    85
  in
skalberg@14226
    86
    thy
skalberg@14226
    87
    |> add_consts [(name, T, syn)]
skalberg@14226
    88
    |> add_final fullname
skalberg@14226
    89
    |> ObjectLogicData.map (new_judgment fullname)
skalberg@14226
    90
  end;
wenzelm@11897
    91
wenzelm@11897
    92
in
wenzelm@11897
    93
wenzelm@11897
    94
val add_judgment = gen_add_judgment Theory.add_consts;
wenzelm@11897
    95
val add_judgment_i = gen_add_judgment Theory.add_consts_i;
wenzelm@11897
    96
wenzelm@11897
    97
end;
wenzelm@11897
    98
wenzelm@11897
    99
wenzelm@11897
   100
(* term operations *)
wenzelm@11897
   101
wenzelm@11897
   102
fun judgment_name sg =
wenzelm@11897
   103
  (case ObjectLogicData.get_sg sg of
wenzelm@11897
   104
    (Some name, _) => name
wenzelm@11897
   105
  | _ => raise TERM ("Unknown object-logic judgment", []));
wenzelm@11897
   106
wenzelm@11897
   107
fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg
wenzelm@11897
   108
  | is_judgment _ _ = false;
wenzelm@11897
   109
wenzelm@11897
   110
fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
wenzelm@12479
   111
  | drop_judgment sg (tm as (Const (c, _) $ t)) =
wenzelm@12479
   112
      if (c = judgment_name sg handle TERM _ => false) then t else tm
wenzelm@11897
   113
  | drop_judgment _ tm = tm;
wenzelm@11897
   114
wenzelm@11897
   115
fun fixed_judgment sg x =
wenzelm@11897
   116
  let  (*be robust wrt. low-level errors*)
wenzelm@11897
   117
    val c = judgment_name sg;
wenzelm@14854
   118
    val aT = TFree ("'a", []);
wenzelm@11897
   119
    val T =
wenzelm@11897
   120
      if_none (Sign.const_type sg c) (aT --> propT)
wenzelm@11897
   121
      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
wenzelm@11897
   122
    val U = Term.domain_type T handle Match => aT;
wenzelm@11897
   123
  in Const (c, T) $ Free (x, U) end;
wenzelm@11897
   124
wenzelm@13376
   125
fun assert_propT sg t =
wenzelm@13376
   126
  let val T = Term.fastype_of t
wenzelm@13376
   127
  in if T = propT then t else Const (judgment_name sg, T --> propT) $ t end;
wenzelm@13376
   128
wenzelm@11897
   129
wenzelm@11897
   130
wenzelm@11897
   131
(** treatment of meta-level connectives **)
wenzelm@11897
   132
wenzelm@11897
   133
(* maintain rules *)
wenzelm@11897
   134
wenzelm@11897
   135
val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
wenzelm@11897
   136
val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
wenzelm@11897
   137
wenzelm@12371
   138
val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
wenzelm@12371
   139
val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
wenzelm@11897
   140
wenzelm@12371
   141
fun declare_atomize (thy, th) = (add_atomize th thy, th);
wenzelm@12371
   142
fun declare_rulify (thy, th) = (add_rulify th thy, th);
wenzelm@11897
   143
wenzelm@11897
   144
wenzelm@11897
   145
(* atomize *)
wenzelm@11897
   146
wenzelm@11897
   147
fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
wenzelm@11897
   148
  (MetaSimplifier.goals_conv (Library.equal i)
wenzelm@11897
   149
    (MetaSimplifier.forall_conv
wenzelm@11897
   150
      (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
wenzelm@11897
   151
wenzelm@12807
   152
fun atomize_term sg =
berghofe@13197
   153
  drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) [];
wenzelm@12729
   154
wenzelm@13376
   155
fun atomize_rule sg = Tactic.rewrite true (get_atomize sg);
wenzelm@13376
   156
paulson@14743
   157
(*Convert a natural-deduction rule into a formula (probably in FOL)*)
paulson@14743
   158
fun atomize_thm th =
paulson@14743
   159
  rewrite_rule  (get_atomize (Thm.sign_of_thm th)) th;
paulson@14743
   160
wenzelm@11897
   161
fun atomize_tac i st =
wenzelm@12807
   162
  if Logic.has_meta_prems (Thm.prop_of st) i then
wenzelm@11897
   163
    (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
wenzelm@11897
   164
  else all_tac st;
wenzelm@11897
   165
wenzelm@12829
   166
fun full_atomize_tac i st =
wenzelm@12829
   167
  rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st;
wenzelm@12829
   168
wenzelm@11897
   169
fun atomize_goal i st =
wenzelm@11897
   170
  (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
wenzelm@11897
   171
wenzelm@11897
   172
wenzelm@11897
   173
(* rulify *)
wenzelm@11897
   174
wenzelm@11897
   175
fun gen_rulify full thm =
wenzelm@11897
   176
  Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
wenzelm@12725
   177
  |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
wenzelm@11897
   178
wenzelm@11897
   179
val rulify = gen_rulify true;
wenzelm@11897
   180
val rulify_no_asm = gen_rulify false;
wenzelm@11897
   181
wenzelm@11897
   182
fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
wenzelm@11897
   183
fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
wenzelm@11897
   184
wenzelm@11897
   185
wenzelm@11897
   186
wenzelm@11897
   187
(** theory setup **)
wenzelm@11897
   188
wenzelm@11897
   189
val setup = [ObjectLogicData.init];
wenzelm@11897
   190
wenzelm@11897
   191
wenzelm@11897
   192
end;