# HG changeset patch
# User kuncar
# Date 1332508649 -3600
# Node ID fa3538d6004ba8b8952eec01fe1a2796f6a87ab1
# Parent  d5cd13aca90ba3cc9acfb7c6f83f99aa105749f5
fix Quotient_Examples

diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -115,6 +115,7 @@
 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
 
 quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
+unfolding add_raw_def by auto
 
 lemma "add x y = add x x"
 nitpick [show_datatypes, expect = genuine]
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/DList.thy
--- a/src/HOL/Quotient_Examples/DList.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/DList.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -88,45 +88,32 @@
 definition [simp]: "card_remdups = length \<circ> remdups"
 definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
 
-lemma [quot_respect]:
-  "(dlist_eq) Nil Nil"
-  "(dlist_eq ===> op =) List.member List.member"
-  "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
-  "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
-  "(dlist_eq ===> op =) card_remdups card_remdups"
-  "(dlist_eq ===> op =) remdups remdups"
-  "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
-  "(op = ===> dlist_eq ===> dlist_eq) map map"
-  "(op = ===> dlist_eq ===> dlist_eq) filter filter"
-  by (auto intro!: fun_relI simp add: remdups_filter)
-     (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+
-
 quotient_definition empty where "empty :: 'a dlist"
-  is "Nil"
+  is "Nil" done
 
 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
-  is "Cons"
+  is "Cons" by (metis (mono_tags) List.insert_def dlist_eq_def remdups.simps(2) set_remdups)
 
 quotient_definition "member :: 'a dlist \<Rightarrow> 'a \<Rightarrow> bool"
-  is "List.member"
+  is "List.member" by (metis dlist_eq_def remdups_eq_member_eq)
 
 quotient_definition foldr where "foldr :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b"
-  is "foldr_remdups"
+  is "foldr_remdups" by auto
 
 quotient_definition "remove :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
-  is "removeAll"
+  is "removeAll" by force
 
 quotient_definition card where "card :: 'a dlist \<Rightarrow> nat"
-  is "card_remdups"
+  is "card_remdups" by fastforce
 
 quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist"
-  is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+  is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" by (metis dlist_eq_def remdups_eq_map_eq)
 
 quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
-  is "List.filter"
+  is "List.filter" by (metis dlist_eq_def remdups_filter)
 
 quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
-  is "remdups"
+  is "remdups" by simp
 
 text {* lifted theorems *}
 
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -179,140 +179,6 @@
   by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
 
 
-
-subsection {* Respectfulness lemmas for list operations *}
-
-lemma list_equiv_rsp [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
-  by (auto intro!: fun_relI)
-
-lemma append_rsp [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
-  by (auto intro!: fun_relI)
-
-lemma sub_list_rsp [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-  by (auto intro!: fun_relI)
-
-lemma member_rsp [quot_respect]:
-  shows "(op \<approx> ===> op =) List.member List.member"
-proof
-  fix x y assume "x \<approx> y"
-  then show "List.member x = List.member y"
-    unfolding fun_eq_iff by simp
-qed
-
-lemma nil_rsp [quot_respect]:
-  shows "(op \<approx>) Nil Nil"
-  by simp
-
-lemma cons_rsp [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
-  by (auto intro!: fun_relI)
-
-lemma map_rsp [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-  by (auto intro!: fun_relI)
-
-lemma set_rsp [quot_respect]:
-  "(op \<approx> ===> op =) set set"
-  by (auto intro!: fun_relI)
-
-lemma inter_list_rsp [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
-  by (auto intro!: fun_relI)
-
-lemma removeAll_rsp [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
-  by (auto intro!: fun_relI)
-
-lemma diff_list_rsp [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
-  by (auto intro!: fun_relI)
-
-lemma card_list_rsp [quot_respect]:
-  shows "(op \<approx> ===> op =) card_list card_list"
-  by (auto intro!: fun_relI)
-
-lemma filter_rsp [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
-  by (auto intro!: fun_relI)
-
-lemma remdups_removeAll: (*FIXME move*)
-  "remdups (removeAll x xs) = remove1 x (remdups xs)"
-  by (induct xs) auto
-
-lemma member_commute_fold_once:
-  assumes "rsp_fold f"
-    and "x \<in> set xs"
-  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
-proof -
-  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
-    by (auto intro!: fold_remove1_split elim: rsp_foldE)
-  then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
-qed
-
-lemma fold_once_set_equiv:
-  assumes "xs \<approx> ys"
-  shows "fold_once f xs = fold_once f ys"
-proof (cases "rsp_fold f")
-  case False then show ?thesis by simp
-next
-  case True
-  then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
-    by (rule rsp_foldE)
-  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
-    by (simp add: set_eq_iff_multiset_of_remdups_eq)
-  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
-    by (rule fold_multiset_equiv)
-  with True show ?thesis by (simp add: fold_once_fold_remdups)
-qed
-
-lemma fold_once_rsp [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op =) fold_once fold_once"
-  unfolding fun_rel_def by (auto intro: fold_once_set_equiv) 
-
-lemma concat_rsp_pre:
-  assumes a: "list_all2 op \<approx> x x'"
-  and     b: "x' \<approx> y'"
-  and     c: "list_all2 op \<approx> y' y"
-  and     d: "\<exists>x\<in>set x. xa \<in> set x"
-  shows "\<exists>x\<in>set y. xa \<in> set x"
-proof -
-  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
-  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
-  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
-  have "ya \<in> set y'" using b h by simp
-  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
-  then show ?thesis using f i by auto
-qed
-
-lemma concat_rsp [quot_respect]:
-  shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-proof (rule fun_relI, elim pred_compE)
-  fix a b ba bb
-  assume a: "list_all2 op \<approx> a ba"
-  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
-  assume b: "ba \<approx> bb"
-  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
-  assume c: "list_all2 op \<approx> bb b"
-  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
-  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
-  proof
-    fix x
-    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
-    proof
-      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
-      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
-    next
-      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
-      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
-    qed
-  qed
-  then show "concat a \<approx> concat b" by auto
-qed
-
-
 section {* Quotient definitions for fsets *}
 
 
@@ -323,7 +189,7 @@
 
 quotient_definition
   "bot :: 'a fset" 
-  is "Nil :: 'a list"
+  is "Nil :: 'a list" done
 
 abbreviation
   empty_fset  ("{||}")
@@ -332,7 +198,7 @@
 
 quotient_definition
   "less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
-  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
+  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" by simp
 
 abbreviation
   subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
@@ -351,7 +217,7 @@
 
 quotient_definition
   "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp
 
 abbreviation
   union_fset (infixl "|\<union>|" 65)
@@ -360,7 +226,7 @@
 
 quotient_definition
   "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp
 
 abbreviation
   inter_fset (infixl "|\<inter>|" 65)
@@ -369,7 +235,7 @@
 
 quotient_definition
   "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by fastforce
 
 instance
 proof
@@ -413,7 +279,7 @@
 
 quotient_definition
   "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is "Cons"
+  is "Cons" by auto
 
 syntax
   "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
@@ -425,7 +291,7 @@
 quotient_definition
   fset_member
 where
-  "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member"
+  "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" by fastforce
 
 abbreviation
   in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50)
@@ -442,31 +308,84 @@
 
 quotient_definition
   "card_fset :: 'a fset \<Rightarrow> nat"
-  is card_list
+  is card_list by simp
 
 quotient_definition
   "map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-  is map
+  is map by simp
 
 quotient_definition
   "remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is removeAll
+  is removeAll by simp
 
 quotient_definition
   "fset :: 'a fset \<Rightarrow> 'a set"
-  is "set"
+  is "set" by simp
+
+lemma fold_once_set_equiv:
+  assumes "xs \<approx> ys"
+  shows "fold_once f xs = fold_once f ys"
+proof (cases "rsp_fold f")
+  case False then show ?thesis by simp
+next
+  case True
+  then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+    by (rule rsp_foldE)
+  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
+    by (simp add: set_eq_iff_multiset_of_remdups_eq)
+  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
+    by (rule fold_multiset_equiv)
+  with True show ?thesis by (simp add: fold_once_fold_remdups)
+qed
 
 quotient_definition
   "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
-  is fold_once
+  is fold_once by (rule fold_once_set_equiv)
+
+lemma concat_rsp_pre:
+  assumes a: "list_all2 op \<approx> x x'"
+  and     b: "x' \<approx> y'"
+  and     c: "list_all2 op \<approx> y' y"
+  and     d: "\<exists>x\<in>set x. xa \<in> set x"
+  shows "\<exists>x\<in>set y. xa \<in> set x"
+proof -
+  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
+  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
+  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
+  have "ya \<in> set y'" using b h by simp
+  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
+  then show ?thesis using f i by auto
+qed
 
 quotient_definition
   "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
-  is concat
+  is concat 
+proof (elim pred_compE)
+fix a b ba bb
+  assume a: "list_all2 op \<approx> a ba"
+  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
+  assume b: "ba \<approx> bb"
+  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
+  assume c: "list_all2 op \<approx> bb b"
+  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
+  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
+  proof
+    fix x
+    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
+    proof
+      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+    next
+      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+    qed
+  qed
+  then show "concat a \<approx> concat b" by auto
+qed
 
 quotient_definition
   "filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-  is filter
+  is filter by force
 
 
 subsection {* Compositional respectfulness and preservation lemmas *}
@@ -538,7 +457,7 @@
 
 lemma append_rsp2 [quot_respect]:
   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
-  by (intro compositional_rsp3 append_rsp)
+  by (intro compositional_rsp3)
      (auto intro!: fun_relI simp add: append_rsp2_pre)
 
 lemma map_rsp2 [quot_respect]:
@@ -967,6 +886,20 @@
   (if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)"
   by descending (simp add: fold_once_fold_remdups)
 
+lemma remdups_removeAll:
+  "remdups (removeAll x xs) = remove1 x (remdups xs)"
+  by (induct xs) auto
+
+lemma member_commute_fold_once:
+  assumes "rsp_fold f"
+    and "x \<in> set xs"
+  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
+proof -
+  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
+    by (auto intro!: fold_remove1_split elim: rsp_foldE)
+  then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
+qed
+
 lemma in_commute_fold_fset:
   "rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h"
   by descending (simp add: member_commute_fold_once)
@@ -1170,7 +1103,7 @@
       then have e': "List.member r a" using list_eq_def [simplified List.member_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
+      have g: "removeAll a l \<approx> removeAll a r" using remove_fset_rsp b by simp
       have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
       have i: "l \<approx>2 (a # removeAll a l)"
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -23,17 +23,17 @@
   by (simp add: identity_equivp)
 
 quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"  is
-  "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
+  "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" done
 
 quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is 
-  fcomp
+  fcomp done
 
 quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd" 
-  is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
+  is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" done
 
-quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on
+quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on done
 
-quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw
+quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw done
 
 
 subsection {* Co/Contravariant type variables *} 
@@ -47,7 +47,7 @@
   where "map_endofun' f g e = map_fun g f e"
 
 quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is
-  map_endofun'
+  map_endofun' done
 
 text {* Registration of the map function for 'a endofun. *}
 
@@ -63,7 +63,7 @@
     by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
 qed
 
-quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
+quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
 
 term  endofun_id_id
 thm  endofun_id_id_def
@@ -73,7 +73,7 @@
 text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting)
   over a type variable which is a covariant and contravariant type variable. *}
 
-quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id
+quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done
 
 term  endofun'_id_id
 thm  endofun'_id_id_def
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Lift_RBT.thy
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -18,7 +18,7 @@
 local_setup {* fn lthy =>
 let
   val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"},
-    equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+    equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
   val qty_full_name = @{type_name "rbt"}
 
   fun qinfo phi = Quotient_Info.transform_quotients phi quotients
@@ -50,6 +50,7 @@
 subsection {* Primitive operations *}
 
 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
+done
 
 declare lookup_def[unfolded map_fun_def comp_def id_def, code]
 
@@ -67,21 +68,21 @@
 *)
 
 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
-is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)"
+is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
 
 lemma impl_of_empty [code abstract]:
   "impl_of empty = RBT_Impl.Empty"
   by (simp add: empty_def RBT_inverse)
 
 quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.insert"
+is "RBT_Impl.insert" done
 
 lemma impl_of_insert [code abstract]:
   "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
   by (simp add: insert_def RBT_inverse)
 
 quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.delete"
+is "RBT_Impl.delete" done
 
 lemma impl_of_delete [code abstract]:
   "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
@@ -89,24 +90,24 @@
 
 (* FIXME: unnecessary type annotations *)
 quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
-is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list"
+is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
 
 lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
 unfolding entries_def map_fun_def comp_def id_def ..
 
 (* FIXME: unnecessary type annotations *)
 quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
-is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list"
+is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
 
 quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.bulkload"
+is "RBT_Impl.bulkload" done
 
 lemma impl_of_bulkload [code abstract]:
   "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
   by (simp add: bulkload_def RBT_inverse)
 
 quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.map_entry"
+is "RBT_Impl.map_entry" done
 
 lemma impl_of_map_entry [code abstract]:
   "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
@@ -115,13 +116,15 @@
 (* FIXME: unnecesary type annotations *)
 quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
 is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
+done
 
 lemma impl_of_map [code abstract]:
   "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
   by (simp add: map_def RBT_inverse)
 
 (* FIXME: unnecessary type annotations *)
-quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c"
+quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
+is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
 
 lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
 unfolding fold_def map_fun_def comp_def id_def ..
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Lift_Set.thy
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -20,7 +20,7 @@
   let
     val quotients =
       {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
-        equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+        equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
     val qty_full_name = @{type_name "set"}
 
     fun qinfo phi = Quotient_Info.transform_quotients phi quotients
@@ -37,7 +37,7 @@
 text {* Now, we can employ quotient_definition to lift definitions. *}
 
 quotient_definition empty where "empty :: 'a set"
-is "bot :: 'a \<Rightarrow> bool"
+is "bot :: 'a \<Rightarrow> bool" done
 
 term "Lift_Set.empty"
 thm Lift_Set.empty_def
@@ -46,7 +46,7 @@
   "insertp x P y \<longleftrightarrow> y = x \<or> P y"
 
 quotient_definition insert where "insert :: 'a => 'a set => 'a set"
-is insertp
+is insertp done
 
 term "Lift_Set.insert"
 thm Lift_Set.insert_def
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Cset.thy
--- a/src/HOL/Quotient_Examples/Quotient_Cset.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -21,75 +21,50 @@
 
 subsection {* Operations *}
 
-lemma [quot_respect]:
-  "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
-  "(op = ===> set_eq) Collect Collect"
-  "(set_eq ===> op =) Set.is_empty Set.is_empty"
-  "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
-  "(op = ===> set_eq ===> set_eq) Set.remove Set.remove"
-  "(op = ===> set_eq ===> set_eq) image image"
-  "(op = ===> set_eq ===> set_eq) Set.project Set.project"
-  "(set_eq ===> op =) Ball Ball"
-  "(set_eq ===> op =) Bex Bex"
-  "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
-  "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
-  "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
-  "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
-  "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
-  "set_eq {} {}"
-  "set_eq UNIV UNIV"
-  "(set_eq ===> set_eq) uminus uminus"
-  "(set_eq ===> set_eq ===> set_eq) minus minus"
-  "(set_eq ===> op =) Inf Inf"
-  "(set_eq ===> op =) Sup Sup"
-  "(op = ===> set_eq) List.set List.set"
-  "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
-by (auto simp: fun_rel_eq)
-
 quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
-is "op \<in>"
+is "op \<in>" by simp
 quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
-is Collect
+is Collect done
 quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
-is Set.is_empty
+is Set.is_empty by simp 
 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.insert
+is Set.insert by simp
 quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.remove
+is Set.remove by simp
 quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
-is image
+is image by simp
 quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.project
+is Set.project by simp
 quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Ball
+is Ball by simp
 quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Bex
+is Bex by simp
 quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
-is Finite_Set.card
+is Finite_Set.card by simp
 quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
-is List.set
+is List.set done
 quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
-is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
 quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
-is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
 quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
 quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
 quotient_definition empty where "empty :: 'a Quotient_Cset.set"
-is "{} :: 'a set"
+is "{} :: 'a set" done
 quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
-is "Set.UNIV :: 'a set"
+is "Set.UNIV :: 'a set" done
 quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
+is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" by simp
 quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
 quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
-is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
+is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" by simp
 quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
-is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
+is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" by simp
 quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
-is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" by simp
 
 hide_const (open) is_empty insert remove map filter forall exists card
   set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -22,10 +22,10 @@
 begin
 
 quotient_definition
-  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" done
 
 quotient_definition
-  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" done
 
 fun
   plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -33,7 +33,7 @@
   "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_definition
-  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
 
 fun
   uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -41,7 +41,7 @@
   "uminus_int_raw (x, y) = (y, x)"
 
 quotient_definition
-  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw" by auto
 
 definition
   minus_int_def:  "z - w = z + (-w\<Colon>int)"
@@ -51,8 +51,38 @@
 where
   "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
+lemma times_int_raw_fst:
+  assumes a: "x \<approx> z"
+  shows "times_int_raw x y \<approx> times_int_raw z y"
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: times_int_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+done
+
+lemma times_int_raw_snd:
+  assumes a: "x \<approx> z"
+  shows "times_int_raw y x \<approx> times_int_raw y z"
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: times_int_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+done
+
 quotient_definition
   "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+  apply(rule equivp_transp[OF int_equivp])
+  apply(rule times_int_raw_fst)
+  apply(assumption)
+  apply(rule times_int_raw_snd)
+  apply(assumption)
+done
 
 fun
   le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -60,7 +90,7 @@
   "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_definition
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
 
 definition
   less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -75,47 +105,6 @@
 
 end
 
-lemma [quot_respect]:
-  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 intro!: fun_relI)
-
-lemma times_int_raw_fst:
-  assumes a: "x \<approx> z"
-  shows "times_int_raw x y \<approx> times_int_raw z y"
-  using a
-  apply(cases x, cases y, cases z)
-  apply(auto simp add: times_int_raw.simps intrel.simps)
-  apply(rename_tac u v w x y z)
-  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: mult_ac)
-  apply(simp add: add_mult_distrib [symmetric])
-  done
-
-lemma times_int_raw_snd:
-  assumes a: "x \<approx> z"
-  shows "times_int_raw y x \<approx> times_int_raw y z"
-  using a
-  apply(cases x, cases y, cases z)
-  apply(auto simp add: times_int_raw.simps intrel.simps)
-  apply(rename_tac u v w x y z)
-  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: mult_ac)
-  apply(simp add: add_mult_distrib [symmetric])
-  done
-
-lemma [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
-  apply(simp only: fun_rel_def)
-  apply(rule allI | rule impI)+
-  apply(rule equivp_transp[OF int_equivp])
-  apply(rule times_int_raw_fst)
-  apply(assumption)
-  apply(rule times_int_raw_snd)
-  apply(assumption)
-  done
-
 
 text{* The integers form a @{text comm_ring_1}*}
 
@@ -165,11 +154,7 @@
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
 quotient_definition
-  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
-
-lemma[quot_respect]:
-  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-  by (auto simp add: equivp_reflp [OF int_equivp])
+  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" done
 
 lemma int_of_nat:
   shows "of_nat m = int_of_nat m"
@@ -304,11 +289,7 @@
 quotient_definition
   "int_to_nat::int \<Rightarrow> nat"
 is
-  "int_to_nat_raw"
-
-lemma [quot_respect]:
-  shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
-  by (auto iff: int_to_nat_raw_def)
+  "int_to_nat_raw" unfolding int_to_nat_raw_def by force
 
 lemma nat_le_eq_zle:
   fixes w z::"int"
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Message.thy
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -136,29 +136,25 @@
   "Nonce :: nat \<Rightarrow> msg"
 is
   "NONCE"
+done
 
 quotient_definition
   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
 is
   "MPAIR"
+by (rule MPAIR)
 
 quotient_definition
   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
 is
   "CRYPT"
+by (rule CRYPT)
 
 quotient_definition
   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
 is
   "DECRYPT"
-
-lemma [quot_respect]:
-  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-lemma [quot_respect]:
-  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
-by (auto intro: DECRYPT)
+by (rule DECRYPT)
 
 text{*Establishing these two equations is the point of the whole exercise*}
 theorem CD_eq [simp]:
@@ -175,25 +171,14 @@
    "nonces:: msg \<Rightarrow> nat set"
 is
   "freenonces"
+by (rule msgrel_imp_eq_freenonces)
 
 text{*Now prove the four equations for @{term nonces}*}
 
-lemma [quot_respect]:
-  shows "(op \<sim> ===> op =) freenonces freenonces"
-  by (auto simp add: msgrel_imp_eq_freenonces)
-
-lemma [quot_respect]:
-  shows "(op = ===> op \<sim>) NONCE NONCE"
-  by (auto simp add: NONCE)
-
 lemma nonces_Nonce [simp]:
   shows "nonces (Nonce N) = {N}"
   by (lifting freenonces.simps(1))
 
-lemma [quot_respect]:
-  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
-  by (auto simp add: MPAIR)
-
 lemma nonces_MPair [simp]:
   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
   by (lifting freenonces.simps(2))
@@ -212,10 +197,7 @@
   "left:: msg \<Rightarrow> msg"
 is
   "freeleft"
-
-lemma [quot_respect]:
-  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
-  by (auto simp add: msgrel_imp_eqv_freeleft)
+by (rule msgrel_imp_eqv_freeleft)
 
 lemma left_Nonce [simp]:
   shows "left (Nonce N) = Nonce N"
@@ -239,13 +221,10 @@
   "right:: msg \<Rightarrow> msg"
 is
   "freeright"
+by (rule msgrel_imp_eqv_freeright)
 
 text{*Now prove the four equations for @{term right}*}
 
-lemma [quot_respect]:
-  shows "(op \<sim> ===> op \<sim>) freeright freeright"
-  by (auto simp add: msgrel_imp_eqv_freeright)
-
 lemma right_Nonce [simp]:
   shows "right (Nonce N) = Nonce N"
   by (lifting freeright.simps(1))
@@ -352,13 +331,10 @@
   "discrim:: msg \<Rightarrow> int"
 is
   "freediscrim"
+by (rule msgrel_imp_eq_freediscrim)
 
 text{*Now prove the four equations for @{term discrim}*}
 
-lemma [quot_respect]:
-  shows "(op \<sim> ===> op =) freediscrim freediscrim"
-  by (auto simp add: msgrel_imp_eq_freediscrim)
-
 lemma discrim_Nonce [simp]:
   shows "discrim (Nonce N) = 0"
   by (lifting freediscrim.simps(1))
diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -32,28 +32,29 @@
 begin
 
 quotient_definition
-  "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)"
+  "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)" by simp
 
 quotient_definition
-  "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)"
+  "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)" by simp
 
 fun times_rat_raw where
   "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
 
 quotient_definition
-  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw
+  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult_assoc mult_left_commute)
 
 fun plus_rat_raw where
   "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
 
 quotient_definition
-  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw
+  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw 
+  by (auto simp add: mult_commute mult_left_commute int_distrib(2))
 
 fun uminus_rat_raw where
   "uminus_rat_raw (a :: int, b :: int) = (-a, b)"
 
 quotient_definition
-  "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw"
+  "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw" by fastforce
 
 definition
   minus_rat_def: "a - b = a + (-b\<Colon>rat)"
@@ -63,6 +64,32 @@
 
 quotient_definition
   "(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw"
+proof -
+  {
+    fix a b c d e f g h :: int
+    assume "a * f * (b * f) \<le> e * b * (b * f)"
+    then have le: "a * f * b * f \<le> e * b * b * f" by simp
+    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
+    then have b2: "b * b > 0"
+      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+    have f2: "f * f > 0" using nz(3)
+      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+    assume eq: "a * d = c * b" "e * h = g * f"
+    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
+      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
+      by (metis (no_types) mult_assoc mult_commute)
+    then have "c * f * f * d \<le> e * f * d * d" using b2
+      by (metis leD linorder_le_less_linear mult_strict_right_mono)
+    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
+      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
+      by (metis (no_types) mult_assoc mult_commute)
+    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
+      by (metis leD linorder_le_less_linear mult_strict_right_mono)
+  }
+  then show "\<And>x y xa ya. x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> le_rat_raw x xa = le_rat_raw y ya" by auto
+qed
 
 definition
   less_rat_def: "(z\<Colon>rat) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -83,14 +110,7 @@
 where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))"
 
 quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is
-  Fract_raw
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) times_rat_raw times_rat_raw"
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_rat_raw plus_rat_raw"
-  "(op \<approx> ===> op \<approx>) uminus_rat_raw uminus_rat_raw"
-  "(op = ===> op = ===> op \<approx>) Fract_raw Fract_raw"
-  by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2))
+  Fract_raw by simp
 
 lemmas [simp] = Respects_def
 
