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 3219 e5d9b6bca88c
parent 3218 89158f401b07
child 3221 ea327a4c4f43
equal deleted inserted replaced
3218:89158f401b07 3219:e5d9b6bca88c 
   352   fixes p q :: "perm"
 
   352   fixes p q :: "perm"
 
   353   shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)"
 
   353   shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)"
 
   354   unfolding permute_atom_def
 
   354   unfolding permute_atom_def
 
   355   by (metis Rep_perm_ext ext)
 
   355   by (metis Rep_perm_ext ext)
 
   356 
   356 
   357 
       
   358 subsection {* Permutations for permutations *}
 
   357 subsection {* Permutations for permutations *}
 
   359 
   358 
   360 instantiation perm :: pt
 
   359 instantiation perm :: pt
 
   361 begin
 
   360 begin
 
   362 
   361 
   998   by (perm_simp) (rule refl)
 
   997   by (perm_simp) (rule refl)
 
   999 
   998 
  1000 lemma union_eqvt [eqvt]:
 
   999 lemma union_eqvt [eqvt]:
 
  1001   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
 
  1000   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
 
  1002   unfolding Un_def by simp
 
  1001   unfolding Un_def by simp
 
       
  1002 
       
  1003 lemma UNION_eqvt [eqvt]:
 
       
  1004   shows "p \<bullet> (UNION A f) = (UNION (p \<bullet> A) (p \<bullet> f))"
 
       
  1005 unfolding UNION_eq
 
       
  1006 by (perm_simp) (simp)
 
  1003 
  1007 
  1004 lemma Diff_eqvt [eqvt]:
 
  1008 lemma Diff_eqvt [eqvt]:
 
  1005   fixes A B :: "'a::pt set"
 
  1009   fixes A B :: "'a::pt set"
 
  1006   shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
 
  1010   shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
 
  1007   unfolding set_diff_eq by simp
 
  1011   unfolding set_diff_eq by simp
 
  1601     by blast
 
  1605     by blast
 
  1602   then show "supp (p + q) = supp p \<union> supp q" using supp_plus_perm
 
  1606   then show "supp (p + q) = supp p \<union> supp q" using supp_plus_perm
 
  1603     by blast
 
  1607     by blast
 
  1604 qed
 
  1608 qed
 
  1605 
  1609 
       
  1610 lemma perm_eq_iff2:
 
       
  1611   fixes p q :: "perm"
 
       
  1612   shows "p = q \<longleftrightarrow> (\<forall>a::atom \<in> supp p \<union> supp q. p \<bullet> a = q \<bullet> a)"
 
       
  1613   unfolding perm_eq_iff
 
       
  1614   apply(auto)
 
       
  1615   apply(case_tac "a \<sharp> p \<and> a \<sharp> q")
 
       
  1616   apply(simp add: fresh_perm)
 
       
  1617   apply(simp add: fresh_def)
 
       
  1618   done
 
       
  1619 
       
  1620 
  1606 instance perm :: fs
 
  1621 instance perm :: fs
 
  1607 by default (simp add: supp_perm finite_perm_lemma)
 
  1622 by default (simp add: supp_perm finite_perm_lemma)
 
  1608 
  1623 
  1609 
  1624 
  1610 
  1625 
  2015 lemma Union_included_in_supp:
 
  2030 lemma Union_included_in_supp:
 
  2016   fixes S::"('a::fs set)"
 
  2031   fixes S::"('a::fs set)"
 
  2017   assumes fin: "finite S"
 
  2032   assumes fin: "finite S"
 
  2018   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 
  2033   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 
  2019 proof -
 
  2034 proof -
 
  2020   have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
  2035   have eqvt: "eqvt (\<lambda>S. \<Union>x \<in> S. supp x)" 
  2021     unfolding eqvt_def 
  2036     unfolding eqvt_def by simp 
  2022     by (perm_simp) (simp)
 
       
  2023   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
 
  2037   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
 
  2024     by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
 
  2038     by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
 
  2025   also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
 
       
  2026   also have "\<dots> \<subseteq> supp S" using eqvt
 
  2039   also have "\<dots> \<subseteq> supp S" using eqvt
 
  2027     by (rule supp_fun_app_eqvt)
 
  2040     by (rule supp_fun_app_eqvt)
 
  2028   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 
  2041   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .  
  2029 qed
 
  2042 qed
 
  2030 
  2043 
  2031 lemma supp_of_finite_sets:
 
  2044 lemma supp_of_finite_sets:
 
  2032   fixes S::"('a::fs set)"
 
  2045   fixes S::"('a::fs set)"
 
  2033   assumes fin: "finite S"
 
  2046   assumes fin: "finite S"
nominal2