(* Title: Nominal2_Atoms Authors: Brian Huffman, Christian Urban Definitions for concrete atom types. *)theory Nominal2_Atomsimports Nominal2_Base Nominal2_Eqvtuses ("nominal_atoms.ML")beginsection {* Infrastructure for concrete atom types *}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 simplemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" by (simp add: flip_commute)lemma flip_eqvt[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_alltext {* 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) donelemma 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_alllemma flip_fresh_fresh: fixes a b::"'a::at_base" assumes "atom a \<sharp> x" "atom b \<sharp> x" shows "(a \<leftrightarrow> b) \<bullet> x = x"using assmsby (simp add: flip_def swap_fresh_fresh)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" => "CONST 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)qedsetup {* 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