1 /home/cu200/Isabelle/nominal-huffman/Nominal2_Eqvt.thy

     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      ("nominal_permeq.ML")

    10 begin

    11 

    12 section {* Logical Operators *}

    13 

    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_eqvt:

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

    91   unfolding mem_def permute_fun_def by simp

    92 

    93 lemma not_mem_eqvt:

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

    95   unfolding mem_def permute_fun_def by (simp add: Not_eqvt)

    96 

    97 lemma Collect_eqvt:

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

    99   unfolding Collect_def permute_fun_def ..

   100 

   101 lemma Collect_eqvt2:

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

   103   unfolding Collect_def permute_fun_def ..

   104 

   105 lemma empty_eqvt:

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

   107   unfolding empty_def Collect_eqvt2 False_eqvt ..

   108 

   109 lemma supp_set_empty:

   110   shows "supp {} = {}"

   111   by (simp add: supp_def empty_eqvt)

   112 

   113 lemma fresh_set_empty:

   114   shows "a \<sharp> {}"

   115   by (simp add: fresh_def supp_set_empty)

   116 

   117 lemma UNIV_eqvt:

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

   119   unfolding UNIV_def Collect_eqvt2 True_eqvt ..

   120 

   121 lemma union_eqvt:

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

   123   unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp

   124 

   125 lemma inter_eqvt:

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

   127   unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp

   128 

   129 lemma Diff_eqvt:

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

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

   132   unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp

   133 

   134 lemma Compl_eqvt:

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

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

   137   unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..

   138 

   139 lemma insert_eqvt:

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

   141   unfolding permute_set_eq_image image_insert ..

   142 

   143 lemma vimage_eqvt:

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

   145   unfolding vimage_def permute_fun_def [where f=f]

   146   unfolding Collect_eqvt2 mem_eqvt ..

   147 

   148 lemma image_eqvt:

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

   150   unfolding permute_set_eq_image

   151   unfolding permute_fun_def [where f=f]

   152   by (simp add: image_image)

   153 

   154 lemma finite_permute_iff:

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

   156   unfolding permute_set_eq_vimage

   157   using bij_permute by (rule finite_vimage_iff)

   158 

   159 lemma finite_eqvt:

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

   161   unfolding finite_permute_iff permute_bool_def ..

   162 

   163 

   164 section {* List Operations *}

   165 

   166 lemma append_eqvt:

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

   168   by (induct xs) auto

   169 

   170 lemma supp_append:

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

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

   173 

   174 lemma fresh_append:

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

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

   177 

   178 lemma rev_eqvt:

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

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

   181 

   182 lemma supp_rev:

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

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

   185 

   186 lemma fresh_rev:

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

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

   189 

   190 lemma set_eqvt:

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

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

   193 

   194 (* needs finite support premise

   195 lemma supp_set:

   196   fixes x :: "'a::pt"

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

   198 *)

   199 

   200 

   201 section {* Product Operations *}

   202 

   203 lemma fst_eqvt:

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

   205  by (cases x) simp

   206 

   207 lemma snd_eqvt:

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

   209  by (cases x) simp

   210 

   211 

   212 section {* Units *}

   213 

   214 lemma supp_unit:

   215   shows "supp () = {}"

   216   by (simp add: supp_def)

   217 

   218 lemma fresh_unit:

   219   shows "a \<sharp> ()"

   220   by (simp add: fresh_def supp_unit)

   221 

   222 section {* Equivariance automation *}

   223 

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

   225 

   226 use "nominal_thmdecls.ML"

   227 setup "Nominal_ThmDecls.setup"

   228 

   229 lemmas [eqvt] = 

   230   (* connectives *)

   231   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 

   232   True_eqvt False_eqvt ex_eqvt all_eqvt

   233   imp_eqvt [folded induct_implies_def]

   234 

   235   (* nominal *)

   236   permute_eqvt supp_eqvt fresh_eqvt

   237   permute_pure

   238 

   239   (* datatypes *)

   240   permute_prod.simps

   241   fst_eqvt snd_eqvt

   242 

   243   (* sets *)

   244   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt

   245   Diff_eqvt Compl_eqvt insert_eqvt

   246 

   247 thm eqvts

   248 thm eqvts_raw

   249 

   250 text {* helper lemmas for the eqvt_tac *}

   251 

   252 definition

   253   "unpermute p = permute (- p)"

   254 

   255 lemma eqvt_apply:

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

   257   and x :: "'a::pt"

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

   259   unfolding permute_fun_def by simp

   260 

   261 lemma eqvt_lambda:

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

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

   264   unfolding permute_fun_def unpermute_def by simp

   265 

   266 lemma eqvt_bound:

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

   268   unfolding unpermute_def by simp

   269 

   270 use "nominal_permeq.ML"

   271 

   272 

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

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

   275 oops

   276 

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

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

   279 oops

   280 

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

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

   283 oops

   284 

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

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

   287 oops

   288 

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

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

   291 oops

   292 

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

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

   295 oops

   296 

   297 

   298 end