Theory Map_Functions

theory Map_Functions
imports Deflation
(*  Title:      HOL/HOLCF/Map_Functions.thy
Author: Brian Huffman
*)


header {* Map functions for various types *}

theory Map_Functions
imports Deflation
begin

subsection {* Map operator for continuous function space *}

default_sort cpo

definition
cfun_map :: "('b -> 'a) -> ('c -> 'd) -> ('a -> 'c) -> ('b -> 'd)"
where
"cfun_map = (Λ a b f x. b·(f·(a·x)))"

lemma cfun_map_beta [simp]: "cfun_map·a·b·f·x = b·(f·(a·x))"
unfolding cfun_map_def by simp

lemma cfun_map_ID: "cfun_map·ID·ID = ID"
unfolding cfun_eq_iff by simp

lemma cfun_map_map:
"cfun_map·f1·g1·(cfun_map·f2·g2·p) =
cfun_map·(Λ x. f2·(f1·x))·(Λ x. g1·(g2·x))·p"

by (rule cfun_eqI) simp

lemma ep_pair_cfun_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
shows "ep_pair (cfun_map·p1·e2) (cfun_map·e1·p2)"
proof
interpret e1p1: ep_pair e1 p1 by fact
interpret e2p2: ep_pair e2 p2 by fact
fix f show "cfun_map·e1·p2·(cfun_map·p1·e2·f) = f"
by (simp add: cfun_eq_iff)
fix g show "cfun_map·p1·e2·(cfun_map·e1·p2·g) \<sqsubseteq> g"
apply (rule cfun_belowI, simp)
apply (rule below_trans [OF e2p2.e_p_below])
apply (rule monofun_cfun_arg)
apply (rule e1p1.e_p_below)
done
qed

lemma deflation_cfun_map:
assumes "deflation d1" and "deflation d2"
shows "deflation (cfun_map·d1·d2)"
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix f
show "cfun_map·d1·d2·(cfun_map·d1·d2·f) = cfun_map·d1·d2·f"
by (simp add: cfun_eq_iff d1.idem d2.idem)
show "cfun_map·d1·d2·f \<sqsubseteq> f"
apply (rule cfun_belowI, simp)
apply (rule below_trans [OF d2.below])
apply (rule monofun_cfun_arg)
apply (rule d1.below)
done
qed

lemma finite_range_cfun_map:
assumes a: "finite (range (λx. a·x))"
assumes b: "finite (range (λy. b·y))"
shows "finite (range (λf. cfun_map·a·b·f))" (is "finite (range ?h)")
proof (rule finite_imageD)
let ?f = "λg. range (λx. (a·x, g·x))"
show "finite (?f ` range ?h)"
proof (rule finite_subset)
let ?B = "Pow (range (λx. a·x) × range (λy. b·y))"
show "?f ` range ?h ⊆ ?B"
by clarsimp
show "finite ?B"
by (simp add: a b)
qed
show "inj_on ?f (range ?h)"
proof (rule inj_onI, rule cfun_eqI, clarsimp)
fix x f g
assume "range (λx. (a·x, b·(f·(a·x)))) = range (λx. (a·x, b·(g·(a·x))))"
hence "range (λx. (a·x, b·(f·(a·x)))) ⊆ range (λx. (a·x, b·(g·(a·x))))"
by (rule equalityD1)
hence "(a·x, b·(f·(a·x))) ∈ range (λx. (a·x, b·(g·(a·x))))"
by (simp add: subset_eq)
then obtain y where "(a·x, b·(f·(a·x))) = (a·y, b·(g·(a·y)))"
by (rule rangeE)
thus "b·(f·(a·x)) = b·(g·(a·x))"
by clarsimp
qed
qed

lemma finite_deflation_cfun_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (cfun_map·d1·d2)"
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
thus "deflation (cfun_map·d1·d2)" by (rule deflation_cfun_map)
have "finite (range (λf. cfun_map·d1·d2·f))"
using d1.finite_range d2.finite_range
by (rule finite_range_cfun_map)
thus "finite {f. cfun_map·d1·d2·f = f}"
by (rule finite_range_imp_finite_fixes)
qed

text {* Finite deflations are compact elements of the function space *}

lemma finite_deflation_imp_compact: "finite_deflation d ==> compact d"
apply (frule finite_deflation_imp_deflation)
apply (subgoal_tac "compact (cfun_map·d·d·d)")
apply (simp add: cfun_map_def deflation.idem eta_cfun)
apply (rule finite_deflation.compact)
apply (simp only: finite_deflation_cfun_map)
done

subsection {* Map operator for product type *}

