Theory Lift_Fun

(*  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 "HOL-Library.Quotient_Syntax"
begin

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.›

quotient_type
('a, 'b) fun' (infixr "→" 55) = "'a ⇒ 'b" / "(=)" 
  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" / "(=)" 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 "(=)" 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) 
qed

text ‹Relator for 'a endofun.›

definition
  rel_endofun' :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ ('b ⇒ 'b) ⇒ bool" 
where
  "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 (opaque_lifting, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
next
  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)
next
  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)
qed

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" / "(=)" 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


end