1 (*  Title:      HOL/Nominal/nominal_thmdecls.ML

     2     Author:     Julien Narboux, TU Muenchen

     3     Author:     Christian Urban, TU Muenchen

     4 

     5 Infrastructure for the lemma collection "eqvts".

     6 

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

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

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

    10 data-slot.

    11 *)

    12 

    13 signature NOMINAL_THMDECLS =

    14 sig

    15   val eqvt_add: attribute

    16   val eqvt_del: attribute

    17   val eqvt_force_add: attribute

    18   val eqvt_force_del: attribute

    19   val setup: theory -> theory

    20   val get_eqvt_thms: Proof.context -> thm list

    21 

    22 end;

    23 

    24 structure NominalThmDecls: NOMINAL_THMDECLS =

    25 struct

    26 

    27 structure Data = Generic_Data

    28 (

    29   type T = thm list

    30   val empty = []

    31   val extend = I

    32   val merge = Thm.merge_thms

    33 )

    34 

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

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

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

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

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

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

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

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

    43 (* equality-lemma can be derived. *)

    44 exception EQVT_FORM of string

    45 

    46 val perm_boolE =

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

    48 

    49 val perm_boolI =

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

    51 

    52 fun prove_eqvt_tac ctxt orig_thm pi pi' =

    53 let

    54   val mypi = Thm.cterm_of ctxt pi

    55   val T = fastype_of pi'

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

    57   val perm_pi_simp = @{thms permute_minus_cancel}

    58 in

    59   EVERY1 [rtac @{thm iffI},

    60           dtac perm_boolE,

    61           etac orig_thm,

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

    63           rtac perm_boolI,

    64           full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)]

    65 end;

    66 

    67 fun get_derived_thm ctxt hyp concl orig_thm pi =

    68   let

    69     val thy = ProofContext.theory_of ctxt;

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

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

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

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

    74   in

    75     Goal.prove ctxt' [] [] goal_term

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

    77     singleton (ProofContext.export ctxt' ctxt)

    78   end

    79 

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

    81 fun apply_pi trm pi =

    82 let

    83   fun replace n ty =

    84   let 

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

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

    87     val v2 = Var (n, ty)

    88   in

    89     c $ v1 $ v2 

    90   end

    91 in

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

    93 end

    94 

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

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

    97 fun get_pi t thy =

    98   let fun get_pi_aux s =

    99         (case s of

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

   101              (Var (pi,_)) $

   102                (Var (n,ty))) =>

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

   104                 then [pi]

   105                 else raise

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

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

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

   109         | _ => [])

   110   in

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

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

   113     (* a singleton-list  *)

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

   115       [pi] => pi

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

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

   118   end;

   119 

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

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

   122 (* certain form. *)

   123 

   124 fun eqvt_add_del_aux flag orig_thm context = 

   125   let

   126     val thy = Context.theory_of context

   127     val thms_to_be_added = (case (prop_of orig_thm) of

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

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

   130           let

   131             val pi = get_pi concl thy

   132           in

   133              if (apply_pi hyp pi = concl)

   134              then

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

   136                 [orig_thm,

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

   138              else raise EQVT_FORM "Type Implication"

   139           end

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

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

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

   143            (if (apply_pi lhs pi) = rhs

   144                then [orig_thm]

   145                else raise EQVT_FORM "Type Equality")

   146       | _ => raise EQVT_FORM "Type unknown")

   147   in

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

   149   end

   150   handle EQVT_FORM s =>

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

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

   153 

   154 

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

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

   157 

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

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

   160 

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

   162 

   163 val setup =

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

   165      "equivariance theorem declaration" 

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

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

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

   169 

   170 

   171 end;