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