src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 41431 138f414f14cb
parent 41413 64cd30d6b0b8
child 41476 0fa9629aa399
equal deleted inserted replaced
41430:1aa23e9f2c87 41431:138f414f14cb
   231 apply (simp add: flat_below_iff)
   231 apply (simp add: flat_below_iff)
   232 by (simp add: flat_below_iff)
   232 by (simp add: flat_below_iff)
   233 
   233 
   234 lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
   234 lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
   235 apply (subgoal_tac "(LUB i. Y i) ~= UU")
   235 apply (subgoal_tac "(LUB i. Y i) ~= UU")
   236 apply (drule chain_UU_I_inverse2, auto)
   236 apply (frule lub_eq_bottom_iff, auto)
   237 apply (drule_tac x="i" in is_ub_thelub, auto)
   237 apply (drule_tac x="i" in is_ub_thelub, auto)
   238 by (drule fstreams_prefix' [THEN iffD1], auto)
   238 by (drule fstreams_prefix' [THEN iffD1], auto)
   239 
   239 
   240 lemma fstreams_lub1: 
   240 lemma fstreams_lub1: 
   241  "[| chain Y; (LUB i. Y i) = <a> ooo s |]
   241  "[| chain Y; (LUB i. Y i) = <a> ooo s |]
   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 lub_prod, clarsimp)
   269 apply (frule lub_prod, clarsimp)
   270 apply (drule chain_UU_I_inverse2, clarsimp)
   270 apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\<lambda>i. fst (Y i)"])
   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)
   275 apply (simp add: max_in_chain_def, auto)
   275 apply (simp add: max_in_chain_def, auto)