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