|
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 |