# HG changeset patch # User nipkow # Date 1205521081 -3600 # Node ID 6c4d534af98d7f8cf9a3733a977c7f8b3a9e1090 # Parent d63776c3be97b79ef8d18a3f7062c63c83bf6f74 Orders as relations diff -r d63776c3be97 -r 6c4d534af98d src/HOL/Library/Order_Relation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Order_Relation.thy Fri Mar 14 19:58:01 2008 +0100 @@ -0,0 +1,76 @@ +(* ID : $Id$ + Author : Tobias Nipkow + +Orders as relations with implicit base set, their Field +*) + +header {* Orders as Relations *} + +theory Order_Relation +imports ATP_Linkup Hilbert_Choice +begin + +definition "Refl r \ \x \ Field r. (x,x) \ r" +definition "Preorder r \ Refl r \ trans r" +definition "Partial_order r \ Preorder r \ antisym r" +definition "Total r \ \x\Field r.\y\Field r. x\y \ (x,y)\r \ (y,x)\r" +definition "Linear_order r \ Partial_order r \ Total r" +definition "Well_order r \ Linear_order r \ wf(r - Id)" + +lemmas Order_defs = + Preorder_def Partial_order_def Linear_order_def Well_order_def + +lemma Refl_empty[simp]: "Refl {}" +by(simp add:Refl_def) + +lemma Preorder_empty[simp]: "Preorder {}" +by(simp add:Preorder_def trans_def) + +lemma Partial_order_empty[simp]: "Partial_order {}" +by(simp add:Partial_order_def) + +lemma Total_empty[simp]: "Total {}" +by(simp add:Total_def) + +lemma Linear_order_empty[simp]: "Linear_order {}" +by(simp add:Linear_order_def) + +lemma Well_order_empty[simp]: "Well_order {}" +by(simp add:Well_order_def) + +lemma Refl_converse[simp]: "Refl(r^-1) = Refl r" +by(simp add:Refl_def) + +lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r" +by (simp add:Preorder_def) + +lemma Partial_order_converse[simp]: "Partial_order (r^-1) = Partial_order r" +by (simp add: Partial_order_def) + +lemma Total_converse[simp]: "Total (r^-1) = Total r" +by (auto simp: Total_def) + +lemma Linear_order_converse[simp]: "Linear_order (r^-1) = Linear_order r" +by (simp add: Linear_order_def) + +lemma subset_Image_Image_iff: + "\ Preorder r; A \ Field r; B \ Field r\ \ + r `` A \ r `` B \ (\a\A.\b\B. (b,a):r)" +apply(auto simp add:subset_def Preorder_def Refl_def Image_def) +apply metis +by(metis trans_def) + +lemma subset_Image1_Image1_iff: + "\ Preorder r; a : Field r; b : Field r\ \ r `` {a} \ r `` {b} \ (b,a):r" +by(simp add:subset_Image_Image_iff) + +lemma Refl_antisym_eq_Image1_Image1_iff: + "\Refl r; antisym r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" +by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def) + metis + +lemma Partial_order_eq_Image1_Image1_iff: + "\Partial_order r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" +by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff) + +end