qpaper / injection proof.
(* Title: Nominal2_Atoms+ −
Authors: Brian Huffman, Christian Urban+ −
+ −
Definitions for concrete atom types. + −
*)+ −
theory Nominal2_Atoms+ −
imports Nominal2_Base+ −
Nominal2_Eqvt+ −
uses ("nominal_atoms.ML")+ −
begin+ −
+ −
section {* 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 simp+ −
+ −
lemma 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_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+ −
+ −
lemma 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 assms+ −
by (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)+ −
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+ −