1.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:25:31 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:26:09 2012 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  
     1.6  theory Lift_Fun
     1.7 -imports Main
     1.8 +imports Main "~~/src/HOL/Library/Quotient_Syntax"
     1.9  begin
    1.10  
    1.11  text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. 
    1.12 @@ -63,6 +63,44 @@
    1.13      by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
    1.14  qed
    1.15  
    1.16 +text {* Relator for 'a endofun. *}
    1.17 +
    1.18 +definition
    1.19 +  endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
    1.20 +where
    1.21 +  "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)"
    1.22 +
    1.23 +quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
    1.24 +  endofun_rel' done
    1.25 +
    1.26 +lemma endofun_quotient:
    1.27 +assumes a: "Quotient R Abs Rep"
    1.28 +shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
    1.29 +proof (intro QuotientI)
    1.30 +  show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
    1.31 +    by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
    1.32 +next
    1.33 +  show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
    1.34 +  using fun_quotient[OF a a, THEN Quotient_rep_reflp]
    1.35 +  unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
    1.36 +    by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
    1.37 +next
    1.38 +  show "\<And>r s. endofun_rel R r s =
    1.39 +          (endofun_rel R r r \<and>
    1.40 +           endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
    1.41 +    apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
    1.42 +    using fun_quotient[OF a a,THEN Quotient_refl1]
    1.43 +    apply metis
    1.44 +    using fun_quotient[OF a a,THEN Quotient_refl2]
    1.45 +    apply metis
    1.46 +    using fun_quotient[OF a a, THEN Quotient_rel]
    1.47 +    apply metis
    1.48 +    using fun_quotient[OF a a, THEN Quotient_rel]
    1.49 +    by (smt Quotient_endofun rep_abs_rsp)
    1.50 +qed
    1.51 +
    1.52 +declare [[map endofun = (endofun_rel, 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  
    1.56  term  endofun_id_id