Do not use atoms for data and constructor names

Author: jvanbruegge

Syntax.thy

@@ -5,8 +5,19 @@ begin
 atom_decl "var"
 atom_decl "tyvar"
 
-atom_decl "data_name"
-atom_decl "ctor_name"
+typedef data_name = "{ x. x \<in> (UNIV :: string set) }" by simp
+typedef ctor_name = "{ x. x \<in> (UNIV :: string set) }" by simp
+
+instantiation data_name :: pure
+begin
+  definition "p \<bullet> (x::data_name) = x"
+  instance by (standard, auto simp: permute_data_name_def)
+end
+instantiation ctor_name :: pure
+begin
+  definition "p \<bullet> (x::ctor_name) = x"
+  instance by (standard, auto simp: permute_ctor_name_def)
+end
 
 nominal_datatype "\<kappa>" =
   Star ("\<star>")
@@ -42,6 +53,8 @@ nominal_datatype "axiom" =
 type_synonym "\<Gamma>" = "binder list"
 type_synonym "\<Delta>" = "axiom list"
 
+declare pure_fresh[simp]
+
 lemma no_vars_in_kinds[simp]: "atom (x :: var) \<sharp> (k :: \<kappa>)"
   by (induction k rule: \<kappa>.induct) auto
 lemma no_vars_in_ty[simp]: "atom (x :: var) \<sharp> (ty :: \<tau>)"
@@ -64,12 +77,13 @@ lemma supp_empty_kinds[simp]: "supp (k :: \<kappa>) = {}"
   by (induction k rule: \<kappa>.induct) (auto simp: \<kappa>.supp)
 
 lemma perm_data_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (T :: data_name) = T"
-  using flip_fresh_fresh by force
+  using flip_fresh_fresh pure_fresh by blast
 lemma perm_data_name_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (T :: data_name) = T"
-  using flip_fresh_fresh by force
+  using flip_fresh_fresh pure_fresh by blast
 lemma perm_ctor_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (D :: ctor_name) = D"
-  using flip_fresh_fresh by force
+  using flip_fresh_fresh pure_fresh by blast
 lemma perm_ctor_name_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (D :: ctor_name) = D"
-  using flip_fresh_fresh by force
+  using flip_fresh_fresh pure_fresh by blast
+
 
 end

Typing.thy

@@ -10,9 +10,9 @@ inductive Ax :: "\<Delta> \<Rightarrow> bool" ("\<turnstile> _")
 
   Ax_Empty: "\<turnstile> []"
 
-| Ax_Data: "\<lbrakk> \<turnstile> \<Delta> ; atom T \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxData T \<kappa> # \<Delta>"
+| Ax_Data: "\<lbrakk> \<turnstile> \<Delta> ; \<nexists>k. AxData T k \<in> set \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxData T \<kappa> # \<Delta>"
 
-| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some T ; atom D \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
+| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some T ; \<nexists>t. AxCtor D t \<in> set \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
 
 (* ------------------------------ *)
 

Typing_Lemmas.thy

@@ -135,33 +135,31 @@ qed simp_all
 lemma axiom_isin_same_kind: "\<lbrakk> AxData T k1 \<in> set (\<Delta>' @ AxData T k2 # \<Delta>) ; \<turnstile> (\<Delta>' @ AxData T k2 # \<Delta>) \<rbrakk> \<Longrightarrow> k1 = k2"
 proof (induction \<Delta>')
   case Nil
-  then have "atom T \<sharp> \<Delta>" by auto
-  then have "\<nexists>k. AxData T k \<in> set \<Delta>" by (metis (mono_tags, lifting) axiom.fresh(1) fresh_Cons fresh_append fresh_at_base(2) in_set_conv_decomp_first)
+  then have "\<nexists>k. AxData T k \<in> set \<Delta>" by auto
   then show ?case using Nil.prems(1) by auto
 next
   case (Cons a \<Delta>')
   then show ?case using axioms_valid(2)
   proof (cases a rule: axiom.exhaust)
     case (AxData T' k3)
-    then have "atom T' \<sharp> (\<Delta>' @ AxData T k2 # \<Delta>)" using Cons(3) by auto
-    then have "T' \<noteq> T" by (simp add: fresh_Cons fresh_append fresh_at_base(2))
+    then have "\<nexists>k. AxData T' k \<in> set (\<Delta>' @ AxData T k2 # \<Delta>)" using Cons(3) by fastforce
+    then have "T' \<noteq> T" by auto
     then show ?thesis using Cons AxData by auto
   qed fastforce
 qed
 
 lemma axiom_isin_same_type: "\<lbrakk> AxCtor D \<tau>1 \<in> set (\<Delta>' @ AxCtor D \<tau>2 # \<Delta>) ; \<turnstile> (\<Delta>' @ AxCtor D \<tau>2 # \<Delta>) \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
 proof (induction \<Delta>')
   case Nil
-  then have "atom D \<sharp> \<Delta>" by auto
-  then have "\<nexists>t. AxCtor D t \<in> set \<Delta>" by (metis (mono_tags, lifting) axiom.fresh(2) fresh_Cons fresh_append fresh_at_base(2) in_set_conv_decomp_first)
+  then have "\<nexists>t. AxCtor D t \<in> set \<Delta>" by auto
   then show ?case using Nil(1) by auto
 next
   case (Cons a \<Delta>')
   then show ?case
   proof (cases a rule: axiom.exhaust)
     case (AxCtor D' \<tau>')
-    then have "atom D' \<sharp> (\<Delta>' @ AxCtor D \<tau>2 # \<Delta>)" using Cons(3) by auto
-    then have "D' \<noteq> D" by (simp add: fresh_Cons fresh_append fresh_at_base(2))
+    then have "\<nexists>t. AxCtor D' t \<in> set (\<Delta>' @ AxCtor D \<tau>2 # \<Delta>)" using Cons(3) by fastforce
+    then have "D' \<noteq> D" by auto
     then show ?thesis using AxCtor Cons axioms_valid_aux(2) set_ConsD by auto
   qed auto
 qed