author | paulson |
Tue, 23 May 2000 18:06:22 +0200 | |
changeset 8935 | 548901d05a0e |
parent 5192 | 704dd3a6d47d |
child 9169 | 85a47aa21f74 |
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 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
48 |
qed_goal "chain_mono3" thy "[| 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
|
49 |
(fn prems => |
1461 | 50 |
[ |
51 |
(cut_facts_tac prems 1), |
|
52 |
(rtac (le_imp_less_or_eq RS disjE) 1), |
|
53 |
(atac 1), |
|
54 |
(etac (chain_mono RS mp) 1), |
|
55 |
(atac 1), |
|
56 |
(hyp_subst_tac 1), |
|
57 |
(rtac refl_less 1) |
|
58 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
59 |
|
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
62 |
(* 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
|
63 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
64 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
65 |
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
|
66 |
"!!F. chain(F) ==> tord(range(F))" |
1886 | 67 |
(fn _ => |
1461 | 68 |
[ |
3724 | 69 |
Safe_tac, |
1461 | 70 |
(rtac nat_less_cases 1), |
4098 | 71 |
(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
|
72 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
73 |
(* ------------------------------------------------------------------------ *) |
625 | 74 |
(* technical lemmas about lub and is_lub *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
(* ------------------------------------------------------------------------ *) |
2640 | 76 |
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
|
77 |
|
2640 | 78 |
qed_goal "lubI" thy "? x. M <<| x ==> M <<| lub(M)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
79 |
(fn prems => |
1461 | 80 |
[ |
81 |
(cut_facts_tac prems 1), |
|
2033 | 82 |
(stac lub 1), |
1675 | 83 |
(etac (select_eq_Ex RS iffD2) 1) |
1461 | 84 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
85 |
|
2640 | 86 |
qed_goal "lubE" thy "M <<| lub(M) ==> ? x. M <<| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
(fn prems => |
1461 | 88 |
[ |
89 |
(cut_facts_tac prems 1), |
|
90 |
(etac exI 1) |
|
91 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
92 |
|
2640 | 93 |
qed_goal "lub_eq" thy "(? x. M <<| x) = M <<| lub(M)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
(fn prems => |
1461 | 95 |
[ |
2033 | 96 |
(stac lub 1), |
1461 | 97 |
(rtac (select_eq_Ex RS subst) 1), |
98 |
(rtac refl 1) |
|
99 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
100 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
101 |
|
2640 | 102 |
qed_goal "thelubI" thy "M <<| l ==> lub(M) = l" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
103 |
(fn prems => |
1461 | 104 |
[ |
105 |
(cut_facts_tac prems 1), |
|
106 |
(rtac unique_lub 1), |
|
2033 | 107 |
(stac lub 1), |
1461 | 108 |
(etac selectI 1), |
109 |
(atac 1) |
|
110 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
111 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
112 |
|
5068 | 113 |
Goal "lub{x} = x"; |
3018 | 114 |
by (rtac thelubI 1); |
4098 | 115 |
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
|
116 |
qed "lub_singleton"; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2640
diff
changeset
|
117 |
Addsimps [lub_singleton]; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2640
diff
changeset
|
118 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
119 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
120 |
(* access to some definition as inference rule *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
121 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
122 |
|
2640 | 123 |
qed_goalw "is_lubE" thy [is_lub] |
1461 | 124 |
"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
|
125 |
(fn prems => |
1461 | 126 |
[ |
127 |
(cut_facts_tac prems 1), |
|
128 |
(atac 1) |
|
129 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
130 |
|
2640 | 131 |
qed_goalw "is_lubI" thy [is_lub] |
1461 | 132 |
"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
|
133 |
(fn prems => |
1461 | 134 |
[ |
135 |
(cut_facts_tac prems 1), |
|
136 |
(atac 1) |
|
137 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
138 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
139 |
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
|
140 |
(fn prems => |
1461 | 141 |
[ |
142 |
(cut_facts_tac prems 1), |
|
143 |
(atac 1)]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
144 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
145 |
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
|
146 |
(fn prems => |
1461 | 147 |
[ |
148 |
(cut_facts_tac prems 1), |
|
149 |
(atac 1)]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
150 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
151 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
152 |
(* technical lemmas about (least) upper bounds of chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
153 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
154 |
|
2640 | 155 |
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
|
156 |
(fn prems => |
1461 | 157 |
[ |
158 |
(cut_facts_tac prems 1), |
|
159 |
(strip_tac 1), |
|
160 |
(rtac mp 1), |
|
161 |
(etac spec 1), |
|
162 |
(rtac rangeI 1) |
|
163 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
|
2640 | 165 |
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
|
166 |
(fn prems => |
1461 | 167 |
[ |
168 |
(cut_facts_tac prems 1), |
|
169 |
(strip_tac 1), |
|
170 |
(etac rangeE 1), |
|
171 |
(hyp_subst_tac 1), |
|
172 |
(etac spec 1) |
|
173 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
174 |
|
1779 | 175 |
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
|
176 |
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
|
1779 | 178 |
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
|
179 |
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
180 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
181 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
182 |
(* results about finite chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
183 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
184 |
|
2640 | 185 |
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
|
186 |
"[| 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
|
187 |
(fn prems => |
1461 | 188 |
[ |
189 |
(cut_facts_tac prems 1), |
|
190 |
(rtac is_lubI 1), |
|
191 |
(rtac conjI 1), |
|
192 |
(rtac ub_rangeI 1), |
|
193 |
(rtac allI 1), |
|
194 |
(res_inst_tac [("m","i")] nat_less_cases 1), |
|
195 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
196 |
(etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1), |
|
197 |
(etac spec 1), |
|
198 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
199 |
(etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1), |
|
200 |
(etac spec 1), |
|
201 |
(etac (chain_mono RS mp) 1), |
|
202 |
(atac 1), |
|
203 |
(strip_tac 1), |
|
204 |
(etac (ub_rangeE RS spec) 1) |
|
205 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
206 |
|
2640 | 207 |
qed_goalw "lub_finch2" thy [finite_chain_def] |
1461 | 208 |
"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
|
209 |
(fn prems=> |
1461 | 210 |
[ |
211 |
(cut_facts_tac prems 1), |
|
212 |
(rtac lub_finch1 1), |
|
213 |
(etac conjunct1 1), |
|
1675 | 214 |
(rtac (select_eq_Ex RS iffD2) 1), |
1461 | 215 |
(etac conjunct2 1) |
216 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
217 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
218 |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
219 |
qed_goal "bin_chain" thy "x<<y ==> chain (%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
|
220 |
(fn prems => |
1461 | 221 |
[ |
222 |
(cut_facts_tac prems 1), |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
223 |
(rtac chainI 1), |
1461 | 224 |
(rtac allI 1), |
5192 | 225 |
(induct_tac "i" 1), |
1461 | 226 |
(Asm_simp_tac 1), |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2640
diff
changeset
|
227 |
(Asm_simp_tac 1) |
1461 | 228 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
229 |
|
2640 | 230 |
qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def] |
1461 | 231 |
"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
|
232 |
(fn prems => |
1461 | 233 |
[ |
234 |
(cut_facts_tac prems 1), |
|
235 |
(rtac allI 1), |
|
5192 | 236 |
(induct_tac "j" 1), |
1461 | 237 |
(Asm_simp_tac 1), |
238 |
(Asm_simp_tac 1) |
|
239 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
240 |
|
2640 | 241 |
qed_goal "lub_bin_chain" thy |
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
5192
diff
changeset
|
242 |
"x << y ==> range(%i::nat. if (i=0) then x else y) <<| y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
243 |
(fn prems=> |
1461 | 244 |
[ (cut_facts_tac prems 1), |
245 |
(res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1), |
|
246 |
(rtac lub_finch1 2), |
|
247 |
(etac bin_chain 2), |
|
248 |
(etac bin_chainmax 2), |
|
249 |
(Simp_tac 1) |
|
250 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
251 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
252 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
253 |
(* 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
|
254 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
255 |
|
2640 | 256 |
qed_goal "lub_chain_maxelem" thy |
3842 | 257 |
"[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c" |
1043 | 258 |
(fn prems => |
1461 | 259 |
[ |
260 |
(cut_facts_tac prems 1), |
|
261 |
(rtac thelubI 1), |
|
262 |
(rtac is_lubI 1), |
|
263 |
(rtac conjI 1), |
|
264 |
(etac ub_rangeI 1), |
|
265 |
(strip_tac 1), |
|
266 |
(etac exE 1), |
|
267 |
(hyp_subst_tac 1), |
|
268 |
(etac (ub_rangeE RS spec) 1) |
|
269 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
270 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
271 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
272 |
(* 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
|
273 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
274 |
|
3842 | 275 |
qed_goal "lub_const" thy "range(%x. c) <<| c" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
276 |
(fn prems => |
1461 | 277 |
[ |
278 |
(rtac is_lubI 1), |
|
279 |
(rtac conjI 1), |
|
280 |
(rtac ub_rangeI 1), |
|
281 |
(strip_tac 1), |
|
282 |
(rtac refl_less 1), |
|
283 |
(strip_tac 1), |
|
284 |
(etac (ub_rangeE RS spec) 1) |
|
285 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
286 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
287 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
288 |