Quelle  Sfun.thy   Sprache: Isabelle

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

section ‹The Strict Function Type›

theory Sfun
  imports Cfun
begin

pcpodef ('a::pcpo, 'b::pcpo) 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::pcpo \ 'b::pcpo) \ ('a \! 'b)"
  where "sfun_abs = (\ f. Abs_sfun (strictify\f))"

definition sfun_rep :: "('a::pcpo \! 'b::pcpo) \ 'a \ 'b"
  where "sfun_rep = (\ f. Rep_sfun f)"

lemma sfun_rep_beta: "sfun_rep\f = Rep_sfun f"
  by (simp add: sfun_rep_def 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 \ g \ sfun_rep\f \ sfun_rep\g"
  by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)

end