src/HOL/Order_Relation.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 58184 db1381d811ab child 58889 5b7a9633cfa8 permissions -rw-r--r--
simpler proof
     1 (*  Title:      HOL/Order_Relation.thy

     2     Author:     Tobias Nipkow

     3     Author:     Andrei Popescu, TU Muenchen

     4 *)

     5

     6 header {* Orders as Relations *}

     7

     8 theory Order_Relation

     9 imports Wfrec

    10 begin

    11

    12 subsection{* Orders on a set *}

    13

    14 definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"

    15

    16 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"

    17

    18 definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"

    19

    20 definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"

    21

    22 definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"

    23

    24 lemmas order_on_defs =

    25   preorder_on_def partial_order_on_def linear_order_on_def

    26   strict_linear_order_on_def well_order_on_def

    27

    28

    29 lemma preorder_on_empty[simp]: "preorder_on {} {}"

    30 by(simp add:preorder_on_def trans_def)

    31

    32 lemma partial_order_on_empty[simp]: "partial_order_on {} {}"

    33 by(simp add:partial_order_on_def)

    34

    35 lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"

    36 by(simp add:linear_order_on_def)

    37

    38 lemma well_order_on_empty[simp]: "well_order_on {} {}"

    39 by(simp add:well_order_on_def)

    40

    41

    42 lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"

    43 by (simp add:preorder_on_def)

    44

    45 lemma partial_order_on_converse[simp]:

    46   "partial_order_on A (r^-1) = partial_order_on A r"

    47 by (simp add: partial_order_on_def)

    48

    49 lemma linear_order_on_converse[simp]:

    50   "linear_order_on A (r^-1) = linear_order_on A r"

    51 by (simp add: linear_order_on_def)

    52

    53

    54 lemma strict_linear_order_on_diff_Id:

    55   "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"

    56 by(simp add: order_on_defs trans_diff_Id)

    57

    58

    59 subsection{* Orders on the field *}

    60

    61 abbreviation "Refl r \<equiv> refl_on (Field r) r"

    62

    63 abbreviation "Preorder r \<equiv> preorder_on (Field r) r"

    64

    65 abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"

    66

    67 abbreviation "Total r \<equiv> total_on (Field r) r"

    68

    69 abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"

    70

    71 abbreviation "Well_order r \<equiv> well_order_on (Field r) r"

    72

    73

    74 lemma subset_Image_Image_iff:

    75   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>

    76    r  A \<subseteq> r  B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"

    77 unfolding preorder_on_def refl_on_def Image_def

    78 apply (simp add: subset_eq)

    79 unfolding trans_def by fast

    80

    81 lemma subset_Image1_Image1_iff:

    82   "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r  {a} \<subseteq> r  {b} \<longleftrightarrow> (b,a):r"

    83 by(simp add:subset_Image_Image_iff)

    84

    85 lemma Refl_antisym_eq_Image1_Image1_iff:

    86   assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"

    87   shows "r  {a} = r  {b} \<longleftrightarrow> a = b"

    88 proof

    89   assume "r  {a} = r  {b}"

    90   hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)

    91   have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)

    92   hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all

    93   thus "a = b" using as[unfolded antisym_def] by blast

    94 qed fast

    95

    96 lemma Partial_order_eq_Image1_Image1_iff:

    97   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r  {a} = r  {b} \<longleftrightarrow> a=b"

    98 by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)

    99

   100 lemma Total_Id_Field:

   101 assumes TOT: "Total r" and NID: "\<not> (r <= Id)"

   102 shows "Field r = Field(r - Id)"

   103 using mono_Field[of "r - Id" r] Diff_subset[of r Id]

   104 proof(auto)

   105   have "r \<noteq> {}" using NID by fast

   106   then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto

   107   hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)

   108

   109   fix a assume *: "a \<in> Field r"

   110   obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"

   111   using * 1 by auto

   112   hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT

   113   by (simp add: total_on_def)

   114   thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast

   115 qed

   116

   117

   118 subsection{* Orders on a type *}

   119

   120 abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"

   121

   122 abbreviation "linear_order \<equiv> linear_order_on UNIV"

   123

   124 abbreviation "well_order \<equiv> well_order_on UNIV"

   125

   126

   127 subsection {* Order-like relations *}

   128

   129 text{* In this subsection, we develop basic concepts and results pertaining

   130 to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or

   131 total relations. We also further define upper and lower bounds operators. *}

   132

   133

   134 subsubsection {* Auxiliaries *}

   135

   136 lemma refl_on_domain:

   137 "\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"

   138 by(auto simp add: refl_on_def)

   139

   140 corollary well_order_on_domain:

   141 "\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"

   142 by (auto simp add: refl_on_domain order_on_defs)

   143

   144 lemma well_order_on_Field:

   145 "well_order_on A r \<Longrightarrow> A = Field r"

   146 by(auto simp add: refl_on_def Field_def order_on_defs)

   147

   148 lemma well_order_on_Well_order:

   149 "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"

   150 using well_order_on_Field by auto

   151

   152 lemma Total_subset_Id:

   153 assumes TOT: "Total r" and SUB: "r \<le> Id"

   154 shows "r = {} \<or> (\<exists>a. r = {(a,a)})"

   155 proof-

   156   {assume "r \<noteq> {}"

   157    then obtain a b where 1: "(a,b) \<in> r" by fast

   158    hence "a = b" using SUB by blast

   159    hence 2: "(a,a) \<in> r" using 1 by simp

   160    {fix c d assume "(c,d) \<in> r"

   161     hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast

   162     hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>

   163            ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"

   164     using TOT unfolding total_on_def by blast

   165     hence "a = c \<and> a = d" using SUB by blast

   166    }

   167    hence "r \<le> {(a,a)}" by auto

   168    with 2 have "\<exists>a. r = {(a,a)}" by blast

   169   }

   170   thus ?thesis by blast

   171 qed

   172

   173 lemma Linear_order_in_diff_Id:

   174 assumes LI: "Linear_order r" and

   175         IN1: "a \<in> Field r" and IN2: "b \<in> Field r"

   176 shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"

   177 using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force

   178

   179

   180 subsubsection {* The upper and lower bounds operators  *}

   181

   182 text{* Here we define upper (above") and lower (below") bounds operators.

   183 We think of @{text "r"} as a {\em non-strict} relation.  The suffix S"

   184 at the names of some operators indicates that the bounds are strict -- e.g.,

   185 @{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).

   186 Capitalization of the first letter in the name reminds that the operator acts on sets, rather

   187 than on individual elements. *}

   188

   189 definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"

   190 where "under r a \<equiv> {b. (b,a) \<in> r}"

   191

   192 definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"

   193 where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"

   194

   195 definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"

   196 where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"

   197

   198 definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"

   199 where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"

   200

   201 definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"

   202 where "above r a \<equiv> {b. (a,b) \<in> r}"

   203

   204 definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"

   205 where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"

   206

   207 definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"

   208 where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"

   209

   210 definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"

   211 where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"

   212

   213 definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"

   214 where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"

   215

   216 text{* Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},

   217   we bounded comprehension by @{text "Field r"} in order to properly cover

   218   the case of @{text "A"} being empty. *}

   219

   220 lemma underS_subset_under: "underS r a \<le> under r a"

   221 by(auto simp add: underS_def under_def)

   222

   223 lemma underS_notIn: "a \<notin> underS r a"

   224 by(simp add: underS_def)

   225

   226 lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"

   227 by(simp add: refl_on_def under_def)

   228

   229 lemma AboveS_disjoint: "A Int (AboveS r A) = {}"

   230 by(auto simp add: AboveS_def)

   231

   232 lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"

   233 by(auto simp add: AboveS_def underS_def)

   234

   235 lemma Refl_under_underS:

   236   assumes "Refl r" "a \<in> Field r"

   237   shows "under r a = underS r a \<union> {a}"

   238 unfolding under_def underS_def

   239 using assms refl_on_def[of _ r] by fastforce

   240

   241 lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"

   242 by (auto simp: Field_def underS_def)

   243

   244 lemma under_Field: "under r a \<le> Field r"

   245 by(unfold under_def Field_def, auto)

   246

   247 lemma underS_Field: "underS r a \<le> Field r"

   248 by(unfold underS_def Field_def, auto)

   249

   250 lemma underS_Field2:

   251 "a \<in> Field r \<Longrightarrow> underS r a < Field r"

   252 using underS_notIn underS_Field by fast

   253

   254 lemma underS_Field3:

   255 "Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"

   256 by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)

   257

   258 lemma AboveS_Field: "AboveS r A \<le> Field r"

   259 by(unfold AboveS_def Field_def, auto)

   260

   261 lemma under_incr:

   262   assumes TRANS: "trans r" and REL: "(a,b) \<in> r"

   263   shows "under r a \<le> under r b"

   264 proof(unfold under_def, auto)

   265   fix x assume "(x,a) \<in> r"

   266   with REL TRANS trans_def[of r]

   267   show "(x,b) \<in> r" by blast

   268 qed

   269

   270 lemma underS_incr:

   271 assumes TRANS: "trans r" and ANTISYM: "antisym r" and

   272         REL: "(a,b) \<in> r"

   273 shows "underS r a \<le> underS r b"

   274 proof(unfold underS_def, auto)

   275   assume *: "b \<noteq> a" and **: "(b,a) \<in> r"

   276   with ANTISYM antisym_def[of r] REL

   277   show False by blast

   278 next

   279   fix x assume "x \<noteq> a" "(x,a) \<in> r"

   280   with REL TRANS trans_def[of r]

   281   show "(x,b) \<in> r" by blast

   282 qed

   283

   284 lemma underS_incl_iff:

   285 assumes LO: "Linear_order r" and

   286         INa: "a \<in> Field r" and INb: "b \<in> Field r"

   287 shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"

   288 proof

   289   assume "(a,b) \<in> r"

   290   thus "underS r a \<le> underS r b" using LO

   291   by (simp add: order_on_defs underS_incr)

   292 next

   293   assume *: "underS r a \<le> underS r b"

   294   {assume "a = b"

   295    hence "(a,b) \<in> r" using assms

   296    by (simp add: order_on_defs refl_on_def)

   297   }

   298   moreover

   299   {assume "a \<noteq> b \<and> (b,a) \<in> r"

   300    hence "b \<in> underS r a" unfolding underS_def by blast

   301    hence "b \<in> underS r b" using * by blast

   302    hence False by (simp add: underS_notIn)

   303   }

   304   ultimately

   305   show "(a,b) \<in> r" using assms

   306   order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast

   307 qed

   308

   309

   310 subsection {* Variations on Well-Founded Relations  *}

   311

   312 text {*

   313 This subsection contains some variations of the results from @{theory Wellfounded}:

   314 \begin{itemize}

   315 \item means for slightly more direct definitions by well-founded recursion;

   316 \item variations of well-founded induction;

   317 \item means for proving a linear order to be a well-order.

   318 \end{itemize}

   319 *}

   320

   321

   322 subsubsection {* Characterizations of well-foundedness *}

   323

   324 text {* A transitive relation is well-founded iff it is locally'' well-founded,

   325 i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}

   326

   327 lemma trans_wf_iff:

   328 assumes "trans r"

   329 shows "wf r = (\<forall>a. wf(r Int (r^-1{a} \<times> r^-1{a})))"

   330 proof-

   331   obtain R where R_def: "R = (\<lambda> a. r Int (r^-1{a} \<times> r^-1{a}))" by blast

   332   {assume *: "wf r"

   333    {fix a

   334     have "wf(R a)"

   335     using * R_def wf_subset[of r "R a"] by auto

   336    }

   337   }

   338   (*  *)

   339   moreover

   340   {assume *: "\<forall>a. wf(R a)"

   341    have "wf r"

   342    proof(unfold wf_def, clarify)

   343      fix phi a

   344      assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"

   345      obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast

   346      with * have "wf (R a)" by auto

   347      hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"

   348      unfolding wf_def by blast

   349      moreover

   350      have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"

   351      proof(auto simp add: chi_def R_def)

   352        fix b

   353        assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"

   354        hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"

   355        using assms trans_def[of r] by blast

   356        thus "phi b" using ** by blast

   357      qed

   358      ultimately have  "\<forall>b. chi b" by (rule mp)

   359      with ** chi_def show "phi a" by blast

   360    qed

   361   }

   362   ultimately show ?thesis using R_def by blast

   363 qed

   364

   365 text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,

   366 allowing one to assume the set included in the field.  *}

   367

   368 lemma wf_eq_minimal2:

   369 "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"

   370 proof-

   371   let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"

   372   have "wf r = (\<forall>A. ?phi A)"

   373   by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)

   374      (rule wfI_min, fast)

   375   (*  *)

   376   also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"

   377   proof

   378     assume "\<forall>A. ?phi A"

   379     thus "\<forall>B \<le> Field r. ?phi B" by simp

   380   next

   381     assume *: "\<forall>B \<le> Field r. ?phi B"

   382     show "\<forall>A. ?phi A"

   383     proof(clarify)

   384       fix A::"'a set" assume **: "A \<noteq> {}"

   385       obtain B where B_def: "B = A Int (Field r)" by blast

   386       show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"

   387       proof(cases "B = {}")

   388         assume Case1: "B = {}"

   389         obtain a where 1: "a \<in> A \<and> a \<notin> Field r"

   390         using ** Case1 unfolding B_def by blast

   391         hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast

   392         thus ?thesis using 1 by blast

   393       next

   394         assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast

   395         obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"

   396         using Case2 1 * by blast

   397         have "\<forall>a' \<in> A. (a',a) \<notin> r"

   398         proof(clarify)

   399           fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"

   400           hence "a' \<in> B" unfolding B_def Field_def by blast

   401           thus False using 2 ** by blast

   402         qed

   403         thus ?thesis using 2 unfolding B_def by blast

   404       qed

   405     qed

   406   qed

   407   finally show ?thesis by blast

   408 qed

   409

   410

   411 subsubsection {* Characterizations of well-foundedness *}

   412

   413 text {* The next lemma and its corollary enable one to prove that

   414 a linear order is a well-order in a way which is more standard than

   415 via well-foundedness of the strict version of the relation.  *}

   416

   417 lemma Linear_order_wf_diff_Id:

   418 assumes LI: "Linear_order r"

   419 shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"

   420 proof(cases "r \<le> Id")

   421   assume Case1: "r \<le> Id"

   422   hence temp: "r - Id = {}" by blast

   423   hence "wf(r - Id)" by (simp add: temp)

   424   moreover

   425   {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"

   426    obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI

   427    unfolding order_on_defs using Case1 Total_subset_Id by auto

   428    hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast

   429    hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast

   430   }

   431   ultimately show ?thesis by blast

   432 next

   433   assume Case2: "\<not> r \<le> Id"

   434   hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI

   435   unfolding order_on_defs by blast

   436   show ?thesis

   437   proof

   438     assume *: "wf(r - Id)"

   439     show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"

   440     proof(clarify)

   441       fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"

   442       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"

   443       using 1 * unfolding wf_eq_minimal2 by simp

   444       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"

   445       using Linear_order_in_diff_Id[of r] ** LI by blast

   446       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast

   447     qed

   448   next

   449     assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"

   450     show "wf(r - Id)"

   451     proof(unfold wf_eq_minimal2, clarify)

   452       fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"

   453       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"

   454       using 1 * by simp

   455       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"

   456       using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast

   457       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast

   458     qed

   459   qed

   460 qed

   461

   462 corollary Linear_order_Well_order_iff:

   463 assumes "Linear_order r"

   464 shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"

   465 using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast

   466

   467 end