(*  Title:      HOL/Nominal/nominal_thmdecls.ML

    Author:     Julien Narboux, TU Muenchen

    Author:     Christian Urban, TU Muenchen

Infrastructure for the lemma collection "eqvts".

By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in

a data-slot in the context. Possible modifiers are [... add] and

[... del] for adding and deleting, respectively, the lemma from the

data-slot.

*)

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

end;

structure NominalThmDecls: NOMINAL_THMDECLS =

struct

structure Data = Generic_Data

(

  type T = thm list

  val empty = []

  val extend = I

  val merge = Thm.merge_thms

)

(* Exception for when a theorem does not conform with form of an equivariance lemma. *)

(* There are two forms: one is an implication (for relations) and the other is an    *)

(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)

(* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)

(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)

(* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)

(* the implicational case it is also checked that the variables and permutation fit  *)

(* together, i.e. are of the right "pt_class", so that a stronger version of the     *)

(* equality-lemma can be derived. *)

exception EQVT_FORM of string

val perm_boolE =

  @{lemma "pi \<bullet> P ==> P" by (simp add: permute_bool_def)};

val perm_boolI =

  @{lemma "P ==> pi \<bullet> P" by (simp add: permute_bool_def)};

fun prove_eqvt_tac ctxt orig_thm pi pi' =

let

  val mypi = Thm.cterm_of ctxt pi

  val T = fastype_of pi'

  val mypifree = Thm.cterm_of ctxt (Const (@{const_name "uminus"}, T --> T) $ pi')

  val perm_pi_simp = @{thms permute_minus_cancel}

in

  EVERY1 [rtac @{thm iffI},

          dtac perm_boolE,

          etac orig_thm,

          dtac (Drule.cterm_instantiate [(mypi, mypifree)] orig_thm),

          rtac perm_boolI,

          full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)]

end;

fun get_derived_thm ctxt hyp concl orig_thm pi =

  let

    val thy = ProofContext.theory_of ctxt;

    val pi' = Var (pi, @{typ "perm"});

    val lhs = Const (@{const_name "permute"}, @{typ "perm"} --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;

    val ([goal_term, pi''], ctxt') = Variable.import_terms false

      [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt

  in

    Goal.prove ctxt' [] [] goal_term

      (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>

    singleton (ProofContext.export ctxt' ctxt)

  end

(* replaces in t every variable, say x, with pi o x *)

fun apply_pi trm pi =

let

  fun replace n ty =

  let 

    val c  = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) 

    val v1 = Var (pi, @{typ "perm"})

    val v2 = Var (n, ty)

  in

    c $ v1 $ v2 

  end

in

  map_aterms (fn Var (n, ty) => replace n ty | t => t) trm

end

(* returns *the* pi which is in front of all variables, provided there *)

(* exists such a pi; otherwise raises EQVT_FORM                        *)

fun get_pi t thy =

  let fun get_pi_aux s =

        (case s of

          (Const (@{const_name "permute"} ,typrm) $

             (Var (pi,_)) $

               (Var (n,ty))) =>

                if (Sign.of_sort thy (ty, @{sort pt}))

                then [pi]

                else raise

                EQVT_FORM ("Could not find any permutation or an argument is not an instance of pt")

        | Abs (_,_,t1) => get_pi_aux t1

        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2

        | _ => [])

  in

    (* collect first all pi's in front of variables in t and then use distinct *)

    (* to ensure that all pi's must have been the same, i.e. distinct returns  *)

    (* a singleton-list  *)

    (case (distinct (op =) (get_pi_aux t)) of

      [pi] => pi

    | [] => raise EQVT_FORM "No permutations found"

    | _ => raise EQVT_FORM "All permutation should be the same")

  end;

(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)

(* lemma list depending on flag. To be added the lemma has to satisfy a     *)

(* certain form. *)

fun eqvt_add_del_aux flag orig_thm context = 

  let

    val thy = Context.theory_of context

    val thms_to_be_added = (case (prop_of orig_thm) of

        (* case: eqvt-lemma is of the implicational form *)

        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>

          let

            val pi = get_pi concl thy

          in

             if (apply_pi hyp pi = concl)

             then

               (warning ("equivariance lemma of the relational form");

                [orig_thm,

                 get_derived_thm (Context.proof_of context) hyp concl orig_thm pi])

             else raise EQVT_FORM "Type Implication"

          end

       (* case: eqvt-lemma is of the equational form *)

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

            (Const (@{const_name "permute"},typrm) $ Var (pi, _) $ lhs) $ rhs)) =>

           (if (apply_pi lhs pi) = rhs

               then [orig_thm]

               else raise EQVT_FORM "Type Equality")

      | _ => raise EQVT_FORM "Type unknown")

  in

      fold (fn thm => Data.map (flag thm)) thms_to_be_added context

  end

  handle EQVT_FORM s =>

      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 

               " does not comply with the form of an equivariance lemma (" ^ s ^").")

val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));

val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));

val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);

val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);

val get_eqvt_thms = Context.Proof #> Data.get;

val setup =

    Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 

     "equivariance theorem declaration" 

 #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)

     "equivariance theorem declaration (without checking the form of the lemma)" 

 #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 

end;