@@ -156,15 +176,11 @@
   "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
 
 quotient_definition
-  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw
+  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw by (force simp add: mult_commute)
 
 definition
   divide_rat_def: "q / r = q * inverse (r::rat)"
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx>) rat_inverse_raw rat_inverse_raw"
-  by (auto intro!: fun_relI simp add: mult_commute)
-
 instance proof
   fix q :: rat
   assume "q \<noteq> 0"
@@ -179,34 +195,6 @@
 
 end
 
-lemma [quot_respect]: "(op \<approx> ===> op \<approx> ===> op =) le_rat_raw le_rat_raw"
-proof -
-  {
-    fix a b c d e f g h :: int
-    assume "a * f * (b * f) \<le> e * b * (b * f)"
-    then have le: "a * f * b * f \<le> e * b * b * f" by simp
-    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
-    then have b2: "b * b > 0"
-      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
-    have f2: "f * f > 0" using nz(3)
-      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
-    assume eq: "a * d = c * b" "e * h = g * f"
-    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
-      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
-    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
-      by (metis (no_types) mult_assoc mult_commute)
-    then have "c * f * f * d \<le> e * f * d * d" using b2
-      by (metis leD linorder_le_less_linear mult_strict_right_mono)
-    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
-      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
-    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
-      by (metis (no_types) mult_assoc mult_commute)
-    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
-      by (metis leD linorder_le_less_linear mult_strict_right_mono)
-  }
-  then show ?thesis by (auto intro!: fun_relI)
-qed
-
 instantiation rat :: linorder
 begin