1.1 --- a/src/HOLCF/Algebraic.thy	Wed Nov 10 14:59:52 2010 -0800
     1.2 +++ b/src/HOLCF/Algebraic.thy	Wed Nov 10 17:56:08 2010 -0800
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Algebraic deflations *}
     1.5  
     1.6  theory Algebraic
     1.7 -imports Universal
     1.8 +imports Universal Map_Functions
     1.9  begin
    1.10  
    1.11  subsection {* Type constructor for finite deflations *}

     2.1 --- a/src/HOLCF/Bifinite.thy	Wed Nov 10 14:59:52 2010 -0800
     2.2 +++ b/src/HOLCF/Bifinite.thy	Wed Nov 10 17:56:08 2010 -0800
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Bifinite domains *}
     2.5  
     2.6  theory Bifinite
     2.7 -imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
     2.8 +imports Algebraic Map_Functions Countable
     2.9  begin
    2.10  
    2.11  subsection {* Class of bifinite domains *}

     3.1 --- a/src/HOLCF/Cfun.thy	Wed Nov 10 14:59:52 2010 -0800
     3.2 +++ b/src/HOLCF/Cfun.thy	Wed Nov 10 17:56:08 2010 -0800
     3.3 @@ -479,24 +479,6 @@
     3.4  lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
     3.5  by (rule cfun_eqI, simp)
     3.6  
     3.7 -subsection {* Map operator for continuous function space *}
     3.8 -
     3.9 -definition
    3.10 -  cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
    3.11 -where
    3.12 -  "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
    3.13 -
    3.14 -lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
    3.15 -unfolding cfun_map_def by simp
    3.16 -
    3.17 -lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
    3.18 -unfolding cfun_eq_iff by simp
    3.19 -
    3.20 -lemma cfun_map_map:
    3.21 -  "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    3.22 -    cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    3.23 -by (rule cfun_eqI) simp
    3.24 -
    3.25  subsection {* Strictified functions *}
    3.26  
    3.27  default_sort pcpo

     4.1 --- a/src/HOLCF/Completion.thy	Wed Nov 10 14:59:52 2010 -0800
     4.2 +++ b/src/HOLCF/Completion.thy	Wed Nov 10 17:56:08 2010 -0800
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Defining algebraic domains by ideal completion *}
     4.5  
     4.6  theory Completion
     4.7 -imports Cfun
     4.8 +imports Plain_HOLCF
     4.9  begin
    4.10  
    4.11  subsection {* Ideals over a preorder *}

     5.1 --- a/src/HOLCF/Cprod.thy	Wed Nov 10 14:59:52 2010 -0800
     5.2 +++ b/src/HOLCF/Cprod.thy	Wed Nov 10 17:56:08 2010 -0800
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* The cpo of cartesian products *}
     5.5  
     5.6  theory Cprod
     5.7 -imports Deflation
     5.8 +imports Cfun
     5.9  begin
    5.10  
    5.11  default_sort cpo
    5.12 @@ -40,61 +40,4 @@
    5.13  lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    5.14  by (simp add: csplit_def)
    5.15  
    5.16 -subsection {* Map operator for product type *}
    5.17 -
    5.18 -definition
    5.19 -  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    5.20 -where
    5.21 -  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    5.22 -
    5.23 -lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    5.24 -unfolding cprod_map_def by simp
    5.25 -
    5.26 -lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
    5.27 -unfolding cfun_eq_iff by auto
    5.28 -
    5.29 -lemma cprod_map_map:
    5.30 -  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    5.31 -    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    5.32 -by (induct p) simp
    5.33 -
    5.34 -lemma ep_pair_cprod_map:
    5.35 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    5.36 -  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    5.37 -proof
    5.38 -  interpret e1p1: ep_pair e1 p1 by fact
    5.39 -  interpret e2p2: ep_pair e2 p2 by fact
    5.40 -  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    5.41 -    by (induct x) simp
    5.42 -  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    5.43 -    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    5.44 -qed
    5.45 -
    5.46 -lemma deflation_cprod_map:
    5.47 -  assumes "deflation d1" and "deflation d2"
    5.48 -  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
    5.49 -proof
    5.50 -  interpret d1: deflation d1 by fact
    5.51 -  interpret d2: deflation d2 by fact
    5.52 -  fix x
    5.53 -  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    5.54 -    by (induct x) (simp add: d1.idem d2.idem)
    5.55 -  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    5.56 -    by (induct x) (simp add: d1.below d2.below)
    5.57 -qed
    5.58 -
    5.59 -lemma finite_deflation_cprod_map:
    5.60 -  assumes "finite_deflation d1" and "finite_deflation d2"
    5.61 -  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
    5.62 -proof (rule finite_deflation_intro)
    5.63 -  interpret d1: finite_deflation d1 by fact
    5.64 -  interpret d2: finite_deflation d2 by fact
    5.65 -  have "deflation d1" and "deflation d2" by fact+
    5.66 -  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
    5.67 -  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    5.68 -    by clarsimp
    5.69 -  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    5.70 -    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    5.71 -qed
    5.72 -
    5.73  end

     6.1 --- a/src/HOLCF/Deflation.thy	Wed Nov 10 14:59:52 2010 -0800
     6.2 +++ b/src/HOLCF/Deflation.thy	Wed Nov 10 17:56:08 2010 -0800
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Continuous deflations and ep-pairs *}
     6.5  
     6.6  theory Deflation
     6.7 -imports Cfun
     6.8 +imports Plain_HOLCF
     6.9  begin
    6.10  
    6.11  default_sort cpo
    6.12 @@ -405,93 +405,4 @@
    6.13  
    6.14  end
    6.15  
    6.16 -subsection {* Map operator for continuous functions *}
    6.17 -
    6.18 -lemma ep_pair_cfun_map:
    6.19 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    6.20 -  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
    6.21 -proof
    6.22 -  interpret e1p1: ep_pair e1 p1 by fact
    6.23 -  interpret e2p2: ep_pair e2 p2 by fact
    6.24 -  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    6.25 -    by (simp add: cfun_eq_iff)
    6.26 -  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
    6.27 -    apply (rule cfun_belowI, simp)
    6.28 -    apply (rule below_trans [OF e2p2.e_p_below])
    6.29 -    apply (rule monofun_cfun_arg)
    6.30 -    apply (rule e1p1.e_p_below)
    6.31 -    done
    6.32 -qed
    6.33 -
    6.34 -lemma deflation_cfun_map:
    6.35 -  assumes "deflation d1" and "deflation d2"
    6.36 -  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
    6.37 -proof
    6.38 -  interpret d1: deflation d1 by fact
    6.39 -  interpret d2: deflation d2 by fact
    6.40 -  fix f
    6.41 -  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
    6.42 -    by (simp add: cfun_eq_iff d1.idem d2.idem)
    6.43 -  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
    6.44 -    apply (rule cfun_belowI, simp)
    6.45 -    apply (rule below_trans [OF d2.below])
    6.46 -    apply (rule monofun_cfun_arg)
    6.47 -    apply (rule d1.below)
    6.48 -    done
    6.49 -qed
    6.50 -
    6.51 -lemma finite_range_cfun_map:
    6.52 -  assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
    6.53 -  assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
    6.54 -  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
    6.55 -proof (rule finite_imageD)
    6.56 -  let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
    6.57 -  show "finite (?f ` range ?h)"
    6.58 -  proof (rule finite_subset)
    6.59 -    let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
    6.60 -    show "?f ` range ?h \<subseteq> ?B"
    6.61 -      by clarsimp
    6.62 -    show "finite ?B"
    6.63 -      by (simp add: a b)
    6.64 -  qed
    6.65 -  show "inj_on ?f (range ?h)"
    6.66 -  proof (rule inj_onI, rule cfun_eqI, clarsimp)
    6.67 -    fix x f g
    6.68 -    assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    6.69 -    hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    6.70 -      by (rule equalityD1)
    6.71 -    hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    6.72 -      by (simp add: subset_eq)
    6.73 -    then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
    6.74 -      by (rule rangeE)
    6.75 -    thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
    6.76 -      by clarsimp
    6.77 -  qed
    6.78 -qed
    6.79 -
    6.80 -lemma finite_deflation_cfun_map:
    6.81 -  assumes "finite_deflation d1" and "finite_deflation d2"
    6.82 -  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
    6.83 -proof (rule finite_deflation_intro)
    6.84 -  interpret d1: finite_deflation d1 by fact
    6.85 -  interpret d2: finite_deflation d2 by fact
    6.86 -  have "deflation d1" and "deflation d2" by fact+
    6.87 -  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
    6.88 -  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
    6.89 -    using d1.finite_range d2.finite_range
    6.90 -    by (rule finite_range_cfun_map)
    6.91 -  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
    6.92 -    by (rule finite_range_imp_finite_fixes)
    6.93 -qed
    6.94 -
    6.95 -text {* Finite deflations are compact elements of the function space *}
    6.96 -
    6.97 -lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
    6.98 -apply (frule finite_deflation_imp_deflation)
    6.99 -apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
   6.100 -apply (simp add: cfun_map_def deflation.idem eta_cfun)
   6.101 -apply (rule finite_deflation.compact)
   6.102 -apply (simp only: finite_deflation_cfun_map)
   6.103 -done
   6.104 -
   6.105  end

     7.1 --- a/src/HOLCF/Domain_Aux.thy	Wed Nov 10 14:59:52 2010 -0800
     7.2 +++ b/src/HOLCF/Domain_Aux.thy	Wed Nov 10 17:56:08 2010 -0800
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Domain package support *}
     7.5  
     7.6  theory Domain_Aux
     7.7 -imports Ssum Sprod Fixrec
     7.8 +imports Map_Functions Fixrec
     7.9  uses
    7.10    ("Tools/Domain/domain_take_proofs.ML")
    7.11  begin

     8.1 --- a/src/HOLCF/Fixrec.thy	Wed Nov 10 14:59:52 2010 -0800
     8.2 +++ b/src/HOLCF/Fixrec.thy	Wed Nov 10 17:56:08 2010 -0800
     8.3 @@ -5,7 +5,7 @@
     8.4  header "Package for defining recursive functions in HOLCF"
     8.5  
     8.6  theory Fixrec
     8.7 -imports Cprod Sprod Ssum Up One Tr Fix
     8.8 +imports Plain_HOLCF
     8.9  uses
    8.10    ("Tools/holcf_library.ML")
    8.11    ("Tools/fixrec.ML")

     9.1 --- a/src/HOLCF/IsaMakefile	Wed Nov 10 14:59:52 2010 -0800
     9.2 +++ b/src/HOLCF/IsaMakefile	Wed Nov 10 17:56:08 2010 -0800
     9.3 @@ -54,9 +54,11 @@
     9.4    HOLCF.thy \
     9.5    Lift.thy \
     9.6    LowerPD.thy \
     9.7 +  Map_Functions.thy \
     9.8    One.thy \
     9.9    Pcpodef.thy \
    9.10    Pcpo.thy \
    9.11 +  Plain_HOLCF.thy \
    9.12    Porder.thy \
    9.13    Powerdomains.thy \
    9.14    Product_Cpo.thy \

    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOLCF/Map_Functions.thy	Wed Nov 10 17:56:08 2010 -0800
    10.3 @@ -0,0 +1,383 @@
    10.4 +(*  Title:      HOLCF/Map_Functions.thy
    10.5 +    Author:     Brian Huffman
    10.6 +*)
    10.7 +
    10.8 +header {* Map functions for various types *}
    10.9 +
   10.10 +theory Map_Functions
   10.11 +imports Deflation
   10.12 +begin
   10.13 +
   10.14 +subsection {* Map operator for continuous function space *}
   10.15 +
   10.16 +default_sort cpo
   10.17 +
   10.18 +definition
   10.19 +  cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
   10.20 +where
   10.21 +  "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
   10.22 +
   10.23 +lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
   10.24 +unfolding cfun_map_def by simp
   10.25 +
   10.26 +lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
   10.27 +unfolding cfun_eq_iff by simp
   10.28 +
   10.29 +lemma cfun_map_map:
   10.30 +  "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
   10.31 +    cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   10.32 +by (rule cfun_eqI) simp
   10.33 +
   10.34 +lemma ep_pair_cfun_map:
   10.35 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   10.36 +  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
   10.37 +proof
   10.38 +  interpret e1p1: ep_pair e1 p1 by fact
   10.39 +  interpret e2p2: ep_pair e2 p2 by fact
   10.40 +  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
   10.41 +    by (simp add: cfun_eq_iff)
   10.42 +  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
   10.43 +    apply (rule cfun_belowI, simp)
   10.44 +    apply (rule below_trans [OF e2p2.e_p_below])
   10.45 +    apply (rule monofun_cfun_arg)
   10.46 +    apply (rule e1p1.e_p_below)
   10.47 +    done
   10.48 +qed
   10.49 +
   10.50 +lemma deflation_cfun_map:
   10.51 +  assumes "deflation d1" and "deflation d2"
   10.52 +  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
   10.53 +proof
   10.54 +  interpret d1: deflation d1 by fact
   10.55 +  interpret d2: deflation d2 by fact
   10.56 +  fix f
   10.57 +  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
   10.58 +    by (simp add: cfun_eq_iff d1.idem d2.idem)
   10.59 +  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
   10.60 +    apply (rule cfun_belowI, simp)
   10.61 +    apply (rule below_trans [OF d2.below])
   10.62 +    apply (rule monofun_cfun_arg)
   10.63 +    apply (rule d1.below)
   10.64 +    done
   10.65 +qed
   10.66 +
   10.67 +lemma finite_range_cfun_map:
   10.68 +  assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   10.69 +  assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
   10.70 +  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
   10.71 +proof (rule finite_imageD)
   10.72 +  let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   10.73 +  show "finite (?f ` range ?h)"
   10.74 +  proof (rule finite_subset)
   10.75 +    let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
   10.76 +    show "?f ` range ?h \<subseteq> ?B"
   10.77 +      by clarsimp
   10.78 +    show "finite ?B"
   10.79 +      by (simp add: a b)
   10.80 +  qed
   10.81 +  show "inj_on ?f (range ?h)"
   10.82 +  proof (rule inj_onI, rule cfun_eqI, clarsimp)
   10.83 +    fix x f g
   10.84 +    assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   10.85 +    hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   10.86 +      by (rule equalityD1)
   10.87 +    hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   10.88 +      by (simp add: subset_eq)
   10.89 +    then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
   10.90 +      by (rule rangeE)
   10.91 +    thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
   10.92 +      by clarsimp
   10.93 +  qed
   10.94 +qed
   10.95 +
   10.96 +lemma finite_deflation_cfun_map:
   10.97 +  assumes "finite_deflation d1" and "finite_deflation d2"
   10.98 +  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   10.99 +proof (rule finite_deflation_intro)
  10.100 +  interpret d1: finite_deflation d1 by fact
  10.101 +  interpret d2: finite_deflation d2 by fact
  10.102 +  have "deflation d1" and "deflation d2" by fact+
  10.103 +  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
  10.104 +  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
  10.105 +    using d1.finite_range d2.finite_range
  10.106 +    by (rule finite_range_cfun_map)
  10.107 +  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
  10.108 +    by (rule finite_range_imp_finite_fixes)
  10.109 +qed
  10.110 +
  10.111 +text {* Finite deflations are compact elements of the function space *}
  10.112 +
  10.113 +lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
  10.114 +apply (frule finite_deflation_imp_deflation)
  10.115 +apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
  10.116 +apply (simp add: cfun_map_def deflation.idem eta_cfun)
  10.117 +apply (rule finite_deflation.compact)
  10.118 +apply (simp only: finite_deflation_cfun_map)
  10.119 +done
  10.120 +
  10.121 +subsection {* Map operator for product type *}
  10.122 +
  10.123 +definition
  10.124 +  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
  10.125 +where
  10.126 +  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
  10.127 +
  10.128 +lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
  10.129 +unfolding cprod_map_def by simp
  10.130 +
  10.131 +lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
  10.132 +unfolding cfun_eq_iff by auto
  10.133 +
  10.134 +lemma cprod_map_map:
  10.135 +  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
  10.136 +    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
  10.137 +by (induct p) simp
  10.138 +
  10.139 +lemma ep_pair_cprod_map:
  10.140 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
  10.141 +  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
  10.142 +proof
  10.143 +  interpret e1p1: ep_pair e1 p1 by fact
  10.144 +  interpret e2p2: ep_pair e2 p2 by fact
  10.145 +  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
  10.146 +    by (induct x) simp
  10.147 +  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
  10.148 +    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
  10.149 +qed
  10.150 +
  10.151 +lemma deflation_cprod_map:
  10.152 +  assumes "deflation d1" and "deflation d2"
  10.153 +  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
  10.154 +proof
  10.155 +  interpret d1: deflation d1 by fact
  10.156 +  interpret d2: deflation d2 by fact
  10.157 +  fix x
  10.158 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
  10.159 +    by (induct x) (simp add: d1.idem d2.idem)
  10.160 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
  10.161 +    by (induct x) (simp add: d1.below d2.below)
  10.162 +qed
  10.163 +
  10.164 +lemma finite_deflation_cprod_map:
  10.165 +  assumes "finite_deflation d1" and "finite_deflation d2"
  10.166 +  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
  10.167 +proof (rule finite_deflation_intro)
  10.168 +  interpret d1: finite_deflation d1 by fact
  10.169 +  interpret d2: finite_deflation d2 by fact
  10.170 +  have "deflation d1" and "deflation d2" by fact+
  10.171 +  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
  10.172 +  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
  10.173 +    by clarsimp
  10.174 +  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
  10.175 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
  10.176 +qed
  10.177 +
  10.178 +subsection {* Map function for lifted cpo *}
  10.179 +
  10.180 +definition
  10.181 +  u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
  10.182 +where
  10.183 +  "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
  10.184 +
  10.185 +lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
  10.186 +unfolding u_map_def by simp
  10.187 +
  10.188 +lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
  10.189 +unfolding u_map_def by simp
  10.190 +
  10.191 +lemma u_map_ID: "u_map\<cdot>ID = ID"
  10.192 +unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
  10.193 +
  10.194 +lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
  10.195 +by (induct p) simp_all
  10.196 +
  10.197 +lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
  10.198 +apply default
  10.199 +apply (case_tac x, simp, simp add: ep_pair.e_inverse)
  10.200 +apply (case_tac y, simp, simp add: ep_pair.e_p_below)
  10.201 +done
  10.202 +
  10.203 +lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
  10.204 +apply default
  10.205 +apply (case_tac x, simp, simp add: deflation.idem)
  10.206 +apply (case_tac x, simp, simp add: deflation.below)
  10.207 +done
  10.208 +
  10.209 +lemma finite_deflation_u_map:
  10.210 +  assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
  10.211 +proof (rule finite_deflation_intro)
  10.212 +  interpret d: finite_deflation d by fact
  10.213 +  have "deflation d" by fact
  10.214 +  thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
  10.215 +  have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
  10.216 +    by (rule subsetI, case_tac x, simp_all)
  10.217 +  thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
  10.218 +    by (rule finite_subset, simp add: d.finite_fixes)
  10.219 +qed
  10.220 +
  10.221 +subsection {* Map function for strict products *}
  10.222 +
  10.223 +default_sort pcpo
  10.224 +
  10.225 +definition
  10.226 +  sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
  10.227 +where
  10.228 +  "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
  10.229 +
  10.230 +lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
  10.231 +unfolding sprod_map_def by simp
  10.232 +
  10.233 +lemma sprod_map_spair [simp]:
  10.234 +  "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
  10.235 +by (simp add: sprod_map_def)
  10.236 +
  10.237 +lemma sprod_map_spair':
  10.238 +  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
  10.239 +by (cases "x = \<bottom> \<or> y = \<bottom>") auto
  10.240 +
  10.241 +lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
  10.242 +unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
  10.243 +
  10.244 +lemma sprod_map_map:
  10.245 +  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
  10.246 +    sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
  10.247 +     sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
  10.248 +apply (induct p, simp)
  10.249 +apply (case_tac "f2\<cdot>x = \<bottom>", simp)
  10.250 +apply (case_tac "g2\<cdot>y = \<bottom>", simp)
  10.251 +apply simp
  10.252 +done
  10.253 +
  10.254 +lemma ep_pair_sprod_map:
  10.255 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
  10.256 +  shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
  10.257 +proof
  10.258 +  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
  10.259 +  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
  10.260 +  fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
  10.261 +    by (induct x) simp_all
  10.262 +  fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
  10.263 +    apply (induct y, simp)
  10.264 +    apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
  10.265 +    apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
  10.266 +    done
  10.267 +qed
  10.268 +
  10.269 +lemma deflation_sprod_map:
  10.270 +  assumes "deflation d1" and "deflation d2"
  10.271 +  shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
  10.272 +proof
  10.273 +  interpret d1: deflation d1 by fact
  10.274 +  interpret d2: deflation d2 by fact
  10.275 +  fix x
  10.276 +  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
  10.277 +    apply (induct x, simp)
  10.278 +    apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
  10.279 +    apply (simp add: d1.idem d2.idem)
  10.280 +    done
  10.281 +  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
  10.282 +    apply (induct x, simp)
  10.283 +    apply (simp add: monofun_cfun d1.below d2.below)
  10.284 +    done
  10.285 +qed
  10.286 +
  10.287 +lemma finite_deflation_sprod_map:
  10.288 +  assumes "finite_deflation d1" and "finite_deflation d2"
  10.289 +  shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
  10.290 +proof (rule finite_deflation_intro)
  10.291 +  interpret d1: finite_deflation d1 by fact
  10.292 +  interpret d2: finite_deflation d2 by fact
  10.293 +  have "deflation d1" and "deflation d2" by fact+
  10.294 +  thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
  10.295 +  have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
  10.296 +        ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
  10.297 +    by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
  10.298 +  thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
  10.299 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
  10.300 +qed
  10.301 +
  10.302 +subsection {* Map function for strict sums *}
  10.303 +
  10.304 +definition
  10.305 +  ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
  10.306 +where
  10.307 +  "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
  10.308 +
  10.309 +lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
  10.310 +unfolding ssum_map_def by simp
  10.311 +
  10.312 +lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
  10.313 +unfolding ssum_map_def by simp
  10.314 +
  10.315 +lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
  10.316 +unfolding ssum_map_def by simp
  10.317 +
  10.318 +lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
  10.319 +by (cases "x = \<bottom>") simp_all
  10.320 +
  10.321 +lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
  10.322 +by (cases "x = \<bottom>") simp_all
  10.323 +
  10.324 +lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
  10.325 +unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
  10.326 +
  10.327 +lemma ssum_map_map:
  10.328 +  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
  10.329 +    ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
  10.330 +     ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
  10.331 +apply (induct p, simp)
  10.332 +apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
  10.333 +apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
  10.334 +done
  10.335 +
  10.336 +lemma ep_pair_ssum_map:
  10.337 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
  10.338 +  shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
  10.339 +proof
  10.340 +  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
  10.341 +  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
  10.342 +  fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
  10.343 +    by (induct x) simp_all
  10.344 +  fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
  10.345 +    apply (induct y, simp)
  10.346 +    apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
  10.347 +    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
  10.348 +    done
  10.349 +qed
  10.350 +
  10.351 +lemma deflation_ssum_map:
  10.352 +  assumes "deflation d1" and "deflation d2"
  10.353 +  shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
  10.354 +proof
  10.355 +  interpret d1: deflation d1 by fact
  10.356 +  interpret d2: deflation d2 by fact
  10.357 +  fix x
  10.358 +  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
  10.359 +    apply (induct x, simp)
  10.360 +    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
  10.361 +    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
  10.362 +    done
  10.363 +  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
  10.364 +    apply (induct x, simp)
  10.365 +    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
  10.366 +    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
  10.367 +    done
  10.368 +qed
  10.369 +
  10.370 +lemma finite_deflation_ssum_map:
  10.371 +  assumes "finite_deflation d1" and "finite_deflation d2"
  10.372 +  shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
  10.373 +proof (rule finite_deflation_intro)
  10.374 +  interpret d1: finite_deflation d1 by fact
  10.375 +  interpret d2: finite_deflation d2 by fact
  10.376 +  have "deflation d1" and "deflation d2" by fact+
  10.377 +  thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
  10.378 +  have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
  10.379 +        (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
  10.380 +        (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
  10.381 +    by (rule subsetI, case_tac x, simp_all)
  10.382 +  thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
  10.383 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
  10.384 +qed
  10.385 +
  10.386 +end

    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOLCF/Plain_HOLCF.thy	Wed Nov 10 17:56:08 2010 -0800
    11.3 @@ -0,0 +1,15 @@
    11.4 +(*  Title:      HOLCF/Plain_HOLCF.thy
    11.5 +    Author:     Brian Huffman
    11.6 +*)
    11.7 +
    11.8 +header {* Plain HOLCF *}
    11.9 +
   11.10 +theory Plain_HOLCF
   11.11 +imports Cfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
   11.12 +begin
   11.13 +
   11.14 +text {*
   11.15 +  Basic HOLCF concepts and types; does not include definition packages.
   11.16 +*}
   11.17 +
   11.18 +end

    12.1 --- a/src/HOLCF/Sprod.thy	Wed Nov 10 14:59:52 2010 -0800
    12.2 +++ b/src/HOLCF/Sprod.thy	Wed Nov 10 17:56:08 2010 -0800
    12.3 @@ -1,11 +1,12 @@
    12.4  (*  Title:      HOLCF/Sprod.thy
    12.5 -    Author:     Franz Regensburger and Brian Huffman
    12.6 +    Author:     Franz Regensburger
    12.7 +    Author:     Brian Huffman
    12.8  *)
    12.9  
   12.10  header {* The type of strict products *}
   12.11  
   12.12  theory Sprod
   12.13 -imports Deflation
   12.14 +imports Cfun
   12.15  begin
   12.16  
   12.17  default_sort pcpo
   12.18 @@ -210,83 +211,4 @@
   12.19      done
   12.20  qed
   12.21  
   12.22 -subsection {* Map function for strict products *}
   12.23 -
   12.24 -definition
   12.25 -  sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
   12.26 -where
   12.27 -  "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
   12.28 -
   12.29 -lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
   12.30 -unfolding sprod_map_def by simp
   12.31 -
   12.32 -lemma sprod_map_spair [simp]:
   12.33 -  "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
   12.34 -by (simp add: sprod_map_def)
   12.35 -
   12.36 -lemma sprod_map_spair':
   12.37 -  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
   12.38 -by (cases "x = \<bottom> \<or> y = \<bottom>") auto
   12.39 -
   12.40 -lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
   12.41 -unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
   12.42 -
   12.43 -lemma sprod_map_map:
   12.44 -  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
   12.45 -    sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
   12.46 -     sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   12.47 -apply (induct p, simp)
   12.48 -apply (case_tac "f2\<cdot>x = \<bottom>", simp)
   12.49 -apply (case_tac "g2\<cdot>y = \<bottom>", simp)
   12.50 -apply simp
   12.51 -done
   12.52 -
   12.53 -lemma ep_pair_sprod_map:
   12.54 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   12.55 -  shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
   12.56 -proof
   12.57 -  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
   12.58 -  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
   12.59 -  fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
   12.60 -    by (induct x) simp_all
   12.61 -  fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
   12.62 -    apply (induct y, simp)
   12.63 -    apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
   12.64 -    apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
   12.65 -    done
   12.66 -qed
   12.67 -
   12.68 -lemma deflation_sprod_map:
   12.69 -  assumes "deflation d1" and "deflation d2"
   12.70 -  shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
   12.71 -proof
   12.72 -  interpret d1: deflation d1 by fact
   12.73 -  interpret d2: deflation d2 by fact
   12.74 -  fix x
   12.75 -  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
   12.76 -    apply (induct x, simp)
   12.77 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
   12.78 -    apply (simp add: d1.idem d2.idem)
   12.79 -    done
   12.80 -  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   12.81 -    apply (induct x, simp)
   12.82 -    apply (simp add: monofun_cfun d1.below d2.below)
   12.83 -    done
   12.84 -qed
   12.85 -
   12.86 -lemma finite_deflation_sprod_map:
   12.87 -  assumes "finite_deflation d1" and "finite_deflation d2"
   12.88 -  shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
   12.89 -proof (rule finite_deflation_intro)
   12.90 -  interpret d1: finite_deflation d1 by fact
   12.91 -  interpret d2: finite_deflation d2 by fact
   12.92 -  have "deflation d1" and "deflation d2" by fact+
   12.93 -  thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
   12.94 -  have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
   12.95 -        ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
   12.96 -    by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
   12.97 -  thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
   12.98 -    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   12.99 -qed
  12.100 -
  12.101  end

    13.1 --- a/src/HOLCF/Ssum.thy	Wed Nov 10 14:59:52 2010 -0800
    13.2 +++ b/src/HOLCF/Ssum.thy	Wed Nov 10 17:56:08 2010 -0800
    13.3 @@ -1,5 +1,6 @@
    13.4  (*  Title:      HOLCF/Ssum.thy
    13.5 -    Author:     Franz Regensburger and Brian Huffman
    13.6 +    Author:     Franz Regensburger
    13.7 +    Author:     Brian Huffman
    13.8  *)
    13.9  
   13.10  header {* The type of strict sums *}
   13.11 @@ -194,88 +195,4 @@
   13.12  apply (case_tac y, simp_all add: flat_below_iff)
   13.13  done
   13.14  
   13.15 -subsection {* Map function for strict sums *}
   13.16 -
   13.17 -definition
   13.18 -  ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
   13.19 -where
   13.20 -  "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
   13.21 -
   13.22 -lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
   13.23 -unfolding ssum_map_def by simp
   13.24 -
   13.25 -lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
   13.26 -unfolding ssum_map_def by simp
   13.27 -
   13.28 -lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
   13.29 -unfolding ssum_map_def by simp
   13.30 -
   13.31 -lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
   13.32 -by (cases "x = \<bottom>") simp_all
   13.33 -
   13.34 -lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
   13.35 -by (cases "x = \<bottom>") simp_all
   13.36 -
   13.37 -lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
   13.38 -unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
   13.39 -
   13.40 -lemma ssum_map_map:
   13.41 -  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
   13.42 -    ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
   13.43 -     ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   13.44 -apply (induct p, simp)
   13.45 -apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
   13.46 -apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
   13.47 -done
   13.48 -
   13.49 -lemma ep_pair_ssum_map:
   13.50 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   13.51 -  shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
   13.52 -proof
   13.53 -  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
   13.54 -  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
   13.55 -  fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
   13.56 -    by (induct x) simp_all
   13.57 -  fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
   13.58 -    apply (induct y, simp)
   13.59 -    apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
   13.60 -    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
   13.61 -    done
   13.62 -qed
   13.63 -
   13.64 -lemma deflation_ssum_map:
   13.65 -  assumes "deflation d1" and "deflation d2"
   13.66 -  shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
   13.67 -proof
   13.68 -  interpret d1: deflation d1 by fact
   13.69 -  interpret d2: deflation d2 by fact
   13.70 -  fix x
   13.71 -  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
   13.72 -    apply (induct x, simp)
   13.73 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
   13.74 -    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
   13.75 -    done
   13.76 -  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   13.77 -    apply (induct x, simp)
   13.78 -    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
   13.79 -    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
   13.80 -    done
   13.81 -qed
   13.82 -
   13.83 -lemma finite_deflation_ssum_map:
   13.84 -  assumes "finite_deflation d1" and "finite_deflation d2"
   13.85 -  shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
   13.86 -proof (rule finite_deflation_intro)
   13.87 -  interpret d1: finite_deflation d1 by fact
   13.88 -  interpret d2: finite_deflation d2 by fact
   13.89 -  have "deflation d1" and "deflation d2" by fact+
   13.90 -  thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
   13.91 -  have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
   13.92 -        (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
   13.93 -        (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
   13.94 -    by (rule subsetI, case_tac x, simp_all)
   13.95 -  thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
   13.96 -    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   13.97 -qed
   13.98 -
   13.99  end

    14.1 --- a/src/HOLCF/Up.thy	Wed Nov 10 14:59:52 2010 -0800
    14.2 +++ b/src/HOLCF/Up.thy	Wed Nov 10 17:56:08 2010 -0800
    14.3 @@ -1,11 +1,12 @@
    14.4  (*  Title:      HOLCF/Up.thy
    14.5 -    Author:     Franz Regensburger and Brian Huffman
    14.6 +    Author:     Franz Regensburger
    14.7 +    Author:     Brian Huffman
    14.8  *)
    14.9  
   14.10  header {* The type of lifted values *}
   14.11  
   14.12  theory Up
   14.13 -imports Deflation
   14.14 +imports Cfun
   14.15  begin
   14.16  
   14.17  default_sort cpo
   14.18 @@ -259,47 +260,4 @@
   14.19  lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
   14.20  by (cases x, simp_all)
   14.21  
   14.22 -subsection {* Map function for lifted cpo *}
   14.23 -
   14.24 -definition
   14.25 -  u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
   14.26 -where
   14.27 -  "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
   14.28 -
   14.29 -lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
   14.30 -unfolding u_map_def by simp
   14.31 -
   14.32 -lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
   14.33 -unfolding u_map_def by simp
   14.34 -
   14.35 -lemma u_map_ID: "u_map\<cdot>ID = ID"
   14.36 -unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
   14.37 -
   14.38 -lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
   14.39 -by (induct p) simp_all
   14.40 -
   14.41 -lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
   14.42 -apply default
   14.43 -apply (case_tac x, simp, simp add: ep_pair.e_inverse)
   14.44 -apply (case_tac y, simp, simp add: ep_pair.e_p_below)
   14.45 -done
   14.46 -
   14.47 -lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
   14.48 -apply default
   14.49 -apply (case_tac x, simp, simp add: deflation.idem)
   14.50 -apply (case_tac x, simp, simp add: deflation.below)
   14.51 -done
   14.52 -
   14.53 -lemma finite_deflation_u_map:
   14.54 -  assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
   14.55 -proof (rule finite_deflation_intro)
   14.56 -  interpret d: finite_deflation d by fact
   14.57 -  have "deflation d" by fact
   14.58 -  thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
   14.59 -  have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
   14.60 -    by (rule subsetI, case_tac x, simp_all)
   14.61 -  thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
   14.62 -    by (rule finite_subset, simp add: d.finite_fixes)
   14.63 -qed
   14.64 -
   14.65  end