(*  Title:      nominal_thmdecls.ML

    Author:     Christian Urban

  Infrastructure for the lemma collection "eqvts".

  Provides the attributes [eqvt] and [eqvt_force], and the theorem

  list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be 

  stored are expected to be of the form

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

  and are transformed into the form

    p o c == c

  TODO

   - deal with eqvt-lemmas of the for 

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

structure Nominal_ThmDecls: NOMINAL_THMDECLS =

structure EqvtData = Generic_Data

  type T = thm Item_Net.T;

  val empty = Thm.full_rules;

  val extend = I;

  val merge = Item_Net.merge;

);

val content = Item_Net.content o EqvtData.get;

val get_eqvt_thms = content 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 =

  val ty = fastype_of trm

  Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm

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 => 

      addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context

  | _ => raise (error "no other cases yet implemented")

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;

val eqvt_force_del = Thm.declaration_attribute del_force_thm;

  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 - they will will be", 

                "added/deleted directly to the eqvt thm-list"]) #>

  PureThy.add_thms_dynamic (@{binding "eqvt"}, content);