# HG changeset patch
# User wenzelm
# Date 1289401515 -3600
# Node ID 34823a2cba08522458b5a8b2c540c7badaae92ad
# Parent  2269544b645730911fc7df8fe6db1df729a13cc4# Parent  b6feba6c9fccf99c951408b85ed30e7793a11836
merged

diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -82,21 +82,15 @@
   apply(rule list_all2_rel[OF q])
   done
 
-lemma cons_prs_aux:
-  assumes q: "Quotient R Abs Rep"
-  shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
-  by (induct t) (simp_all add: Quotient_abs_rep[OF q])
-
 lemma cons_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
-  by (simp only: fun_eq_iff fun_map_def cons_prs_aux[OF q])
-     (simp)
+  by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
 
 lemma cons_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
-  by (auto)
+  by auto
 
 lemma nil_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
@@ -120,15 +114,16 @@
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
   and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
-  by (simp_all only: fun_eq_iff fun_map_def map_prs_aux[OF a b])
-     (simp_all add: Quotient_abs_rep[OF a])
+  by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
+    (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+
 
 lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
   and   "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map"
-  apply simp_all
+  apply (simp_all add: fun_rel_def)
   apply(rule_tac [!] allI)+
   apply(rule_tac [!] impI)
   apply(rule_tac [!] allI)+
@@ -146,7 +141,8 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
-  by (simp only: fun_eq_iff fun_map_def foldr_prs_aux[OF a b])
+  apply (simp add: fun_eq_iff)
+  by (simp only: fun_eq_iff foldr_prs_aux[OF a b])
      (simp)
 
 lemma foldl_prs_aux:
@@ -160,8 +156,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
-  by (simp only: fun_eq_iff fun_map_def foldl_prs_aux[OF a b])
-     (simp)
+  by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
 
 lemma list_all2_empty:
   shows "list_all2 R [] b \<Longrightarrow> length b = 0"
@@ -172,7 +167,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl"
-  apply(auto)
+  apply(auto simp add: fun_rel_def)
   apply (subgoal_tac "R1 xa ya \<longrightarrow> list_all2 R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
   apply simp
   apply (rule_tac x="xa" in spec)
@@ -186,7 +181,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr"
-  apply auto
+  apply (auto simp add: fun_rel_def)
   apply(subgoal_tac "R2 xb yb \<longrightarrow> list_all2 R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
   apply simp
   apply (rule_tac xs="xa" and ys="ya" in list_induct2)
@@ -224,7 +219,7 @@
 
 lemma[quot_respect]:
   "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
-  by (simp add: list_all2_rsp)
+  by (simp add: list_all2_rsp fun_rel_def)
 
 lemma[quot_preserve]:
   assumes a: "Quotient R abs1 rep1"
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 fun
-  option_rel
+  option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
 where
   "option_rel R None None = True"
 | "option_rel R (Some x) None = False"
@@ -56,7 +56,7 @@
 lemma option_Some_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> option_rel R) Some Some"
-  by simp
+  by auto
 
 lemma option_None_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -8,13 +8,16 @@
 imports Main Quotient_Syntax
 begin
 
-fun
-  prod_rel
+definition
+  prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
 where
   "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
 
 declare [[map prod = (prod_fun, prod_rel)]]
 
+lemma prod_rel_apply [simp]:
+  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
+  by (simp add: prod_rel_def)
 
 lemma prod_equivp[quot_equiv]:
   assumes a: "equivp R1"
@@ -22,7 +25,7 @@
   shows "equivp (prod_rel R1 R2)"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
-  apply(simp_all add: split_paired_all)
+  apply(simp_all add: split_paired_all prod_rel_def)
   apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
   apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
   apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
@@ -45,7 +48,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
-  by simp
+  by (auto simp add: prod_rel_def)
 
 lemma Pair_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -59,33 +62,29 @@
   assumes "Quotient R1 Abs1 Rep1"
   assumes "Quotient R2 Abs2 Rep2"
   shows "(prod_rel R1 R2 ===> R1) fst fst"
-  by simp
+  by auto
 
 lemma fst_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
-  apply(simp add: fun_eq_iff)
-  apply(simp add: Quotient_abs_rep[OF q1])
-  done
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
 
 lemma snd_rsp[quot_respect]:
   assumes "Quotient R1 Abs1 Rep1"
   assumes "Quotient R2 Abs2 Rep2"
   shows "(prod_rel R1 R2 ===> R2) snd snd"
-  by simp
+  by auto
 
 lemma snd_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
-  apply(simp add: fun_eq_iff)
-  apply(simp add: Quotient_abs_rep[OF q2])
-  done
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
 
 lemma split_rsp[quot_respect]:
   shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
-  by auto
+  by (auto intro!: fun_relI elim!: fun_relE)
 
 lemma split_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -96,7 +95,7 @@
 lemma [quot_respect]:
   shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
   prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
-  by auto
+  by (auto simp add: fun_rel_def)
 
 lemma [quot_preserve]:
   assumes q1: "Quotient R1 abs1 rep1"
@@ -114,7 +113,7 @@
 
 lemma prod_fun_id[id_simps]:
   shows "prod_fun id id = id"
-  by (simp add: prod_fun_def)
+  by (simp add: fun_eq_iff)
 
 lemma prod_rel_eq[id_simps]:
   shows "prod_rel (op =) (op =) = (op =)"
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -9,15 +9,15 @@
 begin
 
 fun
-  sum_rel
+  sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
 where
   "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
 
-fun
-  sum_map
+primrec
+  sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
 where
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
@@ -62,13 +62,13 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> sum_rel R1 R2) Inl Inl"
-  by simp
+  by auto
 
 lemma sum_Inr_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R2 ===> sum_rel R1 R2) Inr Inr"
