defined height as a function that returns an integer
(* Title: Atoms Authors: Brian Huffman, Christian Urban Instantiations of concrete atoms *)theory Atomsimports Nominal2_Baseuses "~~/src/Tools/subtyping.ML"beginsection {* @{const nat_of} is an example of a function without finite support *}lemma not_fresh_nat_of: shows "\<not> a \<sharp> nat_of"unfolding fresh_def supp_defproof (clarsimp) assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}" hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})" by simp then obtain b where b1: "b \<noteq> a" and b2: "sort_of b = sort_of a" and b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of" by (rule obtain_atom) auto have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def) also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq) also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp also have "\<dots> = 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 simpqedlemma supp_nat_of: shows "supp nat_of = UNIV" using not_fresh_nat_of [unfolded fresh_def] by autosection {* 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 simpsection {* Tests with subtyping and automatic coercions *}declare [[coercion_enabled]]atom_decl var1atom_decl var2declare [[coercion "atom::var1\<Rightarrow>atom"]]declare [[coercion "atom::var2\<Rightarrow>atom"]]lemma fixes a::"var1" and b::"var2" shows "a \<sharp> t \<and> b \<sharp> t"oops(* does not yet work: it needs image as coercion map *)lemma fixes as::"var1 set" shows "atom ` as \<sharp>* t"oopsend