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