src/HOL/Tools/reflection.ML

make reification part of HOL

(*  Title:      HOL/Tools/reflection.ML
    Author:     Amine Chaieb, TU Muenchen

A trial for automatical reflection with user-space declarations.
*)

signature REFLECTION =
sig
  val reflect: Proof.context -> thm list -> thm list -> conv
  val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
  val reflect_with_eval: Proof.context -> thm list -> thm list -> conv -> conv
  val reflection_with_eval_tac: Proof.context -> thm list -> thm list -> conv -> term option -> int -> tactic
  val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
  val add_reification_eq: attribute
  val del_reification_eq: attribute
  val add_correctness_thm: attribute
  val del_correctness_thm: attribute
  val default_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
  val default_reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
end;

structure Reflection : REFLECTION =
struct

fun subst_correctness corr_thms ct =
  Conv.rewrs_conv (map (Thm.symmetric o mk_eq) corr_thms) ct
    handle CTERM _ => error "No suitable correctness theorem found";

fun reflect ctxt corr_thms eqs =
  (Reification.conv ctxt eqs) then_conv (subst_correctness corr_thms)

fun reflection_tac ctxt corr_thms eqs =
  Reification.lift_conv ctxt (reflect ctxt corr_thms eqs);

fun first_arg_conv conv =
  let
    fun conv' ct =
      if can Thm.dest_comb (fst (Thm.dest_comb ct))
      then Conv.combination_conv conv' Conv.all_conv ct
      else Conv.combination_conv Conv.all_conv conv ct;
  in conv' end;

fun reflect_with_eval ctxt corr_thms eqs conv =
  (reflect ctxt corr_thms eqs) then_conv (first_arg_conv conv) then_conv (Reification.dereify ctxt eqs);

fun reflection_with_eval_tac ctxt corr_thms eqs conv =
  Reification.lift_conv ctxt (reflect_with_eval ctxt corr_thms eqs conv);

structure Data = Generic_Data
(
  type T = thm list * thm list;
  val empty = ([], []);
  val extend = I;
  fun merge ((ths1, rths1), (ths2, rths2)) =
    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
);

fun get_default ctxt =
  let
    val (reification_eqs, correctness_thms) = Data.get (Context.Proof ctxt);
  in { reification_eqs = reification_eqs, correctness_thms = correctness_thms } end;

val add_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
val del_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);

val _ = Context.>> (Context.map_theory
  (Attrib.setup @{binding reify}
    (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
  Attrib.setup @{binding reflection}
    (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));

fun default_reify_tac ctxt user_eqs =
  let
    val { reification_eqs = default_eqs, correctness_thms = _ } =
      get_default ctxt;
    val eqs = fold Thm.add_thm user_eqs default_eqs;
  in Reification.tac ctxt eqs end;

fun default_reflection_tac ctxt user_thms user_eqs =
  let
    val { reification_eqs = default_eqs, correctness_thms = default_thms } =
      get_default ctxt;
    val corr_thms = fold Thm.add_thm user_thms default_thms;
    val eqs = fold Thm.add_thm user_eqs default_eqs; 
  in reflection_tac ctxt corr_thms eqs end;

end;