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