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