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 Nominal2_Atoms

     9 uses ("nominal_thmdecls.ML")

    10      ("nominal_permeq.ML")

    11 begin

    12 

    13 section {* Logical Operators *}

    14 

    15 lemma eq_eqvt:

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

    17   unfolding permute_eq_iff permute_bool_def ..

    18 

    19 lemma if_eqvt:

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

    21   by (simp add: permute_fun_def permute_bool_def)

    22 

    23 lemma True_eqvt:

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

    25   unfolding permute_bool_def ..

    26 

    27 lemma False_eqvt:

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

    29   unfolding permute_bool_def ..

    30 

    31 lemma imp_eqvt:

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

    33   by (simp add: permute_bool_def)

    34 

    35 lemma conj_eqvt:

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

    37   by (simp add: permute_bool_def)

    38 

    39 lemma disj_eqvt:

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

    41   by (simp add: permute_bool_def)

    42 

    43 lemma Not_eqvt:

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

    45   by (simp add: permute_bool_def)

    46 

    47 lemma all_eqvt:

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

    49   unfolding permute_fun_def permute_bool_def

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

    51 

    52 lemma all_eqvt2:

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

    54   unfolding permute_fun_def permute_bool_def

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

    56 

    57 lemma ex_eqvt:

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

    59   unfolding permute_fun_def permute_bool_def

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

    61 

    62 lemma ex_eqvt2:

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

    64   unfolding permute_fun_def permute_bool_def

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

    66 

    67 lemma ex1_eqvt:

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

    69   unfolding Ex1_def 

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

    71 

    72 lemma ex1_eqvt2:

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

    74   unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt

    75   by simp

    76 

    77 lemma the_eqvt:

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

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

    80   apply(rule the1_equality [symmetric])

    81   apply(simp add: ex1_eqvt2[symmetric])

    82   apply(simp add: permute_bool_def unique)

    83   apply(simp add: permute_bool_def)

    84   apply(rule theI'[OF unique])

    85   done

    86 

    87 section {* Set Operations *}

    88 

    89 lemma mem_permute_iff:

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

    91 unfolding mem_def permute_fun_def permute_bool_def

    92 by simp

    93 

    94 lemma mem_eqvt:

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

    96   unfolding mem_permute_iff permute_bool_def by simp

    97 

    98 lemma not_mem_eqvt:

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

   100   unfolding mem_def permute_fun_def by (simp add: Not_eqvt)

   101 

   102 lemma Collect_eqvt:

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

   104   unfolding Collect_def permute_fun_def ..

   105 

   106 lemma Collect_eqvt2:

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

   108   unfolding Collect_def permute_fun_def ..

   109 

   110 lemma empty_eqvt:

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

   112   unfolding empty_def Collect_eqvt2 False_eqvt ..

   113 

   114 lemma supp_set_empty:

   115   shows "supp {} = {}"

   116   by (simp add: supp_def empty_eqvt)

   117 

   118 lemma fresh_set_empty:

   119   shows "a \<sharp> {}"

   120   by (simp add: fresh_def supp_set_empty)

   121 

   122 lemma UNIV_eqvt:

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

   124   unfolding UNIV_def Collect_eqvt2 True_eqvt ..

   125 

   126 lemma union_eqvt:

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

   128   unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp

   129 

   130 lemma inter_eqvt:

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

   132   unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp

   133 

   134 lemma Diff_eqvt:

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

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

   137   unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp

   138 

   139 lemma Compl_eqvt:

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

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

   142   unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..

   143 

   144 lemma insert_eqvt:

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

   146   unfolding permute_set_eq_image image_insert ..

   147 

   148 lemma vimage_eqvt:

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

   150   unfolding vimage_def permute_fun_def [where f=f]

   151   unfolding Collect_eqvt2 mem_eqvt ..

   152 

   153 lemma image_eqvt:

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

   155   unfolding permute_set_eq_image

   156   unfolding permute_fun_def [where f=f]

   157   by (simp add: image_image)

   158 

   159 lemma finite_permute_iff:

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

   161   unfolding permute_set_eq_vimage

   162   using bij_permute by (rule finite_vimage_iff)

   163 

   164 lemma finite_eqvt:

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

   166   unfolding finite_permute_iff permute_bool_def ..

   167 

   168 

   169 section {* List Operations *}

   170 

   171 lemma append_eqvt:

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

   173   by (induct xs) auto

   174 

   175 lemma supp_append:

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

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

   178 

   179 lemma fresh_append:

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

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

   182 

   183 lemma rev_eqvt:

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

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

   186 

   187 lemma supp_rev:

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

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

   190 

   191 lemma fresh_rev:

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

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

   194 

   195 lemma set_eqvt:

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

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

   198 

   199 (* needs finite support premise

   200 lemma supp_set:

   201   fixes x :: "'a::pt"

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

   203 *)

   204 

   205 

   206 section {* Product Operations *}

   207 

   208 lemma fst_eqvt:

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

   210  by (cases x) simp

   211 

   212 lemma snd_eqvt:

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

   214  by (cases x) simp

   215 

   216 section {* Units *}

   217 

   218 lemma supp_unit:

   219   shows "supp () = {}"

   220   by (simp add: supp_def)

   221 

   222 lemma fresh_unit:

   223   shows "a \<sharp> ()"

   224   by (simp add: fresh_def supp_unit)

   225 

   226 section {* Equivariance automation *}

   227 

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

   229 

   230 use "nominal_thmdecls.ML"

   231 setup "Nominal_ThmDecls.setup"

   232 

   233 lemmas [eqvt] = 

   234   (* connectives *)

   235   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 

   236   True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt

   237   imp_eqvt [folded induct_implies_def]

   238 

   239   (* nominal *)

   240   (*permute_eqvt commented out since it loops *)

   241   supp_eqvt fresh_eqvt

   242   permute_pure

   243 

   244   (* datatypes *)

   245   permute_prod.simps append_eqvt rev_eqvt set_eqvt

   246   fst_eqvt snd_eqvt Pair_eqvt

   247 

   248   (* sets *)

   249   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt

   250   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt

   251 

   252   atom_eqvt add_perm_eqvt

   253 

   254 thm eqvts

   255 thm eqvts_raw

   256 

   257 text {* helper lemmas for the eqvt_tac *}

   258 

   259 definition

   260   "unpermute p = permute (- p)"

   261 

   262 lemma eqvt_apply:

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

   264   and x :: "'a::pt"

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

   266   unfolding permute_fun_def by simp

   267 

   268 lemma eqvt_lambda:

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

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

   271   unfolding permute_fun_def unpermute_def by simp

   272 

   273 lemma eqvt_bound:

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

   275   unfolding unpermute_def by simp

   276 

   277 use "nominal_permeq.ML"

   278 

   279 

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

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

   282 oops

   283 

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

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

   286 oops

   287 

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

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

   290 oops

   291 

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

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

   294 oops

   295 

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

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

   298 oops

   299 

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

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

   302 oops

   303 

   304 

   305 end