definition
prod_map :: "('a -> 'b) -> ('c -> 'd) -> 'a × 'c -> 'b × 'd"
where
"prod_map = (Λ f g p. (f·(fst p), g·(snd p)))"

lemma prod_map_Pair [simp]: "prod_map·f·g·(x, y) = (f·x, g·y)"
unfolding prod_map_def by simp

lemma prod_map_ID: "prod_map·ID·ID = ID"
unfolding cfun_eq_iff by auto

lemma prod_map_map:
"prod_map·f1·g1·(prod_map·f2·g2·p) =
prod_map·(Λ x. f1·(f2·x))·(Λ x. g1·(g2·x))·p"

by (induct p) simp

lemma ep_pair_prod_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
shows "ep_pair (prod_map·e1·e2) (prod_map·p1·p2)"
proof
interpret e1p1: ep_pair e1 p1 by fact
interpret e2p2: ep_pair e2 p2 by fact
fix x show "prod_map·p1·p2·(prod_map·e1·e2·x) = x"
by (induct x) simp
fix y show "prod_map·e1·e2·(prod_map·p1·p2·y) \<sqsubseteq> y"
by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
qed

lemma deflation_prod_map:
assumes "deflation d1" and "deflation d2"
shows "deflation (prod_map·d1·d2)"
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix x
show "prod_map·d1·d2·(prod_map·d1·d2·x) = prod_map·d1·d2·x"
by (induct x) (simp add: d1.idem d2.idem)
show "prod_map·d1·d2·x \<sqsubseteq> x"
by (induct x) (simp add: d1.below d2.below)
qed

lemma finite_deflation_prod_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (prod_map·d1·d2)"
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
thus "deflation (prod_map·d1·d2)" by (rule deflation_prod_map)
have "{p. prod_map·d1·d2·p = p} ⊆ {x. d1·x = x} × {y. d2·y = y}"
by clarsimp
thus "finite {p. prod_map·d1·d2·p = p}"
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed

subsection {* Map function for lifted cpo *}

definition
u_map :: "('a -> 'b) -> 'a u -> 'b u"
where
"u_map = (Λ f. fup·(up oo f))"

lemma u_map_strict [simp]: "u_map·f·⊥ = ⊥"
unfolding u_map_def by simp

lemma u_map_up [simp]: "u_map·f·(up·x) = up·(f·x)"
unfolding u_map_def by simp

lemma u_map_ID: "u_map·ID = ID"
unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)

lemma u_map_map: "u_map·f·(u_map·g·p) = u_map·(Λ x. f·(g·x))·p"
by (induct p) simp_all

lemma u_map_oo: "u_map·(f oo g) = u_map·f oo u_map·g"
by (simp add: cfcomp1 u_map_map eta_cfun)

lemma ep_pair_u_map: "ep_pair e p ==> ep_pair (u_map·e) (u_map·p)"
apply default
apply (case_tac x, simp, simp add: ep_pair.e_inverse)
apply (case_tac y, simp, simp add: ep_pair.e_p_below)
done

lemma deflation_u_map: "deflation d ==> deflation (u_map·d)"
apply default
apply (case_tac x, simp, simp add: deflation.idem)
apply (case_tac x, simp, simp add: deflation.below)
done

lemma finite_deflation_u_map:
assumes "finite_deflation d" shows "finite_deflation (u_map·d)"
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
have "deflation d" by fact
thus "deflation (u_map·d)" by (rule deflation_u_map)
have "{x. u_map·d·x = x} ⊆ insert ⊥ ((λx. up·x) ` {x. d·x = x})"
by (rule subsetI, case_tac x, simp_all)
thus "finite {x. u_map·d·x = x}"
by (rule finite_subset, simp add: d.finite_fixes)
qed

subsection {* Map function for strict products *}

default_sort pcpo

definition
sprod_map :: "('a -> 'b) -> ('c -> 'd) -> 'a ⊗ 'c -> 'b ⊗ 'd"
where
"sprod_map = (Λ f g. ssplit·(Λ x y. (:f·x, g·y:)))"

lemma sprod_map_strict [simp]: "sprod_map·a·b·⊥ = ⊥"
unfolding sprod_map_def by simp

lemma sprod_map_spair [simp]:
"x ≠ ⊥ ==> y ≠ ⊥ ==> sprod_map·f·g·(:x, y:) = (:f·x, g·y:)"
by (simp add: sprod_map_def)

lemma sprod_map_spair':
"f·⊥ = ⊥ ==> g·⊥ = ⊥ ==> sprod_map·f·g·(:x, y:) = (:f·x, g·y:)"
by (cases "x = ⊥ ∨ y = ⊥") auto

