# HG changeset patch
# User huffman
# Date 1290012478 28800
# Node ID f432973ce0f62994b3ab7aba427b7a9a6a3eb6f3
# Parent  1c0b5bfa52a174bd952b25c1cd5e27b7b09b4c08
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain

diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Bifinite.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -88,8 +88,8 @@
 definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
   where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
 
-definition cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
-  where "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
+  where "sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
 
 definition prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
   where "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
@@ -119,9 +119,9 @@
 using u_map_ID finite_deflation_u_map
 unfolding u_approx_def by (rule approx_chain_lemma1)
 
-lemma cfun_approx: "approx_chain cfun_approx"
-using cfun_map_ID finite_deflation_cfun_map
-unfolding cfun_approx_def by (rule approx_chain_lemma2)
+lemma sfun_approx: "approx_chain sfun_approx"
+using sfun_map_ID finite_deflation_sfun_map
+unfolding sfun_approx_def by (rule approx_chain_lemma2)
 
 lemma prod_approx: "approx_chain prod_approx"
 using cprod_map_ID finite_deflation_cprod_map
@@ -211,8 +211,8 @@
 definition u_defl :: "defl \<rightarrow> defl"
   where "u_defl = defl_fun1 u_approx u_map"
 
-definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-  where "cfun_defl = defl_fun2 cfun_approx cfun_map"
+definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+  where "sfun_defl = defl_fun2 sfun_approx sfun_map"
 
 definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   where "prod_defl = defl_fun2 prod_approx cprod_map"
@@ -229,11 +229,11 @@
 using u_approx finite_deflation_u_map
 unfolding u_defl_def by (rule cast_defl_fun1)
 
-lemma cast_cfun_defl:
-  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
-    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-using cfun_approx finite_deflation_cfun_map
-unfolding cfun_defl_def by (rule cast_defl_fun2)
+lemma cast_sfun_defl:
+  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
+    udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
+using sfun_approx finite_deflation_sfun_map
+unfolding sfun_defl_def by (rule cast_defl_fun2)
 
 lemma cast_prod_defl:
   "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
@@ -393,21 +393,80 @@
 lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
 by (rule defl_u_def)
 
-subsubsection {* Continuous function space *}
+subsubsection {* Strict function space *}
 
-text {* TODO: Allow argument type to be a predomain. *}
-
-instantiation cfun :: ("domain", "domain") liftdomain
+instantiation sfun :: ("domain", "domain") liftdomain
 begin
 
 definition
-  "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
+  "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb"
+
+definition
+  "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
+
+definition
+  "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+definition
+  "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
 
 definition
-  "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
+  "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
+
+instance
+using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
+proof (rule liftdomain_class_intro)
+  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+    unfolding emb_sfun_def prj_sfun_def
+    using ep_pair_udom [OF sfun_approx]
+    by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
+  show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
+    by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
+qed
+
+end
+
+lemma DEFL_sfun:
+  "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sfun_def)
+
+subsubsection {* Continuous function space *}
+
+text {*
+  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
+*}
 
 definition
-  "defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+  "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
+
+definition
+  "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
+
+lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
+unfolding encode_cfun_def decode_cfun_def
+by (simp add: eta_cfun)
+
+lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff strictify_cancel)
+apply (rule cfun_eqI, case_tac x, simp_all)
+done
+
+instantiation cfun :: (predomain, "domain") liftdomain
+begin
+
+definition
+  "emb = (udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb) oo encode_cfun"
+
+definition
+  "prj = decode_cfun oo (sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx)"
+
+definition
+  "defl (t::('a \<rightarrow> 'b) itself) = sfun_defl\<cdot>DEFL('a u)\<cdot>DEFL('b)"
 
 definition
   "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
@@ -421,19 +480,24 @@
 instance
 using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def
 proof (rule liftdomain_class_intro)
-  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+  have "ep_pair encode_cfun decode_cfun"
+    by (rule ep_pair.intro, simp_all)
+  thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
     unfolding emb_cfun_def prj_cfun_def
