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›

(* auxiliary lemma to prefer 2-element sets rather than disjunction *)
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