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