# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1298906470 0
# Node ID 5f6fefdbf05539e2735e5f59847ea2516e6e5322
# Parent  9abc4a70540ca2016ac3783f6565cecf4ca2a6c8
split the library into a basics file; merged Nominal_Eqvt into Nominal_Base

diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2.thy	Mon Feb 28 15:21:10 2011 +0000
@@ -1,6 +1,6 @@
 theory Nominal2
 imports 
-  Nominal2_Base Nominal2_Eqvt Nominal2_Abs
+  Nominal2_Base Nominal2_Abs
 uses ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Feb 28 15:21:10 2011 +0000
@@ -1,6 +1,5 @@
 theory Nominal2_Abs
 imports "Nominal2_Base" 
-        "Nominal2_Eqvt" 
         "~~/src/HOL/Quotient" 
         "~~/src/HOL/Library/Quotient_List"
         "~~/src/HOL/Library/Quotient_Product" 
diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Feb 28 15:21:10 2011 +0000
@@ -8,8 +8,12 @@
 imports Main 
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
-uses ("nominal_library.ML")
+uses ("nominal_basics.ML")
+     ("nominal_thmdecls.ML")
+     ("nominal_permeq.ML")
+     ("nominal_library.ML")
      ("nominal_atoms.ML")
+     ("nominal_eqvt.ML")
 begin
 
 section {* Atoms and Sorts *}
@@ -437,38 +441,6 @@
 
 end
 
-lemma Not_eqvt:
-  shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
-by (simp add: permute_bool_def)
-
-lemma conj_eqvt:
-  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
-lemma imp_eqvt:
-  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
-lemma ex_eqvt:
-  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma all_eqvt:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-lemma ex1_eqvt:
-  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
-  unfolding Ex1_def
-  apply(simp add: ex_eqvt)
-  unfolding permute_fun_def 
-  apply(simp add: conj_eqvt all_eqvt)
-  unfolding permute_fun_def
-  apply(simp add: imp_eqvt permute_bool_def)
-  done
-
 lemma permute_boolE:
   fixes P::"bool"
   shows "p \<bullet> P \<Longrightarrow> P"
@@ -541,11 +513,6 @@
   unfolding mem_def permute_fun_def permute_bool_def
   by simp
 
-lemma mem_eqvt:
-  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def
-  by (simp add: permute_fun_app_eq)
-
 lemma empty_eqvt:
   shows "p \<bullet> {} = {}"
   unfolding empty_def Collect_def
@@ -555,22 +522,6 @@
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
   unfolding permute_set_eq_image image_insert ..
 
-lemma Collect_eqvt:
-  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
-  unfolding Collect_def permute_fun_def ..
-
-lemma inter_eqvt:
-  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def
-  apply(simp add: Collect_eqvt)
-  apply(simp add: permute_fun_def)
-  apply(simp add: conj_eqvt)
-  apply(simp add: mem_eqvt)
-  apply(simp add: permute_fun_def)
-  done
-
-
-
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -635,6 +586,8 @@
   shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
   by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
 
+
+
 subsection {* Permutations for options *}
 
 instantiation option :: (pt) pt
@@ -654,6 +607,8 @@
 
 subsection {* Permutations for fsets *}
 
+
+
 lemma permute_fset_rsp[quot_respect]:
   shows "(op = ===> list_eq ===> list_eq) permute permute"
   unfolding fun_rel_def
@@ -682,7 +637,9 @@
   and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-
+lemma fset_eqvt: 
+  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
+  by (lifting set_eqvt)
 
 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 
@@ -762,6 +719,277 @@
 instance int :: pure
 proof qed (rule permute_int_def)
 
