author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45294  3c5d3d286055 
child 57945  cacb00a569e0 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Cont.thy 
1479  2 
Author: Franz Regensburger 
35794  3 
Author: Brian Huffman 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

4 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

5 

15577  6 
header {* Continuity and monotonicity *} 
7 

8 
theory Cont 

25786  9 
imports Pcpo 
15577  10 
begin 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

11 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

12 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

13 
Now we change the default class! Form now on all untyped type variables are 
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2838
diff
changeset

14 
of default class po 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

15 
*} 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

16 

36452  17 
default_sort po 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

18 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

19 
subsection {* Definitions *} 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

20 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset

21 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset

22 
monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  "monotonicity" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset

23 
"monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

24 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset

25 
definition 
35914  26 
cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" 
27 
where 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset

28 
"cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) << f (\<Squnion>i. Y i))" 
15565  29 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

30 
lemma contI: 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

31 
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) << f (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> cont f" 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

32 
by (simp add: cont_def) 
15565  33 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

34 
lemma contE: 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

35 
"\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) << f (\<Squnion>i. Y i)" 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

36 
by (simp add: cont_def) 
15565  37 

38 
lemma monofunI: 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

39 
"\<lbrakk>\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y\<rbrakk> \<Longrightarrow> monofun f" 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

40 
by (simp add: monofun_def) 
15565  41 

42 
lemma monofunE: 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

43 
"\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

44 
by (simp add: monofun_def) 
15565  45 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

46 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35794
diff
changeset

47 
subsection {* Equivalence of alternate definition *} 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

48 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

49 
text {* monotone functions map chains to chains *} 
15565  50 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

51 
lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))" 
15565  52 
apply (rule chainI) 
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

53 
apply (erule monofunE) 
15565  54 
apply (erule chainE) 
55 
done 

56 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

57 
text {* monotone functions map upper bound to upper bounds *} 
15565  58 

59 
lemma ub2ub_monofun: 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

60 
"\<lbrakk>monofun f; range Y < u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) < f u" 
15565  61 
apply (rule ub_rangeI) 
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

62 
apply (erule monofunE) 
15565  63 
apply (erule ub_rangeD) 
64 
done 

65 

35914  66 
text {* a lemma about binary chains *} 
15565  67 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

68 
lemma binchain_cont: 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

69 
"\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) << f y" 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

70 
apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y") 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

71 
apply (erule subst) 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

72 
apply (erule contE) 
15565  73 
apply (erule bin_chain) 
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

74 
apply (rule_tac f=f in arg_cong) 
40771  75 
apply (erule is_lub_bin_chain [THEN lub_eqI]) 
15565  76 
done 
77 

35914  78 
text {* continuity implies monotonicity *} 
15565  79 

16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

80 
lemma cont2mono: "cont f \<Longrightarrow> monofun f" 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

81 
apply (rule monofunI) 
18088  82 
apply (drule (1) binchain_cont) 
40771  83 
apply (drule_tac i=0 in is_lub_rangeD1) 
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

84 
apply simp 
15565  85 
done 
86 

29532  87 
lemmas cont2monofunE = cont2mono [THEN monofunE] 
88 

16737  89 
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] 
90 

35914  91 
text {* continuity implies preservation of lubs *} 
15565  92 

35914  93 
lemma cont2contlubE: 
94 
"\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))" 

40771  95 
apply (rule lub_eqI [symmetric]) 
18088  96 
apply (erule (1) contE) 
15565  97 
done 
98 

25896  99 
lemma contI2: 
40736  100 
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo" 
25896  101 
assumes mono: "monofun f" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

102 
assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> 
27413  103 
\<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" 
25896  104 
shows "cont f" 
40736  105 
proof (rule contI) 
106 
fix Y :: "nat \<Rightarrow> 'a" 

107 
assume Y: "chain Y" 

108 
with mono have fY: "chain (\<lambda>i. f (Y i))" 

109 
by (rule ch2ch_monofun) 

110 
have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)" 

111 
apply (rule below_antisym) 

112 
apply (rule lub_below [OF fY]) 

113 
apply (rule monofunE [OF mono]) 

114 
apply (rule is_ub_thelub [OF Y]) 

115 
apply (rule below [OF Y fY]) 

116 
done 

117 
with fY show "range (\<lambda>i. f (Y i)) << f (\<Squnion>i. Y i)" 

118 
by (rule thelubE) 

119 
qed 

25896  120 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset

121 
subsection {* Collection of continuity rules *} 
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

122 

9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

123 
ML {* 
31902  124 
structure Cont2ContData = Named_Thms 
125 
( 

45294  126 
val name = @{binding cont2cont} 
31902  127 
val description = "continuity intro rule" 
128 
) 

29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

129 
*} 
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

