author  wenzelm 
Tue, 29 Mar 2011 17:47:11 +0200  
changeset 42151  4da4fc77664b 
parent 40774  0437dbc127b3 
child 49759  ecf1d5d87e5e 
permissions  rwrr 
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 

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 