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