# Theory Sfun

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

section ‹The Strict Function Type›

theory Sfun
imports Cfun
begin

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

type_notation (ASCII)
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"

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"

lemma sfun_abs_sfun_rep [simp]: "sfun_abs⋅(sfun_rep⋅f) = f"
unfolding sfun_abs_def sfun_rep_def
apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
done

lemma sfun_rep_sfun_abs [simp]: "sfun_rep⋅(sfun_abs⋅f) = strictify⋅f"
unfolding sfun_abs_def sfun_rep_def