(* Title: HOL/HOLCF/Library/Defl_Bifinite.thy
Author: Brian Huffman
*)
section \<open>Algebraic deflations are a bifinite domain\<close>
theory Defl_Bifinite
imports HOLCF "HOL-Library.Infinite_Set"
begin
subsection \<open>Lemmas about MOST\<close>
default_sort type
subsection \<open>Eventually constant sequences\<close>
definition
eventually_constant :: "(nat \ 'a) \ bool"
where
"eventually_constant S = (\x. MOST i. S i = x)"
lemma eventually_constant_MOST_MOST:
"eventually_constant S \ (MOST m. MOST n. S n = S m)"
unfolding eventually_constant_def MOST_nat
apply safe
apply (rule_tac x=m in exI, clarify)
apply (rule_tac x=m in exI, clarify)
apply simp
apply fast
done
lemma eventually_constantI: "MOST i. S i = x \ eventually_constant S"
unfolding eventually_constant_def by fast
lemma eventually_constant_comp:
"eventually_constant (\i. S i) \ eventually_constant (\i. f (S i))"
unfolding eventually_constant_def
apply (erule exE, rule_tac x="f x" in exI)
apply (erule MOST_mono, simp)
done
lemma eventually_constant_Suc_iff:
"eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)"
unfolding eventually_constant_def
by (subst MOST_Suc_iff, rule refl)
lemma eventually_constant_SucD:
"eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)"
by (rule eventually_constant_Suc_iff [THEN iffD1])
subsection \<open>Limits of eventually constant sequences\<close>
definition
eventual :: "(nat \ 'a) \ 'a" where
"eventual S = (THE x. MOST i. S i = x)"
lemma eventual_eqI: "MOST i. S i = x \ eventual S = x"
unfolding eventual_def
apply (rule the_equality, assumption)
apply (rename_tac y)
apply (subgoal_tac "MOST i::nat. y = x", simp)
apply (erule MOST_rev_mp)
apply (erule MOST_rev_mp)
apply simp
done
lemma MOST_eq_eventual:
"eventually_constant S \ MOST i. S i = eventual S"
unfolding eventually_constant_def
by (erule exE, simp add: eventual_eqI)
lemma eventual_mem_range:
"eventually_constant S \ eventual S \ range S"
apply (drule MOST_eq_eventual)
apply (simp only: MOST_nat_le, clarify)
apply (drule spec, drule mp, rule order_refl)
apply (erule range_eqI [OF sym])
done
lemma eventually_constant_MOST_iff:
assumes S: "eventually_constant S"
shows "(MOST n. P (S n)) \ P (eventual S)"
apply (subgoal_tac "(MOST n. P (S n)) \ (MOST n::nat. P (eventual S))")
apply simp
apply (rule iffI)
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
apply (erule MOST_mono, force)
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
apply (erule MOST_mono, simp)
done
lemma MOST_eventual:
"\eventually_constant S; MOST n. P (S n)\ \ P (eventual S)"
proof -
assume "eventually_constant S"
hence "MOST n. S n = eventual S"
by (rule MOST_eq_eventual)
moreover assume "MOST n. P (S n)"
ultimately have "MOST n. S n = eventual S \ P (S n)"
by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
hence "MOST n::nat. P (eventual S)"
by (rule MOST_mono) auto
thus ?thesis by simp
qed
lemma eventually_constant_MOST_Suc_eq:
"eventually_constant S \ MOST n. S (Suc n) = S n"
apply (drule MOST_eq_eventual)
apply (frule MOST_Suc_iff [THEN iffD2])
apply (erule MOST_rev_mp)
apply (erule MOST_rev_mp)
apply simp
done
lemma eventual_comp:
"eventually_constant S \ eventual (\i. f (S i)) = f (eventual (\i. S i))"
apply (rule eventual_eqI)
apply (rule MOST_mono)
apply (erule MOST_eq_eventual)
apply simp
done
subsection \<open>Constructing finite deflations by iteration\<close>
default_sort cpo
lemma le_Suc_induct:
assumes le: "i \ j"
assumes step: "\i. P i (Suc i)"
assumes refl: "\i. P i i"
assumes trans: "\i j k. \P i j; P j k\ \ P i k"
shows "P i j"
proof (cases "i = j")
assume "i = j"
thus "P i j" by (simp add: refl)
next
assume "i \ j"
with le have "i < j" by simp
thus "P i j" using step trans by (rule less_Suc_induct)
qed
definition
eventual_iterate :: "('a \ 'a::cpo) \ ('a \ 'a)"
where
"eventual_iterate f = eventual (\n. iterate n\f)"
text \<open>A pre-deflation is like a deflation, but not idempotent.\<close>
locale pre_deflation =
fixes f :: "'a \ 'a::cpo"
assumes below: "\x. f\x \ x"
assumes finite_range: "finite (range (\x. f\x))"
begin
lemma iterate_below: "iterate i\f\x \ x"
by (induct i, simp_all add: below_trans [OF below])
lemma iterate_fixed: "f\x = x \ iterate i\f\x = x"
by (induct i, simp_all)
lemma antichain_iterate_app: "i \ j \ iterate j\f\x \ iterate i\f\x"
apply (erule le_Suc_induct)
apply (simp add: below)
apply (rule below_refl)
apply (erule (1) below_trans)
done
lemma finite_range_iterate_app: "finite (range (\i. iterate i\f\x))"
proof (rule finite_subset)
show "range (\i. iterate i\f\x) \ insert x (range (\x. f\x))"
by (clarify, case_tac i, simp_all)
show "finite (insert x (range (\x. f\x)))"
by (simp add: finite_range)
qed
lemma eventually_constant_iterate_app:
"eventually_constant (\i. iterate i\f\x)"
unfolding eventually_constant_def MOST_nat_le
proof -
let ?Y = "\i. iterate i\f\x"
have "\j. \k. ?Y j \ ?Y k"
apply (rule finite_range_has_max)
apply (erule antichain_iterate_app)
apply (rule finite_range_iterate_app)
done
then obtain j where j: "\k. ?Y j \ ?Y k" by fast
show "\z m. \n\m. ?Y n = z"
proof (intro exI allI impI)
fix k
assume "j \ k"
hence "?Y k \ ?Y j" by (rule antichain_iterate_app)
also have "?Y j \ ?Y k" by (rule j)
finally show "?Y k = ?Y j" .
qed
qed
lemma eventually_constant_iterate:
"eventually_constant (\n. iterate n\f)"
proof -
have "\y\range (\x. f\x). eventually_constant (\i. iterate i\f\y)"
by (simp add: eventually_constant_iterate_app)
hence "\y\range (\x. f\x). MOST i. MOST j. iterate j\f\y = iterate i\f\y"
unfolding eventually_constant_MOST_MOST .
hence "MOST i. MOST j. \y\range (\x. f\x). iterate j\f\y = iterate i\f\y"
by (simp only: MOST_finite_Ball_distrib [OF finite_range])
hence "MOST i. MOST j. \x. iterate j\f\(f\x) = iterate i\f\(f\x)"
by simp
hence "MOST i. MOST j. \x. iterate (Suc j)\f\x = iterate (Suc i)\f\x"
by (simp only: iterate_Suc2)
hence "MOST i. MOST j. iterate (Suc j)\f = iterate (Suc i)\f"
by (simp only: cfun_eq_iff)
hence "eventually_constant (\i. iterate (Suc i)\f)"
unfolding eventually_constant_MOST_MOST .
thus "eventually_constant (\i. iterate i\f)"
by (rule eventually_constant_SucD)
qed
abbreviation
d :: "'a \ 'a"
where
"d \ eventual_iterate f"
lemma MOST_d: "MOST n. P (iterate n\f) \ P d"
unfolding eventual_iterate_def
using eventually_constant_iterate by (rule MOST_eventual)
lemma f_d: "f\(d\x) = d\x"
apply (rule MOST_d)
apply (subst iterate_Suc [symmetric])
apply (rule eventually_constant_MOST_Suc_eq)
apply (rule eventually_constant_iterate_app)
done
lemma d_fixed_iff: "d\x = x \ f\x = x"
proof
assume "d\x = x"
with f_d [where x=x]
show "f\x = x" by simp
next
assume f: "f\x = x"
have "\n. iterate n\f\x = x"
by (rule allI, rule nat.induct, simp, simp add: f)
hence "MOST n. iterate n\f\x = x"
by (rule ALL_MOST)
thus "d\x = x"
by (rule MOST_d)
qed
lemma finite_deflation_d: "finite_deflation d"
proof
fix x :: 'a
have "d \ range (\n. iterate n\f)"
unfolding eventual_iterate_def
using eventually_constant_iterate
by (rule eventual_mem_range)
then obtain n where n: "d = iterate n\f" ..
have "iterate n\f\(d\x) = d\x"
using f_d by (rule iterate_fixed)
thus "d\(d\x) = d\x"
by (simp add: n)
next
fix x :: 'a
show "d\x \ x"
by (rule MOST_d, simp add: iterate_below)
next
from finite_range
have "finite {x. f\x = x}"
by (rule finite_range_imp_finite_fixes)
thus "finite {x. d\x = x}"
by (simp add: d_fixed_iff)
qed
lemma deflation_d: "deflation d"
using finite_deflation_d
by (rule finite_deflation_imp_deflation)
end
lemma finite_deflation_eventual_iterate:
"pre_deflation d \ finite_deflation (eventual_iterate d)"
by (rule pre_deflation.finite_deflation_d)
lemma pre_deflation_oo:
assumes "finite_deflation d"
assumes f: "\x. f\x \ x"
shows "pre_deflation (d oo f)"
proof
interpret d: finite_deflation d by fact
fix x
show "\x. (d oo f)\x \ x"
by (simp, rule below_trans [OF d.below f])
show "finite (range (\x. (d oo f)\x))"
by (rule finite_subset [OF _ d.finite_range], auto)
qed
lemma eventual_iterate_oo_fixed_iff:
assumes "finite_deflation d"
assumes f: "\x. f\x \ x"
shows "eventual_iterate (d oo f)\x = x \ d\x = x \ f\x = x"
proof -
interpret d: finite_deflation d by fact
let ?e = "d oo f"
interpret e: pre_deflation "d oo f"
using \<open>finite_deflation d\<close> f
by (rule pre_deflation_oo)
let ?g = "eventual (\n. iterate n\?e)"
show ?thesis
apply (subst e.d_fixed_iff)
apply simp
apply safe
apply (erule subst)
apply (rule d.idem)
apply (rule below_antisym)
apply (rule f)
apply (erule subst, rule d.below)
apply simp
done
qed
lemma eventual_mono:
assumes A: "eventually_constant A"
assumes B: "eventually_constant B"
assumes below: "\n. A n \ B n"
shows "eventual A \ eventual B"
proof -
from A have "MOST n. A n = eventual A"
by (rule MOST_eq_eventual)
then have "MOST n. eventual A \ B n"
by (rule MOST_mono) (erule subst, rule below)
with B show "eventual A \ eventual B"
by (rule MOST_eventual)
qed
lemma eventual_iterate_mono:
assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \ g"
shows "eventual_iterate f \ eventual_iterate g"
unfolding eventual_iterate_def
apply (rule eventual_mono)
apply (rule pre_deflation.eventually_constant_iterate [OF f])
apply (rule pre_deflation.eventually_constant_iterate [OF g])
apply (rule monofun_cfun_arg [OF \<open>f \<sqsubseteq> g\<close>])
done
lemma cont2cont_eventual_iterate_oo:
assumes d: "finite_deflation d"
assumes cont: "cont f" and below: "\x y. f x\y \ y"
shows "cont (\x. eventual_iterate (d oo f x))"
(is "cont ?e")
proof (rule contI2)
show "monofun ?e"
apply (rule monofunI)
apply (rule eventual_iterate_mono)
apply (rule pre_deflation_oo [OF d below])
apply (rule pre_deflation_oo [OF d below])
apply (rule monofun_cfun_arg)
apply (erule cont2monofunE [OF cont])
done
next
fix Y :: "nat \ 'b"
assume Y: "chain Y"
with cont have fY: "chain (\i. f (Y i))"
by (rule ch2ch_cont)
assume eY: "chain (\i. ?e (Y i))"
have lub_below: "\x. f (\i. Y i)\x \ x"
by (rule admD [OF _ Y], simp add: cont, rule below)
have "deflation (?e (\i. Y i))"
apply (rule pre_deflation.deflation_d)
apply (rule pre_deflation_oo [OF d lub_below])
done
then show "?e (\i. Y i) \ (\i. ?e (Y i))"
proof (rule deflation.belowI)
fix x :: 'a
assume "?e (\i. Y i)\x = x"
hence "d\x = x" and "f (\i. Y i)\x = x"
by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
hence "(\i. f (Y i)\x) = x"
apply (simp only: cont2contlubE [OF cont Y])
apply (simp only: contlub_cfun_fun [OF fY])
done
have "compact (d\x)"
using d by (rule finite_deflation.compact)
then have "compact x"
using \<open>d\<cdot>x = x\<close> by simp
then have "compact (\i. f (Y i)\x)"
using \<open>(\<Squnion>i. f (Y i)\<cdot>x) = x\<close> by simp
then have "\n. max_in_chain n (\i. f (Y i)\x)"
by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
then obtain n where n: "max_in_chain n (\i. f (Y i)\x)" ..
then have "f (Y n)\x = x"
using \<open>(\<Squnion>i. f (Y i)\<cdot>x) = x\<close> fY by (simp add: maxinch_is_thelub)
with \<open>d\<cdot>x = x\<close> have "?e (Y n)\<cdot>x = x"
by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
moreover have "?e (Y n)\x \ (\i. ?e (Y i)\x)"
by (rule is_ub_thelub, simp add: eY)
ultimately have "x \ (\i. ?e (Y i))\x"
by (simp add: contlub_cfun_fun eY)
also have "(\i. ?e (Y i))\x \ x"
apply (rule deflation.below)
apply (rule admD [OF adm_deflation eY])
apply (rule pre_deflation.deflation_d)
apply (rule pre_deflation_oo [OF d below])
done
finally show "(\i. ?e (Y i))\x = x" ..
qed
qed
subsection \<open>Intersection of algebraic deflations\<close>
default_sort bifinite
definition meet_fin_defl :: "'a fin_defl \ 'a fin_defl \ 'a fin_defl"
where "meet_fin_defl a b =
Abs_fin_defl (eventual_iterate (Rep_fin_defl a oo Rep_fin_defl b))"
lemma Rep_meet_fin_defl:
"Rep_fin_defl (meet_fin_defl a b) =
eventual_iterate (Rep_fin_defl a oo Rep_fin_defl b)"
unfolding meet_fin_defl_def
apply (rule Abs_fin_defl_inverse [simplified])
apply (rule finite_deflation_eventual_iterate)
apply (rule pre_deflation_oo)
apply (rule finite_deflation_Rep_fin_defl)
apply (rule Rep_fin_defl.below)
done
lemma Rep_meet_fin_defl_fixed_iff:
"Rep_fin_defl (meet_fin_defl a b)\x = x \
Rep_fin_defl a\<cdot>x = x \<and> Rep_fin_defl b\<cdot>x = x"
unfolding Rep_meet_fin_defl
apply (rule eventual_iterate_oo_fixed_iff)
apply (rule finite_deflation_Rep_fin_defl)
apply (rule Rep_fin_defl.below)
done
lemma meet_fin_defl_mono:
"\a \ b; c \ d\ \ meet_fin_defl a c \ meet_fin_defl b d"
unfolding below_fin_defl_def
apply (rule Rep_fin_defl.belowI)
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD)
done
lemma meet_fin_defl_below1: "meet_fin_defl a b \ a"
unfolding below_fin_defl_def
apply (rule Rep_fin_defl.belowI)
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD)
done
lemma meet_fin_defl_below2: "meet_fin_defl a b \ b"
unfolding below_fin_defl_def
apply (rule Rep_fin_defl.belowI)
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD)
done
lemma meet_fin_defl_greatest: "\a \ b; a \ c\ \ a \ meet_fin_defl b c"
unfolding below_fin_defl_def
apply (rule Rep_fin_defl.belowI)
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD)
done
definition meet_defl :: "'a defl \ 'a defl \ 'a defl"
where "meet_defl = defl.extension (\a. defl.extension (\b.
defl_principal (meet_fin_defl a b)))"
lemma meet_defl_principal:
"meet_defl\(defl_principal a)\(defl_principal b) =
defl_principal (meet_fin_defl a b)"
unfolding meet_defl_def
by (simp add: defl.extension_principal defl.extension_mono meet_fin_defl_mono)
lemma meet_defl_below1: "meet_defl\a\b \ a"
apply (induct a rule: defl.principal_induct, simp)
apply (induct b rule: defl.principal_induct, simp)
apply (simp add: meet_defl_principal meet_fin_defl_below1)
done
lemma meet_defl_below2: "meet_defl\a\b \ b"
apply (induct a rule: defl.principal_induct, simp)
apply (induct b rule: defl.principal_induct, simp)
apply (simp add: meet_defl_principal meet_fin_defl_below2)
done
lemma meet_defl_greatest: "\a \ b; a \ c\ \ a \ meet_defl\b\c"
apply (induct a rule: defl.principal_induct, simp)
apply (induct b rule: defl.principal_induct, simp)
apply (induct c rule: defl.principal_induct, simp)
apply (simp add: meet_defl_principal meet_fin_defl_greatest)
done
lemma meet_defl_eq2: "b \ a \ meet_defl\a\b = b"
by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest)
interpretation meet_defl: semilattice "\a b. meet_defl\a\b"
by standard
(fast intro: below_antisym meet_defl_greatest
meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+
lemma deflation_meet_defl: "deflation (meet_defl\a)"
apply (rule deflation.intro)
apply (rule meet_defl.left_idem)
apply (rule meet_defl_below2)
done
lemma finite_deflation_meet_defl:
assumes "compact a"
shows "finite_deflation (meet_defl\a)"
proof (rule finite_deflation_intro)
obtain d where a: "a = defl_principal d"
using defl.compact_imp_principal [OF assms] ..
have "finite (defl_set -` Pow (defl_set a))"
apply (rule finite_vimageI)
apply (rule finite_Pow_iff [THEN iffD2])
apply (simp add: defl_set_def a cast_defl_principal Abs_fin_defl_inverse)
apply (rule Rep_fin_defl.finite_fixes)
apply (rule injI)
apply (simp add: po_eq_conv defl_set_subset_iff [symmetric])
done
hence "finite (range (\b. meet_defl\a\b))"
apply (rule rev_finite_subset)
apply (clarsimp, erule rev_subsetD)
apply (simp add: defl_set_subset_iff meet_defl_below1)
done
thus "finite {b. meet_defl\a\b = b}"
by (rule finite_range_imp_finite_fixes)
qed (rule deflation_meet_defl)
lemma compact_iff_finite_deflation_cast:
"compact d \ finite_deflation (cast\d)"
apply (safe dest!: defl.compact_imp_principal)
apply (simp add: cast_defl_principal finite_deflation_Rep_fin_defl)
apply (rule compact_cast_iff [THEN iffD1])
apply (erule finite_deflation_imp_compact)
done
lemma compact_iff_finite_defl_set:
"compact d \ finite (defl_set d)"
by (simp add: compact_iff_finite_deflation_cast defl_set_def
finite_deflation_def deflation_cast finite_deflation_axioms_def)
lemma compact_meet_defl1: "compact a \ compact (meet_defl\a\b)"
apply (simp add: compact_iff_finite_defl_set)
apply (erule rev_finite_subset)
apply (simp add: defl_set_subset_iff meet_defl_below1)
done
lemma compact_meet_defl2: "compact b \ compact (meet_defl\a\b)"
by (subst meet_defl.commute, rule compact_meet_defl1)
subsection \<open>Chain of approx functions on algebraic deflations\<close>
context bifinite_approx_chain
begin
definition defl_approx :: "nat \ 'a defl \ 'a defl"
where "defl_approx i = meet_defl\(defl_principal (Abs_fin_defl (approx i)))"
lemma defl_approx: "approx_chain defl_approx"
proof (rule approx_chain.intro)
have chain1: "chain (\i. defl_principal (Abs_fin_defl (approx i)))"
apply (rule chainI)
apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def Abs_fin_defl_inverse)
apply (rule chainE [OF chain_approx])
done
show chain: "chain (\i. defl_approx i)"
unfolding defl_approx_def by (simp add: chain1)
have below: "\i d. defl_approx i\d \ d"
unfolding defl_approx_def by (rule meet_defl_below2)
show "(\i. defl_approx i) = ID"
apply (rule cfun_eqI, rename_tac d, simp)
apply (rule below_antisym)
apply (simp add: contlub_cfun_fun chain)
apply (simp add: lub_below chain below)
apply (simp add: defl_approx_def)
apply (simp add: lub_distribs chain1)
apply (rule meet_defl_greatest [OF _ below_refl])
apply (rule cast_below_imp_below)
apply (simp add: contlub_cfun_arg chain1)
apply (simp add: cast_defl_principal Abs_fin_defl_inverse)
apply (rule cast.below_ID)
done
show "\i. finite_deflation (defl_approx i)"
unfolding defl_approx_def
apply (rule finite_deflation_meet_defl)
apply (rule defl.compact_principal)
done
qed
end
subsection \<open>Algebraic deflations are a bifinite domain\<close>
instance defl :: (bifinite) bifinite
proof
obtain a :: "nat \ 'a \ 'a" where "approx_chain a"
using bifinite ..
hence "bifinite_approx_chain a"
unfolding bifinite_approx_chain_def .
thus "\(a::nat \ 'a defl \ 'a defl). approx_chain a"
by (fast intro: bifinite_approx_chain.defl_approx)
qed
subsection \<open>Algebraic deflations are representable\<close>
default_sort "domain"
definition defl_emb :: "udom defl \ udom"
where "defl_emb = udom_emb (bifinite_approx_chain.defl_approx udom_approx)"
definition defl_prj :: "udom \ udom defl"
where "defl_prj = udom_prj (bifinite_approx_chain.defl_approx udom_approx)"
lemma ep_pair_defl: "ep_pair defl_emb defl_prj"
unfolding defl_emb_def defl_prj_def
apply (rule ep_pair_udom)
apply (rule bifinite_approx_chain.defl_approx)
apply (simp add: bifinite_approx_chain_def)
done
text "Deflation combinator for deflation type constructor"
definition defl_defl :: "udom defl \ udom defl"
where defl_deflation_def:
"defl_defl = defl.extension (\a. defl_principal
(Abs_fin_defl (defl_emb oo meet_defl\<cdot>(defl_principal a) oo defl_prj)))"
lemma cast_defl_defl:
"cast\(defl_defl\a) = defl_emb oo meet_defl\a oo defl_prj"
apply (induct a rule: defl.principal_induct, simp)
apply (subst defl_deflation_def)
apply (subst defl.extension_principal)
apply (simp add: below_fin_defl_def Abs_fin_defl_inverse
ep_pair.finite_deflation_e_d_p ep_pair_defl
finite_deflation_meet_defl monofun_cfun)
apply (simp add: cast_defl_principal
below_fin_defl_def Abs_fin_defl_inverse
ep_pair.finite_deflation_e_d_p ep_pair_defl
finite_deflation_meet_defl monofun_cfun)
done
definition defl_map_emb :: "'a::domain defl \ udom defl"
where "defl_map_emb = defl_fun1 emb prj ID"
definition defl_map_prj :: "udom defl \ 'a::domain defl"
where "defl_map_prj = defl.extension (\a. defl_principal (Abs_fin_defl (prj oo cast\(meet_defl\DEFL('a)\(defl_principal a)) oo emb)))"
lemma defl_map_emb_principal:
"defl_map_emb\(defl_principal a) =
defl_principal (Abs_fin_defl (emb oo Rep_fin_defl a oo prj))"
unfolding defl_map_emb_def defl_fun1_def
apply (subst defl.extension_principal)
apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def Abs_fin_defl_inverse monofun_cfun
domain.finite_deflation_e_d_p finite_deflation_Rep_fin_defl)
apply simp
done
lemma defl_map_prj_principal:
"(defl_map_prj\(defl_principal a) :: 'a::domain defl) =
defl_principal (Abs_fin_defl (prj oo cast\<cdot>(meet_defl\<cdot>DEFL('a)\<cdot>(defl_principal a)) oo emb))"
unfolding defl_map_prj_def
apply (rule defl.extension_principal)
apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def)
apply (subst Abs_fin_defl_inverse, simp)
apply (rule domain.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (simp add: compact_meet_defl2)
apply (subst emb_prj)
apply (intro monofun_cfun below_refl meet_defl_below1)
apply (subst Abs_fin_defl_inverse, simp)
apply (rule domain.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (simp add: compact_meet_defl2)
apply (subst emb_prj)
apply (intro monofun_cfun below_refl meet_defl_below1)
apply (simp add: monofun_cfun below_fin_defl_def)
done
lemma defl_map_prj_defl_map_emb: "defl_map_prj\(defl_map_emb\d) = d"
apply (rule cast_eq_imp_eq)
apply (induct_tac d rule: defl.principal_induct, simp)
apply (subst defl_map_emb_principal)
apply (subst defl_map_prj_principal)
apply (simp add: cast_defl_principal)
apply (subst Abs_fin_defl_inverse, simp)
apply (rule domain.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (simp add: compact_meet_defl2)
apply (subst emb_prj)
apply (intro monofun_cfun below_refl meet_defl_below1)
apply (subst meet_defl_eq2)
apply (rule cast_below_imp_below)
apply (simp add: cast_DEFL)
apply (simp add: cast_defl_principal)
apply (subst Abs_fin_defl_inverse, simp)
apply (rule domain.finite_deflation_e_d_p)
apply (rule finite_deflation_Rep_fin_defl)
apply (rule cfun_belowI, simp)
apply (rule Rep_fin_defl.below)
apply (simp add: cast_defl_principal)
apply (subst Abs_fin_defl_inverse, simp)
apply (rule domain.finite_deflation_e_d_p)
apply (rule finite_deflation_Rep_fin_defl)
apply (simp add: cfun_eqI)
done
lemma defl_map_emb_defl_map_prj:
"defl_map_emb\(defl_map_prj\d :: 'a defl) = meet_defl\DEFL('a)\d"
apply (induct_tac d rule: defl.principal_induct, simp)
apply (subst defl_map_prj_principal)
apply (subst defl_map_emb_principal)
apply (subst Abs_fin_defl_inverse, simp)
apply (rule domain.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (simp add: compact_meet_defl2)
apply (subst emb_prj)
apply (intro monofun_cfun below_refl meet_defl_below1)
apply (rule cast_eq_imp_eq)
apply (subst cast_defl_principal)
apply (simp add: cfcomp1 emb_prj)
apply (subst deflation_below_comp2 [OF deflation_cast deflation_cast])
apply (rule monofun_cfun_arg, rule meet_defl_below1)
apply (subst deflation_below_comp1 [OF deflation_cast deflation_cast])
apply (rule monofun_cfun_arg, rule meet_defl_below1)
apply (simp add: eta_cfun)
apply (rule Abs_fin_defl_inverse, simp)
apply (rule finite_deflation_cast)
apply (rule compact_meet_defl2, simp)
done
lemma ep_pair_defl_map_emb_defl_map_prj:
"ep_pair defl_map_emb defl_map_prj"
apply (rule ep_pair.intro)
apply (rule defl_map_prj_defl_map_emb)
apply (simp add: defl_map_emb_defl_map_prj)
apply (rule meet_defl_below2)
done
instantiation defl :: ("domain") "domain"
begin
definition
"emb = defl_emb oo defl_map_emb"
definition
"prj = defl_map_prj oo defl_prj"
definition
"defl (t::'a defl itself) = defl_defl\DEFL('a)"
definition
"(liftemb :: 'a defl u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ 'a defl u) = u_map\prj"
definition
"liftdefl (t::'a defl itself) = liftdefl_of\DEFL('a defl)"
instance proof
show ep: "ep_pair emb (prj :: udom \ 'a defl)"
unfolding emb_defl_def prj_defl_def
apply (rule ep_pair_comp [OF _ ep_pair_defl])
apply (rule ep_pair_defl_map_emb_defl_map_prj)
done
show "cast\DEFL('a defl) = emb oo (prj :: udom \ 'a defl)"
unfolding defl_defl_def emb_defl_def prj_defl_def
by (simp add: cast_defl_defl cfcomp1 defl_map_emb_defl_map_prj)
qed (fact liftemb_defl_def liftprj_defl_def liftdefl_defl_def)+
end
lemma DEFL_defl [domain_defl_simps]: "DEFL('a defl) = defl_defl\DEFL('a)"
by (rule defl_defl_def)
end
¤ Dauer der Verarbeitung: 0.18 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.
|
