author | blanchet |
Tue, 19 Nov 2013 01:29:50 +0100 | |
changeset 55855 | a2874c8b3558 |
parent 53319 | 57b4fdc59d3b |
child 55924 | 4cd6deb430c3 |
permissions | -rw-r--r-- |
haftmann@30661 | 1 |
(* Author: Tobias Nipkow *) |
nipkow@26273 | 2 |
|
nipkow@26273 | 3 |
header {* Orders as Relations *} |
nipkow@26273 | 4 |
|
nipkow@26273 | 5 |
theory Order_Relation |
nipkow@29796 | 6 |
imports Main |
nipkow@26273 | 7 |
begin |
nipkow@26273 | 8 |
|
nipkow@26295 | 9 |
subsection{* Orders on a set *} |
nipkow@26295 | 10 |
|
nipkow@30198 | 11 |
definition "preorder_on A r \<equiv> refl_on A r \<and> trans r" |
nipkow@26295 | 12 |
|
nipkow@26295 | 13 |
definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r" |
nipkow@26295 | 14 |
|
nipkow@26295 | 15 |
definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r" |
nipkow@26295 | 16 |
|
nipkow@26295 | 17 |
definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r" |
nipkow@26295 | 18 |
|
nipkow@26295 | 19 |
definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)" |
nipkow@26295 | 20 |
|
nipkow@26295 | 21 |
lemmas order_on_defs = |
nipkow@26295 | 22 |
preorder_on_def partial_order_on_def linear_order_on_def |
nipkow@26295 | 23 |
strict_linear_order_on_def well_order_on_def |
nipkow@26295 | 24 |
|
nipkow@26295 | 25 |
|
nipkow@26295 | 26 |
lemma preorder_on_empty[simp]: "preorder_on {} {}" |
nipkow@26295 | 27 |
by(simp add:preorder_on_def trans_def) |
nipkow@26295 | 28 |
|
nipkow@26295 | 29 |
lemma partial_order_on_empty[simp]: "partial_order_on {} {}" |
nipkow@26295 | 30 |
by(simp add:partial_order_on_def) |
nipkow@26295 | 31 |
|
nipkow@26295 | 32 |
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}" |
nipkow@26295 | 33 |
by(simp add:linear_order_on_def) |
nipkow@26295 | 34 |
|
nipkow@26295 | 35 |
lemma well_order_on_empty[simp]: "well_order_on {} {}" |
nipkow@26295 | 36 |
by(simp add:well_order_on_def) |
nipkow@26295 | 37 |
|
nipkow@26295 | 38 |
|
nipkow@26295 | 39 |
lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r" |
nipkow@26295 | 40 |
by (simp add:preorder_on_def) |
nipkow@26295 | 41 |
|
nipkow@26295 | 42 |
lemma partial_order_on_converse[simp]: |
nipkow@26295 | 43 |
"partial_order_on A (r^-1) = partial_order_on A r" |
nipkow@26295 | 44 |
by (simp add: partial_order_on_def) |
nipkow@26295 | 45 |
|
nipkow@26295 | 46 |
lemma linear_order_on_converse[simp]: |
nipkow@26295 | 47 |
"linear_order_on A (r^-1) = linear_order_on A r" |
nipkow@26295 | 48 |
by (simp add: linear_order_on_def) |
nipkow@26295 | 49 |
|
nipkow@26295 | 50 |
|
nipkow@26295 | 51 |
lemma strict_linear_order_on_diff_Id: |
nipkow@26295 | 52 |
"linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)" |
nipkow@26295 | 53 |
by(simp add: order_on_defs trans_diff_Id) |
nipkow@26295 | 54 |
|
nipkow@26295 | 55 |
|
nipkow@26295 | 56 |
subsection{* Orders on the field *} |
nipkow@26295 | 57 |
|
nipkow@30198 | 58 |
abbreviation "Refl r \<equiv> refl_on (Field r) r" |
nipkow@26295 | 59 |
|
nipkow@26295 | 60 |
abbreviation "Preorder r \<equiv> preorder_on (Field r) r" |
nipkow@26295 | 61 |
|
nipkow@26295 | 62 |
abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r" |
nipkow@26295 | 63 |
|
nipkow@26295 | 64 |
abbreviation "Total r \<equiv> total_on (Field r) r" |
nipkow@26295 | 65 |
|
nipkow@26295 | 66 |
abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r" |
nipkow@26295 | 67 |
|
nipkow@26295 | 68 |
abbreviation "Well_order r \<equiv> well_order_on (Field r) r" |
nipkow@26295 | 69 |
|
nipkow@26273 | 70 |
|
nipkow@26273 | 71 |
lemma subset_Image_Image_iff: |
nipkow@26273 | 72 |
"\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow> |
nipkow@26273 | 73 |
r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)" |
blanchet@49765 | 74 |
unfolding preorder_on_def refl_on_def Image_def |
blanchet@49765 | 75 |
apply (simp add: subset_eq) |
blanchet@49765 | 76 |
unfolding trans_def by fast |
nipkow@26273 | 77 |
|
nipkow@26273 | 78 |
lemma subset_Image1_Image1_iff: |
nipkow@26273 | 79 |
"\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r" |
nipkow@26273 | 80 |
by(simp add:subset_Image_Image_iff) |
nipkow@26273 | 81 |
|
nipkow@26273 | 82 |
lemma Refl_antisym_eq_Image1_Image1_iff: |
nipkow@26273 | 83 |
"\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b" |
nipkow@39535 | 84 |
by(simp add: set_eq_iff antisym_def refl_on_def) metis |
nipkow@26273 | 85 |
|
nipkow@26273 | 86 |
lemma Partial_order_eq_Image1_Image1_iff: |
nipkow@26273 | 87 |
"\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b" |
nipkow@26295 | 88 |
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff) |
nipkow@26295 | 89 |
|
popescua@53319 | 90 |
lemma Total_Id_Field: |
popescua@53319 | 91 |
assumes TOT: "Total r" and NID: "\<not> (r <= Id)" |
popescua@53319 | 92 |
shows "Field r = Field(r - Id)" |
popescua@53319 | 93 |
using mono_Field[of "r - Id" r] Diff_subset[of r Id] |
popescua@53319 | 94 |
proof(auto) |
popescua@53319 | 95 |
have "r \<noteq> {}" using NID by fast |
blanchet@55855 | 96 |
then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto |
popescua@53319 | 97 |
hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) |
popescua@53319 | 98 |
(* *) |
popescua@53319 | 99 |
fix a assume *: "a \<in> Field r" |
popescua@53319 | 100 |
obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" |
popescua@53319 | 101 |
using * 1 by auto |
popescua@53319 | 102 |
hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT |
popescua@53319 | 103 |
by (simp add: total_on_def) |
popescua@53319 | 104 |
thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast |
popescua@53319 | 105 |
qed |
popescua@53319 | 106 |
|
nipkow@26295 | 107 |
|
nipkow@26295 | 108 |
subsection{* Orders on a type *} |
nipkow@26295 | 109 |
|
nipkow@26295 | 110 |
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV" |
nipkow@26295 | 111 |
|
nipkow@26295 | 112 |
abbreviation "linear_order \<equiv> linear_order_on UNIV" |
nipkow@26295 | 113 |
|
nipkow@26295 | 114 |
abbreviation "well_order r \<equiv> well_order_on UNIV" |
nipkow@26273 | 115 |
|
nipkow@26273 | 116 |
end |