Quelle  Galois_Connection.thy   Sprache: Isabelle

(*  Title:      HOL/Algebra/Galois_Connection.thy
    Author:     Alasdair Armstrong and Simon Foster
    Copyright:  Alasdair Armstrong and Simon Foster
*)

theory Galois_Connection
  imports Complete_Lattice
begin

section ‹Galois connections›

subsection ‹Definition and basic properties›

record ('a, 'b, 'c, 'd) galcon =
  orderA :: "('a, 'c) gorder_scheme" (‹X🍋›)
  orderB :: "('b, 'd) gorder_scheme" (‹Y🍋›)
  lower  :: "'a \ 'b" (‹π🚫*🍋›)
  upper  :: "'b \ 'a" (‹π🚫*🍋›)

type_synonym ('a, 'b) galois = "('a, 'b, unit, unit) galcon"

abbreviation "inv_galcon G \ \ orderA = inv_gorder \\<^bsub>G\<^esub>, orderB = inv_gorder \\<^bsub>G\<^esub>, lower = upper G, upper = lower G \"

definition comp_galcon :: "('b, 'c) galois \ ('a, 'b) galois \ ('a, 'c) galois" (infixr ‹∘🚫g› 85)
  where "G \\<^sub>g F = \ orderA = orderA F, orderB = orderB G, lower = lower G \ lower F, upper = upper F \ upper G \"

definition id_galcon :: "'a gorder \ ('a, 'a) galois" (‹I🚫g›) where
"I\<^sub>g(A) = \ orderA = A, orderB = A, lower = id, upper = id \"


subsection ‹Well-typed connections›

locale connection =
  fixes G (structure)
  assumes is_order_A: "partial_order \"
  and is_order_B: "partial_order \"
  and lower_closure: "\\<^sup>* \ carrier \ \ carrier \"
  and upper_closure: "\\<^sub>* \ carrier \ \ carrier \"
begin

  lemma lower_closed: "x \ carrier \ \ \\<^sup>* x \ carrier \"
    using lower_closure by auto

  lemma upper_closed: "y \ carrier \ \ \\<^sub>* y \ carrier \"
    using upper_closure by auto

end


subsection ‹Galois connections›
  
locale galois_connection = connection +
  assumes galois_property: "\x \ carrier \; y \ carrier \\ \ \\<^sup>* x \\<^bsub>\\<^esub> y \ x \\<^bsub>\\<^esub> \\<^sub>* y"
