renamed 'endofun_rel' to 'rel_endofun'
authorblanchet
Thu Mar 06 15:12:23 2014 +0100 (2014-03-06)
changeset 55941a6a380edbec5
parent 55940 7339ef350739
child 55942 c2d96043de4b
renamed 'endofun_rel' to 'rel_endofun'
src/HOL/Quotient_Examples/Lift_Fun.thy
     1.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Thu Mar 06 15:10:56 2014 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Thu Mar 06 15:12:23 2014 +0100
     1.3 @@ -66,32 +66,32 @@
     1.4  text {* Relator for 'a endofun. *}
     1.5  
     1.6  definition
     1.7 -  endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
     1.8 +  rel_endofun' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
     1.9  where
    1.10 -  "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)"
    1.11 +  "rel_endofun' R = (\<lambda>f g. (R ===> R) f g)"
    1.12  
    1.13 -quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
    1.14 -  endofun_rel' done
    1.15 +quotient_definition "rel_endofun :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
    1.16 +  rel_endofun' done
    1.17  
    1.18  lemma endofun_quotient:
    1.19  assumes a: "Quotient3 R Abs Rep"
    1.20 -shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
    1.21 +shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
    1.22  proof (intro Quotient3I)
    1.23    show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
    1.24      by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
    1.25  next
    1.26 -  show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
    1.27 +  show "\<And>a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
    1.28    using fun_quotient3[OF a a, THEN Quotient3_rep_reflp]
    1.29 -  unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
    1.30 +  unfolding rel_endofun_def map_endofun_def map_fun_def o_def map_endofun'_def rel_endofun'_def id_def 
    1.31      by (metis (mono_tags) Quotient3_endofun rep_abs_rsp)
    1.32  next
    1.33    have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" 
    1.34    by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun])
    1.35    fix r s
    1.36 -  show "endofun_rel R r s =
    1.37 -          (endofun_rel R r r \<and>
    1.38 -           endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
    1.39 -    apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
    1.40 +  show "rel_endofun R r s =
    1.41 +          (rel_endofun R r r \<and>
    1.42 +           rel_endofun R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
    1.43 +    apply(auto simp add: rel_endofun_def rel_endofun'_def map_endofun_def map_endofun'_def)
    1.44      using fun_quotient3[OF a a,THEN Quotient3_refl1]
    1.45      apply metis
    1.46      using fun_quotient3[OF a a,THEN Quotient3_refl2]
    1.47 @@ -101,7 +101,7 @@
    1.48      by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq)
    1.49  qed
    1.50  
    1.51 -declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]]
    1.52 +declare [[mapQ3 endofun = (rel_endofun, endofun_quotient)]]
    1.53  
    1.54  quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
    1.55