huffman@25903: (* Title: HOLCF/Bifinite.thy
huffman@25903: Author: Brian Huffman
huffman@25903: *)
huffman@25903:
huffman@25903: header {* Bifinite domains and approximation *}
huffman@25903:
huffman@25903: theory Bifinite
huffman@27402: imports Deflation
huffman@25903: begin
huffman@25903:
huffman@26407: subsection {* Omega-profinite and bifinite domains *}
huffman@25903:
haftmann@29614: class profinite =
huffman@26962: fixes approx :: "nat \ 'a \ 'a"
huffman@27310: assumes chain_approx [simp]: "chain approx"
huffman@26962: assumes lub_approx_app [simp]: "(\i. approx i\x) = x"
huffman@26962: assumes approx_idem: "approx i\(approx i\x) = approx i\x"
huffman@26962: assumes finite_fixes_approx: "finite {x. approx i\x = x}"
huffman@25903:
huffman@26962: class bifinite = profinite + pcpo
huffman@25909:
huffman@27402: lemma approx_less: "approx i\x \ x"
huffman@27402: proof -
huffman@27402: have "chain (\i. approx i\x)" by simp
huffman@27402: hence "approx i\x \ (\i. approx i\x)" by (rule is_ub_thelub)
huffman@27402: thus "approx i\x \ x" by simp
huffman@27402: qed
huffman@27402:
huffman@27402: lemma finite_deflation_approx: "finite_deflation (approx i)"
huffman@27402: proof
huffman@27402: fix x :: 'a
huffman@27402: show "approx i\(approx i\x) = approx i\x"
huffman@27402: by (rule approx_idem)
huffman@27402: show "approx i\x \ x"
huffman@27402: by (rule approx_less)
huffman@27402: show "finite {x. approx i\x = x}"
huffman@27402: by (rule finite_fixes_approx)
huffman@27402: qed
huffman@27402:
wenzelm@30729: interpretation approx: finite_deflation "approx i"
huffman@27402: by (rule finite_deflation_approx)
huffman@27402:
ballarin@28234: lemma (in deflation) deflation: "deflation d" ..
ballarin@28234:
huffman@27402: lemma deflation_approx: "deflation (approx i)"
ballarin@28234: by (rule approx.deflation)
huffman@25903:
huffman@27186: lemma lub_approx [simp]: "(\i. approx i) = (\ x. x)"
huffman@25903: by (rule ext_cfun, simp add: contlub_cfun_fun)
huffman@25903:
huffman@27309: lemma approx_strict [simp]: "approx i\\ = \"
huffman@25903: by (rule UU_I, rule approx_less)
huffman@25903:
huffman@25903: lemma approx_approx1:
huffman@27186: "i \ j \ approx i\(approx j\x) = approx i\x"
huffman@27402: apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx])
huffman@25922: apply (erule chain_mono [OF chain_approx])
huffman@25903: done
huffman@25903:
huffman@25903: lemma approx_approx2:
huffman@27186: "j \ i \ approx i\(approx j\x) = approx j\x"
huffman@27402: apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx])
huffman@25922: apply (erule chain_mono [OF chain_approx])
huffman@25903: done
huffman@25903:
huffman@25903: lemma approx_approx [simp]:
huffman@27186: "approx i\(approx j\x) = approx (min i j)\x"
huffman@25903: apply (rule_tac x=i and y=j in linorder_le_cases)
huffman@25903: apply (simp add: approx_approx1 min_def)
huffman@25903: apply (simp add: approx_approx2 min_def)
huffman@25903: done
huffman@25903:
huffman@27402: lemma finite_image_approx: "finite ((\x. approx n\x) ` A)"
huffman@27402: by (rule approx.finite_image)
huffman@25903:
huffman@27402: lemma finite_range_approx: "finite (range (\x. approx i\x))"
huffman@27402: by (rule approx.finite_range)
huffman@27186:
huffman@27186: lemma compact_approx [simp]: "compact (approx n\x)"
huffman@27402: by (rule approx.compact)
huffman@25903:
huffman@27309: lemma profinite_compact_eq_approx: "compact x \ \i. approx i\x = x"
huffman@27402: by (rule admD2, simp_all)
huffman@25903:
huffman@27309: lemma profinite_compact_iff: "compact x \ (\n. approx n\x = x)"
huffman@25903: apply (rule iffI)
huffman@27309: apply (erule profinite_compact_eq_approx)
huffman@25903: apply (erule exE)
huffman@25903: apply (erule subst)
huffman@25903: apply (rule compact_approx)
huffman@25903: done
huffman@25903:
huffman@25903: lemma approx_induct:
huffman@25903: assumes adm: "adm P" and P: "\n x. P (approx n\x)"
huffman@27186: shows "P x"
huffman@25903: proof -
huffman@25903: have "P (\n. approx n\x)"
huffman@25903: by (rule admD [OF adm], simp, simp add: P)
huffman@25903: thus "P x" by simp
huffman@25903: qed
huffman@25903:
huffman@27309: lemma profinite_less_ext: "(\i. approx i\x \ approx i\y) \ x \ y"
huffman@25903: apply (subgoal_tac "(\i. approx i\x) \ (\i. approx i\y)", simp)
huffman@25923: apply (rule lub_mono, simp, simp, simp)
huffman@25903: done
huffman@25903:
huffman@25903: subsection {* Instance for continuous function space *}
huffman@25903:
huffman@27402: lemma finite_range_cfun_lemma:
huffman@27402: assumes a: "finite (range (\x. a\x))"
huffman@27402: assumes b: "finite (range (\y. b\y))"
huffman@27402: shows "finite (range (\f. \ x. b\(f\(a\x))))" (is "finite (range ?h)")
huffman@27402: proof (rule finite_imageD)
huffman@27402: let ?f = "\g. range (\x. (a\x, g\x))"
huffman@27402: show "finite (?f ` range ?h)"
huffman@27402: proof (rule finite_subset)
huffman@27402: let ?B = "Pow (range (\x. a\x) \ range (\y. b\y))"
huffman@27402: show "?f ` range ?h \ ?B"
huffman@27402: by clarsimp
huffman@27402: show "finite ?B"
huffman@27402: by (simp add: a b)
huffman@27402: qed
huffman@27402: show "inj_on ?f (range ?h)"
huffman@27402: proof (rule inj_onI, rule ext_cfun, clarsimp)
huffman@27402: fix x f g
huffman@27402: assume "range (\x. (a\x, b\(f\(a\x)))) = range (\x. (a\x, b\(g\(a\x))))"
huffman@27402: hence "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\x))))"
huffman@27402: by (rule equalityD1)
huffman@27402: hence "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))"
huffman@27402: by (simp add: subset_eq)
huffman@27402: then obtain y where "(a\x, b\(f\(a\x))) = (a\y, b\(g\(a\y)))"
huffman@27402: by (rule rangeE)
huffman@27402: thus "b\(f\(a\x)) = b\(g\(a\x))"
huffman@27402: by clarsimp
huffman@27402: qed
huffman@27402: qed
huffman@25903:
huffman@26962: instantiation "->" :: (profinite, profinite) profinite
huffman@26962: begin
huffman@25903:
huffman@26962: definition
huffman@25903: approx_cfun_def:
huffman@26962: "approx = (\n. \ f x. approx n\(f\(approx n\x)))"
huffman@25903:
huffman@27402: instance proof
huffman@27402: show "chain (approx :: nat \ ('a \ 'b) \ ('a \ 'b))"
huffman@27402: unfolding approx_cfun_def by simp
huffman@27402: next
huffman@27402: fix x :: "'a \ 'b"
huffman@27402: show "(\i. approx i\x) = x"
huffman@27402: unfolding approx_cfun_def
huffman@27402: by (simp add: lub_distribs eta_cfun)
huffman@27402: next
huffman@27402: fix i :: nat and x :: "'a \ 'b"
huffman@27402: show "approx i\(approx i\x) = approx i\x"
huffman@27402: unfolding approx_cfun_def by simp
huffman@27402: next
huffman@27402: fix i :: nat
huffman@27402: show "finite {x::'a \ 'b. approx i\x = x}"
huffman@27402: apply (rule finite_range_imp_finite_fixes)
huffman@27402: apply (simp add: approx_cfun_def)
huffman@27402: apply (intro finite_range_cfun_lemma finite_range_approx)
huffman@27402: done
huffman@27402: qed
huffman@25903:
huffman@26962: end
huffman@26962:
huffman@26407: instance "->" :: (profinite, bifinite) bifinite ..
huffman@25909:
huffman@25903: lemma approx_cfun: "approx n\f\x = approx n\(f\(approx n\x))"
huffman@25903: by (simp add: approx_cfun_def)
huffman@25903:
huffman@25903: end