-  by simp
+  by auto
 
 lemma sum_Inl_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -88,11 +88,7 @@
 
 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   unfolding prime_nat_def
-  apply (subst even_mult_two_ex)
-  apply clarify
-  apply (drule_tac x = 2 in spec)
-  apply auto
-done
+  by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat)
 
 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   unfolding prime_int_def
@@ -275,10 +271,8 @@
 
 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   apply (rule prime_imp_coprime_int, assumption)
-  apply (unfold prime_int_altdef, clarify)
-  apply (drule_tac x = q in spec)
-  apply (drule_tac x = p in spec)
-  apply auto
+  apply (unfold prime_int_altdef)
+  apply (metis int_one_le_iff_zero_less zless_le)
 done
 
 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
@@ -291,11 +285,8 @@
   apply (induct n rule: nat_less_induct)
   apply (case_tac "n = 0")
   using two_is_prime_nat apply blast
-  apply (case_tac "prime n")
-  apply blast
-  apply (subgoal_tac "n > 1")
-  apply (frule (1) not_prime_eq_prod_nat)
-  apply (auto intro: dvd_mult dvd_mult2)
+  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less 
+               neq0_conv prime_nat_def)
 done
 
 (* An Isar version:
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -691,14 +691,9 @@
   apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
     and S = "nat ` S", transferred])
   apply auto
-  apply (subst prime_int_def [symmetric])
-  apply auto
-  apply (subgoal_tac "xb >= 0")
-  apply force
-  apply (rule prime_ge_0_int)
-  apply force
-  apply (subst transfer_nat_int_set_return_embed)
-  apply (unfold nat_set_def, auto)
+  apply (metis prime_int_def)
+  apply (metis prime_ge_0_int)
+  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
 done
 
 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
@@ -739,19 +734,13 @@
     "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   apply (simp only: prime_factors_altdef_nat)
   apply auto
