1 (* ID : $Id$ |
|
2 Author : Tobias Nipkow |
|
3 *) |
|
4 |
|
5 header {* Orders as Relations *} |
|
6 |
|
7 theory Order_Relation |
|
8 imports Plain "~~/src/HOL/Hilbert_Choice" "~~/src/HOL/ATP_Linkup" |
|
9 begin |
|
10 |
|
11 text{* This prelude could be moved to theory Relation: *} |
|
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 |
|
23 lemma refl_on_converse[simp]: "refl A (r^-1) = refl A r" |
|
24 by(auto simp add:refl_def) |
|
25 |
|
26 lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r" |
|
27 by (auto simp: total_on_def) |
|
28 |
|
29 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)" |
|
30 by(simp add:irrefl_def) |
|
31 |
|
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) |
|
39 |
|
40 |
|
41 subsection{* Orders on a set *} |
|
42 |
|
43 definition "preorder_on A r \<equiv> refl A r \<and> trans r" |
|
44 |
|
45 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r" |
|
46 |
|
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)" |
|
52 |
|
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 |
|
57 |
|
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) |
|
63 |
|
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 |
|
70 |
|
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) |
|
77 |
|
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 |
|
82 |
|
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 *} |
|
89 |
|
90 abbreviation "Refl r \<equiv> refl (Field r) r" |
|
91 |
|
92 abbreviation "Preorder r \<equiv> preorder_on (Field r) r" |
|
93 |
|
94 abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r" |
|
95 |
|
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 |
|
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)" |
|
106 apply(auto simp add: subset_eq preorder_on_def refl_def Image_def) |
|
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" |
|
116 by(simp add: expand_set_eq antisym_def refl_def) metis |
|
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" |
|
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" |
|
130 |
|
131 end |
|