diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/GPerm.thy
--- a/Nominal/GPerm.thy	Tue May 22 14:00:59 2012 +0200
+++ b/Nominal/GPerm.thy	Tue May 22 14:55:58 2012 +0200
@@ -162,10 +162,6 @@
   "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y"
   by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx>) uminus_perm_raw uminus_perm_raw"
-  by (auto intro!: fun_relI simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
-
 lemma fst_snd_map_pair[simp]:
   "fst ` map_pair f g ` set l = f ` fst ` set l"
   "snd ` map_pair f g ` set l = g ` snd ` set l"
@@ -240,29 +236,20 @@
   "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya"
   by (simp add: fun_eq_iff perm_add_apply perm_eq_def)
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) perm_add_raw perm_add_raw"
-  by (auto intro!: fun_relI simp add: perm_add_raw_rsp)
-
 lemma [simp]:
   "a \<approx> a \<longleftrightarrow> valid_perm a"
   by (simp_all add: perm_eq_def)
 
-lemma [quot_respect]: "[] \<approx> []"
-  by auto
-
-lemmas [simp] = in_respects
-
 instantiation gperm :: (type) group_add
 begin
 
-quotient_definition "0 :: 'a gperm" is "[] :: ('a \<times> 'a) list"
+lift_definition zero_gperm :: "'a gperm" is "[]" by simp
 
-quotient_definition "uminus :: 'a gperm \<Rightarrow> 'a gperm" is
-  "uminus_perm_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
+lift_definition uminus_gperm :: "'a gperm \<Rightarrow> 'a gperm" is uminus_perm_raw
+  by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 
-quotient_definition "(op +) :: 'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is
-  "perm_add_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
+lift_definition plus_gperm :: "'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is perm_add_raw
+  by simp
 
 definition
   minus_perm_def: "(p1::'a gperm) - p2 = p1 + - p2"
@@ -270,23 +257,17 @@
 instance
   apply default
   unfolding minus_perm_def
-  by (partiality_descending, simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+
+  by (transfer,simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+
 
 end
 
 definition "mk_perm_raw l = (if valid_perm l then l else [])"
 
-quotient_definition "mk_perm :: ('a \<times> 'a) list \<Rightarrow> 'a gperm"
-  is "mk_perm_raw"
+lift_definition mk_perm :: "('a \<times> 'a) list \<Rightarrow> 'a gperm" is "mk_perm_raw"
+  by (simp add: mk_perm_raw_def)
 
 definition "dest_perm_raw p = sort [x\<leftarrow>p. fst x \<noteq> snd x]"
 
-quotient_definition "dest_perm :: ('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"
-  is "dest_perm_raw"
-
-lemma [quot_respect]: "(op = ===> op \<approx>) mk_perm_raw mk_perm_raw"
-  by (auto intro!: fun_relI simp add: mk_perm_raw_def)
-
 lemma distinct_fst_distinct[simp]: "distinct (map fst x) \<Longrightarrow> distinct x"
   by (induct x) auto
 
@@ -341,14 +322,13 @@
   by (rule sorted_distinct_set_unique)
      (simp_all add: distinct_filter valid_perm_def perm_eq_not_eq_same[simplified perm_eq_def, simplified])
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op =) dest_perm_raw dest_perm_raw"
-  by (auto intro!: fun_relI simp add: perm_eq_def)
+lift_definition dest_perm :: "('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"
+  is "dest_perm_raw"
+  by (simp add: perm_eq_def)
 
 lemma dest_perm_mk_perm[simp]:
   "dest_perm (mk_perm xs) = sort [x\<leftarrow>mk_perm_raw xs. fst x \<noteq> snd x]"
-  by (partiality_descending)
-     (simp add: dest_perm_raw_def)
+  by transfer (simp add: dest_perm_raw_def)
 
 lemma valid_perm_filter_id[simp]:
   "valid_perm p \<Longrightarrow> valid_perm [x\<leftarrow>p. fst x \<noteq> snd x]"
@@ -397,7 +377,7 @@
 
 lemma mk_perm_dest_perm[code abstype]:
   "mk_perm (dest_perm p) = p"
-  by (partiality_descending)
+  by transfer
      (auto simp add: mk_perm_raw_def)
 
 instantiation gperm :: (linorder) equal begin
@@ -407,51 +387,46 @@
 instance
   apply default
   unfolding equal_gperm_def
-  by partiality_descending simp
+  by transfer simp
 
 end
 
 lemma [code abstract]:
   "dest_perm 0 = []"
-  by (partiality_descending) (simp add: dest_perm_raw_def)
+  by transfer (simp add: dest_perm_raw_def)
 
 lemma [code abstract]:
   "dest_perm (-a) = dest_perm_raw (uminus_perm_raw (dest_perm a))"
-  by (partiality_descending) (auto)
+  by transfer auto
 
 lemma [code abstract]:
   "dest_perm (a + b) = dest_perm_raw (perm_add_raw (dest_perm a) (dest_perm b))"
-  by (partiality_descending) auto
+  by transfer auto
 
-quotient_definition "gpermute :: 'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"
-is perm_apply
-
-lemma [quot_respect]: "(op \<approx> ===> op =) perm_apply perm_apply"
-  by (auto intro!: fun_relI simp add: perm_eq_def)
+lift_definition gpermute :: "'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"
+  is perm_apply
+  by (simp add: perm_eq_def)
 
 lemma gpermute_zero[simp]:
   "gpermute 0 x = x"
-  by descending simp
+  by transfer simp
 
 lemma gpermute_add[simp]:
   "gpermute (p + q) x = gpermute p (gpermute q x)"
-  by descending (simp add: perm_add_apply)
-
-definition [simp]:"swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"
+  by transfer (simp add: perm_add_apply)
 
-lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) swap_raw swap_raw"
-  by (auto intro!: fun_relI simp add: valid_perm_def)
+definition [simp]: "swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"
 
