(*  Title:      nominal_thmdecls.ML
    Author:     Christian Urban

  Infrastructure for the lemma collection "eqvts".

  Provides the attributes [eqvt] and [eqvt_raw], 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) ...    (1)

  or

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

  and it is stored in the form

    p o c == c

  The [eqvt_raw] attribute just adds the theorem to eqvts_raw.

  TODO: In case of the form in (2) one should also
        add the equational form to eqvts
*)

signature NOMINAL_THMDECLS =
sig
  val eqvt_add: attribute
  val eqvt_del: attribute
  val eqvt_raw_add: attribute
  val eqvt_raw_del: attribute
  val setup: theory -> theory
  val get_eqvts_thms: Proof.context -> thm list
  val get_eqvts_raw_thms: Proof.context -> thm list
  val eqvt_transform: Proof.context -> thm -> thm

  (* TEMPORARY FIX *)
  val add_thm: thm -> Context.generic -> Context.generic
  val add_raw_thm: thm -> Context.generic -> Context.generic
end;

structure Nominal_ThmDecls: NOMINAL_THMDECLS =
struct

fun get_ps trm =
  case trm of 
     Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm])
   | Const (@{const_name permute}, _) $ p $ _ => [p]
   | t $ u => get_ps t @ get_ps u
   | Abs (_, _, t) => get_ps t 
   | _ => []

fun put_p p trm =
  case trm of 
     Bound _ => trm
   | Const _ => trm
   | t $ u => put_p p t $ put_p p u
   | Abs (x, ty, t) => Abs (x, ty, put_p p t)
   | _ => mk_perm p trm

(* tests whether the lists of ps all agree, and that there is at least one p *)
fun is_bad_list [] = true
  | is_bad_list [_] = false
  | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true


structure EqvtData = Generic_Data
( type T = thm Item_Net.T;
  val empty = Thm.full_rules;
  val extend = I;
  val merge = Item_Net.merge );

structure EqvtRawData = Generic_Data
( type T = thm Item_Net.T;
  val empty = Thm.full_rules;
  val extend = I;
  val merge = Item_Net.merge );

val eqvts = Item_Net.content o EqvtData.get;
val eqvts_raw = Item_Net.content o EqvtRawData.get;

val get_eqvts_thms = eqvts o  Context.Proof;
val get_eqvts_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;

fun add_raw_thm thm = 
  case prop_of thm of
    Const ("==", _) $ _ $ _ => 
      EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
  | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 

val del_raw_thm = EqvtRawData.map o Item_Net.remove;


(** transformation of eqvt lemmas **)


(* transforms equations into the "p o c = c"-form 
   from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)

fun eqvt_transform_eq_tac thm = 
let
  val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
in
  REPEAT o FIRST' 
    [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),
     rtac (thm RS @{thm trans}),
     rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
end

fun eqvt_transform_eq ctxt thm = 
let
  val ((p, t), rhs) = apfst dest_perm 
    (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))
    handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c...  = c..."
  val ps = get_ps rhs handle TERM _ => []  
  val (c, c') = (head_of t, head_of rhs)
in
  if c <> c' 
    then error "Eqvt lemma is not of the right form (constants do not agree)"
  else if is_bad_list (p::ps)  
    then error "Eqvt lemma is not of the right form (permutations do not agree)" 
  else if not (rhs aconv (put_p p t))
    then error "Eqvt lemma is not of the right form (arguments do not agree)"
  else if is_Const t 
    then safe_mk_equiv thm
  else 
    let 
      val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
      val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
    in
      Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
      |> singleton (ProofContext.export ctxt' ctxt)
      |> safe_mk_equiv
    end
end

(* transforms equations into the "p o c = c"-form 
   from R x1 ...xn ==> R (p o x1) ... (p o xn) *)

fun eqvt_transform_imp_tac thy p p' thm = 
let
  val cp = Thm.cterm_of thy p
  val cp' = Thm.cterm_of thy (mk_minus p')
  val thm' = Drule.cterm_instantiate [(cp, cp')] thm
  val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)}
in
  EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac,
    rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]
end

fun eqvt_transform_imp ctxt thm =
let
  val thy = ProofContext.theory_of ctxt
  val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
  val (c, c') = (head_of prem, head_of concl)
  val ps = get_ps concl handle TERM _ => []  
  val p = try hd ps
in
  if c <> c' 
    then error "Eqvt lemma is not of the right form (constants do not agree)"
  else if is_bad_list ps  
    then error "Eqvt lemma is not of the right form (permutations do not agree)" 
  else if not (concl aconv (put_p (the p) prem)) 
    then error "Eqvt lemma is not of the right form (arguments do not agree)"
  else 
    let
      val prem' = mk_perm (the p) prem    
      val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))
      val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
    in
      Goal.prove ctxt' [] [] goal'
        (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) 
      |> singleton (ProofContext.export ctxt' ctxt)
      |> eqvt_transform_eq ctxt
    end
end     

fun eqvt_transform ctxt thm = 
 case (prop_of thm) of
   @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ 
     (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => 
       eqvt_transform_eq ctxt thm
 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 
     eqvt_transform_imp ctxt thm
 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
 

(** attributes **)

val eqvt_add = Thm.declaration_attribute 
  (fn thm => fn context =>
   let
     val thm' = eqvt_transform (Context.proof_of context) thm
   in
     context |> add_thm thm |> add_raw_thm thm'
   end)

val eqvt_del = Thm.declaration_attribute
  (fn thm => fn context =>
   let
     val thm' = eqvt_transform (Context.proof_of context) thm
   in
     context |> del_thm thm |> del_raw_thm thm'
   end)

val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;


(** setup function **)

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_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_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;