src/HOL/antisym_setup.ML
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 19277 f7602e74d948
child 20836 9e40d815e002
permissions -rw-r--r--
simplified code generator setup
wenzelm@16833
     1
wenzelm@16833
     2
(* $Id$ *)
wenzelm@16833
     3
nipkow@15198
     4
local
nipkow@15198
     5
nipkow@15198
     6
val order_antisym_conv = thm "order_antisym_conv"
nipkow@15198
     7
val linorder_antisym_conv1 = thm "linorder_antisym_conv1"
nipkow@15198
     8
val linorder_antisym_conv2 = thm "linorder_antisym_conv2"
nipkow@15198
     9
val linorder_antisym_conv3 = thm "linorder_antisym_conv3"
nipkow@15198
    10
nipkow@15198
    11
fun prp t thm = (#prop(rep_thm thm) = t);
nipkow@15198
    12
nipkow@15198
    13
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
nipkow@15198
    14
  let val prems = prems_of_ss ss;
haftmann@19277
    15
      val less = Const("Orderings.less",T);
nipkow@15198
    16
      val t = HOLogic.mk_Trueprop(le $ s $ r);
nipkow@15198
    17
  in case Library.find_first (prp t) prems of
skalberg@15531
    18
       NONE =>
wenzelm@16833
    19
         let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
nipkow@15198
    20
         in case Library.find_first (prp t) prems of
skalberg@15531
    21
              NONE => NONE
skalberg@15531
    22
            | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
nipkow@15198
    23
         end
skalberg@15531
    24
     | SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv))
nipkow@15198
    25
  end
skalberg@15531
    26
  handle THM _ => NONE;
nipkow@15198
    27
nipkow@15198
    28
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
nipkow@15198
    29
  let val prems = prems_of_ss ss;
haftmann@19277
    30
      val le = Const("Orderings.less_eq",T);
nipkow@15198
    31
      val t = HOLogic.mk_Trueprop(le $ r $ s);
nipkow@15198
    32
  in case Library.find_first (prp t) prems of
skalberg@15531
    33
       NONE =>
nipkow@15198
    34
         let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
nipkow@15198
    35
         in case Library.find_first (prp t) prems of
skalberg@15531
    36
              NONE => NONE
skalberg@15531
    37
            | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3))
nipkow@15198
    38
         end
skalberg@15531
    39
     | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2))
nipkow@15198
    40
  end
skalberg@15531
    41
  handle THM _ => NONE;
nipkow@15198
    42
nipkow@15198
    43
val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
nipkow@15198
    44
  "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
nipkow@15198
    45
val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
nipkow@15198
    46
  "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
nipkow@15198
    47
nipkow@15198
    48
in
nipkow@15198
    49
nipkow@15198
    50
val antisym_setup =
wenzelm@18708
    51
 (fn thy => (Simplifier.change_simpset_of thy
wenzelm@18708
    52
  (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy));
nipkow@15198
    53
wenzelm@16833
    54
end