6 *) |
6 *) |
7 |
7 |
8 (*** Term order for commutative rings ***) |
8 (*** Term order for commutative rings ***) |
9 |
9 |
10 fun ring_ord a = |
10 fun ring_ord a = |
11 find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"]; |
11 find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"]; |
12 |
12 |
13 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); |
13 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); |
14 |
14 |
15 (* Some code useful for debugging |
15 (* Some code useful for debugging |
16 |
16 |
17 val intT = HOLogic.intT; |
17 val intT = HOLogic.intT; |
18 val a = Free ("a", intT); |
18 val a = Free ("a", intT); |
19 val b = Free ("b", intT); |
19 val b = Free ("b", intT); |
20 val c = Free ("c", intT); |
20 val c = Free ("c", intT); |
21 val plus = Const ("op +", [intT, intT]--->intT); |
21 val plus = Const ("HOL.plus", [intT, intT]--->intT); |
22 val mult = Const ("op *", [intT, intT]--->intT); |
22 val mult = Const ("HOL.times", [intT, intT]--->intT); |
23 val uminus = Const ("uminus", intT-->intT); |
23 val uminus = Const ("HOL.uminus", intT-->intT); |
24 val one = Const ("1", intT); |
24 val one = Const ("1", intT); |
25 val f = Const("f", intT-->intT); |
25 val f = Const("f", intT-->intT); |
26 |
26 |
27 *) |
27 *) |
28 |
28 |