# Theory Map_Functions

Up to index of Isabelle/HOL/HOLCF

theory Map_Functions
imports Deflation
`(*  Title:      HOL/HOLCF/Map_Functions.thy    Author:     Brian Huffman*)header {* Map functions for various types *}theory Map_Functionsimports Deflationbeginsubsection {* Map operator for continuous function space *}default_sort cpodefinition  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 simplemma cfun_map_ID: "cfun_map·ID·ID = ID"unfolding cfun_eq_iff by simplemma 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) simplemma 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)    doneqedlemma 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)    doneqedlemma 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  qedqedlemma 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)qedtext {* 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)donesubsection {* 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 simplemma prod_map_ID: "prod_map·ID·ID = ID"unfolding cfun_eq_iff by autolemma 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) simplemma 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)qedlemma 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)qedlemma 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)qedsubsection {* 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 simplemma u_map_up [simp]: "u_map·f·(up·x) = up·(f·x)"unfolding u_map_def by simplemma 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_alllemma 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 defaultapply (case_tac x, simp, simp add: ep_pair.e_inverse)apply (case_tac y, simp, simp add: ep_pair.e_p_below)donelemma deflation_u_map: "deflation d ==> deflation (u_map·d)"apply defaultapply (case_tac x, simp, simp add: deflation.idem)apply (case_tac x, simp, simp add: deflation.below)donelemma 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)qedsubsection {* Map function for strict products *}default_sort pcpodefinition  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 simplemma 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 = ⊥") autolemma 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 simpdonelemma 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)    doneqedlemma 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)    doneqedlemma 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)qedsubsection {* 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 simplemma ssum_map_sinl [simp]: "x ≠ ⊥ ==> ssum_map·f·g·(sinl·x) = sinl·(f·x)"unfolding ssum_map_def by simplemma ssum_map_sinr [simp]: "x ≠ ⊥ ==> ssum_map·f·g·(sinr·x) = sinr·(g·x)"unfolding ssum_map_def by simplemma ssum_map_sinl': "f·⊥ = ⊥ ==> ssum_map·f·g·(sinl·x) = sinl·(f·x)"by (cases "x = ⊥") simp_alllemma ssum_map_sinr': "g·⊥ = ⊥ ==> ssum_map·f·g·(sinr·x) = sinr·(g·x)"by (cases "x = ⊥") simp_alllemma 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)donelemma 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)    doneqedlemma 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)    doneqedlemma 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)qedsubsection {* 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_defby (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])    doneqedlemma 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 simpapply (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])donelemma 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`)qedend`