1structure NumRelNorms :> NumRelNorms =
2struct
3
4open HolKernel boolLib
5
6(* ----------------------------------------------------------------------
7    basic canonisers
8   ---------------------------------------------------------------------- *)
9
10(* first define the records containing the necessary information for the
11   generic canoniser *)
12
13(* for addition - right-associated for backwards compatibility *)
14local
15  open numSyntax arithmeticTheory GenPolyCanon
16  fun is_good t = let
17    val (l,r) = dest_mult t
18  in
19    is_numeral l
20  end handle HOL_ERR _ => false
21  fun non_coeff t = if is_good t then rand t
22                    else if is_numeral t then mk_var("   ", num)
23                    else t
24  fun add_coeff (t:term) : thm = if is_good t then ALL_CONV t
25                    else REWR_CONV (GSYM MULT_LEFT_1) t
26  val distrib = GSYM RIGHT_ADD_DISTRIB
27  fun merge t = let
28    val (l,r) = dest_plus t
29  in
30    if is_numeral l andalso is_numeral r then
31      reduceLib.REDUCE_CONV
32    else
33      Conv.BINOP_CONV add_coeff THENC
34      REWR_CONV distrib THENC LAND_CONV reduceLib.REDUCE_CONV
35  end t
36in
37  val rnatadd_gci =
38      GCI { dest = dest_plus,
39            assoc_mode = R,
40            assoc = ADD_ASSOC,
41            symassoc = GSYM ADD_ASSOC,
42            comm = ADD_COMM,
43            r_asscomm = derive_r_asscomm ADD_ASSOC ADD_COMM,
44            l_asscomm = derive_l_asscomm ADD_ASSOC ADD_COMM,
45            is_literal = is_numeral,
46            non_coeff = non_coeff, merge = merge,
47            postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL MULT)) ORELSEC
48            TRY_CONV (REWR_CONV MULT_LEFT_1),
49            left_id = CONJUNCT1 ADD,
50            right_id = ADD_0,
51            reducer = reduceLib.REDUCE_CONV}
52  val lnatadd_gci =
53      GCI { dest = dest_plus,
54            assoc_mode = L,
55            assoc = ADD_ASSOC,
56            symassoc = GSYM ADD_ASSOC,
57            comm = ADD_COMM,
58            r_asscomm = derive_r_asscomm ADD_ASSOC ADD_COMM,
59            l_asscomm = derive_l_asscomm ADD_ASSOC ADD_COMM,
60            is_literal = is_numeral,
61            non_coeff = non_coeff, merge = merge,
62            postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL MULT)) ORELSEC
63            TRY_CONV (REWR_CONV MULT_LEFT_1),
64            left_id = CONJUNCT1 ADD,
65            right_id = ADD_0,
66            reducer = reduceLib.REDUCE_CONV}
67end
68
69val ADDL_CANON_CONV = GenPolyCanon.gencanon lnatadd_gci
70val ADDR_CANON_CONV = GenPolyCanon.gencanon rnatadd_gci
71
72
73
74
75
76(* multiplication *)
77val lcnatmult_gci = let
78  open GenPolyCanon numSyntax arithmeticTheory
79  fun is_good t = let
80    val (l,r) = dest_exp t
81  in
82    is_numeral r
83  end handle HOL_ERR _ => false
84  fun non_coeff t = if is_good t then rand (rator t)
85                    else if is_numeral t then mk_numeral Arbnum.one
86                    else t
87  fun add_coeff t = if is_good t then ALL_CONV t
88                    else REWR_CONV (GSYM (CONJUNCT2 (SPEC_ALL EXP_1))) t
89  val distrib = GSYM EXP_ADD
90  fun merge t = let
91    val (l,r) = dest_mult t
92  in
93    if is_numeral l andalso is_numeral r then reduceLib.REDUCE_CONV
94    else Conv.BINOP_CONV add_coeff THENC REWR_CONV distrib THENC
95         reduceLib.REDUCE_CONV
96  end t
97in
98  GCI { dest = dest_mult,
99        is_literal = is_numeral,
100        assoc_mode = L_Cflipped,
101        assoc = MULT_ASSOC,
102        symassoc = GSYM MULT_ASSOC,
103        comm = MULT_COMM,
104        r_asscomm = derive_r_asscomm MULT_ASSOC MULT_COMM,
105        l_asscomm = derive_l_asscomm MULT_ASSOC MULT_COMM,
106        non_coeff = non_coeff,
107        merge = merge,
108        postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL EXP)) ORELSEC
109                   TRY_CONV (REWR_CONV (CONJUNCT2 (SPEC_ALL EXP_1))),
110        right_id = MULT_RIGHT_1,
111        left_id = MULT_LEFT_1,
112        reducer = reduceLib.REDUCE_CONV}
113end
114
115val MUL_CANON_CONV = GenPolyCanon.gencanon lcnatmult_gci
116
117
118
119(* normalisation of sums over relational operators *)
120structure NumRel_Base =
121struct
122  open numSyntax Abbrev
123  type t = Arbint.int
124  val dest = dest_plus
125  val zero = Arbint.zero
126  val one = Arbint.one
127  val one_t = mk_numeral (Arbint.toNat one)
128  val mk = mk_plus
129  val listmk = list_mk_plus
130  fun toNat t = Arbint.fromNat (dest_numeral t)
131  fun destf t = let
132    val (l,r) = dest_mult t
133  in
134    (toNat l, r)
135  end handle HOL_ERR _ => if is_numeral t then (toNat t, one_t)
136                          else (Arbint.one, t)
137  fun mkf (i,t) = let
138    val i_t = mk_numeral(Arbint.toNat i)
139  in
140    if aconv t one_t then i_t else mk_mult(i_t, t)
141  end
142  val canon = ADDR_CANON_CONV
143  val addid = REWR_CONV (GSYM arithmeticTheory.ADD_0)
144  val op+ = Arbint.+
145  val op- = Arbint.-
146  val op~ = Arbint.~
147  val op < = Arbint.<
148end
149
150structure LEQ_NREL : RelNorm_Input = struct
151  open NumRel_Base
152  val destrel = dest_leq
153  val opr = leq_tm
154  val rwt = arithmeticTheory.LE_ADD_LCANCEL
155end
156
157structure LT_NREL : RelNorm_Input = struct
158  open NumRel_Base
159  val destrel = dest_less
160  val opr = less_tm
161  val rwt = arithmeticTheory.LT_ADD_LCANCEL
162end
163
164structure EQ_NREL : RelNorm_Input = struct
165  open NumRel_Base
166  val destrel = dest_eq
167  val opr = mk_thy_const{Name = "=", Thy = "min", Ty = num --> num --> bool}
168  val rwt = arithmeticTheory.EQ_ADD_LCANCEL
169end
170
171structure NumLEQNorm = GenRelNorm (LEQ_NREL);
172structure NumLTNorm = GenRelNorm (LT_NREL);
173structure NumEQNorm = GenRelNorm (EQ_NREL);
174
175val sum_leq_norm = NumLEQNorm.gen_relnorm
176val sum_lt_norm = NumLTNorm.gen_relnorm
177val sum_eq_norm = NumEQNorm.gen_relnorm
178
179
180end;
181