src/HOL/antisym_setup.ML
author nipkow
Sat Sep 11 09:25:47 2004 +0200 (2004-09-11)
changeset 15198 44495334adcc
child 15531 08c8dad8e399
permissions -rw-r--r--
antisymmetry simproc
     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