-  apply (frule dvd_multiplicity_nat)
-  apply auto
-(* It is a shame that auto and arith don't get this. *)
-  apply (erule order_less_le_trans)back
-  apply assumption
+  apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
 done
 
 lemma dvd_prime_factors_int [intro]:
     "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   apply (auto simp add: prime_factors_altdef_int)
-  apply (erule order_less_le_trans)
-  apply (rule dvd_multiplicity_int)
-  apply auto
+  apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
 done
 
 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
@@ -763,10 +752,8 @@
   apply force
   apply (subst prime_factors_altdef_nat)+
   apply auto
-(* Again, a shame that auto and arith don't get this. *)
-  apply (drule_tac x = xa in spec, auto)
-  apply (rule le_imp_power_dvd)
-  apply blast
+  apply (metis gr0I le_0_eq less_not_refl)
+  apply (metis le_imp_power_dvd)
 done
 
 lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
@@ -778,30 +765,18 @@
   apply force
   apply (subst prime_factors_altdef_int)+
   apply auto
-  apply (rule dvd_power_le)
-  apply auto
-  apply (drule_tac x = xa in spec)
-  apply (erule impE)
-  apply auto
+  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
 done
 
 lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  apply (cases "y = 0")
-  apply auto
-  apply (rule multiplicity_dvd_nat, auto)
-  apply (case_tac "prime p")
-  apply auto
-done
+by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
+          multiplicity_nonprime_nat neq0_conv)
 
 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  apply (cases "y = 0")
-  apply auto
-  apply (rule multiplicity_dvd_int, auto)
-  apply (case_tac "prime p")
-  apply auto
-done
+by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
+          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
 
 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
@@ -820,12 +795,8 @@
   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   apply (subst (asm) prime_factors_altdef_nat, force)
   apply (rule dvd_setprod)
-  apply auto  
-  apply (subst prime_factors_altdef_nat)
-  apply (subst (asm) dvd_multiplicity_eq_nat)
   apply auto
-  apply (drule spec [where x = p])
-  apply auto
+  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
 done
 
 lemma prime_factors_altdef2_int: 
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Quotient.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -5,7 +5,7 @@
 header {* Definition of Quotient Types *}
 
 theory Quotient
-imports Plain Hilbert_Choice
+imports Plain Hilbert_Choice Equiv_Relations
 uses
   ("Tools/Quotient/quotient_info.ML")
   ("Tools/Quotient/quotient_typ.ML")
@@ -21,33 +21,49 @@
 *}
 
 definition
-  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
+  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
+
+lemma refl_reflp:
+  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
+  by (simp add: refl_on_def reflp_def)
 
 definition
-  "reflp E \<equiv> \<forall>x. E x x"
+  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
+
+lemma sym_symp:
+  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
+  by (simp add: sym_def symp_def)
 
 definition
-  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
+
+lemma trans_transp:
+  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
+  by (auto simp add: trans_def transp_def)
 
 definition
-  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
 
 lemma equivp_reflp_symp_transp:
   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
   unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
   by blast
 
+lemma equiv_equivp:
+  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
+  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
+
 lemma equivp_reflp:
   shows "equivp E \<Longrightarrow> E x x"
   by (simp only: equivp_reflp_symp_transp reflp_def)
 
 lemma equivp_symp:
   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
-  by (metis equivp_reflp_symp_transp symp_def)
+  by (simp add: equivp_def)
 
 lemma equivp_transp:
   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
-  by (metis equivp_reflp_symp_transp transp_def)
+  by (simp add: equivp_def)
 
 lemma equivpI:
   assumes "reflp R" "symp R" "transp R"
@@ -62,7 +78,7 @@
 text {* Partial equivalences *}
 
 definition
-  "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
+  "part_equivp E \<longleftrightarrow> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
 lemma equivp_implies_part_equivp:
   assumes a: "equivp E"
@@ -114,6 +130,11 @@
   then show "part_equivp E" unfolding part_equivp_def using a by metis
 qed
 
+lemma part_equivpI:
+  assumes "\<exists>x. R x x" "symp R" "transp R"
+  shows "part_equivp R"
+  using assms by (simp add: part_equivp_refl_symp_transp)
+
 text {* Composition of Relations *}
 
 abbreviation
@@ -128,45 +149,54 @@
 subsection {* Respects predicate *}
 
 definition
-  Respects
+  Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
 where
-  "Respects R x \<equiv> R x x"
+  "Respects R x = R x x"
 
 lemma in_respects:
-  shows "(x \<in> Respects R) = R x x"
+  shows "x \<in> Respects R \<longleftrightarrow> R x x"
   unfolding mem_def Respects_def
   by simp
 
 subsection {* Function map and function relation *}
 
 definition
-  fun_map (infixr "--->" 55)
+  fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
 where
-[simp]: "fun_map f g h x = g (h (f x))"
+  "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
+
+lemma fun_map_apply [simp]:
+  "(f ---> g) h x = g (h (f x))"
+  by (simp add: fun_map_def)
+
+lemma fun_map_id:
+  "(id ---> id) = id"
+  by (simp add: fun_eq_iff id_def)
 
 definition
-  fun_rel (infixr "===>" 55)
+  fun_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" (infixr "===>" 55)
 where
