Theory Lift_Fun

theory Lift_Fun
imports Quotient_Syntax
(*  Title:      HOL/Quotient_Examples/Lift_Fun.thy
    Author:     Ondrej Kuncar

section {* Example of lifting definitions with contravariant or co/contravariant type variables *}

theory Lift_Fun
imports Main "~~/src/HOL/Library/Quotient_Syntax"

text {* This file is meant as a test case. 
  It contains examples of lifting definitions with quotients that have contravariant 
  type variables or type variables which are covariant and contravariant in the same time. *}

subsection {* Contravariant type variables *}

text {* 'a is a contravariant type variable and we are able to map over this variable
  in the following four definitions. This example is based on HOL/Fun.thy. *}

('a, 'b) fun' (infixr "→" 55) = "'a ⇒ 'b" / "op =" 
  by (simp add: identity_equivp)

quotient_definition "comp' :: ('b → 'c) → ('a → 'b) → 'a → 'c"  is
  "comp :: ('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c" done

quotient_definition "fcomp' :: ('a ⇒ 'b) ⇒ ('b ⇒ 'c) ⇒ 'a ⇒ 'c" is 
  fcomp done

quotient_definition "map_fun' :: ('c → 'a) → ('b → 'd) → ('a → 'b) → 'c → 'd" 
  is "map_fun::('c ⇒ 'a) ⇒ ('b ⇒ 'd) ⇒ ('a ⇒ 'b) ⇒ 'c ⇒ 'd" done

quotient_definition "inj_on' :: ('a → 'b) → 'a set → bool" is inj_on done

quotient_definition "bij_betw' :: ('a → 'b) → 'a set → 'b set → bool" is bij_betw done

subsection {* Co/Contravariant type variables *} 

text {* 'a is a covariant and contravariant type variable in the same time.
  The following example is a bit artificial. We haven't had a natural one yet. *}

quotient_type 'a endofun = "'a ⇒ 'a" / "op =" by (simp add: identity_equivp)

definition map_endofun' :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ ('a => 'a) ⇒ ('b => 'b)"
  where "map_endofun' f g e = map_fun g f e"

quotient_definition "map_endofun :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ 'a endofun ⇒ 'b endofun" is
  map_endofun' done

text {* Registration of the map function for 'a endofun. *}

functor map_endofun : map_endofun
proof -
  have "∀ x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
  then show "map_endofun id id = id" 
    by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff)
  have a:"∀ x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun 
    Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
  show "⋀f g h i. map_endofun f g ∘ map_endofun h i = map_endofun (f ∘ h) (i ∘ g)"
    by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 

text {* Relator for 'a endofun. *}

  rel_endofun' :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ ('b ⇒ 'b) ⇒ bool" 
  "rel_endofun' R = (λf g. (R ===> R) f g)"

quotient_definition "rel_endofun :: ('a ⇒ 'b ⇒ bool) ⇒ 'a endofun ⇒ 'b endofun ⇒ bool" is
  rel_endofun' done

lemma endofun_quotient:
assumes a: "Quotient3 R Abs Rep"
shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
proof (intro Quotient3I)
  show "⋀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 o_eq_dest_lhs)
  show "⋀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 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)
  have abs_to_eq: "⋀ x y. abs_endofun x = abs_endofun y ⟹ x = y" 
  by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun])
  fix r s
  show "rel_endofun R r s =
          (rel_endofun R r r ∧
           rel_endofun R s s ∧ 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]
    apply metis
    using fun_quotient3[OF a a, THEN Quotient3_rel]
    apply metis
    by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq)

declare [[mapQ3 endofun = (rel_endofun, endofun_quotient)]]

quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" done

term  endofun_id_id
thm  endofun_id_id_def

quotient_type 'a endofun' = "'a endofun" / "op =" by (simp add: identity_equivp)

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 done

term  endofun'_id_id
thm  endofun'_id_id_def