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