src/HOL/Data_Structures/Less_False.thy
author nipkow
Mon Sep 21 14:44:32 2015 +0200 (2015-09-21)
changeset 61203 a8a8eca85801
child 61640 44c9198f210c
permissions -rw-r--r--
New subdirectory for functional data structures
     1 (* Author: Tobias Nipkow *)
     2 
     3 section {* Improved Simproc for $<$ *}
     4 
     5 theory Less_False
     6 imports Main
     7 begin
     8 
     9 simproc_setup less_False ("(x::'a::order) < y") = {* 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 *}
    30 
    31 end