author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63465  d7610beb98bc 
child 66453  cc19f7ca2ed6 
permissions  rwrr 
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

1 
(* Author: Florian Haftmann, TU Muenchen *) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

2 

60500  3 
section \<open>Preorders with explicit equivalence relation\<close> 
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

4 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

5 
theory Preorder 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

6 
imports Orderings 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

7 
begin 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

8 

31061
1d117af9f9f3
better to have distinguished class for preorders
haftmann
parents:
31060
diff
changeset

9 
class preorder_equiv = preorder 
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

10 
begin 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

11 

63465  12 
definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
13 
where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x" 

31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

14 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

15 
notation 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

16 
equiv ("op \<approx>") and 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

17 
equiv ("(_/ \<approx> _)" [51, 51] 50) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

18 

63465  19 
lemma refl [iff]: "x \<approx> x" 
20 
by (simp add: equiv_def) 

31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

21 

63465  22 
lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z" 
23 
by (auto simp: equiv_def intro: order_trans) 

31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

24 

63465  25 
lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y" 
26 
by (simp only: equiv_def) 

31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

27 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

28 
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

29 
by (auto simp add: equiv_def less_le_not_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

30 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

31 
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

32 
by (auto simp add: equiv_def less_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

33 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

34 
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

35 
by (simp add: less_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

36 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

37 
lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

38 
by (simp add: less_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

39 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

40 
lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

41 
by (simp add: equiv_def less_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

42 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

43 
lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

44 
by (simp add: less_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

45 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

46 
lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

47 
by (simp add: less_le) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

48 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

49 
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y" 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

50 
by (simp add: equiv_def) 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

51 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

52 
end 
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

53 

75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset

54 
end 