# Theory Bifinite

```(*  Title:      HOL/HOLCF/Bifinite.thy
Author:     Brian Huffman
*)

section ‹Profinite and bifinite cpos›

theory Bifinite
imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
begin

default_sort cpo

subsection ‹Chains of finite deflations›

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"

end

subsection ‹Omega-profinite and bifinite domains›

class bifinite = pcpo +
assumes bifinite: "∃(a::nat ⇒ 'a → 'a). approx_chain a"

class profinite = cpo +
assumes profinite: "∃(a::nat ⇒ 'a⇩⊥ → 'a⇩⊥). approx_chain a"

subsection ‹Building approx chains›

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
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 ‹Approx chains for countable discrete types.›

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)
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 -` {..<i})"
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"
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 ‹Class instance proofs›

instance bifinite ⊆ profinite
proof
show "∃(a::nat ⇒ 'a⇩⊥ → 'a⇩⊥). 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 ‹
Types \<^typ>‹'a → 'b› and \<^typ>‹'a u →! 'b› are isomorphic.
›

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

lemma encode_decode_cfun [simp]: "encode_cfun⋅(decode_cfun⋅y) = y"
unfolding encode_cfun_def decode_cfun_def
apply (rule cfun_eqI, case_tac x, simp_all)
done

instance cfun :: (profinite, bifinite) bifinite
proof
obtain a :: "nat ⇒ 'a⇩⊥ → 'a⇩⊥" 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 ‹
Types \<^typ>‹('a * 'b) u› and \<^typ>‹'a u ⊗ 'b u› are isomorphic.
›

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⇩⊥ → 'a⇩⊥" where a: "approx_chain a"
using profinite ..
obtain b :: "nat ⇒ 'b⇩⊥ → 'b⇩⊥" 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)⇩⊥ → ('a × 'b)⇩⊥). 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)⇩⊥ → ('a discr)⇩⊥" 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
```