src/HOL/Cardinals/Order_Relation_More.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 63167 0909deb8059b
permissions -rw-r--r--
more permissive;
blanchet@49310
     1
(*  Title:      HOL/Cardinals/Order_Relation_More.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Basics on order-like relations.
blanchet@48975
     6
*)
blanchet@48975
     7
wenzelm@63167
     8
section \<open>Basics on Order-Like Relations\<close>
blanchet@48975
     9
blanchet@48975
    10
theory Order_Relation_More
blanchet@55026
    11
imports Main
blanchet@48975
    12
begin
blanchet@48975
    13
wenzelm@63167
    14
subsection \<open>The upper and lower bounds operators\<close>
blanchet@48975
    15
blanchet@55023
    16
lemma aboveS_subset_above: "aboveS r a \<le> above r a"
blanchet@48975
    17
by(auto simp add: aboveS_def above_def)
blanchet@48975
    18
blanchet@55023
    19
lemma AboveS_subset_Above: "AboveS r A \<le> Above r A"
blanchet@48975
    20
by(auto simp add: AboveS_def Above_def)
blanchet@48975
    21
blanchet@55023
    22
lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
blanchet@48975
    23
by(auto simp add: UnderS_def)
blanchet@48975
    24
blanchet@55023
    25
lemma aboveS_notIn: "a \<notin> aboveS r a"
blanchet@48975
    26
by(auto simp add: aboveS_def)
blanchet@48975
    27
blanchet@55023
    28
lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above r a"
blanchet@48975
    29
by(auto simp add: refl_on_def above_def)
blanchet@48975
    30
blanchet@55023
    31
lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above r (under r a)"
blanchet@48975
    32
by(auto simp add: Above_def under_def)
blanchet@48975
    33
blanchet@55023
    34
lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under r (above r a)"
blanchet@48975
    35
by(auto simp add: Under_def above_def)
blanchet@48975
    36
blanchet@55023
    37
lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS r (aboveS r a)"
blanchet@48975
    38
by(auto simp add: UnderS_def aboveS_def)
blanchet@48975
    39
blanchet@55023
    40
lemma UnderS_subset_Under: "UnderS r A \<le> Under r A"
blanchet@54479
    41
by(auto simp add: UnderS_def Under_def)
blanchet@54479
    42
blanchet@55023
    43
lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above r (Under r B)"
blanchet@48975
    44
by(auto simp add: Above_def Under_def)
blanchet@48975
    45
blanchet@55023
    46
lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under r (Above r B)"
blanchet@48975
    47
by(auto simp add: Under_def Above_def)
blanchet@48975
    48
blanchet@55023
    49
lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS r (UnderS r B)"
blanchet@48975
    50
by(auto simp add: AboveS_def UnderS_def)
blanchet@48975
    51
blanchet@55023
    52
lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS r (AboveS r B)"
blanchet@48975
    53
by(auto simp add: UnderS_def AboveS_def)
blanchet@48975
    54
blanchet@54479
    55
lemma Under_Above_Galois:
blanchet@55023
    56
"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
blanchet@48975
    57
by(unfold Above_def Under_def, blast)
blanchet@48975
    58
blanchet@54479
    59
lemma UnderS_AboveS_Galois:
blanchet@55023
    60
"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
blanchet@48975
    61
by(unfold AboveS_def UnderS_def, blast)
blanchet@48975
    62
blanchet@54479
    63
lemma Refl_above_aboveS:
blanchet@55023
    64
  assumes REFL: "Refl r" and IN: "a \<in> Field r"
blanchet@55023
    65
  shows "above r a = aboveS r a \<union> {a}"
blanchet@48975
    66
proof(unfold above_def aboveS_def, auto)
blanchet@48975
    67
  show "(a,a) \<in> r" using REFL IN refl_on_def[of _ r] by blast
blanchet@48975
    68
qed
blanchet@48975
    69
blanchet@54479
    70
lemma Linear_order_under_aboveS_Field:
blanchet@55023
    71
  assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
blanchet@55023
    72
  shows "Field r = under r a \<union> aboveS r a"
blanchet@48975
    73
proof(unfold under_def aboveS_def, auto)
blanchet@48975
    74
  assume "a \<in> Field r" "(a, a) \<notin> r"
blanchet@48975
    75
  with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
blanchet@48975
    76
  show False by auto
blanchet@48975
    77
