(* Title: Atoms Authors: Brian Huffman, Christian Urban Instantiations of concrete atoms *)theory Atomsimports Nominal2_Atomsbeginsection {* Manual instantiation of class @{text at}. *}typedef (open) name = "{a. sort_of a = Sort ''name'' []}"by (rule exists_eq_simple_sort)instantiation name :: atbegindefinition "p \<bullet> a = Abs_name (p \<bullet> Rep_name a)"definition "atom a = Rep_name a"instanceapply (rule at_class)apply (rule type_definition_name)apply (rule atom_name_def)apply (rule permute_name_def)doneendlemma sort_of_atom_name: shows "sort_of (atom (a::name)) = Sort ''name'' []" unfolding atom_name_def using Rep_name by simptext {* Custom syntax for concrete atoms of type at *}term "a:::name"text {* a:::name stands for (atom a) with a being of concrete atom type name. The above lemma can therefore also be stated as "sort_of (a:::name) = Sort ''name'' []" This does not work for multi-sorted atoms.*}section {* Automatic instantiation of class @{text at}. *}atom_decl name2lemma sort_of_atom_name2: "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []"unfolding atom_name2_def using Rep_name2 by simptext {* example swappings *}lemma fixes a b::"atom" assumes "sort_of a = sort_of b" shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)"using assmsby simplemma fixes a b::"name2" shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)"by simpsection {* An example for multiple-sort atoms *}datatype ty = TVar string| Fun ty ty ("_ \<rightarrow> _")primrec sort_of_ty::"ty \<Rightarrow> 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 \<longleftrightarrow> x = y"apply(induct x arbitrary: y)apply(case_tac [!] y)apply(simp_all)donedeclare sort_of_ty.simps [simp del]typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}" by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp)instantiation var :: at_basebegindefinition "p \<bullet> a = Abs_var (p \<bullet> Rep_var a)"definition "atom a = Rep_var a"instanceapply (rule at_base_class)apply (rule type_definition_var)apply (rule atom_var_def)apply (rule permute_var_def)doneendtext {* Constructor for variables. *}definition Var :: "nat \<Rightarrow> ty \<Rightarrow> 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 \<longleftrightarrow> x = y \<and> 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 by (simp add: Abs_var_inverse)lemma assumes "\<alpha> \<noteq> \<beta>" shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)" using assms by simptext {* Projecting out the type component of a variable. *}definition ty_of :: "var \<Rightarrow> 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) apply (simp add: inj_on_def sort_of_ty_eq_iff) donelemma ty_of_permute [simp]: shows "ty_of (p \<bullet> x) = ty_of x" unfolding ty_of_def unfolding atom_eqvt [symmetric] by simpend