lemma sprod_map_ID: "sprod_map·ID·ID = ID"
unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)

lemma sprod_map_map:
"[|f1·⊥ = ⊥; g1·⊥ = ⊥|] ==>
sprod_map·f1·g1·(sprod_map·f2·g2·p) =
sprod_map·(Λ x. f1·(f2·x))·(Λ x. g1·(g2·x))·p"

apply (induct p, simp)
apply (case_tac "f2·x = ⊥", simp)
apply (case_tac "g2·y = ⊥", simp)
apply simp
done

lemma ep_pair_sprod_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
shows "ep_pair (sprod_map·e1·e2) (sprod_map·p1·p2)"
proof
interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
fix x show "sprod_map·p1·p2·(sprod_map·e1·e2·x) = x"
by (induct x) simp_all
fix y show "sprod_map·e1·e2·(sprod_map·p1·p2·y) \<sqsubseteq> y"
apply (induct y, simp)
apply (case_tac "p1·x = ⊥", simp, case_tac "p2·y = ⊥", simp)
apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
done
qed

lemma deflation_sprod_map:
assumes "deflation d1" and "deflation d2"
shows "deflation (sprod_map·d1·d2)"
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix x
show "sprod_map·d1·d2·(sprod_map·d1·d2·x) = sprod_map·d1·d2·x"
apply (induct x, simp)
apply (case_tac "d1·x = ⊥", simp, case_tac "d2·y = ⊥", simp)
apply (simp add: d1.idem d2.idem)
done
show "sprod_map·d1·d2·x \<sqsubseteq> x"
apply (induct x, simp)
apply (simp add: monofun_cfun d1.below d2.below)
done
qed