-[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 lemma fun_relI [intro]:
-  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
-  shows "(P ===> Q) x y"
+  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
+  shows "(E1 ===> E2) f g"
   using assms by (simp add: fun_rel_def)
 
-lemma fun_map_id:
-  shows "(id ---> id) = id"
-  by (simp add: fun_eq_iff id_def)
+lemma fun_relE:
+  assumes "(E1 ===> E2) f g" and "E1 x y"
+  obtains "E2 (f x) (g y)"
+  using assms by (simp add: fun_rel_def)
 
 lemma fun_rel_eq:
   shows "((op =) ===> (op =)) = (op =)"
-  by (simp add: fun_eq_iff)
+  by (auto simp add: fun_eq_iff elim: fun_relE)
 
 
 subsection {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<equiv>
+  "Quotient E Abs Rep \<longleftrightarrow>
      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
@@ -232,21 +262,17 @@
   and     q2: "Quotient R2 abs2 rep2"
   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
 proof -
-  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
-    using q1 q2
-    unfolding Quotient_def
-    unfolding fun_eq_iff
-    by simp
+  have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+    using q1 q2 by (simp add: Quotient_def fun_eq_iff)
   moreover
-  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
-    using q1 q2
-    unfolding Quotient_def
-    by (simp (no_asm)) (metis)
+  have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+    by (rule fun_relI)
+      (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
+        simp (no_asm) add: Quotient_def, simp)
   moreover
-  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+  have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
-    unfolding fun_eq_iff
-    apply(auto)
+    apply(auto simp add: fun_rel_def fun_eq_iff)
     using q1 q2 unfolding Quotient_def
     apply(metis)
     using q1 q2 unfolding Quotient_def
@@ -281,7 +307,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by simp
+  by (simp add:)
 
 lemma lambda_prs1:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -289,7 +315,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by simp
+  by (simp add:)
 
 lemma rep_abs_rsp:
   assumes q: "Quotient R Abs Rep"
@@ -317,12 +343,12 @@
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by simp
+  using a by (auto elim: fun_relE)
 
 lemma apply_rsp':
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by simp
+  using a by (auto elim: fun_relE)
 
 subsection {* lemmas for regularisation of ball and bex *}
 
@@ -370,7 +396,7 @@
   apply(rule iffI)
   apply(rule allI)
   apply(drule_tac x="\<lambda>y. f x" in bspec)
-  apply(simp add: in_respects)
+  apply(simp add: in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -384,7 +410,7 @@
   apply(auto)
   apply(rule_tac x="\<lambda>y. f x" in bexI)
   apply(simp)
-  apply(simp add: Respects_def in_respects)
+  apply(simp add: Respects_def in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -429,7 +455,7 @@
 subsection {* Bounded abstraction *}
 
 definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
   "x \<in> p \<Longrightarrow> Babs p m x = m x"
 
@@ -437,10 +463,10 @@
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
-  apply (auto simp add: Babs_def in_respects)
+  apply (auto simp add: Babs_def in_respects fun_rel_def)
   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
-  using a apply (simp add: Babs_def)
-  apply (simp add: in_respects)
+  using a apply (simp add: Babs_def fun_rel_def)
+  apply (simp add: in_respects fun_rel_def)
   using Quotient_rel[OF q]
   by metis
 
@@ -449,7 +475,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   apply (rule ext)
-  apply (simp)
+  apply (simp add:)
   apply (subgoal_tac "Rep1 x \<in> Respects R1")
   apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   apply (simp add: in_respects Quotient_rel_rep[OF q1])
@@ -460,7 +486,7 @@
   shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   apply(rule iffI)
   apply(simp_all only: babs_rsp[OF q])
-  apply(auto simp add: Babs_def)
+  apply(auto simp add: Babs_def fun_rel_def)
   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   apply(metis Babs_def)
   apply (simp add: in_respects)
@@ -478,30 +504,29 @@
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ball (Respects R) f = Ball (Respects R) g"
-  using a by (simp add: Ball_def in_respects)
+  using a by (auto simp add: Ball_def in_respects elim: fun_relE)
 
 lemma bex_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
-  using a by (simp add: Bex_def in_respects)
+  using a by (auto simp add: Bex_def in_respects elim: fun_relE)
 
 lemma bex1_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
-  using a
-  by (simp add: Ex1_def in_respects) auto
+  using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
 
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
   shows "Ball (Respects R) ((absf ---> id) f) = All f"
-  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
   by metis
 
 lemma ex_prs:
   assumes a: "Quotient R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
-  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
   by metis
 
 subsection {* @{text Bex1_rel} quantifier *}
@@ -552,7 +577,7 @@
 lemma bex1_rel_rsp:
   assumes a: "Quotient R absf repf"
   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply rule
   apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
@@ -564,7 +589,7 @@
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
   shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
-apply simp
+apply (simp add:)
 apply (subst Bex1_rel_def)
 apply (subst Bex_def)
 apply (subst Ex1_def)
@@ -643,12 +668,12 @@
   shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
   and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
-  unfolding o_def fun_eq_iff by simp_all
+  by (simp_all add: fun_eq_iff)
 
 lemma o_rsp:
   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
-  unfolding fun_rel_def o_def fun_eq_iff by auto
+  by (auto intro!: fun_relI elim: fun_relE)
 
 lemma cond_prs:
   assumes a: "Quotient R absf repf"
@@ -664,7 +689,7 @@
 lemma if_rsp:
   assumes q: "Quotient R Abs Rep"
   shows "(op = ===> R ===> R ===> R) If If"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma let_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -675,11 +700,11 @@
 
 lemma let_rsp:
   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
-  by auto
+  by (auto intro!: fun_relI elim: fun_relE)
 
 lemma mem_rsp:
   shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
-  by (simp add: mem_def)
+  by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
 
 lemma mem_prs:
   assumes a1: "Quotient R1 Abs1 Rep1"
@@ -689,13 +714,12 @@
 
 lemma id_rsp:
   shows "(R ===> R) id id"
-  by simp
+  by (auto intro: fun_relI)
 
 lemma id_prs:
   assumes a: "Quotient R Abs Rep"
   shows "(Rep ---> Abs) id = id"
-  unfolding fun_eq_iff
-  by (simp add: Quotient_abs_rep[OF a])
+  by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
 
 
 locale quot_type =
@@ -710,12 +734,12 @@
 begin
 
 definition
-  abs::"'a \<Rightarrow> 'b"
+  abs :: "'a \<Rightarrow> 'b"
 where
-  "abs x \<equiv> Abs (R x)"
+  "abs x = Abs (R x)"
 
 definition
-  rep::"'b \<Rightarrow> 'a"
+  rep :: "'b \<Rightarrow> 'a"
 where
   "rep a = Eps (Rep a)"
 
@@ -799,7 +823,9 @@
   about the lifted theorem in a tactic.
 *}
 definition
-  "Quot_True (x :: 'a) \<equiv> True"
+  Quot_True :: "'a \<Rightarrow> bool"
+where
+  "Quot_True x \<longleftrightarrow> True"
 
 lemma
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
@@ -858,4 +884,3 @@
   fun_rel (infixr "===>" 55)
 
 end
-
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -14,10 +14,10 @@
   over lists. The definition of the equivalence:
 *}
 
-fun
+definition
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
-  "list_eq xs ys \<longleftrightarrow> set xs = set ys"
+  [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
@@ -96,8 +96,7 @@
 qed
 
 lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
-  unfolding list_eq.simps
-  by (simp only: set_map)
+  by (simp only: list_eq_def set_map)
 
 lemma quotient_compose_list_g:
   assumes q: "Quotient R Abs Rep"
@@ -167,19 +166,19 @@
 
 lemma list_equiv_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma append_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma sub_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma memb_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op =) memb memb"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma nil_rsp [quot_respect]:
   shows "(op \<approx>) Nil Nil"
@@ -187,35 +186,35 @@
 
 lemma cons_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma map_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma set_rsp [quot_respect]:
   "(op \<approx> ===> op =) set set"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma inter_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma removeAll_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma diff_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma card_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op =) card_list card_list"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma filter_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
-  by simp
+  by (auto intro!: fun_relI)
 
 lemma memb_commute_fold_list:
   assumes a: "rsp_fold f"
@@ -348,13 +347,11 @@
   "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-
 instance
 proof
   fix x y z :: "'a fset"
   show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
-    unfolding less_fset_def 
-    by (descending) (auto)
+    by (unfold less_fset_def, descending) auto
   show "x |\<subseteq>| x"  by (descending) (simp)
   show "{||} |\<subseteq>| x" by (descending) (simp)
   show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
@@ -451,7 +448,7 @@
 
 lemma Cons_rsp2 [quot_respect]:
   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
-  apply auto
+  apply (auto intro!: fun_relI)
   apply (rule_tac b="x # b" in pred_compI)
   apply auto
   apply (rule_tac b="x # ba" in pred_compI)
@@ -477,7 +474,7 @@
   assumes a: "reflp R"
   and b: "list_all2 R l r"
   shows "list_all2 R (z @ l) (z @ r)"
-  by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
+  by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def])
 
 lemma append_rsp2_pre0:
   assumes a:"list_all2 op \<approx> x x'"
