# Theory Map_Functions

theory Map_Functions
imports Deflation Sprod Ssum Sfun

section

theory Map_Functions
imports Deflation Sprod Ssum Sfun Up
begin

subsection

default_sort cpo

definition cfun_map ::
where

lemma cfun_map_beta [simp]:

lemma cfun_map_ID:

lemma cfun_map_map:
by (rule cfun_eqI) simp

lemma ep_pair_cfun_map:
assumes  and
shows
proof
interpret e1p1: ep_pair e1 p1 by fact
interpret e2p2: ep_pair e2 p2 by fact
show  for f
show  for 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  and
shows
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix f
show
by (simp add: cfun_eq_iff d1.idem d2.idem)
show
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:
assumes b:
shows   (is )
proof (rule finite_imageD)
let ?f =
show
proof (rule finite_subset)
let ?B =
show
by clarsimp
show
qed
show
proof (rule inj_onI, rule cfun_eqI, clarsimp)
fix x f g
assume
then have
by (rule equalityD1)
then have
then obtain y where
by (rule rangeE)
then show
by clarsimp
qed
qed

lemma finite_deflation_cfun_map:
assumes  and
shows
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
from d1.deflation_axioms d2.deflation_axioms show
by (rule deflation_cfun_map)
have
using d1.finite_range d2.finite_range
by (rule finite_range_cfun_map)
then show
by (rule finite_range_imp_finite_fixes)
qed

text

lemma finite_deflation_imp_compact:
apply (frule finite_deflation_imp_deflation)
apply (subgoal_tac )
apply (simp add: cfun_map_def deflation.idem eta_cfun)
apply (rule finite_deflation.compact)
apply (simp only: finite_deflation_cfun_map)
done

subsection

definition prod_map ::
where

lemma prod_map_Pair [simp]:

lemma prod_map_ID:
by (auto simp: cfun_eq_iff)

lemma prod_map_map:
by (induct p) simp

lemma ep_pair_prod_map:
assumes  and
shows
proof
interpret e1p1: ep_pair e1 p1 by fact
interpret e2p2: ep_pair e2 p2 by fact
show  for x
by (induct x) simp
show  for y
by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
qed

lemma deflation_prod_map:
assumes  and
shows
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix x
show
by (induct x) (simp add: d1.idem d2.idem)
show
by (induct x) (simp add: d1.below d2.below)
qed

lemma finite_deflation_prod_map:
assumes  and
shows
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
from d1.deflation_axioms d2.deflation_axioms show
by (rule deflation_prod_map)
have
by auto
then show
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed

subsection

definition u_map ::
where

lemma u_map_strict [simp]:

lemma u_map_up [simp]:

lemma u_map_ID:
by (simp add: u_map_def cfun_eq_iff eta_cfun)

lemma u_map_map:
by (induct p) simp_all

lemma u_map_oo:
by (simp add: cfcomp1 u_map_map eta_cfun)

lemma ep_pair_u_map:
apply standard
subgoal for x by (cases x) (simp_all add: ep_pair.e_inverse)
subgoal for y by (cases y) (simp_all add: ep_pair.e_p_below)
done

lemma deflation_u_map:
apply standard
subgoal for x by (cases x) (simp_all add: deflation.idem)
subgoal for x by (cases x) (simp_all add: deflation.below)
done

lemma finite_deflation_u_map:
assumes
shows
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
from d.deflation_axioms show
by (rule deflation_u_map)
have
by (rule subsetI, case_tac x, simp_all)
then show
by (rule finite_subset) (simp add: d.finite_fixes)
qed

subsection

default_sort pcpo

definition sprod_map ::
where

lemma sprod_map_strict [simp]:

lemma sprod_map_spair [simp]:

lemma sprod_map_spair':
by (cases ) auto

lemma sprod_map_ID:
by (simp add: sprod_map_def cfun_eq_iff eta_cfun)

lemma sprod_map_map:

proof (induct p)
case bottom
then show ?case by simp
next
case (spair x y)
then show ?case
apply (cases , simp)
apply (cases , simp)
apply simp
done
qed

