(*  Title:      nominal_thmdecls.ML
    Author:     Christian Urban

  Infrastructure for the lemma collection "eqvts".

  Provides the attributes [eqvt] and [eqvt_force], and the theorem
  lists eqvts and eqvts_raw. The first attribute will store the theorem
  in the eqvts list and also in the eqvts_raw list. For the latter 
  the theorem is expected to be of the form

    p o (c x1 x2 ...) = c (p o x1) (p o x2) ...

  and is stored in the form

    p o c == c

  The [eqvt_force] attribute just adds the theorem to eqvts.

  TODO:

   - deal with eqvt-lemmas of the form 

       c x1 x2 ... ==> c (p o x1) (p o x2) ..
*)

signature NOMINAL_THMDECLS =
sig
  val eqvt_add: attribute
  val eqvt_del: attribute
  val eqvt_force_add: attribute
  val eqvt_force_del: attribute
  val setup: theory -> theory
  val get_eqvt_thms: Proof.context -> thm list
  val get_eqvt_raw_thms: Proof.context -> thm list

end;

structure Nominal_ThmDecls: NOMINAL_THMDECLS =
struct

structure EqvtData = Generic_Data
(
  type T = (thm * thm option) Item_Net.T;
  val empty = Item_Net.init (eq_fst Thm.eq_thm_prop) (single o Thm.full_prop_of o fst)
  val extend = I;
  val merge = Item_Net.merge;
);

val eqvts = (map fst) o Item_Net.content o EqvtData.get;
val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get;

val get_eqvt_thms = eqvts o Context.Proof; 
val get_eqvt_raw_thms = eqvts_raw o Context.Proof; 

val add_thm = EqvtData.map o Item_Net.update;
val del_thm = EqvtData.map o Item_Net.remove;

val add_force_thm = EqvtData.map o Item_Net.update;
val del_force_thm = EqvtData.map o Item_Net.remove;

fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
  | dest_perm t = raise TERM("dest_perm", [t])

fun mk_perm p trm =
let
  val ty = fastype_of trm
in
  Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
end

fun eqvt_transform_tac thm = REPEAT o FIRST' 
  [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),
   rtac (thm RS @{thm trans}),
   rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]

(* transform equations into the required form *)
fun transform_eq ctxt thm lhs rhs = 
let
  val (p, t) = dest_perm lhs
  val (c, args) = strip_comb t
  val (c', args') = strip_comb rhs 
  val eargs = map Envir.eta_contract args 
  val eargs' = map Envir.eta_contract args'
  val p_str = fst (fst (dest_Var p))
  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
in
  if c <> c' 
    then error "eqvt lemma is not of the right form (constants do not agree)"
  else if eargs' <> map (mk_perm p) eargs 
    then error "eqvt lemma is not of the right form (arguments do not agree)"
  else if args = [] 
    then thm
  else Goal.prove ctxt [p_str] [] goal
    (fn _ => eqvt_transform_tac thm 1)
end

fun transform addel_fn thm context = 
let
  val ctxt = Context.proof_of context
  val trm = HOLogic.dest_Trueprop (prop_of thm)
in
  case trm of
    Const (@{const_name "op ="}, _) $ lhs $ rhs =>
      let 
        val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
      in
        addel_fn (thm, SOME thm2) context
      end
  | _ => raise (error "only (op=) case implemented yet")
end 

val eqvt_add = Thm.declaration_attribute (transform add_thm);
val eqvt_del = Thm.declaration_attribute (transform del_thm);

val eqvt_force_add = Thm.declaration_attribute (add_force_thm o rpair NONE);
val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE);

val setup =
  Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
    (cat_lines ["declaration of equivariance lemmas - they will automtically be",  
       "brought into the form p o c = c"]) #>
  Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
    (cat_lines ["declaration of equivariance lemmas - no",
       "transformation is performed"]) #>
  PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
  PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);

end;