begin

  lemma is_weak_order_A: "weak_partial_order \"
  proof -
    interpret po: partial_order X
      by (metis is_order_A)
    show ?thesis ..
  qed

  lemma is_weak_order_B: "weak_partial_order \"
  proof -
    interpret po: partial_order Y
      by (metis is_order_B)
    show ?thesis ..
  qed

  lemma right: "\x \ carrier \; y \ carrier \; \\<^sup>* x \\<^bsub>\\<^esub> y\ \ x \\<^bsub>\\<^esub> \\<^sub>* y"
    by (metis galois_property)

  lemma left: "\x \ carrier \; y \ carrier \; x \\<^bsub>\\<^esub> \\<^sub>* y\ \ \\<^sup>* x \\<^bsub>\\<^esub> y"
    by (metis galois_property)

  lemma deflation: "y \ carrier \ \ \\<^sup>* (\\<^sub>* y) \\<^bsub>\\<^esub> y"
    by (metis Pi_iff is_weak_order_A left upper_closure weak_partial_order.le_refl)

  lemma inflation: "x \ carrier \ \ x \\<^bsub>\\<^esub> \\<^sub>* (\\<^sup>* x)"
    by (metis (no_types, lifting) PiE galois_connection.right galois_connection_axioms is_weak_order_B lower_closure weak_partial_order.le_refl)

  lemma lower_iso: "isotone \ \ \\<^sup>*"
  proof (auto simp add:isotone_def)
    show "weak_partial_order \"
      by (metis is_weak_order_A)
    show "weak_partial_order \"
      by (metis is_weak_order_B)
    fix x y
    assume a: "x \ carrier \" "y \ carrier \" "x \\<^bsub>\\<^esub> y"
    have b: "\\<^sup>* y \ carrier \"
      using a(2) lower_closure by blast
    then have "\\<^sub>* (\\<^sup>* y) \ carrier \"
      using upper_closure by blast
    then have "x \\<^bsub>\\<^esub> \\<^sub>* (\\<^sup>* y)"
      by (meson a inflation is_weak_order_A weak_partial_order.le_trans)
    thus "\\<^sup>* x \\<^bsub>\\<^esub> \\<^sup>* y"
      by (meson b a(1) Pi_iff galois_property lower_closure upper_closure)
  qed

  lemma upper_iso: "isotone \ \ \\<^sub>*"
    apply (auto simp add:isotone_def)
    apply (metis is_weak_order_B)
    apply (metis is_weak_order_A)
    apply (metis (no_types, lifting) Pi_mem deflation is_weak_order_B lower_closure right upper_closure weak_partial_order.le_trans)
  done

  lemma lower_comp: "x \ carrier \ \ \\<^sup>* (\\<^sub>* (\\<^sup>* x)) = \\<^sup>* x"
    by (meson deflation funcset_mem inflation is_order_B lower_closure lower_iso partial_order.le_antisym upper_closure use_iso2)

  lemma lower_comp': "x \ carrier \ \ (\\<^sup>* \ \\<^sub>* \ \\<^sup>*) x = \\<^sup>* x"
    by (simp add: lower_comp)

  lemma upper_comp: "y \ carrier \ \ \\<^sub>* (\\<^sup>* (\\<^sub>* y)) = \\<^sub>* y"
  proof -
    assume a1: "y \ carrier \"
    hence f1: "\\<^sub>* y \ carrier \" using upper_closure by blast 
    have f2: "\\<^sup>* (\\<^sub>* y) \\<^bsub>\\<^esub> y" using a1 deflation by blast
    have f3: "\\<^sub>* (\\<^sup>* (\\<^sub>* y)) \ carrier \"
      using f1 lower_closure upper_closure by auto 
    have "\\<^sup>* (\\<^sub>* y) \ carrier \" using f1 lower_closure by blast   
    thus "\\<^sub>* (\\<^sup>* (\\<^sub>* y)) = \\<^sub>* y"
      by (meson a1 f1 f2 f3 inflation is_order_A partial_order.le_antisym upper_iso use_iso2) 
  qed

  lemma upper_comp': "y \ carrier \ \ (\\<^sub>* \ \\<^sup>* \ \\<^sub>*) y = \\<^sub>* y"
    by (simp add: upper_comp)

  lemma adjoint_idem1: "idempotent \ (\\<^sup>* \ \\<^sub>*)"
    by (simp add: idempotent_def is_order_B partial_order.eq_is_equal upper_comp)

  lemma adjoint_idem2: "idempotent \ (\\<^sub>* \ \\<^sup>*)"
    by (simp add: idempotent_def is_order_A partial_order.eq_is_equal lower_comp)

  lemma fg_iso: "isotone \ \ (\\<^sup>* \ \\<^sub>*)"
    by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)

  lemma gf_iso: "isotone \ \ (\\<^sub>* \ \\<^sup>*)"
    by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)

  lemma semi_inverse1: "x \ carrier \ \ \\<^sup>* x = \\<^sup>* (\\<^sub>* (\\<^sup>* x))"
    by (metis lower_comp)

  lemma semi_inverse2: "x \ carrier \ \ \\<^sub>* x = \\<^sub>* (\\<^sup>* (\\<^sub>* x))"
    by (metis upper_comp)

  theorem lower_by_complete_lattice:
    assumes "complete_lattice \" "x \ carrier \"
    shows "\\<^sup>*(x) = \\<^bsub>\\<^esub> { y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>*(y) }"
  proof -
    interpret Y: complete_lattice Y
      by (simp add: assms)

    show ?thesis
    proof (rule Y.le_antisym)
      show x: "\\<^sup>* x \ carrier \"
        using assms(2) lower_closure by blast
      show "\\<^sup>* x \\<^bsub>\\<^esub> \\<^bsub>\\<^esub>{y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y}"
      proof (rule Y.weak.inf_greatest)
        show "{y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y} \ carrier \"
          by auto
        show "\\<^sup>* x \ carrier \" by (fact x)
        fix z
        assume "z \ {y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y}" 
        thus "\\<^sup>* x \\<^bsub>\\<^esub> z"
          using assms(2) left by auto
      qed
      show "\\<^bsub>\\<^esub>{y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y} \\<^bsub>\\<^esub> \\<^sup>* x"
      proof (rule Y.weak.inf_lower)
        show "{y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y} \ carrier \"
          by auto
        show "\\<^sup>* x \ {y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y}"
        proof (auto)
          show "\\<^sup>* x \ carrier \" by (fact x)
          show "x \\<^bsub>\\<^esub> \\<^sub>* (\\<^sup>* x)"
            using assms(2) inflation by blast
        qed
      qed
      show "\\<^bsub>\\<^esub>{y \ carrier \. x \\<^bsub>\\<^esub> \\<^sub>* y} \ carrier \"
       by (auto intro: Y.weak.inf_closed)
    qed
  qed

  theorem upper_by_complete_lattice:
    assumes "complete_lattice \" "y \ carrier \"
    shows "\\<^sub>*(y) = \\<^bsub>\\<^esub> { x \ carrier \. \\<^sup>*(x) \\<^bsub>\\<^esub> y }"
  proof -
    interpret X: complete_lattice X
      by (simp add: assms)
    show ?thesis
    proof (rule X.le_antisym)
      show y: "\\<^sub>* y \ carrier \"
        using assms(2) upper_closure by blast
      show "\\<^sub>* y \\<^bsub>\\<^esub> \\<^bsub>\\<^esub>{x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y}"
      proof (rule X.weak.sup_upper)
        show "{x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y} \ carrier \"
          by auto
        show "\\<^sub>* y \ {x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y}"
        proof (auto)
          show "\\<^sub>* y \ carrier \" by (fact y)
          show "\\<^sup>* (\\<^sub>* y) \\<^bsub>\\<^esub> y"
            by (simp add: assms(2) deflation)
        qed
      qed
      show "\\<^bsub>\\<^esub>{x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y} \\<^bsub>\\<^esub> \\<^sub>* y"
      proof (rule X.weak.sup_least)
        show "{x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y} \ carrier \"
          by auto
        show "\\<^sub>* y \ carrier \" by (fact y)
        fix z
        assume "z \ {x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y}" 
        thus "z \\<^bsub>\\<^esub> \\<^sub>* y"
          by (simp add: assms(2) right)
      qed
      show "\\<^bsub>\\<^esub>{x \ carrier \. \\<^sup>* x \\<^bsub>\\<^esub> y} \ carrier \"
       by (auto intro: X.weak.sup_closed)
    qed
  qed

