(*  Title:      Nominal2_Atoms+
−
    Authors:    Brian Huffman, Christian Urban+
−
+
−
    Definitions for concrete atom types. +
−
*)+
−
theory Nominal2_Atoms+
−
imports Nominal2_Base+
−
uses ("nominal_atoms.ML")+
−
begin+
−
+
−
section {* Concrete atom types *}+
−
+
−
text {*+
−
  Class @{text at_base} allows types containing multiple sorts of atoms.+
−
  Class @{text at} only allows types with a single sort.+
−
*}+
−
+
−
class at_base = pt ++
−
  fixes atom :: "'a \<Rightarrow> atom"+
−
  assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"+
−
  assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"+
−
+
−
class at = at_base ++
−
  assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"+
−
+
−
instance at < at_base ..+
−
+
−
lemma supp_at_base: +
−
  fixes a::"'a::at_base"+
−
  shows "supp a = {atom a}"+
−
  by (simp add: supp_atom [symmetric] supp_def atom_eqvt)+
−
+
−
lemma fresh_at_base: +
−
  shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"+
−
  unfolding fresh_def by (simp add: supp_at_base)+
−
+
−
instance at_base < fs+
−
proof qed (simp add: supp_at_base)+
−
+
−
lemma at_base_infinite [simp]:+
−
  shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U")+
−
proof+
−
  obtain a :: 'a where "True" by auto+
−
  assume "finite ?U"+
−
  hence "finite (atom ` ?U)"+
−
    by (rule finite_imageI)+
−
  then obtain b where b: "b \<notin> atom ` ?U" "sort_of b = sort_of (atom a)"+
−
    by (rule obtain_atom)+
−
  from b(2) have "b = atom ((atom a \<rightleftharpoons> b) \<bullet> a)"+
−
    unfolding atom_eqvt [symmetric]+
−
    by (simp add: swap_atom)+
−
  hence "b \<in> atom ` ?U" by simp+
−
  with b(1) show "False" by simp+
−
qed+
−
+
−
lemma swap_at_base_simps [simp]:+
−
  fixes x y::"'a::at_base"+
−
  shows "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> x = y"+
−
  and   "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> y = x"+
−
  and   "atom x \<noteq> a \<Longrightarrow> atom x \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x"+
−
  unfolding atom_eq_iff [symmetric]+
−
  unfolding atom_eqvt [symmetric]+
−
  by simp_all+
−
+
−
lemma obtain_at_base:+
−
  assumes X: "finite X"+
−
  obtains a::"'a::at_base" where "atom a \<notin> X"+
−
proof -+
−
  have "inj (atom :: 'a \<Rightarrow> atom)"+
−
    by (simp add: inj_on_def)+
−
  with X have "finite (atom -` X :: 'a set)"+
−
    by (rule finite_vimageI)+
−
  with at_base_infinite have "atom -` X \<noteq> (UNIV :: 'a set)"+
−
    by auto+
−
  then obtain a :: 'a where "atom a \<notin> X"+
−
    by auto+
−
  thus ?thesis ..+
−
qed+
−
+
−
+
−
section {* A swapping operation for concrete atoms *}+
−
  +
−
definition+
−
  flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")+
−
where+
−
  "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"+
−
+
−
lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"+
−
  unfolding flip_def by (rule swap_self)+
−
+
−
lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"+
−
  unfolding flip_def by (rule swap_commute)+
−
+
−
lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"+
−
  unfolding flip_def by (rule minus_swap)+
−
+
−
lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"+
−
  unfolding flip_def by (rule swap_cancel)+
−
+
−
lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"+
−
  unfolding permute_plus [symmetric] add_flip_cancel by simp+
−
+
−
lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"+
−
  by (simp add: flip_commute)+
−
+
−
lemma flip_eqvt: +
−
  fixes a b c::"'a::at_base"+
−
  shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"+
−
  unfolding flip_def+
−
  by (simp add: swap_eqvt atom_eqvt)+
−
+
−
lemma flip_at_base_simps [simp]:+
−
  shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"+
−
  and   "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"+
−
  and   "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"+
−
  and   "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"+
−
  unfolding flip_def+
−
  unfolding atom_eq_iff [symmetric]+
−
  unfolding atom_eqvt [symmetric]+
−
  by simp_all+
−
+
−
text {* the following two lemmas do not hold for at_base, +
−
  only for single sort atoms from at *}+
−
+
−
lemma permute_flip_at:+
−
  fixes a b c::"'a::at"+
−
  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"+
−
  unfolding flip_def+
