equal
deleted
inserted
replaced
336 by (simp add: cfun_below_iff) |
336 by (simp add: cfun_below_iff) |
337 |
337 |
338 text \<open>some lemmata for functions with flat/chfin domain/range types\<close> |
338 text \<open>some lemmata for functions with flat/chfin domain/range types\<close> |
339 |
339 |
340 lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin) |
340 lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin) |
341 ==> !s. ? n. (LUB i. Y i)$s = Y n$s" |
341 ==> !s. ? n. (LUB i. Y i)\<cdot>s = Y n\<cdot>s" |
342 apply (rule allI) |
342 apply (rule allI) |
343 apply (subst contlub_cfun_fun) |
343 apply (subst contlub_cfun_fun) |
344 apply assumption |
344 apply assumption |
345 apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL) |
345 apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL) |
346 done |
346 done |