end

lemma dual_galois [simp]: " galois_connection \ orderA = inv_gorder B, orderB = inv_gorder A, lower = f, upper = g \
                          = galois_connection ( orderA = A, orderB = B, lower = g, upper = f )"
  by (auto simp add: galois_connection_def galois_connection_axioms_def connection_def dual_order_iff)

definition lower_adjoint :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where
  "lower_adjoint A B f \ \g. galois_connection \ orderA = A, orderB = B, lower = f, upper = g \"

definition upper_adjoint :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('b \ 'a) \ bool" where
  "upper_adjoint A B g \ \f. galois_connection \ orderA = A, orderB = B, lower = f, upper = g \"

lemma lower_adjoint_dual [simp]: "lower_adjoint (inv_gorder A) (inv_gorder B) f = upper_adjoint B A f"
  by (simp add: lower_adjoint_def upper_adjoint_def)

lemma upper_adjoint_dual [simp]: "upper_adjoint (inv_gorder A) (inv_gorder B) f = lower_adjoint B A f"
  by (simp add: lower_adjoint_def upper_adjoint_def)

lemma lower_type: "lower_adjoint A B f \ f \ carrier A \ carrier B"
  by (auto simp add:lower_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)

lemma upper_type: "upper_adjoint A B g \ g \ carrier B \ carrier A"
  by (auto simp add:upper_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)


subsection ‹Composition of Galois connections›

lemma id_galois: "partial_order A \ galois_connection (I\<^sub>g(A))"
  by (simp add: id_galcon_def galois_connection_def galois_connection_axioms_def connection_def)

lemma comp_galcon_closed:
  assumes "galois_connection G" "galois_connection F" "\\<^bsub>F\<^esub> = \\<^bsub>G\<^esub>"
  shows "galois_connection (G \\<^sub>g F)"
