src/HOL/Algebra/Galois_Connection.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 65099 30d0b2f1df76 permissions -rw-r--r--
More on Algebra by Paulo and Martin
```     1 (*  Title:      HOL/Algebra/Galois_Connection.thy
```
```     2     Author:     Alasdair Armstrong and Simon Foster
```
```     3     Copyright:  Alasdair Armstrong and Simon Foster
```
```     4 *)
```
```     5
```
```     6 theory Galois_Connection
```
```     7   imports Complete_Lattice
```
```     8 begin
```
```     9
```
```    10 section \<open>Galois connections\<close>
```
```    11
```
```    12 subsection \<open>Definition and basic properties\<close>
```
```    13
```
```    14 record ('a, 'b, 'c, 'd) galcon =
```
```    15   orderA :: "('a, 'c) gorder_scheme" ("\<X>\<index>")
```
```    16   orderB :: "('b, 'd) gorder_scheme" ("\<Y>\<index>")
```
```    17   lower  :: "'a \<Rightarrow> 'b" ("\<pi>\<^sup>*\<index>")
```
```    18   upper  :: "'b \<Rightarrow> 'a" ("\<pi>\<^sub>*\<index>")
```
```    19
```
```    20 type_synonym ('a, 'b) galois = "('a, 'b, unit, unit) galcon"
```
```    21
```
```    22 abbreviation "inv_galcon G \<equiv> \<lparr> orderA = inv_gorder \<Y>\<^bsub>G\<^esub>, orderB = inv_gorder \<X>\<^bsub>G\<^esub>, lower = upper G, upper = lower G \<rparr>"
```
```    23
```
```    24 definition comp_galcon :: "('b, 'c) galois \<Rightarrow> ('a, 'b) galois \<Rightarrow> ('a, 'c) galois" (infixr "\<circ>\<^sub>g" 85)
```
```    25   where "G \<circ>\<^sub>g F = \<lparr> orderA = orderA F, orderB = orderB G, lower = lower G \<circ> lower F, upper = upper F \<circ> upper G \<rparr>"
```
```    26
```
```    27 definition id_galcon :: "'a gorder \<Rightarrow> ('a, 'a) galois" ("I\<^sub>g") where
```
```    28 "I\<^sub>g(A) = \<lparr> orderA = A, orderB = A, lower = id, upper = id \<rparr>"
```
```    29
```
```    30
```
```    31 subsection \<open>Well-typed connections\<close>
```
```    32
```
```    33 locale connection =
```
```    34   fixes G (structure)
```
```    35   assumes is_order_A: "partial_order \<X>"
```
```    36   and is_order_B: "partial_order \<Y>"
```
```    37   and lower_closure: "\<pi>\<^sup>* \<in> carrier \<X> \<rightarrow> carrier \<Y>"
```
```    38   and upper_closure: "\<pi>\<^sub>* \<in> carrier \<Y> \<rightarrow> carrier \<X>"
```
```    39 begin
```
```    40
```
```    41   lemma lower_closed: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* x \<in> carrier \<Y>"
```
```    42     using lower_closure by auto
```
```    43
```
```    44   lemma upper_closed: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* y \<in> carrier \<X>"
```
```    45     using upper_closure by auto
```
```    46
```
```    47 end
```
```    48
```
```    49
```
```    50 subsection \<open>Galois connections\<close>
```
```    51
```
```    52 locale galois_connection = connection +
```
```    53   assumes galois_property: "\<lbrakk>x \<in> carrier \<X>; y \<in> carrier \<Y>\<rbrakk> \<Longrightarrow> \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
```
```    54 begin
```
```    55
```
```    56   lemma is_weak_order_A: "weak_partial_order \<X>"
```
```    57   proof -
```
```    58     interpret po: partial_order \<X>
```
```    59       by (metis is_order_A)
```
```    60     show ?thesis ..
```
```    61   qed
```
```    62
```
```    63   lemma is_weak_order_B: "weak_partial_order \<Y>"
```
```    64   proof -
```
```    65     interpret po: partial_order \<Y>
```
```    66       by (metis is_order_B)
```
```    67     show ?thesis ..
```
```    68   qed
```
```    69
```
```    70   lemma right: "\<lbrakk>x \<in> carrier \<X>; y \<in> carrier \<Y>; \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
```
```    71     by (metis galois_property)
```
```    72
```
```    73   lemma left: "\<lbrakk>x \<in> carrier \<X>; y \<in> carrier \<Y>; x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y\<rbrakk> \<Longrightarrow> \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
```
```    74     by (metis galois_property)
```
```    75
```
```    76   lemma deflation: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
```
```    77     by (metis Pi_iff is_weak_order_A left upper_closure weak_partial_order.le_refl)
```
```    78
```
```    79   lemma inflation: "x \<in> carrier \<X> \<Longrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* x)"
```
```    80     by (metis (no_types, lifting) PiE galois_connection.right galois_connection_axioms is_weak_order_B lower_closure weak_partial_order.le_refl)
```
```    81
```
```    82   lemma lower_iso: "isotone \<X> \<Y> \<pi>\<^sup>*"
```
```    83   proof (auto simp add:isotone_def)
```
```    84     show "weak_partial_order \<X>"
```
```    85       by (metis is_weak_order_A)
```
```    86     show "weak_partial_order \<Y>"
```
```    87       by (metis is_weak_order_B)
```
```    88     fix x y
```
```    89     assume a: "x \<in> carrier \<X>" "y \<in> carrier \<X>" "x \<sqsubseteq>\<^bsub>\<X>\<^esub> y"
```
```    90     have b: "\<pi>\<^sup>* y \<in> carrier \<Y>"
```
```    91       using a(2) lower_closure by blast
```
```    92     then have "\<pi>\<^sub>* (\<pi>\<^sup>* y) \<in> carrier \<X>"
```
```    93       using upper_closure by blast
```
```    94     then have "x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* y)"
```
```    95       by (meson a inflation is_weak_order_A weak_partial_order.le_trans)
```
```    96     thus "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* y"
```
```    97       by (meson b a(1) Pi_iff galois_property lower_closure upper_closure)
```
```    98   qed
```
```    99
```
```   100   lemma upper_iso: "isotone \<Y> \<X> \<pi>\<^sub>*"
```
```   101     apply (auto simp add:isotone_def)
```
```   102     apply (metis is_weak_order_B)
```
```   103     apply (metis is_weak_order_A)
```
```   104     apply (metis (no_types, lifting) Pi_mem deflation is_weak_order_B lower_closure right upper_closure weak_partial_order.le_trans)
```
```   105   done
```
```   106
```
```   107   lemma lower_comp: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* (\<pi>\<^sup>* x)) = \<pi>\<^sup>* x"
```
```   108     by (meson deflation funcset_mem inflation is_order_B lower_closure lower_iso partial_order.le_antisym upper_closure use_iso2)
```
```   109
```
```   110   lemma lower_comp': "x \<in> carrier \<X> \<Longrightarrow> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>* \<circ> \<pi>\<^sup>*) x = \<pi>\<^sup>* x"
```
```   111     by (simp add: lower_comp)
```
```   112
```
```   113   lemma upper_comp: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) = \<pi>\<^sub>* y"
```
```   114   proof -
```
```   115     assume a1: "y \<in> carrier \<Y>"
```
```   116     hence f1: "\<pi>\<^sub>* y \<in> carrier \<X>" using upper_closure by blast
```
```   117     have f2: "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y" using a1 deflation by blast
```
```   118     have f3: "\<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) \<in> carrier \<X>"
```
```   119       using f1 lower_closure upper_closure by auto
```
```   120     have "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<in> carrier \<Y>" using f1 lower_closure by blast
```
```   121     thus "\<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) = \<pi>\<^sub>* y"
```
```   122       by (meson a1 f1 f2 f3 inflation is_order_A partial_order.le_antisym upper_iso use_iso2)
```
```   123   qed
```
```   124
```
```   125   lemma upper_comp': "y \<in> carrier \<Y> \<Longrightarrow> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>* \<circ> \<pi>\<^sub>*) y = \<pi>\<^sub>* y"
```
```   126     by (simp add: upper_comp)
```
```   127
```
```   128   lemma adjoint_idem1: "idempotent \<Y> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>*)"
```
```   129     by (simp add: idempotent_def is_order_B partial_order.eq_is_equal upper_comp)
```
```   130
```
```   131   lemma adjoint_idem2: "idempotent \<X> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>*)"
```
```   132     by (simp add: idempotent_def is_order_A partial_order.eq_is_equal lower_comp)
```
```   133
```
```   134   lemma fg_iso: "isotone \<Y> \<Y> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>*)"
```
```   135     by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)
```
```   136
```
```   137   lemma gf_iso: "isotone \<X> \<X> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>*)"
```
```   138     by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)
```
```   139
```
```   140   lemma semi_inverse1: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* x = \<pi>\<^sup>* (\<pi>\<^sub>* (\<pi>\<^sup>* x))"
```
```   141     by (metis lower_comp)
```
```   142
```
```   143   lemma semi_inverse2: "x \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* x = \<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* x))"
```
```   144     by (metis upper_comp)
```
```   145
```
```   146   theorem lower_by_complete_lattice:
```
```   147     assumes "complete_lattice \<Y>" "x \<in> carrier \<X>"
```
```   148     shows "\<pi>\<^sup>*(x) = \<Sqinter>\<^bsub>\<Y>\<^esub> { y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>*(y) }"
```
```   149   proof -
```
```   150     interpret Y: complete_lattice \<Y>
```
```   151       by (simp add: assms)
```
```   152
```
```   153     show ?thesis
```
```   154     proof (rule Y.le_antisym)
```
```   155       show x: "\<pi>\<^sup>* x \<in> carrier \<Y>"
```
```   156         using assms(2) lower_closure by blast
```
```   157       show "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
```
```   158       proof (rule Y.weak.inf_greatest)
```
```   159         show "{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<subseteq> carrier \<Y>"
```
```   160           by auto
```
```   161         show "\<pi>\<^sup>* x \<in> carrier \<Y>" by (fact x)
```
```   162         fix z
```
```   163         assume "z \<in> {y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
```
```   164         thus "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> z"
```
```   165           using assms(2) left by auto
```
```   166       qed
```
```   167       show "\<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* x"
```
```   168       proof (rule Y.weak.inf_lower)
```
```   169         show "{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<subseteq> carrier \<Y>"
```
```   170           by auto
```
```   171         show "\<pi>\<^sup>* x \<in> {y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
```
```   172         proof (auto)
```
```   173           show "\<pi>\<^sup>* x \<in> carrier \<Y>" by (fact x)
```
```   174           show "x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* x)"
```
```   175             using assms(2) inflation by blast
```
```   176         qed
```
```   177       qed
```
```   178       show "\<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<in> carrier \<Y>"
```
```   179        by (auto intro: Y.weak.inf_closed)
```
```   180     qed
```
```   181   qed
```
```   182
```
```   183   theorem upper_by_complete_lattice:
```
```   184     assumes "complete_lattice \<X>" "y \<in> carrier \<Y>"
```
```   185     shows "\<pi>\<^sub>*(y) = \<Squnion>\<^bsub>\<X>\<^esub> { x \<in> carrier \<X>. \<pi>\<^sup>*(x) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y }"
```
```   186   proof -
```
```   187     interpret X: complete_lattice \<X>
```
```   188       by (simp add: assms)
```
```   189     show ?thesis
```
```   190     proof (rule X.le_antisym)
```
```   191       show y: "\<pi>\<^sub>* y \<in> carrier \<X>"
```
```   192         using assms(2) upper_closure by blast
```
```   193       show "\<pi>\<^sub>* y \<sqsubseteq>\<^bsub>\<X>\<^esub> \<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
```
```   194       proof (rule X.weak.sup_upper)
```
```   195         show "{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<subseteq> carrier \<X>"
```
```   196           by auto
```
```   197         show "\<pi>\<^sub>* y \<in> {x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
```
```   198         proof (auto)
```
```   199           show "\<pi>\<^sub>* y \<in> carrier \<X>" by (fact y)
```
```   200           show "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
```
```   201             by (simp add: assms(2) deflation)
```
```   202         qed
```
```   203       qed
```
```   204       show "\<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
```
```   205       proof (rule X.weak.sup_least)
```
```   206         show "{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<subseteq> carrier \<X>"
```
```   207           by auto
```
```   208         show "\<pi>\<^sub>* y \<in> carrier \<X>" by (fact y)
```
```   209         fix z
```
```   210         assume "z \<in> {x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
```
```   211         thus "z \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
```
```   212           by (simp add: assms(2) right)
```
```   213       qed
```
```   214       show "\<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<in> carrier \<X>"
```
```   215        by (auto intro: X.weak.sup_closed)
```
```   216     qed
```
```   217   qed
```
```   218
```
```   219 end
```
```   220
```
```   221 lemma dual_galois [simp]: " galois_connection \<lparr> orderA = inv_gorder B, orderB = inv_gorder A, lower = f, upper = g \<rparr>
```
```   222                           = galois_connection \<lparr> orderA = A, orderB = B, lower = g, upper = f \<rparr>"
```
```   223   by (auto simp add: galois_connection_def galois_connection_axioms_def connection_def dual_order_iff)
```
```   224
```
```   225 definition lower_adjoint :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
```
```   226   "lower_adjoint A B f \<equiv> \<exists>g. galois_connection \<lparr> orderA = A, orderB = B, lower = f, upper = g \<rparr>"
```
```   227
```
```   228 definition upper_adjoint :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool" where
```
```   229   "upper_adjoint A B g \<equiv> \<exists>f. galois_connection \<lparr> orderA = A, orderB = B, lower = f, upper = g \<rparr>"
```
```   230
```
```   231 lemma lower_adjoint_dual [simp]: "lower_adjoint (inv_gorder A) (inv_gorder B) f = upper_adjoint B A f"
```
```   232   by (simp add: lower_adjoint_def upper_adjoint_def)
```
```   233
```
```   234 lemma upper_adjoint_dual [simp]: "upper_adjoint (inv_gorder A) (inv_gorder B) f = lower_adjoint B A f"
```
```   235   by (simp add: lower_adjoint_def upper_adjoint_def)
```
```   236
```
```   237 lemma lower_type: "lower_adjoint A B f \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier B"
```
```   238   by (auto simp add:lower_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)
```
```   239
```
```   240 lemma upper_type: "upper_adjoint A B g \<Longrightarrow> g \<in> carrier B \<rightarrow> carrier A"
```
```   241   by (auto simp add:upper_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)
```
```   242
```
```   243
```
```   244 subsection \<open>Composition of Galois connections\<close>
```
```   245
```
```   246 lemma id_galois: "partial_order A \<Longrightarrow> galois_connection (I\<^sub>g(A))"
```
```   247   by (simp add: id_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
```
```   248
```
```   249 lemma comp_galcon_closed:
```
```   250   assumes "galois_connection G" "galois_connection F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
```
```   251   shows "galois_connection (G \<circ>\<^sub>g F)"
```
```   252 proof -
```
```   253   interpret F: galois_connection F
```
```   254     by (simp add: assms)
```
```   255   interpret G: galois_connection G
```
```   256     by (simp add: assms)
```
```   257
```
```   258   have "partial_order \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   259     by (simp add: F.is_order_A comp_galcon_def)
```
```   260   moreover have "partial_order \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   261     by (simp add: G.is_order_B comp_galcon_def)
```
```   262   moreover have "\<pi>\<^sup>*\<^bsub>G\<^esub> \<circ> \<pi>\<^sup>*\<^bsub>F\<^esub> \<in> carrier \<X>\<^bsub>F\<^esub> \<rightarrow> carrier \<Y>\<^bsub>G\<^esub>"
```
```   263     using F.lower_closure G.lower_closure assms(3) by auto
```
```   264   moreover have "\<pi>\<^sub>*\<^bsub>F\<^esub> \<circ> \<pi>\<^sub>*\<^bsub>G\<^esub> \<in> carrier \<Y>\<^bsub>G\<^esub> \<rightarrow> carrier \<X>\<^bsub>F\<^esub>"
```
```   265     using F.upper_closure G.upper_closure assms(3) by auto
```
```   266   moreover
```
```   267   have "\<And> x y. \<lbrakk>x \<in> carrier \<X>\<^bsub>F\<^esub>; y \<in> carrier \<Y>\<^bsub>G\<^esub> \<rbrakk> \<Longrightarrow>
```
```   268                (\<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))"
```
```   269     by (metis F.galois_property F.lower_closure G.galois_property G.upper_closure assms(3) Pi_iff)
```
```   270   ultimately show ?thesis
```
```   271     by (simp add: comp_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
```
```   272 qed
```
```   273
```
```   274 lemma comp_galcon_right_unit [simp]: "F \<circ>\<^sub>g I\<^sub>g(\<X>\<^bsub>F\<^esub>) = F"
```
```   275   by (simp add: comp_galcon_def id_galcon_def)
```
```   276
```
```   277 lemma comp_galcon_left_unit [simp]: "I\<^sub>g(\<Y>\<^bsub>F\<^esub>) \<circ>\<^sub>g F = F"
```
```   278   by (simp add: comp_galcon_def id_galcon_def)
```
```   279
```
```   280 lemma galois_connectionI:
```
```   281   assumes
```
```   282     "partial_order A" "partial_order B"
```
```   283     "L \<in> carrier A \<rightarrow> carrier B" "R \<in> carrier B \<rightarrow> carrier A"
```
```   284     "isotone A B L" "isotone B A R"
```
```   285     "\<And> x y. \<lbrakk> x \<in> carrier A; y \<in> carrier B \<rbrakk> \<Longrightarrow> L x \<sqsubseteq>\<^bsub>B\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>A\<^esub> R y"
```
```   286   shows "galois_connection \<lparr> orderA = A, orderB = B, lower = L, upper = R \<rparr>"
```
```   287   using assms by (simp add: galois_connection_def connection_def galois_connection_axioms_def)
```
```   288
```
```   289 lemma galois_connectionI':
```
```   290   assumes
```
```   291     "partial_order A" "partial_order B"
```
```   292     "L \<in> carrier A \<rightarrow> carrier B" "R \<in> carrier B \<rightarrow> carrier A"
```
```   293     "isotone A B L" "isotone B A R"
```
```   294     "\<And> X. X \<in> carrier(B) \<Longrightarrow> L(R(X)) \<sqsubseteq>\<^bsub>B\<^esub> X"
```
```   295     "\<And> X. X \<in> carrier(A) \<Longrightarrow> X \<sqsubseteq>\<^bsub>A\<^esub> R(L(X))"
```
```   296   shows "galois_connection \<lparr> orderA = A, orderB = B, lower = L, upper = R \<rparr>"
```
```   297   using assms
```
```   298   by (auto simp add: galois_connection_def connection_def galois_connection_axioms_def, (meson PiE isotone_def weak_partial_order.le_trans)+)
```
```   299
```
```   300
```
```   301 subsection \<open>Retracts\<close>
```
```   302
```
```   303 locale retract = galois_connection +
```
```   304   assumes retract_property: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) \<sqsubseteq>\<^bsub>\<X>\<^esub> x"
```
```   305 begin
```
```   306   lemma retract_inverse: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) = x"
```
```   307     by (meson funcset_mem inflation is_order_A lower_closure partial_order.le_antisym retract_axioms retract_axioms_def retract_def upper_closure)
```
```   308
```
```   309   lemma retract_injective: "inj_on \<pi>\<^sup>* (carrier \<X>)"
```
```   310     by (metis inj_onI retract_inverse)
```
```   311 end
```
```   312
```
```   313 theorem comp_retract_closed:
```
```   314   assumes "retract G" "retract F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
```
```   315   shows "retract (G \<circ>\<^sub>g F)"
```
```   316 proof -
```
```   317   interpret f: retract F
```
```   318     by (simp add: assms)
```
```   319   interpret g: retract G
```
```   320     by (simp add: assms)
```
```   321   interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
```
```   322     by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed retract.axioms(1))
```
```   323   show ?thesis
```
```   324   proof
```
```   325     fix x
```
```   326     assume "x \<in> carrier \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   327     thus "le \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> x)) x"
```
```   328       using assms(3) f.inflation f.lower_closed f.retract_inverse g.retract_inverse by (auto simp add: comp_galcon_def)
```
```   329   qed
```
```   330 qed
```
```   331
```
```   332
```
```   333 subsection \<open>Coretracts\<close>
```
```   334
```
```   335 locale coretract = galois_connection +
```
```   336   assumes coretract_property: "y \<in> carrier \<Y> \<Longrightarrow> y \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* (\<pi>\<^sub>* y)"
```
```   337 begin
```
```   338   lemma coretract_inverse: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) = y"
```
```   339     by (meson coretract_axioms coretract_axioms_def coretract_def deflation funcset_mem is_order_B lower_closure partial_order.le_antisym upper_closure)
```
```   340
```
```   341   lemma retract_injective: "inj_on \<pi>\<^sub>* (carrier \<Y>)"
```
```   342     by (metis coretract_inverse inj_onI)
```
```   343 end
```
```   344
```
```   345 theorem comp_coretract_closed:
```
```   346   assumes "coretract G" "coretract F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
```
```   347   shows "coretract (G \<circ>\<^sub>g F)"
```
```   348 proof -
```
```   349   interpret f: coretract F
```
```   350     by (simp add: assms)
```
```   351   interpret g: coretract G
```
```   352     by (simp add: assms)
```
```   353   interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
```
```   354     by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed coretract.axioms(1))
```
```   355   show ?thesis
```
```   356   proof
```
```   357     fix y
```
```   358     assume "y \<in> carrier \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   359     thus "le \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub> y (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> y))"
```
```   360       by (simp add: comp_galcon_def assms(3) f.coretract_inverse g.coretract_property g.upper_closed)
```
```   361   qed
```
```   362 qed
```
```   363
```
```   364
```
```   365 subsection \<open>Galois Bijections\<close>
```
```   366
```
```   367 locale galois_bijection = connection +
```
```   368   assumes lower_iso: "isotone \<X> \<Y> \<pi>\<^sup>*"
```
```   369   and upper_iso: "isotone \<Y> \<X> \<pi>\<^sub>*"
```
```   370   and lower_inv_eq: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) = x"
```
```   371   and upper_inv_eq: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) = y"
```
```   372 begin
```
```   373
```
```   374   lemma lower_bij: "bij_betw \<pi>\<^sup>* (carrier \<X>) (carrier \<Y>)"
```
```   375     by (rule bij_betwI[where g="\<pi>\<^sub>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)
```
```   376
```
```   377   lemma upper_bij: "bij_betw \<pi>\<^sub>* (carrier \<Y>) (carrier \<X>)"
```
```   378     by (rule bij_betwI[where g="\<pi>\<^sup>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)
```
```   379
```
```   380 sublocale gal_bij_conn: galois_connection
```
```   381   apply (unfold_locales, auto)
```
```   382   using lower_closed lower_inv_eq upper_iso use_iso2 apply fastforce
```
```   383   using lower_iso upper_closed upper_inv_eq use_iso2 apply fastforce
```
```   384 done
```
```   385
```
```   386 sublocale gal_bij_ret: retract
```
```   387   by (unfold_locales, simp add: gal_bij_conn.is_weak_order_A lower_inv_eq weak_partial_order.le_refl)
```
```   388
```
```   389 sublocale gal_bij_coret: coretract
```
```   390   by (unfold_locales, simp add: gal_bij_conn.is_weak_order_B upper_inv_eq weak_partial_order.le_refl)
```
```   391
```
```   392 end
```
```   393
```
```   394 theorem comp_galois_bijection_closed:
```
```   395   assumes "galois_bijection G" "galois_bijection F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
```
```   396   shows "galois_bijection (G \<circ>\<^sub>g F)"
```
```   397 proof -
```
```   398   interpret f: galois_bijection F
```
```   399     by (simp add: assms)
```
```   400   interpret g: galois_bijection G
```
```   401     by (simp add: assms)
```
```   402   interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
```
```   403     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))
```
```   404   show ?thesis
```
```   405   proof
```
```   406     show "isotone \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   407       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)
```
```   408     show "isotone \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   409       by (simp add: gf.upper_iso)
```
```   410     fix x
```
```   411     assume "x \<in> carrier \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   412     thus "\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> x) = x"
```
```   413       using assms(3) f.lower_closed f.lower_inv_eq g.lower_inv_eq by (auto simp add: comp_galcon_def)
```
```   414   next
```
```   415     fix y
```
```   416     assume "y \<in> carrier \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
```
```   417     thus "\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> y) = y"
```
```   418       by (simp add: comp_galcon_def assms(3) f.upper_inv_eq g.upper_closed g.upper_inv_eq)
```
```   419   qed
```
```   420 qed
```
```   421
```
```   422 end
```