src/Pure/Isar/object_logic.ML
author wenzelm
Fri Nov 09 00:19:20 2001 +0100 (2001-11-09)
changeset 12123 739eba13e2cd
parent 11897 b9f2028f53bd
child 12311 ce5f9e61c037
permissions -rw-r--r--
theory data: finish method;
     1 (*  Title:      Pure/Isar/object_logic.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Specifics about common object-logics.
     7 *)
     8 
     9 signature OBJECT_LOGIC =
    10 sig
    11   val add_judgment: bstring * string * mixfix -> theory -> theory
    12   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
    13   val judgment_name: Sign.sg -> string
    14   val is_judgment: Sign.sg -> term -> bool
    15   val drop_judgment: Sign.sg -> term -> term
    16   val fixed_judgment: Sign.sg -> string -> term
    17   val declare_atomize: theory attribute
    18   val declare_rulify: theory attribute
    19   val atomize_tac: int -> tactic
    20   val atomize_goal: int -> thm -> thm
    21   val rulify: thm -> thm
    22   val rulify_no_asm: thm -> thm
    23   val rule_format: 'a attribute
    24   val rule_format_no_asm: 'a attribute
    25   val setup: (theory -> theory) list
    26 end;
    27 
    28 structure ObjectLogic: OBJECT_LOGIC =
    29 struct
    30 
    31 
    32 (** object-logic theory data **)
    33 
    34 (* data kind 'Pure/object-logic' *)
    35 
    36 structure ObjectLogicDataArgs =
    37 struct
    38   val name = "Pure/object-logic";
    39   type T = string option * (thm list * thm list);
    40 
    41   val empty = (None, ([], [Drule.norm_hhf_eq]));
    42   val copy = I;
    43   val finish = I;
    44   val prep_ext = I;
    45 
    46   fun merge_judgment (Some x, Some y) =
    47         if x = y then Some x else error "Attempt to merge different object-logics"
    48     | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
    49 
    50   fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    51     (merge_judgment (judgment1, judgment2),
    52       (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
    53 
    54   fun print _ _ = ();
    55 end;
    56 
    57 structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
    58 
    59 
    60 (** generic treatment of judgments -- with a single argument only **)
    61 
    62 (* add_judgment(_i) *)
    63 
    64 local
    65 
    66 fun new_judgment name (None, rules) = (Some name, rules)
    67   | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment";
    68 
    69 fun gen_add_judgment add_consts (name, T, syn) thy =
    70   thy
    71   |> add_consts [(name, T, syn)]
    72   |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name));
    73 
    74 in
    75 
    76 val add_judgment = gen_add_judgment Theory.add_consts;
    77 val add_judgment_i = gen_add_judgment Theory.add_consts_i;
    78 
    79 end;
    80 
    81 
    82 (* term operations *)
    83 
    84 fun judgment_name sg =
    85   (case ObjectLogicData.get_sg sg of
    86     (Some name, _) => name
    87   | _ => raise TERM ("Unknown object-logic judgment", []));
    88 
    89 fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg
    90   | is_judgment _ _ = false;
    91 
    92 fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
    93   | drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm
    94   | drop_judgment _ tm = tm;
    95 
    96 fun fixed_judgment sg x =
    97   let  (*be robust wrt. low-level errors*)
    98     val c = judgment_name sg;
    99     val aT = TFree ("'a", logicS);
   100     val T =
   101       if_none (Sign.const_type sg c) (aT --> propT)
   102       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
   103     val U = Term.domain_type T handle Match => aT;
   104   in Const (c, T) $ Free (x, U) end;
   105 
   106 
   107 
   108 (** treatment of meta-level connectives **)
   109 
   110 (* maintain rules *)
   111 
   112 val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
   113 val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
   114 
   115 val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
   116 val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
   117 
   118 fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
   119 fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
   120 
   121 
   122 (* atomize *)
   123 
   124 fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
   125   (MetaSimplifier.goals_conv (Library.equal i)
   126     (MetaSimplifier.forall_conv
   127       (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
   128 
   129 fun atomize_tac i st =
   130   if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
   131     (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
   132   else all_tac st;
   133 
   134 fun atomize_goal i st =
   135   (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
   136 
   137 
   138 (* rulify *)
   139 
   140 fun gen_rulify full thm =
   141   Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
   142   |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
   143 
   144 val rulify = gen_rulify true;
   145 val rulify_no_asm = gen_rulify false;
   146 
   147 fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
   148 fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   149 
   150 
   151 
   152 (** theory setup **)
   153 
   154 val setup = [ObjectLogicData.init];
   155 
   156 
   157 end;