author | paulson |
Wed, 28 Jun 2000 10:54:21 +0200 | |
changeset 9169 | 85a47aa21f74 |
parent 8935 | 548901d05a0e |
child 9245 | 428385c4bc50 |
permissions | -rw-r--r-- |
2640 | 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$ |
1461 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
2640 | 6 |
Lemmas for theory Porder.thy |
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 |
|
625 | 9 |
(* ------------------------------------------------------------------------ *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
(* lubs are unique *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
|
4031 | 13 |
qed_goalw "unique_lub" thy [is_lub, is_ub] |
1461 | 14 |
"[| S <<| x ; S <<| y |] ==> x=y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
( fn prems => |
1461 | 16 |
[ |
17 |
(cut_facts_tac prems 1), |
|
18 |
(etac conjE 1), |
|
19 |
(etac conjE 1), |
|
20 |
(rtac antisym_less 1), |
|
21 |
(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)), |
|
22 |
(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)) |
|
23 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
26 |
(* chains are monotone functions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
29 |
qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
( fn prems => |
1461 | 31 |
[ |
32 |
(cut_facts_tac prems 1), |
|
5192 | 33 |
(induct_tac "y" 1), |
1461 | 34 |
(rtac impI 1), |
35 |
(etac less_zeroE 1), |
|
2033 | 36 |
(stac less_Suc_eq 1), |
1461 | 37 |
(strip_tac 1), |
38 |
(etac disjE 1), |
|
39 |
(rtac trans_less 1), |
|
40 |
(etac allE 2), |
|
41 |
(atac 2), |
|
42 |
(fast_tac HOL_cs 1), |
|
43 |
(hyp_subst_tac 1), |
|
44 |
(etac allE 1), |
|
45 |
(atac 1) |
|
46 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
47 |
|
9169 | 48 |
Goal "[| chain F; x <= y |] ==> F x << F y"; |
49 |
by (rtac (le_imp_less_or_eq RS disjE) 1); |
|
50 |
by (atac 1); |
|
51 |
by (etac (chain_mono RS mp) 1); |
|
52 |
by (atac 1); |
|
53 |
by (hyp_subst_tac 1); |
|
54 |
by (rtac refl_less 1); |
|
55 |
qed "chain_mono3"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
59 |
(* The range of a chain is a totaly ordered << *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
61 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
62 |
qed_goalw "chain_tord" thy [tord] |
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
63 |
"!!F. chain(F) ==> tord(range(F))" |
1886 | 64 |
(fn _ => |
1461 | 65 |
[ |
3724 | 66 |
Safe_tac, |
1461 | 67 |
(rtac nat_less_cases 1), |
4098 | 68 |
(ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
69 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
70 |
(* ------------------------------------------------------------------------ *) |
625 | 71 |
(* technical lemmas about lub and is_lub *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
72 |
(* ------------------------------------------------------------------------ *) |
2640 | 73 |
bind_thm("lub",lub_def RS meta_eq_to_obj_eq); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
74 |
|
9169 | 75 |
Goal "? x. M <<| x ==> M <<| lub(M)"; |
76 |
by (stac lub 1); |
|
77 |
by (etac (select_eq_Ex RS iffD2) 1); |
|
78 |
qed "lubI"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
79 |
|
9169 | 80 |
Goal "M <<| lub(M) ==> ? x. M <<| x"; |
81 |
by (etac exI 1); |
|
82 |
qed "lubE"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
83 |
|
9169 | 84 |
Goal "(? x. M <<| x) = M <<| lub(M)"; |
85 |
by (stac lub 1); |
|
86 |
by (rtac (select_eq_Ex RS subst) 1); |
|
87 |
by (rtac refl 1); |
|
88 |
qed "lub_eq"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
89 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
90 |
|
9169 | 91 |
Goal "M <<| l ==> lub(M) = l"; |
92 |
by (rtac unique_lub 1); |
|
93 |
by (stac lub 1); |
|
94 |
by (etac selectI 1); |
|
95 |
by (atac 1); |
|
96 |
qed "thelubI"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
97 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
98 |
|
5068 | 99 |
Goal "lub{x} = x"; |
3018 | 100 |
by (rtac thelubI 1); |
4098 | 101 |
by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1); |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2640
diff
changeset
|
102 |
qed "lub_singleton"; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2640
diff
changeset
|
103 |
Addsimps [lub_singleton]; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2640
diff
changeset
|
104 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
105 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
106 |
(* access to some definition as inference rule *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
107 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
108 |
|
2640 | 109 |
qed_goalw "is_lubE" thy [is_lub] |
1461 | 110 |
"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
|
111 |
(fn prems => |
1461 | 112 |
[ |
113 |
(cut_facts_tac prems 1), |
|
114 |
(atac 1) |
|
115 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
116 |
|
2640 | 117 |
qed_goalw "is_lubI" thy [is_lub] |
1461 | 118 |
"S <| x & (! u. S <| u --> x << u) ==> S <<| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
119 |
(fn prems => |
1461 | 120 |
[ |
121 |
(cut_facts_tac prems 1), |
|
122 |
(atac 1) |
|
123 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
124 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
125 |
qed_goalw "chainE" thy [chain] "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
|
126 |
(fn prems => |
1461 | 127 |
[ |
128 |
(cut_facts_tac prems 1), |
|
129 |
(atac 1)]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
130 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
131 |
qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
132 |
(fn prems => |
1461 | 133 |
[ |
134 |
(cut_facts_tac prems 1), |
|
135 |
(atac 1)]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
136 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
137 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
138 |
(* technical lemmas about (least) upper bounds of chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
139 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
140 |
|
2640 | 141 |
qed_goalw "ub_rangeE" thy [is_ub] "range S <| x ==> !i. S(i) << x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
142 |
(fn prems => |
1461 | 143 |
[ |
144 |
(cut_facts_tac prems 1), |
|
145 |
(strip_tac 1), |
|
146 |
(rtac mp 1), |
|
147 |
(etac spec 1), |
|
148 |
(rtac rangeI 1) |
|
149 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
150 |
|
2640 | 151 |
qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x ==> range S <| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
152 |
(fn prems => |
1461 | 153 |
[ |
154 |
(cut_facts_tac prems 1), |
|
155 |
(strip_tac 1), |
|
156 |
(etac rangeE 1), |
|
157 |
(hyp_subst_tac 1), |
|
158 |
(etac spec 1) |
|
159 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
160 |
|
1779 | 161 |
bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
162 |
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
163 |
|
1779 | 164 |
bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
165 |
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
166 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
167 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
168 |
(* results about finite chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
169 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
170 |
|
2640 | 171 |
qed_goalw "lub_finch1" thy [max_in_chain_def] |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
172 |
"[| chain C; max_in_chain i C|] ==> range C <<| C i" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
173 |
(fn prems => |
1461 | 174 |
[ |
175 |
(cut_facts_tac prems 1), |
|
176 |
(rtac is_lubI 1), |
|
177 |
(rtac conjI 1), |
|
178 |
(rtac ub_rangeI 1), |
|
179 |
(rtac allI 1), |
|
180 |
(res_inst_tac [("m","i")] nat_less_cases 1), |
|
181 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
182 |
(etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1), |
|
183 |
(etac spec 1), |
|
184 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
185 |
(etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1), |
|
186 |
(etac spec 1), |
|
187 |
(etac (chain_mono RS mp) 1), |
|
188 |
(atac 1), |
|
189 |
(strip_tac 1), |
|
190 |
(etac (ub_rangeE RS spec) 1) |
|
191 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
192 |
|
2640 | 193 |
qed_goalw "lub_finch2" thy [finite_chain_def] |
1461 | 194 |
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
195 |
(fn prems=> |
1461 | 196 |
[ |
197 |
(cut_facts_tac prems 1), |
|
198 |
(rtac lub_finch1 1), |
|
199 |
(etac conjunct1 1), |
|
1675 | 200 |
(rtac (select_eq_Ex RS iffD2) 1), |
1461 | 201 |
(etac conjunct2 1) |
202 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
203 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
204 |
|
9169 | 205 |
Goal "x<<y ==> chain (%i. if i=0 then x else y)"; |
206 |
by (rtac chainI 1); |
|
207 |
by (rtac allI 1); |
|
208 |
by (induct_tac "i" 1); |
|
209 |
by (Asm_simp_tac 1); |
|
210 |
by (Asm_simp_tac 1); |
|
211 |
qed "bin_chain"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
212 |
|
2640 | 213 |
qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def] |
1461 | 214 |
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
215 |
(fn prems => |
1461 | 216 |
[ |
217 |
(cut_facts_tac prems 1), |
|
218 |
(rtac allI 1), |
|
5192 | 219 |
(induct_tac "j" 1), |
1461 | 220 |
(Asm_simp_tac 1), |
221 |
(Asm_simp_tac 1) |
|
222 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
223 |
|
9169 | 224 |
Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y"; |
225 |
by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1 |
|
226 |
THEN rtac lub_finch1 2); |
|
227 |
by (etac bin_chain 2); |
|
228 |
by (etac bin_chainmax 2); |
|
229 |
by (Simp_tac 1); |
|
230 |
qed "lub_bin_chain"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
231 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
232 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
233 |
(* the maximal element in a chain is its lub *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
234 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
235 |
|
9169 | 236 |
Goal "[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c"; |
237 |
by (rtac thelubI 1); |
|
238 |
by (rtac is_lubI 1); |
|
239 |
by (rtac conjI 1); |
|
240 |
by (etac ub_rangeI 1); |
|
241 |
by (strip_tac 1); |
|
242 |
by (etac exE 1); |
|
243 |
by (hyp_subst_tac 1); |
|
244 |
by (etac (ub_rangeE RS spec) 1); |
|
245 |
qed "lub_chain_maxelem"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
246 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
248 |
(* the lub of a constant chain is the constant *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
249 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
250 |
|
9169 | 251 |
Goal "range(%x. c) <<| c"; |
252 |
by (rtac is_lubI 1); |
|
253 |
by (rtac conjI 1); |
|
254 |
by (rtac ub_rangeI 1); |
|
255 |
by (strip_tac 1); |
|
256 |
by (rtac refl_less 1); |
|
257 |
by (strip_tac 1); |
|
258 |
by (etac (ub_rangeE RS spec) 1); |
|
259 |
qed "lub_const"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
260 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
261 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
262 |