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