-quotient_definition "gswap :: 'a \<Rightarrow> 'a \<Rightarrow> 'a gperm"
-is swap_raw
+lift_definition gswap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a gperm" is swap_raw
+  by (auto simp add: valid_perm_def)
 
 lemma [code abstract]:
   "dest_perm (gswap a b) = (if (a, b) \<le> (b, a) then swap_raw a b else swap_raw b a)"
-  by (partiality_descending) (auto simp add: dest_perm_raw_def)
+  by transfer (auto simp add: dest_perm_raw_def)
 
 lemma swap_self [simp]:
   "gswap a a = 0"
-  by (partiality_descending, auto)
+  by transfer simp
 
 lemma [simp]: "a \<noteq> b \<Longrightarrow> valid_perm [(a, b), (b, a)]"
   unfolding valid_perm_def by auto
@@ -459,35 +434,35 @@
 lemma swap_cancel [simp]:
   "gswap a b + gswap a b = 0"
   "gswap a b + gswap b a = 0"
-  by (descending, auto simp add: perm_eq_def perm_add_apply)+
+  by (transfer, auto simp add: perm_eq_def perm_add_apply)+
 
 lemma minus_swap [simp]:
   "- gswap a b = gswap a b"
-  by (partiality_descending, auto simp add: perm_eq_def)
+  by transfer (auto simp add: perm_eq_def)
 
 lemma swap_commute:
   "gswap a b = gswap b a"
-  by (partiality_descending, auto simp add: perm_eq_def)
+  by transfer (auto simp add: perm_eq_def)
 
 lemma swap_triple:
   assumes "a \<noteq> b" "c \<noteq> b"
   shows "gswap a c + gswap b c + gswap a c = gswap a b"
   using assms
-  by descending (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)
+  by transfer (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)
 
 lemma gpermute_gswap[simp]:
   "b \<noteq> a \<Longrightarrow> gpermute (gswap a b) b = a"
   "a \<noteq> b \<Longrightarrow> gpermute (gswap a b) a = b"
   "c \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> gpermute (gswap a b) c = c"
-  by (descending, auto)+
+  by (transfer, auto)+
 
 lemma gperm_eq:
   "(p = q) = (\<forall>a. gpermute p a = gpermute q a)"
-  by (partiality_descending) (auto simp add: perm_eq_def)
+  by transfer (auto simp add: perm_eq_def)
 
 lemma finite_gpermute_neq:
   "finite {a. gpermute p a \<noteq> a}"
-  apply descending
+  apply transfer
   apply (rule_tac B="fst ` set p" in finite_subset)
   apply auto
   by (metis perm_apply_outset)