# Theory Atoms

theory Atoms
imports Nominal2_Base
begin
section ‹@{const nat_of} is an example of a function
without finite support›
lemma not_fresh_nat_of:
shows "¬ a ♯ nat_of"
unfolding fresh_def supp_def
proof (clarsimp)
assume "finite {b. (a ⇌ b) ∙ nat_of ≠ nat_of}"
hence "finite ({a} ∪ {b. (a ⇌ b) ∙ nat_of ≠ nat_of})"
by simp
then obtain b where
b1: "b ≠ a" and
b2: "sort_of b = sort_of a" and
b3: "(a ⇌ b) ∙ nat_of = nat_of"
by (rule obtain_atom) auto
have "nat_of a = (a ⇌ b) ∙ (nat_of a)" by (simp add: permute_nat_def)
also have "… = ((a ⇌ b) ∙ nat_of) ((a ⇌ b) ∙ a)" by (simp add: permute_fun_app_eq)
also have "… = nat_of ((a ⇌ b) ∙ a)" using b3 by simp
also have "… = nat_of b" using b2 by simp
finally have "nat_of a = nat_of b" by simp
with b2 have "a = b" by (simp add: atom_components_eq_iff)
with b1 show "False" by simp
qed
lemma supp_nat_of:
shows "supp nat_of = UNIV"
using not_fresh_nat_of [unfolded fresh_def] by auto
section ‹Manual instantiation of class ‹at›.›
typedef name = "{a. sort_of a = Sort ''name'' []}"
by (rule exists_eq_simple_sort)
instantiation name :: at
begin
definition
"p ∙ a = Abs_name (p ∙ Rep_name a)"
definition
"atom a = Rep_name a"
instance
apply (rule at_class)
apply (rule type_definition_name)
apply (rule atom_name_def)
apply (rule permute_name_def)
done
end
lemma sort_of_atom_name:
shows "sort_of (atom (a::name)) = Sort ''name'' []"
by (simp add: atom_name_def Rep_name[simplified])
text ‹Custom syntax for concrete atoms of type at›
term "a:::name"
section ‹Automatic instantiation of class ‹at›.›
atom_decl name2
lemma
"sort_of (atom (a::name2)) ≠ sort_of (atom (b::name))"
by (simp add: sort_of_atom_name)
text ‹example swappings›
lemma
fixes a b::"atom"
assumes "sort_of a = sort_of b"
shows "(a ⇌ b) ∙ (a, b) = (b, a)"
using assms
by simp
lemma
fixes a b::"name2"
shows "(a ↔ b) ∙ (a, b) = (b, a)"
by simp
section ‹An example for multiple-sort atoms›