4 Orders as relations with implicit base set, their Field
7 header {* Orders as Relations *}
10 imports ATP_Linkup Hilbert_Choice
13 definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
14 definition "Preorder r \<equiv> Refl r \<and> trans r"
15 definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
16 definition "Total r \<equiv> \<forall>x\<in>Field r.\<forall>y\<in>Field r. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
17 definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
18 definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
21 Preorder_def Partial_order_def Linear_order_def Well_order_def
23 lemma Refl_empty[simp]: "Refl {}"
26 lemma Preorder_empty[simp]: "Preorder {}"
27 by(simp add:Preorder_def trans_def)
29 lemma Partial_order_empty[simp]: "Partial_order {}"
30 by(simp add:Partial_order_def)
32 lemma Total_empty[simp]: "Total {}"
33 by(simp add:Total_def)
35 lemma Linear_order_empty[simp]: "Linear_order {}"
36 by(simp add:Linear_order_def)
38 lemma Well_order_empty[simp]: "Well_order {}"
39 by(simp add:Well_order_def)
41 lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
44 lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
45 by (simp add:Preorder_def)
47 lemma Partial_order_converse[simp]: "Partial_order (r^-1) = Partial_order r"
48 by (simp add: Partial_order_def)
50 lemma Total_converse[simp]: "Total (r^-1) = Total r"
51 by (auto simp: Total_def)
53 lemma Linear_order_converse[simp]: "Linear_order (r^-1) = Linear_order r"
54 by (simp add: Linear_order_def)
56 lemma subset_Image_Image_iff:
57 "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
58 r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
59 apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
63 lemma subset_Image1_Image1_iff:
64 "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
65 by(simp add:subset_Image_Image_iff)
67 lemma Refl_antisym_eq_Image1_Image1_iff:
68 "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
69 by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def)
72 lemma Partial_order_eq_Image1_Image1_iff:
73 "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
74 by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff)