Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Galois_Connection.thy Sprache: Isabelle

Original von: 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 \<open>Galois connections\<close>

subsection \<open>Definition and basic properties\<close>

record ('a, 'b, 'c, 'd) galcon =
  orderA :: "('a, 'c) gorder_scheme" ("\\")
  orderB :: "('b, 'd) gorder_scheme" ("\\")
  lower  :: "'a \ 'b" ("\\<^sup>*\")
  upper  :: "'b \ 'a" ("\\<^sub>*\")

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 "\\<^sub>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\<^sub>g") where
"I\<^sub>g(A) = \ orderA = A, orderB = A, lower = id, upper = id \"

subsection \<open>Well-typed connections\<close>

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 \<open>Galois connections\<close>

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 \<lparr> orderA = A, orderB = B, lower = g, upper = f \<rparr>"
  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 \<open>Composition of Galois connections\<close>

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> \ \
               (\<pi>\<^sup>*\<^bsub>G\<^esub> (\<pi>\<^sup>*\<^bsub>F\<^esub> x) \<sqsubseteq>\<^bsub>\<Y>\<^bsub>G\<^esub>\<^esub> y) = (x \<sqsubseteq>\<^bsub>\<X>\<^bsub>F\<^esub>\<^esub> \<pi>\<^sub>*\<^bsub>F\<^esub> (\<pi>\<^sub>*\<^bsub>G\<^esub> 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 \<open>Retracts\<close>

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 \<open>Coretracts\<close>

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 \<open>Galois Bijections\<close>

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

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.