lemma finite_deflation_sprod_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (sprod_map·d1·d2)"
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
thus "deflation (sprod_map·d1·d2)" by (rule deflation_sprod_map)
have "{x. sprod_map·d1·d2·x = x} ⊆ insert ⊥
((λ(x, y). (:x, y:)) ` ({x. d1·x = x} × {y. d2·y = y}))"

by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
thus "finite {x. sprod_map·d1·d2·x = x}"
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed

subsection {* Map function for strict sums *}

definition
ssum_map :: "('a -> 'b) -> ('c -> 'd) -> 'a ⊕ 'c -> 'b ⊕ 'd"
where
"ssum_map = (Λ f g. sscase·(sinl oo f)·(sinr oo g))"

lemma ssum_map_strict [simp]: "ssum_map·f·g·⊥ = ⊥"
unfolding ssum_map_def by simp

lemma ssum_map_sinl [simp]: "x ≠ ⊥ ==> ssum_map·f·g·(sinl·x) = sinl·(f·x)"
unfolding ssum_map_def by simp

lemma ssum_map_sinr [simp]: "x ≠ ⊥ ==> ssum_map·f·g·(sinr·x) = sinr·(g·x)"
unfolding ssum_map_def by simp

lemma ssum_map_sinl': "f·⊥ = ⊥ ==> ssum_map·f·g·(sinl·x) = sinl·(f·x)"
by (cases "x = ⊥") simp_all

lemma ssum_map_sinr': "g·⊥ = ⊥ ==> ssum_map·f·g·(sinr·x) = sinr·(g·x)"
by (cases "x = ⊥") simp_all

lemma ssum_map_ID: "ssum_map·ID·ID = ID"
unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)

lemma ssum_map_map:
"[|f1·⊥ = ⊥; g1·⊥ = ⊥|] ==>
ssum_map·f1·g1·(ssum_map·f2·g2·p) =
ssum_map·(Λ x. f1·(f2·x))·(Λ x. g1·(g2·x))·p"

apply (induct p, simp)
apply (case_tac "f2·x = ⊥", simp, simp)
apply (case_tac "g2·y = ⊥", simp, simp)
done

lemma ep_pair_ssum_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
shows "ep_pair (ssum_map·e1·e2) (ssum_map·p1·p2)"
proof
interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
fix x show "ssum_map·p1·p2·(ssum_map·e1·e2·x) = x"
by (induct x) simp_all
fix y show "ssum_map·e1·e2·(ssum_map·p1·p2·y) \<sqsubseteq> y"
apply (induct y, simp)
apply (case_tac "p1·x = ⊥", simp, simp add: e1p1.e_p_below)
apply (case_tac "p2·y = ⊥", simp, simp add: e2p2.e_p_below)
done
qed

lemma deflation_ssum_map:
assumes "deflation d1" and "deflation d2"
shows "deflation (ssum_map·d1·d2)"
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix x
show "ssum_map·d1·d2·(ssum_map·d1·d2·x) = ssum_map·d1·d2·x"
apply (induct x, simp)
apply (case_tac "d1·x = ⊥", simp, simp add: d1.idem)
apply (case_tac "d2·y = ⊥", simp, simp add: d2.idem)
done
show "ssum_map·d1·d2·x \<sqsubseteq> x"
apply (induct x, simp)
apply (case_tac "d1·x = ⊥", simp, simp add: d1.below)
apply (case_tac "d2·y = ⊥", simp, simp add: d2.below)
done
qed

lemma finite_deflation_ssum_map:
assumes "finite_deflation d1" and "finite_deflation d2"
shows "finite_deflation (ssum_map·d1·d2)"
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
thus "deflation (ssum_map·d1·d2)" by (rule deflation_ssum_map)
have "{x. ssum_map·d1·d2·x = x} ⊆
(λx. sinl·x) ` {x. d1·x = x} ∪
(λx. sinr·x) ` {x. d2·x = x} ∪ {⊥}"

by (rule subsetI, case_tac x, simp_all)
thus "finite {x. ssum_map·d1·d2·x = x}"
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed

subsection {* Map operator for strict function space *}

definition
sfun_map :: "('b -> 'a) -> ('c -> 'd) -> ('a ->! 'c) -> ('b ->! 'd)"
where
"sfun_map = (Λ a b. sfun_abs oo cfun_map·a·b oo sfun_rep)"

lemma sfun_map_ID: "sfun_map·ID·ID = ID"
unfolding sfun_map_def
by (simp add: cfun_map_ID cfun_eq_iff)

lemma sfun_map_map:
assumes "f2·⊥ = ⊥" and "g2·⊥ = ⊥" shows
"sfun_map·f1·g1·(sfun_map·f2·g2·p) =
sfun_map·(Λ x. f2·(f1·x))·(Λ x. g1·(g2·x))·p"

unfolding sfun_map_def
by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)

lemma ep_pair_sfun_map:
assumes 1: "ep_pair e1 p1"
assumes 2: "ep_pair e2 p2"
shows "ep_pair (sfun_map·p1·e2) (sfun_map·e1·p2)"
proof
interpret e1p1: pcpo_ep_pair e1 p1
unfolding pcpo_ep_pair_def by fact
interpret e2p2: pcpo_ep_pair e2 p2
unfolding pcpo_ep_pair_def by fact
fix f show "sfun_map·e1·p2·(sfun_map·p1·e2·f) = f"
unfolding sfun_map_def
apply (simp add: sfun_eq_iff strictify_cancel)
apply (rule ep_pair.e_inverse)
apply (rule ep_pair_cfun_map [OF 1 2])
done
fix g show "sfun_map·p1·e2·(sfun_map·e1·p2·g) \<sqsubseteq> g"
unfolding sfun_map_def
apply (simp add: sfun_below_iff strictify_cancel)
apply (rule ep_pair.e_p_below)
apply (rule ep_pair_cfun_map [OF 1 2])
done
qed

lemma deflation_sfun_map:
assumes 1: "deflation d1"
assumes 2: "deflation d2"
shows "deflation (sfun_map·d1·d2)"
apply (simp add: sfun_map_def)
apply (rule deflation.intro)
apply simp
apply (subst strictify_cancel)
apply (simp add: cfun_map_def deflation_strict 1 2)
apply (simp add: cfun_map_def deflation.idem 1 2)
apply (simp add: sfun_below_iff)
apply (subst strictify_cancel)
apply (simp add: cfun_map_def deflation_strict 1 2)
apply (rule deflation.below)
apply (rule deflation_cfun_map [OF 1 2])
done

lemma finite_deflation_sfun_map:
assumes 1: "finite_deflation d1"
assumes 2: "finite_deflation d2"
shows "finite_deflation (sfun_map·d1·d2)"
proof (intro finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
have "deflation d1" and "deflation d2" by fact+
thus "deflation (sfun_map·d1·d2)" by (rule deflation_sfun_map)
from 1 2 have "finite_deflation (cfun_map·d1·d2)"
by (rule finite_deflation_cfun_map)
then have "finite {f. cfun_map·d1·d2·f = f}"
by (rule finite_deflation.finite_fixes)
moreover have "inj (λf. sfun_rep·f)"
by (rule inj_onI, simp add: sfun_eq_iff)
ultimately have "finite ((λf. sfun_rep·f) -` {f. cfun_map·d1·d2·f = f})"
by (rule finite_vimageI)
then show "finite {f. sfun_map·d1·d2·f = f}"
unfolding sfun_map_def sfun_eq_iff
by (simp add: strictify_cancel
deflation_strict `deflation d1` `deflation d2`)
qed

end