14 |
14 |
15 notation |
15 notation |
16 equiv ("'(\<approx>')") and |
16 equiv ("'(\<approx>')") and |
17 equiv ("(_/ \<approx> _)" [51, 51] 50) |
17 equiv ("(_/ \<approx> _)" [51, 51] 50) |
18 |
18 |
19 lemma refl [iff]: "x \<approx> x" |
19 lemma equivD1: "x \<le> y" if "x \<approx> y" |
|
20 using that by (simp add: equiv_def) |
|
21 |
|
22 lemma equivD2: "y \<le> x" if "x \<approx> y" |
|
23 using that by (simp add: equiv_def) |
|
24 |
|
25 lemma equiv_refl [iff]: "x \<approx> x" |
20 by (simp add: equiv_def) |
26 by (simp add: equiv_def) |
21 |
27 |
22 lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z" |
28 lemma equiv_sym: "x \<approx> y \<longleftrightarrow> y \<approx> x" |
|
29 by (auto simp add: equiv_def) |
|
30 |
|
31 lemma equiv_trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z" |
23 by (auto simp: equiv_def intro: order_trans) |
32 by (auto simp: equiv_def intro: order_trans) |
24 |
33 |
25 lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y" |
34 lemma equiv_antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y" |
26 by (simp only: equiv_def) |
35 by (simp only: equiv_def) |
27 |
36 |
28 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y" |
37 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y" |
29 by (auto simp add: equiv_def less_le_not_le) |
38 by (auto simp add: equiv_def less_le_not_le) |
30 |
39 |
31 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y" |
40 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y" |
32 by (auto simp add: equiv_def less_le) |
41 by (auto simp add: equiv_def less_le) |
33 |
42 |
34 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y" |
43 lemma le_imp_less_or_equiv: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y" |
35 by (simp add: less_le) |
44 by (simp add: less_le) |
36 |
45 |
37 lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False" |
46 lemma less_imp_not_equiv: "x < y \<Longrightarrow> \<not> x \<approx> y" |
38 by (simp add: less_le) |
47 by (simp add: less_le) |
39 |
48 |
40 lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False" |
49 lemma not_equiv_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" |
41 by (simp add: equiv_def less_le) |
|
42 |
|
43 lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" |
|
44 by (simp add: less_le) |
50 by (simp add: less_le) |
45 |
51 |
46 lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b" |
52 lemma le_not_equiv_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b" |
47 by (simp add: less_le) |
53 by (rule not_equiv_le_trans) |
48 |
54 |
49 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y" |
55 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y" |
50 by (simp add: equiv_def) |
56 by (simp add: equiv_def) |
51 |
57 |
52 end |
58 end |
53 |
59 |
|
60 thm order_trans |
|
61 |
|
62 find_theorems "?i < ?j \<Longrightarrow> ?i \<le> ?j" |
|
63 |
|
64 ML_file \<open>~~/src/Provers/preorder.ML\<close> |
|
65 |
|
66 ML \<open> |
|
67 structure Quasi = Quasi_Tac( |
|
68 struct |
|
69 |
|
70 val le_trans = @{thm order_trans}; |
|
71 val le_refl = @{thm order_refl}; |
|
72 val eqD1 = @{thm equivD1}; |
|
73 val eqD2 = @{thm equivD2}; |
|
74 val less_reflE = @{thm less_irrefl}; |
|
75 val less_imp_le = @{thm less_imp_le}; |
|
76 val le_neq_trans = @{thm le_not_equiv_trans}; |
|
77 val neq_le_trans = @{thm not_equiv_le_trans}; |
|
78 val less_imp_neq = @{thm less_imp_not_equiv}; |
|
79 |
|
80 fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2) |
|
81 | decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2) |
|
82 | decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2) |
|
83 | decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2) |
|
84 | decomp_quasi thy _ = NONE; |
|
85 |
|
86 fun decomp_trans thy t = case decomp_quasi thy t of |
|
87 x as SOME (t1, "<=", t2) => x |
|
88 | _ => NONE; |
|
89 |
54 end |
90 end |
|
91 ); |
|
92 \<close> |
|
93 |
|
94 end |