equal
deleted
inserted
replaced
10 |
10 |
11 fun prp t thm = (#prop(rep_thm thm) = t); |
11 fun prp t thm = (#prop(rep_thm thm) = t); |
12 |
12 |
13 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) = |
13 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) = |
14 let val prems = prems_of_ss ss; |
14 let val prems = prems_of_ss ss; |
15 val less = Const("op <",T); |
15 val less = Const("Orderings.less",T); |
16 val t = HOLogic.mk_Trueprop(le $ s $ r); |
16 val t = HOLogic.mk_Trueprop(le $ s $ r); |
17 in case Library.find_first (prp t) prems of |
17 in case Library.find_first (prp t) prems of |
18 NONE => |
18 NONE => |
19 let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) |
19 let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) |
20 in case Library.find_first (prp t) prems of |
20 in case Library.find_first (prp t) prems of |
25 end |
25 end |
26 handle THM _ => NONE; |
26 handle THM _ => NONE; |
27 |
27 |
28 fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) = |
28 fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) = |
29 let val prems = prems_of_ss ss; |
29 let val prems = prems_of_ss ss; |
30 val le = Const("op <=",T); |
30 val le = Const("Orderings.less_eq",T); |
31 val t = HOLogic.mk_Trueprop(le $ r $ s); |
31 val t = HOLogic.mk_Trueprop(le $ r $ s); |
32 in case Library.find_first (prp t) prems of |
32 in case Library.find_first (prp t) prems of |
33 NONE => |
33 NONE => |
34 let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r)) |
34 let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r)) |
35 in case Library.find_first (prp t) prems of |
35 in case Library.find_first (prp t) prems of |