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