1 (*  Title:      nominal_thmdecls.ML

     2     Author:     Christian Urban

     3 

     4   Infrastructure for the lemma collection "eqvts".

     5 

     6   Provides the attributes [eqvt] and [eqvt_raw], and the theorem

     7   lists eqvts and eqvts_raw. The first attribute will store the 

     8   theorem in the eqvts list and also in the eqvts_raw list. For 

     9   the latter the theorem is expected to be of the form

    10 

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

    12 

    13   and it is stored in the form

    14 

    15     p o c == c

    16 

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

    18 

    19   TODO:

    20 

    21    - deal with eqvt-lemmas of the form 

    22 

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

    24 *)

    25 

    26 signature NOMINAL_THMDECLS =

    27 sig

    28   val eqvt_add: attribute

    29   val eqvt_del: attribute

    30   val eqvt_raw_add: attribute

    31   val eqvt_raw_del: attribute

    32   val setup: theory -> theory

    33   val get_eqvts_thms: Proof.context -> thm list

    34   val get_eqvts_raw_thms: Proof.context -> thm list

    35 

    36 end;

    37 

    38 structure Nominal_ThmDecls: NOMINAL_THMDECLS =

    39 struct

    40 

    41 

    42 structure EqvtData = Generic_Data

    43 ( type T = thm Item_Net.T;

    44   val empty = Thm.full_rules;

    45   val extend = I;

    46   val merge = Item_Net.merge );

    47 

    48 structure EqvtRawData = Generic_Data

    49 ( type T = thm Item_Net.T;

    50   val empty = Thm.full_rules;

    51   val extend = I;

    52   val merge = Item_Net.merge );

    53 

    54 val eqvts = Item_Net.content o EqvtData.get;

    55 val eqvts_raw = Item_Net.content o EqvtRawData.get;

    56 

    57 val get_eqvts_thms = eqvts o Context.Proof; 

    58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; 

    59 

    60 val add_thm = EqvtData.map o Item_Net.update;

    61 val del_thm = EqvtData.map o Item_Net.remove;

    62 

    63 val add_raw_thm = EqvtRawData.map o Item_Net.update;

    64 val del_raw_thm = EqvtRawData.map o Item_Net.remove;

    65 

    66 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)

    67   | dest_perm t = raise TERM("dest_perm", [t])

    68 

    69 fun mk_perm p trm =

    70 let

    71   val ty = fastype_of trm

    72 in

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

    74 end

    75 

    76 fun eqvt_transform_tac thm = REPEAT o FIRST' 

    77   [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),

    78    rtac (thm RS @{thm trans}),

    79    rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]

    80 

    81 (* transform equations into the required form *)

    82 fun transform_eq ctxt thm lhs rhs = 

    83 let

    84   val (p, t) = dest_perm lhs

    85   val (c, args) = strip_comb t

    86   val (c', args') = strip_comb rhs 

    87   val eargs = map Envir.eta_contract args 

    88   val eargs' = map Envir.eta_contract args'

    89   val p_str = fst (fst (dest_Var p))

    90   val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))

    91 in

    92   if c <> c' 

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

    94   else if eargs' <> map (mk_perm p) eargs 

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

    96   else if args = [] 

    97     then thm

    98   else Goal.prove ctxt [p_str] [] goal

    99     (fn _ => eqvt_transform_tac thm 1)

   100 end

   101 

   102 fun transform addel_fun thm context = 

   103 let

   104   val ctxt = Context.proof_of context

   105   val trm = HOLogic.dest_Trueprop (prop_of thm)

   106 in

   107   case trm of

   108     Const (@{const_name "op ="}, _) $ lhs $ rhs =>

   109       let 

   110         val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}

   111       in

   112         addel_fun thm' context

   113       end

   114   | _ => raise (error "only (op=) case implemented yet")

   115 end 

   116 

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

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

   119 

   120 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;

   121 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;

   122 

   123 val setup =

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

   125     (cat_lines ["declaration of equivariance lemmas - they will automtically be",  

   126        "brought into the form p o c = c"]) #>

   127   Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) 

   128     (cat_lines ["declaration of equivariance lemmas - no",

   129        "transformation is performed"]) #>

   130   PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>

   131   PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);

   132 

   133 

   134 end;