src/HOL/HOLCF/Sfun.thy
 author kuncar Fri, 09 Dec 2011 18:07:04 +0100 changeset 45802 b16f976db515 parent 42151 4da4fc77664b child 49759 ecf1d5d87e5e permissions -rw-r--r--
Quotient_Info stores only relation maps
```
(*  Title:      HOL/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"

lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>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\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
unfolding sfun_abs_def sfun_rep_def