# HG changeset patch
# User blanchet
# Date 1394115143 -3600
# Node ID a6a380edbec5d0d63dcc09563345ea52b7c56a4e
# Parent  7339ef350739ab0b1196409217249d4d73d8784f
renamed 'endofun_rel' to 'rel_endofun'

diff -r 7339ef350739 -r a6a380edbec5 src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Thu Mar 06 15:10:56 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Thu Mar 06 15:12:23 2014 +0100
@@ -66,32 +66,32 @@
 text {* Relator for 'a endofun. *}
 
 definition
-  endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
+  rel_endofun' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
 where
-  "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)"
+  "rel_endofun' R = (\<lambda>f g. (R ===> R) f g)"
 
-quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
-  endofun_rel' done
+quotient_definition "rel_endofun :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
+  rel_endofun' done
 
 lemma endofun_quotient:
 assumes a: "Quotient3 R Abs Rep"
-shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
+shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
 proof (intro Quotient3I)
   show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
     by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
 next
-  show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
+  show "\<And>a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
   using fun_quotient3[OF a a, THEN Quotient3_rep_reflp]
-  unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
+  unfolding rel_endofun_def map_endofun_def map_fun_def o_def map_endofun'_def rel_endofun'_def id_def 
     by (metis (mono_tags) Quotient3_endofun rep_abs_rsp)
 next
   have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" 
   by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun])
   fix r s
-  show "endofun_rel R r s =
-          (endofun_rel R r r \<and>
-           endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
-    apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
+  show "rel_endofun R r s =
+          (rel_endofun R r r \<and>
+           rel_endofun R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
+    apply(auto simp add: rel_endofun_def rel_endofun'_def map_endofun_def map_endofun'_def)
     using fun_quotient3[OF a a,THEN Quotient3_refl1]
     apply metis
     using fun_quotient3[OF a a,THEN Quotient3_refl2]
@@ -101,7 +101,7 @@
     by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq)
 qed
 
-declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]]
+declare [[mapQ3 endofun = (rel_endofun, endofun_quotient)]]
 
 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done