-    using ep_pair_udom [OF cfun_approx]
-    by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair_comp)
+    apply (intro ep_pair_sfun_map ep_pair_emb_prj)
+    apply (rule ep_pair_udom [OF sfun_approx])
+    done
   show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
-    unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map)
+    unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_sfun_defl
+    by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
 qed
 
 end
 
 lemma DEFL_cfun:
-  "DEFL('a::domain \<rightarrow> 'b::domain) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+  "DEFL('a::predomain \<rightarrow> 'b::domain) = sfun_defl\<cdot>DEFL('a u)\<cdot>DEFL('b)"
 by (rule defl_cfun_def)
 
 subsubsection {* Cartesian product *}
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Domain.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -237,13 +237,13 @@
 unfolding isodefl_def
 by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
 
-lemma isodefl_cfun:
+lemma isodefl_sfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
+    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_cfun_defl cast_isodefl)
-apply (simp add: emb_cfun_def prj_cfun_def)
-apply (simp add: cfun_map_map cfcomp1)
+apply (simp add: cast_sfun_defl cast_isodefl)
+apply (simp add: emb_sfun_def prj_sfun_def)
+apply (simp add: sfun_map_map isodefl_strict)
 done
 
 lemma isodefl_ssum:
@@ -299,6 +299,23 @@
 apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
 done
 
+lemma encode_cfun_map:
+  "encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
+    = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def)
+apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all)
+done
+
+lemma isodefl_cfun:
+  "isodefl (u_map\<cdot>d1) t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+    isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_sfun_defl cast_isodefl)
+apply (simp add: emb_cfun_def prj_cfun_def encode_cfun_map)
+apply (simp add: sfun_map_map isodefl_strict)
+done
+
 subsection {* Setting up the domain package *}
 
 use "Tools/Domain/domain_isomorphism.ML"
@@ -308,23 +325,24 @@
 setup Domain_Isomorphism.setup
 
 lemmas [domain_defl_simps] =
-  DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
+  DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
   liftdefl_eq LIFTDEFL_prod
 
 lemmas [domain_map_ID] =
-  cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
 
 lemmas [domain_isodefl] =
-  isodefl_u isodefl_cfun isodefl_ssum isodefl_sprod
-  isodefl_cprod isodefl_cprod_u
+  isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
+  isodefl_cfun isodefl_cprod isodefl_cprod_u
 
 lemmas [domain_deflation] =
