Theory Sfun

theory Sfun
imports Cfun
(*  Title:      HOL/HOLCF/Sfun.thy
    Author:     Brian Huffman
*)

header {* The Strict Function Type *}

theory Sfun
imports Cfun
begin

pcpodef ('a, 'b) sfun (infixr "->!" 0)
  = "{f :: 'a -> 'b. f·⊥ = ⊥}"
by simp_all

type_notation (xsymbols)
  sfun  (infixr "->!" 0)

text {* TODO: Define nice syntax for abstraction, application. *}

definition
  sfun_abs :: "('a -> 'b) -> ('a ->! 'b)"
where
  "sfun_abs = (Λ f. Abs_sfun (strictify·f))"

definition
  sfun_rep :: "('a ->! 'b) -> 'a -> 'b"
where
  "sfun_rep = (Λ f. Rep_sfun f)"

lemma sfun_rep_beta: "sfun_rep·f = Rep_sfun f"
  unfolding sfun_rep_def by (simp add: cont_Rep_sfun)

lemma sfun_rep_strict1 [simp]: "sfun_rep·⊥ = ⊥"
  unfolding sfun_rep_beta by (rule Rep_sfun_strict)

lemma sfun_rep_strict2 [simp]: "sfun_rep·f·⊥ = ⊥"
  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])

lemma strictify_cancel: "f·⊥ = ⊥ ==> strictify·f = f"
  by (simp add: cfun_eq_iff strictify_conv_if)

lemma sfun_abs_sfun_rep [simp]: "sfun_abs·(sfun_rep·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·(sfun_abs·f) = strictify·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 <-> sfun_rep·f = sfun_rep·g"
by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)

lemma sfun_below_iff: "f \<sqsubseteq> g <-> sfun_rep·f \<sqsubseteq> sfun_rep·g"
by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)

end