fix Quotient_Examples
authorkuncar
Fri Mar 23 14:17:29 2012 +0100 (2012-03-23)
changeset 47092fa3538d6004b
parent 47091 d5cd13aca90b
child 47093 0516a6c1ea59
fix Quotient_Examples
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Quotient_Examples/DList.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Lift_Fun.thy
src/HOL/Quotient_Examples/Lift_RBT.thy
src/HOL/Quotient_Examples/Lift_Set.thy
src/HOL/Quotient_Examples/Quotient_Cset.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 23 14:03:58 2012 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 23 14:17:29 2012 +0100
     1.3 @@ -115,6 +115,7 @@
     1.4  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
     1.5  
     1.6  quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
     1.7 +unfolding add_raw_def by auto
     1.8  
     1.9  lemma "add x y = add x x"
    1.10  nitpick [show_datatypes, expect = genuine]
     2.1 --- a/src/HOL/Quotient_Examples/DList.thy	Fri Mar 23 14:03:58 2012 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Fri Mar 23 14:17:29 2012 +0100
     2.3 @@ -88,45 +88,32 @@
     2.4  definition [simp]: "card_remdups = length \<circ> remdups"
     2.5  definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
     2.6  
     2.7 -lemma [quot_respect]:
     2.8 -  "(dlist_eq) Nil Nil"
     2.9 -  "(dlist_eq ===> op =) List.member List.member"
    2.10 -  "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
    2.11 -  "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
    2.12 -  "(dlist_eq ===> op =) card_remdups card_remdups"
    2.13 -  "(dlist_eq ===> op =) remdups remdups"
    2.14 -  "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
    2.15 -  "(op = ===> dlist_eq ===> dlist_eq) map map"
    2.16 -  "(op = ===> dlist_eq ===> dlist_eq) filter filter"
    2.17 -  by (auto intro!: fun_relI simp add: remdups_filter)
    2.18 -     (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+
    2.19 -
    2.20  quotient_definition empty where "empty :: 'a dlist"
    2.21 -  is "Nil"
    2.22 +  is "Nil" done
    2.23  
    2.24  quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
    2.25 -  is "Cons"
    2.26 +  is "Cons" by (metis (mono_tags) List.insert_def dlist_eq_def remdups.simps(2) set_remdups)
    2.27  
    2.28  quotient_definition "member :: 'a dlist \<Rightarrow> 'a \<Rightarrow> bool"
    2.29 -  is "List.member"
    2.30 +  is "List.member" by (metis dlist_eq_def remdups_eq_member_eq)
    2.31  
    2.32  quotient_definition foldr where "foldr :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b"
    2.33 -  is "foldr_remdups"
    2.34 +  is "foldr_remdups" by auto
    2.35  
    2.36  quotient_definition "remove :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
    2.37 -  is "removeAll"
    2.38 +  is "removeAll" by force
    2.39  
    2.40  quotient_definition card where "card :: 'a dlist \<Rightarrow> nat"
    2.41 -  is "card_remdups"
    2.42 +  is "card_remdups" by fastforce
    2.43  
    2.44  quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist"
    2.45 -  is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
    2.46 +  is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" by (metis dlist_eq_def remdups_eq_map_eq)
    2.47  
    2.48  quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
    2.49 -  is "List.filter"
    2.50 +  is "List.filter" by (metis dlist_eq_def remdups_filter)
    2.51  
    2.52  quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
    2.53 -  is "remdups"
    2.54 +  is "remdups" by simp
    2.55  
    2.56  text {* lifted theorems *}
    2.57  
     3.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 23 14:03:58 2012 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 23 14:17:29 2012 +0100
     3.3 @@ -179,140 +179,6 @@
     3.4    by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
     3.5  
     3.6  
     3.7 -
     3.8 -subsection {* Respectfulness lemmas for list operations *}
     3.9 -
    3.10 -lemma list_equiv_rsp [quot_respect]:
    3.11 -  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
    3.12 -  by (auto intro!: fun_relI)
    3.13 -
    3.14 -lemma append_rsp [quot_respect]:
    3.15 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
    3.16 -  by (auto intro!: fun_relI)
    3.17 -
    3.18 -lemma sub_list_rsp [quot_respect]:
    3.19 -  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
    3.20 -  by (auto intro!: fun_relI)
    3.21 -
    3.22 -lemma member_rsp [quot_respect]:
    3.23 -  shows "(op \<approx> ===> op =) List.member List.member"
    3.24 -proof
    3.25 -  fix x y assume "x \<approx> y"
    3.26 -  then show "List.member x = List.member y"
    3.27 -    unfolding fun_eq_iff by simp
    3.28 -qed
    3.29 -
    3.30 -lemma nil_rsp [quot_respect]:
    3.31 -  shows "(op \<approx>) Nil Nil"
    3.32 -  by simp
    3.33 -
    3.34 -lemma cons_rsp [quot_respect]:
    3.35 -  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
    3.36 -  by (auto intro!: fun_relI)
    3.37 -
    3.38 -lemma map_rsp [quot_respect]:
    3.39 -  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
    3.40 -  by (auto intro!: fun_relI)
    3.41 -
    3.42 -lemma set_rsp [quot_respect]:
    3.43 -  "(op \<approx> ===> op =) set set"
    3.44 -  by (auto intro!: fun_relI)
    3.45 -
    3.46 -lemma inter_list_rsp [quot_respect]:
    3.47 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
    3.48 -  by (auto intro!: fun_relI)
    3.49 -
    3.50 -lemma removeAll_rsp [quot_respect]:
    3.51 -  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
    3.52 -  by (auto intro!: fun_relI)
    3.53 -
    3.54 -lemma diff_list_rsp [quot_respect]:
    3.55 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
    3.56 -  by (auto intro!: fun_relI)
    3.57 -
    3.58 -lemma card_list_rsp [quot_respect]:
    3.59 -  shows "(op \<approx> ===> op =) card_list card_list"
    3.60 -  by (auto intro!: fun_relI)
    3.61 -
    3.62 -lemma filter_rsp [quot_respect]:
    3.63 -  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
    3.64 -  by (auto intro!: fun_relI)
    3.65 -
    3.66 -lemma remdups_removeAll: (*FIXME move*)
    3.67 -  "remdups (removeAll x xs) = remove1 x (remdups xs)"
    3.68 -  by (induct xs) auto
    3.69 -
    3.70 -lemma member_commute_fold_once:
    3.71 -  assumes "rsp_fold f"
    3.72 -    and "x \<in> set xs"
    3.73 -  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
    3.74 -proof -
    3.75 -  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
    3.76 -    by (auto intro!: fold_remove1_split elim: rsp_foldE)
    3.77 -  then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
    3.78 -qed
    3.79 -
    3.80 -lemma fold_once_set_equiv:
    3.81 -  assumes "xs \<approx> ys"
    3.82 -  shows "fold_once f xs = fold_once f ys"
    3.83 -proof (cases "rsp_fold f")
    3.84 -  case False then show ?thesis by simp
    3.85 -next
    3.86 -  case True
    3.87 -  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"
    3.88 -    by (rule rsp_foldE)
    3.89 -  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
    3.90 -    by (simp add: set_eq_iff_multiset_of_remdups_eq)
    3.91 -  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
    3.92 -    by (rule fold_multiset_equiv)
    3.93 -  with True show ?thesis by (simp add: fold_once_fold_remdups)
    3.94 -qed
    3.95 -
    3.96 -lemma fold_once_rsp [quot_respect]:
    3.97 -  shows "(op = ===> op \<approx> ===> op =) fold_once fold_once"
    3.98 -  unfolding fun_rel_def by (auto intro: fold_once_set_equiv) 
    3.99 -
   3.100 -lemma concat_rsp_pre:
   3.101 -  assumes a: "list_all2 op \<approx> x x'"
   3.102 -  and     b: "x' \<approx> y'"
   3.103 -  and     c: "list_all2 op \<approx> y' y"
   3.104 -  and     d: "\<exists>x\<in>set x. xa \<in> set x"
   3.105 -  shows "\<exists>x\<in>set y. xa \<in> set x"
   3.106 -proof -
   3.107 -  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
   3.108 -  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
   3.109 -  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
   3.110 -  have "ya \<in> set y'" using b h by simp
   3.111 -  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
   3.112 -  then show ?thesis using f i by auto
   3.113 -qed
   3.114 -
   3.115 -lemma concat_rsp [quot_respect]:
   3.116 -  shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
   3.117 -proof (rule fun_relI, elim pred_compE)
   3.118 -  fix a b ba bb
   3.119 -  assume a: "list_all2 op \<approx> a ba"
   3.120 -  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
   3.121 -  assume b: "ba \<approx> bb"
   3.122 -  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
   3.123 -  assume c: "list_all2 op \<approx> bb b"
   3.124 -  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
   3.125 -  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
   3.126 -  proof
   3.127 -    fix x
   3.128 -    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
   3.129 -    proof
   3.130 -      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
   3.131 -      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
   3.132 -    next
   3.133 -      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
   3.134 -      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
   3.135 -    qed
   3.136 -  qed
   3.137 -  then show "concat a \<approx> concat b" by auto
   3.138 -qed
   3.139 -
   3.140 -
   3.141  section {* Quotient definitions for fsets *}
   3.142  
   3.143  
   3.144 @@ -323,7 +189,7 @@
   3.145  
   3.146  quotient_definition
   3.147    "bot :: 'a fset" 
   3.148 -  is "Nil :: 'a list"
   3.149 +  is "Nil :: 'a list" done
   3.150  
   3.151  abbreviation
   3.152    empty_fset  ("{||}")
   3.153 @@ -332,7 +198,7 @@
   3.154  
   3.155  quotient_definition
   3.156    "less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
   3.157 -  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
   3.158 +  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" by simp
   3.159  
   3.160  abbreviation
   3.161    subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
   3.162 @@ -351,7 +217,7 @@
   3.163  
   3.164  quotient_definition
   3.165    "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   3.166 -  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   3.167 +  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp
   3.168  
   3.169  abbreviation
   3.170    union_fset (infixl "|\<union>|" 65)
   3.171 @@ -360,7 +226,7 @@
   3.172  
   3.173  quotient_definition
   3.174    "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   3.175 -  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   3.176 +  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp
   3.177  
   3.178  abbreviation
   3.179    inter_fset (infixl "|\<inter>|" 65)
   3.180 @@ -369,7 +235,7 @@
   3.181  
   3.182  quotient_definition
   3.183    "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   3.184 -  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   3.185 +  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by fastforce
   3.186  
   3.187  instance
   3.188  proof
   3.189 @@ -413,7 +279,7 @@
   3.190  
   3.191  quotient_definition
   3.192    "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   3.193 -  is "Cons"
   3.194 +  is "Cons" by auto
   3.195  
   3.196  syntax
   3.197    "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
   3.198 @@ -425,7 +291,7 @@
   3.199  quotient_definition
   3.200    fset_member
   3.201  where
   3.202 -  "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member"
   3.203 +  "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" by fastforce
   3.204  
   3.205  abbreviation
   3.206    in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50)
   3.207 @@ -442,31 +308,84 @@
   3.208  
   3.209  quotient_definition
   3.210    "card_fset :: 'a fset \<Rightarrow> nat"
   3.211 -  is card_list
   3.212 +  is card_list by simp
   3.213  
   3.214  quotient_definition
   3.215    "map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
   3.216 -  is map
   3.217 +  is map by simp
   3.218  
   3.219  quotient_definition
   3.220    "remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   3.221 -  is removeAll
   3.222 +  is removeAll by simp
   3.223  
   3.224  quotient_definition
   3.225    "fset :: 'a fset \<Rightarrow> 'a set"
   3.226 -  is "set"
   3.227 +  is "set" by simp
   3.228 +
   3.229 +lemma fold_once_set_equiv:
   3.230 +  assumes "xs \<approx> ys"
   3.231 +  shows "fold_once f xs = fold_once f ys"
   3.232 +proof (cases "rsp_fold f")
   3.233 +  case False then show ?thesis by simp
   3.234 +next
   3.235 +  case True
   3.236 +  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"
   3.237 +    by (rule rsp_foldE)
   3.238 +  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
   3.239 +    by (simp add: set_eq_iff_multiset_of_remdups_eq)
   3.240 +  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
   3.241 +    by (rule fold_multiset_equiv)
   3.242 +  with True show ?thesis by (simp add: fold_once_fold_remdups)
   3.243 +qed
   3.244  
   3.245  quotient_definition
   3.246    "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
   3.247 -  is fold_once
   3.248 +  is fold_once by (rule fold_once_set_equiv)
   3.249 +
   3.250 +lemma concat_rsp_pre:
   3.251 +  assumes a: "list_all2 op \<approx> x x'"
   3.252 +  and     b: "x' \<approx> y'"
   3.253 +  and     c: "list_all2 op \<approx> y' y"
   3.254 +  and     d: "\<exists>x\<in>set x. xa \<in> set x"
   3.255 +  shows "\<exists>x\<in>set y. xa \<in> set x"
   3.256 +proof -
   3.257 +  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
   3.258 +  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
   3.259 +  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
   3.260 +  have "ya \<in> set y'" using b h by simp
   3.261 +  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
   3.262 +  then show ?thesis using f i by auto
   3.263 +qed
   3.264  
   3.265  quotient_definition
   3.266    "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
   3.267 -  is concat
   3.268 +  is concat 
   3.269 +proof (elim pred_compE)
   3.270 +fix a b ba bb
   3.271 +  assume a: "list_all2 op \<approx> a ba"
   3.272 +  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
   3.273 +  assume b: "ba \<approx> bb"
   3.274 +  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
   3.275 +  assume c: "list_all2 op \<approx> bb b"
   3.276 +  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
   3.277 +  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
   3.278 +  proof
   3.279 +    fix x
   3.280 +    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
   3.281 +    proof
   3.282 +      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
   3.283 +      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
   3.284 +    next
   3.285 +      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
   3.286 +      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
   3.287 +    qed
   3.288 +  qed
   3.289 +  then show "concat a \<approx> concat b" by auto
   3.290 +qed
   3.291  
   3.292  quotient_definition
   3.293    "filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   3.294 -  is filter
   3.295 +  is filter by force
   3.296  
   3.297  
   3.298  subsection {* Compositional respectfulness and preservation lemmas *}
   3.299 @@ -538,7 +457,7 @@
   3.300  
   3.301  lemma append_rsp2 [quot_respect]:
   3.302    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
   3.303 -  by (intro compositional_rsp3 append_rsp)
   3.304 +  by (intro compositional_rsp3)
   3.305       (auto intro!: fun_relI simp add: append_rsp2_pre)
   3.306  
   3.307  lemma map_rsp2 [quot_respect]:
   3.308 @@ -967,6 +886,20 @@
   3.309    (if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)"
   3.310    by descending (simp add: fold_once_fold_remdups)
   3.311  
   3.312 +lemma remdups_removeAll:
   3.313 +  "remdups (removeAll x xs) = remove1 x (remdups xs)"
   3.314 +  by (induct xs) auto
   3.315 +
   3.316 +lemma member_commute_fold_once:
   3.317 +  assumes "rsp_fold f"
   3.318 +    and "x \<in> set xs"
   3.319 +  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
   3.320 +proof -
   3.321 +  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
   3.322 +    by (auto intro!: fold_remove1_split elim: rsp_foldE)
   3.323 +  then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
   3.324 +qed
   3.325 +
   3.326  lemma in_commute_fold_fset:
   3.327    "rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h"
   3.328    by descending (simp add: member_commute_fold_once)
   3.329 @@ -1170,7 +1103,7 @@
   3.330        then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b 
   3.331          by auto
   3.332        have f: "card_list (removeAll a l) = m" using e d by (simp)
   3.333 -      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
   3.334 +      have g: "removeAll a l \<approx> removeAll a r" using remove_fset_rsp b by simp
   3.335        have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
   3.336        then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
   3.337        have i: "l \<approx>2 (a # removeAll a l)"
     4.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:03:58 2012 +0100
     4.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:17:29 2012 +0100
     4.3 @@ -23,17 +23,17 @@
     4.4    by (simp add: identity_equivp)
     4.5  
     4.6  quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"  is
     4.7 -  "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
     4.8 +  "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" done
     4.9  
    4.10  quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is 
    4.11 -  fcomp
    4.12 +  fcomp done
    4.13  
    4.14  quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd" 
    4.15 -  is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
    4.16 +  is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" done
    4.17  
    4.18 -quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on
    4.19 +quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on done
    4.20  
    4.21 -quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw
    4.22 +quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw done
    4.23  
    4.24  
    4.25  subsection {* Co/Contravariant type variables *} 
    4.26 @@ -47,7 +47,7 @@
    4.27    where "map_endofun' f g e = map_fun g f e"
    4.28  
    4.29  quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is
    4.30 -  map_endofun'
    4.31 +  map_endofun' done
    4.32  
    4.33  text {* Registration of the map function for 'a endofun. *}
    4.34  
    4.35 @@ -63,7 +63,7 @@
    4.36      by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
    4.37  qed
    4.38  
    4.39 -quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
    4.40 +quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
    4.41  
    4.42  term  endofun_id_id
    4.43  thm  endofun_id_id_def
    4.44 @@ -73,7 +73,7 @@
    4.45  text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting)
    4.46    over a type variable which is a covariant and contravariant type variable. *}
    4.47  
    4.48 -quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id
    4.49 +quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done
    4.50  
    4.51  term  endofun'_id_id
    4.52  thm  endofun'_id_id_def
     5.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:03:58 2012 +0100
     5.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:17:29 2012 +0100
     5.3 @@ -18,7 +18,7 @@
     5.4  local_setup {* fn lthy =>
     5.5  let
     5.6    val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"},
     5.7 -    equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
     5.8 +    equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
     5.9    val qty_full_name = @{type_name "rbt"}
    5.10  
    5.11    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    5.12 @@ -50,6 +50,7 @@
    5.13  subsection {* Primitive operations *}
    5.14  
    5.15  quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
    5.16 +done
    5.17  
    5.18  declare lookup_def[unfolded map_fun_def comp_def id_def, code]
    5.19  
    5.20 @@ -67,21 +68,21 @@
    5.21  *)
    5.22  
    5.23  quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
    5.24 -is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)"
    5.25 +is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
    5.26  
    5.27  lemma impl_of_empty [code abstract]:
    5.28    "impl_of empty = RBT_Impl.Empty"
    5.29    by (simp add: empty_def RBT_inverse)
    5.30  
    5.31  quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    5.32 -is "RBT_Impl.insert"
    5.33 +is "RBT_Impl.insert" done
    5.34  
    5.35  lemma impl_of_insert [code abstract]:
    5.36    "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
    5.37    by (simp add: insert_def RBT_inverse)
    5.38  
    5.39  quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    5.40 -is "RBT_Impl.delete"
    5.41 +is "RBT_Impl.delete" done
    5.42  
    5.43  lemma impl_of_delete [code abstract]:
    5.44    "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
    5.45 @@ -89,24 +90,24 @@
    5.46  
    5.47  (* FIXME: unnecessary type annotations *)
    5.48  quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    5.49 -is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list"
    5.50 +is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
    5.51  
    5.52  lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
    5.53  unfolding entries_def map_fun_def comp_def id_def ..
    5.54  
    5.55  (* FIXME: unnecessary type annotations *)
    5.56  quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
    5.57 -is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list"
    5.58 +is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
    5.59  
    5.60  quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
    5.61 -is "RBT_Impl.bulkload"
    5.62 +is "RBT_Impl.bulkload" done
    5.63  
    5.64  lemma impl_of_bulkload [code abstract]:
    5.65    "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
    5.66    by (simp add: bulkload_def RBT_inverse)
    5.67  
    5.68  quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    5.69 -is "RBT_Impl.map_entry"
    5.70 +is "RBT_Impl.map_entry" done
    5.71  
    5.72  lemma impl_of_map_entry [code abstract]:
    5.73    "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
    5.74 @@ -115,13 +116,15 @@
    5.75  (* FIXME: unnecesary type annotations *)
    5.76  quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    5.77  is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
    5.78 +done
    5.79  
    5.80  lemma impl_of_map [code abstract]:
    5.81    "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
    5.82    by (simp add: map_def RBT_inverse)
    5.83  
    5.84  (* FIXME: unnecessary type annotations *)
    5.85 -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"
    5.86 +quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
    5.87 +is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
    5.88  
    5.89  lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
    5.90  unfolding fold_def map_fun_def comp_def id_def ..
     6.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:03:58 2012 +0100
     6.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:17:29 2012 +0100
     6.3 @@ -20,7 +20,7 @@
     6.4    let
     6.5      val quotients =
     6.6        {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
     6.7 -        equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
     6.8 +        equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
     6.9      val qty_full_name = @{type_name "set"}
    6.10  
    6.11      fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    6.12 @@ -37,7 +37,7 @@
    6.13  text {* Now, we can employ quotient_definition to lift definitions. *}
    6.14  
    6.15  quotient_definition empty where "empty :: 'a set"
    6.16 -is "bot :: 'a \<Rightarrow> bool"
    6.17 +is "bot :: 'a \<Rightarrow> bool" done
    6.18  
    6.19  term "Lift_Set.empty"
    6.20  thm Lift_Set.empty_def
    6.21 @@ -46,7 +46,7 @@
    6.22    "insertp x P y \<longleftrightarrow> y = x \<or> P y"
    6.23  
    6.24  quotient_definition insert where "insert :: 'a => 'a set => 'a set"
    6.25 -is insertp
    6.26 +is insertp done
    6.27  
    6.28  term "Lift_Set.insert"
    6.29  thm Lift_Set.insert_def
     7.1 --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy	Fri Mar 23 14:03:58 2012 +0100
     7.2 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy	Fri Mar 23 14:17:29 2012 +0100
     7.3 @@ -21,75 +21,50 @@
     7.4  
     7.5  subsection {* Operations *}
     7.6  
     7.7 -lemma [quot_respect]:
     7.8 -  "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
     7.9 -  "(op = ===> set_eq) Collect Collect"
    7.10 -  "(set_eq ===> op =) Set.is_empty Set.is_empty"
    7.11 -  "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
    7.12 -  "(op = ===> set_eq ===> set_eq) Set.remove Set.remove"
    7.13 -  "(op = ===> set_eq ===> set_eq) image image"
    7.14 -  "(op = ===> set_eq ===> set_eq) Set.project Set.project"
    7.15 -  "(set_eq ===> op =) Ball Ball"
    7.16 -  "(set_eq ===> op =) Bex Bex"
    7.17 -  "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
    7.18 -  "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
    7.19 -  "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
    7.20 -  "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
    7.21 -  "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
    7.22 -  "set_eq {} {}"
    7.23 -  "set_eq UNIV UNIV"
    7.24 -  "(set_eq ===> set_eq) uminus uminus"
    7.25 -  "(set_eq ===> set_eq ===> set_eq) minus minus"
    7.26 -  "(set_eq ===> op =) Inf Inf"
    7.27 -  "(set_eq ===> op =) Sup Sup"
    7.28 -  "(op = ===> set_eq) List.set List.set"
    7.29 -  "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
    7.30 -by (auto simp: fun_rel_eq)
    7.31 -
    7.32  quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
    7.33 -is "op \<in>"
    7.34 +is "op \<in>" by simp
    7.35  quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
    7.36 -is Collect
    7.37 +is Collect done
    7.38  quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
    7.39 -is Set.is_empty
    7.40 +is Set.is_empty by simp 
    7.41  quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.42 -is Set.insert
    7.43 +is Set.insert by simp
    7.44  quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.45 -is Set.remove
    7.46 +is Set.remove by simp
    7.47  quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
    7.48 -is image
    7.49 +is image by simp
    7.50  quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.51 -is Set.project
    7.52 +is Set.project by simp
    7.53  quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    7.54 -is Ball
    7.55 +is Ball by simp
    7.56  quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    7.57 -is Bex
    7.58 +is Bex by simp
    7.59  quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
    7.60 -is Finite_Set.card
    7.61 +is Finite_Set.card by simp
    7.62  quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
    7.63 -is List.set
    7.64 +is List.set done
    7.65  quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
    7.66 -is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    7.67 +is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
    7.68  quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
    7.69 -is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    7.70 +is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
    7.71  quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.72 -is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    7.73 +is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
    7.74  quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.75 -is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    7.76 +is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
    7.77  quotient_definition empty where "empty :: 'a Quotient_Cset.set"
    7.78 -is "{} :: 'a set"
    7.79 +is "{} :: 'a set" done
    7.80  quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
    7.81 -is "Set.UNIV :: 'a set"
    7.82 +is "Set.UNIV :: 'a set" done
    7.83  quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.84 -is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
    7.85 +is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" by simp
    7.86  quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    7.87 -is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    7.88 +is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
    7.89  quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
    7.90 -is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
    7.91 +is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" by simp
    7.92  quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
    7.93 -is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
    7.94 +is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" by simp
    7.95  quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
    7.96 -is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    7.97 +is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" by simp
    7.98  
    7.99  hide_const (open) is_empty insert remove map filter forall exists card
   7.100    set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
     8.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Mar 23 14:03:58 2012 +0100
     8.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Mar 23 14:17:29 2012 +0100
     8.3 @@ -22,10 +22,10 @@
     8.4  begin
     8.5  
     8.6  quotient_definition
     8.7 -  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
     8.8 +  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" done
     8.9  
    8.10  quotient_definition
    8.11 -  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
    8.12 +  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" done
    8.13  
    8.14  fun
    8.15    plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    8.16 @@ -33,7 +33,7 @@
    8.17    "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
    8.18  
    8.19  quotient_definition
    8.20 -  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
    8.21 +  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
    8.22  
    8.23  fun
    8.24    uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    8.25 @@ -41,7 +41,7 @@
    8.26    "uminus_int_raw (x, y) = (y, x)"
    8.27  
    8.28  quotient_definition
    8.29 -  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
    8.30 +  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw" by auto
    8.31  
    8.32  definition
    8.33    minus_int_def:  "z - w = z + (-w\<Colon>int)"
    8.34 @@ -51,8 +51,38 @@
    8.35  where
    8.36    "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
    8.37  
    8.38 +lemma times_int_raw_fst:
    8.39 +  assumes a: "x \<approx> z"
    8.40 +  shows "times_int_raw x y \<approx> times_int_raw z y"
    8.41 +  using a
    8.42 +  apply(cases x, cases y, cases z)
    8.43 +  apply(auto simp add: times_int_raw.simps intrel.simps)
    8.44 +  apply(rename_tac u v w x y z)
    8.45 +  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
    8.46 +  apply(simp add: mult_ac)
    8.47 +  apply(simp add: add_mult_distrib [symmetric])
    8.48 +done
    8.49 +
    8.50 +lemma times_int_raw_snd:
    8.51 +  assumes a: "x \<approx> z"
    8.52 +  shows "times_int_raw y x \<approx> times_int_raw y z"
    8.53 +  using a
    8.54 +  apply(cases x, cases y, cases z)
    8.55 +  apply(auto simp add: times_int_raw.simps intrel.simps)
    8.56 +  apply(rename_tac u v w x y z)
    8.57 +  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
    8.58 +  apply(simp add: mult_ac)
    8.59 +  apply(simp add: add_mult_distrib [symmetric])
    8.60 +done
    8.61 +
    8.62  quotient_definition
    8.63    "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
    8.64 +  apply(rule equivp_transp[OF int_equivp])
    8.65 +  apply(rule times_int_raw_fst)
    8.66 +  apply(assumption)
    8.67 +  apply(rule times_int_raw_snd)
    8.68 +  apply(assumption)
    8.69 +done
    8.70  
    8.71  fun
    8.72    le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
    8.73 @@ -60,7 +90,7 @@
    8.74    "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
    8.75  
    8.76  quotient_definition
    8.77 -  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
    8.78 +  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
    8.79  
    8.80  definition
    8.81    less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
    8.82 @@ -75,47 +105,6 @@
    8.83  
    8.84  end
    8.85  
    8.86 -lemma [quot_respect]:
    8.87 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
    8.88 -  and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
    8.89 -  and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
    8.90 -  by (auto intro!: fun_relI)
    8.91 -
    8.92 -lemma times_int_raw_fst:
    8.93 -  assumes a: "x \<approx> z"
    8.94 -  shows "times_int_raw x y \<approx> times_int_raw z y"
    8.95 -  using a
    8.96 -  apply(cases x, cases y, cases z)
    8.97 -  apply(auto simp add: times_int_raw.simps intrel.simps)
    8.98 -  apply(rename_tac u v w x y z)
    8.99 -  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
   8.100 -  apply(simp add: mult_ac)
   8.101 -  apply(simp add: add_mult_distrib [symmetric])
   8.102 -  done
   8.103 -
   8.104 -lemma times_int_raw_snd:
   8.105 -  assumes a: "x \<approx> z"
   8.106 -  shows "times_int_raw y x \<approx> times_int_raw y z"
   8.107 -  using a
   8.108 -  apply(cases x, cases y, cases z)
   8.109 -  apply(auto simp add: times_int_raw.simps intrel.simps)
   8.110 -  apply(rename_tac u v w x y z)
   8.111 -  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
   8.112 -  apply(simp add: mult_ac)
   8.113 -  apply(simp add: add_mult_distrib [symmetric])
   8.114 -  done
   8.115 -
   8.116 -lemma [quot_respect]:
   8.117 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
   8.118 -  apply(simp only: fun_rel_def)
   8.119 -  apply(rule allI | rule impI)+
   8.120 -  apply(rule equivp_transp[OF int_equivp])
   8.121 -  apply(rule times_int_raw_fst)
   8.122 -  apply(assumption)
   8.123 -  apply(rule times_int_raw_snd)
   8.124 -  apply(assumption)
   8.125 -  done
   8.126 -
   8.127  
   8.128  text{* The integers form a @{text comm_ring_1}*}
   8.129  
   8.130 @@ -165,11 +154,7 @@
   8.131    "int_of_nat_raw m = (m :: nat, 0 :: nat)"
   8.132  
   8.133  quotient_definition
   8.134 -  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
   8.135 -
   8.136 -lemma[quot_respect]:
   8.137 -  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
   8.138 -  by (auto simp add: equivp_reflp [OF int_equivp])
   8.139 +  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" done
   8.140  
   8.141  lemma int_of_nat:
   8.142    shows "of_nat m = int_of_nat m"
   8.143 @@ -304,11 +289,7 @@
   8.144  quotient_definition
   8.145    "int_to_nat::int \<Rightarrow> nat"
   8.146  is
   8.147 -  "int_to_nat_raw"
   8.148 -
   8.149 -lemma [quot_respect]:
   8.150 -  shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
   8.151 -  by (auto iff: int_to_nat_raw_def)
   8.152 +  "int_to_nat_raw" unfolding int_to_nat_raw_def by force
   8.153  
   8.154  lemma nat_le_eq_zle:
   8.155    fixes w z::"int"
     9.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Mar 23 14:03:58 2012 +0100
     9.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Mar 23 14:17:29 2012 +0100
     9.3 @@ -136,29 +136,25 @@
     9.4    "Nonce :: nat \<Rightarrow> msg"
     9.5  is
     9.6    "NONCE"
     9.7 +done
     9.8  
     9.9  quotient_definition
    9.10    "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
    9.11  is
    9.12    "MPAIR"
    9.13 +by (rule MPAIR)
    9.14  
    9.15  quotient_definition
    9.16    "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
    9.17  is
    9.18    "CRYPT"
    9.19 +by (rule CRYPT)
    9.20  
    9.21  quotient_definition
    9.22    "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
    9.23  is
    9.24    "DECRYPT"
    9.25 -
    9.26 -lemma [quot_respect]:
    9.27 -  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
    9.28 -by (auto intro: CRYPT)
    9.29 -
    9.30 -lemma [quot_respect]:
    9.31 -  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
    9.32 -by (auto intro: DECRYPT)
    9.33 +by (rule DECRYPT)
    9.34  
    9.35  text{*Establishing these two equations is the point of the whole exercise*}
    9.36  theorem CD_eq [simp]:
    9.37 @@ -175,25 +171,14 @@
    9.38     "nonces:: msg \<Rightarrow> nat set"
    9.39  is
    9.40    "freenonces"
    9.41 +by (rule msgrel_imp_eq_freenonces)
    9.42  
    9.43  text{*Now prove the four equations for @{term nonces}*}
    9.44  
    9.45 -lemma [quot_respect]:
    9.46 -  shows "(op \<sim> ===> op =) freenonces freenonces"
    9.47 -  by (auto simp add: msgrel_imp_eq_freenonces)
    9.48 -
    9.49 -lemma [quot_respect]:
    9.50 -  shows "(op = ===> op \<sim>) NONCE NONCE"
    9.51 -  by (auto simp add: NONCE)
    9.52 -
    9.53  lemma nonces_Nonce [simp]:
    9.54    shows "nonces (Nonce N) = {N}"
    9.55    by (lifting freenonces.simps(1))
    9.56  
    9.57 -lemma [quot_respect]:
    9.58 -  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
    9.59 -  by (auto simp add: MPAIR)
    9.60 -
    9.61  lemma nonces_MPair [simp]:
    9.62    shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
    9.63    by (lifting freenonces.simps(2))
    9.64 @@ -212,10 +197,7 @@
    9.65    "left:: msg \<Rightarrow> msg"
    9.66  is
    9.67    "freeleft"
    9.68 -
    9.69 -lemma [quot_respect]:
    9.70 -  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
    9.71 -  by (auto simp add: msgrel_imp_eqv_freeleft)
    9.72 +by (rule msgrel_imp_eqv_freeleft)
    9.73  
    9.74  lemma left_Nonce [simp]:
    9.75    shows "left (Nonce N) = Nonce N"
    9.76 @@ -239,13 +221,10 @@
    9.77    "right:: msg \<Rightarrow> msg"
    9.78  is
    9.79    "freeright"
    9.80 +by (rule msgrel_imp_eqv_freeright)
    9.81  
    9.82  text{*Now prove the four equations for @{term right}*}
    9.83  
    9.84 -lemma [quot_respect]:
    9.85 -  shows "(op \<sim> ===> op \<sim>) freeright freeright"
    9.86 -  by (auto simp add: msgrel_imp_eqv_freeright)
    9.87 -
    9.88  lemma right_Nonce [simp]:
    9.89    shows "right (Nonce N) = Nonce N"
    9.90    by (lifting freeright.simps(1))
    9.91 @@ -352,13 +331,10 @@
    9.92    "discrim:: msg \<Rightarrow> int"
    9.93  is
    9.94    "freediscrim"
    9.95 +by (rule msgrel_imp_eq_freediscrim)
    9.96  
    9.97  text{*Now prove the four equations for @{term discrim}*}
    9.98  
    9.99 -lemma [quot_respect]:
   9.100 -  shows "(op \<sim> ===> op =) freediscrim freediscrim"
   9.101 -  by (auto simp add: msgrel_imp_eq_freediscrim)
   9.102 -
   9.103  lemma discrim_Nonce [simp]:
   9.104    shows "discrim (Nonce N) = 0"
   9.105    by (lifting freediscrim.simps(1))
    10.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Mar 23 14:03:58 2012 +0100
    10.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Mar 23 14:17:29 2012 +0100
    10.3 @@ -32,28 +32,29 @@
    10.4  begin
    10.5  
    10.6  quotient_definition
    10.7 -  "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)"
    10.8 +  "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)" by simp
    10.9  
   10.10  quotient_definition
   10.11 -  "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)"
   10.12 +  "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)" by simp
   10.13  
   10.14  fun times_rat_raw where
   10.15    "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
   10.16  
   10.17  quotient_definition
   10.18 -  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw
   10.19 +  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult_assoc mult_left_commute)
   10.20  
   10.21  fun plus_rat_raw where
   10.22    "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
   10.23  
   10.24  quotient_definition
   10.25 -  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw
   10.26 +  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw 
   10.27 +  by (auto simp add: mult_commute mult_left_commute int_distrib(2))
   10.28  
   10.29  fun uminus_rat_raw where
   10.30    "uminus_rat_raw (a :: int, b :: int) = (-a, b)"
   10.31  
   10.32  quotient_definition
   10.33 -  "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw"
   10.34 +  "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw" by fastforce
   10.35  
   10.36  definition
   10.37    minus_rat_def: "a - b = a + (-b\<Colon>rat)"
   10.38 @@ -63,6 +64,32 @@
   10.39  
   10.40  quotient_definition
   10.41    "(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw"
   10.42 +proof -
   10.43 +  {
   10.44 +    fix a b c d e f g h :: int
   10.45 +    assume "a * f * (b * f) \<le> e * b * (b * f)"
   10.46 +    then have le: "a * f * b * f \<le> e * b * b * f" by simp
   10.47 +    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
   10.48 +    then have b2: "b * b > 0"
   10.49 +      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
   10.50 +    have f2: "f * f > 0" using nz(3)
   10.51 +      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
   10.52 +    assume eq: "a * d = c * b" "e * h = g * f"
   10.53 +    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
   10.54 +      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
   10.55 +    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
   10.56 +      by (metis (no_types) mult_assoc mult_commute)
   10.57 +    then have "c * f * f * d \<le> e * f * d * d" using b2
   10.58 +      by (metis leD linorder_le_less_linear mult_strict_right_mono)
   10.59 +    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
   10.60 +      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
   10.61 +    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
   10.62 +      by (metis (no_types) mult_assoc mult_commute)
   10.63 +    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
   10.64 +      by (metis leD linorder_le_less_linear mult_strict_right_mono)
   10.65 +  }
   10.66 +  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
   10.67 +qed
   10.68  
   10.69  definition
   10.70    less_rat_def: "(z\<Colon>rat) < w = (z \<le> w \<and> z \<noteq> w)"
   10.71 @@ -83,14 +110,7 @@
   10.72  where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))"
   10.73  
   10.74  quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is
   10.75 -  Fract_raw
   10.76 -
   10.77 -lemma [quot_respect]:
   10.78 -  "(op \<approx> ===> op \<approx> ===> op \<approx>) times_rat_raw times_rat_raw"
   10.79 -  "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_rat_raw plus_rat_raw"
   10.80 -  "(op \<approx> ===> op \<approx>) uminus_rat_raw uminus_rat_raw"
   10.81 -  "(op = ===> op = ===> op \<approx>) Fract_raw Fract_raw"
   10.82 -  by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2))
   10.83 +  Fract_raw by simp
   10.84  
   10.85  lemmas [simp] = Respects_def
   10.86  
   10.87 @@ -156,15 +176,11 @@
   10.88    "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
   10.89  
   10.90  quotient_definition
   10.91 -  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw
   10.92 +  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw by (force simp add: mult_commute)
   10.93  
   10.94  definition
   10.95    divide_rat_def: "q / r = q * inverse (r::rat)"
   10.96  
   10.97 -lemma [quot_respect]:
   10.98 -  "(op \<approx> ===> op \<approx>) rat_inverse_raw rat_inverse_raw"
   10.99 -  by (auto intro!: fun_relI simp add: mult_commute)
  10.100 -
  10.101  instance proof
  10.102    fix q :: rat
  10.103    assume "q \<noteq> 0"
  10.104 @@ -179,34 +195,6 @@
  10.105  
  10.106  end
  10.107  
  10.108 -lemma [quot_respect]: "(op \<approx> ===> op \<approx> ===> op =) le_rat_raw le_rat_raw"
  10.109 -proof -
  10.110 -  {
  10.111 -    fix a b c d e f g h :: int
  10.112 -    assume "a * f * (b * f) \<le> e * b * (b * f)"
  10.113 -    then have le: "a * f * b * f \<le> e * b * b * f" by simp
  10.114 -    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
  10.115 -    then have b2: "b * b > 0"
  10.116 -      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
  10.117 -    have f2: "f * f > 0" using nz(3)
  10.118 -      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
  10.119 -    assume eq: "a * d = c * b" "e * h = g * f"
  10.120 -    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
  10.121 -      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
  10.122 -    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
  10.123 -      by (metis (no_types) mult_assoc mult_commute)
  10.124 -    then have "c * f * f * d \<le> e * f * d * d" using b2
  10.125 -      by (metis leD linorder_le_less_linear mult_strict_right_mono)
  10.126 -    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
  10.127 -      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
  10.128 -    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
  10.129 -      by (metis (no_types) mult_assoc mult_commute)
  10.130 -    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
  10.131 -      by (metis leD linorder_le_less_linear mult_strict_right_mono)
  10.132 -  }
  10.133 -  then show ?thesis by (auto intro!: fun_relI)
  10.134 -qed
  10.135 -
  10.136  instantiation rat :: linorder
  10.137  begin
  10.138