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