(* Title: HOL/HOLCF/Bifinite.thy
Author: Brian Huffman
*)
section \<open>Profinite and bifinite cpos\<close>
theory Bifinite
imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
begin
default_sort cpo
subsection \<open>Chains of finite deflations\<close>
locale approx_chain =
fixes approx :: "nat \ 'a \ 'a"
assumes chain_approx [simp]: "chain (\i. approx i)"
assumes lub_approx [simp]: "(\i. approx i) = ID"
assumes finite_deflation_approx [simp]: "\i. finite_deflation (approx i)"
begin
lemma deflation_approx: "deflation (approx i)"
using finite_deflation_approx by (rule finite_deflation_imp_deflation)
lemma approx_idem: "approx i\(approx i\x) = approx i\x"
using deflation_approx by (rule deflation.idem)
lemma approx_below: "approx i\x \ x"
using deflation_approx by (rule deflation.below)
lemma finite_range_approx: "finite (range (\x. approx i\x))"
apply (rule finite_deflation.finite_range)
apply (rule finite_deflation_approx)
done
lemma compact_approx [simp]: "compact (approx n\x)"
apply (rule finite_deflation.compact)
apply (rule finite_deflation_approx)
done
lemma compact_eq_approx: "compact x \ \i. approx i\x = x"
by (rule admD2, simp_all)
end
subsection \<open>Omega-profinite and bifinite domains\<close>
class bifinite = pcpo +
assumes bifinite: "\(a::nat \ 'a \ 'a). approx_chain a"
class profinite = cpo +
assumes profinite: "\(a::nat \ 'a\<^sub>\ \ 'a\<^sub>\). approx_chain a"
subsection \<open>Building approx chains\<close>
lemma approx_chain_iso:
assumes a: "approx_chain a"
assumes [simp]: "\x. f\(g\x) = x"
assumes [simp]: "\y. g\(f\y) = y"
shows "approx_chain (\i. f oo a i oo g)"
proof -
have 1: "f oo g = ID" by (simp add: cfun_eqI)
have 2: "ep_pair f g" by (simp add: ep_pair_def)
from 1 2 show ?thesis
using a unfolding approx_chain_def
by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
qed
lemma approx_chain_u_map:
assumes "approx_chain a"
shows "approx_chain (\i. u_map\(a i))"
using assms unfolding approx_chain_def
by (simp add: lub_APP u_map_ID finite_deflation_u_map)
lemma approx_chain_sfun_map:
assumes "approx_chain a" and "approx_chain b"
shows "approx_chain (\i. sfun_map\(a i)\(b i))"
using assms unfolding approx_chain_def
by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
lemma approx_chain_sprod_map:
assumes "approx_chain a" and "approx_chain b"
shows "approx_chain (\i. sprod_map\(a i)\(b i))"
using assms unfolding approx_chain_def
by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
lemma approx_chain_ssum_map:
assumes "approx_chain a" and "approx_chain b"
shows "approx_chain (\i. ssum_map\(a i)\(b i))"
using assms unfolding approx_chain_def
by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
lemma approx_chain_cfun_map:
assumes "approx_chain a" and "approx_chain b"
shows "approx_chain (\i. cfun_map\(a i)\(b i))"
using assms unfolding approx_chain_def
by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
lemma approx_chain_prod_map:
assumes "approx_chain a" and "approx_chain b"
shows "approx_chain (\i. prod_map\(a i)\(b i))"
using assms unfolding approx_chain_def
by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
text \<open>Approx chains for countable discrete types.\<close>
definition discr_approx :: "nat \ 'a::countable discr u \ 'a discr u"
where "discr_approx = (\i. \(up\x). if to_nat (undiscr x) < i then up\x else \)"
lemma chain_discr_approx [simp]: "chain discr_approx"
unfolding discr_approx_def
by (rule chainI, simp add: monofun_cfun monofun_LAM)
lemma lub_discr_approx [simp]: "(\i. discr_approx i) = ID"
apply (rule cfun_eqI)
apply (simp add: contlub_cfun_fun)
apply (simp add: discr_approx_def)
subgoal for x
apply (cases x)
apply simp
apply (rule lub_eqI)
apply (rule is_lubI)
apply (rule ub_rangeI, simp)
apply (drule ub_rangeD)
apply (erule rev_below_trans)
apply simp
apply (rule lessI)
done
done
lemma inj_on_undiscr [simp]: "inj_on undiscr A"
using Discr_undiscr by (rule inj_on_inverseI)
lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
proof
fix x :: "'a discr u"
show "discr_approx i\x \ x"
unfolding discr_approx_def
by (cases x, simp, simp)
show "discr_approx i\(discr_approx i\x) = discr_approx i\x"
unfolding discr_approx_def
by (cases x, simp, simp)
show "finite {x::'a discr u. discr_approx i\x = x}"
proof (rule finite_subset)
let ?S = "insert (\::'a discr u) ((\x. up\x) ` undiscr -` to_nat -` {..
show "{x::'a discr u. discr_approx i\x = x} \ ?S"
unfolding discr_approx_def
by (rule subsetI, case_tac x, simp, simp split: if_split_asm)
show "finite ?S"
by (simp add: finite_vimageI)
qed
qed
lemma discr_approx: "approx_chain discr_approx"
using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
by (rule approx_chain.intro)
subsection \<open>Class instance proofs\<close>
instance bifinite \<subseteq> profinite
proof
show "\(a::nat \ 'a\<^sub>\ \ 'a\<^sub>\). approx_chain a"
using bifinite [where 'a='a]
by (fast intro!: approx_chain_u_map)
qed
instance u :: (profinite) bifinite
by standard (rule profinite)
text \<open>
Types \<^typ>\<open>'a \<rightarrow> 'b\<close> and \<^typ>\<open>'a u \<rightarrow>! 'b\<close> are isomorphic.
\<close>
definition "encode_cfun = (\ f. sfun_abs\(fup\f))"
definition "decode_cfun = (\ g x. sfun_rep\g\(up\x))"
lemma decode_encode_cfun [simp]: "decode_cfun\(encode_cfun\x) = x"
unfolding encode_cfun_def decode_cfun_def
by (simp add: eta_cfun)
lemma encode_decode_cfun [simp]: "encode_cfun\(decode_cfun\y) = y"
unfolding encode_cfun_def decode_cfun_def
apply (simp add: sfun_eq_iff strictify_cancel)
apply (rule cfun_eqI, case_tac x, simp_all)
done
instance cfun :: (profinite, bifinite) bifinite
proof
obtain a :: "nat \ 'a\<^sub>\ \ 'a\<^sub>\" where a: "approx_chain a"
using profinite ..
obtain b :: "nat \ 'b \ 'b" where b: "approx_chain b"
using bifinite ..
have "approx_chain (\i. decode_cfun oo sfun_map\(a i)\(b i) oo encode_cfun)"
using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
thus "\(a::nat \ ('a \ 'b) \ ('a \ 'b)). approx_chain a"
by - (rule exI)
qed
text \<open>
Types \<^typ>\<open>('a * 'b) u\<close> and \<^typ>\<open>'a u \<otimes> 'b u\<close> are isomorphic.
\<close>
definition "encode_prod_u = (\(up\(x, y)). (:up\x, up\y:))"
definition "decode_prod_u = (\(:up\x, up\y:). up\(x, y))"
lemma decode_encode_prod_u [simp]: "decode_prod_u\(encode_prod_u\x) = x"
unfolding encode_prod_u_def decode_prod_u_def
apply (cases x)
apply simp
subgoal for y by (cases y) simp
done
lemma encode_decode_prod_u [simp]: "encode_prod_u\(decode_prod_u\y) = y"
unfolding encode_prod_u_def decode_prod_u_def
apply (cases y)
apply simp
subgoal for a b
apply (cases a, simp)
apply (cases b, simp, simp)
done
done
instance prod :: (profinite, profinite) profinite
proof
obtain a :: "nat \ 'a\<^sub>\ \ 'a\<^sub>\" where a: "approx_chain a"
using profinite ..
obtain b :: "nat \ 'b\<^sub>\ \ 'b\<^sub>\" where b: "approx_chain b"
using profinite ..
have "approx_chain (\i. decode_prod_u oo sprod_map\(a i)\(b i) oo encode_prod_u)"
using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
thus "\(a::nat \ ('a \ 'b)\<^sub>\ \ ('a \ 'b)\<^sub>\). approx_chain a"
by - (rule exI)
qed
instance prod :: (bifinite, bifinite) bifinite
proof
show "\(a::nat \ ('a \ 'b) \ ('a \ 'b)). approx_chain a"
using bifinite [where 'a='a] and bifinite [where 'a='b]
by (fast intro!: approx_chain_prod_map)
qed
instance sfun :: (bifinite, bifinite) bifinite
proof
show "\(a::nat \ ('a \! 'b) \ ('a \! 'b)). approx_chain a"
using bifinite [where 'a='a] and bifinite [where 'a='b]
by (fast intro!: approx_chain_sfun_map)
qed
instance sprod :: (bifinite, bifinite) bifinite
proof
show "\(a::nat \ ('a \ 'b) \ ('a \ 'b)). approx_chain a"
using bifinite [where 'a='a] and bifinite [where 'a='b]
by (fast intro!: approx_chain_sprod_map)
qed
instance ssum :: (bifinite, bifinite) bifinite
proof
show "\(a::nat \ ('a \ 'b) \ ('a \ 'b)). approx_chain a"
using bifinite [where 'a='a] and bifinite [where 'a='b]
by (fast intro!: approx_chain_ssum_map)
qed
lemma approx_chain_unit: "approx_chain (\ :: nat \ unit \ unit)"
by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
instance unit :: bifinite
by standard (fast intro!: approx_chain_unit)
instance discr :: (countable) profinite
by standard (fast intro!: discr_approx)
instance lift :: (countable) bifinite
proof
note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
obtain a :: "nat \ ('a discr)\<^sub>\ \ ('a discr)\<^sub>\" where a: "approx_chain a"
using profinite ..
hence "approx_chain (\i. (\ y. Abs_lift y) oo a i oo (\ x. Rep_lift x))"
by (rule approx_chain_iso) simp_all
thus "\(a::nat \ 'a lift \ 'a lift). approx_chain a"
by - (rule exI)
qed
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