+
+
+subsection {* Basic functions about permutations *}
+
+use "nominal_basics.ML"
+
+
+subsection {* Equivariance infrastructure *}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+use "nominal_thmdecls.ML"
+setup "Nominal_ThmDecls.setup"
+
+
+lemmas [eqvt] =
+  (* permutations *)
+  uminus_eqvt add_perm_eqvt swap_eqvt 
+
+  (* datatypes *)
+  Pair_eqvt 
+  permute_list.simps 
+  permute_option.simps 
+  permute_sum.simps
+
+  (* sets *)
+  empty_eqvt insert_eqvt set_eqvt 
+
+  (* fsets *)
+  permute_fset fset_eqvt
+
+
+
+subsection {* perm_simp infrastructure *}
+
+definition
+  "unpermute p = permute (- p)"
+
+lemma eqvt_apply:
+  fixes f :: "'a::pt \<Rightarrow> 'b::pt" 
+  and x :: "'a::pt"
+  shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+  unfolding permute_fun_def by simp
+
+lemma eqvt_lambda:
+  fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+  shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+  unfolding permute_fun_def unpermute_def by simp
+
+lemma eqvt_bound:
+  shows "p \<bullet> unpermute p x \<equiv> x"
+  unfolding unpermute_def by simp
+
+text {* provides perm_simp methods *}
+
+use "nominal_permeq.ML"
+setup Nominal_Permeq.setup
+
+method_setup perm_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
+
+method_setup perm_strict_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+
+(* the normal version of this lemma would cause loops *)
+lemma permute_eqvt_raw[eqvt_raw]:
+  shows "p \<bullet> permute \<equiv> permute"
+apply(simp add: fun_eq_iff permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
+subsubsection {* Equivariance of Logical Operators *}
+
+lemma eq_eqvt [eqvt]:
+  shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+  unfolding permute_eq_iff permute_bool_def ..
+
+lemma Not_eqvt [eqvt]:
+  shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
+by (simp add: permute_bool_def)
+
+lemma conj_eqvt [eqvt]:
+  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+lemma imp_eqvt [eqvt]:
+  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+declare imp_eqvt[folded induct_implies_def, eqvt]
+
+lemma ex_eqvt [eqvt]:
+  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+  unfolding permute_fun_def permute_bool_def
+  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+lemma all_eqvt [eqvt]:
+  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+  unfolding permute_fun_def permute_bool_def
+  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
+declare all_eqvt[folded induct_forall_def, eqvt]
+
+lemma ex1_eqvt [eqvt]:
+  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+  unfolding Ex1_def
+  by (perm_simp) (rule refl)
+
+lemma mem_eqvt [eqvt]:
+  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+  unfolding mem_def
+  by (simp add: permute_fun_app_eq)
+
+lemma Collect_eqvt [eqvt]:
+  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+  unfolding Collect_def permute_fun_def ..
+
+
+
+lemma inter_eqvt [eqvt]:
+  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+  unfolding Int_def
+  by (perm_simp) (rule refl)
+
+lemma image_eqvt [eqvt]:
+  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+  unfolding permute_set_eq_image
+  unfolding permute_fun_def [where f=f]
+  by (simp add: image_image)
+
+lemma if_eqvt [eqvt]:
+  shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+  by (simp add: permute_fun_def permute_bool_def)
+
+lemma True_eqvt [eqvt]:
+  shows "p \<bullet> True = True"
+  unfolding permute_bool_def ..
+
+lemma False_eqvt [eqvt]:
+  shows "p \<bullet> False = False"
+  unfolding permute_bool_def ..
+
+lemma disj_eqvt [eqvt]:
+  shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+lemma all_eqvt2:
+  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+  by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex_eqvt2:
+  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+  by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex1_eqvt2:
+  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+  by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma the_eqvt:
+  assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+  apply(rule the1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule theI'[OF unique])
+  done
+
+lemma the_eqvt2:
+  assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+  apply(rule the1_equality [symmetric])
+  apply(simp add: ex1_eqvt2[symmetric])
+  apply(simp add: permute_bool_def unique)
+  apply(simp add: permute_bool_def)
+  apply(rule theI'[OF unique])
+  done
+
+subsubsection {* Equivariance Set Operations *}
+
+lemma Bex_eqvt[eqvt]:
+  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Bex_def
+  by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Ball_def
+  by (perm_simp) (rule refl)
+
+lemma UNIV_eqvt[eqvt]:
+  shows "p \<bullet> UNIV = UNIV"
+  unfolding UNIV_def
+  by (perm_simp) (rule refl)
+
+lemma union_eqvt[eqvt]:
+  shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+  unfolding Un_def
+  by (perm_simp) (rule refl)
+
+lemma Diff_eqvt[eqvt]:
+  fixes A B :: "'a::pt set"
+  shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+  unfolding set_diff_eq
+  by (perm_simp) (rule refl)
+
+lemma Compl_eqvt[eqvt]:
+  fixes A :: "'a::pt set"
+  shows "p \<bullet> (- A) = - (p \<bullet> A)"
+  unfolding Compl_eq_Diff_UNIV
+  by (perm_simp) (rule refl)
+
+lemma subset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
+  unfolding subset_eq
+  by (perm_simp) (rule refl)
+
+lemma psubset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
+  unfolding psubset_eq
+  by (perm_simp) (rule refl)
+
+lemma vimage_eqvt[eqvt]:
+  shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+  unfolding vimage_def
+  by (perm_simp) (rule refl)
+
+lemma Union_eqvt[eqvt]:
+  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+  unfolding Union_eq 
+  by (perm_simp) (rule refl)
+
+lemma Sigma_eqvt:
+  shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
+unfolding Sigma_def
+unfolding UNION_eq_Union_image
+by (perm_simp) (rule refl)
+
+lemma finite_permute_iff:
+  shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+  unfolding permute_set_eq_vimage
+  using bij_permute by (rule finite_vimage_iff)
+
+lemma finite_eqvt[eqvt]:
+  shows "p \<bullet> finite A = finite (p \<bullet> A)"
+  unfolding finite_permute_iff permute_bool_def ..
+
+
+subsubsection {* Product Operations *}
+
+lemma fst_eqvt[eqvt]:
+  "p \<bullet> (fst x) = fst (p \<bullet> x)"
+ by (cases x) simp
+
+lemma snd_eqvt[eqvt]:
+  "p \<bullet> (snd x) = snd (p \<bullet> x)"
+ by (cases x) simp
+
+lemma split_eqvt[eqvt]: 
+  shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+  unfolding split_def
+  by (perm_simp) (rule refl)
+
+
+
+
 subsection {* Supp, Freshness and Supports *}
 
 context pt
@@ -843,12 +1071,12 @@
   finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
 qed
 
-lemma fresh_eqvt:
+lemma fresh_eqvt [eqvt]:
   shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
   unfolding permute_bool_def
   by (simp add: fresh_permute_iff)
 
-lemma supp_eqvt:
+lemma supp_eqvt [eqvt]:
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
   unfolding supp_conv_fresh
   unfolding Collect_def
@@ -970,7 +1198,6 @@
   "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
 
 
-
 section {* Finitely-supported types *}
 
 class fs = pt +
@@ -1246,6 +1473,58 @@
   by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
 
 
+subsubsection {* List Operations *}
+
+lemma append_eqvt[eqvt]:
+  shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+  by (induct xs) auto
+
+lemma rev_eqvt[eqvt]:
+  shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+  by (induct xs) (simp_all add: append_eqvt)
+
+lemma supp_rev:
+  shows "supp (rev xs) = supp xs"
+  by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+
+lemma fresh_rev:
+  shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+  by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+
+lemma map_eqvt[eqvt]: 
+  shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+  by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+  by (induct xs) (auto)
+
+lemma supp_removeAll:
+  fixes x::"atom"
+  shows "supp (removeAll x xs) = supp xs - {x}"
+  by (induct xs)
+     (auto simp add: supp_Nil supp_Cons supp_atom)
+
+lemma filter_eqvt[eqvt]:
+  shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt[eqvt]:
+  shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
+lemma length_eqvt[eqvt]:
+  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
+
 instance list :: (fs) fs
 apply default
 apply (induct_tac x)
@@ -1266,13 +1545,6 @@
   unfolding fresh_def supp_def 
   unfolding MOST_iff_cofinite by simp
 
-lemma supp_subset_fresh:
-  assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
-  shows "supp y \<subseteq> supp x"
-  using a
-  unfolding fresh_def
-  by blast
-
 lemma fresh_fun_app:
   assumes "a \<sharp> f" and "a \<sharp> x" 
   shows "a \<sharp> f x"
@@ -1316,6 +1588,16 @@
     using supp_fun_app by auto
 qed
 
+lemma supp_fun_app_eqvt:
+  assumes a: "eqvt f"
+  shows "supp (f x) \<subseteq> supp x"
+proof -
+  from a have "supp f = {}" by (simp add: supp_fun_eqvt)
+  then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast
+qed
+
+
+
 text {* equivariance of a function at a given argument *}
 
 definition
@@ -1353,7 +1635,8 @@
 using supp_eqvt_at[OF asm fin]
 by auto
 
-text {* helper functions for nominal_functions *}
+
+subsection {* helper functions for nominal_functions *}
 
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
@@ -1445,27 +1728,6 @@
   unfolding fresh_def
   by (auto simp add: supp_finite_atom_set assms)
 
-
-lemma Union_fresh:
-  shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
-  unfolding Union_image_eq[symmetric]
-  apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
-  unfolding eqvt_def
-  unfolding permute_fun_def
-  apply(simp)
-  unfolding UNION_def 
-  unfolding Collect_def 
-  unfolding Bex_def 
-  apply(simp add: ex_eqvt)
-  unfolding permute_fun_def
-  apply(simp add: conj_eqvt)
-  apply(simp add: mem_eqvt)
-  apply(simp add: supp_eqvt) 
-  unfolding permute_fun_def
-  apply(simp)
-  apply(assumption)
-  done
-
 lemma Union_supports_set:
   shows "(\<Union>x \<in> S. supp x) supports S"
 proof -
@@ -1489,12 +1751,14 @@
   assumes fin: "finite S"
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
+  have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
+    unfolding eqvt_def
+    by (perm_simp) (simp)
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
-    by (rule supp_finite_atom_set[symmetric])
-       (rule Union_of_finite_supp_sets[OF fin])
-  also have "\<dots> \<subseteq> supp S"
-    by (rule supp_subset_fresh)
-       (simp add: Union_fresh)
+    by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
+  also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
+  also have "\<dots> \<subseteq> supp S" using eqvt
+    by (rule supp_fun_app_eqvt)
   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 qed
 
@@ -1564,10 +1828,6 @@
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
-lemma fset_eqvt: 
-  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
-  by (lifting set_eqvt)
-
 lemma supp_fset [simp]:
   shows "supp (fset S) = supp S"
   unfolding supp_def
@@ -1610,6 +1870,30 @@
   done
 
 
+lemma in_fset_eqvt[eqvt]:
+  shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
+unfolding in_fset
+by (perm_simp) (simp)
+
+lemma union_fset_eqvt[eqvt]:
+  shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
+by (induct S) (simp_all)
+
+lemma supp_union_fset:
+  fixes S T::"'a::fs fset"
+  shows "supp (S |\<union>| T) = supp S \<union> supp T"
+by (induct S) (auto)
+
+lemma fresh_union_fset:
+  fixes S T::"'a::fs fset"
+  shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
+unfolding fresh_def
+by (simp add: supp_union_fset)
+
+lemma map_fset_eqvt[eqvt]: 
+  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+  by (lifting map_eqvt)
+
 section {* Freshness and Fresh-Star *}
 
 lemma fresh_Unit_elim: 
@@ -1751,15 +2035,10 @@
   unfolding fresh_star_def
   by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
 
-lemma fresh_star_eqvt:
+lemma fresh_star_eqvt [eqvt]:
   shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
 unfolding fresh_star_def
-unfolding Ball_def
-apply(simp add: all_eqvt)
-apply(subst permute_fun_def)
-apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
-done
-
+by (perm_simp) (rule refl)
 
 
 section {* Induction principle for permutations *}
@@ -2191,6 +2470,8 @@
   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
 
+declare atom_eqvt[eqvt]
+
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
 
@@ -2300,6 +2581,7 @@
 where
   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
 
+
 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
   unfolding flip_def by (rule swap_self)
 
@@ -2318,7 +2600,7 @@
 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
   by (simp add: flip_commute)
 
-lemma flip_eqvt: 
+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
@@ -2638,5 +2920,10 @@
 use "nominal_atoms.ML"
 
 
+section {* automatic equivariance procedure for inductive definitions *}
+
+use "nominal_eqvt.ML"
+
+
 
 end
diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Feb 28 15:21:10 2011 +0000
@@ -2,330 +2,13 @@
     Author:     Brian Huffman, 
     Author:     Christian Urban
 
-    Equivariance, supp and freshness lemmas for various operators 
-    (contains many, but not all such lemmas).
+    Test cases for perm_simp
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base 
-uses ("nominal_thmdecls.ML")
-     ("nominal_permeq.ML")
-     ("nominal_eqvt.ML")
 begin
 
 
-section {* Permsimp and Eqvt infrastructure *}
-
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
-
-use "nominal_thmdecls.ML"
-setup "Nominal_ThmDecls.setup"
-
-
-section {* eqvt lemmas *}
-
-lemmas [eqvt] =
-  conj_eqvt Not_eqvt ex_eqvt all_eqvt ex1_eqvt imp_eqvt uminus_eqvt
-  imp_eqvt[folded induct_implies_def]
-  all_eqvt[folded induct_forall_def]
-
-  (* nominal *)
-  supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
-  swap_eqvt flip_eqvt
-
-  (* datatypes *)
-  Pair_eqvt permute_list.simps permute_option.simps 
-  permute_sum.simps
-
-  (* sets *)
-  mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt
-
-  (* fsets *)
-  permute_fset fset_eqvt
-
-
-text {* helper lemmas for the perm_simp *}
-
-definition
-  "unpermute p = permute (- p)"
-
-lemma eqvt_apply:
-  fixes f :: "'a::pt \<Rightarrow> 'b::pt" 
-  and x :: "'a::pt"
-  shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
-  unfolding permute_fun_def by simp
-
-lemma eqvt_lambda:
-  fixes f :: "'a::pt \<Rightarrow> 'b::pt"
-  shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
-  unfolding permute_fun_def unpermute_def by simp
-
-lemma eqvt_bound:
-  shows "p \<bullet> unpermute p x \<equiv> x"
-  unfolding unpermute_def by simp
-
-text {* provides perm_simp methods *}
-
-use "nominal_permeq.ML"
-setup Nominal_Permeq.setup
-
-method_setup perm_simp =
- {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
- {* pushes permutations inside. *}
-
-method_setup perm_strict_simp =
- {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
- {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
-
-(* the normal version of this lemma would cause loops *)
-lemma permute_eqvt_raw[eqvt_raw]:
-  shows "p \<bullet> permute \<equiv> permute"
-apply(simp add: fun_eq_iff permute_fun_def)
-apply(subst permute_eqvt)
-apply(simp)
-done
-
-subsection {* Equivariance of Logical Operators *}
-
-lemma eq_eqvt[eqvt]:
-  shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
-  unfolding permute_eq_iff permute_bool_def ..
-
-lemma if_eqvt[eqvt]:
-  shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
-  by (simp add: permute_fun_def permute_bool_def)
-
-lemma True_eqvt[eqvt]:
-  shows "p \<bullet> True = True"
-  unfolding permute_bool_def ..
-
-lemma False_eqvt[eqvt]:
-  shows "p \<bullet> False = False"
-  unfolding permute_bool_def ..
-
-lemma disj_eqvt[eqvt]:
-  shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
-lemma all_eqvt2:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
-  by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma ex_eqvt2:
-  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
-  by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma ex1_eqvt2:
-  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
-  by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma the_eqvt:
-  assumes unique: "\<exists>!x. P x"
-  shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
-  apply(rule the1_equality [symmetric])
-  apply(rule_tac p="-p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel)
-  apply(rule unique)
-  apply(rule_tac p="-p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel)
-  apply(rule theI'[OF unique])
-  done
-
-lemma the_eqvt2:
-  assumes unique: "\<exists>!x. P x"
-  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
-  apply(rule the1_equality [symmetric])
-  apply(simp add: ex1_eqvt2[symmetric])
-  apply(simp add: permute_bool_def unique)
-  apply(simp add: permute_bool_def)
-  apply(rule theI'[OF unique])
-  done
-
-subsection {* Equivariance Set Operations *}
-
-lemma not_mem_eqvt:
-  shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
-  by (perm_simp) (rule refl)
-
-lemma Collect_eqvt[eqvt]:
-  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
-  unfolding Collect_def permute_fun_def ..
-
-lemma Collect_eqvt2:
-  shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
-  by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma Bex_eqvt[eqvt]:
-  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
-  unfolding Bex_def
-  by (perm_simp) (rule refl)
-
-lemma Ball_eqvt[eqvt]:
-  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
-  unfolding Ball_def
-  by (perm_simp) (rule refl)
-
-lemma UNIV_eqvt[eqvt]:
-  shows "p \<bullet> UNIV = UNIV"
-  unfolding UNIV_def
-  by (perm_simp) (rule refl)
-
-lemma union_eqvt[eqvt]:
-  shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
-  unfolding Un_def
-  by (perm_simp) (rule refl)
-
-lemma Diff_eqvt[eqvt]:
-  fixes A B :: "'a::pt set"
-  shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
-  unfolding set_diff_eq
-  by (perm_simp) (rule refl)
-
-lemma Compl_eqvt[eqvt]:
-  fixes A :: "'a::pt set"
-  shows "p \<bullet> (- A) = - (p \<bullet> A)"
-  unfolding Compl_eq_Diff_UNIV
-  by (perm_simp) (rule refl)
-
-lemma subset_eqvt[eqvt]:
-  shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
-  unfolding subset_eq
-  by (perm_simp) (rule refl)
-
-lemma psubset_eqvt[eqvt]:
-  shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
-  unfolding psubset_eq
-  by (perm_simp) (rule refl)
-
-lemma image_eqvt[eqvt]:
-  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding permute_set_eq_image
-  unfolding permute_fun_def [where f=f]
-  by (simp add: image_image)
-
-lemma vimage_eqvt[eqvt]:
-  shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
-  unfolding vimage_def
-  by (perm_simp) (rule refl)
-
-lemma Union_eqvt[eqvt]:
-  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
-  unfolding Union_eq 
-  by (perm_simp) (rule refl)
-
-lemma Sigma_eqvt:
-  shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
-unfolding Sigma_def
-unfolding UNION_eq_Union_image
-by (perm_simp) (rule refl)
-
-lemma finite_permute_iff:
-  shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
-  unfolding permute_set_eq_vimage
-  using bij_permute by (rule finite_vimage_iff)
-
-lemma finite_eqvt[eqvt]:
-  shows "p \<bullet> finite A = finite (p \<bullet> A)"
-  unfolding finite_permute_iff permute_bool_def ..
-
-
-section {* List Operations *}
-
-lemma append_eqvt[eqvt]:
-  shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
-  by (induct xs) auto
-
-lemma rev_eqvt[eqvt]:
-  shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
-  by (induct xs) (simp_all add: append_eqvt)
-
-lemma supp_rev:
-  shows "supp (rev xs) = supp xs"
-  by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
-
-lemma fresh_rev:
-  shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
-  by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
-
-lemma map_eqvt[eqvt]: 
-  shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
-  by (induct xs) (simp_all, simp only: permute_fun_app_eq)
-
-lemma removeAll_eqvt[eqvt]:
-  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
-  by (induct xs) (auto)
-
-lemma supp_removeAll:
-  fixes x::"atom"
-  shows "supp (removeAll x xs) = supp xs - {x}"
-  by (induct xs)
-     (auto simp add: supp_Nil supp_Cons supp_atom)
-
-lemma filter_eqvt[eqvt]:
-  shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
-apply(induct xs)
-apply(simp)
-apply(simp only: filter.simps permute_list.simps if_eqvt)
-apply(simp only: permute_fun_app_eq)
-done
-
-lemma distinct_eqvt[eqvt]:
-  shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
-apply(induct xs)
-apply(simp add: permute_bool_def)
-apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
-done
-
-lemma length_eqvt[eqvt]:
-  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
-by (induct xs) (simp_all add: permute_pure)
-
-
-subsection {* Equivariance Finite-Set Operations *}
-
-lemma in_fset_eqvt[eqvt]:
-  shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset
-by (perm_simp) (simp)
-
-lemma union_fset_eqvt[eqvt]:
-  shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
-by (induct S) (simp_all)
-
-lemma supp_union_fset:
-  fixes S T::"'a::fs fset"
-  shows "supp (S |\<union>| T) = supp S \<union> supp T"
-by (induct S) (auto)
-
-lemma fresh_union_fset:
-  fixes S T::"'a::fs fset"
-  shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
-unfolding fresh_def
-by (simp add: supp_union_fset)
-
-lemma map_fset_eqvt[eqvt]: 
-  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
-  by (lifting map_eqvt)
-
-
-subsection {* Product Operations *}
-
-lemma fst_eqvt[eqvt]:
-  "p \<bullet> (fst x) = fst (p \<bullet> x)"
- by (cases x) simp
-
-lemma snd_eqvt[eqvt]:
-  "p \<bullet> (snd x) = snd (p \<bullet> x)"
- by (cases x) simp
-
-lemma split_eqvt[eqvt]: 
-  shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
-  unfolding split_def
-  by (perm_simp) (rule refl)
-
-
-section {* Test cases *}
-
-
 declare [[trace_eqvt = false]]
 (* declare [[trace_eqvt = true]] *)
 
diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/nominal_basics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_basics.ML	Mon Feb 28 15:21:10 2011 +0000
@@ -0,0 +1,152 @@
+(*  Title:      nominal_basic.ML
+    Author:     Christian Urban
+
+  Basic functions for nominal.
+*)
+
+signature NOMINAL_BASIC =
+sig
+  val trace: bool Unsynchronized.ref
+  val trace_msg: (unit -> string) -> unit
+
+  val last2: 'a list -> 'a * 'a
+  val split_last2: 'a list -> 'a list * 'a * 'a
+  val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
+  val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
+  val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
+  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+  val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a
+  
+  val is_true: term -> bool
+ 
+  val dest_listT: typ -> typ
+  val dest_fsetT: typ -> typ
+
+  val mk_id: term -> term
+  val mk_all: (string * typ) -> term -> term
+  val mk_All: (string * typ) -> term -> term
+  val mk_exists: (string * typ) -> term -> term
+
+  val sum_case_const: typ -> typ -> typ -> term
+  val mk_sum_case: term -> term -> term
+ 
+  val mk_equiv: thm -> thm
+  val safe_mk_equiv: thm -> thm
+
+  val mk_minus: term -> term
+  val mk_plus: term -> term -> term
+
+  val perm_ty: typ -> typ 
+  val perm_const: typ -> term
+  val mk_perm_ty: typ -> term -> term -> term
+  val mk_perm: term -> term -> term
+  val dest_perm: term -> term * term
+
+end
+
+
+structure Nominal_Basic: NOMINAL_BASIC =
+struct
+
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if ! trace then tracing (msg ()) else ()
+
+
+(* orders an AList according to keys - every key needs to be there *)
+fun order eq keys list = 
+  map (the o AList.lookup eq list) keys
+
+(* orders an AList according to keys - returns default for non-existing keys *)
+fun order_default eq default keys list = 
+  map (the_default default o AList.lookup eq list) keys
+
+(* remove duplicates *)
+fun remove_dups eq [] = []
+  | remove_dups eq (x :: xs) = 
+      if member eq xs x 
+      then remove_dups eq xs 
+      else x :: remove_dups eq xs
+
+fun last2 [] = raise Empty
+  | last2 [_] = raise Empty
+  | last2 [x, y] = (x, y)
+  | last2 (_ :: xs) = last2 xs
+
+fun split_last2 xs = 
+  let
+    val (xs', x) = split_last xs
+    val (xs'', y) = split_last xs'
+  in
+    (xs'', y, x)
+  end
+
+fun map4 _ [] [] [] [] = []
+  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
+
+fun split_filter f [] = ([], [])
+  | split_filter f (x :: xs) =
+      let 
+        val (r, l) = split_filter f xs 
+      in 
+        if f x 
+        then (x :: r, l) 
+        else (r, x :: l) 
+      end
+
+(* to be used with left-infix binop-operations *)
+fun fold_left f [] z = z
+  | fold_left f [x] z = x
+  | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
+
+
+
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
+fun dest_listT (Type (@{type_name list}, [T])) = T
+  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
+
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+
+
+fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
+
+fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
+
+fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)
+
+fun mk_exists (a, T) t =  HOLogic.exists_const T $ Abs (a, T, t)
+
+fun sum_case_const ty1 ty2 ty3 = 
+  Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
+
+fun mk_sum_case trm1 trm2 =
+  let
+    val ([ty1], ty3) = strip_type (fastype_of trm1)
+    val ty2 = domain_type (fastype_of trm2)
+  in
+    sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
+  end 
+
+
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
+
+
+fun mk_minus p = @{term "uminus::perm => perm"} $ p
+
+fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
+
+fun perm_ty ty = @{typ "perm"} --> ty --> ty
+fun perm_const ty  = Const (@{const_name "permute"}, perm_ty ty)
+fun mk_perm_ty ty p trm = perm_const ty $ p $ trm
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
+
+fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
+  | dest_perm t = raise TERM ("dest_perm", [t]);
+
+end (* structure *)
+
+open Nominal_Basic;
\ No newline at end of file
diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/nominal_library.ML	Mon Feb 28 15:21:10 2011 +0000
@@ -1,45 +1,11 @@
 (*  Title:      nominal_library.ML
     Author:     Christian Urban
 
-  Basic functions for nominal.
+  Library functions for nominal.
 *)
 
 signature NOMINAL_LIBRARY =
 sig
-  val trace: bool Unsynchronized.ref
-  val trace_msg: (unit -> string) -> unit
-
-  val last2: 'a list -> 'a * 'a
-  val split_last2: 'a list -> 'a list * 'a * 'a
-  val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
-  val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
-  val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
-  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a
-  
-  val is_true: term -> bool
- 
-  val dest_listT: typ -> typ
-  val dest_fsetT: typ -> typ
-
-  val mk_id: term -> term
-  val mk_all: (string * typ) -> term -> term
-  val mk_All: (string * typ) -> term -> term
-  val mk_exists: (string * typ) -> term -> term
-
-  val sum_case_const: typ -> typ -> typ -> term
-  val mk_sum_case: term -> term -> term
- 
-  val mk_minus: term -> term
-  val mk_plus: term -> term -> term
-
-  val perm_ty: typ -> typ 
-  val perm_const: typ -> term
-  val mk_perm_ty: typ -> term -> term -> term
-  val mk_perm: term -> term -> term
-  val dest_perm: term -> term * term
-
   val mk_sort_of: term -> term
   val atom_ty: typ -> typ
   val atom_const: typ -> term
@@ -91,9 +57,6 @@
   val mk_finite_ty: typ -> term -> term
   val mk_finite: term -> term
 
-  val mk_equiv: thm -> thm
-  val safe_mk_equiv: thm -> thm
-
   val mk_diff: term * term -> term
   val mk_append: term * term -> term
   val mk_union: term * term -> term
@@ -144,101 +107,6 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if ! trace then tracing (msg ()) else ()
-
-
-(* orders an AList according to keys - every key needs to be there *)
-fun order eq keys list = 
-  map (the o AList.lookup eq list) keys
-
-(* orders an AList according to keys - returns default for non-existing keys *)
-fun order_default eq default keys list = 
-  map (the_default default o AList.lookup eq list) keys
-
-(* remove duplicates *)
-fun remove_dups eq [] = []
-  | remove_dups eq (x :: xs) = 
-      if member eq xs x 
-      then remove_dups eq xs 
-      else x :: remove_dups eq xs
-
-fun last2 [] = raise Empty
-  | last2 [_] = raise Empty
-  | last2 [x, y] = (x, y)
-  | last2 (_ :: xs) = last2 xs
-
-fun split_last2 xs = 
-  let
-    val (xs', x) = split_last xs
-    val (xs'', y) = split_last xs'
-  in
-    (xs'', y, x)
-  end
-
-fun map4 _ [] [] [] [] = []
-  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
-
-fun split_filter f [] = ([], [])
-  | split_filter f (x :: xs) =
-      let 
-        val (r, l) = split_filter f xs 
-      in 
-        if f x 
-        then (x :: r, l) 
-        else (r, x :: l) 
-      end
-
-(* to be used with left-infix binop-operations *)
-fun fold_left f [] z = z
-  | fold_left f [x] z = x
-  | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
-
-
-
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
-
-fun dest_listT (Type (@{type_name list}, [T])) = T
-  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
-
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
-  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-
-
-fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
-
-fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
-
-fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)
-
-fun mk_exists (a, T) t =  HOLogic.exists_const T $ Abs (a, T, t)
-
-fun sum_case_const ty1 ty2 ty3 = 
-  Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
-
-fun mk_sum_case trm1 trm2 =
-  let
-    val ([ty1], ty3) = strip_type (fastype_of trm1)
-    val ty2 = domain_type (fastype_of trm2)
-  in
-    sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
-  end 
-
-
-
-fun mk_minus p = @{term "uminus::perm => perm"} $ p
-
-fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
-
-fun perm_ty ty = @{typ "perm"} --> ty --> ty
-fun perm_const ty  = Const (@{const_name "permute"}, perm_ty ty)
-fun mk_perm_ty ty p trm = perm_const ty $ p $ trm
-fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
-
-fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
-  | dest_perm t = raise TERM ("dest_perm", [t]);
-
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
 fun atom_ty ty = ty --> @{typ "atom"};
@@ -358,10 +226,6 @@
 fun mk_finite t = mk_finite_ty (fastype_of t) t
 
 
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
-
 (* functions that construct differences, appends and unions
    but avoid producing empty atom sets or empty atom lists *)