next
blanchet@48975
    78
  fix b assume "b \<in> Field r" "(b, a) \<notin> r"
blanchet@48975
    79
  with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
blanchet@48975
    80
  have "(a,b) \<in> r \<or> a = b" by blast
blanchet@48975
    81
  thus "(a,b) \<in> r"
blanchet@48975
    82
  using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
blanchet@48975
    83
next
blanchet@48975
    84
  fix b assume "(b, a) \<in> r"
blanchet@48975
    85
  thus "b \<in> Field r"
blanchet@48975
    86
  using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
blanchet@48975
    87
next
blanchet@48975
    88
  fix b assume "b \<noteq> a" "(a, b) \<in> r"
blanchet@48975
    89
  thus "b \<in> Field r"
blanchet@48975
    90
  using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
blanchet@48975
    91
qed
blanchet@48975
    92
blanchet@54479
    93
lemma Linear_order_underS_above_Field:
blanchet@48975
    94
assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
blanchet@55023
    95
shows "Field r = underS r a \<union> above r a"
blanchet@48975
    96
proof(unfold underS_def above_def, auto)
blanchet@48975
    97
  assume "a \<in> Field r" "(a, a) \<notin> r"
blanchet@48975
    98
  with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
traytel@51764
    99
  show False by metis
blanchet@48975
   100
next
blanchet@48975
   101
  fix b assume "b \<in> Field r" "(a, b) \<notin> r"
blanchet@48975
   102
  with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
blanchet@48975
   103
  have "(b,a) \<in> r \<or> b = a" by blast
blanchet@48975
   104
  thus "(b,a) \<in> r"
blanchet@48975
   105
  using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
blanchet@48975
   106
next
blanchet@48975
   107
  fix b assume "b \<noteq> a" "(b, a) \<in> r"
blanchet@48975
   108
  thus "b \<in> Field r"
blanchet@48975
   109
  using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
blanchet@48975
   110
next
blanchet@48975
   111
  fix b assume "(a, b) \<in> r"
blanchet@48975
   112
  thus "b \<in> Field r"
blanchet@48975
   113
  using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
blanchet@48975
   114
qed
blanchet@48975
   115
blanchet@55023
   116
lemma under_empty: "a \<notin> Field r \<Longrightarrow> under r a = {}"
blanchet@48975
   117
unfolding Field_def under_def by auto
blanchet@48975
   118
blanchet@55023
   119
lemma Under_Field: "Under r A \<le> Field r"
blanchet@54479
   120
by(unfold Under_def Field_def, auto)
blanchet@54479
   121
blanchet@55023
   122
lemma UnderS_Field: "UnderS r A \<le> Field r"
blanchet@54479
   123
by(unfold UnderS_def Field_def, auto)
blanchet@54479
   124
blanchet@55023
   125
lemma above_Field: "above r a \<le> Field r"
blanchet@48975
   126
by(unfold above_def Field_def, auto)
blanchet@48975
   127
blanchet@55023
   128
lemma aboveS_Field: "aboveS r a \<le> Field r"
blanchet@48975
   129
by(unfold aboveS_def Field_def, auto)
blanchet@48975
   130
blanchet@55023
   131
lemma Above_Field: "Above r A \<le> Field r"
blanchet@48975
   132
by(unfold Above_def Field_def, auto)
blanchet@48975
   133
blanchet@54479
   134
lemma Refl_under_Under:
blanchet@48975
   135
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
wenzelm@60585
   136
shows "Under r A = (\<Inter>a \<in> A. under r a)"
blanchet@48975
   137
proof
wenzelm@60585
   138
  show "Under r A \<subseteq> (\<Inter>a \<in> A. under r a)"
blanchet@48975
   139
  by(unfold Under_def under_def, auto)
blanchet@48975
   140
next
wenzelm@60585
   141
  show "(\<Inter>a \<in> A. under r a) \<subseteq> Under r A"
blanchet@48975
   142
  proof(auto)
blanchet@48975
   143
    fix x
blanchet@55023
   144
    assume *: "\<forall>xa \<in> A. x \<in> under r xa"
blanchet@48975
   145
    hence "\<forall>xa \<in> A. (x,xa) \<in> r"
blanchet@48975
   146
    by (simp add: under_def)
blanchet@48975
   147
    moreover
