src/HOL/Library/Order_Relation.thy
 author nipkow Fri Mar 14 19:58:01 2008 +0100 (2008-03-14) changeset 26273 6c4d534af98d child 26295 afc43168ed85 permissions -rw-r--r--
Orders as relations
 nipkow@26273 ` 1` ```(* ID : \$Id\$ ``` nipkow@26273 ` 2` ``` Author : Tobias Nipkow ``` nipkow@26273 ` 3` nipkow@26273 ` 4` ```Orders as relations with implicit base set, their Field ``` nipkow@26273 ` 5` ```*) ``` nipkow@26273 ` 6` nipkow@26273 ` 7` ```header {* Orders as Relations *} ``` nipkow@26273 ` 8` nipkow@26273 ` 9` ```theory Order_Relation ``` nipkow@26273 ` 10` ```imports ATP_Linkup Hilbert_Choice ``` nipkow@26273 ` 11` ```begin ``` nipkow@26273 ` 12` nipkow@26273 ` 13` ```definition "Refl r \ \x \ Field r. (x,x) \ r" ``` nipkow@26273 ` 14` ```definition "Preorder r \ Refl r \ trans r" ``` nipkow@26273 ` 15` ```definition "Partial_order r \ Preorder r \ antisym r" ``` nipkow@26273 ` 16` ```definition "Total r \ \x\Field r.\y\Field r. x\y \ (x,y)\r \ (y,x)\r" ``` nipkow@26273 ` 17` ```definition "Linear_order r \ Partial_order r \ Total r" ``` nipkow@26273 ` 18` ```definition "Well_order r \ Linear_order r \ wf(r - Id)" ``` nipkow@26273 ` 19` nipkow@26273 ` 20` ```lemmas Order_defs = ``` nipkow@26273 ` 21` ``` Preorder_def Partial_order_def Linear_order_def Well_order_def ``` nipkow@26273 ` 22` nipkow@26273 ` 23` ```lemma Refl_empty[simp]: "Refl {}" ``` nipkow@26273 ` 24` ```by(simp add:Refl_def) ``` nipkow@26273 ` 25` nipkow@26273 ` 26` ```lemma Preorder_empty[simp]: "Preorder {}" ``` nipkow@26273 ` 27` ```by(simp add:Preorder_def trans_def) ``` nipkow@26273 ` 28` nipkow@26273 ` 29` ```lemma Partial_order_empty[simp]: "Partial_order {}" ``` nipkow@26273 ` 30` ```by(simp add:Partial_order_def) ``` nipkow@26273 ` 31` nipkow@26273 ` 32` ```lemma Total_empty[simp]: "Total {}" ``` nipkow@26273 ` 33` ```by(simp add:Total_def) ``` nipkow@26273 ` 34` nipkow@26273 ` 35` ```lemma Linear_order_empty[simp]: "Linear_order {}" ``` nipkow@26273 ` 36` ```by(simp add:Linear_order_def) ``` nipkow@26273 ` 37` nipkow@26273 ` 38` ```lemma Well_order_empty[simp]: "Well_order {}" ``` nipkow@26273 ` 39` ```by(simp add:Well_order_def) ``` nipkow@26273 ` 40` nipkow@26273 ` 41` ```lemma Refl_converse[simp]: "Refl(r^-1) = Refl r" ``` nipkow@26273 ` 42` ```by(simp add:Refl_def) ``` nipkow@26273 ` 43` nipkow@26273 ` 44` ```lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r" ``` nipkow@26273 ` 45` ```by (simp add:Preorder_def) ``` nipkow@26273 ` 46` nipkow@26273 ` 47` ```lemma Partial_order_converse[simp]: "Partial_order (r^-1) = Partial_order r" ``` nipkow@26273 ` 48` ```by (simp add: Partial_order_def) ``` nipkow@26273 ` 49` nipkow@26273 ` 50` ```lemma Total_converse[simp]: "Total (r^-1) = Total r" ``` nipkow@26273 ` 51` ```by (auto simp: Total_def) ``` nipkow@26273 ` 52` nipkow@26273 ` 53` ```lemma Linear_order_converse[simp]: "Linear_order (r^-1) = Linear_order r" ``` nipkow@26273 ` 54` ```by (simp add: Linear_order_def) ``` nipkow@26273 ` 55` nipkow@26273 ` 56` ```lemma subset_Image_Image_iff: ``` nipkow@26273 ` 57` ``` "\ Preorder r; A \ Field r; B \ Field r\ \ ``` nipkow@26273 ` 58` ``` r `` A \ r `` B \ (\a\A.\b\B. (b,a):r)" ``` nipkow@26273 ` 59` ```apply(auto simp add:subset_def Preorder_def Refl_def Image_def) ``` nipkow@26273 ` 60` ```apply metis ``` nipkow@26273 ` 61` ```by(metis trans_def) ``` nipkow@26273 ` 62` nipkow@26273 ` 63` ```lemma subset_Image1_Image1_iff: ``` nipkow@26273 ` 64` ``` "\ Preorder r; a : Field r; b : Field r\ \ r `` {a} \ r `` {b} \ (b,a):r" ``` nipkow@26273 ` 65` ```by(simp add:subset_Image_Image_iff) ``` nipkow@26273 ` 66` nipkow@26273 ` 67` ```lemma Refl_antisym_eq_Image1_Image1_iff: ``` nipkow@26273 ` 68` ``` "\Refl r; antisym r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" ``` nipkow@26273 ` 69` ```by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def) ``` nipkow@26273 ` 70` ``` metis ``` nipkow@26273 ` 71` nipkow@26273 ` 72` ```lemma Partial_order_eq_Image1_Image1_iff: ``` nipkow@26273 ` 73` ``` "\Partial_order r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" ``` nipkow@26273 ` 74` ```by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff) ``` nipkow@26273 ` 75` nipkow@26273 ` 76` ```end ```