Theory Galois_Connections
section ‹Galois Connections and Fusion Theorems \label{S:galois}›
theory Galois_Connections
imports Refinement_Lattice
begin
text ‹
The concept of Galois connections is introduced here to prove the fixed-point fusion lemmas.
The definition of Galois connections used is quite simple but encodes a lot of
information.
The material in this section is largely based on the work of the Eindhoven
Mathematics of Program Construction Group \<^cite>‹"fixedpointcalculus1995"›
and the reader is referred to their work for a full explanation of this section.
›
subsection ‹Lower Galois connections›
lemma Collect_2set [simp]: "{F x |x. x = a ∨ x = b} = {F a, F b}"
by auto
locale lower_galois_connections
begin
definition
l_adjoint :: "('a::refinement_lattice ⇒ 'a) ⇒ ('a ⇒ 'a)" ("_⇧♭" [201] 200)
where
"(F⇧♭) x ≡ ⨅{y. x ⊑ F y}"
lemma dist_inf_mono:
assumes distF: "dist_over_inf F"
shows "mono F"
proof
fix x :: 'a and y :: 'a
assume "x ⊑ y"
then have "F x = F (x ⊓ y)" by (simp add: le_iff_inf)
also have "... = F x ⊓ F y"
proof -
from distF
have "F (⨅{x, y}) = ⨅{F x, F y}" by (drule_tac x = "{x, y}" in spec, simp)
then show "F (x ⊓ y) = F x ⊓ F y" by simp
qed
finally show "F x ⊑ F y" by (metis le_iff_inf)
qed
lemma l_cancellation: "dist_over_inf F ⟹ x ⊑ (F ∘ F⇧♭) x"
proof -
assume dist: "dist_over_inf F"
define Y where "Y = {F y | y. x ⊑ F y}"
define X where "X = {x}"
have "(∀ y ∈ Y. (∃ x ∈ X. x ⊑ y))" using X_def Y_def CollectD singletonI by auto
then have "⨅ X ⊑ ⨅ Y" by (simp add: Inf_mono)
then have "x ⊑ ⨅{F y | y. x ⊑ F y}" by (simp add: X_def Y_def)
then have "x ⊑ F (⨅{y. x ⊑ F y})" by (simp add: dist le_INF_iff)
thus ?thesis by (metis comp_def l_adjoint_def)
qed
lemma l_galois_connection: "dist_over_inf F ⟹ ((F⇧♭) x ⊑ y) ⟷ (x ⊑ F y)"
proof
assume "x ⊑ F y"
then have "⨅{y. x ⊑ F y} ⊑ y" by (simp add: Inf_lower)
thus "(F⇧♭) x ⊑ y" by (metis l_adjoint_def)
next
assume dist: "dist_over_inf F" then have monoF: "mono F" by (simp add: dist_inf_mono)
assume "(F⇧♭) x ⊑ y" then have a: "F ((F⇧♭) x) ⊑ F y" by (simp add: monoD monoF)
have "x ⊑ F ((F⇧♭) x)" using dist l_cancellation by simp
thus "x ⊑ F y" using a by auto
qed
lemma v_simple_fusion: "mono G ⟹ ∀x. ((F ∘ G) x ⊑ (H ∘ F) x) ⟹ F (gfp G) ⊑ gfp H"
by (metis comp_eq_dest_lhs gfp_unfold gfp_upperbound)
subsection ‹Greatest fixpoint fusion theorems›
text ‹
Combining lower Galois connections and greatest fixed points allows
elegant proofs of the weak fusion lemmas.
›
theorem fusion_gfp_geq:
assumes monoH: "mono H"
and distribF: "dist_over_inf F"
and comp_geq: "⋀x. ((H ∘ F) x ⊑ (F ∘ G) x)"
shows "gfp H ⊑ F (gfp G)"
proof -
have "(gfp H) ⊑ (F ∘ F⇧♭) (gfp H)" using distribF l_cancellation by simp
then have "H (gfp H) ⊑ H ((F ∘ F⇧♭) (gfp H))" by (simp add: monoD monoH)
then have "H (gfp H) ⊑ F ((G ∘ F⇧♭) (gfp H))" using comp_geq by (metis comp_def refine_trans)
then have "(F⇧♭) (H (gfp H)) ⊑ (G ∘ F⇧♭) (gfp H)" using distribF by (metis (mono_tags) l_galois_connection)
then have "(F⇧♭) (gfp H) ⊑ (gfp G)" by (metis comp_apply gfp_unfold gfp_upperbound monoH)
thus "gfp H ⊑ F (gfp G)" using distribF by (metis (mono_tags) l_galois_connection)
qed
theorem fusion_gfp_eq:
assumes monoH: "mono H" and monoG: "mono G"
and distF: "dist_over_inf F"
and fgh_comp: "⋀x. ((F ∘ G) x = (H ∘ F) x)"
shows "F (gfp G) = gfp H"
proof (rule antisym)
show "F (gfp G) ⊑ (gfp H)" by (metis fgh_comp le_less v_simple_fusion monoG)
next
have "⋀x. ((H ∘ F) x ⊑ (F ∘ G) x)" using fgh_comp by auto
then show "gfp H ⊑ F (gfp G)" using monoH distF fusion_gfp_geq by blast
qed
end
subsection ‹Upper Galois connections›
locale upper_galois_connections
begin
definition
u_adjoint :: "('a::refinement_lattice ⇒ 'a) ⇒ ('a ⇒ 'a)" ("_⇧#" [201] 200)
where
"(F⇧#) x ≡ ⨆{y. F y ⊑ x}"
lemma dist_sup_mono:
assumes distF: "dist_over_sup F"
shows "mono F"
proof
fix x :: 'a and y :: 'a
assume "x ⊑ y"
then have "F y = F (x ⊔ y)" by (simp add: le_iff_sup)
also have "... = F x ⊔ F y"
proof -
from distF
have "F (⨆{x, y}) = ⨆{F x, F y}" by (drule_tac x = "{x, y}" in spec, simp)
then show "F (x ⊔ y) = F x ⊔ F y" by simp
qed
finally show "F x ⊑ F y" by (metis le_iff_sup)
qed
lemma u_cancellation: "dist_over_sup F ⟹ (F ∘ F⇧#) x ⊑ x"
proof -
assume dist: "dist_over_sup F"
define Y where "Y = {F y | y. F y ⊑ x}"
define X where "X = {x}"
have "(∀ y ∈ Y. (∃ x ∈ X. y ⊑ x))" using X_def Y_def CollectD singletonI by auto
then have "⨆ Y ⊑ ⨆ X" by (simp add: Sup_mono)
then have "⨆{F y | y. F y ⊑ x} ⊑ x" by (simp add: X_def Y_def)
then have "F (⨆{y. F y ⊑ x}) ⊑ x" using SUP_le_iff dist by fastforce
thus ?thesis by (metis comp_def u_adjoint_def)
qed
lemma u_galois_connection: "dist_over_sup F ⟹ (F x ⊑ y) ⟷ (x ⊑ (F⇧#) y)"
proof
assume dist: "dist_over_sup F" then have monoF: "mono F" by (simp add: dist_sup_mono)
assume "x ⊑ (F⇧#) y" then have a: "F x ⊑ F ((F⇧#) y)" by (simp add: monoD monoF)
have "F ((F⇧#) y) ⊑ y" using dist u_cancellation by simp
thus "F x ⊑ y" using a by auto
next
assume "F x ⊑ y"
then have "x ⊑ ⨆{x. F x ⊑ y}" by (simp add: Sup_upper)
thus "x ⊑ (F⇧#) y" by (metis u_adjoint_def)
qed
lemma u_simple_fusion: "mono H ⟹ ∀x. ((F ∘ G) x ⊑ (G ∘ H) x) ⟹ lfp F ⊑ G (lfp H)"
by (metis comp_def lfp_lowerbound lfp_unfold)
subsection ‹Least fixpoint fusion theorems›
text ‹
Combining upper Galois connections and least fixed points allows elegant proofs
of the strong fusion lemmas.
›
theorem fusion_lfp_leq:
assumes monoH: "mono H"
and distribF: "dist_over_sup F"
and comp_leq: "⋀x. ((F ∘ G) x ⊑ (H ∘ F) x)"
shows "F (lfp G) ⊑ (lfp H)"
proof -
have "((F ∘ F⇧#) (lfp H)) ⊑ lfp H" using distribF u_cancellation by simp
then have "H ((F ∘ F⇧#) (lfp H)) ⊑ H (lfp H)" by (simp add: monoD monoH)
then have "F ((G ∘ F⇧#) (lfp H)) ⊑ H (lfp H)" using comp_leq by (metis comp_def refine_trans)
then have "(G ∘ F⇧#) (lfp H) ⊑ (F⇧#) (H (lfp H))" using distribF by (metis (mono_tags) u_galois_connection)
then have "(lfp G) ⊑ (F⇧#) (lfp H)" by (metis comp_def def_lfp_unfold lfp_lowerbound monoH)
thus "F (lfp G) ⊑ (lfp H)" using distribF by (metis (mono_tags) u_galois_connection)
qed
theorem fusion_lfp_eq:
assumes monoH: "mono H" and monoG: "mono G"
and distF: "dist_over_sup F"
and fgh_comp: "⋀x. ((F ∘ G) x = (H ∘ F) x)"
shows "F (lfp G) = (lfp H)"
proof (rule antisym)
show "lfp H ⊑ F (lfp G)" by (metis monoG fgh_comp eq_iff upper_galois_connections.u_simple_fusion)
next
have "⋀x. (F ∘ G) x ⊑ (H ∘ F) x" using fgh_comp by auto
then show "F (lfp G) ⊑ (lfp H)" using monoH distF fusion_lfp_leq by blast
qed
end
end