191 apply (rule cont_flift1_not_arg) |
191 apply (rule cont_flift1_not_arg) |
192 apply auto |
192 apply auto |
193 apply (rule cont_flift1_arg) |
193 apply (rule cont_flift1_arg) |
194 done |
194 done |
195 |
195 |
196 lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))" |
|
197 -- {* @{text flift2} is continuous in its argument itself. *} |
|
198 apply (rule flatdom_strict2cont) |
|
199 apply simp |
|
200 done |
|
201 |
|
202 text {* |
196 text {* |
203 \medskip Extension of @{text cont_tac} and installation of simplifier. |
197 \medskip Extension of @{text cont_tac} and installation of simplifier. |
204 *} |
198 *} |
205 |
199 |
206 lemmas cont_lemmas_ext [simp] = |
200 lemmas cont_lemmas_ext [simp] = |
207 cont_flift1_arg cont_flift2_arg |
|
208 cont_flift1_arg_and_not_arg cont2cont_lambda |
201 cont_flift1_arg_and_not_arg cont2cont_lambda |
209 cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if |
202 cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if |
210 |
203 |
211 ML {* |
204 ML {* |
212 val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext"; |
205 val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext"; |
213 |
206 |
214 fun cont_tac i = resolve_tac cont_lemmas2 i; |
207 fun cont_tac i = resolve_tac cont_lemmas2 i; |
215 fun cont_tacR i = REPEAT (cont_tac i); |
208 fun cont_tacR i = REPEAT (cont_tac i); |
216 |
209 |
217 local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def" |
210 local val flift1_def = thm "flift1_def" |
218 in fun cont_tacRs i = |
211 in fun cont_tacRs i = |
219 simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN |
212 simp_tac (simpset() addsimps [flift1_def]) i THEN |
220 REPEAT (cont_tac i) |
213 REPEAT (cont_tac i) |
221 end; |
214 end; |
222 *} |
215 *} |
223 |
216 |
224 end |
217 end |