1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Sfun.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,62 @@
     1.4 +(*  Title:      HOLCF/Sfun.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* The Strict Function Type *}
     1.9 +
    1.10 +theory Sfun
    1.11 +imports Cfun
    1.12 +begin
    1.13 +
    1.14 +pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
    1.15 +  = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    1.16 +by simp_all
    1.17 +
    1.18 +type_notation (xsymbols)
    1.19 +  sfun  (infixr "\<rightarrow>!" 0)
    1.20 +
    1.21 +text {* TODO: Define nice syntax for abstraction, application. *}
    1.22 +
    1.23 +definition
    1.24 +  sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
    1.25 +where
    1.26 +  "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
    1.27 +
    1.28 +definition
    1.29 +  sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
    1.30 +where
    1.31 +  "sfun_rep = (\<Lambda> f. Rep_sfun f)"
    1.32 +
    1.33 +lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
    1.34 +  unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
    1.35 +
    1.36 +lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
    1.37 +  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
    1.38 +
    1.39 +lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
    1.40 +  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
    1.41 +
    1.42 +lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
    1.43 +  by (simp add: cfun_eq_iff strictify_conv_if)
    1.44 +
    1.45 +lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
    1.46 +  unfolding sfun_abs_def sfun_rep_def
    1.47 +  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    1.48 +  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
    1.49 +  apply (simp add: cfun_eq_iff strictify_conv_if)
    1.50 +  apply (simp add: Rep_sfun [simplified])
    1.51 +  done
    1.52 +
    1.53 +lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
    1.54 +  unfolding sfun_abs_def sfun_rep_def
    1.55 +  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    1.56 +  apply (simp add: Abs_sfun_inverse)
    1.57 +  done
    1.58 +
    1.59 +lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g"
    1.60 +by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
    1.61 +
    1.62 +lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g"
    1.63 +by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
    1.64 +
    1.65 +end