src/HOL/Data_Structures/Less_False.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Less_False.thy	Mon Sep 21 14:44:32 2015 +0200
@@ -0,0 +1,31 @@
+(* Author: Tobias Nipkow *)
+
+section {* Improved Simproc for $<$ *}
+
+theory Less_False
+imports Main
+begin
+
+simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
+  let
+    fun prp t thm = Thm.full_prop_of thm aconv t;
+
+    val eq_False_if_not = @{thm eq_False} RS iffD2
+
+    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
+      let val prems = Simplifier.prems_of ctxt;
+          val le = Const (@{const_name less_eq}, T);
+          val t = HOLogic.mk_Trueprop(le $ s $ r);
+      in case find_first (prp t) prems of
+           NONE =>
+             let val t = HOLogic.mk_Trueprop(less $ s $ r)
+             in case find_first (prp t) prems of
+                  NONE => NONE
+                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
+             end
+         | SOME thm => NONE
+      end;
+  in prove_less_False (Thm.term_of ct) end
+*}
+
+end