lemma ep_pair_sprod_map:
assumes  and
shows
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
show  for x
by (induct x) simp_all
show  for y
proof (induct y)
case bottom
then show ?case by simp
next
case (spair x y)
then show ?case
apply simp
apply (cases , simp, cases , simp)
apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
done
qed
qed

lemma deflation_sprod_map:
assumes  and
shows
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix x
show
proof (induct x)
case bottom
then show ?case by simp
next
case (spair x y)
then show ?case
apply (cases , simp, cases , simp)
done
qed
show
proof (induct x)
case bottom
then show ?case by simp
next
case spair
then show ?case by (simp add: monofun_cfun d1.below d2.below)
qed
qed

lemma finite_deflation_sprod_map:
assumes  and
shows
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
from d1.deflation_axioms d2.deflation_axioms show
by (rule deflation_sprod_map)
have
by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
then show
by (rule finite_subset) (simp add: d1.finite_fixes d2.finite_fixes)
qed

subsection

definition ssum_map ::
where

lemma ssum_map_strict [simp]:

lemma ssum_map_sinl [simp]:

lemma ssum_map_sinr [simp]:

lemma ssum_map_sinl':
by (cases ) simp_all

lemma ssum_map_sinr':
by (cases ) simp_all

lemma ssum_map_ID:
by (simp add: ssum_map_def cfun_eq_iff eta_cfun)

lemma ssum_map_map:

proof (induct p)
case bottom
then show ?case by simp
next
case (sinl x)
then show ?case by (cases ) simp_all
next
case (sinr y)
then show ?case by (cases ) simp_all
qed

lemma ep_pair_ssum_map:
assumes  and
shows
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
show  for x
by (induct x) simp_all
show  for y
proof (induct y)
case bottom
then show ?case by simp
next
case (sinl x)
then show ?case by (cases ) (simp_all add: e1p1.e_p_below)
next
case (sinr y)
then show ?case by (cases ) (simp_all add: e2p2.e_p_below)
qed
qed

lemma deflation_ssum_map:
assumes  and
shows
proof
interpret d1: deflation d1 by fact
interpret d2: deflation d2 by fact
fix x
show
proof (induct x)
case bottom
then show ?case by simp
next
case (sinl x)
then show ?case by (cases ) (simp_all add: d1.idem)
next
case (sinr y)
then show ?case by (cases ) (simp_all add: d2.idem)
qed
show
proof (induct x)
case bottom
then show ?case by simp
next
case (sinl x)
then show ?case by (cases ) (simp_all add: d1.below)
next
case (sinr y)
then show ?case by (cases ) (simp_all add: d2.below)
qed
qed

lemma finite_deflation_ssum_map:
assumes  and
shows
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
from d1.deflation_axioms d2.deflation_axioms show
by (rule deflation_ssum_map)
have
by (rule subsetI, case_tac x, simp_all)
then show
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed

subsection

definition sfun_map ::
where

lemma sfun_map_ID:
by (simp add: sfun_map_def cfun_map_ID cfun_eq_iff)

lemma sfun_map_map:
assumes  and
shows
by (simp add: sfun_map_def cfun_eq_iff strictify_cancel assms cfun_map_map)

lemma ep_pair_sfun_map:
assumes 1:
assumes 2:
shows
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
show  for f
unfolding sfun_map_def
apply (rule ep_pair.e_inverse)
apply (rule ep_pair_cfun_map [OF 1 2])
done
show  for g
unfolding sfun_map_def
apply (rule ep_pair.e_p_below)
apply (rule ep_pair_cfun_map [OF 1 2])
done
qed

lemma deflation_sfun_map:
assumes 1:
assumes 2:
shows
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 (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
and
shows
proof (intro finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
from d1.deflation_axioms d2.deflation_axioms show
by (rule deflation_sfun_map)
from assms have
by (rule finite_deflation_cfun_map)
then have
by (rule finite_deflation.finite_fixes)
moreover have
by (rule inj_onI) (simp add: sfun_eq_iff)
ultimately have
by (rule finite_vimageI)
with   show
by (simp add: sfun_map_def sfun_eq_iff strictify_cancel deflation_strict)
qed

end