--- a/Nominal/Nominal2_Base.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -7,7 +7,8 @@
 theory Nominal2_Base
 imports "~~/src/HOL/Library/Old_Datatype"
         "~~/src/HOL/Library/Infinite_Set"
-        "~~/src/HOL/Quotient_Examples/FSet"
+        "~~/src/HOL/Library/Multiset"
+        "~~/src/HOL/Library/FSet"
         "~~/src/HOL/Library/FinFun"
 keywords
   "atom_decl" "equivariance" :: thy_decl 
@@ -18,7 +19,7 @@
 
 section {* Atoms and Sorts *}
 
-text {* A simple implementation for atom_sorts is strings. *}
+text {* A simple implementation for @{text atom_sorts} is strings. *}
 (* types atom_sort = string *)
 
 text {* To deal with Church-like binding we use trees of  
@@ -611,7 +612,7 @@
 lemma permute_multiset [simp]:
   fixes M N::"('a::pt) multiset"
   shows "(p \<bullet> {#}) = ({#} ::('a::pt) multiset)"
-  and   "(p \<bullet> {# x #}) = {# p \<bullet> x #}"
+  and   "(p \<bullet> add_mset x M) = add_mset (p \<bullet> x) (p \<bullet> M)"
   and   "(p \<bullet> (M + N)) = (p \<bullet> M) + (p \<bullet> N)"
   unfolding permute_multiset_def
   by (simp_all)
@@ -619,38 +620,40 @@
 
 subsection {* Permutations for @{typ "'a fset"} *}
 
-lemma permute_fset_rsp[quot_respect]:
-  shows "(op = ===> list_eq ===> list_eq) permute permute"
-  unfolding rel_fun_def
-  by (simp add: set_eqvt[symmetric])
-
 instantiation fset :: (pt) pt
 begin
 
-quotient_definition
-  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  by (simp add: set_eqvt[symmetric])
-
+context includes fset.lifting begin
+lift_definition
+  "permute_fset" :: "perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is "permute :: perm \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
+end
+
+context includes fset.lifting begin
 instance 
 proof
   fix x :: "'a fset" and p q :: "perm"
-  show "0 \<bullet> x = x" by (descending) (simp)
-  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
+  show "0 \<bullet> x = x" by transfer simp
+  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"  by transfer simp
 qed
+end
 
 end
 
+context includes fset.lifting
+begin
 lemma permute_fset [simp]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
-  and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
-  by (lifting permute_list.simps)
+  and   "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)"
+  apply (transfer, simp add: empty_eqvt)
+  apply (transfer, simp add: insert_eqvt)
+  done
 
 lemma fset_eqvt: 
   shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
-  by (lifting set_eqvt)
+  by transfer simp
+end
 
 
 subsection {* Permutations for @{typ "('a, 'b) finfun"} *}
@@ -762,7 +765,7 @@
 proof qed (rule permute_int_def)
 
 
-section {* Infrastructure for Equivariance and Perm_simp *}
+section {* Infrastructure for Equivariance and @{text Perm_simp} *}
 
 subsection {* Basic functions about permutations *}
 
@@ -792,7 +795,7 @@
   (* multisets *)
   permute_multiset
 
-subsection {* perm_simp infrastructure *}
+subsection {* @{text perm_simp} infrastructure *}
 
 definition
   "unpermute p = permute (- p)"
@@ -812,7 +815,7 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
-text {* provides perm_simp methods *}
+text {* provides @{text perm_simp} methods *}
 
 ML_file "nominal_permeq.ML"
 
@@ -974,10 +977,6 @@
   unfolding permute_set_eq permute_fun_def
   by (auto simp: permute_bool_def)
 
-lemma inter_eqvt [eqvt]:
-  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def by simp
-
 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 simp
@@ -999,14 +998,22 @@
   unfolding UNIV_def 
   by (perm_simp) (rule refl)
 
+lemma inter_eqvt [eqvt]:
+  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+  unfolding Int_def by simp
+
+lemma Inter_eqvt [eqvt]:
+  shows "p \<bullet> \<Inter>S = \<Inter>(p \<bullet> S)"
+  unfolding Inter_eq by simp
+
 lemma union_eqvt [eqvt]:
   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
   unfolding Un_def by simp
 
-lemma UNION_eqvt [eqvt]:
-  shows "p \<bullet> (UNION A f) = (UNION (p \<bullet> A) (p \<bullet> f))"
-unfolding UNION_eq
-by (perm_simp) (simp)
+lemma Union_eqvt [eqvt]:
+  shows "p \<bullet> \<Union>A = \<Union>(p \<bullet> A)"
+  unfolding Union_eq
+  by perm_simp rule
 
 lemma Diff_eqvt [eqvt]:
   fixes A B :: "'a::pt set"
@@ -1030,16 +1037,6 @@
   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
   unfolding vimage_def by simp
 
-lemma Union_eqvt [eqvt]:
-  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
-  unfolding Union_eq by simp
-
-lemma Inter_eqvt [eqvt]:
-  shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
-  unfolding Inter_eq by simp
-
-thm foldr.simps
-
 lemma foldr_eqvt[eqvt]:
   "p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)"
   apply(induct xs)
@@ -1052,7 +1049,6 @@
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
 unfolding Sigma_def
-unfolding SUP_def
 by (perm_simp) (rule refl)
 
 text {* 
@@ -1109,7 +1105,7 @@
 
 instance 
 apply standard
-unfolding Inf_fun_def INF_def
+unfolding Inf_fun_def
 apply(perm_simp)
 apply(rule refl)
 done 
@@ -1200,9 +1196,10 @@
 
 subsubsection {* Equivariance for @{typ "'a fset"} *}
 
+context includes fset.lifting begin
 lemma in_fset_eqvt [eqvt]:
   shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset by simp
+  by transfer simp
 
 lemma union_fset_eqvt [eqvt]:
   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
@@ -1210,21 +1207,16 @@
 
 lemma inter_fset_eqvt [eqvt]:
   shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
-  apply(descending)
-  unfolding list_eq_def inter_list_def
-  apply(simp)
-  done
+  by transfer simp
 
 lemma subset_fset_eqvt [eqvt]:
   shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
-  apply(descending)
-  unfolding sub_list_def
-  apply(simp)
-  done
+  by transfer simp
   
 lemma map_fset_eqvt [eqvt]: 
-  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
-  by (lifting map_eqvt)
+  shows "p \<bullet> (f |`| S) = (p \<bullet> f) |`| (p \<bullet> S)"
+  by transfer simp
+end
 
 subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *}
 
@@ -1906,7 +1898,7 @@
   end
 *}
 
