15198
|
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
|
15531
|
15 |
NONE =>
|
15198
|
16 |
let val t = HOLogic.mk_Trueprop(HOLogic.not_const $ (less $ r $ s))
|
|
17 |
in case Library.find_first (prp t) prems of
|
15531
|
18 |
NONE => NONE
|
|
19 |
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
|
15198
|
20 |
end
|
15531
|
21 |
| SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv))
|
15198
|
22 |
end
|
15531
|
23 |
handle THM _ => NONE;
|
15198
|
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
|
15531
|
30 |
NONE =>
|
15198
|
31 |
let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
|
|
32 |
in case Library.find_first (prp t) prems of
|
15531
|
33 |
NONE => NONE
|
|
34 |
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3))
|
15198
|
35 |
end
|
15531
|
36 |
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2))
|
15198
|
37 |
end
|
15531
|
38 |
handle THM _ => NONE;
|
15198
|
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 |