blanchet@48975
   148
    {from NE obtain a where "a \<in> A" by blast
blanchet@55023
   149
     with * have "x \<in> under r a" by simp
blanchet@48975
   150
     hence "x \<in> Field r"
blanchet@55023
   151
     using under_Field[of r a] by auto
blanchet@48975
   152
    }
blanchet@55023
   153
    ultimately show "x \<in> Under r A"
blanchet@48975
   154
    unfolding Under_def by auto
blanchet@48975
   155
  qed
blanchet@48975
   156
qed
blanchet@48975
   157
blanchet@54479
   158
lemma Refl_underS_UnderS:
blanchet@48975
   159
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
wenzelm@60585
   160
shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
blanchet@48975
   161
proof
wenzelm@60585
   162
  show "UnderS r A \<subseteq> (\<Inter>a \<in> A. underS r a)"
blanchet@48975
   163
  by(unfold UnderS_def underS_def, auto)
blanchet@48975
   164
next
wenzelm@60585
   165
  show "(\<Inter>a \<in> A. underS r a) \<subseteq> UnderS r A"
blanchet@48975
   166
  proof(auto)
blanchet@48975
   167
    fix x
blanchet@55023
   168
    assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
blanchet@48975
   169
    hence "\<forall>xa \<in> A. x \<noteq> xa \<and> (x,xa) \<in> r"
blanchet@48975
   170
    by (auto simp add: underS_def)
blanchet@48975
   171
    moreover
blanchet@48975
   172
    {from NE obtain a where "a \<in> A" by blast
blanchet@55023
   173
     with * have "x \<in> underS r a" by simp
blanchet@48975
   174
     hence "x \<in> Field r"
blanchet@55065
   175
     using underS_Field[of _ r a] by auto
blanchet@48975
   176
    }
blanchet@55023
   177
    ultimately show "x \<in> UnderS r A"
blanchet@48975
   178
    unfolding UnderS_def by auto
blanchet@48975
   179
  qed
blanchet@48975
   180
qed
blanchet@48975
   181
blanchet@54479
   182
lemma Refl_above_Above:
blanchet@48975
   183
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
wenzelm@60585
   184
shows "Above r A = (\<Inter>a \<in> A. above r a)"
blanchet@48975
   185
proof
wenzelm@60585
   186
  show "Above r A \<subseteq> (\<Inter>a \<in> A. above r a)"
blanchet@48975
   187
  by(unfold Above_def above_def, auto)
blanchet@48975
   188
next
wenzelm@60585
   189
  show "(\<Inter>a \<in> A. above r a) \<subseteq> Above r A"
blanchet@48975
   190
  proof(auto)
blanchet@48975
   191
    fix x
blanchet@55023
   192
    assume *: "\<forall>xa \<in> A. x \<in> above r xa"
blanchet@48975
   193
    hence "\<forall>xa \<in> A. (xa,x) \<in> r"
blanchet@48975
   194
    by (simp add: above_def)
blanchet@48975
   195
    moreover
blanchet@48975
   196
    {from NE obtain a where "a \<in> A" by blast
blanchet@55023
   197
     with * have "x \<in> above r a" by simp
blanchet@48975
   198
     hence "x \<in> Field r"
blanchet@55023
   199
     using above_Field[of r a] by auto
blanchet@48975
   200
    }
blanchet@55023
   201
    ultimately show "x \<in> Above r A"
blanchet@48975
   202
    unfolding Above_def by auto
blanchet@48975
   203
  qed
blanchet@48975
   204
qed
blanchet@48975
   205
blanchet@54479
   206
lemma Refl_aboveS_AboveS:
blanchet@48975
   207
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
wenzelm@60585
   208
shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
blanchet@48975
   209
proof
wenzelm@60585
   210
  show "AboveS r A \<subseteq> (\<Inter>a \<in> A. aboveS r a)"
blanchet@48975
   211
  by(unfold AboveS_def aboveS_def, auto)
blanchet@48975
   212
next
wenzelm@60585
   213
  show "(\<Inter>a \<in> A. aboveS r a) \<subseteq> AboveS r A"
blanchet@48975
   214
  proof(auto)
blanchet@48975
   215
    fix x
blanchet@55023
   216
    assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
blanchet@48975
   217
    hence "\<forall>xa \<in> A. xa \<noteq> x \<and> (xa,x) \<in> r"
blanchet@48975
   218
    by (auto simp add: aboveS_def)
blanchet@48975
   219
    moreover
