26273
|
1 |
(* ID : $Id$
|
|
2 |
Author : Tobias Nipkow
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Orders as Relations *}
|
|
6 |
|
|
7 |
theory Order_Relation
|
|
8 |
imports ATP_Linkup Hilbert_Choice
|
|
9 |
begin
|
|
10 |
|
26298
|
11 |
text{* This prelude could be moved to theory Relation: *}
|
26295
|
12 |
|
|
13 |
definition "irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
|
|
14 |
|
|
15 |
definition "total_on A r \<equiv> \<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
|
|
16 |
|
|
17 |
abbreviation "total \<equiv> total_on UNIV"
|
|
18 |
|
|
19 |
|
|
20 |
lemma total_on_empty[simp]: "total_on {} r"
|
|
21 |
by(simp add:total_on_def)
|
|
22 |
|
26298
|
23 |
lemma refl_on_converse[simp]: "refl A (r^-1) = refl A r"
|
|
24 |
by(auto simp add:refl_def)
|
26295
|
25 |
|
|
26 |
lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
|
|
27 |
by (auto simp: total_on_def)
|
26273
|
28 |
|
26295
|
29 |
lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
|
|
30 |
by(simp add:irrefl_def)
|
26273
|
31 |
|
26295
|
32 |
declare [[simp_depth_limit = 2]]
|
|
33 |
lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
|
|
34 |
by(simp add: antisym_def trans_def) blast
|
|
35 |
declare [[simp_depth_limit = 50]]
|
|
36 |
|
|
37 |
lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
|
|
38 |
by(simp add: total_on_def)
|
26273
|
39 |
|
26298
|
40 |
|
26295
|
41 |
subsection{* Orders on a set *}
|
|
42 |
|
26298
|
43 |
definition "preorder_on A r \<equiv> refl A r \<and> trans r"
|
26295
|
44 |
|
|
45 |
definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
|
26273
|
46 |
|
26295
|
47 |
definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
|
|
48 |
|
|
49 |
definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
|
|
50 |
|
|
51 |
definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
|
26273
|
52 |
|
26295
|
53 |
lemmas order_on_defs =
|
|
54 |
preorder_on_def partial_order_on_def linear_order_on_def
|
|
55 |
strict_linear_order_on_def well_order_on_def
|
|
56 |
|
26273
|
57 |
|
26295
|
58 |
lemma preorder_on_empty[simp]: "preorder_on {} {}"
|
|
59 |
by(simp add:preorder_on_def trans_def)
|
|
60 |
|
|
61 |
lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
|
|
62 |
by(simp add:partial_order_on_def)
|
26273
|
63 |
|
26295
|
64 |
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
|
|
65 |
by(simp add:linear_order_on_def)
|
|
66 |
|
|
67 |
lemma well_order_on_empty[simp]: "well_order_on {} {}"
|
|
68 |
by(simp add:well_order_on_def)
|
|
69 |
|
26273
|
70 |
|
26295
|
71 |
lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
|
|
72 |
by (simp add:preorder_on_def)
|
|
73 |
|
|
74 |
lemma partial_order_on_converse[simp]:
|
|
75 |
"partial_order_on A (r^-1) = partial_order_on A r"
|
|
76 |
by (simp add: partial_order_on_def)
|
26273
|
77 |
|
26295
|
78 |
lemma linear_order_on_converse[simp]:
|
|
79 |
"linear_order_on A (r^-1) = linear_order_on A r"
|
|
80 |
by (simp add: linear_order_on_def)
|
|
81 |
|
26273
|
82 |
|
26295
|
83 |
lemma strict_linear_order_on_diff_Id:
|
|
84 |
"linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
|
|
85 |
by(simp add: order_on_defs trans_diff_Id)
|
|
86 |
|
|
87 |
|
|
88 |
subsection{* Orders on the field *}
|
26273
|
89 |
|
26298
|
90 |
abbreviation "Refl r \<equiv> refl (Field r) r"
|
26295
|
91 |
|
|
92 |
abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
|
|
93 |
|
|
94 |
abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
|
26273
|
95 |
|
26295
|
96 |
abbreviation "Total r \<equiv> total_on (Field r) r"
|
|
97 |
|
|
98 |
abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
|
|
99 |
|
|
100 |
abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
|
|
101 |
|
26273
|
102 |
|
|
103 |
lemma subset_Image_Image_iff:
|
|
104 |
"\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
|
|
105 |
r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
|
26298
|
106 |
apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
|
26273
|
107 |
apply metis
|
|
108 |
by(metis trans_def)
|
|
109 |
|
|
110 |
lemma subset_Image1_Image1_iff:
|
|
111 |
"\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
|
|
112 |
by(simp add:subset_Image_Image_iff)
|
|
113 |
|
|
114 |
lemma Refl_antisym_eq_Image1_Image1_iff:
|
|
115 |
"\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
|
26298
|
116 |
by(simp add: expand_set_eq antisym_def refl_def) metis
|
26273
|
117 |
|
|
118 |
lemma Partial_order_eq_Image1_Image1_iff:
|
|
119 |
"\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
|
26295
|
120 |
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
|
|
121 |
|
|
122 |
|
|
123 |
subsection{* Orders on a type *}
|
|
124 |
|
|
125 |
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
|
|
126 |
|
|
127 |
abbreviation "linear_order \<equiv> linear_order_on UNIV"
|
|
128 |
|
|
129 |
abbreviation "well_order r \<equiv> well_order_on UNIV"
|
26273
|
130 |
|
|
131 |
end
|