antisymmetry simproc
authornipkow
Sat Sep 11 09:25:47 2004 +0200 (2004-09-11)
changeset 1519844495334adcc
parent 15197 19e735596e51
child 15199 29ca1fe63e7b
antisymmetry simproc
src/HOL/antisym_setup.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/antisym_setup.ML	Sat Sep 11 09:25:47 2004 +0200
     1.3 @@ -0,0 +1,50 @@
     1.4 +local
     1.5 +
     1.6 +val order_antisym_conv = thm "order_antisym_conv"
     1.7 +val linorder_antisym_conv1 = thm "linorder_antisym_conv1"
     1.8 +val linorder_antisym_conv2 = thm "linorder_antisym_conv2"
     1.9 +val linorder_antisym_conv3 = thm "linorder_antisym_conv3"
    1.10 +
    1.11 +fun prp t thm = (#prop(rep_thm thm) = t);
    1.12 +
    1.13 +fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
    1.14 +  let val prems = prems_of_ss ss;
    1.15 +      val less = Const("op <",T);
    1.16 +      val t = HOLogic.mk_Trueprop(le $ s $ r);
    1.17 +  in case Library.find_first (prp t) prems of
    1.18 +       None =>
    1.19 +         let val t = HOLogic.mk_Trueprop(HOLogic.not_const $ (less $ r $ s))
    1.20 +         in case Library.find_first (prp t) prems of
    1.21 +              None => None
    1.22 +            | Some thm => Some(mk_meta_eq(thm RS linorder_antisym_conv1))
    1.23 +         end
    1.24 +     | Some thm => Some(mk_meta_eq(thm RS order_antisym_conv))
    1.25 +  end
    1.26 +  handle THM _ => None;
    1.27 +
    1.28 +fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
    1.29 +  let val prems = prems_of_ss ss;
    1.30 +      val le = Const("op <=",T);
    1.31 +      val t = HOLogic.mk_Trueprop(le $ r $ s);
    1.32 +  in case Library.find_first (prp t) prems of
    1.33 +       None =>
    1.34 +         let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
    1.35 +         in case Library.find_first (prp t) prems of
    1.36 +              None => None
    1.37 +            | Some thm => Some(mk_meta_eq(thm RS linorder_antisym_conv3))
    1.38 +         end
    1.39 +     | Some thm => Some(mk_meta_eq(thm RS linorder_antisym_conv2))
    1.40 +  end
    1.41 +  handle THM _ => None;
    1.42 +
    1.43 +val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
    1.44 +  "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
    1.45 +val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
    1.46 +  "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
    1.47 +
    1.48 +in
    1.49 +
    1.50 +val antisym_setup =
    1.51 + [Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
    1.52 +
    1.53 +end
    1.54 \ No newline at end of file