@@ -490,7 +487,7 @@
   shows "list_all2 op \<approx> (z @ x) (z @ x')"
   using a apply (induct x x' arbitrary: z rule: list_induct2')
   apply (rule list_all2_refl'[OF list_eq_equivp])
-  apply (simp_all del: list_eq.simps)
+  apply (simp_all del: list_eq_def)
   apply (rule list_all2_app_l)
   apply (simp_all add: reflp_def)
   done
@@ -760,7 +757,7 @@
 
 lemma inj_map_fset_cong:
   shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
-  by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
+  by (descending) (metis inj_vimage_image_eq list_eq_def set_map)
 
 lemma map_union_fset: 
   shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
@@ -1111,7 +1108,7 @@
 	apply(blast)
 	done
       then obtain a where e: "memb a l" by auto
-      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
+      then have e': "memb a r" using list_eq_def [simplified memb_def [symmetric], of l r] b 
 	by auto
       have f: "card_list (removeAll a l) = m" using e d by (simp)
       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -77,7 +77,7 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
   and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
   and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma times_int_raw_fst:
   assumes a: "x \<approx> z"
@@ -167,7 +167,7 @@
 
 lemma[quot_respect]:
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-  by (simp add: equivp_reflp[OF int_equivp])
+  by (auto simp add: equivp_reflp [OF int_equivp])
 
 lemma int_of_nat:
   shows "of_nat m = int_of_nat m"
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Quotient_Examples/Quotient_Message.thy
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Wed Nov 10 16:05:15 2010 +0100
@@ -179,11 +179,11 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op =) freenonces freenonces"
-  by (simp add: msgrel_imp_eq_freenonces)
+  by (auto simp add: msgrel_imp_eq_freenonces)
 
 lemma [quot_respect]:
   shows "(op = ===> op \<sim>) NONCE NONCE"