-  deflation_cfun_map deflation_ssum_map deflation_sprod_map
-  deflation_cprod_map deflation_u_map
+  deflation_cfun_map deflation_sfun_map deflation_ssum_map
+  deflation_sprod_map deflation_cprod_map deflation_u_map
 
 setup {*
   fold Domain_Take_Proofs.add_map_function
     [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
+     (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]),
      (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
      (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
      (@{type_name prod}, @{const_name cprod_map}, [true, true]),
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/IsaMakefile	Wed Nov 17 08:47:58 2010 -0800
@@ -62,6 +62,7 @@
   Porder.thy \
   Powerdomains.thy \
   Product_Cpo.thy \
+  Sfun.thy \
   Sprod.thy \
   Ssum.thy \
   Tr.thy \
@@ -105,7 +106,6 @@
   Library/Defl_Bifinite.thy \
   Library/List_Cpo.thy \
   Library/Stream.thy \
-  Library/Strict_Fun.thy \
   Library/Sum_Cpo.thy \
   Library/HOLCF_Library.thy \
   Library/ROOT.ML
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Library/HOLCF_Library.thy
--- a/src/HOLCF/Library/HOLCF_Library.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Library/HOLCF_Library.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -3,7 +3,6 @@
   Defl_Bifinite
   List_Cpo
   Stream
-  Strict_Fun
   Sum_Cpo
 begin
 
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Library/Strict_Fun.thy
--- a/src/HOLCF/Library/Strict_Fun.thy	Wed Nov 17 06:49:23 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(*  Title:      HOLCF/Library/Strict_Fun.thy
-    Author:     Brian Huffman
-*)
-
-header {* The Strict Function Type *}
-
-theory Strict_Fun
-imports HOLCF
-begin
-
-pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
-  = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
-by simp_all
-
-type_notation (xsymbols)
-  sfun  (infixr "\<rightarrow>!" 0)
-
-text {* TODO: Define nice syntax for abstraction, application. *}
-
-definition
-  sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
-where
-  "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
-
-definition
-  sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
-where
-  "sfun_rep = (\<Lambda> f. Rep_sfun f)"
-
-lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
-  unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
-
-lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
-  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
-
-lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
-  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
-
-lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
-  by (simp add: cfun_eq_iff strictify_conv_if)
-
-lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
-  unfolding sfun_abs_def sfun_rep_def
-  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
-  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
-  apply (simp add: cfun_eq_iff strictify_conv_if)
-  apply (simp add: Rep_sfun [simplified])
-  done
-
-lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
-  unfolding sfun_abs_def sfun_rep_def
-  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
-  apply (simp add: Abs_sfun_inverse)
-  done
-
-lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
-apply default
-apply (rule sfun_abs_sfun_rep)
-apply (simp add: cfun_below_iff strictify_conv_if)
-done
-
-interpretation sfun: ep_pair sfun_rep sfun_abs
-  by (rule ep_pair_sfun)
-
-subsection {* Map functional for strict function space *}
-
-definition
-  sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
-where
-  "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
-
-lemma sfun_map_ID [domain_map_ID]: "sfun_map\<cdot>ID\<cdot>ID = ID"
-  unfolding sfun_map_def
-  by (simp add: cfun_map_ID cfun_eq_iff)
-
-lemma sfun_map_map:
-  assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
-  "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
-    sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>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\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>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\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
-    unfolding sfun_map_def
-    apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel)
-    apply (rule ep_pair.e_inverse)
-    apply (rule ep_pair_cfun_map [OF 1 2])
-    done
-  fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
-    unfolding sfun_map_def
-    apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel)
-    apply (rule ep_pair.e_p_below)
-    apply (rule ep_pair_cfun_map [OF 1 2])
-    done
-qed
-
-lemma deflation_sfun_map [domain_deflation]:
-  assumes 1: "deflation d1"
-  assumes 2: "deflation d2"
-  shows "deflation (sfun_map\<cdot>d1\<cdot>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.e_below_iff [symmetric])
-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\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.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\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
-  from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
-    by (rule finite_deflation_cfun_map)
-  then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
-    by (rule finite_deflation.finite_fixes)
-  moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
-    by (rule inj_onI, simp)
-  ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
-    by (rule finite_vimageI)
-  then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
-    unfolding sfun_map_def sfun.e_eq_iff [symmetric]
-    by (simp add: strictify_cancel
-         deflation_strict `deflation d1` `deflation d2`)
-qed
-
-subsection {* Strict function space is a bifinite domain *}
-
-definition
-  sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
-where
-  "sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma sfun_approx: "approx_chain sfun_approx"
-proof (rule approx_chain.intro)
-  show "chain (\<lambda>i. sfun_approx i)"
-    unfolding sfun_approx_def by simp
-  show "(\<Squnion>i. sfun_approx i) = ID"
-    unfolding sfun_approx_def
-    by (simp add: lub_distribs sfun_map_ID)
-  show "\<And>i. finite_deflation (sfun_approx i)"
-    unfolding sfun_approx_def
-    by (intro finite_deflation_sfun_map finite_deflation_udom_approx)
-qed
-
-definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "sfun_defl = defl_fun2 sfun_approx sfun_map"
-
-lemma cast_sfun_defl:
-  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
-    udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
-unfolding sfun_defl_def
-apply (rule cast_defl_fun2 [OF sfun_approx])
-apply (erule (1) finite_deflation_sfun_map)
-done
-
-instantiation sfun :: ("domain", "domain") liftdomain
-begin
-
-definition
-  "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb"
-
-definition
-  "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
-
-definition
-  "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-definition
-  "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
-  "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
-  "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
-
-instance
-using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
-proof (rule liftdomain_class_intro)
-  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
-    unfolding emb_sfun_def prj_sfun_def
-    using ep_pair_udom [OF sfun_approx]
-    by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
-next
-  show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
-    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
-qed
-
-end
-
-lemma DEFL_sfun [domain_defl_simps]:
-  "DEFL('a \<rightarrow>! 'b) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-by (rule defl_sfun_def)
-
-lemma isodefl_sfun [domain_isodefl]:
-  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_sfun_defl cast_isodefl)
-apply (simp add: emb_sfun_def prj_sfun_def)
-apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
-done
-
-setup {*
-  Domain_Take_Proofs.add_map_function
-    (@{type_name "sfun"}, @{const_name sfun_map}, [true, true])
-*}
-
-end
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Map_Functions.thy
--- a/src/HOLCF/Map_Functions.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Map_Functions.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -380,4 +380,85 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
+subsection {* Map operator for strict function space *}
+
+definition
+  sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
+where
+  "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
+
+lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
+  unfolding sfun_map_def
+  by (simp add: cfun_map_ID cfun_eq_iff)
+
+lemma sfun_map_map:
+  assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
+  "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+    sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>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\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>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\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>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\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>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\<cdot>d1\<cdot>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\<cdot>d1\<cdot>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\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
+  from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+    by (rule finite_deflation_cfun_map)
+  then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+    by (rule finite_deflation.finite_fixes)
+  moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
+    by (rule inj_onI, simp add: sfun_eq_iff)
+  ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
+    by (rule finite_vimageI)
+  then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+    unfolding sfun_map_def sfun_eq_iff
+    by (simp add: strictify_cancel
+         deflation_strict `deflation d1` `deflation d2`)
+qed
+
 end
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Plain_HOLCF.thy
--- a/src/HOLCF/Plain_HOLCF.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Plain_HOLCF.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -5,7 +5,7 @@
 header {* Plain HOLCF *}
 
 theory Plain_HOLCF