blanchet@48975
   220
    {from NE obtain a where "a \<in> A" by blast
blanchet@55023
   221
     with * have "x \<in> aboveS r a" by simp
blanchet@48975
   222
     hence "x \<in> Field r"
blanchet@55023
   223
     using aboveS_Field[of r a] by auto
blanchet@48975
   224
    }
blanchet@55023
   225
    ultimately show "x \<in> AboveS r A"
blanchet@48975
   226
    unfolding AboveS_def by auto
blanchet@48975
   227
  qed
blanchet@48975
   228
qed
blanchet@48975
   229
blanchet@55023
   230
lemma under_Under_singl: "under r a = Under r {a}"
blanchet@48975
   231
by(unfold Under_def under_def, auto simp add: Field_def)
blanchet@48975
   232
blanchet@55023
   233
lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
blanchet@48975
   234
by(unfold UnderS_def underS_def, auto simp add: Field_def)
blanchet@48975
   235
blanchet@55023
   236
lemma above_Above_singl: "above r a = Above r {a}"
blanchet@48975
   237
by(unfold Above_def above_def, auto simp add: Field_def)
blanchet@48975
   238
blanchet@55023
   239
lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
blanchet@48975
   240
by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
blanchet@48975
   241
blanchet@55023
   242
lemma Under_decr: "A \<le> B \<Longrightarrow> Under r B \<le> Under r A"
blanchet@48975
   243
by(unfold Under_def, auto)
blanchet@48975
   244
blanchet@55023
   245
lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS r B \<le> UnderS r A"
blanchet@48975
   246
by(unfold UnderS_def, auto)
blanchet@48975
   247
blanchet@55023
   248
lemma Above_decr: "A \<le> B \<Longrightarrow> Above r B \<le> Above r A"
blanchet@48975
   249
by(unfold Above_def, auto)
blanchet@48975
   250
blanchet@55023
   251
lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS r B \<le> AboveS r A"
blanchet@48975
   252
by(unfold AboveS_def, auto)
blanchet@48975
   253
blanchet@54479
   254
lemma under_incl_iff:
blanchet@48975
   255
assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
blanchet@55023
   256
shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
blanchet@48975
   257
proof
blanchet@48975
   258
  assume "(a,b) \<in> r"
blanchet@55023
   259
  thus "under r a \<le> under r b" using TRANS
blanchet@48975
   260
  by (auto simp add: under_incr)
blanchet@48975
   261
next
blanchet@55023
   262
  assume "under r a \<le> under r b"
blanchet@48975
   263
  moreover
blanchet@55023
   264
  have "a \<in> under r a" using REFL IN
blanchet@48975
   265
  by (auto simp add: Refl_under_in)
blanchet@48975
   266
  ultimately show "(a,b) \<in> r"
blanchet@48975
   267
  by (auto simp add: under_def)
blanchet@48975
   268
qed
blanchet@48975
   269
blanchet@54479
   270
lemma above_decr:
blanchet@48975
   271
assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
blanchet@55023
   272
shows "above r b \<le> above r a"
blanchet@48975
   273
proof(unfold above_def, auto)
blanchet@48975
   274
  fix x assume "(b,x) \<in> r"
blanchet@48975
   275
  with REL TRANS trans_def[of r]
blanchet@48975
   276
  show "(a,x) \<in> r" by blast
blanchet@48975
   277
qed
blanchet@48975
   278
blanchet@54479
   279
lemma aboveS_decr:
blanchet@48975
   280
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@48975
   281
        REL: "(a,b) \<in> r"
blanchet@55023
   282
shows "aboveS r b \<le> aboveS r a"
blanchet@48975
   283
proof(unfold aboveS_def, auto)
blanchet@48975
   284
  assume *: "a \<noteq> b" and **: "(b,a) \<in> r"
blanchet@48975
   285
  with ANTISYM antisym_def[of r] REL
blanchet@48975
   286
  show False by auto
blanchet@48975
   287
next
blanchet@48975
   288
  fix x assume "x \<noteq> b" "(b,x) \<in> r"
blanchet@48975
   289
  with REL TRANS trans_def[of r]
blanchet@48975
   290
  show "(a,x) \<in> r" by blast
blanchet@48975
   291
qed
blanchet@48975
   292
blanchet@54479
   293
lemma under_trans:
blanchet@48975
   294
assumes TRANS: "trans r" and
blanchet@55023
   295
        IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
blanchet@55023
   296
