163 (strip_tac 1), |
163 (strip_tac 1), |
164 (rtac (thelubI RS sym) 1), |
164 (rtac (thelubI RS sym) 1), |
165 (etac (contE RS spec RS mp) 1), |
165 (etac (contE RS spec RS mp) 1), |
166 (atac 1) |
166 (atac 1) |
167 ]); |
167 ]); |
|
168 |
|
169 (* ------------------------------------------------------------------------ *) |
|
170 (* monotone functions map finite chains to finite chains *) |
|
171 (* ------------------------------------------------------------------------ *) |
|
172 |
|
173 qed_goalw "monofun_finch2finch" Cont.thy [finite_chain_def] |
|
174 "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" |
|
175 (fn prems => |
|
176 [ |
|
177 cut_facts_tac prems 1, |
|
178 safe_tac HOL_cs, |
|
179 fast_tac (HOL_cs addSEs [ch2ch_monofun]) 1, |
|
180 fast_tac (HOL_cs addss (HOL_ss addsimps [max_in_chain_def])) 1 |
|
181 ]); |
|
182 |
|
183 (* ------------------------------------------------------------------------ *) |
|
184 (* The same holds for continuous functions *) |
|
185 (* ------------------------------------------------------------------------ *) |
|
186 |
|
187 bind_thm ("cont_finch2finch", cont2mono RS monofun_finch2finch); |
|
188 (* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *) |
|
189 |
168 |
190 |
169 (* ------------------------------------------------------------------------ *) |
191 (* ------------------------------------------------------------------------ *) |
170 (* The following results are about a curried function that is monotone *) |
192 (* The following results are about a curried function that is monotone *) |
171 (* in both arguments *) |
193 (* in both arguments *) |
172 (* ------------------------------------------------------------------------ *) |
194 (* ------------------------------------------------------------------------ *) |