(*  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 is_equiv (Const ("==", _) $ _ $ _) = true

  | is_equiv _ = false

fun add_raw_thm thm = 

  case prop_of thm of

    Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)

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

val del_raw_thm = EqvtRawData.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 eq_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 "p o c = c"-form *)

fun transform_eq ctxt thm = 

let

  val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))

  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 _ => eq_transform_tac thm 1)

end

(* tests whether the lists of pis 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

fun mk_minus p = 

 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p   

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 (c, prem_args) = strip_comb prem

  val (c', concl_args) = strip_comb concl

  val ps = map (fst o dest_perm) concl_args 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 concl_args <> map (mk_perm (the p)) prem_args 

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

  else 

    let

      val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (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 _ => imp_transform_tac thy (the p) p' thm 1) 

      |> singleton (ProofContext.export ctxt' ctxt)

      |> transform_eq ctxt

    end

end     

fun mk_equiv r = r RS @{thm eq_reflection};

fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;

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;