Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2_Base.thy
changeset 3104 f7c4b8e6918b
parent 3101 09acd7e116e8
child 3121 878de0084b62
equal deleted inserted replaced
3103:9a63d90d1752 3104:f7c4b8e6918b 
   428   shows "P \<Longrightarrow> p \<bullet> P"
 
   428   shows "P \<Longrightarrow> p \<bullet> P"
 
   429   by(simp add: permute_bool_def)
 
   429   by(simp add: permute_bool_def)
 
   430 
   430 
   431 subsection {* Permutations for sets *}
 
   431 subsection {* Permutations for sets *}
 
   432 
   432 
       
   433 instantiation "set" :: (pt) pt
 
       
   434 begin
 
       
   435 
       
   436 definition
 
       
   437   "p \<bullet> X = {p \<bullet> x | x. x \<in> X}" 
       
   438 
       
   439 instance
 
       
   440 apply default
 
       
   441 apply (auto simp add: permute_set_def)
 
       
   442 done
 
       
   443 
       
   444 end
 
       
   445 
   433 lemma permute_set_eq:
 
   446 lemma permute_set_eq:
 
   434   fixes x::"'a::pt"
 
   447   shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}"
 
   435   shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
 
   448 unfolding permute_set_def
 
   436   unfolding permute_fun_def
 
   449 by (auto) (metis permute_minus_cancel(1))
 
   437   unfolding permute_bool_def
 
       
   438   apply(auto simp add: mem_def)
 
       
   439   apply(rule_tac x="- p \<bullet> x" in exI)
 
       
   440   apply(simp)
 
       
   441   done
 
       
   442 
   450 
   443 lemma permute_set_eq_image:
 
   451 lemma permute_set_eq_image:
 
   444   shows "p \<bullet> X = permute p ` X"
 
   452   shows "p \<bullet> X = permute p ` X"
 
   445   unfolding permute_set_eq by auto
 
   453   unfolding permute_set_def by auto
 
   446 
   454 
   447 lemma permute_set_eq_vimage:
 
   455 lemma permute_set_eq_vimage:
 
   448   shows "p \<bullet> X = permute (- p) -` X"
 
   456   shows "p \<bullet> X = permute (- p) -` X"
 
   449   unfolding permute_fun_def permute_bool_def
 
   457   unfolding permute_set_eq vimage_def
 
   450   unfolding vimage_def Collect_def mem_def ..
 
   458   by simp
 
   451 
   459   
   452 lemma permute_finite [simp]:
 
   460 lemma permute_finite [simp]:
 
   453   shows "finite (p \<bullet> X) = finite X"
 
   461   shows "finite (p \<bullet> X) = finite X"
 
   454   unfolding permute_set_eq_vimage
 
   462   unfolding permute_set_eq_vimage
 
   455   using bij_permute by (rule finite_vimage_iff)
 
   463   using bij_permute by (rule finite_vimage_iff)
 
   456 
   464 
   457 lemma swap_set_not_in:
 
   465 lemma swap_set_not_in:
 
   458   assumes a: "a \<notin> S" "b \<notin> S"
 
   466   assumes a: "a \<notin> S" "b \<notin> S"
 
   459   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
 
   467   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
 
   460   unfolding permute_set_eq
 
   468   unfolding permute_set_def
 
   461   using a by (auto simp add: swap_atom)
 
   469   using a by (auto simp add: swap_atom)
 
   462 
   470 
   463 lemma swap_set_in:
 
   471 lemma swap_set_in:
 
   464   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
 
   472   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
 
   465   shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
 
   473   shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
 
   466   unfolding permute_set_eq
 
   474   unfolding permute_set_def
 
   467   using a by (auto simp add: swap_atom)
 
   475   using a by (auto simp add: swap_atom)
 
   468 
   476 
   469 lemma swap_set_in_eq:
 
   477 lemma swap_set_in_eq:
 
   470   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
 
   478   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
 
   471   shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
 
   479   shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
 
   472   unfolding permute_set_eq
 
   480   unfolding permute_set_def
 
   473   using a by (auto simp add: swap_atom)
 
   481   using a by (auto simp add: swap_atom)
 
   474 
   482 
   475 lemma swap_set_both_in:
 
   483 lemma swap_set_both_in:
 
   476   assumes a: "a \<in> S" "b \<in> S"
 
   484   assumes a: "a \<in> S" "b \<in> S"
 
   477   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
 
   485   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
 
   478   unfolding permute_set_eq
 
   486   unfolding permute_set_def
 
   479   using a by (auto simp add: swap_atom)
 
   487   using a by (auto simp add: swap_atom)
 
   480 
   488 
   481 lemma mem_permute_iff:
 
   489 lemma mem_permute_iff:
 
   482   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
 
   490   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
 
   483   unfolding mem_def permute_fun_def permute_bool_def
 
   491   unfolding permute_set_def
 
   484   by simp
 
   492   by auto
 
   485 
   493 
   486 lemma empty_eqvt:
 
   494 lemma empty_eqvt:
 
   487   shows "p \<bullet> {} = {}"
 
   495   shows "p \<bullet> {} = {}"
 
   488   unfolding empty_def Collect_def
 
   496   unfolding permute_set_def
 
   489   by (simp add: permute_fun_def permute_bool_def)
 
   497   by (simp)
 
   490 
   498 
   491 lemma insert_eqvt:
 
   499 lemma insert_eqvt:
 
   492   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
 
   500   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
 
   493   unfolding permute_set_eq_image image_insert ..
 
   501   unfolding permute_set_eq_image image_insert ..
 
   494 
   502 
   662 
   670 
   663 text {* Other type constructors preserve purity. *}
 
   671 text {* Other type constructors preserve purity. *}
 
   664 
   672 
   665 instance "fun" :: (pure, pure) pure
 
   673 instance "fun" :: (pure, pure) pure
 
   666 by default (simp add: permute_fun_def permute_pure)
 
   674 by default (simp add: permute_fun_def permute_pure)
 
       
   675 
       
   676 instance set :: (pure) pure
 
       
   677 by default (simp add: permute_set_def permute_pure)
 
   667 
   678 
   668 instance prod :: (pure, pure) pure
 
   679 instance prod :: (pure, pure) pure
 
   669 by default (induct_tac x, simp add: permute_pure)
 
   680 by default (induct_tac x, simp add: permute_pure)
 
   670 
   681 
   671 instance sum :: (pure, pure) pure
 
   682 instance sum :: (pure, pure) pure
 
   877 
   888 
   878 subsubsection {* Equivariance of Set operators *}
 
   889 subsubsection {* Equivariance of Set operators *}
 
   879 
   890 
   880 lemma mem_eqvt [eqvt]:
 
   891 lemma mem_eqvt [eqvt]:
 
   881   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
 
   892   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
 
   882   unfolding mem_def
 
   893   unfolding permute_bool_def permute_set_def
 
   883   by (rule permute_fun_app_eq)
 
   894   by (auto)
 
   884 
   895 
   885 lemma Collect_eqvt [eqvt]:
 
   896 lemma Collect_eqvt [eqvt]:
 
   886   shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
 
   897   shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
 
   887   unfolding Collect_def permute_fun_def ..
 
   898   unfolding permute_set_eq permute_fun_def
 
       
   899   by (auto simp add: permute_bool_def)
 
   888 
   900 
   889 lemma inter_eqvt [eqvt]:
 
   901 lemma inter_eqvt [eqvt]:
 
   890   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
 
   902   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
 
   891   unfolding Int_def
 
   903   unfolding Int_def
 
   892   by (perm_simp) (rule refl)
 
   904   by (perm_simp) (rule refl)
 
  1869 lemma Union_supports_set:
 
  1881 lemma Union_supports_set:
 
  1870   shows "(\<Union>x \<in> S. supp x) supports S"
 
  1882   shows "(\<Union>x \<in> S. supp x) supports S"
 
  1871 proof -
 
  1883 proof -
 
  1872   { fix a b
 
  1884   { fix a b
 
  1873     have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
 
  1885     have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
 
  1874       unfolding permute_set_eq by force
 
  1886       unfolding permute_set_def by force
 
  1875   }
 
  1887   }
 
  1876   then show "(\<Union>x \<in> S. supp x) supports S"
 
  1888   then show "(\<Union>x \<in> S. supp x) supports S"
 
  1877     unfolding supports_def 
  1889     unfolding supports_def 
  1878     by (simp add: fresh_def[symmetric] swap_fresh_fresh)
 
  1890     by (simp add: fresh_def[symmetric] swap_fresh_fresh)
 
  1879 qed
 
  1891 qed
 
  2489   have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
 
  2501   have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
 
  2490   obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
 
  2502   obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
 
  2491     using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
 
  2503     using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
 
  2492   have c: "(p \<bullet> a) \<sharp> c" using p1
 
  2504   have c: "(p \<bullet> a) \<sharp> c" using p1
 
  2493     unfolding fresh_star_def Ball_def 
  2505     unfolding fresh_star_def Ball_def 
  2494     by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
 
  2506     by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_def)
 
  2495   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
 
  2507   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
 
  2496   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 
  2508   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 
  2497 qed
 
  2509 qed
 
  2498 
  2510 
  2499 
  2511 
  2504   shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
 
  2516   shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
 
  2505 using b
 
  2517 using b
 
  2506 proof (induct)
 
  2518 proof (induct)
 
  2507   case empty
 
  2519   case empty
 
  2508   have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
 
  2520   have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
 
  2509     by (simp add: permute_set_eq supp_perm)
 
  2521     by (simp add: permute_set_def supp_perm)
 
  2510   then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
 
  2522   then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
 
  2511 next
 
  2523 next
 
  2512   case (insert a bs)
 
  2524   case (insert a bs)
 
  2513   then have " \<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" by simp 
  2525   then have " \<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" by simp 
  2514   then obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs"
 
  2526   then obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs"
nominal2