author | wenzelm |
Sat, 24 Mar 2018 20:51:42 +0100 | |
changeset 67945 | 984c3dc46cc0 |
parent 67312 | 0d25e02759b7 |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Sfun.thy |
40592
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 |
|
62175 | 5 |
section \<open>The Strict Function Type\<close> |
40592
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 |
67312 | 8 |
imports Cfun |
40592
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 |
|
67312 | 11 |
pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}" |
12 |
by simp_all |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
13 |
|
61998 | 14 |
type_notation (ASCII) |
15 |
sfun (infixr "->!" 0) |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
16 |
|
62175 | 17 |
text \<open>TODO: Define nice syntax for abstraction, application.\<close> |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
18 |
|
67312 | 19 |
definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)" |
20 |
where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))" |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
21 |
|
67312 | 22 |
definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b" |
23 |
where "sfun_rep = (\<Lambda> f. Rep_sfun f)" |
|
40592
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 |
lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f" |
67312 | 26 |
by (simp add: sfun_rep_def cont_Rep_sfun) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
27 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
28 |
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
|
29 |
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
|
30 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
34 |
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
|
35 |
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
|
36 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
37 |
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
|
38 |
unfolding sfun_abs_def sfun_rep_def |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
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
|
42 |
apply (simp add: Rep_sfun [simplified]) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
43 |
done |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
44 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
45 |
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
|
46 |
unfolding sfun_abs_def sfun_rep_def |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
47 |
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
|
48 |
apply (simp add: Abs_sfun_inverse) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
49 |
done |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
50 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
51 |
lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g" |
67312 | 52 |
by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
53 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
54 |
lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g" |
67312 | 55 |
by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
56 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff
changeset
|
57 |
end |