1(* Author: Tobias Nipkow *)
2
3section \<open>Improved Simproc for $<$\<close>
4
5theory Less_False
6imports Main
7begin
8
9simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
10  let
11    fun prp t thm = Thm.full_prop_of thm aconv t;
12
13    val eq_False_if_not = @{thm eq_False} RS iffD2
14
15    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
16      let val prems = Simplifier.prems_of ctxt;
17          val le = Const (@{const_name less_eq}, T);
18          val t = HOLogic.mk_Trueprop(le $ s $ r);
19      in case find_first (prp t) prems of
20           NONE =>
21             let val t = HOLogic.mk_Trueprop(less $ s $ r)
22             in case find_first (prp t) prems of
23                  NONE => NONE
24                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
25             end
26         | SOME thm => NONE
27      end;
28  in prove_less_False (Thm.term_of ct) end
29\<close>
30
31end
32