-imports Cfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
+imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
 begin
 
 text {*
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Sfun.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Sfun.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -0,0 +1,62 @@
+(*  Title:      HOLCF/Sfun.thy
+    Author:     Brian Huffman
+*)
+
+header {* The Strict Function Type *}
+
+theory Sfun
+imports Cfun
+begin
+
+pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
+  = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
+by simp_all
+
+type_notation (xsymbols)
+  sfun  (infixr "\<rightarrow>!" 0)
+
+text {* TODO: Define nice syntax for abstraction, application. *}
+
+definition
+  sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
+where
+  "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
+
+definition
+  sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
+where
+  "sfun_rep = (\<Lambda> f. Rep_sfun f)"
+
+lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
+  unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
+
+lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
+  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
+
+lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
+  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
+
+lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
+  by (simp add: cfun_eq_iff strictify_conv_if)
+
+lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
+  unfolding sfun_abs_def sfun_rep_def
+  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
+  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
+  apply (simp add: cfun_eq_iff strictify_conv_if)
+  apply (simp add: Rep_sfun [simplified])
+  done
+
+lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
+  unfolding sfun_abs_def sfun_rep_def
+  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
+  apply (simp add: Abs_sfun_inverse)
+  done
+
+lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g"
+by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
+
+lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g"
+by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
+
+end
diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -34,14 +34,14 @@
 where
   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
-    , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
-    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
 
 lemma foo_bar_baz_deflF_beta:
   "foo_bar_baz_deflF\<cdot>a\<cdot>t =
     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
-    , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
-    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
 unfolding foo_bar_baz_deflF_def
 by (simp add: split_def)
 
@@ -68,10 +68,10 @@
   "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>DEFL(tr))"
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 text "The automation for the previous steps will be quite similar to