--- a/Quot/Nominal/Nominal2_Atoms.thy Wed Feb 24 17:32:43 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,251 +0,0 @@
-(* 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