289 done |
289 done |
290 |
290 |
291 subsection {* Defining functions in terms of basis elements *} |
291 subsection {* Defining functions in terms of basis elements *} |
292 |
292 |
293 definition |
293 definition |
294 basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where |
294 extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where |
295 "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))" |
295 "extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))" |
296 |
296 |
297 lemma basis_fun_lemma: |
297 lemma extension_lemma: |
298 fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
298 fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
299 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
299 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
300 shows "\<exists>u. f ` rep x <<| u" |
300 shows "\<exists>u. f ` rep x <<| u" |
301 proof - |
301 proof - |
302 obtain Y where Y: "\<forall>i. Y i \<preceq> Y (Suc i)" |
302 obtain Y where Y: "\<forall>i. Y i \<preceq> Y (Suc i)" |
318 apply assumption |
318 apply assumption |
319 done |
319 done |
320 thus ?thesis .. |
320 thus ?thesis .. |
321 qed |
321 qed |
322 |
322 |
323 lemma basis_fun_beta: |
323 lemma extension_beta: |
324 fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
324 fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
325 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
325 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
326 shows "basis_fun f\<cdot>x = lub (f ` rep x)" |
326 shows "extension f\<cdot>x = lub (f ` rep x)" |
327 unfolding basis_fun_def |
327 unfolding extension_def |
328 proof (rule beta_cfun) |
328 proof (rule beta_cfun) |
329 have lub: "\<And>x. \<exists>u. f ` rep x <<| u" |
329 have lub: "\<And>x. \<exists>u. f ` rep x <<| u" |
330 using f_mono by (rule basis_fun_lemma) |
330 using f_mono by (rule extension_lemma) |
331 show cont: "cont (\<lambda>x. lub (f ` rep x))" |
331 show cont: "cont (\<lambda>x. lub (f ` rep x))" |
332 apply (rule contI2) |
332 apply (rule contI2) |
333 apply (rule monofunI) |
333 apply (rule monofunI) |
334 apply (rule is_lub_thelub_ex [OF lub ub_imageI]) |
334 apply (rule is_lub_thelub_ex [OF lub ub_imageI]) |
335 apply (rule is_ub_thelub_ex [OF lub imageI]) |
335 apply (rule is_ub_thelub_ex [OF lub imageI]) |
339 apply (erule rev_below_trans [OF is_ub_thelub]) |
339 apply (erule rev_below_trans [OF is_ub_thelub]) |
340 apply (erule is_ub_thelub_ex [OF lub imageI]) |
340 apply (erule is_ub_thelub_ex [OF lub imageI]) |
341 done |
341 done |
342 qed |
342 qed |
343 |
343 |
344 lemma basis_fun_principal: |
344 lemma extension_principal: |
345 fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
345 fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
346 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
346 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
347 shows "basis_fun f\<cdot>(principal a) = f a" |
347 shows "extension f\<cdot>(principal a) = f a" |
348 apply (subst basis_fun_beta, erule f_mono) |
348 apply (subst extension_beta, erule f_mono) |
349 apply (subst rep_principal) |
349 apply (subst rep_principal) |
350 apply (rule lub_eqI) |
350 apply (rule lub_eqI) |
351 apply (rule is_lub_maximal) |
351 apply (rule is_lub_maximal) |
352 apply (rule ub_imageI) |
352 apply (rule ub_imageI) |
353 apply (simp add: f_mono) |
353 apply (simp add: f_mono) |
354 apply (rule imageI) |
354 apply (rule imageI) |
355 apply (simp add: r_refl) |
355 apply (simp add: r_refl) |
356 done |
356 done |
357 |
357 |
358 lemma basis_fun_mono: |
358 lemma extension_mono: |
359 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
359 assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
360 assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b" |
360 assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b" |
361 assumes below: "\<And>a. f a \<sqsubseteq> g a" |
361 assumes below: "\<And>a. f a \<sqsubseteq> g a" |
362 shows "basis_fun f \<sqsubseteq> basis_fun g" |
362 shows "extension f \<sqsubseteq> extension g" |
363 apply (rule cfun_belowI) |
363 apply (rule cfun_belowI) |
364 apply (simp only: basis_fun_beta f_mono g_mono) |
364 apply (simp only: extension_beta f_mono g_mono) |
365 apply (rule is_lub_thelub_ex) |
365 apply (rule is_lub_thelub_ex) |
366 apply (rule basis_fun_lemma, erule f_mono) |
366 apply (rule extension_lemma, erule f_mono) |
367 apply (rule ub_imageI, rename_tac a) |
367 apply (rule ub_imageI, rename_tac a) |
368 apply (rule below_trans [OF below]) |
368 apply (rule below_trans [OF below]) |
369 apply (rule is_ub_thelub_ex) |
369 apply (rule is_ub_thelub_ex) |
370 apply (rule basis_fun_lemma, erule g_mono) |
370 apply (rule extension_lemma, erule g_mono) |
371 apply (erule imageI) |
371 apply (erule imageI) |
372 done |
372 done |
373 |
373 |
374 lemma cont_basis_fun: |
374 lemma cont_extension: |
375 assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b" |
375 assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b" |
376 assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)" |
376 assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)" |
377 shows "cont (\<lambda>x. basis_fun (\<lambda>a. f x a))" |
377 shows "cont (\<lambda>x. extension (\<lambda>a. f x a))" |
378 apply (rule contI2) |
378 apply (rule contI2) |
379 apply (rule monofunI) |
379 apply (rule monofunI) |
380 apply (rule basis_fun_mono, erule f_mono, erule f_mono) |
380 apply (rule extension_mono, erule f_mono, erule f_mono) |
381 apply (erule cont2monofunE [OF f_cont]) |
381 apply (erule cont2monofunE [OF f_cont]) |
382 apply (rule cfun_belowI) |
382 apply (rule cfun_belowI) |
383 apply (rule principal_induct, simp) |
383 apply (rule principal_induct, simp) |
384 apply (simp only: contlub_cfun_fun) |
384 apply (simp only: contlub_cfun_fun) |
385 apply (simp only: basis_fun_principal f_mono) |
385 apply (simp only: extension_principal f_mono) |
386 apply (simp add: cont2contlubE [OF f_cont]) |
386 apply (simp add: cont2contlubE [OF f_cont]) |
387 done |
387 done |
388 |
388 |
389 end |
389 end |
390 |
390 |