# Theory Atoms

```(*  Title:      Atoms
Authors:    Brian Huffman, Christian Urban

Instantiations of concrete 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'' []"

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))"

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›

datatype ty =
TVar string
| Fun ty ty ("_ → _")

primrec
sort_of_ty::"ty ⇒ atom_sort"
where
"sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]"
| "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]"

lemma sort_of_ty_eq_iff:
shows "sort_of_ty x = sort_of_ty y ⟷ x = y"
apply(induct x arbitrary: y)
apply(case_tac [!] y)
apply(simp_all)
done

declare sort_of_ty.simps [simp del]

typedef var = "{a. sort_of a ∈ range sort_of_ty}"
by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp)

instantiation var :: at_base
begin

definition
"p ∙ a = Abs_var (p ∙ Rep_var a)"

definition
"atom a = Rep_var a"

instance
apply (rule at_base_class)
apply (rule type_definition_var)
apply (rule atom_var_def)
apply (rule permute_var_def)
done

end

text ‹Constructor for variables.›

definition
Var :: "nat ⇒ ty ⇒ var"
where
"Var x t = Abs_var (Atom (sort_of_ty t) x)"

lemma Var_eq_iff [simp]:
shows "Var x s = Var y t ⟷ x = y ∧ s = t"
unfolding Var_def
by (auto simp add: Abs_var_inject sort_of_ty_eq_iff)

lemma sort_of_atom_var [simp]:
"sort_of (atom (Var n ty)) = sort_of_ty ty"
unfolding atom_var_def Var_def

lemma
assumes "α ≠ β"
shows "(Var x α ↔ Var y α) ∙ (Var x α, Var x β) = (Var y α, Var x β)"
using assms by simp

text ‹Projecting out the type component of a variable.›

definition
ty_of :: "var ⇒ ty"
where
"ty_of x = inv sort_of_ty (sort_of (atom x))"

text ‹
Functions @{term Var}/@{term ty_of} satisfy many of the same
properties as @{term Atom}/@{term sort_of}.
›

lemma ty_of_Var [simp]:
shows "ty_of (Var x t) = t"
unfolding ty_of_def
unfolding sort_of_atom_var
apply (rule inv_f_f)
done

lemma ty_of_permute [simp]:
shows "ty_of (p ∙ x) = ty_of x"
unfolding ty_of_def
unfolding atom_eqvt [symmetric]
by (simp only: sort_of_permute)

section ‹Tests with subtyping and automatic coercions›

declare [[coercion_enabled]]

atom_decl var1
atom_decl var2

declare [[coercion "atom::var1⇒atom"]]

declare [[coercion "atom::var2⇒atom"]]

lemma
fixes a::"var1" and b::"var2"
shows "a ♯ t ∧ b ♯ t"
oops

(* does not yet work: it needs image as
coercion map *)

lemma
fixes as::"var1 set"
shows "atom ` as ♯* t"

oops

end
```