wenzelm@11897: (*  Title:      Pure/Isar/object_logic.ML
wenzelm@11897:     ID:         $Id$
wenzelm@11897:     Author:     Markus Wenzel, TU Muenchen
wenzelm@11897: 
wenzelm@11897: Specifics about common object-logics.
wenzelm@11897: *)
wenzelm@11897: 
wenzelm@11897: signature OBJECT_LOGIC =
wenzelm@11897: sig
wenzelm@11897:   val add_judgment: bstring * string * mixfix -> theory -> theory
wenzelm@11897:   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
wenzelm@16449:   val judgment_name: theory -> string
wenzelm@16449:   val is_judgment: theory -> term -> bool
wenzelm@16449:   val drop_judgment: theory -> term -> term
wenzelm@16449:   val fixed_judgment: theory -> string -> term
wenzelm@18121:   val ensure_propT: theory -> term -> term
wenzelm@19261:   val is_elim: thm -> bool
wenzelm@18728:   val declare_atomize: attribute
wenzelm@18728:   val declare_rulify: attribute
wenzelm@16449:   val atomize_term: theory -> term -> term
wenzelm@18783:   val atomize_cterm: cterm -> thm
paulson@14743:   val atomize_thm: thm -> thm
wenzelm@11897:   val atomize_tac: int -> tactic
wenzelm@12829:   val full_atomize_tac: int -> tactic
wenzelm@11897:   val atomize_goal: int -> thm -> thm
wenzelm@18807:   val rulify_term: theory -> term -> term
wenzelm@18807:   val rulify_tac: int -> tactic
wenzelm@11897:   val rulify: thm -> thm
wenzelm@11897:   val rulify_no_asm: thm -> thm
wenzelm@18728:   val rule_format: attribute
wenzelm@18728:   val rule_format_no_asm: attribute
wenzelm@11897: end;
wenzelm@11897: 
wenzelm@11897: structure ObjectLogic: OBJECT_LOGIC =
wenzelm@11897: struct
wenzelm@11897: 
wenzelm@11897: 
wenzelm@18825: (** theory data **)
wenzelm@11897: 
wenzelm@16449: structure ObjectLogicData = TheoryDataFun
wenzelm@22846: (
wenzelm@11897:   type T = string option * (thm list * thm list);
wenzelm@22846:   val empty = (NONE, ([], []));
wenzelm@11897:   val copy = I;
wenzelm@16449:   val extend = I;
wenzelm@11897: 
skalberg@15531:   fun merge_judgment (SOME x, SOME y) =
skalberg@15531:         if x = y then SOME x else error "Attempt to merge different object-logics"
wenzelm@15973:     | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
wenzelm@11897: 
wenzelm@16449:   fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
wenzelm@11897:     (merge_judgment (judgment1, judgment2),
wenzelm@11897:       (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
wenzelm@22846: );
wenzelm@15801: 
wenzelm@11897: 
wenzelm@11897: 
wenzelm@11897: (** generic treatment of judgments -- with a single argument only **)
wenzelm@11897: 
wenzelm@18825: (* add judgment *)
wenzelm@11897: 
wenzelm@11897: local
wenzelm@11897: 
skalberg@15531: fun new_judgment name (NONE, rules) = (SOME name, rules)
skalberg@15531:   | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment";
wenzelm@11897: 
wenzelm@16449: fun gen_add_judgment add_consts (bname, T, mx) thy =
wenzelm@16449:   let val c = Sign.full_name thy (Syntax.const_name bname mx) in
skalberg@14226:     thy
wenzelm@16449:     |> add_consts [(bname, T, mx)]
wenzelm@16449:     |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy')
wenzelm@16449:     |> ObjectLogicData.map (new_judgment c)
skalberg@14226:   end;
wenzelm@11897: 
wenzelm@11897: in
wenzelm@11897: 
wenzelm@22796: val add_judgment = gen_add_judgment Sign.add_consts;
wenzelm@22796: val add_judgment_i = gen_add_judgment Sign.add_consts_i;
wenzelm@11897: 
wenzelm@11897: end;
wenzelm@11897: 
wenzelm@11897: 
wenzelm@11897: (* term operations *)
wenzelm@11897: 
wenzelm@16449: fun judgment_name thy =
wenzelm@16449:   (case ObjectLogicData.get thy of
skalberg@15531:     (SOME name, _) => name
wenzelm@11897:   | _ => raise TERM ("Unknown object-logic judgment", []));
wenzelm@11897: 
wenzelm@16449: fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
wenzelm@11897:   | is_judgment _ _ = false;
wenzelm@11897: 
wenzelm@16449: fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
wenzelm@16449:   | drop_judgment thy (tm as (Const (c, _) $ t)) =
wenzelm@16449:       if (c = judgment_name thy handle TERM _ => false) then t else tm
wenzelm@11897:   | drop_judgment _ tm = tm;
wenzelm@11897: 
wenzelm@16449: fun fixed_judgment thy x =
wenzelm@11897:   let  (*be robust wrt. low-level errors*)
wenzelm@16449:     val c = judgment_name thy;
wenzelm@14854:     val aT = TFree ("'a", []);
wenzelm@11897:     val T =
wenzelm@18939:       the_default (aT --> propT) (Sign.const_type thy c)
wenzelm@11897:       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
wenzelm@11897:     val U = Term.domain_type T handle Match => aT;
wenzelm@11897:   in Const (c, T) $ Free (x, U) end;
wenzelm@11897: 
wenzelm@18121: fun ensure_propT thy t =
wenzelm@13376:   let val T = Term.fastype_of t
wenzelm@16449:   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
wenzelm@13376: 
wenzelm@11897: 
wenzelm@19261: (* elimination rules *)
wenzelm@19261: 
wenzelm@19261: fun is_elim rule =
wenzelm@19261:   let
wenzelm@19261:     val thy = Thm.theory_of_thm rule;
wenzelm@19261:     val concl = Thm.concl_of rule;
wenzelm@19261:   in
wenzelm@19261:     Term.is_Var (drop_judgment thy concl) andalso
wenzelm@19261:       exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
wenzelm@19261:   end;
wenzelm@19261: 
wenzelm@19261: 
wenzelm@11897: 
wenzelm@11897: (** treatment of meta-level connectives **)
wenzelm@11897: 
wenzelm@11897: (* maintain rules *)
wenzelm@11897: 
wenzelm@16449: val get_atomize = #1 o #2 o ObjectLogicData.get;
wenzelm@16449: val get_rulify = #2 o #2 o ObjectLogicData.get;
wenzelm@11897: 
wenzelm@22846: val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
wenzelm@22846: val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
wenzelm@11897: 
wenzelm@22846: val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
wenzelm@22846: val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
wenzelm@22846: 
wenzelm@22846: val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
wenzelm@11897: 
wenzelm@11897: 
wenzelm@11897: (* atomize *)
wenzelm@11897: 
wenzelm@22900: fun rewrite_prems_tac rews i = PRIMITIVE (Conv.fconv_rule
wenzelm@22900:   (Conv.goals_conv (Library.equal i)
wenzelm@22900:     (Conv.forall_conv ~1
wenzelm@22900:       (Conv.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
wenzelm@11897: 
wenzelm@16449: fun atomize_term thy =
wenzelm@16449:   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
wenzelm@12729: 
wenzelm@21708: fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
wenzelm@17902: fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
paulson@14743: 
wenzelm@11897: fun atomize_tac i st =
wenzelm@12807:   if Logic.has_meta_prems (Thm.prop_of st) i then
wenzelm@16449:     (rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st
wenzelm@11897:   else all_tac st;
wenzelm@11897: 
wenzelm@12829: fun full_atomize_tac i st =
wenzelm@21687:   Goal.rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
wenzelm@12829: 
wenzelm@11897: fun atomize_goal i st =
skalberg@15531:   (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
wenzelm@11897: 
wenzelm@11897: 
wenzelm@11897: (* rulify *)
wenzelm@11897: 
wenzelm@18807: fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
wenzelm@21687: fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
wenzelm@18807: 
wenzelm@11897: fun gen_rulify full thm =
wenzelm@21708:   MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
wenzelm@20912:   |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
wenzelm@11897: 
wenzelm@11897: val rulify = gen_rulify true;
wenzelm@11897: val rulify_no_asm = gen_rulify false;
wenzelm@11897: 
wenzelm@18728: fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
wenzelm@18728: fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
wenzelm@11897: 
wenzelm@11897: end;