-  by (simp add: NONCE)
+  by (auto simp add: NONCE)
 
 lemma nonces_Nonce [simp]:
   shows "nonces (Nonce N) = {N}"
@@ -191,7 +191,7 @@
 
 lemma [quot_respect]:
   shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
-  by (simp add: MPAIR)
+  by (auto simp add: MPAIR)
 
 lemma nonces_MPair [simp]:
   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
@@ -214,7 +214,7 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
-  by (simp add: msgrel_imp_eqv_freeleft)
+  by (auto simp add: msgrel_imp_eqv_freeleft)
 
 lemma left_Nonce [simp]:
   shows "left (Nonce N) = Nonce N"
@@ -243,7 +243,7 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op \<sim>) freeright freeright"
-  by (simp add: msgrel_imp_eqv_freeright)
+  by (auto simp add: msgrel_imp_eqv_freeright)
 
 lemma right_Nonce [simp]:
   shows "right (Nonce N) = Nonce N"
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -434,7 +434,7 @@
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
         if member (op=) xs h
         then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
+        else Conv.rewr_conv @{thm fun_map_apply [THEN eq_reflection]} ctrm
   | _ => Conv.all_conv ctrm
 
 fun fun_map_conv xs ctxt ctrm =
diff -r b6feba6c9fcc -r 34823a2cba08 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 10 15:59:23 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -449,7 +449,7 @@
     val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   in
     if too_many_facts_perhaps andalso iter < smt_max_iter andalso
-       not (null facts) andalso timeout > Time.zeroTime then
+       not (null facts) andalso Time.> (timeout, Time.zeroTime) then
       let val facts = take (length facts div smt_iter_fact_divisor) facts in
         smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state
                         facts i