244 apply (rule_tac x="%n. stream_take n$s" in exI, auto) |
244 apply (rule_tac x="%n. stream_take n$s" in exI, auto) |
245 apply (induct_tac i, auto) |
245 apply (induct_tac i, auto) |
246 apply (drule fstreams_lub_lemma1, auto) |
246 apply (drule fstreams_lub_lemma1, auto) |
247 apply (rule_tac x="j" in exI, auto) |
247 apply (rule_tac x="j" in exI, auto) |
248 apply (case_tac "max_in_chain j Y") |
248 apply (case_tac "max_in_chain j Y") |
249 apply (frule lub_finch1 [THEN thelubI], auto) |
249 apply (frule lub_finch1 [THEN lub_eqI], auto) |
250 apply (rule_tac x="j" in exI) |
250 apply (rule_tac x="j" in exI) |
251 apply (erule subst) back back |
251 apply (erule subst) back back |
252 apply (simp add: below_prod_def sconc_mono) |
252 apply (simp add: below_prod_def sconc_mono) |
253 apply (simp add: max_in_chain_def, auto) |
253 apply (simp add: max_in_chain_def, auto) |
254 apply (rule_tac x="ja" in exI) |
254 apply (rule_tac x="ja" in exI) |
264 |
264 |
265 |
265 |
266 lemma lub_Pair_not_UU_lemma: |
266 lemma lub_Pair_not_UU_lemma: |
267 "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] |
267 "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] |
268 ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU" |
268 ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU" |
269 apply (frule thelub_cprod, clarsimp) |
269 apply (frule lub_prod, clarsimp) |
270 apply (drule chain_UU_I_inverse2, clarsimp) |
270 apply (drule chain_UU_I_inverse2, clarsimp) |
271 apply (case_tac "Y i", clarsimp) |
271 apply (case_tac "Y i", clarsimp) |
272 apply (case_tac "max_in_chain i Y") |
272 apply (case_tac "max_in_chain i Y") |
273 apply (drule maxinch_is_thelub, auto) |
273 apply (drule maxinch_is_thelub, auto) |
274 apply (rule_tac x="i" in exI, auto) |
274 apply (rule_tac x="i" in exI, auto) |
296 apply (rule_tac x="%n. stream_take n$ms" in exI, auto) |
296 apply (rule_tac x="%n. stream_take n$ms" in exI, auto) |
297 apply (induct_tac i, auto) |
297 apply (induct_tac i, auto) |
298 apply (drule fstreams_lub_lemma2, auto) |
298 apply (drule fstreams_lub_lemma2, auto) |
299 apply (rule_tac x="j" in exI, auto) |
299 apply (rule_tac x="j" in exI, auto) |
300 apply (case_tac "max_in_chain j Y") |
300 apply (case_tac "max_in_chain j Y") |
301 apply (frule lub_finch1 [THEN thelubI], auto) |
301 apply (frule lub_finch1 [THEN lub_eqI], auto) |
302 apply (rule_tac x="j" in exI) |
302 apply (rule_tac x="j" in exI) |
303 apply (erule subst) back back |
303 apply (erule subst) back back |
304 apply (simp add: sconc_mono) |
304 apply (simp add: sconc_mono) |
305 apply (simp add: max_in_chain_def, auto) |
305 apply (simp add: max_in_chain_def, auto) |
306 apply (rule_tac x="ja" in exI) |
306 apply (rule_tac x="ja" in exI) |
310 apply (simp add: ax_flat, auto) |
310 apply (simp add: ax_flat, auto) |
311 apply (drule fstreams_prefix, auto)+ |
311 apply (drule fstreams_prefix, auto)+ |
312 apply (rule sconc_mono) |
312 apply (rule sconc_mono) |
313 apply (subgoal_tac "tt ~= tta" "tta << ms") |
313 apply (subgoal_tac "tt ~= tta" "tta << ms") |
314 apply (blast intro: fstreams_chain_lemma) |
314 apply (blast intro: fstreams_chain_lemma) |
315 apply (frule lub_cprod [THEN thelubI], auto) |
315 apply (frule lub_prod, auto) |
316 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp) |
316 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp) |
317 apply (drule fstreams_mono, simp) |
317 apply (drule fstreams_mono, simp) |
318 apply (rule is_ub_thelub chainI) |
318 apply (rule is_ub_thelub chainI) |
319 apply (simp add: chain_def below_prod_def) |
319 apply (simp add: chain_def below_prod_def) |
320 apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp) |
320 apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp) |