−
  apply (rule atom_eq_iff [THEN iffD1])+
−
  apply (subst atom_eqvt [symmetric])+
−
  apply (simp add: swap_atom)+
−
  done+
−
+
−
lemma flip_at_simps [simp]:+
−
  fixes a b::"'a::at"+
−
  shows "(a \<leftrightarrow> b) \<bullet> a = b" +
−
  and   "(a \<leftrightarrow> b) \<bullet> b = a"+
−
  unfolding permute_flip_at by simp_all+
−
+
−
+
−
subsection {* Syntax for coercing at-elements to the atom-type *}+
−
+
−
(*+
−
syntax+
−
  "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)+
−
+
−
translations+
−
  "_atom_constrain a t" => "atom (_constrain a t)"+
−
*)+
−
+
−
subsection {* A lemma for proving instances of class @{text at}. *}+
−
+
−
setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}+
−
setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}+
−
+
−
text {*+
−
  New atom types are defined as subtypes of @{typ atom}.+
−
*}+
−
+
−
lemma exists_eq_simple_sort: +
−
  shows "\<exists>a. a \<in> {a. sort_of a = s}"+
−
  by (rule_tac x="Atom s 0" in exI, simp)+
−
+
−
lemma exists_eq_sort: +
−
  shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"+
−
  by (rule_tac x="Atom (sort_fun x) y" in exI, simp)+
−
+
−
lemma at_base_class:+
−
  fixes sort_fun :: "'b \<Rightarrow>atom_sort"+
−
  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"+
−
  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"+
−
  assumes atom_def: "\<And>a. atom a = Rep a"+
−
  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"+
−
  shows "OFCLASS('a, at_base_class)"+
−
proof+
−
  interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)+
−
  have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp+
−
  fix a b :: 'a and p p1 p2 :: perm+
−
  show "0 \<bullet> a = a"+
−
    unfolding permute_def by (simp add: Rep_inverse)+
−
  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"+
−
    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)+
−
  show "atom a = atom b \<longleftrightarrow> a = b"+
−
    unfolding atom_def by (simp add: Rep_inject)+
−
  show "p \<bullet> atom a = atom (p \<bullet> a)"+
−
    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)+
−
qed+
−
+
−
(*+
−
lemma at_class:+
−
  fixes s :: atom_sort+
−
  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"+
−
  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"+
−
  assumes atom_def: "\<And>a. atom a = Rep a"+
−
  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"+
−
  shows "OFCLASS('a, at_class)"+
−
proof+
−
  interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)+
−
  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)+
−
  fix a b :: 'a and p p1 p2 :: perm+
−
  show "0 \<bullet> a = a"+
−
    unfolding permute_def by (simp add: Rep_inverse)+
−
  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"+
−
    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)+
−
  show "sort_of (atom a) = sort_of (atom b)"+
−
    unfolding atom_def by (simp add: sort_of_Rep)+
−
  show "atom a = atom b \<longleftrightarrow> a = b"+
−
    unfolding atom_def by (simp add: Rep_inject)+
−
  show "p \<bullet> atom a = atom (p \<bullet> a)"+
−
    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)+
−
qed+
−
*)+
−
+
−
lemma at_class:+
−
  fixes s :: atom_sort+
−
  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"+
−
  assumes type: "type_definition Rep Abs {a. sort_of a = s}"+
−
  assumes atom_def: "\<And>a. atom a = Rep a"+
−
  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"+
−
  shows "OFCLASS('a, at_class)"+
−
proof+
−
  interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)+
−
  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)+
−
  fix a b :: 'a and p p1 p2 :: perm+
−
  show "0 \<bullet> a = a"+
−
    unfolding permute_def by (simp add: Rep_inverse)+
−
  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"+
−
    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)+
−
  show "sort_of (atom a) = sort_of (atom b)"+
−
    unfolding atom_def by (simp add: sort_of_Rep)+
−
  show "atom a = atom b \<longleftrightarrow> a = b"+
−
    unfolding atom_def by (simp add: Rep_inject)+
−
  show "p \<bullet> atom a = atom (p \<bullet> a)"+
−
    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)+
−
qed+
−
+
−
setup {* Sign.add_const_constraint+
−
  (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}+
−
setup {* Sign.add_const_constraint+
−
  (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}+
−
+
−
+
−
section {* Automation for creating concrete atom types *}+
−
+
−
text {* at the moment only single-sort concrete atoms are supported *}+
−
+
−
use "nominal_atoms.ML"+
−
+
−
+
−
+
−
+
−
end+
−