author | wenzelm |
Mon, 25 Apr 2016 16:09:26 +0200 | |
changeset 63040 | eb4ddd18d635 |
parent 62175 | 8ffc4d0e652d |
child 67312 | 0d25e02759b7 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Up.thy |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
2 |
Author: Franz Regensburger |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
3 |
Author: Brian Huffman |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
4 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
|
62175 | 6 |
section \<open>The type of lifted values\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
|
15577 | 8 |
theory Up |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
9 |
imports Cfun |
15577 | 10 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
|
36452 | 12 |
default_sort cpo |
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
13 |
|
62175 | 14 |
subsection \<open>Definition of new type for lifting\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
|
61998 | 16 |
datatype 'a u ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a |
18290 | 17 |
|
34941 | 18 |
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where |
19 |
"Ifup f Ibottom = \<bottom>" |
|
20 |
| "Ifup f (Iup x) = f\<cdot>x" |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
|
62175 | 22 |
subsection \<open>Ordering on lifted cpo\<close> |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
23 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
24 |
instantiation u :: (cpo) below |
25787 | 25 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
|
25787 | 27 |
definition |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
28 |
below_up_def: |
16753 | 29 |
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow> |
30 |
(case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))" |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
|
25787 | 32 |
instance .. |
33 |
end |
|
34 |
||
16753 | 35 |
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
36 |
by (simp add: below_up_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
|
41182 | 38 |
lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
39 |
by (simp add: below_up_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
41 |
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)" |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
42 |
by (simp add: below_up_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
|
62175 | 44 |
subsection \<open>Lifted cpo is a partial order\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
46 |
instance u :: (cpo) po |
25787 | 47 |
proof |
48 |
fix x :: "'a u" |
|
49 |
show "x \<sqsubseteq> x" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
50 |
unfolding below_up_def by (simp split: u.split) |
25787 | 51 |
next |
52 |
fix x y :: "'a u" |
|
53 |
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
54 |
unfolding below_up_def |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
55 |
by (auto split: u.split_asm intro: below_antisym) |
25787 | 56 |
next |
57 |
fix x y z :: "'a u" |
|
58 |
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
59 |
unfolding below_up_def |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
60 |
by (auto split: u.split_asm intro: below_trans) |
25787 | 61 |
qed |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
62 |
|
62175 | 63 |
subsection \<open>Lifted cpo is a cpo\<close> |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
64 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
65 |
lemma is_lub_Iup: |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
66 |
"range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x" |
40084 | 67 |
unfolding is_lub_def is_ub_def ball_simps |
68 |
by (auto simp add: below_up_def split: u.split) |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
69 |
|
17838 | 70 |
lemma up_chain_lemma: |
40084 | 71 |
assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom" |
72 |
| A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" |
|
73 |
proof (cases "\<exists>k. Y k \<noteq> Ibottom") |
|
74 |
case True |
|
75 |
then obtain k where k: "Y k \<noteq> Ibottom" .. |
|
63040 | 76 |
define A where "A i = (THE a. Iup a = Y (i + k))" for i |
40084 | 77 |
have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)" |
78 |
proof |
|
79 |
fix i :: nat |
|
80 |
from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono) |
|
81 |
with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto) |
|
82 |
thus "Iup (A i) = Y (i + k)" |
|
83 |
by (cases "Y (i + k)", simp_all add: A_def) |
|
84 |
qed |
|
85 |
from Y have chain_A: "chain A" |
|
86 |
unfolding chain_def Iup_below [symmetric] |
|
87 |
by (simp add: Iup_A) |
|
88 |
hence "range A <<| (\<Squnion>i. A i)" |
|
89 |
by (rule cpo_lubI) |
|
90 |
hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)" |
|
91 |
by (rule is_lub_Iup) |
|
92 |
hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)" |
|
93 |
by (simp only: Iup_A) |
|
94 |
hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)" |
|
95 |
by (simp only: is_lub_range_shift [OF Y]) |
|
96 |
with Iup_A chain_A show ?thesis .. |
|
97 |
next |
|
98 |
case False |
|
99 |
then have "\<forall>i. Y i = Ibottom" by simp |
|
100 |
then show ?thesis .. |
|
101 |
qed |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
103 |
instance u :: (cpo) cpo |
40084 | 104 |
proof |
105 |
fix S :: "nat \<Rightarrow> 'a u" |
|
106 |
assume S: "chain S" |
|
107 |
thus "\<exists>x. range (\<lambda>i. S i) <<| x" |
|
108 |
proof (rule up_chain_lemma) |
|
109 |
assume "\<forall>i. S i = Ibottom" |
|
110 |
hence "range (\<lambda>i. S i) <<| Ibottom" |
|
40771 | 111 |
by (simp add: is_lub_const) |
40084 | 112 |
thus ?thesis .. |
113 |
next |
|
40085 | 114 |
fix A :: "nat \<Rightarrow> 'a" |
115 |
assume "range S <<| Iup (\<Squnion>i. A i)" |
|
40084 | 116 |
thus ?thesis .. |
117 |
qed |
|
118 |
qed |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
119 |
|
62175 | 120 |
subsection \<open>Lifted cpo is pointed\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
121 |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
122 |
instance u :: (cpo) pcpo |
40084 | 123 |
by intro_classes fast |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
124 |
|
62175 | 125 |
text \<open>for compatibility with old HOLCF-Version\<close> |
16753 | 126 |
lemma inst_up_pcpo: "\<bottom> = Ibottom" |
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset
|
127 |
by (rule minimal_up [THEN bottomI, symmetric]) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
128 |
|
62175 | 129 |
subsection \<open>Continuity of \emph{Iup} and \emph{Ifup}\<close> |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
130 |
|
62175 | 131 |
text \<open>continuity for @{term Iup}\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
132 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
133 |
lemma cont_Iup: "cont Iup" |
16215 | 134 |
apply (rule contI) |
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
135 |
apply (rule is_lub_Iup) |
26027 | 136 |
apply (erule cpo_lubI) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
137 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
138 |
|
62175 | 139 |
text \<open>continuity for @{term Ifup}\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
140 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
141 |
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" |
16753 | 142 |
by (induct x, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
143 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
144 |
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)" |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
145 |
apply (rule monofunI) |
16753 | 146 |
apply (case_tac x, simp) |
147 |
apply (case_tac y, simp) |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
148 |
apply (simp add: monofun_cfun_arg) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
149 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
150 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
151 |
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)" |
40084 | 152 |
proof (rule contI2) |
153 |
fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))" |
|
154 |
from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))" |
|
155 |
proof (rule up_chain_lemma) |
|
156 |
fix A and k |
|
157 |
assume A: "\<forall>i. Iup (A i) = Y (i + k)" |
|
158 |
assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" |
|
159 |
hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))" |
|
40771 | 160 |
by (simp add: lub_eqI contlub_cfun_arg) |
40084 | 161 |
also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))" |
162 |
by (simp add: A) |
|
163 |
also have "\<dots> = (\<Squnion>i. Ifup f (Y i))" |
|
164 |
using Y' by (rule lub_range_shift) |
|
165 |
finally show ?thesis by simp |
|
166 |
qed simp |
|
167 |
qed (rule monofun_Ifup2) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
168 |
|
62175 | 169 |
subsection \<open>Continuous versions of constants\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
170 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
171 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
172 |
up :: "'a \<rightarrow> 'a u" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
173 |
"up = (\<Lambda> x. Iup x)" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
174 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
175 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
176 |
fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
177 |
"fup = (\<Lambda> f p. Ifup f p)" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
178 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
179 |
translations |
26046 | 180 |
"case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" |
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
42151
diff
changeset
|
181 |
"case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" |
26046 | 182 |
"\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
183 |
|
62175 | 184 |
text \<open>continuous versions of lemmas for @{typ "('a)u"}\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
185 |
|
16753 | 186 |
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)" |
187 |
apply (induct z) |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
188 |
apply (simp add: inst_up_pcpo) |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
189 |
apply (simp add: up_def cont_Iup) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
190 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
191 |
|
16753 | 192 |
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
193 |
by (simp add: up_def cont_Iup) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
194 |
|
16753 | 195 |
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y" |
196 |
by simp |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
197 |
|
17838 | 198 |
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
199 |
by (simp add: up_def cont_Iup inst_up_pcpo) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
200 |
|
41182 | 201 |
lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
202 |
by simp (* FIXME: remove? *) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
203 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
204 |
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
205 |
by (simp add: up_def cont_Iup) |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
206 |
|
35783 | 207 |
lemma upE [case_names bottom up, cases type: u]: |
208 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
|
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
209 |
apply (cases p) |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
210 |
apply (simp add: inst_up_pcpo) |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
211 |
apply (simp add: up_def cont_Iup) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
212 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
213 |
|
35783 | 214 |
lemma up_induct [case_names bottom up, induct type: u]: |
215 |
"\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x" |
|
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
216 |
by (cases x, simp_all) |
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
217 |
|
62175 | 218 |
text \<open>lifting preserves chain-finiteness\<close> |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset
|
219 |
|
17838 | 220 |
lemma up_chain_cases: |
40084 | 221 |
assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>" |
222 |
| A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)" |
|
223 |
apply (rule up_chain_lemma [OF Y]) |
|
40771 | 224 |
apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) |
40084 | 225 |
done |
17838 | 226 |
|
25879 | 227 |
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" |
228 |
apply (rule compactI2) |
|
40084 | 229 |
apply (erule up_chain_cases) |
230 |
apply simp |
|
25879 | 231 |
apply (drule (1) compactD2, simp) |
40084 | 232 |
apply (erule exE) |
233 |
apply (drule_tac f="up" and x="x" in monofun_cfun_arg) |
|
234 |
apply (simp, erule exI) |
|
25879 | 235 |
done |
236 |
||
237 |
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x" |
|
238 |
unfolding compact_def |
|
40327 | 239 |
by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) |
25879 | 240 |
|
241 |
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x" |
|
242 |
by (safe elim!: compact_up compact_upD) |
|
243 |
||
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset
|
244 |
instance u :: (chfin) chfin |
25921 | 245 |
apply intro_classes |
25879 | 246 |
apply (erule compact_imp_max_in_chain) |
25898 | 247 |
apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all) |
17838 | 248 |
done |
249 |
||
62175 | 250 |
text \<open>properties of fup\<close> |
17838 | 251 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
252 |
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>" |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
253 |
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
254 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
255 |
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
256 |
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
257 |
|
16553 | 258 |
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" |
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
259 |
by (cases x, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
260 |
|
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset
|
261 |
end |