|
61640
|
1 |
(* Author: Tobias Nipkow *)
|
|
|
2 |
|
|
67406
|
3 |
section \<open>Improved Simproc for $<$\<close>
|
|
61640
|
4 |
|
|
|
5 |
theory Less_False
|
|
|
6 |
imports Main
|
|
|
7 |
begin
|
|
|
8 |
|
|
67406
|
9 |
simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
|
|
61640
|
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;
|
|
69597
|
17 |
val le = Const (\<^const_name>\<open>less_eq\<close>, T);
|
|
61640
|
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
|
|
67406
|
29 |
\<close>
|
|
61640
|
30 |
|
|
|
31 |
end
|