author | huffman |
Thu, 03 Jan 2008 23:58:27 +0100 | |
changeset 25825 | 94c075b912ff |
parent 25786 | 6b3c79acac1f |
child 25896 | b2d2f1ae5808 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Cont.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
|
16070
4a83dd540b88
removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents:
16053
diff
changeset
|
5 |
Results about continuity and monotonicity. |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
|
15577 | 8 |
header {* Continuity and monotonicity *} |
9 |
||
10 |
theory Cont |
|
25786 | 11 |
imports Pcpo |
15577 | 12 |
begin |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
14 |
text {* |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
15 |
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
|
16 |
of default class po |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
17 |
*} |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
|
15565 | 19 |
defaultsort po |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
21 |
subsection {* Definitions *} |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
23 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
24 |
monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
25 |
"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
|
26 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
27 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
28 |
contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
29 |
"contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
31 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
32 |
cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
33 |
"cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))" |
15565 | 34 |
|
35 |
lemma contlubI: |
|
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
|
36 |
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub 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
|
37 |
by (simp add: contlub_def) |
15565 | 38 |
|
39 |
lemma contlubE: |
|
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
|
40 |
"\<lbrakk>contlub f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>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
|
41 |
by (simp add: contlub_def) |
15565 | 42 |
|
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 |
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
|
44 |
"\<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
|
45 |
by (simp add: cont_def) |
15565 | 46 |
|
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
|
47 |
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
|
48 |
"\<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
|
49 |
by (simp add: cont_def) |
15565 | 50 |
|
51 |
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
|
52 |
"\<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
|
53 |
by (simp add: monofun_def) |
15565 | 54 |
|
55 |
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
|
56 |
"\<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
|
57 |
by (simp add: monofun_def) |
15565 | 58 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
59 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
60 |
subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
61 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
62 |
text {* monotone functions map chains to chains *} |
15565 | 63 |
|
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
|
64 |
lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))" |
15565 | 65 |
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
|
66 |
apply (erule monofunE) |
15565 | 67 |
apply (erule chainE) |
68 |
done |
|
69 |
||
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
70 |
text {* monotone functions map upper bound to upper bounds *} |
15565 | 71 |
|
72 |
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
|
73 |
"\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u" |
15565 | 74 |
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
|
75 |
apply (erule monofunE) |
15565 | 76 |
apply (erule ub_rangeD) |
77 |
done |
|
78 |
||
25783 | 79 |
lemma ub2ub_monofun': |
80 |
"\<lbrakk>monofun f; S <| u\<rbrakk> \<Longrightarrow> f ` S <| f u" |
|
81 |
apply (rule ub_imageI) |
|
82 |
apply (erule monofunE) |
|
83 |
apply (erule (1) is_ubD) |
|
84 |
done |
|
85 |
||
25779 | 86 |
text {* monotone functions map directed sets to directed sets *} |
87 |
||
88 |
lemma dir2dir_monofun: |
|
89 |
assumes f: "monofun f" |
|
90 |
assumes S: "directed S" |
|
91 |
shows "directed (f ` S)" |
|
92 |
proof (rule directedI) |
|
93 |
from directedD1 [OF S] |
|
94 |
obtain x where "x \<in> S" .. |
|
95 |
hence "f x \<in> f ` S" by simp |
|
96 |
thus "\<exists>x. x \<in> f ` S" .. |
|
97 |
next |
|
98 |
fix x assume "x \<in> f ` S" |
|
99 |
then obtain a where x: "x = f a" and a: "a \<in> S" .. |
|
100 |
fix y assume "y \<in> f ` S" |
|
101 |
then obtain b where y: "y = f b" and b: "b \<in> S" .. |
|
102 |
from directedD2 [OF S a b] |
|
103 |
obtain c where "c \<in> S" and "a \<sqsubseteq> c \<and> b \<sqsubseteq> c" .. |
|
104 |
hence "f c \<in> f ` S" and "x \<sqsubseteq> f c \<and> y \<sqsubseteq> f c" |
|
105 |
using monofunE [OF f] x y by simp_all |
|
106 |
thus "\<exists>z\<in>f ` S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" .. |
|
107 |
qed |
|
108 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
109 |
text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *} |
15565 | 110 |
|
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
|
111 |
lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<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
|
112 |
apply (rule contI) |
15565 | 113 |
apply (rule thelubE) |
18088 | 114 |
apply (erule (1) ch2ch_monofun) |
115 |
apply (erule (1) contlubE [symmetric]) |
|
15565 | 116 |
done |
117 |
||
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
118 |
text {* first a lemma about binary chains *} |
15565 | 119 |
|
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
|
120 |
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
|
121 |
"\<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
|
122 |
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
|
123 |
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
|
124 |
apply (erule contE) |
15565 | 125 |
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
|
126 |
apply (rule_tac f=f in arg_cong) |
15565 | 127 |
apply (erule lub_bin_chain [THEN thelubI]) |
128 |
done |
|
129 |
||
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
|
130 |
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub 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
|
131 |
text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *} |
15565 | 132 |
|
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
|
133 |
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
|
134 |
apply (rule monofunI) |
18088 | 135 |
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
|
136 |
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
|
137 |
apply simp |
15565 | 138 |
done |
139 |
||
16737 | 140 |
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] |
141 |
||
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
|
142 |
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub 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
|
143 |
text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *} |
15565 | 144 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
145 |
lemma cont2contlub: "cont f \<Longrightarrow> contlub f" |
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
|
146 |
apply (rule contlubI) |
15565 | 147 |
apply (rule thelubI [symmetric]) |
18088 | 148 |
apply (erule (1) contE) |
15565 | 149 |
done |
150 |
||
16737 | 151 |
lemmas cont2contlubE = cont2contlub [THEN contlubE] |
152 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
153 |
subsection {* Continuity of basic functions *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
154 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
155 |
text {* The identity function is continuous *} |
15565 | 156 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
157 |
lemma cont_id: "cont (\<lambda>x. x)" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
158 |
apply (rule contI) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
159 |
apply (erule thelubE) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
160 |
apply (rule refl) |
15565 | 161 |
done |
162 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
163 |
text {* constant functions are continuous *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
164 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
165 |
lemma cont_const: "cont (\<lambda>x. c)" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
166 |
apply (rule contI) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
167 |
apply (rule lub_const) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
168 |
done |
15565 | 169 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
170 |
text {* if-then-else is continuous *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
171 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
172 |
lemma cont_if: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
173 |
by (induct b) simp_all |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
174 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
175 |
subsection {* Finite chains and flat pcpos *} |
15565 | 176 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
177 |
text {* monotone functions map finite chains to finite chains *} |
15565 | 178 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
179 |
lemma monofun_finch2finch: |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
180 |
"\<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
|
181 |
apply (unfold finite_chain_def) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
182 |
apply (simp add: ch2ch_monofun) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
183 |
apply (force simp add: max_in_chain_def) |
15565 | 184 |
done |
185 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
186 |
text {* The same holds for continuous functions *} |
15565 | 187 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
188 |
lemma cont_finch2finch: |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
189 |
"\<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
|
190 |
by (rule cont2mono [THEN monofun_finch2finch]) |
15565 | 191 |
|
25825 | 192 |
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)" |
15565 | 193 |
apply (rule monocontlub2cont) |
194 |
apply assumption |
|
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
|
195 |
apply (rule contlubI) |
15565 | 196 |
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
|
197 |
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
|
198 |
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
|
199 |
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
|
200 |
apply (force simp add: max_in_chain_def) |
15565 | 201 |
done |
202 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
203 |
text {* some properties of flat *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
204 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
205 |
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
|
206 |
apply (rule monofunI) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
207 |
apply (drule ax_flat [rule_format]) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
208 |
apply auto |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
209 |
done |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
210 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
211 |
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
|
212 |
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) |
15565 | 213 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
214 |
end |