author | aspinall |
Wed, 13 Jul 2005 20:07:01 +0200 | |
changeset 16821 | ba1f6aba44ed |
parent 16318 | 45b12a01382f |
child 17372 | d73f67e90a95 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Porder.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 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
5 |
Definition of class porder (partial order). |
16070
4a83dd540b88
removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents:
15930
diff
changeset
|
6 |
Conservative extension of theory Porder0 by constant definitions. |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
9 |
header {* Partial orders *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
10 |
|
15577 | 11 |
theory Porder |
12 |
imports Main |
|
13 |
begin |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
14 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
15 |
subsection {* Type class for partial orders *} |
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
16 |
|
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
17 |
-- {* introduce a (syntactic) class for the constant @{text "<<"} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
18 |
axclass sq_ord < type |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
19 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
20 |
-- {* characteristic constant @{text "<<"} for po *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
21 |
consts |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
22 |
"<<" :: "['a,'a::sq_ord] => bool" (infixl 55) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
23 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
24 |
syntax (xsymbols) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
25 |
"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\<sqsubseteq>" 55) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
26 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
27 |
axclass po < sq_ord |
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
28 |
-- {* class axioms: *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
29 |
refl_less [iff]: "x << x" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
30 |
antisym_less: "[|x << y; y << x |] ==> x = y" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
31 |
trans_less: "[|x << y; y << z |] ==> x << z" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
32 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
33 |
text {* minimal fixes least element *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
34 |
|
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
35 |
lemma minimal2UU[OF allI] : "!x::'a::po. uu<<x ==> uu=(THE u.!y. u<<y)" |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
36 |
by (blast intro: theI2 antisym_less) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
37 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
38 |
text {* the reverse law of anti-symmetry of @{term "op <<"} *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
39 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
40 |
lemma antisym_less_inverse: "(x::'a::po)=y ==> x << y & y << x" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
41 |
apply blast |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
42 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
43 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
44 |
lemma box_less: "[| (a::'a::po) << b; c << a; b << d|] ==> c << d" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
45 |
apply (erule trans_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
46 |
apply (erule trans_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
47 |
apply assumption |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
48 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
49 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
50 |
lemma po_eq_conv: "((x::'a::po)=y) = (x << y & y << x)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
51 |
apply (fast elim!: antisym_less_inverse intro!: antisym_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
52 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
53 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
54 |
subsection {* Chains and least upper bounds *} |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
|
1479 | 56 |
consts |
57 |
"<|" :: "['a set,'a::po] => bool" (infixl 55) |
|
58 |
"<<|" :: "['a set,'a::po] => bool" (infixl 55) |
|
59 |
lub :: "'a set => 'a::po" |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
60 |
tord :: "'a::po set => bool" |
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
61 |
chain :: "(nat=>'a::po) => bool" |
1479 | 62 |
max_in_chain :: "[nat,nat=>'a::po]=>bool" |
63 |
finite_chain :: "(nat=>'a::po)=>bool" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
64 |
|
2394 | 65 |
syntax |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12114
diff
changeset
|
66 |
"@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10) |
2394 | 67 |
|
68 |
translations |
|
3842 | 69 |
"LUB x. t" == "lub(range(%x. t))" |
2394 | 70 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12030
diff
changeset
|
71 |
syntax (xsymbols) |
15562 | 72 |
"LUB " :: "[idts, 'a] => 'a" ("(3\<Squnion>_./ _)"[0,10] 10) |
2394 | 73 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset
|
74 |
defs |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
76 |
-- {* class definitions *} |
15562 | 77 |
is_ub_def: "S <| x == ! y. y:S --> y<<x" |
78 |
is_lub_def: "S <<| x == S <| x & (!u. S <| u --> x << u)" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
79 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
80 |
-- {* Arbitrary chains are total orders *} |
15562 | 81 |
tord_def: "tord S == !x y. x:S & y:S --> (x<<y | y<<x)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
82 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
83 |
-- {* Here we use countable chains and I prefer to code them as functions! *} |
15562 | 84 |
chain_def: "chain F == !i. F i << F (Suc i)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
85 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
86 |
-- {* finite chains, needed for monotony of continouous functions *} |
15562 | 87 |
max_in_chain_def: "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" |
88 |
finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)" |
|
89 |
||
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
90 |
lub_def: "lub S == (THE x. S <<| x)" |
15562 | 91 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
92 |
text {* lubs are unique *} |
15562 | 93 |
|
94 |
lemma unique_lub: |
|
95 |
"[| S <<| x ; S <<| y |] ==> x=y" |
|
96 |
apply (unfold is_lub_def is_ub_def) |
|
97 |
apply (blast intro: antisym_less) |
|
98 |
done |
|
99 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
100 |
text {* chains are monotone functions *} |
15562 | 101 |
|
102 |
lemma chain_mono [rule_format]: "chain F ==> x<y --> F x<<F y" |
|
103 |
apply (unfold chain_def) |
|
104 |
apply (induct_tac "y") |
|
105 |
apply auto |
|
106 |
prefer 2 apply (blast intro: trans_less) |
|
107 |
apply (blast elim!: less_SucE) |
|
108 |
done |
|
109 |
||
110 |
lemma chain_mono3: "[| chain F; x <= y |] ==> F x << F y" |
|
111 |
apply (drule le_imp_less_or_eq) |
|
112 |
apply (blast intro: chain_mono) |
|
113 |
done |
|
114 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
115 |
text {* The range of a chain is a totally ordered *} |
15562 | 116 |
|
117 |
lemma chain_tord: "chain(F) ==> tord(range(F))" |
|
118 |
apply (unfold tord_def) |
|
119 |
apply safe |
|
120 |
apply (rule nat_less_cases) |
|
121 |
apply (fast intro: chain_mono)+ |
|
122 |
done |
|
123 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
124 |
text {* technical lemmas about @{term lub} and @{term is_lub} *} |
15562 | 125 |
|
126 |
lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] |
|
127 |
||
128 |
lemma lubI[OF exI]: "EX x. M <<| x ==> M <<| lub(M)" |
|
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
129 |
apply (unfold lub_def) |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
130 |
apply (rule theI') |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
131 |
apply (erule ex_ex1I) |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
132 |
apply (erule unique_lub) |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
133 |
apply assumption |
15562 | 134 |
done |
135 |
||
136 |
lemma thelubI: "M <<| l ==> lub(M) = l" |
|
137 |
apply (rule unique_lub) |
|
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
138 |
apply (rule lubI) |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
139 |
apply assumption |
15562 | 140 |
apply assumption |
141 |
done |
|
142 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
143 |
lemma lub_singleton [simp]: "lub{x} = x" |
15562 | 144 |
apply (simp (no_asm) add: thelubI is_lub_def is_ub_def) |
145 |
done |
|
146 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
147 |
text {* access to some definition as inference rule *} |
15562 | 148 |
|
149 |
lemma is_lubD1: "S <<| x ==> S <| x" |
|
150 |
apply (unfold is_lub_def) |
|
151 |
apply auto |
|
152 |
done |
|
153 |
||
154 |
lemma is_lub_lub: "[| S <<| x; S <| u |] ==> x << u" |
|
155 |
apply (unfold is_lub_def) |
|
156 |
apply auto |
|
157 |
done |
|
158 |
||
159 |
lemma is_lubI: |
|
160 |
"[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x" |
|
161 |
apply (unfold is_lub_def) |
|
162 |
apply blast |
|
163 |
done |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
|
15562 | 165 |
lemma chainE: "chain F ==> F(i) << F(Suc(i))" |
166 |
apply (unfold chain_def) |
|
167 |
apply auto |
|
168 |
done |
|
169 |
||
170 |
lemma chainI: "(!!i. F i << F(Suc i)) ==> chain F" |
|
171 |
apply (unfold chain_def) |
|
172 |
apply blast |
|
173 |
done |
|
174 |
||
175 |
lemma chain_shift: "chain Y ==> chain (%i. Y (i + j))" |
|
176 |
apply (rule chainI) |
|
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
177 |
apply simp |
15562 | 178 |
apply (erule chainE) |
179 |
done |
|
180 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
181 |
text {* technical lemmas about (least) upper bounds of chains *} |
15562 | 182 |
|
183 |
lemma ub_rangeD: "range S <| x ==> S(i) << x" |
|
184 |
apply (unfold is_ub_def) |
|
185 |
apply blast |
|
186 |
done |
|
187 |
||
188 |
lemma ub_rangeI: "(!!i. S i << x) ==> range S <| x" |
|
189 |
apply (unfold is_ub_def) |
|
190 |
apply blast |
|
191 |
done |
|
192 |
||
193 |
lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard] |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
194 |
-- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) |
15562 | 195 |
|
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
196 |
lemma is_ub_range_shift: |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
197 |
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x" |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
198 |
apply (rule iffI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
199 |
apply (rule ub_rangeI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
200 |
apply (rule_tac y="S (i + j)" in trans_less) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
201 |
apply (erule chain_mono3) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
202 |
apply (rule le_add1) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
203 |
apply (erule ub_rangeD) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
204 |
apply (rule ub_rangeI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
205 |
apply (erule ub_rangeD) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
206 |
done |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
207 |
|
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
208 |
lemma is_lub_range_shift: |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
209 |
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x" |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
210 |
by (simp add: is_lub_def is_ub_range_shift) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
211 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
212 |
text {* results about finite chains *} |
15562 | 213 |
|
214 |
lemma lub_finch1: |
|
215 |
"[| chain C; max_in_chain i C|] ==> range C <<| C i" |
|
216 |
apply (unfold max_in_chain_def) |
|
217 |
apply (rule is_lubI) |
|
218 |
apply (rule ub_rangeI) |
|
219 |
apply (rule_tac m = "i" in nat_less_cases) |
|
220 |
apply (rule antisym_less_inverse [THEN conjunct2]) |
|
221 |
apply (erule disjI1 [THEN less_or_eq_imp_le, THEN rev_mp]) |
|
222 |
apply (erule spec) |
|
223 |
apply (rule antisym_less_inverse [THEN conjunct2]) |
|
224 |
apply (erule disjI2 [THEN less_or_eq_imp_le, THEN rev_mp]) |
|
225 |
apply (erule spec) |
|
226 |
apply (erule chain_mono) |
|
227 |
apply assumption |
|
228 |
apply (erule ub_rangeD) |
|
229 |
done |
|
230 |
||
231 |
lemma lub_finch2: |
|
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
232 |
"finite_chain(C) ==> range(C) <<| C(LEAST i. max_in_chain i C)" |
15562 | 233 |
apply (unfold finite_chain_def) |
234 |
apply (rule lub_finch1) |
|
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
235 |
prefer 2 apply (best intro: LeastI) |
15562 | 236 |
apply blast |
237 |
done |
|
238 |
||
239 |
lemma bin_chain: "x<<y ==> chain (%i. if i=0 then x else y)" |
|
240 |
apply (rule chainI) |
|
241 |
apply (induct_tac "i") |
|
242 |
apply auto |
|
243 |
done |
|
244 |
||
245 |
lemma bin_chainmax: |
|
246 |
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)" |
|
247 |
apply (unfold max_in_chain_def le_def) |
|
248 |
apply (rule allI) |
|
249 |
apply (induct_tac "j") |
|
250 |
apply auto |
|
251 |
done |
|
252 |
||
253 |
lemma lub_bin_chain: "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y" |
|
254 |
apply (rule_tac s = "if (Suc 0) = 0 then x else y" in subst , rule_tac [2] lub_finch1) |
|
255 |
apply (erule_tac [2] bin_chain) |
|
256 |
apply (erule_tac [2] bin_chainmax) |
|
257 |
apply (simp (no_asm)) |
|
258 |
done |
|
259 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
260 |
text {* the maximal element in a chain is its lub *} |
15562 | 261 |
|
262 |
lemma lub_chain_maxelem: "[| Y i = c; ALL i. Y i<<c |] ==> lub(range Y) = c" |
|
263 |
apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) |
|
264 |
done |
|
265 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
266 |
text {* the lub of a constant chain is the constant *} |
15562 | 267 |
|
268 |
lemma lub_const: "range(%x. c) <<| c" |
|
269 |
apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI) |
|
270 |
done |
|
1274 | 271 |
|
16092 | 272 |
lemmas thelub_const = lub_const [THEN thelubI, standard] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset
|
273 |
|
16092 | 274 |
end |