shows "a \<in> under r c"
blanchet@48975
   297
proof-
blanchet@48975
   298
  have "(a,b) \<in> r \<and> (b,c) \<in> r"
blanchet@55023
   299
  using IN1 IN2 under_def by fastforce
blanchet@48975
   300
  hence "(a,c) \<in> r"
blanchet@48975
   301
  using TRANS trans_def[of r] by blast
blanchet@48975
   302
  thus ?thesis unfolding under_def by simp
blanchet@48975
   303
qed
blanchet@48975
   304
blanchet@54479
   305
lemma under_underS_trans:
blanchet@48975
   306
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   307
        IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
blanchet@55023
   308
shows "a \<in> underS r c"
blanchet@48975
   309
proof-
blanchet@48975
   310
  have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
blanchet@55023
   311
  using IN1 IN2 under_def underS_def by fastforce
blanchet@48975
   312
  hence 1: "(a,c) \<in> r"
blanchet@48975
   313
  using TRANS trans_def[of r] by blast
blanchet@55023
   314
  have 2: "b \<noteq> c" using IN2 underS_def by force
blanchet@48975
   315
  have 3: "a \<noteq> c"
blanchet@48975
   316
  proof
blanchet@48975
   317
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
blanchet@48975
   318
    show False by auto
blanchet@48975
   319
  qed
blanchet@48975
   320
  from 1 3 show ?thesis unfolding underS_def by simp
blanchet@48975
   321
qed
blanchet@48975
   322
blanchet@54479
   323
lemma underS_under_trans:
blanchet@48975
   324
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   325
        IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
blanchet@55023
   326
shows "a \<in> underS r c"
blanchet@48975
   327
proof-
blanchet@48975
   328
  have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
blanchet@55023
   329
  using IN1 IN2 under_def underS_def by fast
blanchet@48975
   330
  hence 1: "(a,c) \<in> r"
blanchet@55023
   331
  using TRANS trans_def[of r] by fast
blanchet@55023
   332
  have 2: "a \<noteq> b" using IN1 underS_def by force
blanchet@48975
   333
  have 3: "a \<noteq> c"
blanchet@48975
   334
  proof
blanchet@48975
   335
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
blanchet@48975
   336
    show False by auto
blanchet@48975
   337
  qed
blanchet@48975
   338
  from 1 3 show ?thesis unfolding underS_def by simp
blanchet@48975
   339
qed
blanchet@48975
   340
blanchet@54479
   341
lemma underS_underS_trans:
blanchet@48975
   342
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   343
        IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
blanchet@55023
   344
shows "a \<in> underS r c"
blanchet@48975
   345
proof-
blanchet@55023
   346
  have "a \<in> under r b"
blanchet@55023
   347
  using IN1 underS_subset_under by fast
blanchet@55023
   348
  with assms under_underS_trans show ?thesis by fast
blanchet@48975
   349
qed
blanchet@48975
   350
blanchet@54479
   351
lemma above_trans:
blanchet@48975
   352
assumes TRANS: "trans r" and
blanchet@55023
   353
        IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
blanchet@55023
   354
shows "c \<in> above r a"
blanchet@48975
   355
proof-
blanchet@48975
   356
  have "(a,b) \<in> r \<and> (b,c) \<in> r"
blanchet@55023
   357
  using IN1 IN2 above_def by fast
blanchet@48975
   358
  hence "(a,c) \<in> r"
blanchet@48975
   359
  using TRANS trans_def[of r] by blast
blanchet@48975
   360
  thus ?thesis unfolding above_def by simp
blanchet@48975
   361
qed
blanchet@48975
   362
blanchet@54479
   363
lemma above_aboveS_trans:
blanchet@48975
   364
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   365
        IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
blanchet@55023
   366
shows "c \<in> aboveS r a"
blanchet@48975
   367
proof-
blanchet@48975
   368
  have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
blanchet@55023
   369
  using IN1 IN2 above_def aboveS_def by fast
blanchet@48975
   370
  hence 1: "(a,c) \<in> r"
blanchet@48975
   371
  using TRANS trans_def[of r] by blast
blanchet@55023
   372
  have 2: "b \<noteq> c" using IN2 aboveS_def by force
blanchet@48975
   373
  have 3: "a \<noteq> c"
blanchet@48975
   374
  proof
blanchet@48975
   375
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
blanchet@48975
   376
    show False by auto
blanchet@48975
   377
  qed