-subsection {* helper functions for nominal_functions *}
+subsection {* helper functions for @{text nominal_functions} *}
 
 lemma THE_defaultI2:
   assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
@@ -2146,30 +2138,22 @@
 qed
 
 lemma Union_supports_multiset:
-  shows "\<Union>{supp x | x. x :# M} supports M"
+  shows "\<Union>{supp x | x. x \<in># M} supports M"
 proof -
-  have sw: "\<And>a b. ((\<And>x. x :# M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
-    unfolding permute_multiset_def 
-    apply(induct M)
-    apply(simp_all)
-    done
-  show "(\<Union>{supp x | x. x :# M}) supports M"
-    unfolding supports_def
-    apply(clarify)
-    apply(rule sw)
-    apply(rule swap_fresh_fresh)
-    apply(simp_all only: fresh_def)
-    apply(auto)
-    apply(metis neq0_conv)+
-    done
+  have sw: "\<And>a b. ((\<And>x. x \<in># M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
+    unfolding permute_multiset_def by (induct M) simp_all
+  have "(\<Union>x\<in>set_mset M. supp x) supports M"
+    by (auto intro!: sw swap_fresh_fresh simp add: fresh_def supports_def)
+  also have "(\<Union>x\<in>set_mset M. supp x) = (\<Union>{supp x | x. x \<in># M})"
+    by auto
+  finally show "(\<Union>{supp x | x. x \<in># M}) supports M" .
 qed
 
 lemma Union_included_multiset:
   fixes M::"('a::fs multiset)" 
   shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
 proof -
-  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
-  also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
+  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>x \<in> set_mset M. supp x)" by auto
   also have "... = supp (set_mset M)"
     by (simp add: supp_of_finite_sets)
   also have " ... \<subseteq> supp M" by (rule supp_set_mset)
@@ -2178,7 +2162,7 @@
 
 lemma supp_of_multisets:
   fixes M::"('a::fs multiset)"
-  shows "(supp M) = (\<Union>{supp x | x. x :# M})"
+  shows "(supp M) = (\<Union>{supp x | x. x \<in># M})"
 apply(rule subset_antisym)
 apply(rule supp_is_subset)
 apply(rule Union_supports_multiset)
@@ -2221,20 +2205,20 @@
 unfolding fresh_def
 by (simp)
 
-lemma supp_insert_fset [simp]:
+lemma supp_finsert [simp]:
   fixes x::"'a::fs"
   and   S::"'a fset"
-  shows "supp (insert_fset x S) = supp x \<union> supp S"
+  shows "supp (finsert x S) = supp x \<union> supp S"
   apply(subst supp_fset[symmetric])
   apply(simp add: supp_of_finite_insert)
   done
 
-lemma fresh_insert_fset:
+lemma fresh_finsert:
   fixes x::"'a::fs"
   and   S::"'a fset"
-  shows "a \<sharp> insert_fset x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+  shows "a \<sharp> finsert x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
   unfolding fresh_def
-  by (simp)
+  by simp
 
 lemma fset_finite_supp:
   fixes S::"('a::fs) fset"
@@ -3121,7 +3105,7 @@
   unfolding atom_eqvt [symmetric]
   by simp_all
 
-text {* the following two lemmas do not hold for at_base, 
+text {* the following two lemmas do not hold for @{text at_base}, 
   only for single sort atoms from at *}
 
 lemma flip_triple: