author | haftmann |
Thu, 18 Nov 2010 17:01:15 +0100 | |
changeset 40602 | 91e583511113 |
parent 40010 | d7fdd84b959f |
child 40736 | 72857de90621 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Cont.thy |
1479 | 2 |
Author: Franz Regensburger |
35794 | 3 |
Author: Brian Huffman |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order 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 Higher-Order 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 Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
36452 | 17 |
default_sort po |
243
c22b85994e17
Franz Regensburger's Higher-Order 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 Higher-Order 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 Higher-Order 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) |
15565 | 75 |
apply (erule lub_bin_chain [THEN thelubI]) |
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) |
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
|
83 |
apply (drule_tac i=0 in is_ub_lub) |
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))" |
|
15565 | 95 |
apply (rule thelubI [symmetric]) |
18088 | 96 |
apply (erule (1) contE) |
15565 | 97 |
done |
98 |
||
25896 | 99 |
lemma contI2: |
100 |
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
|
101 |
assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> |
27413 | 102 |
\<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" |
25896 | 103 |
shows "cont f" |
35914 | 104 |
apply (rule contI) |
105 |
apply (rule thelubE) |
|
106 |
apply (erule ch2ch_monofun [OF mono]) |
|
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
|
107 |
apply (rule below_antisym) |
25896 | 108 |
apply (rule is_lub_thelub) |
109 |
apply (erule ch2ch_monofun [OF mono]) |
|
110 |
apply (rule ub2ub_monofun [OF mono]) |
|
111 |
apply (rule is_lubD1) |
|
26027 | 112 |
apply (erule cpo_lubI) |
35914 | 113 |
apply (rule below, assumption) |
114 |
apply (erule ch2ch_monofun [OF mono]) |
|
25896 | 115 |
done |
116 |
||
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset
|
117 |
subsection {* Collection of continuity rules *} |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
118 |
|
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
119 |
ML {* |
31902 | 120 |
structure Cont2ContData = Named_Thms |
121 |
( |
|
122 |
val name = "cont2cont" |
|
123 |
val description = "continuity intro rule" |
|
124 |
) |
|
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
125 |
*} |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
126 |
|
31030 | 127 |
setup Cont2ContData.setup |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
128 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
129 |
subsection {* Continuity of basic functions *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
130 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
131 |
text {* The identity function is continuous *} |
15565 | 132 |
|
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset
|
133 |
lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)" |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
134 |
apply (rule contI) |
26027 | 135 |
apply (erule cpo_lubI) |
15565 | 136 |
done |
137 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
138 |
text {* constant functions are continuous *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
139 |
|
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset
|
140 |
lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)" |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
141 |
apply (rule contI) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
142 |
apply (rule lub_const) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
143 |
done |
15565 | 144 |
|
29532 | 145 |
text {* application of functions is continuous *} |
146 |
||
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset
|
147 |
lemma cont_apply: |
29532 | 148 |
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
|
149 |
assumes 1: "cont (\<lambda>x. t x)" |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset
|
150 |
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
|
151 |
assumes 3: "\<And>y. cont (\<lambda>x. f x y)" |
29532 | 152 |
shows "cont (\<lambda>x. (f x) (t x))" |
35914 | 153 |
proof (rule contI2 [OF monofunI]) |
29532 | 154 |
fix x y :: "'a" assume "x \<sqsubseteq> y" |
155 |
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
|
156 |
by (auto intro: cont2monofunE [OF 1] |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset
|
157 |
cont2monofunE [OF 2] |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset
|
158 |
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
|
159 |
below_trans) |
29532 | 160 |
next |
161 |
fix Y :: "nat \<Rightarrow> 'a" assume "chain Y" |
|
35914 | 162 |
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
|
163 |
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
|
164 |
cont2contlubE [OF 2] ch2ch_cont [OF 2] |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset
|
165 |
cont2contlubE [OF 3] ch2ch_cont [OF 3] |
35914 | 166 |
diag_lub below_refl) |
29532 | 167 |
qed |
168 |
||
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
31030
diff
changeset
|
169 |
lemma cont_compose: |
29532 | 170 |
"\<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
|
171 |
by (rule cont_apply [OF _ _ cont_const]) |
29532 | 172 |
|
40004
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
173 |
text {* Least upper bounds preserve continuity *} |
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
174 |
|
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
175 |
lemma cont2cont_lub [simp]: |
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
176 |
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
|
177 |
shows "cont (\<lambda>x. \<Squnion>i. F i x)" |
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
178 |
apply (rule contI2) |
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
179 |
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
|
180 |
apply (simp add: cont2contlubE [OF cont]) |
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
181 |
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
|
182 |
done |
9f6ed6840e8d
reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents:
37099
diff
changeset
|
183 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
184 |
text {* if-then-else is continuous *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
185 |
|
37099 | 186 |
lemma cont_if [simp, cont2cont]: |
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26027
diff
changeset
|
187 |
"\<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
|
188 |
by (induct b) simp_all |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
189 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
190 |
subsection {* Finite chains and flat pcpos *} |
15565 | 191 |
|
40010 | 192 |
text {* Monotone functions map finite chains to finite chains. *} |
15565 | 193 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
194 |
lemma monofun_finch2finch: |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
195 |
"\<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
|
196 |
apply (unfold finite_chain_def) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
197 |
apply (simp add: ch2ch_monofun) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
198 |
apply (force simp add: max_in_chain_def) |
15565 | 199 |
done |
200 |
||
40010 | 201 |
text {* The same holds for continuous functions. *} |
15565 | 202 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
203 |
lemma cont_finch2finch: |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
204 |
"\<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
|
205 |
by (rule cont2mono [THEN monofun_finch2finch]) |
15565 | 206 |
|
40010 | 207 |
text {* All monotone functions with chain-finite domain are continuous. *} |
208 |
||
25825 | 209 |
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)" |
35914 | 210 |
apply (erule contI2) |
15565 | 211 |
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
|
212 |
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
|
213 |
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
|
214 |
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
|
215 |
apply (force simp add: max_in_chain_def) |
15565 | 216 |
done |
217 |
||
40010 | 218 |
text {* All strict functions with flat domain are continuous. *} |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
219 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
220 |
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
|
221 |
apply (rule monofunI) |
25920 | 222 |
apply (drule ax_flat) |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
223 |
apply auto |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
224 |
done |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
225 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
226 |
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
|
227 |
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) |
15565 | 228 |
|
40010 | 229 |
text {* All functions with discrete domain are continuous. *} |
26024 | 230 |
|
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36658
diff
changeset
|
231 |
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)" |
26024 | 232 |
apply (rule contI) |
233 |
apply (drule discrete_chain_const, clarify) |
|
234 |
apply (simp add: lub_const) |
|
235 |
done |
|
236 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
237 |
end |