blanchet@48975
   378
  from 1 3 show ?thesis unfolding aboveS_def by simp
blanchet@48975
   379
qed
blanchet@48975
   380
blanchet@54479
   381
lemma aboveS_above_trans:
blanchet@48975
   382
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   383
        IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
blanchet@55023
   384
shows "c \<in> aboveS r a"
blanchet@48975
   385
proof-
blanchet@48975
   386
  have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
blanchet@55023
   387
  using IN1 IN2 above_def aboveS_def by fast
blanchet@48975
   388
  hence 1: "(a,c) \<in> r"
blanchet@48975
   389
  using TRANS trans_def[of r] by blast
blanchet@55023
   390
  have 2: "a \<noteq> b" using IN1 aboveS_def by force
blanchet@48975
   391
  have 3: "a \<noteq> c"
blanchet@48975
   392
  proof
blanchet@48975
   393
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
blanchet@48975
   394
    show False by auto
blanchet@48975
   395
  qed
blanchet@48975
   396
  from 1 3 show ?thesis unfolding aboveS_def by simp
blanchet@48975
   397
qed
blanchet@48975
   398
blanchet@54479
   399
lemma aboveS_aboveS_trans:
blanchet@48975
   400
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   401
        IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
blanchet@55023
   402
shows "c \<in> aboveS r a"
blanchet@48975
   403
proof-
blanchet@55023
   404
  have "b \<in> above r a"
blanchet@55023
   405
  using IN1 aboveS_subset_above by fast
blanchet@55023
   406
  with assms above_aboveS_trans show ?thesis by fast
blanchet@48975
   407
qed
blanchet@48975
   408
blanchet@54479
   409
lemma under_Under_trans:
blanchet@54479
   410
assumes TRANS: "trans r" and
blanchet@55023
   411
        IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
blanchet@55023
   412
shows "a \<in> Under r C"
blanchet@54479
   413
proof-
blanchet@55023
   414
  have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
blanchet@55023
   415
    using IN2 Under_def by force
blanchet@55023
   416
  hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
blanchet@55023
   417
    using IN1 under_def by fast
blanchet@54479
   418
  hence "\<forall>c \<in> C. (a,c) \<in> r"
blanchet@54479
   419
  using TRANS trans_def[of r] by blast
blanchet@54479
   420
  moreover
blanchet@54479
   421
  have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast
blanchet@54479
   422
  ultimately
blanchet@54479
   423
  show ?thesis unfolding Under_def by blast
blanchet@54479
   424
qed
blanchet@54479
   425
blanchet@54479
   426
lemma underS_Under_trans:
blanchet@48975
   427
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   428
        IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
blanchet@55023
   429
shows "a \<in> UnderS r C"
blanchet@48975
   430
proof-
blanchet@55023
   431
  from IN1 have "a \<in> under r b"
blanchet@55023
   432
  using underS_subset_under[of r b] by fast
blanchet@48975
   433
  with assms under_Under_trans
blanchet@55023
   434
  have "a \<in> Under r C" by fast
blanchet@48975
   435
  (*  *)
blanchet@48975
   436
  moreover
blanchet@48975
   437
  have "a \<notin> C"
blanchet@48975
   438
  proof
blanchet@48975
   439
    assume *: "a \<in> C"
blanchet@48975
   440
    have 1: "b \<noteq> a \<and> (a,b) \<in> r"
blanchet@55023
   441
    using IN1 underS_def[of r b] by auto
blanchet@48975
   442
    have "\<forall>c \<in> C. (b,c) \<in> r"
blanchet@55023
   443
    using IN2 Under_def[of r C] by auto
blanchet@48975
   444
    with * have "(b,a) \<in> r" by simp
blanchet@48975
   445
    with 1 ANTISYM antisym_def[of r]
blanchet@48975
   446
    show False by blast
blanchet@48975
   447
  qed
blanchet@48975
   448
  (*  *)
blanchet@48975
   449
  ultimately
blanchet@48975
   450
  show ?thesis unfolding UnderS_def
blanchet@55023
   451
  using Under_def by force
blanchet@48975
   452
qed
blanchet@48975
   453
blanchet@54479
   454
lemma underS_UnderS_trans:
blanchet@48975
   455
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   456
        IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
blanchet@55023
   457
shows "a \<in> UnderS r C"
blanchet@48975
   458
proof-
blanchet@55023
   459
  from IN2 have "b \<in> Under r C"
