10 uses ("nominal_thmdecls.ML")

    11      ("nominal_permeq.ML")

    12      ("nominal_eqvt.ML")

    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 ex1_eqvt imp_eqvt uminus_eqvt

    28   imp_eqvt[folded induct_implies_def]

    29   all_eqvt[folded induct_forall_def]

    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 permute_option.simps 

    37   permute_sum.simps

    38 

    39   (* sets *)

    40   mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt

    41 

    42   (* fsets *)

    43   permute_fset fset_eqvt

    44 

    45 

    46 text {* helper lemmas for the perm_simp *}

    47 

    48 definition

    49   "unpermute p = permute (- p)"

    50 

    51 lemma eqvt_apply:

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

    53   and x :: "'a::pt"

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

    55   unfolding permute_fun_def by simp

    56 

    57 lemma eqvt_lambda:

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

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

    60   unfolding permute_fun_def unpermute_def by simp

    61 

    62 lemma eqvt_bound:

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

    64   unfolding unpermute_def by simp

    65 

    66 text {* provides perm_simp methods *}

    67 

    68 use "nominal_permeq.ML"

    69 setup Nominal_Permeq.setup

    70 

    71 method_setup perm_simp =

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

    73  {* pushes permutations inside. *}

    74 

    75 method_setup perm_strict_simp =

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

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

    78 

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

    80 lemma permute_eqvt_raw[eqvt_raw]:

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

    82 apply(simp add: fun_eq_iff permute_fun_def)

    83 apply(subst permute_eqvt)

    84 apply(simp)

    85 done

    86 

    87 subsection {* Equivariance of Logical Operators *}

    88 

    89 lemma eq_eqvt[eqvt]:

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

    91   unfolding permute_eq_iff permute_bool_def ..

    92 

    93 lemma if_eqvt[eqvt]:

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

    95   by (simp add: permute_fun_def permute_bool_def)

    96 

    97 lemma True_eqvt[eqvt]:

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

    99   unfolding permute_bool_def ..

   100 

   101 lemma False_eqvt[eqvt]:

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

   103   unfolding permute_bool_def ..

   104 

   105 lemma disj_eqvt[eqvt]:

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

   107   by (simp add: permute_bool_def)

   108 

   109 lemma all_eqvt2:

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

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

   112 

   113 lemma ex_eqvt2:

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

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

   116 

   117 lemma ex1_eqvt2:

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

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

   120 

   121 lemma the_eqvt:

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

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

   124   apply(rule the1_equality [symmetric])

   125   apply(rule_tac p="-p" in permute_boolE)

   126   apply(perm_simp add: permute_minus_cancel)

   127   apply(rule unique)

   128   apply(rule_tac p="-p" in permute_boolE)

   129   apply(perm_simp add: permute_minus_cancel)

   130   apply(rule theI'[OF unique])

   131   done

   132 

   133 lemma the_eqvt2:

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

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

   136   apply(rule the1_equality [symmetric])

   137   apply(simp add: ex1_eqvt2[symmetric])

   138   apply(simp add: permute_bool_def unique)

   139   apply(simp add: permute_bool_def)

   140   apply(rule theI'[OF unique])

   141   done

   142 

   143 subsection {* Equivariance Set Operations *}

   144 

   145 lemma not_mem_eqvt:

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

   147   by (perm_simp) (rule refl)

   148 

   149 lemma Collect_eqvt[eqvt]:

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

   151   unfolding Collect_def permute_fun_def ..

   152 

   153 lemma Collect_eqvt2:

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

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

   156 

   157 lemma Bex_eqvt[eqvt]:

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

   159   unfolding Bex_def

   160   by (perm_simp) (rule refl)

   161 

   162 lemma Ball_eqvt[eqvt]:

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

   164   unfolding Ball_def

   165   by (perm_simp) (rule refl)

   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 Diff_eqvt[eqvt]:

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

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

   180   unfolding set_diff_eq

   181   by (perm_simp) (rule refl)

   182 

   183 lemma Compl_eqvt[eqvt]:

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

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

   186   unfolding Compl_eq_Diff_UNIV

   187   by (perm_simp) (rule refl)

   188 

   189 lemma subset_eqvt[eqvt]:

   190   shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"

   191   unfolding subset_eq

   192   by (perm_simp) (rule refl)

   193 

   194 lemma psubset_eqvt[eqvt]:

   195   shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"

   196   unfolding psubset_eq

   197   by (perm_simp) (rule refl)

   198 

   199 lemma image_eqvt[eqvt]:

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

   201   unfolding permute_set_eq_image

   202   unfolding permute_fun_def [where f=f]

   203   by (simp add: image_image)

   204 

   205 lemma vimage_eqvt[eqvt]:

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

   207   unfolding vimage_def

   208   by (perm_simp) (rule refl)

   209 

   210 lemma Union_eqvt[eqvt]:

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

   212   unfolding Union_eq 

   213   by (perm_simp) (rule refl)

   214 

   215 lemma Sigma_eqvt:

   216   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"

   217 unfolding Sigma_def

   218 unfolding UNION_eq_Union_image

   219 by (perm_simp) (rule refl)

   220 

   221 lemma finite_permute_iff:

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

   223   unfolding permute_set_eq_vimage

   224   using bij_permute by (rule finite_vimage_iff)

   225 

   226 lemma finite_eqvt[eqvt]:

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

   228   unfolding finite_permute_iff permute_bool_def ..

   229 

   230 

   231 section {* List Operations *}

   232 

   233 lemma append_eqvt[eqvt]:

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

   235   by (induct xs) auto

   236 

   237 lemma rev_eqvt[eqvt]:

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

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

   240 

   241 lemma supp_rev:

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

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

   244 

   245 lemma fresh_rev:

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

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

   248 

   249 lemma map_eqvt[eqvt]: 

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

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

   252 

   253 lemma removeAll_eqvt[eqvt]:

   254   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"

   255   by (induct xs) (auto)

   256 

   257 lemma supp_removeAll:

   258   fixes x::"atom"

   259   shows "supp (removeAll x xs) = supp xs - {x}"

   260   by (induct xs)

   261      (auto simp add: supp_Nil supp_Cons supp_atom)

   262 

   263 lemma filter_eqvt[eqvt]:

   264   shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"

   265 apply(induct xs)

   266 apply(simp)

   267 apply(simp only: filter.simps permute_list.simps if_eqvt)

   268 apply(simp only: permute_fun_app_eq)

   269 done

   270 

   271 lemma distinct_eqvt[eqvt]:

   272   shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"

   273 apply(induct xs)

   274 apply(simp add: permute_bool_def)

   275 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)

   276 done

   277 

   278 lemma length_eqvt[eqvt]:

   279   shows "p \<bullet> (length xs) = length (p \<bullet> xs)"

   280 by (induct xs) (simp_all add: permute_pure)

   281 

   282 

   283 subsection {* Equivariance Finite-Set Operations *}

   284 

   285 lemma in_fset_eqvt[eqvt]:

   286   shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"

   287 unfolding in_fset

   288 by (perm_simp) (simp)

   289 

   290 lemma union_fset_eqvt[eqvt]:

   291   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"

   292 by (induct S) (simp_all)

   293 

   294 lemma supp_union_fset:

   295   fixes S T::"'a::fs fset"

   296   shows "supp (S |\<union>| T) = supp S \<union> supp T"

   297 by (induct S) (auto)

   298 

   299 lemma fresh_union_fset:

   300   fixes S T::"'a::fs fset"

   301   shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"

   302 unfolding fresh_def

   303 by (simp add: supp_union_fset)

   304 

   305 lemma map_fset_eqvt[eqvt]: 

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

   307   by (lifting map_eqvt)

   308 

   309 

   310 subsection {* Product Operations *}

   311 

   312 lemma fst_eqvt[eqvt]:

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

   314  by (cases x) simp

   315 

   316 lemma snd_eqvt[eqvt]:

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

   318  by (cases x) simp

   319 

   320 lemma split_eqvt[eqvt]: 

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

   322   unfolding split_def

   323   by (perm_simp) (rule refl)

   324 

   325 

   326 section {* Test cases *}