Theory Fixpoints
section ‹Fixpoints›
text ‹
This theory develops a fixpoint calculus based on partial orders.
Besides fixpoints we consider least prefixpoints and greatest postfixpoints of functions on a partial order.
We do not assume that the underlying structure is complete or that all functions are continuous or isotone.
Assumptions about the existence of fixpoints and necessary properties of the involved functions will be stated explicitly in each theorem.
This way, the results can be instantiated by various structures, such as complete lattices and Kleene algebras, which impose different kinds of restriction.
See, for example, \<^cite>‹"AartsBackhouseBoitenDoornbosGasterenGeldropHoogendijkVoermansWoude1995" and "DaveyPriestley2002"› for fixpoint calculi in complete lattices.
Our fixpoint calculus contains similar rules, in particular:
\begin{itemize}
\item unfold rule,
\item fixpoint operators preserve isotonicity,
\item square rule,
\item rolling rule,
\item various fusion rules,
\item exchange rule and
\item diagonal rule.
\end{itemize}
All of our rules are based on existence rather than completeness of the underlying structure.
We have applied results from this theory in \<^cite>‹"Guttmann2012c"› and subsequent papers for unifying and reasoning about the semantics of recursion in various relational and matrix-based computation models.
›
theory Fixpoints
imports Stone_Algebras.Lattice_Basics
begin
text ‹
The whole calculus is based on partial orders only.
›
context order
begin
text ‹
We first define when an element $x$ is a least/greatest (pre/post)fixpoint of a given function $f$.
›
definition is_fixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_fixpoint f x ≡ f x = x"
definition is_prefixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_prefixpoint f x ≡ f x ≤ x"
definition is_postfixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_postfixpoint f x ≡ f x ≥ x"
definition is_least_fixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_least_fixpoint f x ≡ f x = x ∧ (∀y . f y = y ⟶ x ≤ y)"
definition is_greatest_fixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_greatest_fixpoint f x ≡ f x = x ∧ (∀y . f y = y ⟶ x ≥ y)"
definition is_least_prefixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_least_prefixpoint f x ≡ f x ≤ x ∧ (∀y . f y ≤ y ⟶ x ≤ y)"
definition is_greatest_postfixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ bool" where "is_greatest_postfixpoint f x ≡ f x ≥ x ∧ (∀y . f y ≥ y ⟶ x ≥ y)"
text ‹
Next follows the existence of the corresponding fixpoints for a given function $f$.
›
definition has_fixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_fixpoint f ≡ ∃x . is_fixpoint f x"
definition has_prefixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_prefixpoint f ≡ ∃x . is_prefixpoint f x"
definition has_postfixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_postfixpoint f ≡ ∃x . is_postfixpoint f x"
definition has_least_fixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_least_fixpoint f ≡ ∃x . is_least_fixpoint f x"
definition has_greatest_fixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_greatest_fixpoint f ≡ ∃x . is_greatest_fixpoint f x"
definition has_least_prefixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_least_prefixpoint f ≡ ∃x . is_least_prefixpoint f x"
definition has_greatest_postfixpoint :: "('a ⇒ 'a) ⇒ bool" where "has_greatest_postfixpoint f ≡ ∃x . is_greatest_postfixpoint f x"
text ‹
The actual least/greatest (pre/post)fixpoints of a given function $f$ are extracted by the following operators.
›
definition the_least_fixpoint :: "('a ⇒ 'a) ⇒ 'a" (‹μ _› [201] 200) where "μ f = (THE x . is_least_fixpoint f x)"
definition the_greatest_fixpoint :: "('a ⇒ 'a) ⇒ 'a" (‹ν _› [201] 200) where "ν f = (THE x . is_greatest_fixpoint f x)"
definition the_least_prefixpoint :: "('a ⇒ 'a) ⇒ 'a" (‹pμ _› [201] 200) where "pμ f = (THE x . is_least_prefixpoint f x)"
definition the_greatest_postfixpoint :: "('a ⇒ 'a) ⇒ 'a" (‹pν _› [201] 200) where "pν f = (THE x . is_greatest_postfixpoint f x)"
text ‹
We start with basic consequences of the above definitions.
›
lemma least_fixpoint_unique:
"has_least_fixpoint f ⟹ ∃!x . is_least_fixpoint f x"
using has_least_fixpoint_def is_least_fixpoint_def order.antisym by auto
lemma greatest_fixpoint_unique:
"has_greatest_fixpoint f ⟹ ∃!x . is_greatest_fixpoint f x"
using has_greatest_fixpoint_def is_greatest_fixpoint_def order.antisym by auto
lemma least_prefixpoint_unique:
"has_least_prefixpoint f ⟹ ∃!x . is_least_prefixpoint f x"
using has_least_prefixpoint_def is_least_prefixpoint_def order.antisym by auto
lemma greatest_postfixpoint_unique:
"has_greatest_postfixpoint f ⟹ ∃!x . is_greatest_postfixpoint f x"
using has_greatest_postfixpoint_def is_greatest_postfixpoint_def order.antisym by auto
lemma least_fixpoint:
"has_least_fixpoint f ⟹ is_least_fixpoint f (μ f)"
by (simp add: least_fixpoint_unique theI' the_least_fixpoint_def)
lemma greatest_fixpoint:
"has_greatest_fixpoint f ⟹ is_greatest_fixpoint f (ν f)"
by (simp add: greatest_fixpoint_unique theI' the_greatest_fixpoint_def)
lemma least_prefixpoint:
"has_least_prefixpoint f ⟹ is_least_prefixpoint f (pμ f)"
by (simp add: least_prefixpoint_unique theI' the_least_prefixpoint_def)
lemma greatest_postfixpoint:
"has_greatest_postfixpoint f ⟹ is_greatest_postfixpoint f (pν f)"
by (simp add: greatest_postfixpoint_unique theI' the_greatest_postfixpoint_def)
lemma least_fixpoint_same:
"is_least_fixpoint f x ⟹ x = μ f"
by (simp add: is_least_fixpoint_def order.antisym the_equality the_least_fixpoint_def)
lemma greatest_fixpoint_same:
"is_greatest_fixpoint f x ⟹ x = ν f"
using greatest_fixpoint greatest_fixpoint_unique has_greatest_fixpoint_def by auto
lemma least_prefixpoint_same:
"is_least_prefixpoint f x ⟹ x = pμ f"
using has_least_prefixpoint_def least_prefixpoint least_prefixpoint_unique by blast
lemma greatest_postfixpoint_same:
"is_greatest_postfixpoint f x ⟹ x = pν f"
using greatest_postfixpoint greatest_postfixpoint_unique has_greatest_postfixpoint_def by auto
lemma least_fixpoint_char:
"is_least_fixpoint f x ⟷ has_least_fixpoint f ∧ x = μ f"
using has_least_fixpoint_def least_fixpoint_same by auto
lemma least_prefixpoint_char:
"is_least_prefixpoint f x ⟷ has_least_prefixpoint f ∧ x = pμ f"
using has_least_prefixpoint_def least_prefixpoint_same by auto
lemma greatest_fixpoint_char:
"is_greatest_fixpoint f x ⟷ has_greatest_fixpoint f ∧ x = ν f"
using greatest_fixpoint_same has_greatest_fixpoint_def by auto
lemma greatest_postfixpoint_char:
"is_greatest_postfixpoint f x ⟷ has_greatest_postfixpoint f ∧ x = pν f"
using greatest_postfixpoint_same has_greatest_postfixpoint_def by auto
text ‹
Next come the unfold rules for least/greatest (pre/post)fixpoints.
›
lemma mu_unfold:
"has_least_fixpoint f ⟹ f (μ f) = μ f"
using is_least_fixpoint_def least_fixpoint by auto
lemma pmu_unfold:
"has_least_prefixpoint f ⟹ f (pμ f) ≤ pμ f"
using is_least_prefixpoint_def least_prefixpoint by blast
lemma nu_unfold:
"has_greatest_fixpoint f ⟹ ν f = f (ν f)"
by (metis is_greatest_fixpoint_def greatest_fixpoint)
lemma pnu_unfold:
"has_greatest_postfixpoint f ⟹ pν f ≤ f (pν f)"
using greatest_postfixpoint is_greatest_postfixpoint_def by auto
text ‹
Pre-/postfixpoints of isotone functions are fixpoints.
›
lemma least_prefixpoint_fixpoint:
"has_least_prefixpoint f ⟹ isotone f ⟹ is_least_fixpoint f (pμ f)"
using is_least_fixpoint_def is_least_prefixpoint_def least_prefixpoint order.antisym isotone_def by auto
lemma pmu_mu:
"has_least_prefixpoint f ⟹ isotone f ⟹ pμ f = μ f"
by (simp add: least_fixpoint_same least_prefixpoint_fixpoint)
lemma greatest_postfixpoint_fixpoint:
"has_greatest_postfixpoint f ⟹ isotone f ⟹ is_greatest_fixpoint f (pν f)"
using greatest_postfixpoint is_greatest_fixpoint_def is_greatest_postfixpoint_def order.antisym isotone_def by auto
lemma pnu_nu:
"has_greatest_postfixpoint f ⟹ isotone f ⟹ pν f = ν f"
by (simp add: greatest_fixpoint_same greatest_postfixpoint_fixpoint)
text ‹
The fixpoint operators preserve isotonicity.
›
lemma pmu_isotone:
"has_least_prefixpoint f ⟹ has_least_prefixpoint g ⟹ f ≤≤ g ⟹ pμ f ≤ pμ g"
by (metis is_least_prefixpoint_def least_prefixpoint order_trans lifted_less_eq_def)
lemma mu_isotone:
"has_least_prefixpoint f ⟹ has_least_prefixpoint g ⟹ isotone f ⟹ isotone g ⟹ f ≤≤ g ⟹ μ f ≤ μ g"
using pmu_isotone pmu_mu by fastforce
lemma pnu_isotone:
"has_greatest_postfixpoint f ⟹ has_greatest_postfixpoint g ⟹ f ≤≤ g ⟹ pν f ≤ pν g"
by (metis greatest_postfixpoint is_greatest_postfixpoint_def order_trans lifted_less_eq_def)
lemma nu_isotone:
"has_greatest_postfixpoint f ⟹ has_greatest_postfixpoint g ⟹ isotone f ⟹ isotone g ⟹ f ≤≤ g ⟹ ν f ≤ ν g"
using pnu_isotone pnu_nu by fastforce
text ‹
The square rule for fixpoints of a function applied twice.
›
lemma mu_square:
"isotone f ⟹ has_least_fixpoint f ⟹ has_least_fixpoint (f ∘ f) ⟹ μ f = μ (f ∘ f)"
by (metis (no_types, opaque_lifting) order.antisym is_least_fixpoint_def isotone_def least_fixpoint_char least_fixpoint_unique o_apply)
lemma nu_square:
"isotone f ⟹ has_greatest_fixpoint f ⟹ has_greatest_fixpoint (f ∘ f) ⟹ ν f = ν (f ∘ f)"
by (metis (no_types, opaque_lifting) order.antisym is_greatest_fixpoint_def isotone_def greatest_fixpoint_char greatest_fixpoint_unique o_apply)
text ‹
The rolling rule for fixpoints of the composition of two functions.
›
lemma mu_roll:
assumes "isotone g"
and "has_least_fixpoint (f ∘ g)"
and "has_least_fixpoint (g ∘ f)"
shows "μ (g ∘ f) = g (μ (f ∘ g))"
proof (rule order.antisym)
show "μ (g ∘ f) ≤ g (μ (f ∘ g))"
by (metis assms(2-3) comp_apply is_least_fixpoint_def least_fixpoint)
next
have "is_least_fixpoint (g ∘ f) (μ (g ∘ f))"
by (simp add: assms(3) least_fixpoint)
thus "g (μ (f ∘ g)) ≤ μ (g ∘ f)"
by (metis (no_types) assms(1-2) comp_def is_least_fixpoint_def least_fixpoint isotone_def)
qed
lemma nu_roll:
assumes "isotone g"
and "has_greatest_fixpoint (f ∘ g)"
and "has_greatest_fixpoint (g ∘ f)"
shows "ν (g ∘ f) = g (ν (f ∘ g))"
proof (rule order.antisym)
have 1: "is_greatest_fixpoint (f ∘ g) (ν (f ∘ g))"
by (simp add: assms(2) greatest_fixpoint)
have "is_greatest_fixpoint (g ∘ f) (ν (g ∘ f))"
by (simp add: assms(3) greatest_fixpoint)
thus "ν (g ∘ f) ≤ g (ν (f ∘ g))"
using 1 by (metis (no_types) assms(1) comp_def is_greatest_fixpoint_def isotone_def)
next
show "g (ν (f ∘ g)) ≤ ν (g ∘ f)"
by (metis assms(2-3) comp_apply greatest_fixpoint is_greatest_fixpoint_def)
qed
text ‹
Least (pre)fixpoints are below greatest (post)fixpoints.
›
lemma mu_below_nu:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ μ f ≤ ν f"
using greatest_fixpoint is_greatest_fixpoint_def mu_unfold by auto
lemma pmu_below_pnu_fix:
"has_fixpoint f ⟹ has_least_prefixpoint f ⟹ has_greatest_postfixpoint f ⟹ pμ f ≤ pν f"
by (metis greatest_postfixpoint has_fixpoint_def is_fixpoint_def is_greatest_postfixpoint_def is_least_prefixpoint_def least_prefixpoint order_refl order_trans)
lemma pmu_below_pnu_iso:
"isotone f ⟹ has_least_prefixpoint f ⟹ has_greatest_postfixpoint f ⟹ pμ f ≤ pν f"
using greatest_postfixpoint_fixpoint is_greatest_fixpoint_def is_least_fixpoint_def least_prefixpoint_fixpoint by auto
text ‹
Several variants of the fusion rule for fixpoints follow.
›
lemma mu_fusion_1:
assumes "galois l u"
and "isotone h"
and "has_least_prefixpoint g"
and "has_least_fixpoint h"
and "l (g (u (μ h))) ≤ h (l (u (μ h)))"
shows "l (pμ g) ≤ μ h"
proof -
have "l (g (u (μ h))) ≤ μ h"
by (metis assms(1,2,4,5) galois_char isotone_def order_lesseq_imp mu_unfold)
thus "l (pμ g) ≤ μ h"
using assms(1,3) is_least_prefixpoint_def least_prefixpoint galois_def by auto
qed
lemma mu_fusion_2:
"galois l u ⟹ isotone h ⟹ has_least_prefixpoint g ⟹ has_least_fixpoint h ⟹ l ∘ g ≤≤ h ∘ l ⟹ l (pμ g) ≤ μ h"
by (simp add: mu_fusion_1 lifted_less_eq_def)
lemma mu_fusion_equal_1:
"galois l u ⟹ isotone g ⟹ isotone h ⟹ has_least_prefixpoint g ⟹ has_least_fixpoint h ⟹ l (g (u (μ h))) ≤ h(l(u(μ h))) ⟹ l (g (pμ g)) = h (l (pμ g)) ⟹ μ h = l (pμ g) ∧ μ h = l (μ g)"
by (metis order.antisym least_fixpoint least_prefixpoint_fixpoint is_least_fixpoint_def mu_fusion_1 pmu_mu)
lemma mu_fusion_equal_2:
"galois l u ⟹ isotone h ⟹ has_least_prefixpoint g ⟹ has_least_prefixpoint h ⟹ l (g (u (μ h))) ≤ h (l (u (μ h))) ∧ l (g (pμ g)) = h (l (pμ g)) ⟶ pμ h = l (pμ g) ∧ μ h = l (pμ g)"
by (metis is_least_prefixpoint_def least_fixpoint_char least_prefixpoint least_prefixpoint_fixpoint order.antisym galois_char isotone_def mu_fusion_1)
lemma mu_fusion_equal_3:
assumes "galois l u"
and "isotone g"
and "isotone h"
and "has_least_prefixpoint g"
and "has_least_fixpoint h"
and "l ∘ g = h ∘ l"
shows "μ h = l (pμ g)"
and "μ h = l (μ g)"
proof -
have "∀x . l (g x) = h (l x)"
using assms(6) comp_eq_elim by blast
thus "μ h = l (pμ g)"
using assms(1-5) mu_fusion_equal_1 by auto
thus "μ h = l (μ g)"
by (simp add: assms(2,4) pmu_mu)
qed
lemma mu_fusion_equal_4:
assumes "galois l u"
and "isotone h"
and "has_least_prefixpoint g"
and "has_least_prefixpoint h"
and "l ∘ g = h ∘ l"
shows "pμ h = l (pμ g)"
and "μ h = l (pμ g)"
proof -
have "∀x . l (g x) = h (l x)"
using assms(5) comp_eq_elim by blast
thus "pμ h = l (pμ g)"
using assms(1-4) mu_fusion_equal_2 by auto
thus "μ h = l (pμ g)"
by (simp add: assms(2,4) pmu_mu)
qed
lemma nu_fusion_1:
assumes "galois l u"
and "isotone h"
and "has_greatest_postfixpoint g"
and "has_greatest_fixpoint h"
and "h (u (l (ν h))) ≤ u (g (l (ν h)))"
shows "ν h ≤ u (pν g)"
proof -
have "ν h ≤ u (g (l (ν h)))"
by (metis assms(1,2,4,5) order_trans galois_char isotone_def nu_unfold)
thus "ν h ≤ u (pν g)"
by (metis assms(1,3) greatest_postfixpoint is_greatest_postfixpoint_def ord.galois_def)
qed
lemma nu_fusion_2:
"galois l u ⟹ isotone h ⟹ has_greatest_postfixpoint g ⟹ has_greatest_fixpoint h ⟹ h ∘ u ≤≤ u ∘ g ⟹ ν h ≤ u (pν g)"
by (simp add: nu_fusion_1 lifted_less_eq_def)
lemma nu_fusion_equal_1:
"galois l u ⟹ isotone g ⟹ isotone h ⟹ has_greatest_postfixpoint g ⟹ has_greatest_fixpoint h ⟹ h (u (l (ν h))) ≤ u (g (l (ν h))) ⟹ h (u (pν g)) = u (g (pν g)) ⟹ ν h = u (pν g) ∧ ν h = u (ν g)"
by (metis greatest_fixpoint_char greatest_postfixpoint_fixpoint is_greatest_fixpoint_def order.antisym nu_fusion_1)
lemma nu_fusion_equal_2:
"galois l u ⟹ isotone h ⟹ has_greatest_postfixpoint g ⟹ has_greatest_postfixpoint h ⟹ h (u (l (ν h))) ≤ u (g (l (ν h))) ∧ h (u (pν g)) = u (g (pν g)) ⟹ pν h = u (pν g) ∧ ν h = u (pν g)"
by (metis greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint is_greatest_postfixpoint_def order.antisym galois_char nu_fusion_1 isotone_def)
lemma nu_fusion_equal_3:
assumes "galois l u"
and "isotone g"
and "isotone h"
and "has_greatest_postfixpoint g"
and "has_greatest_fixpoint h"
and "h ∘ u = u ∘ g"
shows "ν h = u (pν g)"
and "ν h = u (ν g)"
proof -
have "∀x . u (g x) = h (u x)"
using assms(6) comp_eq_dest by fastforce
thus "ν h = u (pν g)"
using assms(1-5) nu_fusion_equal_1 by auto
thus "ν h = u (ν g)"
by (simp add: assms(2-4) pnu_nu)
qed
lemma nu_fusion_equal_4:
assumes "galois l u"
and "isotone h"
and "has_greatest_postfixpoint g"
and "has_greatest_postfixpoint h"
and "h ∘ u = u ∘ g"
shows "pν h = u (pν g)"
and "ν h = u (pν g)"
proof -
have "∀x . u (g x) = h (u x)"
using assms(5) comp_eq_dest by fastforce
thus "pν h = u (pν g)"
using assms(1-4) nu_fusion_equal_2 by auto
thus "ν h = u (pν g)"
by (simp add: assms(2,4) pnu_nu)
qed
text ‹
Next come the exchange rules for replacing the first/second function in a composition.
›
lemma mu_exchange_1:
assumes "galois l u"
and "isotone g"
and "isotone h"
and "has_least_prefixpoint (l ∘ h)"
and "has_least_prefixpoint (h ∘ g)"
and "has_least_fixpoint (g ∘ h)"
and "l ∘ h ∘ g ≤≤ g ∘ h ∘ l"
shows "μ (l ∘ h) ≤ μ (g ∘ h)"
proof -
have 1: "l ∘ (h ∘ g) ≤≤ (g ∘ h) ∘ l"
by (simp add: assms(7) rewriteL_comp_comp)
have "(l ∘ h) (μ (g ∘ h)) = l (μ (h ∘ g))"
by (metis assms(2,3,5,6) comp_apply least_fixpoint_char least_prefixpoint_fixpoint isotone_def mu_roll)
also have "... ≤ μ (g ∘ h)"
using 1 by (metis assms(1-3,5,6) comp_apply least_fixpoint_char least_prefixpoint_fixpoint isotone_def mu_fusion_2)
finally have "pμ (l ∘ h) ≤ μ (g ∘ h)"
using assms(4) is_least_prefixpoint_def least_prefixpoint by blast
thus "μ (l ∘ h) ≤ μ (g ∘ h)"
by (metis assms(1,3,4) galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint o_apply)
qed
lemma mu_exchange_2:
assumes "galois l u"
and "isotone g"
and "isotone h"
and "has_least_prefixpoint (l ∘ h)"
and "has_least_prefixpoint (h ∘ l)"
and "has_least_prefixpoint (h ∘ g)"
and "has_least_fixpoint (g ∘ h)"
and "has_least_fixpoint (h ∘ g)"
and "l ∘ h ∘ g ≤≤ g ∘ h ∘ l"
shows "μ (h ∘ l) ≤ μ (h ∘ g)"
proof -
have "μ (h ∘ l) = h (μ (l ∘ h))"
by (metis (no_types, lifting) assms(1,3-5) galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint mu_roll o_apply)
also have "... ≤ h (μ (g ∘ h))"
using assms(1-4,6,7,9) isotone_def mu_exchange_1 by blast
also have "... = μ (h ∘ g)"
by (simp add: assms(3,7,8) mu_roll)
finally show ?thesis
.
qed
lemma mu_exchange_equal:
assumes "galois l u"
and "galois k t"
and "isotone h"
and "has_least_prefixpoint (l ∘ h)"
and "has_least_prefixpoint (h ∘ l)"
and "has_least_prefixpoint (k ∘ h)"
and "has_least_prefixpoint (h ∘ k)"
and "l ∘ h ∘ k = k ∘ h ∘ l"
shows "μ (l ∘ h) = μ (k ∘ h)"
and "μ (h ∘ l) = μ (h ∘ k)"
proof -
have 1: "has_least_fixpoint (k ∘ h)"
using assms(2,3,6) least_fixpoint_char least_prefixpoint_fixpoint galois_char isotone_def by auto
have 2: "has_least_fixpoint (h ∘ k)"
using assms(2,3,7) least_fixpoint_char least_prefixpoint_fixpoint galois_char isotone_def by auto
have 3: "has_least_fixpoint (l ∘ h)"
using assms(1,3,4) least_fixpoint_char least_prefixpoint_fixpoint galois_char isotone_def by auto
have 4: "has_least_fixpoint (h ∘ l)"
using assms(1,3,5) least_fixpoint_char least_prefixpoint_fixpoint galois_char isotone_def by auto
show "μ (h ∘ l) = μ (h ∘ k)"
using 1 2 3 4 assms order.antisym galois_char lifted_reflexive mu_exchange_2 by auto
show "μ (l ∘ h) = μ (k ∘ h)"
using 1 2 3 4 assms order.antisym galois_char lifted_reflexive mu_exchange_1 by auto
qed
lemma nu_exchange_1:
assumes "galois l u"
and "isotone g"
and "isotone h"
and "has_greatest_postfixpoint (u ∘ h)"
and "has_greatest_postfixpoint (h ∘ g)"
and "has_greatest_fixpoint (g ∘ h)"
and "g ∘ h ∘ u ≤≤ u ∘ h ∘ g"
shows "ν (g ∘ h) ≤ ν (u ∘ h)"
proof -
have "(g ∘ h) ∘ u ≤≤ u ∘ (h ∘ g)"
by (simp add: assms(7) o_assoc)
hence "ν (g ∘ h) ≤ u (ν (h ∘ g))"
by (metis assms(1-3,5,6) greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def nu_fusion_2 o_apply)
also have "... = (u ∘ h) (ν (g ∘ h))"
by (metis assms(2,3,5,6) greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def nu_roll o_apply)
finally have "ν (g ∘ h) ≤ pν (u ∘ h)"
using assms(4) greatest_postfixpoint is_greatest_postfixpoint_def by blast
thus "ν (g ∘ h) ≤ ν (u ∘ h)"
using assms(1,3,4) galois_char greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def by auto
qed
lemma nu_exchange_2:
assumes "galois l u"
and "isotone g"
and "isotone h"
and "has_greatest_postfixpoint (u ∘ h)"
and "has_greatest_postfixpoint (h ∘ u)"
and "has_greatest_postfixpoint (h ∘ g)"
and "has_greatest_fixpoint (g ∘ h)"
and "has_greatest_fixpoint (h ∘ g)"
and "g ∘ h ∘ u ≤≤ u ∘ h ∘ g"
shows "ν (h ∘ g) ≤ ν (h ∘ u)"
proof -
have "ν (h ∘ g) = h (ν (g ∘ h))"
by (simp add: assms(3,7,8) nu_roll)
also have "... ≤ h (ν (u ∘ h))"
using assms(1-4,6,7,9) isotone_def nu_exchange_1 by blast
also have "... = ν (h ∘ u)"
by (metis (no_types, lifting) assms(1,3-5) galois_char greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def nu_roll o_apply)
finally show "ν (h ∘ g) ≤ ν (h ∘ u)"
.
qed
lemma nu_exchange_equal:
assumes "galois l u"
and "galois k t"
and "isotone h"
and "has_greatest_postfixpoint (u ∘ h)"
and "has_greatest_postfixpoint (h ∘ u)"
and "has_greatest_postfixpoint (t ∘ h)"
and "has_greatest_postfixpoint (h ∘ t)"
and "u ∘ h ∘ t = t ∘ h ∘ u"
shows "ν (u ∘ h) = ν (t ∘ h)"
and "ν (h ∘ u) = ν (h ∘ t)"
proof -
have 1: "has_greatest_fixpoint (u ∘ h)"
using assms(1,3,4) greatest_fixpoint_char greatest_postfixpoint_fixpoint galois_char isotone_def by auto
have 2: "has_greatest_fixpoint (h ∘ u)"
using assms(1,3,5) greatest_fixpoint_char greatest_postfixpoint_fixpoint galois_char isotone_def by auto
have 3: "has_greatest_fixpoint (t ∘ h)"
using assms(2,3,6) greatest_fixpoint_char greatest_postfixpoint_fixpoint galois_char isotone_def by auto
have 4: "has_greatest_fixpoint (h ∘ t)"
using assms(2,3,7) greatest_fixpoint_char greatest_postfixpoint_fixpoint galois_char isotone_def by auto
show "ν (u ∘ h) = ν (t ∘ h)"
using 1 2 3 4 assms order.antisym galois_char lifted_reflexive nu_exchange_1 by auto
show "ν (h ∘ u) = ν (h ∘ t)"
using 1 2 3 4 assms order.antisym galois_char lifted_reflexive nu_exchange_2 by auto
qed
text ‹
The following results generalise parts of \<^cite>‹‹Exercise 8.27› in "DaveyPriestley2002"› from continuous functions on complete partial orders to the present setting.
›
lemma mu_commute_fixpoint_1:
"isotone f ⟹ has_least_fixpoint (f ∘ g) ⟹ f ∘ g = g ∘ f ⟹ is_fixpoint f (μ (f ∘ g))"
by (metis is_fixpoint_def mu_roll)
lemma mu_commute_fixpoint_2:
"isotone g ⟹ has_least_fixpoint (f ∘ g) ⟹ f ∘ g = g ∘ f ⟹ is_fixpoint g (μ (f ∘ g))"
by (simp add: mu_commute_fixpoint_1)
lemma mu_commute_least_fixpoint:
"isotone f ⟹ isotone g ⟹ has_least_fixpoint f ⟹ has_least_fixpoint g ⟹ has_least_fixpoint (f ∘ g) ⟹ f ∘ g = g ∘ f ⟹ μ (f ∘ g) = μ f ⟹ μ g ≤ μ f"
by (metis is_least_fixpoint_def least_fixpoint mu_roll)
text ‹
The converse of the preceding result is claimed for continuous $f$, $g$ on a complete partial order; it is unknown whether it holds without these additional assumptions.
›
lemma nu_commute_fixpoint_1:
"isotone f ⟹ has_greatest_fixpoint (f ∘ g) ⟹ f ∘ g = g ∘ f ⟹ is_fixpoint f (ν(f ∘ g))"
by (metis is_fixpoint_def nu_roll)
lemma nu_commute_fixpoint_2:
"isotone g ⟹ has_greatest_fixpoint (f ∘ g) ⟹ f ∘ g = g ∘ f ⟹ is_fixpoint g (ν(f ∘ g))"
by (simp add: nu_commute_fixpoint_1)
lemma nu_commute_greatest_fixpoint:
"isotone f ⟹ isotone g ⟹ has_greatest_fixpoint f ⟹ has_greatest_fixpoint g ⟹ has_greatest_fixpoint (f ∘ g) ⟹ f ∘ g = g ∘ f ⟹ ν (f ∘ g) = ν f ⟹ ν f ≤ ν g"
by (metis greatest_fixpoint is_greatest_fixpoint_def nu_roll)
text ‹
Finally, we show a number of versions of the diagonal rule for functions with two arguments.
›
lemma mu_diagonal_1:
assumes "isotone (λx . μ (λy . f x y))"
and "∀x . has_least_fixpoint (λy . f x y)"
and "has_least_prefixpoint (λx . μ (λy . f x y))"
shows "μ (λx . f x x) = μ (λx . μ (λy . f x y))"
proof -
let ?g = "λx . μ (λy . f x y)"
have 1: "is_least_prefixpoint ?g (μ ?g)"
using assms(1,3) least_prefixpoint pmu_mu by fastforce
have "f (μ ?g) (μ ?g) = μ ?g"
by (metis (no_types, lifting) assms is_least_fixpoint_def least_fixpoint_char least_prefixpoint_fixpoint)
hence "is_least_fixpoint (λx . f x x) (μ ?g)"
using 1 assms(2) is_least_fixpoint_def is_least_prefixpoint_def least_fixpoint by auto
thus ?thesis
using least_fixpoint_same by simp
qed
lemma mu_diagonal_2:
"∀x . isotone (λy . f x y) ∧ isotone (λy . f y x) ∧ has_least_prefixpoint (λy . f x y) ⟹ has_least_prefixpoint (λx . μ (λy . f x y)) ⟹ μ (λx . f x x) = μ (λx . μ (λy . f x y))"
apply (rule mu_diagonal_1)
using isotone_def lifted_less_eq_def mu_isotone apply simp
using has_least_fixpoint_def least_prefixpoint_fixpoint apply blast
by simp
lemma nu_diagonal_1:
assumes "isotone (λx . ν (λy . f x y))"
and "∀x . has_greatest_fixpoint (λy . f x y)"
and "has_greatest_postfixpoint (λx . ν (λy . f x y))"
shows "ν (λx . f x x) = ν (λx . ν (λy . f x y))"
proof -
let ?g = "λx . ν (λy . f x y)"
have 1: "is_greatest_postfixpoint ?g (ν ?g)"
using assms(1,3) greatest_postfixpoint pnu_nu by fastforce
have "f (ν ?g) (ν ?g) = ν ?g"
by (metis (no_types, lifting) assms is_greatest_fixpoint_def greatest_fixpoint_char greatest_postfixpoint_fixpoint)
hence "is_greatest_fixpoint (λx . f x x) (ν ?g)"
using 1 assms(2) is_greatest_fixpoint_def is_greatest_postfixpoint_def greatest_fixpoint by auto
thus ?thesis
using greatest_fixpoint_same by simp
qed
lemma nu_diagonal_2:
"∀x . isotone (λy . f x y) ∧ isotone (λy . f y x) ∧ has_greatest_postfixpoint (λy . f x y) ⟹ has_greatest_postfixpoint (λx . ν (λy . f x y)) ⟹ ν (λx . f x x) = ν (λx . ν (λy . f x y))"
apply (rule nu_diagonal_1)
using isotone_def lifted_less_eq_def nu_isotone apply simp
using has_greatest_fixpoint_def greatest_postfixpoint_fixpoint apply blast
by simp
end
end