--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal-General/Atoms.thy	Sun Apr 04 21:39:28 2010 +0200
@@ -0,0 +1,164 @@
+(*  Title:      Atoms
+    Authors:    Brian Huffman, Christian Urban
+
+    Instantiations of concrete atoms 
+*)
+theory Atoms
+imports Nominal2_Atoms
+begin
+
+section {* Manual instantiation of class @{text at}. *}
+
+typedef (open) name = "{a. sort_of a = Sort ''name'' []}"
+by (rule exists_eq_simple_sort)
+
+instantiation name :: at
+begin
+
+definition
+  "p \<bullet> a = Abs_name (p \<bullet> 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'' []"
+  unfolding atom_name_def using Rep_name by simp
+
+text {* 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 name2
+
+lemma sort_of_atom_name2:
+  "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []"
+unfolding atom_name2_def 
+using Rep_name2 
+by simp
+
+text {* example swappings *}
+lemma
+  fixes a b::"atom"
+  assumes "sort_of a = sort_of b"
+  shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)"
+using assms
+by simp
+
+lemma
+  fixes a b::"name2"
+  shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)"
+by simp
+
+section {* 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)
+done
+
+declare 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_base
+begin
+
+definition
+  "p \<bullet> a = Abs_var (p \<bullet> 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 \<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 simp
+
+text {* 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)
+  done
+
+lemma ty_of_permute [simp]:
+  shows "ty_of (p \<bullet> x) = ty_of x"
+  unfolding ty_of_def
+  unfolding atom_eqvt [symmetric]
+  by simp
+
+end