13735
|
1 |
(*
|
|
2 |
Title: Term order, needed for normal forms in rings
|
|
3 |
Id: $Id$
|
13783
|
4 |
Author: Clemens Ballarin
|
13735
|
5 |
Copyright: TU Muenchen
|
|
6 |
*)
|
|
7 |
|
|
8 |
local
|
|
9 |
|
13783
|
10 |
(*** Lexicographic path order on terms.
|
13735
|
11 |
|
13783
|
12 |
See Baader & Nipkow, Term rewriting, CUP 1998.
|
|
13 |
Without variables. Const, Var, Bound, Free and Abs are treated all as
|
|
14 |
constants.
|
13735
|
15 |
|
13783
|
16 |
f_ord maps strings to integers and serves two purposes:
|
|
17 |
- Predicate on constant symbols. Those that are not recognised by f_ord
|
|
18 |
must be mapped to ~1.
|
|
19 |
- Order on the recognised symbols. These must be mapped to distinct
|
|
20 |
integers >= 0.
|
13735
|
21 |
|
13783
|
22 |
***)
|
13735
|
23 |
|
13783
|
24 |
fun dest_hd f_ord (Const (a, T)) =
|
|
25 |
let val ord = f_ord a in
|
|
26 |
if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
|
|
27 |
end
|
|
28 |
| dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
|
|
29 |
| dest_hd _ (Var v) = ((1, v), 1)
|
|
30 |
| dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
|
|
31 |
| dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
|
13735
|
32 |
|
13783
|
33 |
fun term_lpo f_ord (s, t) =
|
|
34 |
let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
|
|
35 |
if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
|
|
36 |
then case hd_ord f_ord (f, g) of
|
|
37 |
GREATER =>
|
|
38 |
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
|
|
39 |
then GREATER else LESS
|
|
40 |
| EQUAL =>
|
|
41 |
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
|
|
42 |
then list_ord (term_lpo f_ord) (ss, ts)
|
|
43 |
else LESS
|
|
44 |
| LESS => LESS
|
|
45 |
else GREATER
|
|
46 |
end
|
|
47 |
and hd_ord f_ord (f, g) = case (f, g) of
|
|
48 |
(Abs (_, T, t), Abs (_, U, u)) =>
|
|
49 |
(case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
|
|
50 |
| (_, _) => prod_ord (prod_ord int_ord
|
|
51 |
(prod_ord Term.indexname_ord Term.typ_ord)) int_ord
|
|
52 |
(dest_hd f_ord f, dest_hd f_ord g)
|
13735
|
53 |
|
|
54 |
in
|
|
55 |
|
13783
|
56 |
(*** Term order for commutative rings ***)
|
|
57 |
|
|
58 |
fun ring_ord a =
|
|
59 |
find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"];
|
|
60 |
|
|
61 |
fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
|
|
62 |
|
15531
|
63 |
(* SOME code useful for debugging
|
13735
|
64 |
|
13783
|
65 |
val intT = HOLogic.intT;
|
|
66 |
val a = Free ("a", intT);
|
|
67 |
val b = Free ("b", intT);
|
|
68 |
val c = Free ("c", intT);
|
|
69 |
val plus = Const ("op +", [intT, intT]--->intT);
|
|
70 |
val mult = Const ("op *", [intT, intT]--->intT);
|
|
71 |
val uminus = Const ("uminus", intT-->intT);
|
|
72 |
val one = Const ("1", intT);
|
|
73 |
val f = Const("f", intT-->intT);
|
|
74 |
|
|
75 |
*)
|
13735
|
76 |
|
|
77 |
(*** Rewrite rules ***)
|
|
78 |
|
|
79 |
val a_assoc = thm "ring.a_assoc";
|
|
80 |
val l_zero = thm "ring.l_zero";
|
|
81 |
val l_neg = thm "ring.l_neg";
|
|
82 |
val a_comm = thm "ring.a_comm";
|
|
83 |
val m_assoc = thm "ring.m_assoc";
|
|
84 |
val l_one = thm "ring.l_one";
|
|
85 |
val l_distr = thm "ring.l_distr";
|
|
86 |
val m_comm = thm "ring.m_comm";
|
|
87 |
val minus_def = thm "ring.minus_def";
|
|
88 |
val inverse_def = thm "ring.inverse_def";
|
|
89 |
val divide_def = thm "ring.divide_def";
|
|
90 |
val power_def = thm "ring.power_def";
|
|
91 |
|
|
92 |
(* These are the following axioms:
|
|
93 |
|
|
94 |
a_assoc: "(a + b) + c = a + (b + c)"
|
|
95 |
l_zero: "0 + a = a"
|
|
96 |
l_neg: "(-a) + a = 0"
|
|
97 |
a_comm: "a + b = b + a"
|
|
98 |
|
|
99 |
m_assoc: "(a * b) * c = a * (b * c)"
|
|
100 |
l_one: "1 * a = a"
|
|
101 |
|
|
102 |
l_distr: "(a + b) * c = a * c + b * c"
|
|
103 |
|
|
104 |
m_comm: "a * b = b * a"
|
|
105 |
|
|
106 |
-- {* Definition of derived operations *}
|
|
107 |
|
|
108 |
minus_def: "a - b = a + (-b)"
|
|
109 |
inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
|
|
110 |
divide_def: "a / b = a * inverse b"
|
|
111 |
power_def: "a ^ n = nat_rec 1 (%u b. b * a) n"
|
|
112 |
*)
|
|
113 |
|
|
114 |
(* These lemmas are needed in the proofs *)
|
|
115 |
val trans = thm "trans";
|
|
116 |
val sym = thm "sym";
|
|
117 |
val subst = thm "subst";
|
|
118 |
val box_equals = thm "box_equals";
|
|
119 |
val arg_cong = thm "arg_cong";
|
|
120 |
(* current theory *)
|
|
121 |
val thy = the_context ();
|
|
122 |
|
|
123 |
(* derived rewrite rules *)
|
|
124 |
val a_lcomm = prove_goal thy "(a::'a::ring)+(b+c) = b+(a+c)"
|
|
125 |
(fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1,
|
|
126 |
rtac (a_comm RS arg_cong) 1]);
|
|
127 |
val r_zero = prove_goal thy "(a::'a::ring) + 0 = a"
|
|
128 |
(fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
|
|
129 |
val r_neg = prove_goal thy "(a::'a::ring) + (-a) = 0"
|
|
130 |
(fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
|
|
131 |
val r_neg2 = prove_goal thy "(a::'a::ring) + (-a + b) = b"
|
|
132 |
(fn _ => [rtac (a_assoc RS sym RS trans) 1,
|
|
133 |
simp_tac (simpset() addsimps [r_neg, l_zero]) 1]);
|
|
134 |
val r_neg1 = prove_goal thy "-(a::'a::ring) + (a + b) = b"
|
|
135 |
(fn _ => [rtac (a_assoc RS sym RS trans) 1,
|
|
136 |
simp_tac (simpset() addsimps [l_neg, l_zero]) 1]);
|
|
137 |
(* auxiliary *)
|
|
138 |
val a_lcancel = prove_goal thy "!! a::'a::ring. a + b = a + c ==> b = c"
|
|
139 |
(fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2,
|
|
140 |
res_inst_tac [("a1", "a")] (l_neg RS subst) 1,
|
|
141 |
asm_simp_tac (simpset() addsimps [a_assoc]) 1]);
|
|
142 |
val minus_add = prove_goal thy "-((a::'a::ring) + b) = (-a) + (-b)"
|
|
143 |
(fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1,
|
|
144 |
simp_tac (simpset() addsimps [r_neg, l_neg, l_zero,
|
|
145 |
a_assoc, a_comm, a_lcomm]) 1]);
|
|
146 |
val minus_minus = prove_goal thy "-(-(a::'a::ring)) = a"
|
|
147 |
(fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]);
|
|
148 |
val minus0 = prove_goal thy "- 0 = (0::'a::ring)"
|
|
149 |
(fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1,
|
|
150 |
rtac (l_zero RS sym) 1]);
|
|
151 |
|
|
152 |
(* derived rules for multiplication *)
|
|
153 |
val m_lcomm = prove_goal thy "(a::'a::ring)*(b*c) = b*(a*c)"
|
|
154 |
(fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1,
|
|
155 |
rtac (m_comm RS arg_cong) 1]);
|
|
156 |
val r_one = prove_goal thy "(a::'a::ring) * 1 = a"
|
|
157 |
(fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
|
|
158 |
val r_distr = prove_goal thy "(a::'a::ring) * (b + c) = a * b + a * c"
|
|
159 |
(fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1,
|
|
160 |
simp_tac (simpset() addsimps [m_comm]) 1]);
|
|
161 |
(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
|
|
162 |
val l_null = prove_goal thy "0 * (a::'a::ring) = 0"
|
|
163 |
(fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1,
|
|
164 |
simp_tac (simpset() addsimps [r_zero]) 1]);
|
|
165 |
val r_null = prove_goal thy "(a::'a::ring) * 0 = 0"
|
|
166 |
(fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
|
|
167 |
val l_minus = prove_goal thy "(-(a::'a::ring)) * b = - (a * b)"
|
|
168 |
(fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
|
|
169 |
rtac (l_distr RS sym RS trans) 1,
|
|
170 |
simp_tac (simpset() addsimps [l_null, r_neg]) 1]);
|
|
171 |
val r_minus = prove_goal thy "(a::'a::ring) * (-b) = - (a * b)"
|
|
172 |
(fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
|
|
173 |
rtac (r_distr RS sym RS trans) 1,
|
|
174 |
simp_tac (simpset() addsimps [r_null, r_neg]) 1]);
|
|
175 |
|
|
176 |
val ring_ss = HOL_basic_ss settermless termless_ring addsimps
|
|
177 |
[a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
|
|
178 |
r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
|
13783
|
179 |
a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
|
|
180 |
|
|
181 |
(* Note: r_one is not necessary in ring_ss *)
|
13735
|
182 |
|
13783
|
183 |
val x = bind_thms ("ring_simps",
|
|
184 |
[l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,
|
13735
|
185 |
l_one, r_one, l_null, r_null, l_minus, r_minus]);
|
|
186 |
|
|
187 |
(* note: not added (and not proved):
|
|
188 |
a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one,
|
|
189 |
m_lcancel_eq, m_rcancel_eq,
|
|
190 |
thms involving dvd, integral domains, fields
|
|
191 |
*)
|
|
192 |
|
|
193 |
end; |