src/HOL/Nominal/Examples/Support.thy

 theory Support 
   imports "../Nominal" 
 begin
 
-text {* 
+text \<open>
   An example showing that in general
 
   x\<sharp>(A \<union> B) does not imply  x\<sharp>A and  x\<sharp>B
 
   For this we set A to the set of even atoms and B to 
   the set of odd atoms. Then A \<union> B, that is the set of 
   all atoms, has empty support. The sets A, respectively B, 
   however have the set of all atoms as their support. 
-*}
+\<close>
 
 atom_decl atom
 
-text {* The set of even atoms. *}
+text \<open>The set of even atoms.\<close>
 abbreviation
   EVEN :: "atom set"
 where
   "EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}"
 
-text {* The set of odd atoms: *}
+text \<open>The set of odd atoms:\<close>
 abbreviation  
   ODD :: "atom set"
 where
   "ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}"
 
-text {* An atom is either even or odd. *}
+text \<open>An atom is either even or odd.\<close>
 lemma even_or_odd:
   fixes n :: nat
   shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
   by (induct n) (presburger)+
 
-text {* 
+text \<open>
   The union of even and odd atoms is the set of all atoms. 
-  (Unfortunately I do not know a simpler proof of this fact.) *}
+  (Unfortunately I do not know a simpler proof of this fact.)\<close>
 lemma EVEN_union_ODD:
   shows "EVEN \<union> ODD = UNIV"
   using even_or_odd
 proof -
   have "EVEN \<union> ODD = (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i} \<union> (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i+1}" by auto

   also have "\<dots> = (UNIV::atom set)" using atom.exhaust
     by (auto simp add: surj_def)
   finally show "EVEN \<union> ODD = UNIV" by simp
 qed
 
-text {* The sets of even and odd atoms are disjunct. *}
+text \<open>The sets of even and odd atoms are disjunct.\<close>
 lemma EVEN_intersect_ODD:
   shows "EVEN \<inter> ODD = {}"
   using even_or_odd
   by (auto) (presburger)
 
-text {* 
+text \<open>
   The preceeding two lemmas help us to prove 
-  the following two useful equalities: *}
+  the following two useful equalities:\<close>
 
 lemma UNIV_subtract:
   shows "UNIV - EVEN = ODD"
   and   "UNIV - ODD  = EVEN"
   using EVEN_union_ODD EVEN_intersect_ODD
   by (blast)+
 
-text {* The sets EVEN and ODD are infinite. *}
+text \<open>The sets EVEN and ODD are infinite.\<close>
 lemma EVEN_ODD_infinite:
   shows "infinite EVEN"
   and   "infinite ODD"
 unfolding infinite_iff_countable_subset
 proof -

   let ?f = "\<lambda>n. atom (2*n+1)"
   have "inj ?f \<and> range ?f \<subseteq> ODD" by (auto simp add: inj_on_def)
   then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> ODD" by (rule_tac exI)
 qed
 
-text {* 
+text \<open>
   A general fact about a set S of atoms that is both infinite and 
   coinfinite. Then S has all atoms as its support. Steve Zdancewic 
-  helped with proving this fact. *}
+  helped with proving this fact.\<close>
 
 lemma supp_infinite_coinfinite:
   fixes S::"atom set"
   assumes asm1: "infinite S"
   and     asm2: "infinite (UNIV-S)"

     qed
   qed
   then show "(supp S) = (UNIV::atom set)" by auto
 qed
 
-text {* As a corollary we get that EVEN and ODD have infinite support. *}
+text \<open>As a corollary we get that EVEN and ODD have infinite support.\<close>
 lemma EVEN_ODD_supp:
   shows "supp EVEN = (UNIV::atom set)"
   and   "supp ODD  = (UNIV::atom set)"
   using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite
   by simp_all
 
-text {* 
+text \<open>
   The set of all atoms has empty support, since any swappings leaves 
-  this set unchanged. *}
+  this set unchanged.\<close>
 
 lemma UNIV_supp:
   shows "supp (UNIV::atom set) = ({}::atom set)"
 proof -
   have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
     by (auto simp add: perm_set_def calc_atm)
   then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
 qed
 
-text {* Putting everything together. *}
+text \<open>Putting everything together.\<close>
 theorem EVEN_ODD_freshness:
   fixes x::"atom"
   shows "x\<sharp>(EVEN \<union> ODD)"
   and   "\<not>x\<sharp>EVEN"
   and   "\<not>x\<sharp>ODD"
   by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)
 
-text {* Moral: support is a sublte notion. *}
+text \<open>Moral: support is a sublte notion.\<close>
 
 end