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) ...    (1)

    12 

    13   or

    14 

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

    16 

    17   and it is stored in the form

    18 

    19     p o c == c

    20 

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

    22 

    23   TODO: In case of the form in (2) one should also

    24         add the equational form to eqvts

    25 *)

    26 

    27 signature NOMINAL_THMDECLS =

    28 sig

    29   val eqvt_add: attribute

    30   val eqvt_del: attribute

    31   val eqvt_raw_add: attribute

    32   val eqvt_raw_del: attribute

    33   val setup: theory -> theory

    34   val get_eqvts_thms: Proof.context -> thm list

    35   val get_eqvts_raw_thms: Proof.context -> thm list

    36   val eqvt_transform: Proof.context -> thm -> thm

    37   val is_eqvt: Proof.context -> term -> bool

    38 end;

    39 

    40 structure Nominal_ThmDecls: NOMINAL_THMDECLS =

    41 struct

    42 

    43 structure EqvtData = Generic_Data

    44 ( type T = thm Item_Net.T;

    45   val empty = Thm.full_rules;

    46   val extend = I;

    47   val merge = Item_Net.merge);

    48 

    49 structure EqvtRawData = Generic_Data

    50 ( type T = thm Termtab.table;

    51   val empty = Termtab.empty;

    52   val extend = I;

    53   val merge = Termtab.merge (K true));

    54 

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

    56 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get;

    57 

    58 val get_eqvts_thms = eqvts o  Context.Proof;

    59 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;

    60 

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

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

    63 

    64 fun add_raw_thm thm = 

    65   case prop_of thm of

    66     Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) 

    67   | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 

    68 

    69 fun del_raw_thm thm = 

    70   case prop_of thm of

    71     Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c)

    72   | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 

    73 

    74 fun is_eqvt ctxt trm =

    75   case trm of 

    76     (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c

    77   | _ => raise TERM ("Term must be a constsnt.", [trm])

    78 

    79 

    80 

    81 (** transformation of eqvt lemmas **)

    82 

    83 fun get_perms trm =

    84   case trm of 

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

    86        raise TERM ("get_perms called on bound", [trm])

    87    | Const (@{const_name permute}, _) $ p $ _ => [p]

    88    | t $ u => get_perms t @ get_perms u

    89    | Abs (_, _, t) => get_perms t 

    90    | _ => []

    91 

    92 fun put_perm p trm =

    93   case trm of 

    94      Bound _ => trm

    95    | Const _ => trm

    96    | t $ u => put_perm p t $ put_perm p u

    97    | Abs (x, ty, t) => Abs (x, ty, put_perm p t)

    98    | _ => mk_perm p trm

    99 

   100 (* tests whether there is a disagreement between the permutations, 

   101    and that there is at least one permutation *)

   102 fun is_bad_list [] = true

   103   | is_bad_list [_] = false

   104   | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true

   105 

   106 

   107 (* transforms equations into the "p o c == c"-form 

   108    from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)

   109 

   110 fun eqvt_transform_eq_tac thm = 

   111 let

   112   val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}

   113 in

   114   REPEAT o FIRST' 

   115     [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),

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

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

   118 end

   119 

   120 fun eqvt_transform_eq ctxt thm = 

   121   let

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

   123       handle TERM _ => error "Equivariance lemma must be an equality."

   124     val (p, t) = dest_perm lhs 

   125       handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c...  = c..."

   126 

   127     val ps = get_perms rhs handle TERM _ => []  

   128     val (c, c') = (head_of t, head_of rhs)

   129     val msg = "Equivariance lemma is not of the right form "

   130   in

   131     if c <> c' 

   132       then error (msg ^ "(constants do not agree).")

   133     else if is_bad_list (p :: ps)  

   134       then error (msg ^ "(permutations do not agree).") 

   135     else if not (rhs aconv (put_perm p t))

   136       then error (msg ^ "(arguments do not agree).")

   137     else if is_Const t 

   138       then safe_mk_equiv thm

   139     else 

   140       let 

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

   142         val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt

   143       in

   144         Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)

   145         |> singleton (ProofContext.export ctxt' ctxt)

   146         |> safe_mk_equiv

   147         |> zero_var_indexes

   148       end

   149   end

   150 

   151 (* transforms equations into the "p o c == c"-form 

   152    from R x1 ...xn ==> R (p o x1) ... (p o xn) *)

   153 

   154 fun eqvt_transform_imp_tac ctxt p p' thm = 

   155   let

   156     val thy = ProofContext.theory_of ctxt

   157     val cp = Thm.cterm_of thy p

   158     val cp' = Thm.cterm_of thy (mk_minus p')

   159     val thm' = Drule.cterm_instantiate [(cp, cp')] thm

   160     val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)}

   161   in

   162     EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac,

   163       rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]

   164   end

   165 

   166 fun eqvt_transform_imp ctxt thm =

   167   let

   168     val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))

   169     val (c, c') = (head_of prem, head_of concl)

   170     val ps = get_perms concl handle TERM _ => []  

   171     val p = try hd ps

   172     val msg = "Equivariance lemma is not of the right form "

   173   in

   174     if c <> c' 

   175       then error (msg ^ "(constants do not agree).")

   176     else if is_bad_list ps  

   177       then error (msg ^ "(permutations do not agree).") 

   178     else if not (concl aconv (put_perm (the p) prem)) 

   179       then error (msg ^ "(arguments do not agree).")

   180     else 

   181       let

   182         val prem' = mk_perm (the p) prem    

   183         val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))

   184         val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt

   185       in

   186         Goal.prove ctxt' [] [] goal'

   187           (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) 

   188         |> singleton (ProofContext.export ctxt' ctxt)

   189       end

   190   end     

   191 

   192 fun eqvt_transform ctxt thm = 

   193   case (prop_of thm) of

   194     @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ 

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

   196         eqvt_transform_eq ctxt thm

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

   198       eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt

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

   200  

   201 

   202 (** attributes **)

   203 

   204 val eqvt_add = Thm.declaration_attribute 

   205   (fn thm => fn context =>

   206    let

   207      val thm' = eqvt_transform (Context.proof_of context) thm

   208    in

   209      context |> add_thm thm |> add_raw_thm thm'

   210    end)

   211 

   212 val eqvt_del = Thm.declaration_attribute

   213   (fn thm => fn context =>

   214    let

   215      val thm' = eqvt_transform (Context.proof_of context) thm

   216    in

   217      context |> del_thm thm  |> del_raw_thm thm'

   218    end)

   219 

   220 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;

   221 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;

   222 

   223 

   224 (** setup function **)

   225 

   226 val setup =

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

   228     (cat_lines ["Declaration of equivariance lemmas - they will automtically be",  

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

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

   231     (cat_lines ["Declaration of equivariance lemmas - no",

   232        "transformation is performed"]) #>

   233   Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>

   234   Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);

   235 

   236 

   237 end;