author  huffman 
Fri, 08 May 2009 16:19:51 0700  
changeset 31076  99fe356cbbc2 
parent 29138  661a8db7e647 
child 35914  91a7311177c4 
permissions  rwrr 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

1 
(* Title: HOLCF/FunCpo.thy 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

3 
*) 
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 
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

6 

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

7 
theory Ffun 
25786  8 
imports Cont 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

10 

18291  11 
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

12 

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

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

15 

25758  16 
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

17 
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

18 

25758  19 
instance .. 
20 
end 

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

21 

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

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

25 
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

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

29 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = 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

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

33 
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

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

36 

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

37 
text {* make the symbol @{text "<<"} accessible for type fun *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

38 

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 
lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

40 
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

41 

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 
lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

43 
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

44 

18291  45 
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

46 

25786  47 
text {* function application is monotone *} 
48 

49 
lemma monofun_app: "monofun (\<lambda>f. f 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

50 
by (rule monofunI, simp add: below_fun_def) 
25786  51 

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

52 
text {* chains of functions yield chains in the po range *} 
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 {* upper bounds of function chains yield upper bound in the po range *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

61 

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

62 
lemma ub2ub_fun: 
26028  63 
"range S < u \<Longrightarrow> range (\<lambda>i. S i x) < u 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

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

65 

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

66 
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

67 

26028  68 
lemma is_lub_lambda: 
69 
assumes f: "\<And>x. range (\<lambda>i. Y i x) << f x" 

70 
shows "range Y << f" 

71 
apply (rule is_lubI) 

72 
apply (rule ub_rangeI) 

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

73 
apply (rule below_fun_ext) 
26028  74 
apply (rule is_ub_lub [OF 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

75 
apply (rule below_fun_ext) 
26028  76 
apply (rule is_lub_lub [OF f]) 
77 
apply (erule ub2ub_fun) 

78 
done 

79 

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

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

81 
"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

82 
\<Longrightarrow> range S << (\<lambda>x. \<Squnion>i. S i x)" 
26028  83 
apply (rule is_lub_lambda) 
84 
apply (rule cpo_lubI) 

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

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

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

87 

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

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

89 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
27413  90 
\<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

91 
by (rule lub_fun [THEN thelubI]) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

92 

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

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

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

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

96 

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

97 
instance "fun" :: (type, cpo) cpo 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

98 
by intro_classes (rule cpo_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

99 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

100 
instance "fun" :: (finite, finite_po) finite_po .. 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

101 

26025  102 
instance "fun" :: (type, discrete_cpo) discrete_cpo 
103 
proof 

104 
fix f g :: "'a \<Rightarrow> 'b" 

105 
show "f \<sqsubseteq> g \<longleftrightarrow> f = 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

106 
unfolding expand_fun_below expand_fun_eq 
26025  107 
by simp 
108 
qed 

109 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

110 
text {* chainfinite function spaces *} 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

111 

c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

112 
lemma maxinch2maxinch_lambda: 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

113 
"(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

114 
unfolding max_in_chain_def expand_fun_eq by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

115 

c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

116 
lemma maxinch_mono: 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

117 
"\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

118 
unfolding max_in_chain_def 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

119 
proof (intro allI impI) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

120 
fix k 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

121 
assume Y: "\<forall>n\<ge>i. Y i = Y n" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

122 
assume ij: "i \<le> j" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

123 
assume jk: "j \<le> k" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

124 
from ij jk have ik: "i \<le> k" by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

125 
from Y ij have Yij: "Y i = Y j" by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

126 
from Y ik have Yik: "Y i = Y k" by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

127 
from Yij Yik show "Y j = Y k" by auto 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

128 
qed 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

129 

c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

130 
instance "fun" :: (finite, chfin) chfin 
25921  131 
proof 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

132 
fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

133 
let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

134 
assume "chain Y" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

135 
hence "\<And>x. chain (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

136 
by (rule ch2ch_fun) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

137 
hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)" 
25921  138 
by (rule chfin) 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

139 
hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

140 
by (rule LeastI_ex) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

141 
hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

142 
by (rule maxinch_mono [OF _ Max_ge], simp_all) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

143 
hence "max_in_chain (Max (range ?n)) Y" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

144 
by (rule maxinch2maxinch_lambda) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

145 
thus "\<exists>n. max_in_chain n Y" .. 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

146 
qed 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

147 

18291  148 
subsection {* Full function space is pointed *} 
17831  149 

150 
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

151 
by (simp add: below_fun_def) 
17831  152 

25786  153 
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" 
17831  154 
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) 
155 
apply (rule minimal_fun [THEN allI]) 

156 
done 

157 

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

158 
instance "fun" :: (type, pcpo) pcpo 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

159 
by intro_classes (rule least_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

160 

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

161 
text {* for compatibility with old HOLCFVersion *} 
17831  162 
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

164 

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

165 
text {* function application is strict in the left argument *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

166 
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

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

168 

25786  169 
text {* 
170 
The following results are about application for functions in @{typ "'a=>'b"} 

171 
*} 

172 

173 
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> 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

174 
by (simp add: below_fun_def) 
25786  175 

176 
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" 

177 
by (rule monofunE) 

178 

179 
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y" 

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

180 
by (rule below_trans [OF monofun_fun_arg monofun_fun_fun]) 
25786  181 

182 
subsection {* Propagation of monotonicity and continuity *} 

183 

184 
text {* the lub of a chain of monotone functions is monotone *} 

185 

186 
lemma monofun_lub_fun: 

187 
"\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> 

188 
\<Longrightarrow> monofun (\<Squnion>i. F i)" 

189 
apply (rule monofunI) 

190 
apply (simp add: thelub_fun) 

25923  191 
apply (rule lub_mono) 
25786  192 
apply (erule ch2ch_fun) 
193 
apply (erule ch2ch_fun) 

194 
apply (simp add: monofunE) 

195 
done 

196 

197 
text {* the lub of a chain of continuous functions is continuous *} 

198 

199 
lemma contlub_lub_fun: 

200 
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)" 

201 
apply (rule contlubI) 

202 
apply (simp add: thelub_fun) 

203 
apply (simp add: cont2contlubE) 

204 
apply (rule ex_lub) 

205 
apply (erule ch2ch_fun) 

206 
apply (simp add: ch2ch_cont) 

207 
done 

208 

209 
lemma cont_lub_fun: 

210 
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" 

211 
apply (rule monocontlub2cont) 

212 
apply (erule monofun_lub_fun) 

213 
apply (simp add: cont2mono) 

214 
apply (erule (1) contlub_lub_fun) 

215 
done 

216 

217 
lemma cont2cont_lub: 

218 
"\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)" 

219 
by (simp add: thelub_fun [symmetric] cont_lub_fun) 

220 

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

222 
apply (rule monofunI) 

223 
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) 

224 
done 

225 

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

227 
apply (rule monocontlub2cont) 

228 
apply (erule cont2mono [THEN mono2mono_fun]) 

229 
apply (rule contlubI) 

230 
apply (simp add: cont2contlubE) 

231 
apply (simp add: thelub_fun ch2ch_cont) 

232 
done 

233 

234 
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} 

235 

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

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

237 
assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f" 
25786  238 
apply (rule monofunI) 
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

239 
apply (rule below_fun_ext) 
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

240 
apply (erule monofunE [OF f]) 
25786  241 
done 
242 

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

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

244 
assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f" 
25786  245 
apply (subgoal_tac "monofun f") 
246 
apply (rule monocontlub2cont) 

247 
apply assumption 

248 
apply (rule contlubI) 

249 
apply (rule ext) 

250 
apply (simp add: thelub_fun ch2ch_monofun) 

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

251 
apply (erule cont2contlubE [OF f]) 
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

252 
apply (simp add: mono2mono_lambda cont2mono f) 
25786  253 
done 
254 

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

256 

257 
lemma contlub_lambda: 

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

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

260 
by (simp add: thelub_fun ch2ch_lambda) 

261 

262 
lemma contlub_abstraction: 

263 
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> 

264 
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" 

265 
apply (rule thelub_fun [symmetric]) 

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

266 
apply (simp add: ch2ch_cont) 
25786  267 
done 
268 

269 
lemma mono2mono_app: 

270 
"\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))" 

271 
apply (rule monofunI) 

272 
apply (simp add: monofun_fun monofunE) 

273 
done 

274 

275 
lemma cont2contlub_app: 

276 
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))" 

277 
apply (rule contlubI) 

278 
apply (subgoal_tac "chain (\<lambda>i. f (Y i))") 

279 
apply (subgoal_tac "chain (\<lambda>i. t (Y i))") 

280 
apply (simp add: cont2contlubE thelub_fun) 

281 
apply (rule diag_lub) 

282 
apply (erule ch2ch_fun) 

283 
apply (drule spec) 

284 
apply (erule (1) ch2ch_cont) 

285 
apply (erule (1) ch2ch_cont) 

286 
apply (erule (1) ch2ch_cont) 

287 
done 

288 

289 
lemma cont2cont_app: 

290 
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))" 

291 
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) 

292 

293 
lemmas cont2cont_app2 = cont2cont_app [rule_format] 

294 

295 
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))" 

296 
by (rule cont2cont_app2 [OF cont_const]) 

297 

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

298 
end 