1 (*  Title:      Nominal2_Eqvt

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Equivariance, Supp and Fresh Lemmas for Operators. 

     5     (Contains most, but not all such lemmas.)

     6 *)

     7 theory Nominal2_Eqvt

     8 imports Nominal2_Base

     9 uses ("nominal_thmdecls.ML")

    10      ("nominal_permeq.ML")

    11 begin

    12 

    13 section {* Logical Operators *}

    14 

    15 

    16 lemma eq_eqvt:

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

    18   unfolding permute_eq_iff permute_bool_def ..

    19 

    20 lemma if_eqvt:

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

    22   by (simp add: permute_fun_def permute_bool_def)

    23 

    24 lemma True_eqvt:

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

    26   unfolding permute_bool_def ..

    27 

    28 lemma False_eqvt:

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

    30   unfolding permute_bool_def ..

    31 

    32 lemma imp_eqvt:

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

    34   by (simp add: permute_bool_def)

    35 

    36 lemma conj_eqvt:

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

    38   by (simp add: permute_bool_def)

    39 

    40 lemma disj_eqvt:

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

    42   by (simp add: permute_bool_def)

    43 

    44 lemma Not_eqvt:

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

    46   by (simp add: permute_bool_def)

    47 

    48 lemma all_eqvt:

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

    50   unfolding permute_fun_def permute_bool_def

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

    52 

    53 lemma all_eqvt2:

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

    55   unfolding permute_fun_def permute_bool_def

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

    57 

    58 lemma ex_eqvt:

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

    60   unfolding permute_fun_def permute_bool_def

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

    62 

    63 lemma ex_eqvt2:

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

    65   unfolding permute_fun_def permute_bool_def

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

    67 

    68 lemma ex1_eqvt:

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

    70   unfolding Ex1_def 

    71   by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt)

    72 

    73 lemma ex1_eqvt2:

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

    75   unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt

    76   by simp

    77 

    78 lemma the_eqvt:

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

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

    81   apply(rule the1_equality [symmetric])

    82   apply(simp add: ex1_eqvt2[symmetric])

    83   apply(simp add: permute_bool_def unique)

    84   apply(simp add: permute_bool_def)

    85   apply(rule theI'[OF unique])

    86   done

    87 

    88 section {* Set Operations *}

    89 

    90 lemma mem_permute_iff:

    91   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"

    92 unfolding mem_def permute_fun_def permute_bool_def

    93 by simp

    94 

    95 lemma mem_eqvt:

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

    97   unfolding mem_permute_iff permute_bool_def by simp

    98 

    99 lemma not_mem_eqvt:

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

   101   unfolding mem_def permute_fun_def by (simp add: Not_eqvt)

   102 

   103 lemma Collect_eqvt:

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

   105   unfolding Collect_def permute_fun_def ..

   106 

   107 lemma Collect_eqvt2:

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

   109   unfolding Collect_def permute_fun_def ..

   110 

   111 lemma empty_eqvt:

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

   113   unfolding empty_def Collect_eqvt2 False_eqvt ..

   114 

   115 lemma supp_set_empty:

   116   shows "supp {} = {}"

   117   by (simp add: supp_def empty_eqvt)

   118 

   119 lemma fresh_set_empty:

   120   shows "a \<sharp> {}"

   121   by (simp add: fresh_def supp_set_empty)

   122 

   123 lemma UNIV_eqvt:

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

   125   unfolding UNIV_def Collect_eqvt2 True_eqvt ..

   126 

   127 lemma union_eqvt:

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

   129   unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp

   130 

   131 lemma inter_eqvt:

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

   133   unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp

   134 

   135 lemma Diff_eqvt:

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

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

   138   unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp

   139 

   140 lemma Compl_eqvt:

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

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

   143   unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..

   144 

   145 lemma insert_eqvt:

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

   147   unfolding permute_set_eq_image image_insert ..

   148 

   149 lemma vimage_eqvt:

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

   151   unfolding vimage_def permute_fun_def [where f=f]

   152   unfolding Collect_eqvt2 mem_eqvt ..

   153 

   154 lemma image_eqvt:

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

   156   unfolding permute_set_eq_image

   157   unfolding permute_fun_def [where f=f]

   158   by (simp add: image_image)

   159 

   160 lemma finite_permute_iff:

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

   162   unfolding permute_set_eq_vimage

   163   using bij_permute by (rule finite_vimage_iff)

   164 

   165 lemma finite_eqvt:

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

   167   unfolding finite_permute_iff permute_bool_def ..

   168 

   169 

   170 section {* List Operations *}

   171 

   172 lemma append_eqvt:

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

   174   by (induct xs) auto

   175 

   176 lemma supp_append:

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

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

   179 

   180 lemma fresh_append:

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

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

   183 

   184 lemma rev_eqvt:

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

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

   187 

   188 lemma supp_rev:

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

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

   191 

   192 lemma fresh_rev:

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

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

   195 

   196 lemma set_eqvt:

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

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

   199 

   200 (* needs finite support premise

   201 lemma supp_set:

   202   fixes x :: "'a::pt"

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

   204 *)

   205 

   206 

   207 section {* Product Operations *}

   208 

   209 lemma fst_eqvt:

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

   211  by (cases x) simp

   212 

   213 lemma snd_eqvt:

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

   215  by (cases x) simp

   216 

   217 

   218 section {* Units *}

   219 

   220 lemma supp_unit:

   221   shows "supp () = {}"

   222   by (simp add: supp_def)

   223 

   224 lemma fresh_unit:

   225   shows "a \<sharp> ()"

   226   by (simp add: fresh_def supp_unit)

   227 

   228 section {* Equivariance automation *}

   229 

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

   231 

   232 use "nominal_thmdecls.ML"

   233 setup "Nominal_ThmDecls.setup"

   234 

   235 lemmas [eqvt] = 

   236   (* connectives *)

   237   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 

   238   True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt

   239   imp_eqvt [folded induct_implies_def]

   240 

   241   (* nominal *)

   242   permute_eqvt supp_eqvt fresh_eqvt

   243   permute_pure

   244 

   245   (* datatypes *)

   246   permute_prod.simps append_eqvt rev_eqvt set_eqvt

   247   fst_eqvt snd_eqvt

   248 

   249   (* sets *)

   250   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt

   251   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt

   252 

   253 thm eqvts

   254 thm eqvts_raw

   255 

   256 text {* helper lemmas for the eqvt_tac *}

   257 

   258 definition

   259   "unpermute p = permute (- p)"

   260 

   261 lemma eqvt_apply:

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

   263   and x :: "'a::pt"

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

   265   unfolding permute_fun_def by simp

   266 

   267 lemma eqvt_lambda:

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

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

   270   unfolding permute_fun_def unpermute_def by simp

   271 

   272 lemma eqvt_bound:

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

   274   unfolding unpermute_def by simp

   275 

   276 use "nominal_permeq.ML"

   277 

   278 

   279 lemma "p \<bullet> (A \<longrightarrow> B = C)"

   280 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) 

   281 oops

   282 

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

   284 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})

   285 oops

   286 

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

   288 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})

   289 oops

   290 

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

   292 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})

   293 oops

   294 

   295 lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo"

   296 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})

   297 oops

   298 

   299 lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo"

   300 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})

   301 oops

   302 

   303 

   304 end