18 

    19 class at_base = pt +

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

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

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

    23 

    24 declare atom_eqvt[eqvt]

    25 

    26 class at = at_base +

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

    28 

    29 lemma supp_at_base: 

    30   fixes a::"'a::at_base"

    31   shows "supp a = {atom a}"

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

    33 

    34 lemma fresh_at_base: 

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

    36   unfolding fresh_def by (simp add: supp_at_base)

    37 

    38 instance at_base < fs

    39 proof qed (simp add: supp_at_base)

    40 

    41 lemma at_base_infinite [simp]:

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

    43 proof

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

    45   assume "finite ?U"

    46   hence "finite (atom ` ?U)"

    47     by (rule finite_imageI)

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

    49     by (rule obtain_atom)

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

    51     unfolding atom_eqvt [symmetric]

    52     by (simp add: swap_atom)

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

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

    55 qed

    56 

    57 lemma swap_at_base_simps [simp]:

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

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

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

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

    62   unfolding atom_eq_iff [symmetric]

    63   unfolding atom_eqvt [symmetric]

    64   by simp_all

    65 

    66 lemma obtain_at_base:

    67   assumes X: "finite X"

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

    69 proof -

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

    71     by (simp add: inj_on_def)

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

    73     by (rule finite_vimageI)

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

    75     by auto

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

    77     by auto

    78   thus ?thesis ..

    79 qed