--- a/Nominal-General/Nominal2_Atoms.thy	Sat Sep 04 05:43:03 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,188 +0,0 @@
-(*  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

--- a/Nominal-General/Nominal2_Base.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal-General/Nominal2_Base.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -7,6 +7,7 @@
 theory Nominal2_Base
 imports Main Infinite_Set
 uses ("nominal_library.ML")
+     ("nominal_atoms.ML")
 begin
 
 section {* Atoms and Sorts *}
@@ -1268,10 +1269,187 @@
 apply(auto)
 done
 
+section {* Infrastructure for concrete atom types *}
 
-section {* library functions for the nominal infrastructure *}
+
+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
+
+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 {* Library functions for the nominal infrastructure *}
+
 use "nominal_library.ML"
 
 
+section {* Automation for creating concrete atom types *}
+
+text {* at the moment only single-sort concrete atoms are supported *}
+
+use "nominal_atoms.ML"
+
+
 
 end

--- a/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -26,9 +26,11 @@
 lemmas [eqvt] =
   conj_eqvt Not_eqvt ex_eqvt imp_eqvt
   imp_eqvt[folded induct_implies_def]
+  uminus_eqvt
 
   (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
+  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt 
+  swap_eqvt flip_eqvt
 
   (* datatypes *)
   Pair_eqvt permute_list.simps

--- a/Nominal-General/Nominal2_Supp.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal-General/Nominal2_Supp.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -5,7 +5,7 @@
     Nominal Isabelle. 
 *)
 theory Nominal2_Supp
-imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms
+imports Nominal2_Base Nominal2_Eqvt 
 begin
 
 

--- a/Nominal-General/nominal_atoms.ML	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal-General/nominal_atoms.ML	Sat Sep 04 06:10:04 2010 +0800
@@ -26,7 +26,7 @@
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
   let
-    val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
+    val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
     val str = Sign.full_name thy name;
 
     (* typedef *)

--- a/Nominal/Abs.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -1,5 +1,5 @@
 theory Abs
-imports "../Nominal-General/Nominal2_Atoms" 
+imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
         "Quotient" 

--- a/Nominal/Nominal2_FSet.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -1,6 +1,6 @@
 theory Nominal2_FSet
-imports "../Nominal-General/Nominal2_Supp"
-        "../Nominal-General/Nominal2_Atoms" 
+imports "../Nominal-General/Nominal2_Base"
+        "../Nominal-General/Nominal2_Supp"
         "../Nominal-General/Nominal2_Eqvt" 
         FSet 
 begin

--- a/Pearl-jv/Paper.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Pearl-jv/Paper.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -1,7 +1,6 @@
 (*<*)
 theory Paper
 imports "../Nominal-General/Nominal2_Base" 
-        "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt"
         "../Nominal-General/Nominal2_Supp" 
         "../Nominal-General/Atoms" 

--- a/Pearl/Paper.thy	Sat Sep 04 05:43:03 2010 +0800
+++ b/Pearl/Paper.thy	Sat Sep 04 06:10:04 2010 +0800
@@ -1,7 +1,6 @@
 (*<*)
 theory Paper
 imports "../Nominal-General/Nominal2_Base" 
-        "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Atoms" 
         "LaTeXsugar"