blanchet@55023
   460
  using UnderS_subset_Under[of r C] by blast
blanchet@48975
   461
  with underS_Under_trans assms
blanchet@55023
   462
  show ?thesis by force
blanchet@48975
   463
qed
blanchet@48975
   464
blanchet@54479
   465
lemma above_Above_trans:
blanchet@48975
   466
assumes TRANS: "trans r" and
blanchet@55023
   467
        IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
blanchet@55023
   468
shows "a \<in> Above r C"
blanchet@48975
   469
proof-
blanchet@48975
   470
  have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
blanchet@55023
   471
    using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
blanchet@48975
   472
  hence "\<forall>c \<in> C. (c,a) \<in> r"
blanchet@48975
   473
  using TRANS trans_def[of r] by blast
blanchet@48975
   474
  moreover
blanchet@55023
   475
  have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
blanchet@48975
   476
  ultimately
blanchet@48975
   477
  show ?thesis unfolding Above_def by auto
blanchet@48975
   478
qed
blanchet@48975
   479
blanchet@54479
   480
lemma aboveS_Above_trans:
blanchet@48975
   481
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   482
        IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
blanchet@55023
   483
shows "a \<in> AboveS r C"
blanchet@48975
   484
proof-
blanchet@55023
   485
  from IN1 have "a \<in> above r b"
blanchet@55023
   486
  using aboveS_subset_above[of r b] by blast
blanchet@48975
   487
  with assms above_Above_trans
blanchet@55023
   488
  have "a \<in> Above r C" by fast
blanchet@48975
   489
  (*  *)
blanchet@48975
   490
  moreover
blanchet@48975
   491
  have "a \<notin> C"
blanchet@48975
   492
  proof
blanchet@48975
   493
    assume *: "a \<in> C"
blanchet@48975
   494
    have 1: "b \<noteq> a \<and> (b,a) \<in> r"
blanchet@55023
   495
    using IN1 aboveS_def[of r b] by auto
blanchet@48975
   496
    have "\<forall>c \<in> C. (c,b) \<in> r"
blanchet@55023
   497
    using IN2 Above_def[of r C] by auto
blanchet@48975
   498
    with * have "(a,b) \<in> r" by simp
blanchet@48975
   499
    with 1 ANTISYM antisym_def[of r]
blanchet@48975
   500
    show False by blast
blanchet@48975
   501
  qed
blanchet@48975
   502
  (*  *)
blanchet@48975
   503
  ultimately
blanchet@48975
   504
  show ?thesis unfolding AboveS_def
blanchet@55023
   505
  using Above_def by force
blanchet@48975
   506
qed
blanchet@48975
   507
blanchet@54479
   508
lemma above_AboveS_trans:
blanchet@48975
   509
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   510
        IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
blanchet@55023
   511
shows "a \<in> AboveS r C"
blanchet@48975
   512
proof-
blanchet@55023
   513
  from IN2 have "b \<in> Above r C"
blanchet@55023
   514
  using AboveS_subset_Above[of r C] by blast
blanchet@48975
   515
  with assms above_Above_trans
blanchet@55023
   516
  have "a \<in> Above r C" by force
blanchet@48975
   517
  (*  *)
blanchet@48975
   518
  moreover
blanchet@48975
   519
  have "a \<notin> C"
blanchet@48975
   520
  proof
blanchet@48975
   521
    assume *: "a \<in> C"
blanchet@48975
   522
    have 1: "(b,a) \<in> r"
blanchet@55023
   523
    using IN1 above_def[of r b] by auto
blanchet@48975
   524
    have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
blanchet@55023
   525
    using IN2 AboveS_def[of r C] by auto
blanchet@48975
   526
    with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
blanchet@48975
   527
    with 1 ANTISYM antisym_def[of r]
blanchet@48975
   528
    show False by blast
blanchet@48975
   529
  qed
blanchet@48975
   530
  (*  *)
blanchet@48975
   531
  ultimately
blanchet@48975
   532
  show ?thesis unfolding AboveS_def
blanchet@55023
   533
  using Above_def by force
blanchet@48975
   534
qed
blanchet@48975
   535
blanchet@54479
   536
lemma aboveS_AboveS_trans:
blanchet@48975
   537
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   538
        IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
blanchet@55023
   539
shows "a \<in> AboveS r C"
blanchet@48975
   540
