src/HOL/Library/Preorder.thy

--- a/src/HOL/Library/Preorder.thy	Fri Feb 15 07:11:11 2019 +0000
+++ b/src/HOL/Library/Preorder.thy	Fri Feb 15 18:24:22 2019 +0000
@@ -16,13 +16,22 @@
   equiv ("'(\<approx>')") and
   equiv ("(_/ \<approx> _)"  [51, 51] 50)
 
-lemma refl [iff]: "x \<approx> x"
+lemma equivD1: "x \<le> y" if "x \<approx> y"
+  using that by (simp add: equiv_def)
+
+lemma equivD2: "y \<le> x" if "x \<approx> y"
+  using that by (simp add: equiv_def)
+
+lemma equiv_refl [iff]: "x \<approx> x"
   by (simp add: equiv_def)
 
-lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
+lemma equiv_sym: "x \<approx> y \<longleftrightarrow> y \<approx> x"
+  by (auto simp add: equiv_def)
+
+lemma equiv_trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
   by (auto simp: equiv_def intro: order_trans)
 
-lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
+lemma equiv_antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
   by (simp only: equiv_def)
 
 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
@@ -31,24 +40,55 @@
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
   by (auto simp add: equiv_def less_le)
 
-lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
+lemma le_imp_less_or_equiv: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
   by (simp add: less_le)
 
-lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
+lemma less_imp_not_equiv: "x < y \<Longrightarrow> \<not> x \<approx> y"
   by (simp add: less_le)
 
-lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
-  by (simp add: equiv_def less_le)
-
-lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
+lemma not_equiv_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
   by (simp add: less_le)
 
-lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
-  by (simp add: less_le)
+lemma le_not_equiv_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
+  by (rule not_equiv_le_trans)
 
 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
   by (simp add: equiv_def)
 
 end
 
+thm order_trans
+
+find_theorems "?i < ?j \<Longrightarrow> ?i \<le> ?j"
+
+ML_file \<open>~~/src/Provers/preorder.ML\<close>
+
+ML \<open>
+structure Quasi = Quasi_Tac(
+struct
+
+val le_trans = @{thm order_trans};
+val le_refl = @{thm order_refl};
+val eqD1 = @{thm equivD1};
+val eqD2 = @{thm equivD2};
+val less_reflE = @{thm less_irrefl};
+val less_imp_le = @{thm less_imp_le};
+val le_neq_trans = @{thm le_not_equiv_trans};
+val neq_le_trans = @{thm not_equiv_le_trans};
+val less_imp_neq = @{thm less_imp_not_equiv};
+
+fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2)
+  | decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2)
+  | decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2)
+  | decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2)
+  | decomp_quasi thy _ = NONE;
+
+fun decomp_trans thy t = case decomp_quasi thy t of
+    x as SOME (t1, "<=", t2) => x
+  | _ => NONE;
+
 end
+);
+\<close>
+
+end