author  popescua 
Fri, 24 May 2013 18:11:57 +0200  
changeset 52182  57b4fdc59d3b 
parent 48750  a151db85a62b 
child 54482  a2874c8b3558 
permissions  rwrr 
30661  1 
(* Author: Tobias Nipkow *) 
26273  2 

3 
header {* Orders as Relations *} 

4 

5 
theory Order_Relation 

29859
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
28952
diff
changeset

6 
imports Main 
26273  7 
begin 
8 

26295  9 
subsection{* Orders on a set *} 
10 

30198  11 
definition "preorder_on A r \<equiv> refl_on A r \<and> trans r" 
26295  12 

13 
definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r" 

26273  14 

26295  15 
definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r" 
16 

17 
definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r" 

18 

19 
definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r  Id)" 

26273  20 

26295  21 
lemmas order_on_defs = 
22 
preorder_on_def partial_order_on_def linear_order_on_def 

23 
strict_linear_order_on_def well_order_on_def 

24 

26273  25 

26295  26 
lemma preorder_on_empty[simp]: "preorder_on {} {}" 
27 
by(simp add:preorder_on_def trans_def) 

28 

29 
lemma partial_order_on_empty[simp]: "partial_order_on {} {}" 

30 
by(simp add:partial_order_on_def) 

26273  31 

26295  32 
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}" 
33 
by(simp add:linear_order_on_def) 

34 

35 
lemma well_order_on_empty[simp]: "well_order_on {} {}" 

36 
by(simp add:well_order_on_def) 

37 

26273  38 

26295  39 
lemma preorder_on_converse[simp]: "preorder_on A (r^1) = preorder_on A r" 
40 
by (simp add:preorder_on_def) 

41 

42 
lemma partial_order_on_converse[simp]: 

43 
"partial_order_on A (r^1) = partial_order_on A r" 

44 
by (simp add: partial_order_on_def) 

26273  45 

26295  46 
lemma linear_order_on_converse[simp]: 
47 
"linear_order_on A (r^1) = linear_order_on A r" 

48 
by (simp add: linear_order_on_def) 

49 

26273  50 

26295  51 
lemma strict_linear_order_on_diff_Id: 
52 
"linear_order_on A r \<Longrightarrow> strict_linear_order_on A (rId)" 

53 
by(simp add: order_on_defs trans_diff_Id) 

54 

55 

56 
subsection{* Orders on the field *} 

26273  57 

30198  58 
abbreviation "Refl r \<equiv> refl_on (Field r) r" 
26295  59 

60 
abbreviation "Preorder r \<equiv> preorder_on (Field r) r" 

61 

62 
abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r" 

26273  63 

26295  64 
abbreviation "Total r \<equiv> total_on (Field r) r" 
65 

66 
abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r" 

67 

68 
abbreviation "Well_order r \<equiv> well_order_on (Field r) r" 

69 

26273  70 

71 
lemma subset_Image_Image_iff: 

72 
"\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow> 

73 
r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)" 

48750  74 
unfolding preorder_on_def refl_on_def Image_def 
75 
apply (simp add: subset_eq) 

76 
unfolding trans_def by fast 

26273  77 

78 
lemma subset_Image1_Image1_iff: 

79 
"\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r" 

80 
by(simp add:subset_Image_Image_iff) 

81 

82 
lemma Refl_antisym_eq_Image1_Image1_iff: 

83 
"\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

84 
by(simp add: set_eq_iff antisym_def refl_on_def) metis 
26273  85 

86 
lemma Partial_order_eq_Image1_Image1_iff: 

87 
"\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b" 

26295  88 
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff) 
89 

52182  90 
lemma Total_Id_Field: 
91 
assumes TOT: "Total r" and NID: "\<not> (r <= Id)" 

92 
shows "Field r = Field(r  Id)" 

93 
using mono_Field[of "r  Id" r] Diff_subset[of r Id] 

94 
proof(auto) 

95 
have "r \<noteq> {}" using NID by fast 

96 
then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast 

97 
hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) 

98 
(* *) 

99 
fix a assume *: "a \<in> Field r" 

100 
obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" 

101 
using * 1 by auto 

102 
hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT 

103 
by (simp add: total_on_def) 

104 
thus "a \<in> Field(r  Id)" using 3 unfolding Field_def by blast 

105 
qed 

106 

26295  107 

108 
subsection{* Orders on a type *} 

109 

110 
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV" 

111 

112 
abbreviation "linear_order \<equiv> linear_order_on UNIV" 

113 

114 
abbreviation "well_order r \<equiv> well_order_on UNIV" 

26273  115 

116 
end 