1. Function package accepts a parameter (default "some_term"), which specifies the functions
behaviour outside its domain.
2. Bugfix: An exception occured when a function in a mutual definition
was declared but no equation was given.
(* $Id$ *)
local
val order_antisym_conv = thm "order_antisym_conv"
val linorder_antisym_conv1 = thm "linorder_antisym_conv1"
val linorder_antisym_conv2 = thm "linorder_antisym_conv2"
val linorder_antisym_conv3 = thm "linorder_antisym_conv3"
fun prp t thm = (#prop(rep_thm thm) = t);
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
let val prems = prems_of_ss ss;
val less = Const("Orderings.less",T);
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case Library.find_first (prp t) prems of
NONE =>
let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
in case Library.find_first (prp t) prems of
NONE => NONE
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
end
| SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv))
end
handle THM _ => NONE;
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
let val prems = prems_of_ss ss;
val le = Const("Orderings.less_eq",T);
val t = HOLogic.mk_Trueprop(le $ r $ s);
in case Library.find_first (prp t) prems of
NONE =>
let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
in case Library.find_first (prp t) prems of
NONE => NONE
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3))
end
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2))
end
handle THM _ => NONE;
val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
"antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
"antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
in
val antisym_setup =
(fn thy => (Simplifier.change_simpset_of thy
(fn ss => ss addsimprocs [antisym_le, antisym_less]); thy));
end