src/HOL/Data_Structures/Less_False.thy
changeset 61203 a8a8eca85801
child 61640 44c9198f210c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Less_False.thy	Mon Sep 21 14:44:32 2015 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section {* Improved Simproc for $<$ *}
     1.7 +
     1.8 +theory Less_False
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
    1.13 +  let
    1.14 +    fun prp t thm = Thm.full_prop_of thm aconv t;
    1.15 +
    1.16 +    val eq_False_if_not = @{thm eq_False} RS iffD2
    1.17 +
    1.18 +    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
    1.19 +      let val prems = Simplifier.prems_of ctxt;
    1.20 +          val le = Const (@{const_name less_eq}, T);
    1.21 +          val t = HOLogic.mk_Trueprop(le $ s $ r);
    1.22 +      in case find_first (prp t) prems of
    1.23 +           NONE =>
    1.24 +             let val t = HOLogic.mk_Trueprop(less $ s $ r)
    1.25 +             in case find_first (prp t) prems of
    1.26 +                  NONE => NONE
    1.27 +                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
    1.28 +             end
    1.29 +         | SOME thm => NONE
    1.30 +      end;
    1.31 +  in prove_less_False (Thm.term_of ct) end
    1.32 +*}
    1.33 +
    1.34 +end