1 (*  Title:      Nominal2_Eqvt

     2     Author:     Brian Huffman, 

     3     Author:     Christian Urban

     4 

     5     Equivariance, supp and freshness lemmas for various operators 

     6     (contains many, but not all such lemmas).

     7 *)

     8 theory Nominal2_Eqvt

     9 imports Nominal2_Base 

    10 uses ("nominal_thmdecls.ML")

    11      ("nominal_permeq.ML")

    12      ("nominal_eqvt.ML")

    13 begin

    14 

    15 

    16 section {* Permsimp and Eqvt infrastructure *}

    17 

    18 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}

    19 

    20 use "nominal_thmdecls.ML"

    21 setup "Nominal_ThmDecls.setup"

    22 

    23 

    24 section {* eqvt lemmas *}

    25 

    26 lemmas [eqvt] =

    27   conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt

    28   imp_eqvt[folded induct_implies_def]

    29   uminus_eqvt

    30 

    31   (* nominal *)

    32   supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 

    33   swap_eqvt flip_eqvt

    34 

    35   (* datatypes *)

    36   Pair_eqvt permute_list.simps 

    37 

    38   (* sets *)

    39   mem_eqvt empty_eqvt insert_eqvt set_eqvt

    40 

    41   (* fsets *)

    42   permute_fset fset_eqvt

    43 

    44 text {* helper lemmas for the perm_simp *}

    45 

    46 definition

    47   "unpermute p = permute (- p)"

    48 

    49 lemma eqvt_apply:

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

    51   and x :: "'a::pt"

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

    53   unfolding permute_fun_def by simp

    54 

    55 lemma eqvt_lambda:

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

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

    58   unfolding permute_fun_def unpermute_def by simp

    59 

    60 lemma eqvt_bound:

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

    62   unfolding unpermute_def by simp

    63 

    64 text {* provides perm_simp methods *}

    65 

    66 use "nominal_permeq.ML"

    67 setup Nominal_Permeq.setup

    68 

    69 method_setup perm_simp =

    70  {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}

    71  {* pushes permutations inside. *}

    72 

    73 method_setup perm_strict_simp =

    74  {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}

    75  {* pushes permutations inside, raises an error if it cannot solve all permutations. *}

    76 

    77 (* the normal version of this lemma would cause loops *)

    78 lemma permute_eqvt_raw[eqvt_raw]:

    79   shows "p \<bullet> permute \<equiv> permute"

    80 apply(simp add: fun_eq_iff permute_fun_def)

    81 apply(subst permute_eqvt)

    82 apply(simp)

    83 done

    84 

    85 subsection {* Equivariance of Logical Operators *}

    86 

    87 lemma eq_eqvt[eqvt]:

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

    89   unfolding permute_eq_iff permute_bool_def ..

    90 

    91 lemma if_eqvt[eqvt]:

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

    93   by (simp add: permute_fun_def permute_bool_def)

    94 

    95 lemma True_eqvt[eqvt]:

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

    97   unfolding permute_bool_def ..

    98 

    99 lemma False_eqvt[eqvt]:

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

   101   unfolding permute_bool_def ..

   102 

   103 lemma disj_eqvt[eqvt]:

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

   105   by (simp add: permute_bool_def)

   106 

   107 lemma all_eqvt2:

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

   109   by (perm_simp add: permute_minus_cancel) (rule refl)

   110 

   111 lemma ex_eqvt2:

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

   113   by (perm_simp add: permute_minus_cancel) (rule refl)

   114 

   115 lemma ex1_eqvt[eqvt]:

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

   117   unfolding Ex1_def

   118   by (perm_simp) (rule refl)

   119 

   120 lemma ex1_eqvt2:

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

   122   by (perm_simp add: permute_minus_cancel) (rule refl)

   123 

   124 lemma the_eqvt:

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

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

   127   apply(rule the1_equality [symmetric])

   128   apply(simp add: ex1_eqvt2[symmetric])

   129   apply(simp add: permute_bool_def unique)

   130   apply(simp add: permute_bool_def)

   131   apply(rule theI'[OF unique])

   132   done

   133 

   134 subsection {* Equivariance Set Operations *}

   135 

   136 lemma not_mem_eqvt:

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

   138   by (perm_simp) (rule refl)

   139 

   140 lemma Collect_eqvt[eqvt]:

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

   142   unfolding Collect_def permute_fun_def ..

   143 

   144 lemma Collect_eqvt2:

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

   146   by (perm_simp add: permute_minus_cancel) (rule refl)

   147 

   148 lemma Bex_eqvt[eqvt]:

   149   shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"

   150   unfolding Bex_def

   151   by (perm_simp) (rule refl)

   152 

   153 lemma Ball_eqvt[eqvt]:

   154   shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"

   155   unfolding Ball_def

   156   by (perm_simp) (rule refl)

   157 

   158 lemma supp_set_empty:

   159   shows "supp {} = {}"

   160   unfolding supp_def

   161   by (simp add: empty_eqvt)

   162 

   163 lemma fresh_set_empty:

   164   shows "a \<sharp> {}"

   165   by (simp add: fresh_def supp_set_empty)

   166 

   167 lemma UNIV_eqvt[eqvt]:

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

   169   unfolding UNIV_def

   170   by (perm_simp) (rule refl)

   171 

   172 lemma union_eqvt[eqvt]:

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

   174   unfolding Un_def

   175   by (perm_simp) (rule refl)

   176 

   177 lemma inter_eqvt[eqvt]:

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

   179   unfolding Int_def 

   180   by (perm_simp) (rule refl)

   181 

   182 lemma Diff_eqvt[eqvt]:

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

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

   185   unfolding set_diff_eq

   186   by (perm_simp) (rule refl)

   187 

   188 lemma Compl_eqvt[eqvt]:

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

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

   191   unfolding Compl_eq_Diff_UNIV

   192   by (perm_simp) (rule refl)

   193 

   194 lemma image_eqvt:

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

   196   unfolding permute_set_eq_image

   197   unfolding permute_fun_def [where f=f]

   198   by (simp add: image_image)

   199 

   200 lemma vimage_eqvt[eqvt]:

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

   202   unfolding vimage_def

   203   by (perm_simp) (rule refl)

   204 

   205 lemma Union_eqvt[eqvt]:

   206   shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"

   207   unfolding Union_eq 

   208   by (perm_simp) (rule refl)

   209 

   210 lemma finite_permute_iff:

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

   212   unfolding permute_set_eq_vimage

   213   using bij_permute by (rule finite_vimage_iff)

   214 

   215 lemma finite_eqvt[eqvt]:

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

   217   unfolding finite_permute_iff permute_bool_def ..

   218 

   219 lemma supp_set:

   220   fixes xs :: "('a::fs) list"

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

   222 apply(induct xs)

   223 apply(simp add: supp_set_empty supp_Nil)

   224 apply(simp add: supp_Cons supp_of_finite_insert)

   225 done

   226 

   227 

   228 section {* List Operations *}

   229 

   230 lemma append_eqvt[eqvt]:

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

   232   by (induct xs) auto

   233 

   234 lemma supp_append:

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

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

   237 

   238 lemma fresh_append:

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

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

   241 

   242 lemma rev_eqvt[eqvt]:

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

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

   245 

   246 lemma supp_rev:

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

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

   249 

   250 lemma fresh_rev:

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

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

   253 

   254 lemma map_eqvt[eqvt]: 

   255   shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"

   256   by (induct xs) (simp_all, simp only: permute_fun_app_eq)

   257 

   258 

   259 subsection {* Equivariance for fsets *} 

   260 

   261 lemma map_fset_eqvt[eqvt]: 

   262   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"

   263   by (lifting map_eqvt)

   264 

   265 

   266 subsection {* Product Operations *}

   267 

   268 lemma fst_eqvt[eqvt]:

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

   270  by (cases x) simp

   271 

   272 lemma snd_eqvt[eqvt]:

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

   274  by (cases x) simp

   275 

   276 lemma split_eqvt[eqvt]: 

   277   shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"

   278   unfolding split_def

   279   by (perm_simp) (rule refl)

   280 

   281 

   282 section {* Test cases *}

   283 

   284 

   285 declare [[trace_eqvt = false]]

   286 (* declare [[trace_eqvt = true]] *)

   287 

   288 lemma 

   289   fixes B::"'a::pt"

   290   shows "p \<bullet> (B = C)"

   291 apply(perm_simp)

   292 oops

   293 

   294 lemma 

   295   fixes B::"bool"

   296   shows "p \<bullet> (B = C)"

   297 apply(perm_simp)

   298 oops

   299 

   300 lemma 

   301   fixes B::"bool"

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

   303 apply (perm_simp) 

   304 oops

   305 

   306 lemma 

   307   shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"

   308 apply(perm_simp)

   309 oops

   310 

   311 lemma 

   312   shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"

   313 apply (perm_simp)

   314 oops

   315 

   316 lemma 

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

   318 apply (perm_simp)

   319 oops

   320 

   321 lemma 

   322   shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"

   323 apply (perm_simp)

   324 oops

   325 

   326 lemma 

   327   fixes p q::"perm"

   328   and   x::"'a::pt"

   329   shows "p \<bullet> (q \<bullet> x) = foo"

   330 apply(perm_simp)

   331 oops

   332 

   333 lemma 

   334   fixes p q r::"perm"

   335   and   x::"'a::pt"

   336   shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"

   337 apply(perm_simp)

   338 oops

   339 

   340 lemma 

   341   fixes p r::"perm"

   342   shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"

   343 apply (perm_simp)

   344 oops

   345 

   346 lemma 

   347   fixes C D::"bool"

   348   shows "B (p \<bullet> (C = D))"

   349 apply(perm_simp)

   350 oops

   351 

   352 declare [[trace_eqvt = false]]

   353 

   354 text {* there is no raw eqvt-rule for The *}

   355 lemma "p \<bullet> (THE x. P x) = foo"

   356 apply(perm_strict_simp exclude: The)

   357 apply(perm_simp exclude: The)

   358 oops

   359 

   360 lemma 

   361   fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"

   362   shows "p \<bullet> (P The) = foo"

   363 apply(perm_simp exclude: The)

   364 oops

   365 

   366 lemma

   367   fixes  P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"

   368   shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"

   369 apply(perm_simp)

   370 oops

   371 

   372 thm eqvts

   373 thm eqvts_raw

   374 

   375 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}

   376 

   377 

   378 section {* automatic equivariance procedure for inductive definitions *}

   379 

   380 use "nominal_eqvt.ML"

   381 

   382 end