(*  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

end;

structure Nominal_ThmDecls: NOMINAL_THMDECLS =

struct

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

  | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 

val del_raw_thm = EqvtRawData.map o Item_Net.remove;

(* transform equations into the "p o c = c"-form *)

fun transform_eq ctxt thm = 

let

in

  if c <> c' 

    then error "Eqvt lemma is not of the right form (constants do not agree)"

    then error "Eqvt lemma is not of the right form (arguments do not agree)"

    then thm

end

fun imp_transform_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 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 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)" 

    then error "Eqvt lemma is not of the right form (arguments do not agree)"

  else 

    let

      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 _ => imp_transform_tac thy (the p) p' thm 1) 

      |> singleton (ProofContext.export ctxt' ctxt)

      |> transform_eq ctxt

    end

end     

fun transform addel_fun thm context = 

let

  val ctxt = Context.proof_of context

in

  case (prop_of thm) of

    @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ 

      (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>

        addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context

  | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 

        addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context

  | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."

end 

val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));

val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));

val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;

val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;

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;