proof-
blanchet@55023
   541
  from IN2 have "b \<in> Above r C"
blanchet@55023
   542
  using AboveS_subset_Above[of r C] by blast
blanchet@48975
   543
  with aboveS_Above_trans assms
blanchet@55023
   544
  show ?thesis by force
blanchet@48975
   545
qed
blanchet@48975
   546
blanchet@54479
   547
lemma under_UnderS_trans:
blanchet@54479
   548
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55023
   549
        IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
blanchet@55023
   550
shows "a \<in> UnderS r C"
blanchet@54479
   551
proof-
blanchet@55023
   552
  from IN2 have "b \<in> Under r C"
blanchet@55023
   553
  using UnderS_subset_Under[of r C] by blast
blanchet@54479
   554
  with assms under_Under_trans
blanchet@55023
   555
  have "a \<in> Under r C" by force
blanchet@54479
   556
  (*  *)
blanchet@54479
   557
  moreover
blanchet@54479
   558
  have "a \<notin> C"
blanchet@54479
   559
  proof
blanchet@54479
   560
    assume *: "a \<in> C"
blanchet@54479
   561
    have 1: "(a,b) \<in> r"
blanchet@55023
   562
    using IN1 under_def[of r b] by auto
blanchet@54479
   563
    have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
blanchet@55023
   564
    using IN2 UnderS_def[of r C] by blast
blanchet@54479
   565
    with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
blanchet@54479
   566
    with 1 ANTISYM antisym_def[of r]
blanchet@54479
   567
    show False by blast
blanchet@54479
   568
  qed
blanchet@54479
   569
  (*  *)
blanchet@54479
   570
  ultimately
blanchet@54479
   571
  show ?thesis unfolding UnderS_def Under_def by fast
blanchet@54479
   572
qed
blanchet@54479
   573
blanchet@48975
   574
wenzelm@63167
   575
subsection \<open>Properties depending on more than one relation\<close>
blanchet@48975
   576
blanchet@48975
   577
lemma under_incr2:
blanchet@48975
   578
"r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
blanchet@55023
   579
unfolding under_def by blast
blanchet@48975
   580
blanchet@48975
   581
lemma underS_incr2:
blanchet@48975
   582
"r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
blanchet@55023
   583
unfolding underS_def by blast
blanchet@48975
   584
blanchet@55023
   585
(* FIXME: r \<leadsto> r'
blanchet@48975
   586
lemma Under_incr:
blanchet@48975
   587
"r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
blanchet@55023
   588
unfolding Under_def by blast
blanchet@48975
   589
blanchet@48975
   590
lemma UnderS_incr:
blanchet@48975
   591
"r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
blanchet@55023
   592
unfolding UnderS_def by blast
blanchet@48975
   593
blanchet@48975
   594
lemma Under_incr_decr:
blanchet@48975
   595
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Under r A \<le> Under r A'"
blanchet@55023
   596
unfolding Under_def by blast
blanchet@48975
   597
blanchet@48975
   598
lemma UnderS_incr_decr:
blanchet@48975
   599
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> UnderS r A \<le> UnderS r A'"
blanchet@55023
   600
unfolding UnderS_def by blast
blanchet@55023
   601
*)
blanchet@48975
   602
blanchet@48975
   603
lemma above_incr2:
blanchet@48975
   604
"r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
blanchet@55023
   605
unfolding above_def by blast
blanchet@48975
   606
blanchet@48975
   607
lemma aboveS_incr2:
blanchet@48975
   608
"r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
blanchet@55023
   609
unfolding aboveS_def by blast
blanchet@48975
   610
blanchet@55023
   611
(* FIXME
blanchet@48975
   612
lemma Above_incr:
blanchet@48975
   613
"r \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
blanchet@55023
   614
unfolding Above_def by blast
blanchet@48975
   615
blanchet@48975
   616
lemma AboveS_incr:
blanchet@48975
   617
"r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
blanchet@55023
   618
unfolding AboveS_def by blast
blanchet@48975
   619
blanchet@48975
   620
lemma Above_incr_decr:
blanchet@55023
   621
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
blanchet@55023
   622
unfolding Above_def by blast
blanchet@48975
   623
blanchet@48975
   624
lemma AboveS_incr_decr:
blanchet@55023
   625
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
blanchet@55023
   626
unfolding AboveS_def by blast
blanchet@55023
   627
*)
blanchet@48975
   628
blanchet@48975
   629
end