1102 

  1103 section {* Concrete atoms types *}

  1104 

  1105 class at_base = pt +

  1106   fixes atom :: "'a \<Rightarrow> atom"

  1107   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"

  1108   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"

  1109 

  1110 class at = at_base +

  1111   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"

  1112 

  1113 lemma supp_at_base: 

  1114   fixes a::"'a::at_base"

  1115   shows "supp a = {atom a}"

  1116   by (simp add: supp_atom [symmetric] supp_def atom_eqvt)

  1117 

  1118 lemma fresh_at_base: 

  1119   shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"

  1120   unfolding fresh_def by (simp add: supp_at_base)

  1121 

  1122 instance at_base < fs

  1123 proof qed (simp add: supp_at_base)

  1124 

  1125 lemma at_base_infinite [simp]:

  1126   shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U")

  1127 proof

  1128   obtain a :: 'a where "True" by auto

  1129   assume "finite ?U"

  1130   hence "finite (atom ` ?U)"

  1131     by (rule finite_imageI)

  1132   then obtain b where b: "b \<notin> atom ` ?U" "sort_of b = sort_of (atom a)"

  1133     by (rule obtain_atom)

  1134   from b(2) have "b = atom ((atom a \<rightleftharpoons> b) \<bullet> a)"

  1135     unfolding atom_eqvt [symmetric]

  1136     by (simp add: swap_atom)

  1137   hence "b \<in> atom ` ?U" by simp

  1138   with b(1) show "False" by simp

  1139 qed

  1140 

  1141 lemma swap_at_base_simps [simp]:

  1142   fixes x y::"'a::at_base"

  1143   shows "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> x = y"

  1144   and   "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> y = x"

  1145   and   "atom x \<noteq> a \<Longrightarrow> atom x \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x"

  1146   unfolding atom_eq_iff [symmetric]

  1147   unfolding atom_eqvt [symmetric]

  1148   by simp_all

  1149 

  1150 lemma obtain_at_base:

  1151   assumes X: "finite X"

  1152   obtains a::"'a::at_base" where "atom a \<notin> X"

  1153 proof -

  1154   have "inj (atom :: 'a \<Rightarrow> atom)"

  1155     by (simp add: inj_on_def)

  1156   with X have "finite (atom -` X :: 'a set)"

  1157     by (rule finite_vimageI)

  1158   with at_base_infinite have "atom -` X \<noteq> (UNIV :: 'a set)"

  1159     by auto

  1160   then obtain a :: 'a where "atom a \<notin> X"

  1161     by auto

  1162   thus ?thesis ..

  1163 qed

  1164