1 (*  Title:      Nominal2_Eqvt

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Equivariance, Supp and Fresh Lemmas for Operators. 

     5 *)

     6 theory Nominal2_Eqvt

     7 imports Nominal2_Base

     8 uses ("nominal_thmdecls.ML")

     9 begin

    10 

    11 section {* Logical Operators *}

    12 

    13 lemma eq_eqvt:

    14   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"

    15   unfolding permute_eq_iff permute_bool_def ..

    16 

    17 lemma if_eqvt:

    18   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"

    19   by (simp add: permute_fun_def permute_bool_def)

    20 

    21 lemma True_eqvt:

    22   shows "p \<bullet> True = True"

    23   unfolding permute_bool_def ..

    24 

    25 lemma False_eqvt:

    26   shows "p \<bullet> False = False"

    27   unfolding permute_bool_def ..

    28 

    29 lemma imp_eqvt:

    30   shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"

    31   by (simp add: permute_bool_def)

    32 

    33 lemma conj_eqvt:

    34   shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"

    35   by (simp add: permute_bool_def)

    36 

    37 lemma disj_eqvt:

    38   shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"

    39   by (simp add: permute_bool_def)

    40 

    41 lemma Not_eqvt:

    42   shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"

    43   by (simp add: permute_bool_def)

    44 

    45 lemma all_eqvt:

    46   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"

    47   unfolding permute_fun_def permute_bool_def

    48   by (auto, drule_tac x="p \<bullet> x" in spec, simp)

    49 

    50 lemma ex_eqvt:

    51   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"

    52   unfolding permute_fun_def permute_bool_def

    53   by (auto, rule_tac x="p \<bullet> x" in exI, simp)

    54 

    55 lemma ex1_eqvt:

    56   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"

    57   unfolding Ex1_def ex_eqvt conj_eqvt all_eqvt imp_eqvt eq_eqvt

    58   by simp

    59 

    60 lemma the_eqvt:

    61   assumes unique: "\<exists>!x. P x"

    62   shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))"

    63   apply(rule the1_equality [symmetric])

    64   apply(simp add: ex1_eqvt[symmetric])

    65   apply(simp add: permute_bool_def unique)

    66   apply(simp add: permute_bool_def)

    67   apply(rule theI'[OF unique])

    68   done

    69 

    70 section {* Set Operations *}

    71 

    72 lemma mem_eqvt:

    73   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"

    74   unfolding mem_def permute_fun_def by simp

    75 

    76 lemma not_mem_eqvt:

    77   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"

    78   unfolding mem_def permute_fun_def by (simp add: Not_eqvt)

    79 

    80 lemma Collect_eqvt:

    81   shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"

    82   unfolding Collect_def permute_fun_def ..

    83 

    84 lemma empty_eqvt:

    85   shows "p \<bullet> {} = {}"

    86   unfolding empty_def Collect_eqvt False_eqvt ..

    87 

    88 lemma supp_set_empty:

    89   shows "supp {} = {}"

    90   by (simp add: supp_def empty_eqvt)

    91 

    92 lemma fresh_set_empty:

    93   shows "a \<sharp> {}"

    94   by (simp add: fresh_def supp_set_empty)

    95 

    96 lemma UNIV_eqvt:

    97   shows "p \<bullet> UNIV = UNIV"

    98   unfolding UNIV_def Collect_eqvt True_eqvt ..

    99 

   100 lemma union_eqvt:

   101   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"

   102   unfolding Un_def Collect_eqvt disj_eqvt mem_eqvt by simp

   103 

   104 lemma inter_eqvt:

   105   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"

   106   unfolding Int_def Collect_eqvt conj_eqvt mem_eqvt by simp

   107 

   108 lemma Diff_eqvt:

   109   fixes A B :: "'a::pt set"

   110   shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"

   111   unfolding set_diff_eq Collect_eqvt conj_eqvt Not_eqvt mem_eqvt by simp

   112 

   113 lemma Compl_eqvt:

   114   fixes A :: "'a::pt set"

   115   shows "p \<bullet> (- A) = - (p \<bullet> A)"

   116   unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..

   117 

   118 lemma insert_eqvt:

   119   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"

   120   unfolding permute_set_eq_image image_insert ..

   121 

   122 lemma vimage_eqvt:

   123   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"

   124   unfolding vimage_def permute_fun_def [where f=f]

   125   unfolding Collect_eqvt mem_eqvt ..

   126 

   127 lemma image_eqvt:

   128   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"

   129   unfolding permute_set_eq_image

   130   unfolding permute_fun_def [where f=f]

   131   by (simp add: image_image)

   132 

   133 lemma finite_permute_iff:

   134   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"

   135   unfolding permute_set_eq_vimage

   136   using bij_permute by (rule finite_vimage_iff)

   137 

   138 lemma finite_eqvt:

   139   shows "p \<bullet> finite A = finite (p \<bullet> A)"

   140   unfolding finite_permute_iff permute_bool_def ..

   141 

   142 lemma supp_eqvt: "p \<bullet> supp S = supp (p \<bullet> S)"

   143   unfolding supp_def

   144   by (simp only: Collect_eqvt Not_eqvt finite_eqvt eq_eqvt

   145       permute_eqvt [of p] swap_eqvt permute_minus_cancel)

   146 

   147 

   148 section {* List Operations *}

   149 

   150 lemma append_eqvt:

   151   shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"

   152   by (induct xs) auto

   153 

   154 lemma supp_append:

   155   shows "supp (xs @ ys) = supp xs \<union> supp ys"

   156   by (induct xs) (auto simp add: supp_Nil supp_Cons)

   157 

   158 lemma fresh_append:

   159   shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"

   160   by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

   161 

   162 lemma rev_eqvt:

   163   shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"

   164   by (induct xs) (simp_all add: append_eqvt)

   165 

   166 lemma supp_rev:

   167   shows "supp (rev xs) = supp xs"

   168   by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)

   169 

   170 lemma fresh_rev:

   171   shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"

   172   by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)

   173 

   174 lemma set_eqvt:

   175   shows "p \<bullet> (set xs) = set (p \<bullet> xs)"

   176   by (induct xs) (simp_all add: empty_eqvt insert_eqvt)

   177 

   178 (* needs finite support premise

   179 lemma supp_set:

   180   fixes x :: "'a::pt"

   181   shows "supp (set xs) = supp xs"

   182 *)

   183 

   184 

   185 section {* Product Operations *}

   186 

   187 lemma fst_eqvt:

   188   "p \<bullet> (fst x) = fst (p \<bullet> x)"

   189  by (cases x) simp

   190 

   191 lemma snd_eqvt:

   192   "p \<bullet> (snd x) = snd (p \<bullet> x)"

   193  by (cases x) simp

   194 

   195 

   196 section {* Units *}

   197 

   198 lemma supp_unit:

   199   shows "supp () = {}"

   200   by (simp add: supp_def)

   201 

   202 lemma fresh_unit:

   203   shows "a \<sharp> ()"

   204   by (simp add: fresh_def supp_unit)

   205 

   206 section {* Equivariance automation *}

   207 

   208 text {* 

   209   below is a construction site for a conversion that  

   210   pushes permutations into a term as far as possible 

   211 *}

   212 

   213 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}

   214 

   215 use "nominal_thmdecls.ML"

   216 setup "NominalThmDecls.setup"

   217 

   218 lemmas [eqvt] = 

   219   (* connectives *)

   220   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 

   221   True_eqvt False_eqvt

   222   imp_eqvt [folded induct_implies_def]

   223 

   224   (* datatypes *)

   225   permute_prod.simps

   226   fst_eqvt snd_eqvt

   227 

   228   (* sets *)

   229   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt

   230   Diff_eqvt Compl_eqvt insert_eqvt

   231 

   232 (* A simple conversion pushing permutations into a term *)

   233 

   234 ML {*

   235 fun OF1 thm1 thm2 = thm2 RS thm1

   236 

   237 fun get_eqvt_thms ctxt =

   238   map (OF1 @{thm eq_reflection}) (NominalThmDecls.get_eqvt_thms ctxt)  

   239 *}

   240 

   241 ML {* 

   242 fun eqvt_conv ctxt ctrm =

   243   case (term_of ctrm) of

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

   245        (if is_Const (head_of t)

   246         then (More_Conv.rewrs_conv (get_eqvt_thms ctxt) 

   247               then_conv eqvt_conv ctxt) ctrm

   248         else Conv.comb_conv (eqvt_conv ctxt) ctrm)

   249      | _ $ _ => Conv.comb_conv (eqvt_conv ctxt) ctrm

   250      | Abs _ => Conv.abs_conv (fn (_, ctxt) => eqvt_conv ctxt) ctxt ctrm

   251      | _ => Conv.all_conv ctrm

   252 *}

   253 

   254 ML {*

   255 fun eqvt_tac ctxt = 

   256   CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)

   257 *}

   258 

   259 lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"

   260 apply(tactic {* eqvt_tac @{context} 1 *}) 

   261 oops

   262 

   263 text {*

   264   Another conversion for pushing permutations into a term.

   265   It is designed not to apply rules like @{term permute_pure} to

   266   applications or abstractions, only to constants or free

   267   variables. Thus permutations are not removed too early, and they

   268   have a chance to cancel with bound variables.

   269 *}

   270 

   271 definition

   272   "unpermute p = permute (- p)"

   273 

   274 lemma push_apply:

   275   fixes f :: "'a::pt \<Rightarrow> 'b::pt" and x :: "'a::pt"

   276   shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"

   277   unfolding permute_fun_def by simp

   278 

   279 lemma push_lambda:

   280   fixes f :: "'a::pt \<Rightarrow> 'b::pt"

   281   shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"

   282   unfolding permute_fun_def unpermute_def by simp

   283 

   284 lemma push_bound:

   285   shows "p \<bullet> unpermute p x \<equiv> x"

   286   unfolding unpermute_def by simp

   287 

   288 ML {*

   289 structure PushData = Named_Thms

   290 (

   291   val name = "push"

   292   val description = "push permutations"

   293 )

   294 

   295 local

   296 

   297 fun push_apply_conv ctxt ct =

   298   case (term_of ct) of

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

   300       let

   301         val (perm, t) = Thm.dest_comb ct

   302         val (_, p) = Thm.dest_comb perm

   303         val (f, x) = Thm.dest_comb t

   304         val a = ctyp_of_term x;

   305         val b = ctyp_of_term t;

   306         val ty_insts = map SOME [b, a]

   307         val term_insts = map SOME [p, f, x]

   308       in

   309         Drule.instantiate' ty_insts term_insts @{thm push_apply}

   310       end

   311   | _ => Conv.no_conv ct

   312 

   313 fun push_lambda_conv ctxt ct =

   314   case (term_of ct) of

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

   316       Conv.rewr_conv @{thm push_lambda} ct

   317   | _ => Conv.no_conv ct

   318 

   319 in

   320 

   321 fun push_conv ctxt ct =

   322   Conv.first_conv

   323     [ Conv.rewr_conv @{thm push_bound},

   324       push_apply_conv ctxt

   325         then_conv Conv.comb_conv (push_conv ctxt),

   326       push_lambda_conv ctxt

   327         then_conv Conv.abs_conv (fn (v, ctxt) => push_conv ctxt) ctxt,

   328       More_Conv.rewrs_conv (PushData.get ctxt),

   329       Conv.all_conv

   330     ] ct

   331 

   332 fun push_tac ctxt = 

   333   CONVERSION (More_Conv.bottom_conv (fn ctxt => push_conv ctxt) ctxt)

   334 

   335 end

   336 *}

   337 

   338 setup PushData.setup

   339 

   340 declare permute_pure [THEN eq_reflection, push]

   341 

   342 lemma push_eq [THEN eq_reflection, push]:

   343   "p \<bullet> (op =) = (op =)"

   344   by (simp add: expand_fun_eq permute_fun_def eq_eqvt)

   345 

   346 lemma push_All [THEN eq_reflection, push]:

   347   "p \<bullet> All = All"

   348   by (simp add: expand_fun_eq permute_fun_def all_eqvt)

   349 

   350 lemma push_Ex [THEN eq_reflection, push]:

   351   "p \<bullet> Ex = Ex"

   352   by (simp add: expand_fun_eq permute_fun_def ex_eqvt)

   353 

   354 lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"

   355 apply (tactic {* push_tac @{context} 1 *}) 

   356 oops

   357 

   358 lemma "p \<bullet> (\<lambda>x. A \<longrightarrow> B x = (C::bool)) = foo"

   359 apply (tactic {* push_tac @{context} 1 *})

   360 oops

   361 

   362 lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"

   363 apply (tactic {* push_tac @{context} 1 *})

   364 oops

   365 

   366 lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"

   367 apply (tactic {* push_tac @{context} 1 *})

   368 oops

   369 

   370 end