proof -
  interpret F: galois_connection F
    by (simp add: assms)
  interpret G: galois_connection G
    by (simp add: assms)
  
  have "partial_order \\<^bsub>G \\<^sub>g F\<^esub>"
    by (simp add: F.is_order_A comp_galcon_def)
  moreover have "partial_order \\<^bsub>G \\<^sub>g F\<^esub>"
    by (simp add: G.is_order_B comp_galcon_def)
  moreover have "\\<^sup>*\<^bsub>G\<^esub> \ \\<^sup>*\<^bsub>F\<^esub> \ carrier \\<^bsub>F\<^esub> \ carrier \\<^bsub>G\<^esub>"
    using F.lower_closure G.lower_closure assms(3) by auto
  moreover have "\\<^sub>*\<^bsub>F\<^esub> \ \\<^sub>*\<^bsub>G\<^esub> \ carrier \\<^bsub>G\<^esub> \ carrier \\<^bsub>F\<^esub>"
    using F.upper_closure G.upper_closure assms(3) by auto
  moreover 
  have "\ x y. \x \ carrier \\<^bsub>F\<^esub>; y \ carrier \\<^bsub>G\<^esub> \ \
               (π🚫*🚫G🚫 (π🚫*🚫F🚫 x) ⊑🚫Y🚫G🚫🚫 y) = (x ⊑🚫X🚫F🚫🚫 π🚫*🚫F🚫 (π🚫*🚫G🚫 y))"
    by (metis F.galois_property F.lower_closure G.galois_property G.upper_closure assms(3) Pi_iff)
  ultimately show ?thesis
    by (simp add: comp_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
qed

lemma comp_galcon_right_unit [simp]: "F \\<^sub>g I\<^sub>g(\\<^bsub>F\<^esub>) = F"
  by (simp add: comp_galcon_def id_galcon_def)

lemma comp_galcon_left_unit [simp]: "I\<^sub>g(\\<^bsub>F\<^esub>) \\<^sub>g F = F"
  by (simp add: comp_galcon_def id_galcon_def)

lemma galois_connectionI:
  assumes
    "partial_order A" "partial_order B"
    "L \ carrier A \ carrier B" "R \ carrier B \ carrier A"
    "isotone A B L" "isotone B A R" 
    "\ x y. \ x \ carrier A; y \ carrier B \ \ L x \\<^bsub>B\<^esub> y \ x \\<^bsub>A\<^esub> R y"
  shows "galois_connection \ orderA = A, orderB = B, lower = L, upper = R \"
  using assms by (simp add: galois_connection_def connection_def galois_connection_axioms_def)

lemma galois_connectionI':
  assumes
    "partial_order A" "partial_order B"
    "L \ carrier A \ carrier B" "R \ carrier B \ carrier A"
    "isotone A B L" "isotone B A R" 
    "\ X. X \ carrier(B) \ L(R(X)) \\<^bsub>B\<^esub> X"
    "\ X. X \ carrier(A) \ X \\<^bsub>A\<^esub> R(L(X))"
  shows "galois_connection \ orderA = A, orderB = B, lower = L, upper = R \"
  using assms
  by (auto simp add: galois_connection_def connection_def galois_connection_axioms_def, (meson PiE isotone_def weak_partial_order.le_trans)+)


subsection ‹Retracts›

locale retract = galois_connection +
  assumes retract_property: "x \ carrier \ \ \\<^sub>* (\\<^sup>* x) \\<^bsub>\\<^esub> x"
begin
  lemma retract_inverse: "x \ carrier \ \ \\<^sub>* (\\<^sup>* x) = x"
    by (meson funcset_mem inflation is_order_A lower_closure partial_order.le_antisym retract_axioms retract_axioms_def retract_def upper_closure)

  lemma retract_injective: "inj_on \\<^sup>* (carrier \)"
    by (metis inj_onI retract_inverse)
end  

theorem comp_retract_closed:
  assumes "retract G" "retract F" "\\<^bsub>F\<^esub> = \\<^bsub>G\<^esub>"
  shows "retract (G \\<^sub>g F)"
proof -
  interpret f: retract F
    by (simp add: assms)
  interpret g: retract G
    by (simp add: assms)
  interpret gf: galois_connection "(G \\<^sub>g F)"
    by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed retract.axioms(1))
  show ?thesis
  proof
    fix x
    assume "x \ carrier \\<^bsub>G \\<^sub>g F\<^esub>"
    thus "le \\<^bsub>G \\<^sub>g F\<^esub> (\\<^sub>*\<^bsub>G \\<^sub>g F\<^esub> (\\<^sup>*\<^bsub>G \\<^sub>g F\<^esub> x)) x"
      using assms(3) f.inflation f.lower_closed f.retract_inverse g.retract_inverse by (auto simp add: comp_galcon_def)
  qed
qed


subsection ‹Coretracts›
  
locale coretract = galois_connection +
  assumes coretract_property: "y \ carrier \ \ y \\<^bsub>\\<^esub> \\<^sup>* (\\<^sub>* y)"
begin
  lemma coretract_inverse: "y \ carrier \ \ \\<^sup>* (\\<^sub>* y) = y"
    by (meson coretract_axioms coretract_axioms_def coretract_def deflation funcset_mem is_order_B lower_closure partial_order.le_antisym upper_closure)
 
  lemma retract_injective: "inj_on \\<^sub>* (carrier \)"
    by (metis coretract_inverse inj_onI)
