Theory Order_Lattice_Props.Fixpoint_Fusion

(* 
  Title: Fixpoint Fusion
  Author: Georg Struth 
  Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Fixpoint Fusion›

theory Fixpoint_Fusion
  imports Galois_Connections

begin

text ‹Least and greatest fixpoint fusion laws for adjoints in a Galois connection, 
including some variants, are proved in this section. Again, the laws for least and greatest fixpoints are duals. ›

lemma lfp_Fix:
  fixes f :: "'a::complete_lattice_with_dual  'a"
  shows "mono f  lfp f = (Fix f)"
  unfolding lfp_def Fix_def
  apply (rule antisym)
  apply (simp add: Collect_mono Inf_superset_mono)
  by (metis (mono_tags) Inf_lower lfp_def lfp_unfold mem_Collect_eq)

lemma gfp_Fix:
  fixes f :: "'a::complete_lattice_with_dual  'a"
  shows "mono f  gfp f = (Fix f)"
  by (simp add: iso_map_dual gfp_to_lfp lfp_Fix Fix_map_dual_var Sup_to_Inf_var)

lemma gfp_little_fusion:
  fixes f :: "'a::complete_lattice  'a"
  and g :: "'b::complete_lattice  'b"
  assumes "mono f"
  assumes "h  f  g  h"
  shows "h (gfp f)  gfp g"
proof-
  have "h (f (gfp f))  g (h (gfp f))"
    using assms(2) le_funD by fastforce
  hence "h (gfp f)  g (h (gfp f))"
    by (simp add: assms(1) gfp_fixpoint)
  thus "h (gfp f)  gfp g" 
    by (simp add: gfp_upperbound)
qed

lemma lfp_little_fusion:
  fixes f :: "'a::complete_lattice_with_dual  'a"
  and g :: "'b::complete_lattice_with_dual  'b"
  assumes "mono f"
  assumes "g  h  h  f"
  shows "lfp g  h (lfp f)"
proof-
  have a: "mono (map_dual f)"
    by (simp add: assms iso_map_dual)
  have "map_dual h  map_dual f  map_dual g  map_dual h"
    by (metis assms map_dual_anti map_dual_func1)
  thus ?thesis
    by (metis a comp_eq_elim dual_dual_ord fun_dual1 gfp_little_fusion lfp_dual_var map_dual_def)
qed

lemma gfp_fusion:
  fixes f :: "'a::complete_lattice  'a"
  and g :: "'b::complete_lattice  'b"
  assumes "f. f  h"
  and "mono f"
  and "mono g"
  and "h  f = g  h"
  shows "h (gfp f) = gfp g"
proof-
  have a: "h (gfp f)  gfp g"
    by (simp add: assms(2) assms(4) gfp_little_fusion)
  obtain hl where conn: "x y. (hl x  y)  (x  h y)"
    using assms adj_def by blast 
  have "hl  g  hl  g  h  hl"
    by (simp add: le_fun_def, meson conn assms(3) monoE order_refl order_trans)
  also have "... = hl  h  f  hl"
    by (simp add: assms(4) comp_assoc)
  finally have "hl  g  f  hl"
    by (simp add: le_fun_def, metis conn inf.coboundedI2 inf.orderE order_refl)
  hence "hl (gfp g)  f (hl (gfp g))"
    by (metis comp_eq_dest_lhs gfp_unfold assms(3) le_fun_def)
  hence "hl (gfp g)  gfp f"
    by (simp add: gfp_upperbound)
  hence "gfp g  h (gfp f)"
    by (simp add: conn)
  thus ?thesis
    by (simp add: a eq_iff)
qed

lemma lfp_fusion:
  fixes f :: "'a::complete_lattice_with_dual  'a"
  and g :: "'b::complete_lattice_with_dual  'b"
  assumes "f. h  f"
  and "mono f"
  and "mono g"
  and "h  f = g  h"
  shows "h (lfp f) = lfp g"
proof-
  have a: "f. map_dual f  map_dual h"
    using adj_dual assms(1) by auto
  have b: "mono (map_dual f)"
    by (simp add: assms(2) iso_map_dual)
  have c: "mono (map_dual g)"
    by (simp add: assms(3) iso_map_dual)
  have "map_dual h  map_dual f = map_dual g  map_dual h"
    by (metis assms(4) map_dual_func1)
  thus ?thesis   
    by (metis a adj_dual b c gfp_fusion ladj_adj ladj_radj_dual lfp_dual_var lfp_to_gfp_var radj_adj)
qed
 
lemma gfp_fusion_inf_pres:
  fixes f :: "'a::complete_lattice  'a"
  and g :: "'b::complete_lattice  'b"
  assumes "Inf_pres h"
  and "mono f"
  and "mono g"
  and "h  f = g  h"
  shows "h (gfp f) = gfp g"
  by (simp add: Inf_pres_radj assms gfp_fusion)

lemma lfp_fusion_sup_pres:
  fixes f :: "'a::complete_lattice_with_dual  'a"
  and g :: "'b::complete_lattice_with_dual  'b"
  assumes "Sup_pres h"
  and "mono f"
  and "mono g"
  and "h  f = g  h"
shows "h (lfp f) = lfp g"
  by (simp add: Sup_pres_ladj assms lfp_fusion)

text ‹The following facts are usueful for the semantics of isotone predicate transformers. 
A dual statement for least fixpoints can be proved, but is not spelled out here.›

lemma k_adju: 
  fixes k :: "'a::order  'b::complete_lattice"
  shows "F.x. (F::'b  'a  'b)  (λk. k y)"
  by (force intro!: fun_eq_iff Inf_pres_radj)

lemma k_adju_var: "F. x.f::'a::order  'b::complete_lattice. (F x  f) = (x  (λk. k y) f)"
  using k_adju unfolding adj_def by simp

lemma gfp_fusion_var:
  fixes F :: "('a::order  'b::complete_lattice)  'a  'b"
  and g :: "'b  'b"
  assumes "mono F"
  and "mono g"
  and "h. F h x = g (h x)"
  shows "gfp F x = gfp g"
  by (metis (no_types, opaque_lifting) assms eq_iff gfp_fixpoint gfp_upperbound k_adju_var monoE order_refl)

text ‹This time, Isabelle is picking up dualities rather inconsistently.›

end