130 

31030  131 
setup Cont2ContData.setup 
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

132 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

133 
subsection {* Continuity of basic functions *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

134 

645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

135 
text {* The identity function is continuous *} 
15565  136 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset

137 
lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)" 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

138 
apply (rule contI) 
26027  139 
apply (erule cpo_lubI) 
15565  140 
done 
141 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

142 
text {* constant functions are continuous *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

143 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset

144 
lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)" 
40771  145 
using is_lub_const by (rule contI) 
15565  146 

29532  147 
text {* application of functions is continuous *} 
148 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

149 
lemma cont_apply: 
29532  150 
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b" 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

151 
assumes 1: "cont (\<lambda>x. t x)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

152 
assumes 2: "\<And>x. cont (\<lambda>y. f x y)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

153 
assumes 3: "\<And>y. cont (\<lambda>x. f x y)" 
29532  154 
shows "cont (\<lambda>x. (f x) (t x))" 
35914  155 
proof (rule contI2 [OF monofunI]) 
29532  156 
fix x y :: "'a" assume "x \<sqsubseteq> y" 
157 
then show "f x (t x) \<sqsubseteq> f y (t y)" 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

158 
by (auto intro: cont2monofunE [OF 1] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

159 
cont2monofunE [OF 2] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

160 
cont2monofunE [OF 3] 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

161 
below_trans) 
29532  162 
next 
163 
fix Y :: "nat \<Rightarrow> 'a" assume "chain Y" 

35914  164 
then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) \<sqsubseteq> (\<Squnion>i. f (Y i) (t (Y i)))" 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

165 
by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

166 
cont2contlubE [OF 2] ch2ch_cont [OF 2] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

167 
cont2contlubE [OF 3] ch2ch_cont [OF 3] 
35914  168 
diag_lub below_refl) 
29532  169 
qed 
170 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

171 
lemma cont_compose: 
29532  172 
"\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))" 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset

173 
by (rule cont_apply [OF _ _ cont_const]) 
29532  174 

40004
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

175 
text {* Least upper bounds preserve continuity *} 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

176 

9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

177 
lemma cont2cont_lub [simp]: 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

178 
assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)" 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

179 
shows "cont (\<lambda>x. \<Squnion>i. F i x)" 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

180 
apply (rule contI2) 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

181 
apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain) 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

182 
apply (simp add: cont2contlubE [OF cont]) 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

183 
apply (simp add: diag_lub ch2ch_cont [OF cont] chain) 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

184 
done 
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset

185 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

186 
text {* ifthenelse is continuous *} 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

187 

37099  188 
lemma cont_if [simp, cont2cont]: 
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26027
diff
changeset

189 
"\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

190 
by (induct b) simp_all 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

191 

645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

192 
subsection {* Finite chains and flat pcpos *} 
15565  193 

40010  194 
text {* Monotone functions map finite chains to finite chains. *} 
15565  195 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

196 
lemma monofun_finch2finch: 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

197 
"\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))" 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

198 
apply (unfold finite_chain_def) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

199 
apply (simp add: ch2ch_monofun) 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

200 
apply (force simp add: max_in_chain_def) 
15565  201 
done 
202 

40010  203 
text {* The same holds for continuous functions. *} 
15565  204 

16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

205 
lemma cont_finch2finch: 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

206 
"\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))" 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

207 
by (rule cont2mono [THEN monofun_finch2finch]) 
15565  208 

40010  209 
text {* All monotone functions with chainfinite domain are continuous. *} 
210 

25825  211 
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)" 
35914  212 
apply (erule contI2) 
15565  213 
apply (frule chfin2finch) 
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

214 
apply (clarsimp simp add: finite_chain_def) 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

215 
apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))") 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

216 
apply (simp add: maxinch_is_thelub ch2ch_monofun) 
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset

217 
apply (force simp add: max_in_chain_def) 
15565  218 
done 
219 

40010  220 
text {* All strict functions with flat domain are continuous. *} 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

221 

645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

222 
lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)" 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

223 
apply (rule monofunI) 
25920  224 
apply (drule ax_flat) 
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

225 
apply auto 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

226 
done 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

227 

645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

228 
lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)" 
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset

229 
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) 
15565  230 

40010  231 
text {* All functions with discrete domain are continuous. *} 
26024  232 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset

233 
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)" 
26024  234 
apply (rule contI) 
235 
apply (drule discrete_chain_const, clarify) 

40771  236 
apply (simp add: is_lub_const) 
26024  237 
done 
238 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

239 
end 