src/Pure/Isar/object_logic.ML
author wenzelm
Thu Oct 04 20:29:24 2007 +0200 (2007-10-04)
changeset 24848 5dbbd33c3236
parent 24832 64cd13299d39
child 25018 fac2ceba75b4
permissions -rw-r--r--
replaced literal 'a by Name.aT;
     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 dest_judgment: cterm -> cterm
    18   val judgment_conv: conv -> conv
    19   val is_elim: thm -> bool
    20   val declare_atomize: attribute
    21   val declare_rulify: attribute
    22   val atomize_term: theory -> term -> term
    23   val atomize: conv
    24   val atomize_prems: conv
    25   val atomize_prems_tac: int -> tactic
    26   val full_atomize_tac: int -> tactic
    27   val rulify_term: theory -> term -> term
    28   val rulify_tac: int -> tactic
    29   val rulify: thm -> thm
    30   val rulify_no_asm: thm -> thm
    31   val rule_format: attribute
    32   val rule_format_no_asm: attribute
    33 end;
    34 
    35 structure ObjectLogic: OBJECT_LOGIC =
    36 struct
    37 
    38 
    39 (** theory data **)
    40 
    41 structure ObjectLogicData = TheoryDataFun
    42 (
    43   type T = string option * (thm list * thm list);
    44   val empty = (NONE, ([], []));
    45   val copy = I;
    46   val extend = I;
    47 
    48   fun merge_judgment (SOME x, SOME y) =
    49         if (x: string) = 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       (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
    55 );
    56 
    57 
    58 
    59 (** generic treatment of judgments -- with a single argument only **)
    60 
    61 (* add judgment *)
    62 
    63 local
    64 
    65 fun new_judgment name (NONE, rules) = (SOME name, rules)
    66   | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment";
    67 
    68 fun gen_add_judgment add_consts (bname, T, mx) thy =
    69   let val c = Sign.full_name thy (Syntax.const_name bname mx) in
    70     thy
    71     |> add_consts [(bname, T, mx)]
    72     |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy')
    73     |> ObjectLogicData.map (new_judgment c)
    74   end;
    75 
    76 in
    77 
    78 val add_judgment = gen_add_judgment Sign.add_consts;
    79 val add_judgment_i = gen_add_judgment Sign.add_consts_i;
    80 
    81 end;
    82 
    83 
    84 (* judgments *)
    85 
    86 fun judgment_name thy =
    87   (case ObjectLogicData.get thy of
    88     (SOME name, _) => name
    89   | _ => raise TERM ("Unknown object-logic judgment", []));
    90 
    91 fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
    92   | is_judgment _ _ = false;
    93 
    94 fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
    95   | drop_judgment thy (tm as (Const (c, _) $ t)) =
    96       if (c = judgment_name thy handle TERM _ => false) then t else tm
    97   | drop_judgment _ tm = tm;
    98 
    99 fun fixed_judgment thy x =
   100   let  (*be robust wrt. low-level errors*)
   101     val c = judgment_name thy;
   102     val aT = TFree (Name.aT, []);
   103     val T =
   104       the_default (aT --> propT) (Sign.const_type thy c)
   105       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
   106     val U = Term.domain_type T handle Match => aT;
   107   in Const (c, T) $ Free (x, U) end;
   108 
   109 fun ensure_propT thy t =
   110   let val T = Term.fastype_of t
   111   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
   112 
   113 fun dest_judgment ct =
   114   if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
   115   then Thm.dest_arg ct
   116   else raise CTERM ("dest_judgment", [ct]);
   117 
   118 fun judgment_conv cv ct =
   119   if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
   120   then Conv.arg_conv cv ct
   121   else raise CTERM ("judgment_conv", [ct]);
   122 
   123 
   124 (* elimination rules *)
   125 
   126 fun is_elim rule =
   127   let
   128     val thy = Thm.theory_of_thm rule;
   129     val concl = Thm.concl_of rule;
   130   in
   131     Term.is_Var (drop_judgment thy concl) andalso
   132       exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
   133   end;
   134 
   135 
   136 
   137 (** treatment of meta-level connectives **)
   138 
   139 (* maintain rules *)
   140 
   141 val get_atomize = #1 o #2 o ObjectLogicData.get;
   142 val get_rulify = #2 o #2 o ObjectLogicData.get;
   143 
   144 val add_atomize = ObjectLogicData.map o apsnd o apfst o Thm.add_thm;
   145 val add_rulify = ObjectLogicData.map o apsnd o apsnd o Thm.add_thm;
   146 
   147 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
   148 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
   149 
   150 val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
   151 
   152 
   153 (* atomize *)
   154 
   155 fun atomize_term thy =
   156   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
   157 
   158 fun atomize ct =
   159   MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   160 
   161 fun atomize_prems ct =
   162   if Logic.has_meta_prems (Thm.term_of ct) then
   163     Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize))
   164       (ProofContext.init (Thm.theory_of_cterm ct)) ct
   165   else Conv.all_conv ct;
   166 
   167 val atomize_prems_tac = CONVERSION atomize_prems;
   168 val full_atomize_tac = CONVERSION atomize;
   169 
   170 
   171 (* rulify *)
   172 
   173 fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
   174 fun rulify_tac i st = MetaSimplifier.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   175 
   176 fun gen_rulify full thm =
   177   MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   178   |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
   179 
   180 val rulify = gen_rulify true;
   181 val rulify_no_asm = gen_rulify false;
   182 
   183 fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
   184 fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
   185 
   186 end;