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
     1 local
     2 
     3 val order_antisym_conv = thm "order_antisym_conv"
     4 val linorder_antisym_conv1 = thm "linorder_antisym_conv1"
     5 val linorder_antisym_conv2 = thm "linorder_antisym_conv2"
     6 val linorder_antisym_conv3 = thm "linorder_antisym_conv3"
     7 
     8 fun prp t thm = (#prop(rep_thm thm) = t);
     9 
    10 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
    11   let val prems = prems_of_ss ss;
    12       val less = Const("op <",T);
    13       val t = HOLogic.mk_Trueprop(le $ s $ r);
    14   in case Library.find_first (prp t) prems of
    15        NONE =>
    16          let val t = HOLogic.mk_Trueprop(HOLogic.not_const $ (less $ r $ s))
    17          in case Library.find_first (prp t) prems of
    18               NONE => NONE
    19             | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
    20          end
    21      | SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv))
    22   end
    23   handle THM _ => NONE;
    24 
    25 fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
    26   let val prems = prems_of_ss ss;
    27       val le = Const("op <=",T);
    28       val t = HOLogic.mk_Trueprop(le $ r $ s);
    29   in case Library.find_first (prp t) prems of
    30        NONE =>
    31          let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
    32          in case Library.find_first (prp t) prems of
    33               NONE => NONE
    34             | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3))
    35          end
    36      | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2))
    37   end
    38   handle THM _ => NONE;
    39 
    40 val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
    41   "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
    42 val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
    43   "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
    44 
    45 in
    46 
    47 val antisym_setup =
    48  [Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
    49 
    50 end