end  

theorem comp_coretract_closed:
  assumes "coretract G" "coretract F" "\\<^bsub>F\<^esub> = \\<^bsub>G\<^esub>"
  shows "coretract (G \\<^sub>g F)"
proof -
  interpret f: coretract F
    by (simp add: assms)
  interpret g: coretract G
    by (simp add: assms)
  interpret gf: galois_connection "(G \\<^sub>g F)"
    by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed coretract.axioms(1))
  show ?thesis
  proof
    fix y
    assume "y \ carrier \\<^bsub>G \\<^sub>g F\<^esub>"
    thus "le \\<^bsub>G \\<^sub>g F\<^esub> y (\\<^sup>*\<^bsub>G \\<^sub>g F\<^esub> (\\<^sub>*\<^bsub>G \\<^sub>g F\<^esub> y))"
      by (simp add: comp_galcon_def assms(3) f.coretract_inverse g.coretract_property g.upper_closed)
  qed
qed


subsection ‹Galois Bijections›
  
locale galois_bijection = connection +
  assumes lower_iso: "isotone \ \ \\<^sup>*" 
  and upper_iso: "isotone \ \ \\<^sub>*"
  and lower_inv_eq: "x \ carrier \ \ \\<^sub>* (\\<^sup>* x) = x"
  and upper_inv_eq: "y \ carrier \ \ \\<^sup>* (\\<^sub>* y) = y"
begin

  lemma lower_bij: "bij_betw \\<^sup>* (carrier \) (carrier \)"
    by (rule bij_betwI[where g="\\<^sub>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)  

  lemma upper_bij: "bij_betw \\<^sub>* (carrier \) (carrier \)"
    by (rule bij_betwI[where g="\\<^sup>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)  

sublocale gal_bij_conn: galois_connection
  apply (unfold_locales, auto)
  using lower_closed lower_inv_eq upper_iso use_iso2 apply fastforce
  using lower_iso upper_closed upper_inv_eq use_iso2 apply fastforce
done

sublocale gal_bij_ret: retract
  by (unfold_locales, simp add: gal_bij_conn.is_weak_order_A lower_inv_eq weak_partial_order.le_refl)

sublocale gal_bij_coret: coretract
  by (unfold_locales, simp add: gal_bij_conn.is_weak_order_B upper_inv_eq weak_partial_order.le_refl)

end

theorem comp_galois_bijection_closed:
  assumes "galois_bijection G" "galois_bijection F" "\\<^bsub>F\<^esub> = \\<^bsub>G\<^esub>"
  shows "galois_bijection (G \\<^sub>g F)"
proof -
  interpret f: galois_bijection F
    by (simp add: assms)
  interpret g: galois_bijection G
    by (simp add: assms)
  interpret gf: galois_connection "(G \\<^sub>g F)"
    by (simp add: assms(3) comp_galcon_closed f.gal_bij_conn.galois_connection_axioms g.gal_bij_conn.galois_connection_axioms galois_connection.axioms(1))
  show ?thesis
  proof
    show "isotone \\<^bsub>G \\<^sub>g F\<^esub> \\<^bsub>G \\<^sub>g F\<^esub> \\<^sup>*\<^bsub>G \\<^sub>g F\<^esub>"
      by (simp add: comp_galcon_def, metis comp_galcon_def galcon.select_convs(1) galcon.select_convs(2) galcon.select_convs(3) gf.lower_iso)
    show "isotone \\<^bsub>G \\<^sub>g F\<^esub> \\<^bsub>G \\<^sub>g F\<^esub> \\<^sub>*\<^bsub>G \\<^sub>g F\<^esub>"
      by (simp add: gf.upper_iso)
    fix x
    assume "x \ carrier \\<^bsub>G \\<^sub>g F\<^esub>"
    thus "\\<^sub>*\<^bsub>G \\<^sub>g F\<^esub> (\\<^sup>*\<^bsub>G \\<^sub>g F\<^esub> x) = x"
      using assms(3) f.lower_closed f.lower_inv_eq g.lower_inv_eq by (auto simp add: comp_galcon_def)
  next
    fix y
    assume "y \ carrier \\<^bsub>G \\<^sub>g F\<^esub>"
    thus "\\<^sup>*\<^bsub>G \\<^sub>g F\<^esub> (\\<^sub>*\<^bsub>G \\<^sub>g F\<^esub> y) = y"
      by (simp add: comp_galcon_def assms(3) f.upper_inv_eq g.upper_closed g.upper_inv_eq)
  qed
qed

end