author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 1886 | 0922b597b53d |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
1461 | 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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
Lemmas for theory porder.thy |
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 |
|
297 | 9 |
open Porder0; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
open Porder; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
|
625 | 12 |
|
13 |
(* ------------------------------------------------------------------------ *) |
|
14 |
(* the reverse law of anti--symmetrie of << *) |
|
15 |
(* ------------------------------------------------------------------------ *) |
|
16 |
||
892 | 17 |
qed_goal "antisym_less_inverse" Porder.thy "x=y ==> x << y & y << x" |
625 | 18 |
(fn prems => |
1461 | 19 |
[ |
20 |
(cut_facts_tac prems 1), |
|
21 |
(rtac conjI 1), |
|
22 |
((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)), |
|
23 |
((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1)) |
|
24 |
]); |
|
625 | 25 |
|
26 |
||
892 | 27 |
qed_goal "box_less" Porder.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
"[| a << b; c << a; b << d|] ==> c << d" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
(fn prems => |
1461 | 30 |
[ |
31 |
(cut_facts_tac prems 1), |
|
32 |
(etac trans_less 1), |
|
33 |
(etac trans_less 1), |
|
34 |
(atac 1) |
|
35 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
36 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
37 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
(* lubs are unique *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
40 |
|
892 | 41 |
qed_goalw "unique_lub " Porder.thy [is_lub, is_ub] |
1461 | 42 |
"[| S <<| x ; S <<| y |] ==> x=y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |
( fn prems => |
1461 | 44 |
[ |
45 |
(cut_facts_tac prems 1), |
|
46 |
(etac conjE 1), |
|
47 |
(etac conjE 1), |
|
48 |
(rtac antisym_less 1), |
|
49 |
(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)), |
|
50 |
(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)) |
|
51 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
(* chains are monotone functions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
|
892 | 57 |
qed_goalw "chain_mono" Porder.thy [is_chain] |
1461 | 58 |
" is_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
|
59 |
( fn prems => |
1461 | 60 |
[ |
61 |
(cut_facts_tac prems 1), |
|
62 |
(nat_ind_tac "y" 1), |
|
63 |
(rtac impI 1), |
|
64 |
(etac less_zeroE 1), |
|
65 |
(rtac (less_Suc_eq RS ssubst) 1), |
|
66 |
(strip_tac 1), |
|
67 |
(etac disjE 1), |
|
68 |
(rtac trans_less 1), |
|
69 |
(etac allE 2), |
|
70 |
(atac 2), |
|
71 |
(fast_tac HOL_cs 1), |
|
72 |
(hyp_subst_tac 1), |
|
73 |
(etac allE 1), |
|
74 |
(atac 1) |
|
75 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
76 |
|
892 | 77 |
qed_goal "chain_mono3" Porder.thy |
1461 | 78 |
"[| is_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
|
79 |
(fn prems => |
1461 | 80 |
[ |
81 |
(cut_facts_tac prems 1), |
|
82 |
(rtac (le_imp_less_or_eq RS disjE) 1), |
|
83 |
(atac 1), |
|
84 |
(etac (chain_mono RS mp) 1), |
|
85 |
(atac 1), |
|
86 |
(hyp_subst_tac 1), |
|
87 |
(rtac refl_less 1) |
|
88 |
]); |
|
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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
91 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
92 |
(* 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
|
93 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
|
1886 | 95 |
qed_goalw "chain_is_tord" Porder.thy [is_tord] |
96 |
"!!F. is_chain(F) ==> is_tord(range(F))" |
|
97 |
(fn _ => |
|
1461 | 98 |
[ |
1886 | 99 |
(Step_tac 1), |
1461 | 100 |
(rtac nat_less_cases 1), |
1886 | 101 |
(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
|
102 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
103 |
(* ------------------------------------------------------------------------ *) |
625 | 104 |
(* technical lemmas about lub and is_lub *) |
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 |
|
892 | 107 |
qed_goal "lubI" Porder.thy "(? x. M <<| x) ==> M <<| lub(M)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
108 |
(fn prems => |
1461 | 109 |
[ |
110 |
(cut_facts_tac prems 1), |
|
111 |
(rtac (lub RS ssubst) 1), |
|
1675 | 112 |
(etac (select_eq_Ex RS iffD2) 1) |
1461 | 113 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
114 |
|
892 | 115 |
qed_goal "lubE" Porder.thy " M <<| lub(M) ==> ? x. M <<| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
116 |
(fn prems => |
1461 | 117 |
[ |
118 |
(cut_facts_tac prems 1), |
|
119 |
(etac exI 1) |
|
120 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
121 |
|
892 | 122 |
qed_goal "lub_eq" Porder.thy |
1461 | 123 |
"(? x. M <<| x) = M <<| lub(M)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
124 |
(fn prems => |
1461 | 125 |
[ |
126 |
(rtac (lub RS ssubst) 1), |
|
127 |
(rtac (select_eq_Ex RS subst) 1), |
|
128 |
(rtac refl 1) |
|
129 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
130 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
131 |
|
892 | 132 |
qed_goal "thelubI" Porder.thy " M <<| l ==> lub(M) = l" |
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 |
(rtac unique_lub 1), |
|
137 |
(rtac (lub RS ssubst) 1), |
|
138 |
(etac selectI 1), |
|
139 |
(atac 1) |
|
140 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
141 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
142 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
143 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
144 |
(* access to some definition as inference rule *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
145 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
146 |
|
892 | 147 |
qed_goalw "is_lubE" Porder.thy [is_lub] |
1461 | 148 |
"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
|
149 |
(fn prems => |
1461 | 150 |
[ |
151 |
(cut_facts_tac prems 1), |
|
152 |
(atac 1) |
|
153 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
154 |
|
892 | 155 |
qed_goalw "is_lubI" Porder.thy [is_lub] |
1461 | 156 |
"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
|
157 |
(fn prems => |
1461 | 158 |
[ |
159 |
(cut_facts_tac prems 1), |
|
160 |
(atac 1) |
|
161 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
162 |
|
892 | 163 |
qed_goalw "is_chainE" Porder.thy [is_chain] |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
"is_chain(F) ==> ! i. F(i) << F(Suc(i))" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
165 |
(fn prems => |
1461 | 166 |
[ |
167 |
(cut_facts_tac prems 1), |
|
168 |
(atac 1)]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
169 |
|
892 | 170 |
qed_goalw "is_chainI" Porder.thy [is_chain] |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
171 |
"! i. F(i) << F(Suc(i)) ==> is_chain(F) " |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
172 |
(fn prems => |
1461 | 173 |
[ |
174 |
(cut_facts_tac prems 1), |
|
175 |
(atac 1)]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
176 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
178 |
(* technical lemmas about (least) upper bounds of chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
179 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
180 |
|
892 | 181 |
qed_goalw "ub_rangeE" Porder.thy [is_ub] |
1461 | 182 |
"range(S) <| x ==> ! i. S(i) << x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
183 |
(fn prems => |
1461 | 184 |
[ |
185 |
(cut_facts_tac prems 1), |
|
186 |
(strip_tac 1), |
|
187 |
(rtac mp 1), |
|
188 |
(etac spec 1), |
|
189 |
(rtac rangeI 1) |
|
190 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
191 |
|
892 | 192 |
qed_goalw "ub_rangeI" Porder.thy [is_ub] |
1461 | 193 |
"! i. S(i) << x ==> range(S) <| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
194 |
(fn prems => |
1461 | 195 |
[ |
196 |
(cut_facts_tac prems 1), |
|
197 |
(strip_tac 1), |
|
198 |
(etac rangeE 1), |
|
199 |
(hyp_subst_tac 1), |
|
200 |
(etac spec 1) |
|
201 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
202 |
|
1779 | 203 |
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
|
204 |
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
205 |
|
1779 | 206 |
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
|
207 |
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
208 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
209 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
210 |
(* Prototype lemmas for class pcpo *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
211 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
212 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
213 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
214 |
(* a technical argument about << on void *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
215 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
216 |
|
892 | 217 |
qed_goal "less_void" Porder.thy "((u1::void) << u2) = (u1 = u2)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
218 |
(fn prems => |
1461 | 219 |
[ |
220 |
(rtac (inst_void_po RS ssubst) 1), |
|
221 |
(rewtac less_void_def), |
|
222 |
(rtac iffI 1), |
|
223 |
(rtac injD 1), |
|
224 |
(atac 2), |
|
225 |
(rtac inj_inverseI 1), |
|
226 |
(rtac Rep_Void_inverse 1), |
|
227 |
(etac arg_cong 1) |
|
228 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
229 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
230 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
231 |
(* void is pointed. The least element is UU_void *) |
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 |
|
1461 | 234 |
qed_goal "minimal_void" Porder.thy "UU_void << x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
235 |
(fn prems => |
1461 | 236 |
[ |
237 |
(rtac (inst_void_po RS ssubst) 1), |
|
238 |
(rewtac less_void_def), |
|
239 |
(simp_tac (!simpset addsimps [unique_void]) 1) |
|
240 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
241 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
242 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
243 |
(* UU_void is the trivial lub of all chains in void *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
244 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
245 |
|
892 | 246 |
qed_goalw "lub_void" Porder.thy [is_lub] "M <<| UU_void" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
(fn prems => |
1461 | 248 |
[ |
249 |
(rtac conjI 1), |
|
250 |
(rewtac is_ub), |
|
251 |
(strip_tac 1), |
|
252 |
(rtac (inst_void_po RS ssubst) 1), |
|
253 |
(rewtac less_void_def), |
|
254 |
(simp_tac (!simpset addsimps [unique_void]) 1), |
|
255 |
(strip_tac 1), |
|
256 |
(rtac minimal_void 1) |
|
257 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
258 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
259 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
260 |
(* lub(?M) = UU_void *) |
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 |
|
1779 | 263 |
bind_thm ("thelub_void", lub_void RS thelubI); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
264 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
265 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
266 |
(* void is a cpo wrt. countable chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
267 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
268 |
|
892 | 269 |
qed_goal "cpo_void" Porder.thy |
1461 | 270 |
"is_chain((S::nat=>void)) ==> ? x. range(S) <<| x " |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
271 |
(fn prems => |
1461 | 272 |
[ |
273 |
(cut_facts_tac prems 1), |
|
274 |
(res_inst_tac [("x","UU_void")] exI 1), |
|
275 |
(rtac lub_void 1) |
|
276 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
277 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
278 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
279 |
(* end of prototype lemmas for class pcpo *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
280 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
281 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
282 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
283 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
284 |
(* results about finite chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
285 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
286 |
|
892 | 287 |
qed_goalw "lub_finch1" Porder.thy [max_in_chain_def] |
1461 | 288 |
"[| is_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
|
289 |
(fn prems => |
1461 | 290 |
[ |
291 |
(cut_facts_tac prems 1), |
|
292 |
(rtac is_lubI 1), |
|
293 |
(rtac conjI 1), |
|
294 |
(rtac ub_rangeI 1), |
|
295 |
(rtac allI 1), |
|
296 |
(res_inst_tac [("m","i")] nat_less_cases 1), |
|
297 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
298 |
(etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1), |
|
299 |
(etac spec 1), |
|
300 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
301 |
(etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1), |
|
302 |
(etac spec 1), |
|
303 |
(etac (chain_mono RS mp) 1), |
|
304 |
(atac 1), |
|
305 |
(strip_tac 1), |
|
306 |
(etac (ub_rangeE RS spec) 1) |
|
307 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
308 |
|
892 | 309 |
qed_goalw "lub_finch2" Porder.thy [finite_chain_def] |
1461 | 310 |
"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
|
311 |
(fn prems=> |
1461 | 312 |
[ |
313 |
(cut_facts_tac prems 1), |
|
314 |
(rtac lub_finch1 1), |
|
315 |
(etac conjunct1 1), |
|
1675 | 316 |
(rtac (select_eq_Ex RS iffD2) 1), |
1461 | 317 |
(etac conjunct2 1) |
318 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
319 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
320 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
321 |
qed_goal "bin_chain" Porder.thy "x<<y ==> is_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
|
322 |
(fn prems => |
1461 | 323 |
[ |
324 |
(cut_facts_tac prems 1), |
|
325 |
(rtac is_chainI 1), |
|
326 |
(rtac allI 1), |
|
327 |
(nat_ind_tac "i" 1), |
|
328 |
(Asm_simp_tac 1), |
|
329 |
(Asm_simp_tac 1), |
|
330 |
(rtac refl_less 1) |
|
331 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
332 |
|
892 | 333 |
qed_goalw "bin_chainmax" Porder.thy [max_in_chain_def,le_def] |
1461 | 334 |
"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
|
335 |
(fn prems => |
1461 | 336 |
[ |
337 |
(cut_facts_tac prems 1), |
|
338 |
(rtac allI 1), |
|
339 |
(nat_ind_tac "j" 1), |
|
340 |
(Asm_simp_tac 1), |
|
341 |
(Asm_simp_tac 1) |
|
342 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
343 |
|
892 | 344 |
qed_goal "lub_bin_chain" Porder.thy |
1461 | 345 |
"x << y ==> range(%i. 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
|
346 |
(fn prems=> |
1461 | 347 |
[ (cut_facts_tac prems 1), |
348 |
(res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1), |
|
349 |
(rtac lub_finch1 2), |
|
350 |
(etac bin_chain 2), |
|
351 |
(etac bin_chainmax 2), |
|
352 |
(Simp_tac 1) |
|
353 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
354 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
355 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
356 |
(* 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
|
357 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
358 |
|
892 | 359 |
qed_goal "lub_chain_maxelem" Porder.thy |
1043 | 360 |
"[|? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c" |
361 |
(fn prems => |
|
1461 | 362 |
[ |
363 |
(cut_facts_tac prems 1), |
|
364 |
(rtac thelubI 1), |
|
365 |
(rtac is_lubI 1), |
|
366 |
(rtac conjI 1), |
|
367 |
(etac ub_rangeI 1), |
|
368 |
(strip_tac 1), |
|
369 |
(etac exE 1), |
|
370 |
(hyp_subst_tac 1), |
|
371 |
(etac (ub_rangeE RS spec) 1) |
|
372 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
373 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
374 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
375 |
(* 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
|
376 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
377 |
|
892 | 378 |
qed_goal "lub_const" Porder.thy "range(%x.c) <<| c" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
379 |
(fn prems => |
1461 | 380 |
[ |
381 |
(rtac is_lubI 1), |
|
382 |
(rtac conjI 1), |
|
383 |
(rtac ub_rangeI 1), |
|
384 |
(strip_tac 1), |
|
385 |
(rtac refl_less 1), |
|
386 |
(strip_tac 1), |
|
387 |
(etac (ub_rangeE RS spec) 1) |
|
388 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
389 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
390 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
391 |