src/HOL/antisym_setup.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15531 08c8dad8e399
child 16833 a4e99217e9f9
permissions -rw-r--r--
Constant "If" is now local
nipkow@15198
     1
local
nipkow@15198
     2
nipkow@15198
     3
val order_antisym_conv = thm "order_antisym_conv"
nipkow@15198
     4
val linorder_antisym_conv1 = thm "linorder_antisym_conv1"
nipkow@15198
     5
val linorder_antisym_conv2 = thm "linorder_antisym_conv2"
nipkow@15198
     6
val linorder_antisym_conv3 = thm "linorder_antisym_conv3"
nipkow@15198
     7
nipkow@15198
     8
fun prp t thm = (#prop(rep_thm thm) = t);
nipkow@15198
     9
nipkow@15198
    10
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
nipkow@15198
    11
  let val prems = prems_of_ss ss;
nipkow@15198
    12
      val less = Const("op <",T);
nipkow@15198
    13
      val t = HOLogic.mk_Trueprop(le $ s $ r);
nipkow@15198
    14
  in case Library.find_first (prp t) prems of
skalberg@15531
    15
       NONE =>
nipkow@15198
    16
         let val t = HOLogic.mk_Trueprop(HOLogic.not_const $ (less $ r $ s))
nipkow@15198
    17
         in case Library.find_first (prp t) prems of
skalberg@15531
    18
              NONE => NONE
skalberg@15531
    19
            | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
nipkow@15198
    20
         end
skalberg@15531
    21
     | SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv))
nipkow@15198
    22
  end
skalberg@15531
    23
  handle THM _ => NONE;
nipkow@15198
    24
nipkow@15198
    25
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
nipkow@15198
    26
  let val prems = prems_of_ss ss;
nipkow@15198
    27
      val le = Const("op <=",T);
nipkow@15198
    28
      val t = HOLogic.mk_Trueprop(le $ r $ s);
nipkow@15198
    29
  in case Library.find_first (prp t) prems of
skalberg@15531
    30
       NONE =>
nipkow@15198
    31
         let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
nipkow@15198
    32
         in case Library.find_first (prp t) prems of
skalberg@15531
    33
              NONE => NONE
skalberg@15531
    34
            | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3))
nipkow@15198
    35
         end
skalberg@15531
    36
     | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2))
nipkow@15198
    37
  end
skalberg@15531
    38
  handle THM _ => NONE;
nipkow@15198
    39
nipkow@15198
    40
val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
nipkow@15198
    41
  "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
nipkow@15198
    42
val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
nipkow@15198
    43
  "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
nipkow@15198
    44
nipkow@15198
    45
in
nipkow@15198
    46
nipkow@15198
    47
val antisym_setup =
nipkow@15198
    48
 [Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
nipkow@15198
    49
nipkow@15198
    50
end