author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Fun_Cpo.thy 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

2 
Author: Franz Regensburger 
40001  3 
Author: Brian Huffman 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

4 
*) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

5 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

6 
header {* Class instances for the full function space *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

7 

40001  8 
theory Fun_Cpo 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

9 
imports Adm 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

10 
begin 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

11 

18291  12 
subsection {* Full function space is a partial order *} 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

13 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

14 
instantiation "fun" :: (type, below) below 
25758  15 
begin 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

16 

25758  17 
definition 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

18 
below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

19 

25758  20 
instance .. 
21 
end 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

22 

25758  23 
instance "fun" :: (type, po) po 
24 
proof 

25 
fix f :: "'a \<Rightarrow> 'b" 

26 
show "f \<sqsubseteq> f" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

27 
by (simp add: below_fun_def) 
25758  28 
next 
29 
fix f g :: "'a \<Rightarrow> 'b" 

30 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39199
diff
changeset

31 
by (simp add: below_fun_def fun_eq_iff below_antisym) 
25758  32 
next 
33 
fix f g h :: "'a \<Rightarrow> 'b" 

34 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

35 
unfolding below_fun_def by (fast elim: below_trans) 
25758  36 
qed 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

37 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
40001
diff
changeset

38 
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

39 
by (simp add: below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

40 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
40001
diff
changeset

41 
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

42 
by (simp add: below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

43 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

44 
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

45 
by (simp add: below_fun_def) 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

46 

18291  47 
subsection {* Full function space is chain complete *} 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

48 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

49 
text {* Properties of chains of functions. *} 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

50 

b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

51 
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

52 
unfolding chain_def fun_below_iff by auto 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

53 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

54 
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

55 
by (simp add: chain_def below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

56 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17831
diff
changeset

57 
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

58 
by (simp add: chain_def below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

59 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

60 
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

61 

26028  62 
lemma is_lub_lambda: 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

63 
"(\<And>x. range (\<lambda>i. Y i x) << f x) \<Longrightarrow> range Y << f" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

64 
unfolding is_lub_def is_ub_def below_fun_def by simp 
26028  65 

41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

66 
lemma is_lub_fun: 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

67 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

68 
\<Longrightarrow> range S << (\<lambda>x. \<Squnion>i. S i x)" 
26028  69 
apply (rule is_lub_lambda) 
70 
apply (rule cpo_lubI) 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

71 
apply (erule ch2ch_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

72 
done 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

73 

41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

74 
lemma lub_fun: 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

75 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
27413  76 
\<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)" 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

77 
by (rule is_lub_fun [THEN lub_eqI]) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

78 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset

79 
instance "fun" :: (type, cpo) cpo 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

80 
by intro_classes (rule exI, erule is_lub_fun) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

81 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

82 
instance "fun" :: (type, discrete_cpo) discrete_cpo 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

83 
proof 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

84 
fix f g :: "'a \<Rightarrow> 'b" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

85 
show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

86 
unfolding fun_below_iff fun_eq_iff 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

87 
by simp 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

88 
qed 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

89 

18291  90 
subsection {* Full function space is pointed *} 
17831  91 

92 
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

93 
by (simp add: below_fun_def) 
17831  94 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

95 
instance "fun" :: (type, pcpo) pcpo 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

96 
by default (fast intro: minimal_fun) 
17831  97 

98 
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)" 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41032
diff
changeset

99 
by (rule minimal_fun [THEN bottomI, symmetric]) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

100 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

101 
lemma app_strict [simp]: "\<bottom> x = \<bottom>" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

102 
by (simp add: inst_fun_pcpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

103 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

104 
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41032
diff
changeset

105 
by (rule bottomI, rule minimal_fun) 
25786  106 

107 
subsection {* Propagation of monotonicity and continuity *} 

108 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

109 
text {* The lub of a chain of monotone functions is monotone. *} 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

110 

b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

111 
lemma adm_monofun: "adm monofun" 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

112 
by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono) 
25786  113 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

114 
text {* The lub of a chain of continuous functions is continuous. *} 
25786  115 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

116 
lemma adm_cont: "adm cont" 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

117 
by (rule admI, simp add: lub_fun fun_chain_iff) 
25786  118 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

119 
text {* Function application preserves monotonicity and continuity. *} 
25786  120 

121 
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

122 
by (simp add: monofun_def fun_below_iff) 
25786  123 

124 
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" 

35914  125 
apply (rule contI2) 
25786  126 
apply (erule cont2mono [THEN mono2mono_fun]) 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

127 
apply (simp add: cont2contlubE lub_fun ch2ch_cont) 
25786  128 
done 
129 

40622
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset

130 
lemma cont_fun: "cont (\<lambda>f. f x)" 
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset

131 
using cont_id by (rule cont2cont_fun) 
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset

132 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

133 
text {* 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

134 
Lambda abstraction preserves monotonicity and continuity. 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

135 
(Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.) 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

136 
*} 
25786  137 

26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

138 
lemma mono2mono_lambda: 
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

139 
assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f" 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

140 
using f by (simp add: monofun_def fun_below_iff) 
25786  141 

26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

142 
lemma cont2cont_lambda [simp]: 
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

143 
assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f" 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

144 
by (rule contI, rule is_lub_lambda, rule contE [OF f]) 
25786  145 

146 
text {* What D.A.Schmidt calls continuity of abstraction; never used here *} 

147 

148 
lemma contlub_lambda: 

149 
"(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) 

150 
\<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" 

41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

151 
by (simp add: lub_fun ch2ch_lambda) 
25786  152 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

153 
end 