1(*  Title:      HOL/HOLCF/Sfun.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>The Strict Function Type\<close>
6
7theory Sfun
8  imports Cfun
9begin
10
11pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
12  by simp_all
13
14type_notation (ASCII)
15  sfun  (infixr "->!" 0)
16
17text \<open>TODO: Define nice syntax for abstraction, application.\<close>
18
19definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
20  where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
21
22definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
23  where "sfun_rep = (\<Lambda> f. Rep_sfun f)"
24
25lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
26  by (simp add: sfun_rep_def cont_Rep_sfun)
27
28lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
29  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
30
31lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
32  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
33
34lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
35  by (simp add: cfun_eq_iff strictify_conv_if)
36
37lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
38  unfolding sfun_abs_def sfun_rep_def
39  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
40  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
41  apply (simp add: cfun_eq_iff strictify_conv_if)
42  apply (simp add: Rep_sfun [simplified])
43  done
44
45lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
46  unfolding sfun_abs_def sfun_rep_def
47  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
48  apply (simp add: Abs_sfun_inverse)
49  done
50
51lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g"
52  by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
53
54lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g"
55  by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
56
57end
58