src/HOL/Cardinals/Order_Relation_More.thy
author wenzelm
Thu May 26 17:51:22 2016 +0200 (2016-05-26)
changeset 63167 0909deb8059b
parent 60585 48fdff264eb2
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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