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