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