author | wenzelm |
Tue, 05 Nov 2019 14:16:16 +0100 | |
changeset 71046 | b8aeeedf7e68 |
parent 69821 | 8432b771f12e |
permissions | -rw-r--r-- |
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 |
67006 | 6 |
imports Main |
31060
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 |
67398 | 16 |
equiv ("'(\<approx>')") and |
31060
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 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
19 |
lemma equivD1: "x \<le> y" if "x \<approx> y" |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
20 |
using that by (simp add: equiv_def) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
21 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
22 |
lemma equivD2: "y \<le> x" if "x \<approx> y" |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
23 |
using that by (simp add: equiv_def) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
24 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
25 |
lemma equiv_refl [iff]: "x \<approx> x" |
63465 | 26 |
by (simp add: equiv_def) |
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
27 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
28 |
lemma equiv_sym: "x \<approx> y \<longleftrightarrow> y \<approx> x" |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
29 |
by (auto simp add: equiv_def) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
30 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
31 |
lemma equiv_trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z" |
63465 | 32 |
by (auto simp: equiv_def intro: order_trans) |
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
33 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
34 |
lemma equiv_antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y" |
63465 | 35 |
by (simp only: equiv_def) |
31060
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_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
|
38 |
by (auto simp add: equiv_def less_le_not_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 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
|
41 |
by (auto simp add: equiv_def less_le) |
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
42 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
43 |
lemma le_imp_less_or_equiv: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y" |
31060
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 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
46 |
lemma less_imp_not_equiv: "x < y \<Longrightarrow> \<not> x \<approx> y" |
31060
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 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
49 |
lemma not_equiv_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" |
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
50 |
by (simp add: less_le) |
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
51 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
52 |
lemma le_not_equiv_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b" |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
53 |
by (rule not_equiv_le_trans) |
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
54 |
|
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
55 |
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
|
56 |
by (simp add: equiv_def) |
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
57 |
|
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
58 |
end |
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
59 |
|
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
60 |
ML_file \<open>~~/src/Provers/preorder.ML\<close> |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
61 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
62 |
ML \<open> |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
63 |
structure Quasi = Quasi_Tac( |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
64 |
struct |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
65 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
66 |
val le_trans = @{thm order_trans}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
67 |
val le_refl = @{thm order_refl}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
68 |
val eqD1 = @{thm equivD1}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
69 |
val eqD2 = @{thm equivD2}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
70 |
val less_reflE = @{thm less_irrefl}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
71 |
val less_imp_le = @{thm less_imp_le}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
72 |
val le_neq_trans = @{thm le_not_equiv_trans}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
73 |
val neq_le_trans = @{thm not_equiv_le_trans}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
74 |
val less_imp_neq = @{thm less_imp_not_equiv}; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
75 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
76 |
fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
77 |
| decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
78 |
| decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
79 |
| decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2) |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
80 |
| decomp_quasi thy _ = NONE; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
81 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
82 |
fun decomp_trans thy t = case decomp_quasi thy t of |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
83 |
x as SOME (t1, "<=", t2) => x |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
84 |
| _ => NONE; |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
85 |
|
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
diff
changeset
|
86 |
end |
69815
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
87 |
); |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
88 |
\<close> |
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
89 |
|
56d5bb8c102e
proper installation of ancient procedure for preorders
haftmann
parents:
67398
diff
changeset
|
90 |
end |