1(*Interactive use only... 2 3load "translateTheory"; 4load "intLib"; 5load "translateLib"; 6load "signedintTheory"; 7load "integerTheory"; 8quietdec := true; 9use "extendTranslateScript.sml" handle _ => quietdec := false; 10quietdec := false; 11*) 12 13open Term Type Thm Theory Tactic Tactical Drule Rewrite boolSyntax; 14open Lib bossLib Conv Parse 15open sexpTheory arithmeticTheory integerTheory intLib boolTheory 16 (*hol_defaxiomsTheory*) translateLib translateTheory; 17 18val fix_def=hol_defaxiomsTheory.fix_def; 19val zip_def = hol_defaxiomsTheory.zip_def; 20val nfix_def=hol_defaxiomsTheory.nfix_def; 21val not_def = hol_defaxiomsTheory.not_def; 22val ifix_def = hol_defaxiomsTheory.ifix_def; 23val endp_def = hol_defaxiomsTheory.endp_def; 24val atom_def = hol_defaxiomsTheory.atom_def; 25val zp_def = hol_defaxiomsTheory.zp_def; 26val eql_def = hol_defaxiomsTheory.eql_def; 27 28(*****************************************************************************) 29(* Start new theory "extendTranslate" *) 30(*****************************************************************************) 31 32val _ = new_theory "extendTranslate"; 33 34(*****************************************************************************) 35(* CHOOSEP_TAC : performs the following for ints & nums: *) 36(* *) 37(* A u {|= integerp a} |- G *) 38(* -------------------------------- CHOOSEP_TAC *) 39(* A [int a' / a] |- G [int a' / a] *) 40(* *) 41(*****************************************************************************) 42 43val CHOOSEP_TAC = 44 translateLib.CHOOSEP_TAC 45 [DECENC_BOOL,DECENC_INT,DECENC_NAT,INT_OF_SEXP_TO_INT,NAT_OF_SEXP_TO_NAT]; 46 47(*****************************************************************************) 48(* Lemmas to assist proof *) 49(*****************************************************************************) 50 51val FIX_INT = store_thm("FIX_INT", 52 ``fix (int a) = int a``, 53 RW_TAC arith_ss [fix_def,int_def,acl2_numberp_def,cpx_def,ite_def, 54 TRUTH_REWRITES]); 55 56(*****************************************************************************) 57(* Exponentiation for int and num using acl2 function EXPT *) 58(*****************************************************************************) 59 60val NUM_OF_ABS = save_thm("NUM_OF_ABS", 61 EQ_MP (GSYM (Q.SPEC `ABS p` INT_OF_NUM)) (SPEC_ALL INT_ABS_POS)); 62 63val (acl2_expt_def,acl2_expt_ind) = 64 (REWRITE_RULE [GSYM ite_def] ## I) 65 (sexp.acl2_defn "ACL2::EXPT" 66 (`acl2_expt r i = 67 if zip i = nil then 68 (ite (equal (fix r) (int 0)) (int 0) 69 (if less (int 0) i = nil 70 then (mult (reciprocal r) (acl2_expt r (add i (int 1)))) 71 else (mult r (acl2_expt r (add i (unary_minus (int 1))))))) 72 else int 1`, 73 WF_REL_TAC `measure (\a. Num (ABS (sexp_to_int (SND a))))` THEN 74 RW_TAC std_ss [] THEN 75 FULL_SIMP_TAC std_ss [zip_def,TRUTH_REWRITES,ite_def,GSYM int_def] THEN 76 CHOOSEP_TAC THEN 77 FULL_SIMP_TAC int_ss [GSYM INT_THMS,TRUTH_REWRITES,SEXP_TO_INT_OF_INT] THEN 78 ONCE_REWRITE_TAC [GSYM integerTheory.INT_LT] THEN 79 REWRITE_TAC [NUM_OF_ABS] THEN 80 ARITH_TAC)); 81 82val INT_EXPT = store_thm("INT_EXPT", 83 ``!b a. int (a ** b) = acl2_expt (int a) (nat b)``, 84 Induct THEN ONCE_REWRITE_TAC [acl2_expt_def] THEN 85 RW_TAC int_ss [GSYM INT_THMS,nat_def,ite_def,TRUTH_REWRITES,zip_def, 86 INTEGERP_INT,GSYM int_def,int_exp,FIX_INT, 87 INT_ADD_CALCULATE] THEN 88 FULL_SIMP_TAC int_ss [int_gt,INT_LT_CALCULATE] THEN 89 RW_TAC int_ss [INT_MULT,nat_def]); 90 91val NAT_EXPT = store_thm("NAT_EXPT", 92 ``!b a. nat (a ** b) = acl2_expt (nat a) (nat b)``, 93 RW_TAC std_ss [nat_def,INT_EXPT,GSYM INT_EXP]); 94 95(*****************************************************************************) 96(* Integer division and modulus *) 97(*****************************************************************************) 98 99val (nniq_def,nniq_induction) = 100 Defn.tprove(Defn.Hol_defn "nniq" 101 `nniq (a:int) (b:int) = (if b <= 0i then 0i else 102 (if a < b then 0 else 1 + nniq (a - b) b))`, 103 WF_REL_TAC `measure (\a.Num (FST a))` THEN REPEAT STRIP_TAC THEN 104 ONCE_REWRITE_TAC [GSYM INT_LT_CALCULATE] THEN 105 `0 <= a /\ 0 <= a - b` by ARITH_TAC THEN 106 RW_TAC std_ss [snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM))] THEN ARITH_TAC); 107 108val (acl2_nniq_def,acl2_nniq_ind) = 109 (REWRITE_RULE [GSYM ite_def] ## I) 110 (sexp.acl2_defn "ACL2::NONNEGATIVE-INTEGER-QUOTIENT" 111 (`acl2_nniq i j = 112 if (equal (nfix j) (int 0)) = nil then ( 113 if less (ifix i) j = nil 114 then (add (int 1) (acl2_nniq (add i (unary_minus j)) j)) 115 else (int 0)) 116 else (int 0)`, 117 WF_REL_TAC `measure (\a. Num (ABS (sexp_to_int (FST a))))` THEN 118 RW_TAC std_ss [equal_def,TRUTH_REWRITES,nfix_def,not_def, 119 andl_def,ite_def,nat_def,ifix_def] THEN 120 FULL_SIMP_TAC int_ss [] THEN 121 CHOOSEP_TAC THEN 122 FULL_SIMP_TAC int_ss [GSYM INT_THMS,TRUTH_REWRITES,INT_CONG] THEN 123 REWRITE_TAC [GSYM integerTheory.INT_LT,NUM_OF_ABS,SEXP_TO_INT_OF_INT] THEN 124 ARITH_TAC)); 125 126val _ = overload_on("acl2_nniq", 127 fst (strip_comb (lhs (snd (strip_forall 128 (concl acl2_nniq_def)))))); 129 130val INT_NNIQ = store_thm("INT_NNIQ", 131 ``int (nniq a b) = acl2_nniq (int a) (int b)``, 132 completeInduct_on `Num (ABS a)` THEN FIX_CI_TAC THEN 133 ONCE_REWRITE_TAC [nniq_def,acl2_nniq_def] THEN 134 RW_TAC std_ss [nfix_def,ifix_def,nat_def,GSYM INT_THMS,andl_def,equal_def, 135 ite_def,TRUTH_REWRITES,INTEGERP_INT,not_def] THEN 136 REPEAT (POP_ASSUM MP_TAC) THEN 137 RW_TAC int_ss [INT_CONG,int_gt,INT_NOT_LT,INT_THMS] THEN 138 TRY (CCONTR_TAC THEN POP_ASSUM (K ALL_TAC) THEN ARITH_TAC) THEN 139 REPEAT AP_TERM_TAC THEN REWRITE_TAC [GSYM INT_THMS] THEN 140 FIRST_ASSUM MATCH_MP_TAC THEN 141 RW_TAC std_ss [GSYM integerTheory.INT_LT,NUM_OF_ABS] THEN ARITH_TAC); 142 143val acl2_nniq_correct = 144 REWRITE_RULE [SEXP_TO_INT_OF_INT] (AP_TERM ``sexp_to_int`` INT_NNIQ); 145 146val acl2_nniq_rewrite = GSYM INT_NNIQ; 147 148val int_nat_lem = store_thm("int_nat_lem", 149 ``0i <= a ==> ?a'. a = & a'``, 150 STRIP_TAC THEN Q.EXISTS_TAC `Num a` THEN 151 CONV_TAC SYM_CONV THEN ASM_REWRITE_TAC [INT_OF_NUM]); 152 153val nniq_eq_lem = prove( 154 ``~(b = 0) ==> (nniq (& a) (& b) = int_div (& a) (& b))``, 155 completeInduct_on `a` THEN ONCE_REWRITE_TAC [nniq_def] THEN 156 RW_TAC int_ss [int_div,LESS_DIV_EQ_ZERO, 157 INT_SUB_CALCULATE,INT_ADD_CALCULATE] THEN 158 MATCH_MP_TAC (DECIDE ``0 < b /\ (a = b - 1n) ==> (a + 1 = b)``) THEN 159 CONJ_TAC THEN1 ( 160 RW_TAC arith_ss [X_LT_DIV]) THEN 161 METIS_TAC [DIV_SUB,MULT_CLAUSES,NOT_LESS,DECIDE ``0 < a = ~(a = 0n)``]); 162 163val NNIQ_EQ_DIV = store_thm("NNIQ_EQ_DIV", 164 ``0 <= a /\ 0 <= b /\ ~(b = 0) ==> (nniq a b = int_div a b)``, 165 STRIP_TAC THEN IMP_RES_TAC int_nat_lem THEN 166 REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN MATCH_MP_TAC nniq_eq_lem THEN 167 ARITH_TAC); 168 169val acl2_floor_def = sexp.acl2Define "ACL2::FLOOR" 170 `acl2_floor a b = 171 let q = mult a (reciprocal b) in 172 let n = numerator q in 173 let d = denominator q in 174 ite (equal d (int 1)) n 175 (ite (not (less n (int 0))) 176 (acl2_nniq n d) 177 (add (unary_minus (acl2_nniq (unary_minus n) d)) 178 (unary_minus (int 1))))`; 179 180 181val acl2_truncate_def = sexp.acl2Define "ACL2::TRUNCATE" 182 `acl2_truncate a b = 183 let q = mult a (reciprocal b) in 184 let n = numerator q in 185 let d = denominator q in 186 ite (equal d (int 1)) n 187 (ite (not (less n (int 0))) 188 (acl2_nniq n d) 189 (unary_minus (acl2_nniq (unary_minus n) d)))`; 190 191val INT_SGN_SQUARE = store_thm("INT_SGN_SQUARE", 192 ``~(a = 0) ==> (SGN (a * a) = 1)``, 193 RW_TAC int_ss [intExtensionTheory.SGN_def,INT_MUL_SIGN_CASES] THEN 194 ARITH_TAC); 195 196val INT_ABS_SQUARE = store_thm("INT_ABS_SQUARE", 197 ``ABS (b * b) = b * b``, 198 RW_TAC int_ss [INT_ABS,INT_MUL_SIGN_CASES] THEN ARITH_TAC); 199 200val rat_mul_lem = prove(``0 < c * b /\ 0 < c ==> 201 (abs_rat (abs_frac (a * b,c * b)) = abs_rat (abs_frac (a,c)))``, 202 RW_TAC int_ss [ratTheory.RAT_EQ_CALCULATE,fracTheory.NMR, 203 fracTheory.DNM] THEN 204 ARITH_TAC); 205 206open dividesTheory gcdTheory; 207 208val both_divides = prove(``(a * b = c) ==> divides a c /\ divides b c``, 209 METIS_TAC [divides_def,MULT_COMM]); 210 211val coprime_equal = prove( 212 ``(gcd a d = 1) /\ (gcd b c = 1) /\ (a * b = c * d) 213 ==> (a = c) /\ (b = d)``, 214 DISCH_TAC THEN POP_ASSUM STRIP_ASSUME_TAC THEN 215 FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP both_divides) THEN 216 FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP both_divides o GSYM) THEN 217 METIS_TAC [L_EUCLIDES,GCD_SYM,MULT_COMM,DIVIDES_ANTISYM]); 218 219val num_abs_nz = prove(``0 < b \/ ~(b = 0) ==> ~(Num (ABS b) = 0)``, 220 DISCH_TAC THEN ONCE_REWRITE_TAC [GSYM INT_EQ_CALCULATE] THEN 221 RW_TAC std_ss [snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)),INT_ABS_POS] THEN 222 ARITH_TAC); 223 224val r1 = prove(``a < 0 ==> (a = ~& (Num ~a))``, 225 METIS_TAC [INT_NEG_GT0,INT_OF_NUM,INT_LT_IMP_LE,INT_NEG_EQ]); 226val r2 = prove(``0 < a ==> (a = & (Num a))``, 227 METIS_TAC [INT_NEG_GT0,INT_OF_NUM,INT_LT_IMP_LE]); 228 229val FACTOR_GCD2 = prove( 230 ``!n m. ~(n = 0) /\ ~(m = 0) ==> 231 ?p q. (n = p * gcd n m) /\ (m = q * gcd n m) /\ 232 (gcd p q = 1) /\ ~(gcd n m = 0)``, 233 RW_TAC std_ss [FACTOR_OUT_GCD,GCD_EQ_0]); 234 235fun find_gcd term = 236 if can (match_term ``gcd a b``) term then [term] else 237 (op@ o (find_gcd ## find_gcd)) (dest_comb term) handle _ => []; 238 239fun GCD_FACTOR_GOAL (assums,goal) = 240let val match = PART_MATCH (fst o dest_eq o dest_neg o last o strip_conj o snd o strip_exists o snd o dest_imp o snd o strip_forall) FACTOR_GCD2 in 241(MAP_EVERY (fn x => (STRIP_ASSUME_TAC (SIMP_RULE std_ss (map ASSUME assums) (match x)))) (mk_set (find_gcd goal))) (assums,goal) 242end; 243 244 245 246 247val reduce_thm = 248 store_thm 249 ("reduce_thm", 250 ``0 < b /\ 0 < y /\ 251 ((0 < a /\ 0 < x) \/ (x < 0 /\ a < 0)) /\ (x * b = a * y) ==> 252 (int_div x (& (gcd (Num (ABS x)) (Num (ABS y)))) = 253 int_div a (& (gcd (Num (ABS a)) (Num (ABS b))))) /\ 254 (int_div y (& (gcd (Num (ABS x)) (Num (ABS y)))) = 255 int_div b (& (gcd (Num (ABS a)) (Num (ABS b)))))``, 256 REPEAT STRIP_TAC THEN 257 FULL_SIMP_TAC int_ss [num_abs_nz,GCD_EQ_0,INT_DIV_0] THEN 258 EVERY_ASSUM (fn th => (SUBST_ALL_TAC o MATCH_MP r1) th THEN 259 ASSUME_TAC th handle _ => ALL_TAC) THEN 260 EVERY_ASSUM (fn th => (SUBST_ALL_TAC o MATCH_MP r2) th THEN 261 ASSUME_TAC th handle _ => ALL_TAC) THEN 262 FULL_SIMP_TAC std_ss [INT_NEG_LT0,GSYM INT_NEG_GT0,INT_LT_CALCULATE, 263 GSYM INT_NEG_LMUL,GSYM INT_NEG_RMUL, 264 DECIDE ``0 < a = ~(a = 0n)``,INT_ABS_NEG,NUM_OF_INT, 265 INT_ABS_NUM,INT_NEG_MUL2,INT_MUL,INT_EQ_CALCULATE] THEN 266 GCD_FACTOR_GOAL THEN 267 ASSUM_LIST (fn list => GEN_REWRITE_TAC 268 (BINOP_CONV o LAND_CONV o DEPTH_CONV) (bool_rewrites) list) THEN 269 RW_TAC std_ss [INT_DIV_RMUL,GSYM INT_MUL,INT_NEG_LMUL,INT_EQ_CALCULATE, 270 ARITH_PROVE ``~(a = 0) ==> ~(& a = 0i)``] THEN 271 PAT_ASSUM ``a * b = c * d:num`` MP_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN 272 ONCE_REWRITE_TAC [ 273 prove(``(a * b * (c * d) = e * d * (g * b)) = 274 (b * (d * (a * c)) = b * (d * (e * g:num)))``, 275 HO_MATCH_MP_TAC 276 (PROVE [] ``(a = c) /\ (b = d) ==> (f a b = f c d)``) THEN 277 CONJ_TAC THEN 278 CONV_TAC (AC_CONV (MULT_ASSOC,MULT_COMM)))] THEN 279 RW_TAC std_ss [EQ_MULT_LCANCEL] THEN 280 MAP_FIRST (fn x => x THEN 281 REPEAT CONJ_TAC THEN 282 MAP_FIRST FIRST_ASSUM [ 283 ACCEPT_TAC, 284 ACCEPT_TAC o ONCE_REWRITE_RULE [GCD_SYM], 285 ACCEPT_TAC o GSYM]) [ 286 MATCH_MP_TAC (GEN_ALL (DISCH_ALL (CONJUNCT1 287 (UNDISCH coprime_equal)))) THEN 288 MAP_EVERY Q.EXISTS_TAC [`q`,`q'`], 289 MATCH_MP_TAC (GEN_ALL (DISCH_ALL (CONJUNCT2 290 (UNDISCH coprime_equal)))) THEN 291 MAP_EVERY Q.EXISTS_TAC [`p`,`p'`]]); 292 293val div_id_lem = prove(``0 < a ==> (int_div a (& (Num (ABS a))) = 1i)``, 294 STRIP_TAC THEN `0 <= a` by ARITH_TAC THEN IMP_RES_TAC int_nat_lem THEN 295 RW_TAC int_ss [INT_ABS_NUM] THEN MATCH_MP_TAC INT_DIV_ID THEN 296 ARITH_TAC); 297 298val div_zero_lem = prove(``0 < a ==> (int_div 0 (& (Num (ABS a))) = 0i)``, 299 STRIP_TAC THEN `0 <= a` by ARITH_TAC THEN IMP_RES_TAC int_nat_lem THEN 300 RW_TAC int_ss [INT_ABS_NUM] THEN MATCH_MP_TAC INT_DIV_0 THEN 301 ARITH_TAC); 302 303val int_sign_lem = prove(``0i < a /\ 0 < b /\ (x * a = y * b) /\ ~(x = 0) ==> 304 (0 < x /\ 0 < y \/ y < 0 /\ x < 0)``, 305 STRIP_TAC THEN `0 < x \/ x < 0` by ARITH_TAC THEN Cases_on `y = 0` THEN 306 FULL_SIMP_TAC int_ss [] THEN `0 < y \/ y < 0` by ARITH_TAC THEN 307 RW_TAC int_ss [] THEN 308 METIS_TAC [INT_MUL_SIGN_CASES, 309 ARITH_PROVE ``0 < a /\ b < 0 ==> ~(a = b:int)``]); 310 311val REDUCE_CONG = store_thm("REDUCE_CONG", 312 ``0 < b ==> 313 (reduce (rep_frac (rep_rat (abs_rat (abs_frac (a,b))))) = 314 reduce (a,b))``, 315 RAT_CONG_TAC THEN 316 ONCE_REWRITE_TAC [GSYM fracTheory.FRAC] THEN POP_ASSUM MP_TAC THEN 317 Cases_on `a = 0` THEN 318 RW_TAC int_ss [fst (EQ_IMP_RULE (SPEC_ALL (CONJUNCT2 319 (BETA_RULE fracTheory.frac_tybij)))),fracTheory.FRAC_DNMPOS, 320 fracTheory.DNM,fracTheory.NMR] THEN 321 RW_TAC (int_ss ++ boolSimps.LET_ss) [complex_rationalTheory.reduce_def] THEN 322 FULL_SIMP_TAC int_ss [GCD_0L,div_id_lem,div_zero_lem, 323 fracTheory.FRAC_DNMPOS] THEN 324 MAP_FIRST MATCH_MP_TAC (map DISCH_ALL (CONJUNCTS (UNDISCH reduce_thm))) THEN 325 RW_TAC int_ss [fracTheory.FRAC_DNMPOS,int_sign_lem] THEN 326 MATCH_MP_TAC (GEN_ALL int_sign_lem) THEN 327 METIS_TAC [fracTheory.FRAC_DNMPOS]); 328 329val num_nz = prove(``0 < a ==> ~(Num a = 0)``, 330 ONCE_REWRITE_TAC [GSYM INT_EQ_CALCULATE] THEN 331 RW_TAC std_ss [snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)), 332 INT_LT_IMP_LE] THEN ARITH_TAC); 333 334val gcd_less_eq = prove(``!a b. 0 < b ==> (gcd a b <= b)``, 335 completeInduct_on `a` THEN 336 ONCE_REWRITE_TAC [gcdTheory.GCD_EFFICIENTLY] THEN 337 RW_TAC arith_ss [] THEN 338 Cases_on `a <= b` THEN FULL_SIMP_TAC arith_ss [NOT_LESS_EQUAL] THENL [ 339 PAT_ASSUM ``!a.P`` (MP_TAC o SPEC ``b MOD a``) THEN 340 RW_TAC arith_ss [DIVISION,DECIDE ``~(a = 0n) ==> 0 < a``] THEN 341 POP_ASSUM (MP_TAC o SPEC ``a:num``) THEN RW_TAC arith_ss [], 342 ONCE_REWRITE_TAC [gcdTheory.GCD_EFFICIENTLY] THEN 343 RW_TAC arith_ss [] THEN 344 `a MOD b < a` by (MATCH_MP_TAC LESS_TRANS THEN 345 Q.EXISTS_TAC `b` THEN RW_TAC arith_ss [DIVISION]) THEN 346 PAT_ASSUM ``!a.P`` (MP_TAC o SPEC ``a MOD b``) THEN 347 RW_TAC arith_ss []]); 348 349val gcd_less_eq_mod = prove(``~(a = 0) /\ ~(b = 0) /\ ~(a MOD b = 0) ==> 350 gcd (a * b) (b ** 2) <= b * a MOD b``, 351 ONCE_REWRITE_TAC [GCD_SYM] THEN 352 ONCE_REWRITE_TAC [gcdTheory.GCD_EFFICIENTLY] THEN RW_TAC arith_ss [] THEN 353 RW_TAC arith_ss [GSYM (SIMP_RULE arith_ss [] 354 (Q.SPECL [`b`,`a`,`b`] MOD_COMMON_FACTOR))] THEN 355 MATCH_MP_TAC (ONCE_REWRITE_RULE [GCD_SYM] gcd_less_eq) THEN 356 METIS_TAC [MULT_EQ_0,DECIDE ``0 < a = ~(a = 0n)``]); 357 358val DIVIDES_MOD = store_thm("DIVIDES_MOD", 359 ``~(a = 0) ==> (divides a b = (b MOD a = 0))``, 360 STRIP_TAC THEN EQ_TAC THEN 361 RW_TAC int_ss [compute_divides] THEN 362 RW_TAC int_ss [ZERO_MOD,MOD_1,DECIDE ``~(a = 0n) ==> 0 < a``]); 363 364val MOD_GCD = store_thm("MOD_GCD", 365 ``~(b = 0) \/ ~(a = 0) ==> (a MOD gcd a b = 0)``, 366 STRIP_TAC THEN `~(gcd a b = 0)` by METIS_TAC [GCD_EQ_0] THEN 367 RW_TAC int_ss [GSYM DIVIDES_MOD] THEN 368 METIS_TAC [GCD_IS_GCD,is_gcd_def]); 369 370val ab_INT_TAC = 371 `0 <= b \/ 0 <= ~b` by ARITH_TAC THEN 372 `0 <= a \/ 0 <= ~a` by ARITH_TAC THEN 373 IMP_RES_TAC int_nat_lem THEN 374 RULE_ASSUM_TAC (CONV_RULE (TRY_CONV 375 (REWR_CONV (ARITH_PROVE ``(~a = b) = (a = ~b:int)``)))); 376 377val a_INT_TAC = 378 `0 <= a \/ 0 <= ~a` by ARITH_TAC THEN 379 IMP_RES_TAC int_nat_lem THEN 380 RULE_ASSUM_TAC (CONV_RULE (TRY_CONV 381 (REWR_CONV (ARITH_PROVE ``(~a = b) = (a = ~b:int)``)))) THEN 382 POP_ASSUM SUBST_ALL_TAC; 383 384 385val reduced_dnm_pos = store_thm("reduced_dnm_pos", 386 ``~(b = 0) ==> 0 < SND (reduce (a * b, b * b))``, 387 STRIP_TAC THEN ab_INT_TAC THEN 388 RW_TAC (int_ss ++ boolSimps.LET_ss) 389 [complex_rationalTheory.reduce_def,INT_ABS_NEG,INT_ABS_NUM, 390 INT_MUL_CALCULATE] THEN 391 `~(a'' * a'' = 0)` by (REWRITE_TAC [MULT_EQ_0] THEN ARITH_TAC) THEN 392 RULE_ASSUM_TAC (CONV_RULE (TRY_CONV (RAND_CONV 393 (LAND_CONV (SIMP_CONV arith_ss []))))) THEN 394 RW_TAC int_ss [int_div,GCD_EQ_0,X_LT_DIV, 395 DECIDE ``~(a = 0n) ==> 0 < a``] THEN 396 METIS_TAC [gcd_less_eq,DECIDE ``~(a = 0n) ==> 0 < a``]); 397 398val nmrdnm_rewrite = store_thm("nmrdnm_rewrite", 399 ``~(b = 0) ==> 400 (numerator (mult (int a) (reciprocal (int b))) = 401 int (FST (reduce(a * b, b * b)))) /\ 402 (denominator (mult (int a) (reciprocal (int b))) = 403 int (SND (reduce(a * b, b * b))))``, 404 STRIP_TAC THEN 405 `0 < b * b /\ 0 < b * b * (b * b)` by 406 (RW_TAC int_ss [INT_MUL_SIGN_CASES] THEN ARITH_TAC) THEN 407 RW_TAC (int_ss ++ boolSimps.LET_ss) 408 [mult_def,reciprocal_def,numerator_def,denominator_def, 409 int_def,cpx_def,sexpTheory.rat_def,complex_rationalTheory.com_0_def, 410 translateTheory.rat_def, 411 ratTheory.rat_0_def,fracTheory.frac_0_def,ratTheory.RAT_EQ_CALCULATE, 412 fracTheory.NMR,fracTheory.DNM, 413 complex_rationalTheory.COMPLEX_RECIPROCAL_def, 414 ratTheory.RAT_MUL_CALCULATE,fracTheory.FRAC_MULT_CALCULATE, 415 ratTheory.RAT_DIV_CALCULATE,fracTheory.FRAC_DIV_CALCULATE, 416 ratTheory.RAT_ADD_CALCULATE,fracTheory.FRAC_ADD_CALCULATE, 417 complex_rationalTheory.COMPLEX_MULT_def,fracTheory.frac_mul_def, 418 ratTheory.RAT_AINV_CALCULATE,fracTheory.FRAC_AINV_CALCULATE, 419 ratTheory.RAT_SUB_CALCULATE,fracTheory.FRAC_SUB_CALCULATE, 420 INT_SGN_SQUARE,INT_ABS_SQUARE,rat_mul_lem, 421 complex_rationalTheory.reduced_nmr_def, 422 complex_rationalTheory.reduced_dnm_def,REDUCE_CONG]); 423 424val NEZEROLT = DECIDE ``~(a = 0) ==> 0n < a``; 425 426val div_gcd_lemma = prove( 427 ``~(b = 0) ==> (int_div (~ & a) (& (gcd a b)) = ~& (a DIV gcd a b))``, 428 RW_TAC int_ss [int_div,GCD_EQ_0,GCD_0L,DECIDE ``~(0 < a) = (a = 0n)``, 429 ZERO_DIV,NEZEROLT] THEN METIS_TAC [MOD_GCD]); 430 431val div_num_lemma = prove( 432 ``~(b = 0) ==> (int_div (~& a) (& b) = 433 if (a MOD b = 0) then ~(& (a DIV b)):int else ~& (a DIV b + 1))``, 434 RW_TAC int_ss [int_div,ZERO_DIV,ZERO_MOD] THEN 435 TRY (METIS_TAC [ZERO_MOD,NEZEROLT]) THEN 436 ARITH_TAC); 437 438val thms = [DIVISION,ADD_0,MOD_GCD,MULT_EQ_0,GCD_SYM, 439 GCD_EQ_0,SIMP_CONV arith_ss [] ``a * a:num``, 440 DECIDE ``0 < a = ~(a = 0n)``, 441 DIV_DIV_DIV_MULT,MULT_DIV]; 442 443val GCD_LEMMAS = prove(``~(a'' = 0) ==> 444 (0 < gcd (a' * a'') (a'' ** 2)) /\ 445 (0 < a'' ** 2 DIV gcd (a' * a'') (a'' ** 2)) /\ 446 (a'' ** 2 DIV gcd (a' * a'') (a'' ** 2) * gcd (a' * a'') (a'' ** 2) = 447 a'' ** 2) /\ 448 (a' * a'' DIV a'' ** 2 = a' DIV a'')``, 449 RW_TAC int_ss thms THEN METIS_TAC thms); 450 451val reduce_divide_lemma = store_thm("reduce_divide_lemma", 452 ``~(b = 0) ==> 453 (int_div a b = int_div (FST (reduce (a * b,b * b))) 454 (SND (reduce (a * b,b * b))))``, 455 STRIP_TAC THEN ab_INT_TAC THEN 456 REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN 457 RW_TAC (int_ss ++ boolSimps.LET_ss) 458 [complex_rationalTheory.reduce_def,INT_ABS_NUM, 459 INT_MUL_CALCULATE,INT_ABS_NEG] THEN 460 FULL_SIMP_TAC int_ss [INT_DIV_CALCULATE] THEN 461 IMP_RES_TAC GCD_LEMMAS THEN 462 REPEAT (PAT_ASSUM ``!a.P`` (ASSUME_TAC o Q.SPEC `a'`)) THEN 463 FULL_SIMP_TAC int_ss [INT_DIV_CALCULATE,DIV_DIV_DIV_MULT, 464 div_gcd_lemma,MULT_EQ_0] THEN 465 RW_TAC int_ss [div_num_lemma,GSYM int_sub,DIV_DIV_DIV_MULT] THEN 466 POP_ASSUM MP_TAC THEN 467 RW_TAC int_ss [DIV_MOD_MOD_DIV, 468 GSYM (SIMP_RULE arith_ss [] (Q.SPECL [`q`,`p`,`q`] MOD_COMMON_FACTOR)), 469 ZERO_DIV,DECIDE ``~(a = 0) = 0n < a``,X_LT_DIV,gcd_less_eq_mod] THEN 470 MATCH_MP_TAC gcd_less_eq_mod THEN ASM_REWRITE_TAC [] THEN 471 CCONTR_TAC THEN FULL_SIMP_TAC int_ss [GCD_0L] THEN METIS_TAC [ZERO_MOD]); 472 473val GCD_MULT = store_thm("GCD_MULT", 474 ``!n a. ~(n = 0) /\ ~(a = 0) ==> (gcd (n * a) a = a)``, 475 Induct THEN RW_TAC int_ss [ADD1,LEFT_ADD_DISTRIB,GCD_ADD_L] THEN 476 Cases_on `n = 0` THEN FULL_SIMP_TAC int_ss [GCD_0L,GCD_0R] THEN 477 METIS_TAC [GCD_SYM]); 478 479val reduce_mod_lemma = prove(``FST (reduce (a * b,b * b)) < 0 /\ ~(b = 0) /\ 480 ~(SND (reduce (a * b, b * b)) = 1) ==> 481 ~(Num (~FST (reduce (a * b, b * b))) MOD 482 Num (SND (reduce (a * b, b* b))) = 0)``, 483 RW_TAC (int_ss ++ boolSimps.LET_ss) [complex_rationalTheory.reduce_def] THEN 484 ab_INT_TAC THEN REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN 485 FULL_SIMP_TAC int_ss [INT_MUL_CALCULATE,INT_ABS_NUM,INT_DIV,GCD_EQ_0, 486 INT_ABS_NEG] THEN 487 REPEAT (POP_ASSUM MP_TAC) THEN 488 RW_TAC int_ss [int_div,GCD_EQ_0,GCD_0L,GCD_0R,ZERO_DIV,NEZEROLT] THEN 489 TRY (METIS_TAC [MOD_GCD,MULT_EQ_0,GCD_SYM]) THEN 490 IMP_RES_TAC GCD_LEMMAS THEN 491 REPEAT (PAT_ASSUM ``!a.P`` (ASSUME_TAC o Q.SPEC `a'`)) THEN 492 RW_TAC int_ss [DIV_MOD_MOD_DIV,GCD_EQ_0,NEZEROLT,X_LT_DIV, 493 DECIDE ``~(a = 0) = 0n < a``,ONCE_REWRITE_RULE [MULT_COMM] 494 (GSYM (SIMP_RULE arith_ss [] 495 (Q.SPECL [`n`,`p`,`n`] MOD_COMMON_FACTOR))),NEZEROLT] THEN 496 MATCH_MP_TAC gcd_less_eq_mod THEN 497 RW_TAC int_ss [GSYM DIVIDES_MOD] THEN 498 CCONTR_TAC THEN FULL_SIMP_TAC int_ss [divides_def] THEN 499 POP_ASSUM SUBST_ALL_TAC THEN 500 Cases_on `q = 0` THEN FULL_SIMP_TAC int_ss [] THEN 501 `gcd (a'' ** 2 * q) (a'' ** 2) = a'' ** 2` by 502 RW_TAC int_ss [ONCE_REWRITE_RULE [MULT_COMM] GCD_MULT] THEN 503 POP_ASSUM SUBST_ALL_TAC THEN 504 FULL_SIMP_TAC int_ss [DIVMOD_ID]); 505 506val div_lem = prove( 507 ``x < 0 /\ 0 < y /\ ~(y = 0) /\ ~(Num ~x MOD Num y = 0) 508 ==> (int_div x y = ~(int_div (~x) y) + ~1)``, 509 RW_TAC int_ss [int_div] THEN ARITH_TAC); 510 511val INT_DIV = store_thm("INT_DIV", 512 ``~(b = 0) ==> (int (int_div a b) = acl2_floor (int a) (int b))``, 513 RW_TAC (int_ss ++ boolSimps.LET_ss) [nmrdnm_rewrite,acl2_floor_def, 514 GSYM INT_THMS,ite_def,TRUTH_REWRITES,acl2_nniq_rewrite, 515 reduce_divide_lemma] THEN 516 RW_TAC int_ss [INT_DIV_1] THEN 517 MAP_EVERY Q.ABBREV_TAC [`A = FST (reduce (a * b, b * b))`, 518 `B = SND (reduce (a * b, b * b))`] THENL 519 (map (fn x => x by (MATCH_MP_TAC NNIQ_EQ_DIV THEN 520 METIS_TAC [reduced_dnm_pos,INT_LE_LT,int_ge, 521 INT_NOT_LE,INT_NEG_GE0]))) 522 [`nniq (~A) B = int_div (~A) B`,`nniq A B = int_div A B`] THEN 523 POP_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC [INT_CONG] THEN 524 MATCH_MP_TAC div_lem THEN 525 METIS_TAC [reduce_mod_lemma,int_ge,INT_NOT_LE,INT_LE_LT, 526 INT_NEG_GE0,reduced_dnm_pos]); 527 528val INT_QUOT_DIV = store_thm("INT_QUOT_DIV", 529 ``!a b. ~(b = 0) ==> 530 (a quot b = 531 if (0 <= a = 0 <= b) then int_div a b else ~(int_div (~a) b))``, 532 REPEAT GEN_TAC THEN ab_INT_TAC THEN REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN 533 RW_TAC int_ss [INT_DIV_CALCULATE,ZERO_DIV,NEZEROLT] THEN 534 RW_TAC arith_ss [ZERO_DIV,NEZEROLT]); 535 536val reduce_pos_lem = prove( 537 ``~(b = 0) /\ ~(a = 0) ==> 538 ((0 <= a = 0 <= b) = FST (reduce (a * b, b * b)) >= 0)``, 539 STRIP_TAC THEN ab_INT_TAC THEN 540 FULL_SIMP_TAC int_ss [] THEN 541 `0 < gcd (a' * a'') (a'' ** 2)` by RW_TAC int_ss [GCD_LEMMAS] THEN 542 RW_TAC (int_ss ++ boolSimps.LET_ss) 543 [complex_rationalTheory.reduce_def,int_ge, 544 INT_ABS_NUM,INT_MUL_CALCULATE,INT_ABS_NEG] THEN 545 REPEAT (POP_ASSUM MP_TAC) THEN 546 RW_TAC int_ss [GCD_0L,GCD_0R,INT_DIV_CALCULATE, 547 DECIDE ``0 < a ==> ~(a = 0n)``] THEN 548 RW_TAC int_ss [int_div,DECIDE ``~(a = 0) = (0n < a)``, 549 X_LT_DIV,gcd_less_eq] THEN 550 METIS_TAC [gcd_less_eq,GCD_SYM,NEZEROLT,MULT_EQ_0,MOD_GCD]); 551 552val reduce_zero_lem = prove(``~(a = 0) ==> (FST (reduce (0,a)) = 0)``, 553 RW_TAC (int_ss ++ boolSimps.LET_ss) 554 [complex_rationalTheory.reduce_def,GCD_0L] THEN 555 MATCH_MP_TAC INT_DIV_0 THEN 556 METIS_TAC [INT_OF_NUM,INT_ABS_POS, 557 ARITH_PROVE ``(& a = 0i) = (a = 0n)``,INT_ABS_EQ0]); 558 559val nniq_zero_lem = prove(``nniq 0 a = 0``, 560 ONCE_REWRITE_TAC [nniq_def] THEN 561 RW_TAC int_ss [] THEN ARITH_TAC); 562 563val reduce_neg_lemma = prove(``~(b = 0) ==> 564 (FST (reduce (~a * b, b * b)) = ~FST (reduce (a * b, b* b))) /\ 565 (SND (reduce (~a * b, b * b)) = SND (reduce (a * b, b* b)))``, 566 FULL_SIMP_TAC (int_ss ++ boolSimps.LET_ss) 567 [complex_rationalTheory.reduce_def,INT_ABS_SQUARE, 568 INT_MUL_CALCULATE,INT_ABS_NEG] THEN 569 ab_INT_TAC THEN REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN 570 FULL_SIMP_TAC int_ss [INT_MUL_CALCULATE,INT_ABS_NUM,INT_ABS_NEG,GCD_0L, 571 integerTheory.INT_DIV,GCD_EQ_0,MULT_EQ_0,NEZEROLT] THEN 572 RW_TAC int_ss [int_div,GCD_EQ_0,MULT_EQ_0,NEZEROLT,GCD_0L,ZERO_DIV] THEN 573 METIS_TAC [MOD_GCD,GCD_SYM,MULT_EQ_0,NEZEROLT]); 574 575val INT_QUOT = store_thm("INT_QUOT", 576 ``~(b = 0) ==> (int (a quot b) = acl2_truncate (int a) (int b))``, 577 Cases_on `a = 0` THEN 578 RW_TAC (int_ss ++ boolSimps.LET_ss) [ 579 INT_QUOT_0,nmrdnm_rewrite,acl2_truncate_def, 580 GSYM INT_THMS,ite_def,TRUTH_REWRITES,acl2_nniq_rewrite, 581 INT_QUOT_DIV,reduce_zero_lem,nniq_zero_lem, 582 reduce_divide_lemma,reduce_neg_lemma] THEN 583 RW_TAC int_ss [INT_DIV_1] THEN 584 TRY (METIS_TAC [reduce_pos_lem]) THEN 585 MAP_EVERY Q.ABBREV_TAC [`A = FST (reduce (a * b, b * b))`, 586 `B = SND (reduce (a * b, b * b))`] THENL 587 (map (fn x => x by (MATCH_MP_TAC NNIQ_EQ_DIV THEN 588 METIS_TAC [reduced_dnm_pos,INT_LE_LT,int_ge, 589 INT_NOT_LE,INT_NEG_GE0]))) 590 [`nniq A B = int_div A B`,`nniq (~A) B = int_div (~A) B`] THEN 591 POP_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC [INT_CONG] THEN 592 MATCH_MP_TAC div_lem THEN 593 METIS_TAC [reduce_mod_lemma,int_ge,INT_NOT_LE,INT_LE_LT, 594 INT_NEG_GE0,reduced_dnm_pos]); 595 596 597val acl2_mod_def = sexp.acl2Define "ACL2::MOD" 598 `acl2_mod x y = add x (unary_minus (mult (acl2_floor x y) y))`; 599 600val acl2_rem_def = sexp.acl2Define "ACL2::REM" 601 `acl2_rem x y = add x (unary_minus (mult (acl2_truncate x y) y))`; 602 603val INT_MOD = store_thm("INT_MOD", 604 ``~(b = 0i) ==> (int (a % b) = acl2_mod (int a) (int b))``, 605 RW_TAC int_ss [acl2_mod_def,GSYM INT_DIV,GSYM INT_THMS,int_mod,int_sub]); 606 607val INT_REM = store_thm("INT_REM", 608 ``~(b = 0i) ==> (int (a rem b) = acl2_rem (int a) (int b))``, 609 RW_TAC int_ss [acl2_rem_def,GSYM INT_QUOT,GSYM INT_THMS,int_rem,int_sub]); 610 611(*****************************************************************************) 612(* Natural number division and modulus *) 613(*****************************************************************************) 614 615val NAT_DIV = store_thm("NAT_DIV", 616 ``~(b = 0) ==> (nat (a DIV b) = acl2_floor (nat a) (nat b))``, 617 RW_TAC int_ss [nat_def,GSYM INT_DIV]); 618 619val NAT_MOD = store_thm("NAT_MOD", 620 ``~(b = 0) ==> (nat (a MOD b) = acl2_mod (nat a) (nat b))``, 621 RW_TAC int_ss [nat_def,GSYM INT_MOD]); 622 623(*****************************************************************************) 624(* The following proofs are legacy proofs, used in other theories, but no *) 625(* longer required here. *) 626(*****************************************************************************) 627 628open fracTheory ratTheory intExtensionTheory complex_rationalTheory; 629 630val rat_of_int_def = Define 631 `rat_of_int x = 632 if 0 <= x then & (Num (ABS x)) 633 else rat_ainv (& (Num (ABS x)))`; 634 635val rat_of_int_neg = store_thm("rat_of_int_neg", 636 ``rat_of_int ~x = ~rat_of_int x``, 637 RW_TAC std_ss [rat_of_int_def] THEN TRY (`x = 0` by ARITH_TAC) THEN 638 RW_TAC int_ss [RAT_AINV_0,RAT_AINV_AINV,INT_ABS_NEG]); 639 640val sexp_int_rat = prove(``int a = rat (rat_of_int a)``, 641 RW_TAC int_ss [int_def,translateTheory.rat_def,rat_of_int_def,cpx_def, 642 sexpTheory.rat_def, 643 rat_0_def,frac_0_def,RAT_OF_NUM_CALCULATE, 644 RAT_AINV_CALCULATE,FRAC_AINV_CALCULATE,ratTheory.RAT_EQ,NMR,DNM, 645 INT_ABS_POS,snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM))] THEN 646 ARITH_TAC); 647 648val rat_of_int_div_pos1 = prove( 649 ``0 < b /\ 0 <= a ==> 650 (rat_div (rat_of_int a) (rat_of_int b) = abs_rat (abs_frac (a,b)))``, 651 RW_TAC std_ss [rat_of_int_def,INT_LE_LT] THEN 652 RW_TAC int_ss [INT_ABS_CALCULATE_POS,INT_ABS_CALCULATE_0, 653 RAT_OF_NUM_CALCULATE,snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM))] THEN 654 `~(frac_nmr (abs_frac (b,1)) = 0)` by RW_TAC int_ss [NMR,INT_LT_IMP_NE] THEN 655 RW_TAC int_ss [RAT_DIV_CALCULATE,FRAC_DIV_CALCULATE,INT_LT_IMP_NE, 656 INT_ABS_CALCULATE_POS,SGN_def] THEN 657 CCONTR_TAC THEN POP_ASSUM (K ALL_TAC) THEN ARITH_TAC); 658 659val rat_of_int_div_pos = store_thm("rat_of_int_div_pos", 660 ``0 < b ==> (rat_div (rat_of_int a) (rat_of_int b) = 661 abs_rat (abs_frac (a,b)))``, 662 Cases_on `0 <= a` THEN RW_TAC std_ss [rat_of_int_div_pos1] THEN 663 `?c. (a = ~c) /\ 0 <= c` by 664 (Q.EXISTS_TAC `~a` THEN RW_TAC int_ss [] THEN ARITH_TAC) THEN 665 RW_TAC int_ss [rat_of_int_neg,GSYM FRAC_AINV_CALCULATE,GSYM RAT_AINV_LMUL, 666 GSYM RAT_AINV_CALCULATE,RAT_EQ_AINV,RAT_DIV_MULMINV] THEN 667 RW_TAC int_ss [GSYM RAT_DIV_MULMINV,rat_of_int_div_pos1]); 668 669val rat_of_int_nz = prove(``~(b = 0) ==> ~(rat_of_int b = 0)``, 670 RW_TAC int_ss [rat_of_int_def,INT_ABS_POS,NMR,DNM,RAT_AINV_CALCULATE, 671 snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)),ratTheory.RAT_EQ, 672 RAT_OF_NUM_CALCULATE,FRAC_AINV_CALCULATE] THEN 673 ARITH_TAC); 674 675val rat_of_int_div_neg = store_thm("rat_of_int_div_neg", 676 ``b < 0 ==> (rat_div (rat_of_int a) (rat_of_int b) = 677 abs_rat (abs_frac (~a,~b)))``, 678 DISCH_TAC THEN 679 `?c. (b = ~c) /\ 0 < c` by 680 (Q.EXISTS_TAC `~b` THEN RW_TAC int_ss [] THEN ARITH_TAC) THEN 681 RW_TAC int_ss [rat_of_int_neg,RAT_DIV_MULMINV,GSYM RAT_AINV_RMUL, 682 GSYM RAT_AINV_MINV,rat_of_int_nz,INT_LT_IMP_NE, 683 GSYM FRAC_AINV_CALCULATE,GSYM RAT_AINV_CALCULATE,RAT_EQ_AINV] THEN 684 RW_TAC std_ss [GSYM RAT_DIV_MULMINV,rat_of_int_div_pos]); 685 686val int_sign_clauses_pos = 687 prove(``!b. 0i < b ==> !a. (0 < a * b = 0 < a) /\ (!a. a * b < 0 = a < 0)``, 688 REWRITE_TAC [INT_MUL_SIGN_CASES] THEN ARITH_TAC); 689 690val int_sign_clauses_neg = 691 prove(``!b. b < 0i ==> 692 !a. (0 < a * ~b = 0 < a) /\ (!a. a * ~b < 0 = a < 0)``, 693 REWRITE_TAC [INT_MUL_SIGN_CASES,ARITH_PROVE ``b < 0 = 0i < ~b``] THEN 694 ARITH_TAC); 695 696val neg_reduce_rat = store_thm("neg_reduce_rat", 697 ``b < 0 ==> (reduce (rep_frac (rep_rat 698 (rat_div (rat_of_int a) (rat_of_int b)))) = 699 reduce (~a,~b))``, 700 RW_TAC int_ss [rat_of_int_div_neg,rat_of_int_div_pos] THEN 701 RAT_CONG_TAC THEN 702 POP_ASSUM MP_TAC THEN 703 RW_TAC int_ss [NMR,DNM,snd(EQ_IMP_RULE(SPEC_ALL INT_NEG_GT0))] THEN 704 (SUBGOAL_THEN ``rep_frac x = (frac_nmr x,frac_dnm x)`` SUBST_ALL_TAC THEN1 705 RW_TAC std_ss [frac_nmr_def,frac_dnm_def]) THEN 706 `(0 < frac_nmr x /\ a < 0) \/ (frac_nmr x < 0 /\ 0 < a) \/ 707 ((frac_nmr x = 0) /\ (a = 0))` by 708 (`(0 < ~a * frac_dnm x /\ 0 < frac_nmr x * ~b) \/ 709 ((~a * frac_dnm x = 0) /\ (frac_nmr x * ~b = 0)) \/ 710 (~a * frac_dnm x < 0 /\ frac_nmr x * ~b < 0)` by ARITH_TAC THEN 711 ASSUME_TAC (SPEC ``x:frac`` FRAC_DNMPOS) THEN 712 RULE_ASSUM_TAC (REWRITE_RULE (map UNDISCH 713 [SPEC ``b:int`` int_sign_clauses_neg, 714 SPEC ``frac_dnm x`` int_sign_clauses_pos])) THEN 715 FULL_SIMP_TAC int_ss [] THEN ARITH_TAC) THEN 716 RW_TAC (int_ss ++ boolSimps.LET_ss) [reduce_def] THEN 717 RW_TAC int_ss [INT_DIV_0,num_abs_nz,INT_NEG_GT0, 718 GCD_0L,GCD_0R,FRAC_DNMPOS] THEN 719 FIRST [MATCH_MP_TAC (DISCH_ALL (CONJUNCT1 720 (UNDISCH_ALL (SPEC_ALL reduce_thm)))), 721 MATCH_MP_TAC (DISCH_ALL (CONJUNCT2 722 (UNDISCH_ALL (SPEC_ALL reduce_thm)))),ALL_TAC] THEN 723 RW_TAC int_ss [FRAC_DNMPOS,INT_NEG_GT0,INT_ABS_CALCULATE_POS,INT_LT_IMP_LE, 724 snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)),INT_LT_IMP_NE,INT_DIV_ID]); 725 726val pos_reduce_rat = store_thm("pos_reduce_rat", 727 ``0 < b ==> (reduce (rep_frac (rep_rat 728 (rat_div (rat_of_int a) (rat_of_int b)))) = 729 reduce (a,b))``, 730 RW_TAC int_ss [rat_of_int_div_pos] THEN 731 RAT_CONG_TAC THEN 732 POP_ASSUM MP_TAC THEN 733 RW_TAC int_ss [NMR,DNM,snd(EQ_IMP_RULE(SPEC_ALL INT_NEG_GT0))] THEN 734 (SUBGOAL_THEN ``rep_frac x = (frac_nmr x,frac_dnm x)`` SUBST_ALL_TAC THEN1 735 RW_TAC std_ss [frac_nmr_def,frac_dnm_def]) THEN 736 `(0 < frac_nmr x /\ 0 < a) \/ (frac_nmr x < 0 /\ a < 0) \/ 737 ((frac_nmr x = 0) /\ (a = 0))` by 738 (`(0 < a * frac_dnm x /\ 0 < frac_nmr x * b) \/ 739 ((a * frac_dnm x = 0) /\ (frac_nmr x * b = 0)) \/ 740 (a * frac_dnm x < 0 /\ frac_nmr x * b < 0)` by ARITH_TAC THEN 741 ASSUME_TAC (SPEC ``x:frac`` FRAC_DNMPOS) THEN 742 RULE_ASSUM_TAC (REWRITE_RULE (map UNDISCH 743 [SPEC ``b:int`` int_sign_clauses_pos, 744 SPEC ``frac_dnm x`` int_sign_clauses_pos])) THEN 745 FULL_SIMP_TAC int_ss [] THEN ARITH_TAC) THEN 746 RW_TAC (int_ss ++ boolSimps.LET_ss) [reduce_def] THEN 747 RW_TAC int_ss [INT_DIV_0,num_abs_nz,INT_NEG_GT0, 748 GCD_0L,GCD_0R,FRAC_DNMPOS] THEN 749 FIRST [MATCH_MP_TAC (DISCH_ALL (CONJUNCT1 750 (UNDISCH_ALL (SPEC_ALL reduce_thm)))), 751 MATCH_MP_TAC (DISCH_ALL (CONJUNCT2 752 (UNDISCH_ALL (SPEC_ALL reduce_thm)))),ALL_TAC] THEN 753 RW_TAC int_ss [FRAC_DNMPOS,INT_ABS_CALCULATE_POS,INT_DIV_ID,INT_LT_IMP_LE, 754 snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)),INT_LT_IMP_NE,INT_NEG_GT0]); 755 756val mod_common = store_thm("mod_common", 757 ``0 < b /\ 0 < c ==> ((a MOD b = 0) = ((a * c) MOD (b * c) = 0))``, 758 REPEAT STRIP_TAC THEN EQ_TAC THEN 759 RW_TAC arith_ss [CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV MULT_COMM)) 760 (GSYM MOD_COMMON_FACTOR)]); 761 762val int_div_common = store_thm("int_div_common", 763 ``~(b = 0) /\ ~(c = 0i) ==> (int_div (a * & b) (c * & b) = int_div a c)``, 764 REPEAT STRIP_TAC THEN 765 `(a < 0 \/ (a = 0) \/ 0 < a) /\ (c < 0 \/ 0 < c)` by ARITH_TAC THEN 766 EVERY_ASSUM (fn th => (SUBST_ALL_TAC o MATCH_MP r1) th THEN 767 ASSUME_TAC th handle _ => ALL_TAC) THEN 768 EVERY_ASSUM (fn th => (SUBST_ALL_TAC o MATCH_MP r2) th THEN 769 ASSUME_TAC th handle _ => ALL_TAC) THEN 770 FULL_SIMP_TAC std_ss [INT_NEG_LT0,GSYM INT_NEG_GT0, 771 INT_LT_CALCULATE,GSYM INT_NEG_LMUL,GSYM INT_NEG_RMUL, 772 DECIDE ``0 < a = ~(a = 0n)``,INT_ABS_NEG,NUM_OF_INT, 773 INT_ABS_NUM,INT_NEG_MUL2,INT_MUL, 774 INT_EQ_CALCULATE,INT_DIV_NEG,INT_NEGNEG,integerTheory.INT_DIV, 775 ZERO_DIV,INT_DIV_0,INT_NEG_0] THEN 776 RW_TAC int_ss [int_div] THEN 777 FULL_SIMP_TAC arith_ss [GSYM DIV_DIV_DIV_MULT, 778 DECIDE ``~(0 < a) = (a = 0n)``,ZERO_DIV, 779 ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV] THEN 780 CCONTR_TAC THEN POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN 781 REWRITE_TAC [] THEN POP_ASSUM MP_TAC THEN 782 MAP_FIRST MATCH_MP_TAC [DECIDE ``(a = b) ==> (~a ==> ~b)``, 783 DECIDE ``(a = b) ==> (a ==> b)``] THEN 784 MATCH_MP_TAC (GSYM (ONCE_REWRITE_RULE [MULT_COMM] mod_common)) THEN 785 DECIDE_TAC); 786 787 788val mod_zero_mult = store_thm("mod_zero_mult", 789 ``0 < b ==> ((a MOD b = 0) = (b = 1) \/ (?c. a = b * c))``, 790 REPEAT STRIP_TAC THEN EQ_TAC THEN 791 Cases_on `b = 1n` THEN RW_TAC arith_ss [] THENL [ 792 ASSUM_LIST (fn list => SUBST_ALL_TAC (SIMP_RULE arith_ss list 793 (DISCH_ALL (CONJUNCT1 (SPEC ``a:num`` (UNDISCH 794 (SPEC ``b:num`` DIVISION))))))) THEN 795 Q.EXISTS_TAC `a DIV b` THEN REFL_TAC, 796 ONCE_REWRITE_TAC [MULT_COMM] THEN MATCH_MP_TAC MOD_EQ_0 THEN 797 FIRST_ASSUM ACCEPT_TAC]); 798 799val gcd_mod = store_thm("gcd_mod", 800 ``~(p = q) /\ 1 < q /\ ~(p = 0) /\ ~(q = 0) /\ (gcd p q = 1) ==> 801 ~(p MOD q = 0)``, 802 RW_TAC arith_ss [mod_zero_mult] THEN 803 CCONTR_TAC THEN FULL_SIMP_TAC arith_ss [] THEN POP_ASSUM SUBST_ALL_TAC THEN 804 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [ONCE_REWRITE_RULE [GCD_SYM] 805 GCD_EFFICIENTLY]) THEN 806 POP_ASSUM MP_TAC THEN RW_TAC arith_ss [MOD_EQ_0,GCD_0R]); 807 808(****************************************************************************) 809(* SGN : int -> int using acl2 function SIGNUM *) 810(****************************************************************************) 811 812val acl2_zerop_def = sexp.acl2Define "COMMON-LISP::ZEROP" 813 `acl2_zerop x = equal x (int 0)`; 814 815val _ = overload_on("acl2_zerop", 816 fst (strip_comb (lhs (snd (strip_forall (concl acl2_zerop_def)))))); 817 818val acl2_minusp_def = sexp.acl2Define "COMMON-LISP::MINUSP" 819 `acl2_minusp x = less x (int 0)`; 820 821val _ = overload_on("acl2_minusp", 822 fst (strip_comb (lhs (snd (strip_forall (concl acl2_minusp_def)))))); 823 824val acl2_signum_def = sexp.acl2Define "ACL2::SIGNUM" 825 `acl2_signum x = ite (equal x (int 0)) (int 0) 826 (ite (less x (int 0)) (int ~1) (int 1))`; 827 828val INT_SGN = store_thm("INT_SGN",``int (SGN x) = acl2_signum (int x)``, 829 RW_TAC int_ss [ite_def,GSYM INT_THMS,SGN_def,acl2_signum_def, 830 TRUTH_REWRITES,bool_def,INT_CONG] THEN 831 ARITH_TAC); 832 833(*****************************************************************************) 834(* even and odd for natural numbers using acl2 functions evenp and oddp *) 835(*****************************************************************************) 836 837val acl2_evenp_def = sexp.acl2Define "ACL2::EVENP" 838 `acl2_evenp x = integerp (mult x (reciprocal (int 2)))`; 839 840val acl2_oddp_def = sexp.acl2Define "ACL2::ODDP" 841 `acl2_oddp x = not (acl2_evenp x)`; 842 843val nat_rat = prove(``!a. nat a = rat (& a)``, 844 RW_TAC std_ss [nat_def,int_def,translateTheory.rat_def,cpx_def, 845 sexpTheory.rat_def,rat_0_def,frac_0_def,rat_0,RAT_OF_NUM_CALCULATE]); 846 847val int_rat_n = prove(``!a. int (& a) = rat (& a)``, 848 RW_TAC std_ss [nat_rat,GSYM nat_def]); 849 850val rat_2_nz = prove(``~(0 = 2:rat)``, 851 RW_TAC int_ss [RAT_EQ_CALCULATE,RAT_OF_NUM_CALCULATE,NMR,DNM]); 852 853val NAT_EVEN = prove(``bool (EVEN a) = acl2_evenp (nat a)``, 854 Cases_on `EVEN a` THEN ASM_REWRITE_TAC [] THEN 855 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [GSYM ODD_EVEN]) THEN 856 IMP_RES_TAC EVEN_ODD_EXISTS THEN 857 RW_TAC int_ss [GSYM nat_def,acl2_evenp_def,nat_rat, 858 GSYM RAT_DIV,rat_2_nz] THEN 859 RW_TAC int_ss [translateTheory.rat_def,integerp_def, 860 IS_INT_EXISTS,bool_def,TRUTH_REWRITES] THEN 861 POP_ASSUM MP_TAC THEN RW_TAC int_ss [RAT_LDIV_EQ,rat_2_nz] THENL [ 862 Q.EXISTS_TAC `& m`, 863 `0 <= c \/ 0 <= ~c` by ARITH_TAC THEN IMP_RES_TAC int_nat_lem THEN 864 RULE_ASSUM_TAC (CONV_RULE (TRY_CONV 865 (REWR_CONV (ARITH_PROVE ``(~a = b) = (a = ~b:int)``)))) THEN 866 POP_ASSUM SUBST_ALL_TAC] THEN 867 RW_TAC int_ss [GSYM FRAC_AINV_CALCULATE,GSYM RAT_AINV_CALCULATE, 868 GSYM RAT_OF_NUM_CALCULATE,RAT_MUL_NUM_CALCULATE, 869 RAT_EQ_NUM_CALCULATE] THEN 870 ARITH_TAC); 871 872val NAT_ODD = prove(``bool (ODD a) = acl2_oddp (nat a)``, 873 RW_TAC std_ss [acl2_oddp_def,GSYM NAT_EVEN,bool_def,TRUTH_REWRITES,not_def, 874 ite_def,EVEN_ODD]); 875 876val int_mul_lem = prove(``(?c. i * 8 = c * 16) = ~(i % 2 = 1)``, 877 `!c. (i * 8 = c * 16) = (i = c * 2)` by ARITH_TAC THEN 878 ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN 879 EQ_TAC THEN STRIP_TAC THENL [ 880 ALL_TAC, 881 Q.EXISTS_TAC `int_div i 2`] THEN 882 FULL_SIMP_TAC int_ss [] THEN 883 ARITH_TAC); 884 885 886val EVENP_INTMOD = store_thm("EVENP_INTMOD", 887 ``(|= acl2_evenp (int i)) = ~(i % 2 = 1)``, 888 RW_TAC int_ss [acl2_evenp_def,reciprocal_def,int_def,sexpTheory.cpx_def, 889 mult_def,complex_rationalTheory.com_0_def,sexpTheory.rat_def, 890 ratTheory.rat_0_def,fracTheory.frac_0_def,ratTheory.RAT_EQ_CALCULATE, 891 fracTheory.NMR,fracTheory.DNM, 892 complex_rationalTheory.COMPLEX_RECIPROCAL_def, 893 complex_rationalTheory.COMPLEX_MULT_def,ratTheory.RAT_DIV_CALCULATE, 894 ratTheory.RAT_MUL_CALCULATE,fracTheory.frac_mul_def, 895 ratTheory.RAT_ADD_CALCULATE,fracTheory.frac_add_def, 896 fracTheory.frac_div_def,fracTheory.frac_minv_def, 897 fracTheory.frac_sgn_def,RAT_AINV_CALCULATE,fracTheory.frac_ainv_def, 898 RAT_SUB_CALCULATE,fracTheory.frac_sub_def,EVAL ``SGN 4``] THEN 899 RW_TAC int_ss [integerp_def,TRUTH_REWRITES,IS_INT_EXISTS, 900 ratTheory.rat_0_def,fracTheory.frac_0_def,ratTheory.RAT_EQ_CALCULATE, 901 fracTheory.NMR,fracTheory.DNM,GSYM INT_MUL_ASSOC,int_mul_lem]); 902 903(*****************************************************************************) 904(* Arithmetic shift left for int and num using acl2 function ASH *) 905(*****************************************************************************) 906 907val acl2_ash_def = sexp.acl2Define "ACL2::ASH" 908 `acl2_ash i c = acl2_floor (mult (ifix i) (acl2_expt (int 2) c)) (int 1)`; 909 910val INT_ASH = store_thm("INT_ASH", 911 ``int (i * 2 ** c) = acl2_ash (int i) (nat c)``, 912 RW_TAC int_ss [acl2_ash_def,GSYM INT_EXPT,ifix_def,nat_def, 913 INTEGERP_INT,ite_def,TRUTH_REWRITES,GSYM INT_THMS,GSYM INT_DIV]); 914 915val NAT_ASH = store_thm("NAT_ASH", 916 ``nat (i * 2 ** c) = acl2_ash (nat i) (nat c)``, 917 RW_TAC std_ss [nat_def,GSYM INT_EXP,GSYM integerTheory.INT_MUL,INT_ASH]); 918 919(*****************************************************************************) 920(* Maximum and minimum theories for int and num, *) 921(* using acl2 functions max and min *) 922(*****************************************************************************) 923 924val acl2_max_def = 925 sexp.acl2Define "ACL2::MAX" `acl2_max x y = ite (less y x) x y`; 926val acl2_min_def = 927 sexp.acl2Define "ACL2::MIN" `acl2_min x y = ite (less x y) x y`; 928 929val NAT_MAX = store_thm("NAT_MAX", 930 ``nat (MAX x y) = acl2_max (nat x) (nat y)``, 931 RW_TAC int_ss [MAX_DEF,acl2_max_def,ite_def,TRUTH_REWRITES,NAT_CONG] THEN 932 FULL_SIMP_TAC int_ss [GSYM NAT_THMS,TRUTH_REWRITES]); 933 934val NAT_MIN = store_thm("NAT_MIN", 935 ``nat (MIN x y) = acl2_min (nat x) (nat y)``, 936 RW_TAC int_ss [MIN_DEF,acl2_min_def,ite_def,TRUTH_REWRITES,NAT_CONG] THEN 937 FULL_SIMP_TAC int_ss [GSYM NAT_THMS,TRUTH_REWRITES]); 938 939val INT_MAX = store_thm("INT_MAX", 940 ``int (int_max x y) = acl2_max (int x) (int y)``, 941 RW_TAC int_ss [acl2_max_def,INT_MAX,GSYM INT_THMS,ite_def, 942 TRUTH_REWRITES,INT_CONG] THEN ARITH_TAC); 943 944val INT_MIN = store_thm("INT_MIN", 945 ``int (int_min x y) = acl2_min (int x) (int y)``, 946 RW_TAC int_ss [acl2_min_def,INT_MIN,GSYM INT_THMS,ite_def, 947 TRUTH_REWRITES,INT_CONG] THEN ARITH_TAC); 948 949(*****************************************************************************) 950(* ABS:int -> int, using acl2 function ABS *) 951(*****************************************************************************) 952 953val acl2_abs_def = 954 sexp.acl2Define "ACL2::ABS" 955 `acl2_abs x = ite (less x (int 0)) (unary_minus x) x`; 956 957val INT_ABS = store_thm("INT_ABS", 958 ``int (ABS x) = acl2_abs (int x)``, 959 RW_TAC int_ss [INT_ABS,acl2_abs_def,GSYM INT_THMS,ite_def, 960 TRUTH_REWRITES,INT_CONG] THEN ARITH_TAC); 961 962(*****************************************************************************) 963(* List theorems: *) 964(* *) 965(* acl2 functions: binary-append, revappend, reverse, take, nthcdr, butlast, *) 966(* nth, last, strip_cars, strip_cdrs, pairlis$ *) 967(* *) 968(*****************************************************************************) 969 970open listTheory; 971 972val CAR_NIL = store_thm("CAR_NIL",``car nil = nil``, 973 RW_TAC int_ss [car_def,nil_def]); 974 975val CDR_NIL = store_thm("CDR_NIL",``cdr nil = nil``, 976 RW_TAC int_ss [cdr_def,nil_def]); 977 978val CONSP_NIL = store_thm("CONSP_NIL",``consp nil = nil``, 979 RW_TAC int_ss [consp_def,nil_def]); 980 981val (acl2_append_def,acl2_append_ind) = 982 sexp.acl2_defn "ACL2::BINARY-APPEND" 983 (`acl2_append x y = 984 ite (consp x) (cons (car x) (acl2_append (cdr x) y)) y`, 985 WF_REL_TAC `measure (sexp_size o FST)` THEN 986 Cases THEN RW_TAC arith_ss [cdr_def,nil_def,consp_def,sexp_size_def]); 987 988val _ = overload_on("acl2_append", 989 fst (strip_comb (lhs (snd (strip_forall (concl acl2_append_def)))))); 990 991val APPEND_NIL = store_thm("APPEND_NIL", 992 ``!x. acl2_append nil x = x``, 993 Cases THEN ONCE_REWRITE_TAC [acl2_append_def] THEN 994 RW_TAC int_ss [ite_def,endp_def,atom_def,TRUTH_REWRITES, 995 not_def]); 996 997val LIST_APPEND = store_thm("LIST_APPEND", 998 ``!x y f. list f (x ++ y) = acl2_append (list f x) (list f y)``, 999 completeInduct_on `LENGTH x + LENGTH y` THEN Cases THEN 1000 ONCE_REWRITE_TAC [acl2_append_def] THEN 1001 REWRITE_TAC [list_def,APPEND,LENGTH, 1002 APPEND_NIL,CAR_NIL,CDR_NIL,CONSP_NIL,consp_def,ite_def, 1003 TRUTH_REWRITES,car_def,cdr_def,sexp_11] THEN 1004 FIX_CI_TAC THEN RW_TAC int_ss [] THEN FIRST_ASSUM MATCH_MP_TAC THEN 1005 CCONTR_TAC THEN FULL_SIMP_TAC int_ss [ADD_CLAUSES] THEN 1006 PROVE_TAC [prim_recTheory.LESS_SUC_REFL]); 1007 1008val (acl2_revappend_def,acl2_revappend_ind) = 1009 (PURE_REWRITE_RULE [GSYM ite_def] ## I) 1010 (sexp.acl2_defn "ACL2::REVAPPEND" 1011 (`acl2_revappend x y = 1012 if (consp x = nil) then y 1013 else acl2_revappend (cdr x) (cons (car x) y)`, 1014 WF_REL_TAC `measure (sexp_size o FST)` THEN 1015 Cases THEN RW_TAC arith_ss [cdr_def,nil_def,consp_def,sexp_size_def])); 1016 1017val REVAPPEND_NIL = store_thm("REVAPPEND_NIL", 1018 ``!x. acl2_revappend nil x = x``, 1019 Cases THEN ONCE_REWRITE_TAC [acl2_revappend_def] THEN 1020 RW_TAC int_ss [ite_def,endp_def,atom_def,TRUTH_REWRITES, 1021 not_def]); 1022 1023val LIST_REV = store_thm("LIST_REV", 1024 ``!x y f. list f (REV x y) = acl2_revappend (list f x) (list f y)``, 1025 Induct THEN ONCE_REWRITE_TAC [acl2_revappend_def] THEN 1026 RW_TAC int_ss [list_def,REV_DEF,consp_def,car_def,cdr_def,CONSP_NIL, 1027 CAR_NIL,CDR_NIL,REVAPPEND_NIL,ite_def,TRUTH_REWRITES]); 1028 1029val acl2_reverse_def = 1030 sexp.acl2Define "COMMON-LISP::REVERSE" `acl2_reverse x = 1031 ite (stringp x) 1032 (coerce (acl2_revappend (coerce x (csym "LIST")) nil) (csym "STRING")) 1033 (acl2_revappend x nil)`; 1034 1035val _ = overload_on ("acl2_reverse", 1036 fst (strip_comb (lhs (snd (strip_forall (concl acl2_reverse_def)))))); 1037 1038val LIST_REVERSE = store_thm("LIST_REVERSE", 1039 ``!l. list f (REVERSE l) = acl2_reverse (list f l)``, 1040 RW_TAC int_ss [REVERSE_REV,LIST_REV,acl2_reverse_def,list_def,ite_def] THEN 1041 Cases_on `l` THEN FULL_SIMP_TAC int_ss [stringp_def,list_def,nil_def]); 1042 1043val ZP_RECURSE_LEMMA = store_thm("ZP_RECURSE_LEMMA", 1044 ``!i. (zp i = nil) ==> 1045 sexp_to_nat (add (unary_minus (nat 1)) i) < sexp_to_nat i``, 1046 RW_TAC int_ss [zp_def,ite_def,TRUTH_REWRITES,GSYM int_def] THEN 1047 CHOOSEP_TAC THEN 1048 FULL_SIMP_TAC int_ss [GSYM INT_THMS,nat_def,TRUTH_REWRITES] THEN 1049 FULL_SIMP_TAC int_ss [int_ge,INT_NOT_LE] THEN 1050 `?i. (i' = &i) /\ 0 < i` by 1051 METIS_TAC [INT_OF_NUM,integerTheory.INT_LT,INT_LT_IMP_LE] THEN 1052 RW_TAC int_ss [INT_SUB_CALCULATE,INT_ADD_CALCULATE,GSYM nat_def, 1053 SEXP_TO_NAT_OF_NAT]); 1054 1055val (acl2_firstnac_def,firstnac_ind) = 1056 sexp.acl2_defn "ACL2::FIRST-N-AC" 1057 (`acl2_firstnac i l ac = 1058 ite (zp i) 1059 (acl2_reverse ac) 1060 (acl2_firstnac (add (unary_minus (nat 1)) i) 1061 (cdr l) (cons (car l) ac))`, 1062 WF_REL_TAC `measure (sexp_to_nat o FST)` THEN 1063 METIS_TAC [ZP_RECURSE_LEMMA]); 1064 1065val _ = overload_on ("acl2_firstnac", 1066 fst (strip_comb (lhs (snd (strip_forall (concl acl2_firstnac_def)))))); 1067 1068val acl2_take_def = 1069 sexp.acl2Define "ACL2::TAKE" `acl2_take n l = acl2_firstnac n l nil`; 1070 1071val _ = overload_on ("acl2_take", 1072 fst (strip_comb (lhs (snd (strip_forall (concl acl2_take_def)))))); 1073 1074val REVERSE_NIL = store_thm("REVERSE_NIL", 1075 ``acl2_reverse nil = nil``, 1076 RW_TAC int_ss [acl2_reverse_def,REVAPPEND_NIL,ite_def, 1077 REWRITE_CONV [nil_def] ``stringp nil``,TRUTH_REWRITES,stringp_def]); 1078 1079fun mk_rev x = 1080 GSYM (SIMP_RULE std_ss [list_def] (Q.SPECL [x,`[]`,`I`] 1081 (INST_TYPE [alpha |-> ``:sexp``] LIST_REV))); 1082 1083fun mk_list x = GSYM (SIMP_CONV std_ss [list_def] ``list f ^(x)``); 1084 1085val FIRST_NAC_LEMMA = store_thm("FIRST_NAC_LEMMA", 1086 ``!b a f h x. a <= LENGTH b ==> ( 1087 cons (f h) (acl2_firstnac (nat a) (list f b) (list f x)) = 1088 acl2_firstnac (nat a) (list f b) (list f (x ++ [h])))``, 1089 Induct THEN (Cases ORELSE (GEN_TAC THEN Cases)) THEN 1090 ONCE_REWRITE_TAC [acl2_firstnac_def] THEN 1091 RW_TAC int_ss [GSYM NAT_EQUAL_0,TRUTH_REWRITES,ite_def,GSYM LIST_REVERSE, 1092 REVERSE_APPEND,REVERSE_DEF,APPEND,list_def,car_def,cdr_def,LENGTH, 1093 nat_def,GSYM INT_THMS,INT_ADD_CALCULATE] THEN 1094 RW_TAC int_ss [GSYM nat_def,mk_list ``a::b``,APPEND]); 1095 1096val LIST_FIRSTN = store_thm("LIST_FIRSTN", 1097 ``!l n. (n <= LENGTH l) ==> 1098 (list f (FIRSTN n l) = acl2_take (nat n) (list f l))``, 1099 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN 1100 RW_TAC int_ss [acl2_take_def,rich_listTheory.FIRSTN,LENGTH,list_def] THEN 1101 ONCE_REWRITE_TAC [acl2_firstnac_def] THEN 1102 CONV_TAC (RAND_CONV (ONCE_DEPTH_CONV (REWR_CONV acl2_firstnac_def))) THEN 1103 RW_TAC int_ss [car_def,cdr_def,ite_def,TRUTH_REWRITES,REVERSE_NIL, 1104 GSYM NAT_EQUAL_0,nat_def,GSYM INT_THMS,ADD1, 1105 INT_SUB_CALCULATE,INT_ADD_CALCULATE, 1106 REWRITE_RULE [nat_def] (GSYM NAT_EQUAL_0)] THEN 1107 Cases_on `l` THEN 1108 RW_TAC int_ss [acl2_reverse_def,stringp_def,ite_def,TRUTH_REWRITES, 1109 mk_rev `[x]`,REV_DEF,list_def,car_def,cdr_def,CAR_NIL,CDR_NIL, 1110 GSYM nat_def] THEN 1111 FULL_SIMP_TAC int_ss [LENGTH,mk_list ``[h']``,mk_list ``[h';h]``] THEN 1112 MATCH_MP_TAC (SIMP_RULE std_ss [APPEND] 1113 (Q.SPECL [`b`,`a`,`f`,`h`,`[h']`] FIRST_NAC_LEMMA)) THEN 1114 DECIDE_TAC); 1115 1116 1117val SEXP_ADD_COMM = store_thm("SEXP_ADD_COMM", 1118 ``!a b. add a b = add b a``, 1119 Cases THEN Cases THEN RW_TAC int_ss [add_def,COMPLEX_ADD_def] THEN 1120 Cases_on `c` THEN Cases_on `c'` THEN 1121 PROVE_TAC [RAT_ADD_COMM,COMPLEX_ADD_def]); 1122 1123val (acl2_nthcdr_def,nthcdr_ind) = 1124 sexp.acl2_defn "ACL2::NTHCDR" 1125 (`acl2_nthcdr n l = 1126 ite (zp n) l (acl2_nthcdr (add n (unary_minus (nat 1))) (cdr l))`, 1127 WF_REL_TAC `measure (sexp_to_nat o FST)` THEN 1128 METIS_TAC [ZP_RECURSE_LEMMA,SEXP_ADD_COMM]); 1129 1130val LIST_BUTFIRSTN = store_thm("LIST_BUTFIRSTN", 1131 ``!n l. n <= LENGTH l ==> 1132 (list f (BUTFIRSTN n l) = acl2_nthcdr (nat n) (list f l))``, 1133 Induct_on `l` THEN Cases_on `n` THEN 1134 ONCE_REWRITE_TAC [acl2_nthcdr_def] THEN 1135 RW_TAC arith_ss [rich_listTheory.BUTFIRSTN,list_def,LENGTH,TRUTH_REWRITES, 1136 GSYM NAT_EQUAL_0,ite_def,GSYM NAT_PRE,cdr_def]); 1137 1138val acl2_butlast_def = 1139 sexp.acl2Define "ACL2::BUTLAST" 1140 `acl2_butlast l n = 1141 let lng = len l in 1142 ite (less n lng) (acl2_take (add lng (unary_minus n)) l) nil`; 1143 1144val LIST_BUTLASTN = store_thm("LIST_BUTLASTN", 1145 ``!n l. n <= LENGTH l ==> 1146 (list f (BUTLASTN n l) = acl2_butlast (list f l) (nat n))``, 1147 RW_TAC (int_ss ++ boolSimps.LET_ss) [rich_listTheory.BUTLASTN_FIRSTN, 1148 LIST_FIRSTN,acl2_butlast_def,GSYM LIST_LENGTH,nat_def,GSYM INT_THMS, 1149 ite_def,TRUTH_REWRITES,INT_ADD_CALCULATE] THEN 1150 SUBGOAL_THEN ``LENGTH l - n = 0`` SUBST_ALL_TAC THEN1 ARITH_TAC THEN 1151 RW_TAC int_ss [acl2_take_def] THEN 1152 ONCE_REWRITE_TAC [acl2_firstnac_def] THEN 1153 RW_TAC int_ss [zp_def,ite_def,TRUTH_REWRITES,GSYM INT_THMS, 1154 INTEGERP_INT,GSYM int_def,not_def,REVERSE_NIL]); 1155 1156val LIST_LASTN = store_thm("LIST_LASTN", 1157 ``!n l. n <= LENGTH l ==> 1158 (list f (LASTN n l) = acl2_nthcdr (nat (LENGTH l - n)) (list f l))``, 1159 RW_TAC arith_ss [rich_listTheory.LASTN_BUTFIRSTN,LIST_BUTFIRSTN]); 1160 1161val (acl2_nth_def,nth_ind) = 1162 sexp.acl2_defn "ACL2::NTH" 1163 (`acl2_nth n l = 1164 ite (consp l) 1165 (ite (zp n) (car l) 1166 (acl2_nth (add (unary_minus (nat 1)) n) (cdr l))) nil`, 1167 WF_REL_TAC `measure (sexp_to_nat o FST)` THEN 1168 METIS_TAC [ZP_RECURSE_LEMMA,SEXP_ADD_COMM]); 1169 1170val LIST_EL = store_thm("LIST_EL", 1171 ``!n l. n < LENGTH l ==> 1172 (encode (EL n l) = acl2_nth (nat n) (list encode l))``, 1173 Induct_on `n` THEN Cases_on `l` THEN ONCE_REWRITE_TAC [acl2_nth_def] THEN 1174 FULL_SIMP_TAC arith_ss [EL,HD,TL,car_def,cdr_def,list_def,LENGTH, 1175 ite_def,TRUTH_REWRITES,GSYM NAT_EQUAL_0,consp_def,nat_def,GSYM INT_THMS, 1176 INT_ADD_CALCULATE]); 1177 1178val (acl2_make_list_ac_def,acl2_make_list_ac_ind) = 1179 sexp.acl2_defn "ACL2::MAKE-LIST-AC" 1180 (`acl2_make_list_ac n val ac = 1181 ite (zp n) ac (acl2_make_list_ac (add (int ~1) n) val (cons val ac))`, 1182 WF_REL_TAC `measure (\a. Num (ABS (sexp_to_int (FST a))))` THEN 1183 RW_TAC std_ss [] THEN 1184 FULL_SIMP_TAC std_ss [zp_def,TRUTH_REWRITES,ite_def,GSYM int_def] THEN 1185 CHOOSEP_TAC THEN 1186 FULL_SIMP_TAC int_ss [GSYM INT_THMS,TRUTH_REWRITES,SEXP_TO_INT_OF_INT] THEN 1187 ONCE_REWRITE_TAC [GSYM integerTheory.INT_LT] THEN 1188 REWRITE_TAC [NUM_OF_ABS] THEN 1189 ARITH_TAC); 1190 1191 val LIST_GENLIST_LEMMA = store_thm("LIST_GENLIST_LEMMA", 1192 ``!n v f L. list f (GENLIST (K v) n ++ L) = 1193 acl2_make_list_ac (nat n) (f v) (list f L)``, 1194 Induct THEN 1195 ONCE_REWRITE_TAC [acl2_make_list_ac_def] THEN 1196 RW_TAC int_ss [rich_listTheory.GENLIST,nat_def,zp_def,ite_def, 1197 TRUTH_REWRITES,GSYM INT_THMS,GSYM int_def,not_def,list_def, 1198 rich_listTheory.SNOC_REVERSE_CONS,REVERSE_DEF,APPEND, 1199 GSYM APPEND_ASSOC, 1200 REVERSE_REVERSE,ADD1,INT_ADD_CALCULATE,INTEGERP_INT] THEN 1201 CCONTR_TAC THEN POP_ASSUM (K ALL_TAC) THEN ARITH_TAC); 1202 1203val LIST_GENLIST = save_thm("LIST_GENLIST", 1204 REWRITE_RULE [listTheory.APPEND_NIL,list_def] 1205 (GEN_ALL (Q.SPECL [`n`,`v`,`f`,`[]`] LIST_GENLIST_LEMMA))); 1206(* 1207 1208The following theorems have not yet been converted... 1209 1210val acl2_subseq_def = acl2Define "ACL2::SUBSEQ-LIST" 1211 `acl2_subseq lst start end = acl2_take (nfix (add end (unary_minus start))) (acl2_nthcdr start lst)`; 1212 1213val LIST_SEG = prove(``n + s <= LENGTH l ==> (list f (SEG n s l) = acl2_subseq (list f l) (nat s) (nat (n + s)))``, 1214 RW_TAC arith_ss [SEG_TAKE_DROP,acl2_subseq_def,LIST_BUTFIRSTN,LENGTH_BUTFIRSTN,LIST_FIRSTN] THEN 1215 RW_TAC int_ss [GSYM NAT_SUB]); 1216 1217val len_cons = prove(``len (cons a b) = add (int 1) (len b)``, 1218 RW_TAC std_ss [ONCE_REWRITE_CONV [len_def] ``len (cons a b)``,ite_def,TRUTH_REWRITES,consp_def,cdr_def,nat_def]); 1219 1220val zp_rewrite = prove(``(|= zp (nat n)) = (n = 0)``, 1221 RW_TAC int_ss [zp_def,integerp_def,GSYM int_def,nat_def,GSYM INT_LT,GSYM BOOL_NOT,ite_def, 1222 TRUTH_REWRITES,INTEGERP_INT]); 1223 1224val len_nth = 1225 prove(``!n l. (|= not (less (len l) (nat n))) ==> (len (acl2_nthcdr (nat n) l) = add (len l) (unary_minus (nat n)))``, 1226 Induct_on `l` THEN REPEAT STRIP_TAC THEN 1227 TRY (ONCE_REWRITE_TAC [len_def] THEN ONCE_REWRITE_TAC [acl2_nthcdr_def] THEN 1228 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [len_def]) THEN 1229 FULL_SIMP_TAC arith_ss [ite_def,TRUTH_REWRITES,consp_def,GSYM NAT_LT,GSYM BOOL_NOT,cdr_def] THEN 1230 SUBGOAL_THEN ``n = 0n`` SUBST_ALL_TAC THEN1 DECIDE_TAC THEN 1231 RW_TAC int_ss [nat_def,GSYM INT_SUB,zp_def,GSYM int_def,INTEGERP_INT,GSYM INT_LT,ite_def, 1232 TRUTH_REWRITES,GSYM BOOL_NOT,consp_def] THEN NO_TAC) THEN 1233 ONCE_REWRITE_TAC [acl2_nthcdr_def] THEN FULL_SIMP_TAC std_ss [len_cons,ite_def,TRUTH_REWRITES,zp_rewrite,cdr_def] THEN 1234 RW_TAC int_ss [nat_def,GSYM INT_ADD,len_cons,GSYM INT_UNARY_MINUS] THEN 1235 ASSUME_TAC (SPEC ``l':sexp`` NATP_LEN) THEN CHOOSEP_TAC THEN 1236 FULL_SIMP_TAC int_ss [GSYM INT_ADD,nat_def,GSYM INT_LT,GSYM BOOL_NOT,TRUTH_REWRITES, 1237 integerTheory.INT_SUB,GSYM int_sub] THEN 1238 `~(x < n - 1)` by ARITH_TAC THEN RES_TAC THEN 1239 POP_ASSUM SUBST_ALL_TAC THEN 1240 FULL_SIMP_TAC int_ss [GSYM INT_SUB] THEN AP_TERM_TAC THEN 1241 Cases_on `n` THEN FULL_SIMP_TAC int_ss [ADD1] THEN ARITH_TAC); 1242 1243 1244val subseq_lem1 = 1245 prove(``a <= b /\ (|= not (less (len l) (nat b))) ==> |= not (less (len (acl2_nthcdr (nat a) l)) (nat (b - a)))``, 1246 REPEAT STRIP_TAC THEN 1247 `|= not (less (len l) (nat a))` by 1248 (ASSUME_TAC (SPEC ``l:sexp`` NATP_LEN) THEN CHOOSEP_TAC THEN 1249 FULL_SIMP_TAC int_ss [GSYM INT_LT,GSYM BOOL_NOT,nat_def,TRUTH_REWRITES]) THEN 1250 RW_TAC arith_ss [len_nth] THEN 1251 ASSUME_TAC (SPEC ``l:sexp`` NATP_LEN) THEN CHOOSEP_TAC THEN 1252 FULL_SIMP_TAC int_ss [GSYM INT_LT,GSYM BOOL_NOT,nat_def,TRUTH_REWRITES,GSYM INT_SUB,NOT_LESS, 1253 integerTheory.INT_SUB]); 1254 1255val acl2_nthcdr_nil = prove(``acl2_nthcdr n nil = nil``, 1256 Cases_on `|= natp n` THENL [ 1257 CHOOSEP_TAC THEN FULL_SIMP_TAC std_ss [NATP_NAT] THEN Induct_on `n'`, 1258 ALL_TAC] THEN 1259 ONCE_REWRITE_TAC [acl2_nthcdr_def] THEN 1260 RW_TAC int_ss [ite_def,zp_rewrite,TRUTH_REWRITES,nat_def,GSYM INT_SUB,ADD1,integerTheory.INT_SUB, 1261 cdr_def,AP_TERM ``cdr`` nil_def] THEN 1262 FULL_SIMP_TAC std_ss [TRUTH_REWRITES,nat_def,natp_def,zp_def,ite_def,GSYM int_def,ANDL_REWRITE,not_def] THEN 1263 Cases_on `|= integerp n` THEN TRY CHOOSEP_TAC THEN 1264 FULL_SIMP_TAC int_ss [GSYM INT_LT,GSYM INT_EQUAL,TRUTH_REWRITES,GSYM BOOL_NOT] THEN 1265 DISJ1_TAC THEN ARITH_TAC); 1266 1267val subseq_lem2 = prove(``!l s. ~(|= not (less (len l) (nat s))) ==> (len (acl2_nthcdr (nat s) l) = nat 0)``, 1268 Induct_on `l` THEN REPEAT STRIP_TAC THEN 1269 TRY (ONCE_REWRITE_TAC [len_def] THEN ONCE_REWRITE_TAC [acl2_nthcdr_def] THEN 1270 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [len_def]) THEN 1271 FULL_SIMP_TAC arith_ss [ite_def,TRUTH_REWRITES,consp_def,GSYM NAT_LT,GSYM BOOL_NOT,cdr_def, 1272 zp_rewrite,acl2_nthcdr_nil] THEN NO_TAC) THEN 1273 ONCE_REWRITE_TAC [acl2_nthcdr_def] THEN 1274 FULL_SIMP_TAC int_ss [nat_def,len_cons,ite_def,TRUTH_REWRITES,zp_rewrite,GSYM INT_SUB,cdr_def] THEN 1275 ASSUME_TAC (SPEC ``l':sexp`` NATP_LEN) THEN CHOOSEP_TAC THEN RW_TAC std_ss [] THEN 1276 FULL_SIMP_TAC int_ss [nat_def,GSYM INT_ADD,GSYM INT_LT,GSYM BOOL_NOT,TRUTH_REWRITES,integerTheory.INT_SUB] THEN 1277 `x < s - 1` by ARITH_TAC THEN RES_TAC THEN 1278 FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP (ARITH_PROVE ``1 + &x < 0i ==> F``))); 1279 1280val LISTP_SUBSEQ = prove(``(|= not (less (len l) e)) /\ (|= listp f l) /\ (|= natp s) /\ (|= natp e) ==> 1281 |= listp f (acl2_subseq l s e)``, 1282 REPEAT STRIP_TAC THEN CHOOSEP_TAC THEN 1283 REWRITE_TAC [acl2_subseq_def] THEN 1284 MATCH_MP_TAC LISTP_TAKE THEN 1285 RW_TAC std_ss [LISTP_NTHCDR,NATP_NFIX] THEN 1286 FULL_SIMP_TAC std_ss [NATP_NAT] THEN 1287 RW_TAC int_ss [nat_def,GSYM INT_SUB,nfix_def,ANDL_REWRITE,INTEGERP_INT,ite_def, 1288 TRUTH_REWRITES,integerTheory.INT_SUB,GSYM INT_LT,GSYM BOOL_NOT,INT_NOT_LT,INT_LE_SUB_LADD] THENL [ 1289 Cases_on `|= not (less (len l) (nat s'))` THENL [ 1290 RW_TAC std_ss [GSYM nat_def,len_nth] THEN 1291 ASSUME_TAC (SPEC ``l:sexp`` NATP_LEN) THEN CHOOSEP_TAC, 1292 RW_TAC std_ss [GSYM nat_def,subseq_lem2]] THEN 1293 FULL_SIMP_TAC int_ss [nat_def,GSYM INT_SUB,GSYM INT_LT,GSYM BOOL_NOT,TRUTH_REWRITES] THEN ARITH_TAC, 1294 RW_TAC std_ss [GSYM nat_def] THEN 1295 METIS_TAC [subseq_lem1]]); 1296 1297val (acl2_last_def,acl2_last_ind) = 1298 acl2_defn "ACL2::LAST" 1299 (`acl2_last l = ite (consp (cdr l)) (acl2_last (cdr l)) l`, 1300 WF_REL_TAC `measure sexp_size` THEN Cases THEN 1301 RW_TAC arith_ss [consp_def,car_def,cdr_def,sexp_size_def,nil_def]); 1302 1303val LIST_LAST = prove(``!l. ~(l = []) ==> (encode (LAST l) = car (acl2_last (list encode l)))``, 1304 Induct THEN ONCE_REWRITE_TAC [acl2_last_def] THEN 1305 TRY (Cases_on `l`) THEN 1306 RW_TAC std_ss [car_def,list_def,LAST_DEF,ite_def,consp_def,cdr_def,TRUTH_REWRITES] THEN 1307 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss []); 1308 1309val LISTP_LAST = prove(``!l. (|= listp p l) ==> |= listp p (acl2_last l)``, 1310 Induct THEN ONCE_REWRITE_TAC [acl2_last_def] THEN 1311 RW_TAC std_ss [listp_def,TRUTH_REWRITES,ite_def,consp_def,car_def,cdr_def]); 1312 1313val LIST_FRONT = prove(``!l. ~(l = []) ==> (list f (FRONT l) = acl2_butlast (list f l) (nat 1))``, 1314 Induct THEN 1315 RW_TAC arith_ss [prove(``!l. ~(l = []) ==> 1 <= LENGTH l``,Cases THEN RW_TAC arith_ss [ADD1,LENGTH]), 1316 GSYM LIST_BUTLASTN,BUTLASTN_1]); 1317 1318val LIST_LEN = prove(``nat (LEN l n) = add (nat n) (len (list f l))``, 1319 RW_TAC std_ss [LEN_LENGTH_LEM,GSYM LIST_LENGTH,GSYM NAT_ADD,ADD_COMM]); 1320 1321 1322val LIST_REV = prove(``list f (REV l1 l2) = acl2_revappend (list f l1) (list f l2)``, 1323 RW_TAC std_ss [revappend_append,REV_REVERSE_LEM,LIST_APPEND,LIST_REVERSE]); 1324 1325 1326val (strip_cars_def,strip_cars_ind) = 1327 acl2_defn "ACL2::STRIP-CARS" 1328 (`strip_cars x = ite (consp x) (cons (caar x) (strip_cars (cdr x))) nil`, 1329 WF_REL_TAC `measure sexp_size` THEN 1330 Cases THEN 1331 RW_TAC arith_ss [consp_def,car_def,cdr_def,sexp_size_def]); 1332 1333val (strip_cdrs_def,strip_cdrs_ind) = 1334 acl2_defn "ACL2::STRIP-CDRS" 1335 (`strip_cdrs x = ite (consp x) (cons (cdar x) (strip_cdrs (cdr x))) nil`, 1336 WF_REL_TAC `measure sexp_size` THEN 1337 Cases THEN 1338 RW_TAC arith_ss [consp_def,car_def,cdr_def,sexp_size_def]); 1339 1340val LIST_UNZIP = prove(``pair (list f) (list g) (UNZIP l) = 1341 cons (strip_cars (list (pair f g) l)) (strip_cdrs (list (pair f g) l))``, 1342 Induct_on `l` THEN TRY Cases THEN 1343 ONCE_REWRITE_TAC [strip_cdrs_def,strip_cars_def] THEN 1344 RW_TAC std_ss [pair_def,list_def,UNZIP,consp_def,ite_def,TRUTH_REWRITES,AP_TERM ``consp`` nil_def, 1345 caar_def,cdar_def,car_def,cdr_def] THEN 1346 FULL_SIMP_TAC std_ss [pair_def,sexp_11]); 1347 1348val LISTP_STRIP_CARS = prove(``(|= listp (pairp f g) l) ==> (|= listp f (strip_cars l))``, 1349 Induct_on `l` THEN ONCE_REWRITE_TAC [strip_cars_def] THEN 1350 RW_TAC std_ss [listp_def,TRUTH_REWRITES,equal_def,consp_def,caar_def,AP_TERM ``listp f`` nil_def, 1351 GSYM nil_def,car_def,cdr_def,ite_def] THEN 1352 Cases_on `l` THEN FULL_SIMP_TAC std_ss [pairp_def,TRUTH_REWRITES,car_def,ite_def]); 1353 1354val LISTP_STRIP_CDRS = prove(``(|= listp (pairp f g) l) ==> (|= listp g (strip_cdrs l))``, 1355 Induct_on `l` THEN ONCE_REWRITE_TAC [strip_cdrs_def] THEN 1356 RW_TAC std_ss [listp_def,TRUTH_REWRITES,equal_def,consp_def,cdar_def,AP_TERM ``listp f`` nil_def, 1357 GSYM nil_def,car_def,cdr_def,ite_def] THEN 1358 Cases_on `l` THEN FULL_SIMP_TAC std_ss [pairp_def,TRUTH_REWRITES,cdr_def,ite_def]); 1359 1360 1361val (pairlist_def,pairlist_ind) = 1362 acl2_defn "ACL2::PAIRLIS$" 1363 (`pairlist x y = ite (consp x) (cons (cons (car x) (car y)) (pairlist (cdr x) (cdr y))) nil`, 1364 WF_REL_TAC `measure (sexp_size o FST)` THEN 1365 Cases THEN 1366 RW_TAC arith_ss [consp_def,car_def,cdr_def,sexp_size_def]); 1367 1368val LIST_ZIP = prove(``!l1 l2. (LENGTH l1 = LENGTH l2) ==> 1369 (list (pair f g) (ZIP (l1,l2)) = pairlist (list f l1) (list g l2))``, 1370 Induct_on `l1` THEN Cases_on `l2` THEN 1371 ONCE_REWRITE_TAC [pairlist_def] THEN 1372 RW_TAC std_ss [ZIP,list_def,consp_def,car_def,cdr_def,ite_def,TRUTH_REWRITES,LENGTH,pair_def]); 1373 1374val LISTP_PAIRLIST = prove(``!x y. (|= equal (len x) (len y)) /\ (|= listp f x) /\ (|= listp g y) ==> 1375 (|= listp (pairp f g) (pairlist x y))``, 1376 Induct_on `x` THEN Cases_on `y` THEN ONCE_REWRITE_TAC [len_def] THEN 1377 ONCE_REWRITE_TAC [pairlist_def] THEN 1378 RW_TAC std_ss [TRUTH_REWRITES,ite_def,consp_def,car_def,cdr_def,equal_def,listp_def, 1379 AP_TERM ``listp f`` nil_def,GSYM nil_def,pairp_def,len_cons] THEN 1380 FULL_SIMP_TAC std_ss [len_cons] THEN 1381 REPEAT (PAT_ASSUM ``!y:sexp. P y`` (STRIP_ASSUME_TAC o SPEC ``s0:sexp``)) THEN 1382 REPEAT (POP_ASSUM MP_TAC) THEN 1383 ASSUME_TAC (SPEC ``x':sexp`` NATP_LEN) THEN 1384 ASSUME_TAC (SPEC ``s0:sexp`` NATP_LEN) THEN CHOOSEP_TAC THEN 1385 RW_TAC arith_ss [NATP_NAT,GSYM NAT_ADD,NAT_CONG,GSYM nat_def,equal_def,TRUTH_REWRITES]); 1386 1387(*****************************************************************************) 1388(* String theorems: string-append *) 1389(*****************************************************************************) 1390 1391val acl2_strcat_def = acl2Define "ACL2::STRING-APPEND" `acl2_strcat s1 s2 = coerce (acl2_append (coerce s1 (sym "COMMON-LISP" "LIST")) (coerce s2 (sym "COMMON-LISP" "LIST"))) (sym "COMMON-LISP" "STRING")`; 1392 1393val STRING_STRCAT = prove(``str (STRCAT s1 s2) = acl2_strcat (str s1) (str s2)``, 1394 RW_TAC std_ss [acl2_strcat_def,coerce_rewrite,GSYM LIST_APPEND,stringTheory.STRCAT]); 1395 1396val list_chr_cong = prove(``(list chr a = list chr b) = (a = b)``, 1397 measureInduct_on `LENGTH (a ++ b)` THEN Cases THEN Cases THEN 1398 RW_TAC std_ss [list_def,APPEND,nil_def] THEN 1399 POP_ASSUM (STRIP_ASSUME_TAC o SPEC (listSyntax.mk_append(mk_var("t",``:char list``),``t':char list``))) THEN 1400 FULL_SIMP_TAC arith_ss [LENGTH,LENGTH_APPEND]); 1401 1402val length_lemma1 = prove(``!a b c. LENGTH a < LENGTH b ==> ~(a = b ++ c)``, 1403 Induct_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [LENGTH,APPEND]); 1404 1405val length_lemma2 = prove(``!a b c. ~(a = FIRSTN (LENGTH a) b) ==> ~(b = a ++ c)``, 1406 Induct_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [LENGTH,APPEND,rich_listTheory.FIRSTN] THEN METIS_TAC []); 1407 1408val STRING_PREFIX = prove(``bool (isPREFIX s1 s2) = ite (not (less (length (str s2)) (length (str s1)))) 1409 (equal (coerce (str s1) (sym "COMMON-LISP" "LIST")) (acl2_take (length (str s1)) (coerce (str s2) (sym "COMMON-LISP" "LIST")))) nil``, 1410 RW_TAC std_ss [coerce_rewrite,GSYM STRING_LENGTH,GSYM NAT_LT,ite_def,TRUTH_REWRITES,equal_def,bool_def, 1411 prove(``!a. (bool a = t) = a``,Cases THEN RW_TAC std_ss [bool_def,TRUTH_REWRITES]),stringTheory.STRLEN_THM,GSYM LIST_FIRSTN,NOT_LESS, 1412 DECIDE ``~(a <= b) ==> b <= a:num``,list_chr_cong,stringTheory.isPREFIX_STRCAT,GSYM BOOL_NOT,stringTheory.STRCAT] THEN 1413 GEN_REWRITE_TAC (STRIP_QUANT_CONV o ONCE_DEPTH_CONV) bool_rewrites [GSYM stringTheory.IMPLODE_EXPLODE] THEN 1414 REWRITE_TAC [stringTheory.EXPLODE_IMPLODE,stringTheory.IMPLODE_11] THEN 1415 TRY (Q.EXISTS_TAC `IMPLODE (BUTFIRSTN (LENGTH (EXPLODE s1)) (EXPLODE s2))`) THEN 1416 METIS_TAC [length_lemma1,NOT_LESS_EQUAL,length_lemma2,rich_listTheory.APPEND_FIRSTN_BUTFIRSTN,stringTheory.EXPLODE_IMPLODE]); 1417 1418val LISTP_EXPLODE = prove(``!x. |= listp characterp (coerce x (sym "COMMON-LISP" "LIST"))``, 1419 Cases THEN RW_TAC std_ss [coerce_def,coerce_string_to_list_def,LISTP_NIL,list_rewrite,LISTP_LIST,CHARACTERP_CHAR]); 1420 1421val STRINGP_IMPLODE = prove(``!x. |= stringp (coerce x (sym "COMMON-LISP" "STRING"))``, 1422 Cases THEN RW_TAC std_ss [coerce_def,coerce_list_to_string_def,STRINGP_STRING]); 1423 1424val NATP_LENGTH = prove(``!x. |= natp (length x)``, 1425 Cases_on `|= stringp x` THEN RW_TAC std_ss [ite_def,TRUTH_REWRITES,length_def,NATP_LEN]); 1426 1427val STRINGP_STRCAT = prove(``!s1 s2. |= stringp (acl2_strcat s1 s2)``, 1428 RW_TAC std_ss [acl2_strcat_def,STRINGP_IMPLODE]); 1429*) 1430 1431(*****************************************************************************) 1432(* FCPs *) 1433(*****************************************************************************) 1434 1435open fcpTheory; 1436 1437val fcp_encode_def = 1438 Define `fcp_encode f (:'b) (x:'a ** 'b) = list f (V2L x)`; 1439val fcp_decode_def = 1440 Define `fcp_decode f (:'b) x = 1441 if LENGTH (sexp_to_list I x) = dimindex(:'b) 1442 then L2V (sexp_to_list f x):('a ** 'b) 1443 else FCP i. f nil`; 1444 1445val fcp_detect_def = 1446 Define `fcp_detect f (:'b) x = 1447 listp f x /\ (LENGTH (sexp_to_list I x) = dimindex(:'b))`; 1448 1449val fcp_fix_def = 1450 Define `fcp_fix f (:'b) x = 1451 if LENGTH (sexp_to_list I x) = dimindex(:'b) 1452 then fix_list f x 1453 else fix_list f (fcp_encode I (:'b) ((FCP i.nil):sexp ** 'b))`; 1454 1455val ENCDECMAP_FCP = store_thm("ENCDECMAP_FCP", 1456 ``fcp_decode g (:'b) o fcp_encode f (:'b) = FCP_MAP (g o f)``, 1457 REWRITE_TAC [FUN_EQ_THM,fcp_encode_def,fcp_decode_def,combinTheory.o_THM, 1458 REWRITE_RULE [FUN_EQ_THM,combinTheory.o_THM] ENCDECMAP_LIST, 1459 LENGTH_MAP,LENGTH_V2L,FCP_MAP]); 1460 1461val ENCDETALL_FCP = store_thm("ENCDETALL_FCP", 1462 ``fcp_detect g (:'b) o fcp_encode f (:'b) = FCP_EVERY (g o f)``, 1463 REWRITE_TAC [FUN_EQ_THM,fcp_encode_def,fcp_decode_def,combinTheory.o_THM, 1464 REWRITE_RULE [FUN_EQ_THM,combinTheory.o_THM] ENCDETALL_LIST, 1465 fcp_detect_def,FCP_EVERY,FCP_MAP,LENGTH_MAP,LENGTH_V2L, 1466 REWRITE_RULE [FUN_EQ_THM,combinTheory.o_THM] ENCDECMAP_LIST]); 1467 1468local 1469open rich_listTheory 1470val length_s2l = prove( 1471 ``!x. LENGTH (sexp_to_list f x) = LENGTH (sexp_to_list g x)``, 1472 Induct THEN ASM_REWRITE_TAC [sexp_to_list_def,LENGTH]); 1473val map_fcp_lem = prove( 1474 ``!n x' x''. 1475 (!i. i < n ==> (EL i x' = ((FCP i. x):'a ** 'b) ' i)) /\ 1476 (!i. i < n ==> (EL i x'' = ((FCP i. f x):'c ** 'b) ' i)) /\ 1477 n <= dimindex(:'b) /\ (LENGTH x' = n) /\ (LENGTH x'' = n) 1478 ==> (MAP f x' = x'')``, 1479 REWRITE_TAC [LISTS_EQ] THEN Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN 1480 RW_TAC arith_ss [EL,TL,HD,MAP,LENGTH,FCP_BETA,LENGTH_MAP] THEN 1481 Cases_on `i` THEN FULL_SIMP_TAC arith_ss [EL,HD,TL,EL_MAP] THENL [ 1482 REPEAT (PAT_ASSUM ``!i. P ==> Q`` (MP_TAC o Q.SPEC `0`)), 1483 REPEAT (PAT_ASSUM ``!i. P ==> Q`` (MP_TAC o Q.SPEC `SUC n`))] THEN 1484 RW_TAC arith_ss [EL,HD,TL,FCP_BETA]); 1485in 1486val MAP_V2L = store_thm("MAP_V2L", 1487 ``MAP f (V2L ((FCP i. x):'a ** 'b)) = V2L ((FCP i. f x):'c ** 'b)``, 1488 RW_TAC arith_ss [V2L_def] THEN SELECT_ELIM_TAC THEN 1489 RW_TAC arith_ss [exists_v2l_thm] THEN SELECT_ELIM_TAC THEN 1490 RW_TAC arith_ss [exists_v2l_thm,map_fcp_lem] THEN 1491 MATCH_MP_TAC map_fcp_lem THEN 1492 Q.EXISTS_TAC `dimindex(:'b)` THEN RW_TAC arith_ss []); 1493val DECENCFIX_FCP = store_thm("DECENCFIX_FCP", 1494 ``fcp_encode f (:'b) o fcp_decode g (:'b) = fcp_fix (f o g) (:'b)``, 1495 REPEAT (CHANGED_TAC ( 1496 RW_TAC std_ss [FUN_EQ_THM,fcp_encode_def,fcp_decode_def, 1497 fcp_fix_def,fcp_detect_def,combinTheory.o_THM])) THEN1 1498 METIS_TAC [combinTheory.o_THM,V2L_L2V,length_s2l,DECENCFIX_LIST, 1499 ENCDECMAP_LIST,LENGTH_MAP,LENGTH_V2L] THEN 1500 REWRITE_TAC [GSYM DECENCFIX_LIST,combinTheory.o_THM, 1501 REWRITE_RULE [combinTheory.o_THM,FUN_EQ_THM] ENCDECMAP_LIST, 1502 MAP_V2L, 1503 ENCDECMAP_FCP,combinTheory.I_THM,combinTheory.I_o_ID]) 1504end; 1505 1506val HD_BUTFIRST_EL = store_thm("HD_BUTFIRST_EL", 1507 ``!b a. a < LENGTH b ==> (HD (BUTFIRSTN a b) = EL a b)``, 1508 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN 1509 RW_TAC arith_ss [rich_listTheory.BUTFIRSTN,LENGTH,HD,TL,EL]); 1510 1511val FCP_INDEX = store_thm("FCP_INDEX", 1512 ``a < dimindex(:'b) ==> 1513 (fcp_encode f (:'b) m = M) /\ (nat a = A) ==> 1514 (f (m ' a) = car (acl2_nthcdr A M))``, 1515 RW_TAC arith_ss [fcp_encode_def] THEN 1516 `a < LENGTH (V2L m) /\ (LENGTH (BUTFIRSTN a (V2L m)) = dimindex(:'b) - a)` 1517 by RW_TAC arith_ss [LENGTH_V2L,rich_listTheory.LENGTH_BUTFIRSTN] THEN 1518 Tactical.REVERSE (SUBGOAL_THEN 1519 ``(?x y. BUTFIRSTN a (V2L m) = x::y)`` ASSUME_TAC) THEN 1520 REPEAT (CHANGED_TAC (RW_TAC arith_ss [GSYM LIST_HD,GSYM LIST_BUTFIRSTN, 1521 HD_BUTFIRST_EL,EL_V2L])) THEN 1522 Cases_on `BUTFIRSTN a (V2L m)` THEN FULL_SIMP_TAC int_ss [LENGTH] THEN 1523 METIS_TAC []); 1524 1525 1526 val (acl2_update_nth_def,acl2_update_nth_ind) = 1527 sexp.acl2_defn "ACL2::UPDATE-NTH" 1528 (`acl2_update_nth key val l = 1529 ite (zp key) (cons val (cdr l)) 1530 (cons (car l) (acl2_update_nth (add (int ~1) key) val (cdr l)))`, 1531 WF_REL_TAC `measure (Num o ABS o sexp_to_int o FST)` THEN 1532 RW_TAC int_ss [zp_def,ite_def,TRUTH_REWRITES,GSYM int_def] THEN 1533 CHOOSEP_TAC THEN 1534 REWRITE_TAC [GSYM integerTheory.INT_LT,NUM_OF_ABS] THEN 1535 FULL_SIMP_TAC int_ss [GSYM INT_THMS,not_def,ite_def,TRUTH_REWRITES, 1536 INTEGERP_INT,SEXP_TO_INT_OF_INT] THEN 1537 FULL_SIMP_TAC int_ss [int_ge,INT_NOT_LE] THEN 1538 MAP_EVERY IMP_RES_TAC [INT_LT_IMP_LE,int_nat_lem] THEN 1539 POP_ASSUM SUBST_ALL_TAC THEN 1540 RW_TAC int_ss [INT_ADD_CALCULATE,INT_ABS_NUM,INT_ABS_NEG] THEN 1541 ARITH_TAC); 1542 1543val update_def = Define ` 1544 (update (SUC n) y (x::xs) = x::update n y xs) /\ 1545 (update 0 y (x::xs) = y::xs) /\ 1546 (update _ y [] = [])`; 1547 1548val LIST_UPDATE = store_thm("LIST_UPDATE", 1549 ``!x y z. x < LENGTH z ==> 1550 (list f (update x y z) = acl2_update_nth (nat x) (f y) (list f z))``, 1551 Induct THEN GEN_TAC THEN Cases THEN 1552 ONCE_REWRITE_TAC [acl2_update_nth_def] THEN 1553 RW_TAC int_ss [update_def,list_def,ite_def,TRUTH_REWRITES,zp_def, 1554 nat_def,INTEGERP_INT,GSYM int_def,GSYM INT_THMS,not_def,cdr_def, 1555 car_def,CAR_NIL,CDR_NIL,ADD1,INT_ADD_CALCULATE,LENGTH] THEN 1556 FULL_SIMP_TAC int_ss [int_gt]); 1557 1558local 1559open wordsTheory; 1560val length_update = prove(``!y a b. LENGTH (update a b y) = LENGTH y``, 1561 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN 1562 RW_TAC arith_ss [update_def,LENGTH]); 1563val el_lem = prove(``!i. ~(0 = i) ==> (EL i (a::x) = EL i (b::x))``, 1564 Cases THEN RW_TAC arith_ss [EL,TL]); 1565val el_update1 = prove(``!a b y. a < LENGTH y ==> (EL a (update a b y) = b)``, 1566 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN 1567 RW_TAC arith_ss [LENGTH,update_def,EL,HD,TL]); 1568val el_update2 = prove( 1569 ``!a b c y. c < LENGTH y /\ ~(c = a) ==> (EL c (update a b y) = EL c y)``, 1570 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN 1571 RW_TAC arith_ss [update_def,EL,LENGTH,HD,TL]); 1572val update_lem = prove(``!n x y a b. 1573 (LENGTH x = n) /\ (LENGTH y = n) /\ 1574 (n <= dimindex (:'b)) /\ 1575 (!i. i < n ==> (EL i x = (a :+ b) (m:'a ** 'b) ' i)) /\ 1576 (!i. i < n ==> (EL i y = (m:'a ** 'b) ' i)) ==> 1577 (x = update a b y)``, 1578 REWRITE_TAC [LISTS_EQ] THEN Induct THEN 1579 REPEAT (Cases ORELSE GEN_TAC) THEN 1580 RW_TAC arith_ss [update_def,EL,LENGTH,length_update] THEN 1581 Cases_on `i` THEN 1582 RW_TAC arith_ss [EL,FCP_UPDATE_def,FCP_BETA, 1583 DIMINDEX_GT_0,HD,TL,el_update1] THENL [ 1584 REPEAT (PAT_ASSUM ``!(x:num).P`` (MP_TAC o Q.SPEC `SUC n`)), 1585 REPEAT (PAT_ASSUM ``!(x:num).P`` (MP_TAC o Q.SPEC `0`)), 1586 ALL_TAC] THEN 1587 RW_TAC arith_ss [EL,TL,HD] THEN 1588 MAP_FIRST (fn t => 1589 t by 1590 (REPEAT (PAT_ASSUM ``!(x:num).P`` (MP_TAC o Q.SPEC `SUC n`)) THEN 1591 RW_TAC arith_ss [EL,TL]) THEN 1592 POP_ASSUM SUBST_ALL_TAC THEN 1593 CONV_TAC SYM_CONV THEN MATCH_MP_TAC el_update2 THEN 1594 RW_TAC arith_ss []) 1595 [`(m:'a ** 'b) ' (SUC n) = EL n t''`,`(m:'a ** 'b) ' (SUC n) = EL n t'`]); 1596in 1597val UPDATE_V2L = store_thm("UPDATE_V2L", 1598 ``!a b m. V2L ((a :+ b) m) = update a b (V2L m)``, 1599 REPEAT GEN_TAC THEN 1600 CONV_TAC (LAND_CONV (REWRITE_CONV [fcpTheory.V2L_def])) THEN 1601 SELECT_ELIM_TAC THEN RW_TAC arith_ss [fcpTheory.exists_v2l_thm] THEN 1602 REWRITE_TAC [fcpTheory.V2L_def] THEN SELECT_ELIM_TAC THEN 1603 RW_TAC arith_ss [fcpTheory.exists_v2l_thm] THEN 1604 MATCH_MP_TAC update_lem THEN 1605 Q.EXISTS_TAC `dimindex(:'b)` THEN RW_TAC arith_ss []) 1606end 1607 1608val ENCMAPENC_FCP = store_thm("ENCMAPENC_FCP", 1609 ``fcp_encode g (:'b) o FCP_MAP f = fcp_encode (g o f) (:'b)``, 1610 RW_TAC std_ss [fcp_encode_def,FCP_MAP,combinTheory.o_THM,FUN_EQ_THM, 1611 GSYM (REWRITE_RULE [combinTheory.o_THM,FUN_EQ_THM] ENCMAPENC_LIST)] 1612 THEN 1613 METIS_TAC [V2L_L2V,LENGTH_MAP,LENGTH_V2L]); 1614 1615val MAP_COMPOSE_FCP = store_thm("MAP_COMPOSE_FCP", 1616 ``FCP_MAP f o FCP_MAP g = FCP_MAP (f o g)``, 1617 RW_TAC int_ss [FCP_MAP,combinTheory.o_THM,FUN_EQ_THM, 1618 GSYM rich_listTheory.MAP_MAP_o] THEN 1619 METIS_TAC [V2L_L2V,LENGTH_MAP,LENGTH_V2L]); 1620 1621val FIXID_FCP = store_thm("FIXID_FCP", 1622 ``(!x. p x ==> (f x = x)) ==> 1623 !x. fcp_detect p (:'b) x ==> (fcp_fix f (:'b) x = x)``, 1624 RW_TAC int_ss [fcp_fix_def,fcp_detect_def] THEN 1625 MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] 1626 (CONV_RULE RIGHT_IMP_FORALL_CONV FIXID_LIST)) THEN 1627 PROVE_TAC []); 1628 1629val DETDEAD_FCP = store_thm("DETDEAD_FCP", 1630 ``~fcp_detect p (:'b) nil``, 1631 RW_TAC int_ss [fcp_detect_def,sexp_to_list_def,nil_def,LENGTH, 1632 wordsTheory.DIMINDEX_GT_0,DECIDE ``~(0 = a) = 0n < a``]); 1633 1634val GENERAL_DETECT_FCP = store_thm("GENERAL_DETECT_FCP", 1635 ``fcp_detect f (:'b) x ==> fcp_detect (K T) (:'b) x``, 1636 RW_TAC int_ss [fcp_detect_def] THEN 1637 IMP_RES_TAC GENERAL_DETECT_LIST); 1638 1639val FCP_UPDATE = store_thm("FCP_UPDATE", 1640 ``!a b m. a < dimindex (:'b) ==> 1641 (fcp_encode f (:'b) ((a :+ b) (m:'a ** 'b)) = 1642 acl2_update_nth (nat a) (f b) (fcp_encode f (:'b) m))``, 1643 RW_TAC int_ss [fcp_encode_def,GSYM LIST_UPDATE,LENGTH_V2L,UPDATE_V2L]); 1644 1645val MAPID_FCP = store_thm("MAPID_FCP", 1646 ``FCP_MAP I = I``, 1647 RW_TAC int_ss [FUN_EQ_THM,combinTheory.o_THM,combinTheory.I_THM,FCP_MAP, 1648 quotient_listTheory.LIST_MAP_I,V2L_def,L2V_def] THEN 1649 SELECT_ELIM_TAC THEN 1650 RW_TAC int_ss [exists_v2l_thm,CART_EQ,FCP_BETA]); 1651 1652val ALLID_FCP = store_thm("ALLID_FCP", 1653 ``FCP_EVERY (K T) = K T``, 1654 RW_TAC int_ss [FUN_EQ_THM,combinTheory.o_THM,combinTheory.K_THM,FCP_EVERY, 1655 V2L_def,L2V_def,translateTheory.ALLID_LIST]); 1656 1657val EL_GENLIST = store_thm("EL_GENLIST", 1658 ``!n. i < n ==> (EL i (GENLIST (K x) n) = x)``, 1659 Induct THEN 1660 RW_TAC int_ss [rich_listTheory.GENLIST,rich_listTheory.SNOC_REVERSE_CONS, 1661 REVERSE_DEF,REVERSE_REVERSE] THEN 1662 `LENGTH (GENLIST (K x) n) = n` by 1663 METIS_TAC [LESS_EQ_REFL,rich_listTheory.LENGTH_GENLIST] THEN 1664 `i < LENGTH (GENLIST (K x) n) \/ LENGTH (GENLIST (K x) n) <= i` by 1665 DECIDE_TAC THEN 1666 RW_TAC int_ss [rich_listTheory.EL_APPEND1,rich_listTheory.EL_APPEND2] THEN 1667 `i - n = 0` by FULL_SIMP_TAC arith_ss [ADD1] THEN 1668 RW_TAC int_ss [EL,HD]); 1669 1670val V2L_VALUE = store_thm("V2L_VALUE", 1671 ``(V2L ((FCP i. v) : 'a ** 'b)) = GENLIST (K v) (dimindex (:'b))``, 1672 RW_TAC std_ss [EL_GENLIST,LISTS_EQ,EL_V2L,rich_listTheory.LENGTH_GENLIST, 1673 LENGTH_V2L,FCP_BETA]); 1674 1675val FCP_VALUE = store_thm("FCP_VALUE", 1676 ``fcp_encode f (:'b) (FCP i. v) 1677 = acl2_make_list_ac (nat (dimindex (:'b))) (f v) nil``, 1678 RW_TAC int_ss [fcp_encode_def,V2L_VALUE,LIST_GENLIST]); 1679 1680(*****************************************************************************) 1681(* FCP words *) 1682(*****************************************************************************) 1683 1684open signedintTheory; 1685 1686(*****************************************************************************) 1687(* Coding function definitions *) 1688(*****************************************************************************) 1689 1690val word_encode_def = 1691 Define `word_encode (:'b) (x:'b word) = int (sw2i x)`; 1692val word_decode_def = 1693 Define `word_decode (:'b) x = (i2sw (sexp_to_int x)) : 'b word`; 1694val word_detect_def = 1695 Define `word_detect (:'b) x = 1696 ((sexp_to_bool o integerp) x) /\ 1697 sexp_to_int x < 2 ** (dimindex (:'b) - 1) /\ 1698 ~(2 ** (dimindex (:'b) - 1)) <= sexp_to_int x`; 1699val word_fix_def = 1700 Define `word_fix (:'b) x = int (extend (sexp_to_int x) (dimindex (:'b)))`; 1701 1702(*****************************************************************************) 1703(* Coding function proofs *) 1704(*****************************************************************************) 1705 1706val word_detect_thm = 1707 REWRITE_RULE [combinTheory.o_THM,sexp_to_bool_def] word_detect_def; 1708 1709val ENCDECMAP_WORD = store_thm("ENCDECMAP_WORD", 1710 ``word_decode (:'b) o word_encode (:'b) = I``, 1711 RW_TAC int_ss [word_encode_def,word_decode_def,combinTheory.o_THM, 1712 FUN_EQ_THM,SEXP_TO_INT_OF_INT,i2sw_sw2i,wordsTheory.sw2sw_id]); 1713 1714val DECENCFIX_WORD = store_thm("DECENCFIX_WORD", 1715 ``word_encode (:'b) o word_decode (:'b) = word_fix (:'b)``, 1716 RW_TAC int_ss [word_encode_def,word_decode_def,word_fix_def, 1717 combinTheory.o_THM,FUN_EQ_THM,sw2i_i2sw]); 1718 1719val ENCDETALL_WORD = store_thm("ENCDETALL_WORD", 1720 ``word_detect (:'b) o word_encode (:'b) = K T``, 1721 RW_TAC int_ss [combinTheory.o_THM,FUN_EQ_THM,combinTheory.K_THM, 1722 word_detect_thm,word_encode_def,INTEGERP_INT,SEXP_TO_INT_OF_INT, 1723 sw2i_def,TOP_BIT_LE] THEN 1724 RW_TAC int_ss [INT_SUB_CALCULATE,INT_ADD_CALCULATE,DIMINDEX_DOUBLE, 1725 w2n_lt_full]); 1726 1727val FIXID_WORD = store_thm("FIXID_WORD", 1728 ``!x. word_detect (:'b) x ==> (word_fix (:'b) x = x)``, 1729 RW_TAC int_ss [word_detect_thm,word_fix_def] THEN 1730 Q.ABBREV_TAC `i = sexp_to_int x` THEN 1731 `0 <= i \/ 0 <= ~i` by ARITH_TAC THEN IMP_RES_TAC int_nat_lem THEN 1732 RULE_ASSUM_TAC (CONV_RULE (TRY_CONV 1733 (REWR_CONV (ARITH_PROVE ``(~a = b) = (a = ~b:int)``)))) THEN 1734 POP_ASSUM SUBST_ALL_TAC THEN 1735 FULL_SIMP_TAC int_ss [EXTEND_POS_EQ,EXTEND_NEG_EQ,EXTEND_NEG_NEG, 1736 LESS_OR_EQ,wordsTheory.DIMINDEX_GT_0] THEN 1737 METIS_TAC [INT_OF_SEXP_TO_INT]); 1738 1739val DETDEAD_WORD = store_thm("DETDEAD_WORD", 1740 ``!x. ~word_detect (:'b) nil``, 1741 RW_TAC int_ss [word_detect_thm,DETDEAD_INT,GSYM sexp_to_bool_def]); 1742 1743val WORD_CONG = store_thm("WORD_CONG", 1744 ``(word_encode (:'a) a = word_encode (:'a) b) = (a = b)``, 1745 RW_TAC int_ss [word_encode_def,INT_CONG,GSYM sw2i_eq]); 1746 1747val WORD_FLATTEN = save_thm("WORD_FLATTEN", 1748 REWRITE_RULE [GSYM (REWRITE_CONV [combinTheory.o_THM,sexp_to_bool_def] 1749 ``(sexp_to_bool o integerp) v``)] 1750 (AP_TERM ``bool`` (SPEC_ALL word_detect_thm))); 1751 1752(*****************************************************************************) 1753(* Auxiliary rewrites *) 1754(*****************************************************************************) 1755 1756val INT_SW2I = save_thm("INT_SW2I",GSYM word_encode_def); 1757 1758 1759(*****************************************************************************) 1760(* ACL2 definitions: and, not, ior etc... *) 1761(*****************************************************************************) 1762 1763val INT_DIV2_LT = store_thm("INT_DIV2_LT", 1764 ``~(i = 0) /\ ~(i = ~1) ==> (ABS (int_div i 2) < ABS i)``, 1765 STRIP_TAC THEN 1766 `0 <= i \/ 0 <= ~i` by ARITH_TAC THEN IMP_RES_TAC int_nat_lem THEN 1767 RULE_ASSUM_TAC (CONV_RULE (TRY_CONV 1768 (REWR_CONV (ARITH_PROVE ``(~a = b) = (a = ~b:int)``)))) THEN 1769 POP_ASSUM SUBST_ALL_TAC THEN 1770 FULL_SIMP_TAC int_ss [INT_ABS_NEG,INT_DIV_CALCULATE,INT_ABS_NUM,DIV_LT_X, 1771 int_div] THEN 1772 REPEAT (CHANGED_TAC (RW_TAC int_ss [INT_ABS_NEG,INT_ABS_NUM, 1773 INT_ADD_CALCULATE,DECIDE ``a + 1 < b = a < b - 1n``,DIV_LT_X, 1774 LEFT_SUB_DISTRIB])) THEN 1775 `~(a' = 2)` by (CCONTR_TAC THEN FULL_SIMP_TAC int_ss []) THEN 1776 DECIDE_TAC); 1777 1778 1779val (acl2_logand_def,acl_logand_ind) = sexp.acl2_defn "ACL2::binary_logand" 1780 (`acl2_logand i j = 1781 ite (zip i) (cpx 0 1 0 1) 1782 (ite (zip j) (cpx 0 1 0 1) 1783 (ite (eql i (cpx (~1) 1 0 1)) j 1784 (ite (eql j (cpx (~1) 1 0 1)) i 1785 ((\x j i. 1786 add x 1787 (ite (acl2_evenp i) (cpx 0 1 0 1) 1788 (ite (acl2_evenp j) (cpx 0 1 0 1) (cpx 1 1 0 1)))) 1789 (mult (cpx 2 1 0 1) 1790 (acl2_logand (acl2_floor i (cpx 2 1 0 1)) 1791 (acl2_floor j (cpx 2 1 0 1)))) j i))))`, 1792 WF_REL_TAC `measure (Num o ABS o sexp_to_int o FST)` THEN 1793 REPEAT STRIP_TAC THEN 1794 FULL_SIMP_TAC int_ss [zip_def,ite_def,TRUTH_REWRITES, 1795 GSYM int_def,eql_def] THEN 1796 CHOOSEP_TAC THEN RES_TAC THEN 1797 FULL_SIMP_TAC int_ss [GSYM INT_THMS,TRUTH_REWRITES,SEXP_TO_INT_OF_INT, 1798 GSYM (MATCH_MP INT_DIV (ARITH_PROVE ``~(2 = 0i)``))] THEN 1799 REWRITE_TAC [GSYM integerTheory.INT_LT,NUM_OF_ABS] THEN 1800 PROVE_TAC [INT_DIV2_LT]); 1801 1802val acl2_lognot_def = sexp.acl2Define "COMMON-LISP::LOGNOT" 1803 `acl2_lognot i = add (unary_minus (ifix i)) (int ~1)`; 1804 1805val acl2_lognand_def = sexp.acl2Define "COMMON-LISP::LOGNAND" 1806 `acl2_lognand i j = acl2_lognot (acl2_logand i j)`; 1807 1808val acl2_logior_def = sexp.acl2Define "ACL2::BINARY-LOGIOR" 1809 `acl2_logior i j = 1810 acl2_lognot (acl2_logand (acl2_lognot i) (acl2_lognot j))`; 1811 1812val acl2_logorc1_def = sexp.acl2Define "COMMON-LISP::LOGORC1" 1813 `acl2_logorc1 i j = acl2_logior (acl2_lognot i) j`; 1814 1815val acl2_logorc2_def = sexp.acl2Define "COMMON-LISP::LOGORC2" 1816 `acl2_logorc2 i j = acl2_logior i (acl2_lognot j)`; 1817 1818val acl2_logandc1_def = sexp.acl2Define "COMMON-LISP::LOGANDC1" 1819 `acl2_logandc1 i j = acl2_logand (acl2_lognot i) j`; 1820 1821val acl2_logandc2_def = sexp.acl2Define "COMMON-LISP::LOGANDC2" 1822 `acl2_logandc2 i j = acl2_logand i (acl2_lognot j)`; 1823 1824val acl2_logeqv_def = sexp.acl2Define "ACL2::BINARY-LOGEQV" 1825 `acl2_logeqv i j = acl2_logand (acl2_logorc1 i j) (acl2_logorc1 j i)`; 1826 1827val acl2_logxor_def = sexp.acl2Define "ACL2::BINARY-LOGXOR" 1828 `acl2_logxor i j = acl2_lognot (acl2_logeqv i j)`; 1829 1830val acl2_lognor_def = sexp.acl2Define "COMMON-LISP::LOGNOR" 1831 `acl2_lognor i j = acl2_lognot (acl2_logior i j)`; 1832 1833val acl2_logbitp_def = sexp.acl2Define "COMMON-LISP::LOGBITP" 1834 `acl2_logbitp i j = 1835 acl2_oddp (acl2_floor (ifix j) (acl2_expt (nat 2) (nfix i)))`; 1836 1837val INT_IAND = store_thm("INT_IAND", 1838 ``!i j. int (iand i j) = acl2_logand (int i) (int j)``, 1839 completeInduct_on `Num (ABS i)` THEN 1840 ONCE_REWRITE_TAC [iand_def,acl2_logand_def] THEN 1841 RW_TAC (int_ss ++ boolSimps.LET_ss) [] THEN 1842 RW_TAC (int_ss ++ boolSimps.LET_ss) [GSYM int_def,GSYM INT_THMS,ite_def, 1843 TRUTH_REWRITES,zip_def,eql_def,INTEGERP_INT,GSYM INT_DIV, 1844 EVENP_INTMOD] THEN RES_TAC THEN 1845 REWRITE_TAC [AP_TERM ``int`` (ARITH_PROVE ``(2 * a) = (2 * a + 0i)``)] THEN 1846 REWRITE_TAC [INT_THMS] THEN 1847 FIX_CI_TAC THEN 1848 REPEAT (FIRST_ASSUM MATCH_MP_TAC ORELSE 1849 AP_THM_TAC ORELSE AP_TERM_TAC) THEN 1850 EQUAL_EXISTS_TAC THEN 1851 REWRITE_TAC [GSYM integerTheory.INT_LT,NUM_OF_ABS] THEN 1852 RW_TAC int_ss [INT_DIV2_LT]); 1853 1854val INT_INOT = store_thm("INT_INOT", 1855 ``!i. int (inot x) = acl2_lognot (int x)``, 1856 RW_TAC int_ss [inot_def,acl2_lognot_def,INT_IFIX, 1857 GSYM INT_THMS,INT_CONG] THEN 1858 ARITH_TAC); 1859 1860(*****************************************************************************) 1861(* Logical propagation theorems: *) 1862(*****************************************************************************) 1863 1864val WORD_AND = store_thm("WORD_AND", 1865 ``!a b. word_encode (:'a) (a && b : 'a word) = 1866 acl2_logand (word_encode (:'a) a) (word_encode (:'a) b)``, 1867 RW_TAC int_ss [word_encode_def,INT_IAND,sw2i_and]); 1868 1869val WORD_NOT = store_thm("WORD_NOT", 1870 ``!a. word_encode (:'a) (~ a) = acl2_lognot (word_encode (:'a) a)``, 1871 RW_TAC int_ss [word_encode_def,GSYM INT_INOT,sw2i_not]); 1872 1873val WORD_NAND = store_thm("WORD_NAND", 1874 ``!a b. word_encode (:'a) (~(a && b)) = 1875 acl2_lognand (word_encode (:'a) a) (word_encode (:'a) b)``, 1876 RW_TAC int_ss [acl2_lognand_def,WORD_AND,WORD_NOT]); 1877 1878val word_or_and = store_thm("word_or_and", 1879 ``!a b. a !! b = ~(~a && ~b)``, 1880 RW_TAC int_ss [wordsTheory.WORD_DE_MORGAN_THM,wordsTheory.WORD_NOT_NOT]); 1881 1882val WORD_OR = store_thm("WORD_OR", 1883 ``!a b. word_encode (:'a) (a !! b) = 1884 acl2_logior (word_encode (:'a) a) (word_encode (:'a) b)``, 1885 RW_TAC int_ss [word_or_and,WORD_NOT,WORD_AND,acl2_logior_def]); 1886 1887val WORD_ORC1 = store_thm("WORD_ORC1", 1888 ``!a b. word_encode (:'a) (~a !! b) = 1889 acl2_logorc1 (word_encode (:'a) a) (word_encode (:'a) b)``, 1890 RW_TAC int_ss [acl2_logorc1_def,WORD_OR,WORD_NOT]); 1891 1892val WORD_ORC2 = store_thm("WORD_ORC2", 1893 ``!a b. word_encode (:'a) (a !! ~b) = 1894 acl2_logorc2 (word_encode (:'a) a) (word_encode (:'a) b)``, 1895 RW_TAC int_ss [acl2_logorc2_def,WORD_OR,WORD_NOT]); 1896 1897val WORD_ANDC1 = store_thm("WORD_ANDC1", 1898 ``!a b. word_encode (:'a) (~a && b) = 1899 acl2_logandc1 (word_encode (:'a) a) (word_encode (:'a) b)``, 1900 RW_TAC int_ss [acl2_logandc1_def,WORD_AND,WORD_NOT]); 1901 1902val WORD_ANDC2 = store_thm("WORD_ANDC2", 1903 ``!a b. word_encode (:'a) (a && ~b) = 1904 acl2_logandc2 (word_encode (:'a) a) (word_encode (:'a) b)``, 1905 RW_TAC int_ss [acl2_logandc2_def,WORD_AND,WORD_NOT]); 1906 1907val WORD_NXOR = store_thm("WORD_NXOR", 1908 ``!a b. word_encode (:'a) (~(a ?? b)) = 1909 acl2_logeqv (word_encode (:'a) a) (word_encode (:'a) b)``, 1910 RW_TAC int_ss [acl2_logeqv_def,GSYM WORD_AND,GSYM WORD_ORC1,GSYM WORD_ORC2, 1911 WORD_CONG,wordsTheory.WORD_XOR,wordsTheory.WORD_DE_MORGAN_THM, 1912 wordsTheory.WORD_NOT_NOT]); 1913 1914val WORD_XOR = store_thm("WORD_XOR", 1915 ``!a b. word_encode (:'a) (a ?? b) = 1916 acl2_logxor (word_encode (:'a) a) (word_encode (:'a) b)``, 1917 RW_TAC int_ss [acl2_logxor_def,GSYM WORD_NXOR,GSYM WORD_NOT,WORD_CONG, 1918 wordsTheory.WORD_NOT_NOT]); 1919 1920val WORD_NOR = store_thm("WORD_NOR", 1921 ``!a b. word_encode (:'a) (~(a !! b)) = 1922 acl2_lognor (word_encode (:'a) a) (word_encode (:'a) b)``, 1923 RW_TAC int_ss [acl2_lognor_def,WORD_NOT,WORD_OR]); 1924 1925val ODDP_ABS = store_thm("ODDP_ABS", 1926 ``!a. acl2_oddp (int (ABS a)) = acl2_oddp (int a)``, 1927 GEN_TAC THEN a_INT_TAC THEN 1928 RW_TAC int_ss [INT_ABS_NUM,INT_ABS_NEG,GSYM nat_def,GSYM NAT_ODD] THEN 1929 Cases_on `ODD a'` THEN 1930 RW_TAC int_ss [acl2_oddp_def,ite_def,TRUTH_REWRITES,not_def,EVENP_INTMOD, 1931 bool_def] THEN 1932 REPEAT (POP_ASSUM MP_TAC) THEN 1933 RW_TAC int_ss [int_mod,int_div,INT_ADD_CALCULATE,INT_MUL_CALCULATE, 1934 INT_SUB_CALCULATE,bitTheory.ODD_MOD2_LEM,LEFT_ADD_DISTRIB] THEN 1935 RW_TAC int_ss [INT_MUL_CALCULATE,INT_ADD_CALCULATE] THEN 1936 IMP_RES_TAC NOT_MOD THEN 1937 FULL_SIMP_TAC int_ss [bitTheory.DIV_MULT_THM2]); 1938 1939val WORD_BIT = store_thm("WORD_BIT", 1940 ``!a b. b < dimindex (:'a) ==> (bool (a ' b) = 1941 acl2_logbitp (nat b) (word_encode (:'a) (a:'a word)))``, 1942 RW_TAC int_ss [sw2i_bit,acl2_logbitp_def,ibit_def,NAT_ODD,NAT_NFIX, 1943 GSYM NAT_EXPT] THEN 1944 RW_TAC int_ss [nat_def,NUM_OF_ABS,INT_ABS,INT_DIV,word_encode_def, 1945 INT_IFIX] THEN 1946 RW_TAC int_ss [GSYM INT_DIV,GSYM INT_ABS,ODDP_ABS]); 1947 1948val WORD_ASR = store_thm("WORD_ASR", 1949 ``!a b. word_encode (:'a) (a >> b) = 1950 acl2_floor (word_encode (:'a) a) (int (2 ** b))``, 1951 RW_TAC int_ss [sw2i_asr,word_encode_def,GSYM INT_DIV]); 1952 1953val WORD_LSL = store_thm("WORD_LSL", 1954 ``!a b. word_encode (:'a) (a << b) = 1955 int (extend (sw2i a * 2 ** b) (dimindex (:'a)))``, 1956 RW_TAC int_ss [word_encode_def,sw2i_lsl]); 1957 1958val WORD_MSB = store_thm("WORD_MSB", 1959 ``!a. bool (word_msb a) = bool (sw2i a < 0)``, 1960 RW_TAC int_ss [sw2i_msb]); 1961 1962(*****************************************************************************) 1963(* Word arithmetic: *) 1964(*****************************************************************************) 1965 1966val WORD_ADD = store_thm("WORD_ADD", 1967 ``!a b. word_encode (:'a) (a + b) = 1968 int (extend (sw2i a + sw2i b) (dimindex (:'a)))``, 1969 RW_TAC int_ss [sw2i_add,word_encode_def]); 1970 1971val WORD_SUB = store_thm("WORD_SUB", 1972 ``!a b. word_encode (:'a) (a - b) = 1973 int (extend (sw2i a - sw2i b) (dimindex (:'a)))``, 1974 RW_TAC int_ss [sw2i_sub,word_encode_def]); 1975 1976val WORD_NEG = store_thm("WORD_NEG", 1977 ``!a. word_encode (:'a) (- a) = 1978 int (extend (~ (sw2i a)) (dimindex (:'a)))``, 1979 RW_TAC int_ss [word_encode_def,sw2i_twocomp]); 1980 1981val WORD_MUL = store_thm("WORD_MUL", 1982 ``!a b. word_encode (:'a) (a * b) = 1983 int (extend (sw2i a * sw2i b) (dimindex (:'a)))``, 1984 RW_TAC int_ss [sw2i_mul,word_encode_def]); 1985 1986val WORD_DIV = store_thm("WORD_DIV", 1987 ``!a b. ~(b = 0w) ==> 1988 (word_encode (:'a) (word_sdiv a b) = 1989 int (extend (sw2i a quot sw2i b) (dimindex (:'a))))``, 1990 RW_TAC int_ss [sw2i_div,word_encode_def]); 1991 1992val WORD_T = store_thm("WORD_T", 1993 ``word_encode (:'a) UINT_MAXw = int (~1)``, 1994 RW_TAC int_ss [word_encode_def,sw2i_word_T]); 1995 1996val WORD_LT = store_thm("WORD_LT", 1997 ``bool (a < b) = bool (sw2i a < sw2i b)``, 1998 RW_TAC int_ss [INT_LT,INT_SW2I,sw2i_lt]); 1999 2000val WORD_LE = store_thm("WORD_LE", 2001 ``bool (a <= b) = bool (sw2i a <= sw2i b)``, 2002 RW_TAC int_ss [INT_LE,INT_SW2I,sw2i_le]); 2003 2004val WORD_GT = store_thm("WORD_GT", 2005 ``bool (a > b) = bool (b < a : 'a word)``, 2006 RW_TAC int_ss [wordsTheory.WORD_GREATER]); 2007 2008val WORD_GE = store_thm("WORD_GE", 2009 ``bool (a >= b) = bool (b <= a : 'a word)``, 2010 RW_TAC int_ss [wordsTheory.WORD_GREATER_EQ]); 2011 2012(*****************************************************************************) 2013(* Conversion operations: *) 2014(*****************************************************************************) 2015 2016val WORD_N2W = store_thm("WORD_N2W", 2017 ``word_encode (:'a) (n2w a) = int (extend (& a) (dimindex (:'a)))``, 2018 RW_TAC int_ss [word_encode_def,sw2i_n2w]); 2019 2020val NAT_W2N = store_thm("NAT_W2N", 2021 ``nat (w2n a) = nat (i2n (sw2i (a:'a word)) (dimindex (:'a)))``, 2022 `dimindex (:'a) - 1 + 1 = dimindex (:'a)` by 2023 METIS_TAC [wordsTheory.DIMINDEX_GT_0, 2024 DECIDE ``0 < a ==> (a - 1 + 1n = a)``] THEN 2025 RW_TAC int_ss [NAT_CONG,sw2i_def,I2N_NUM,w2n_lt_full,INT_SUB_CALCULATE, 2026 INT_ADD_CALCULATE,BIT_RWR,ADD1] THEN 2027 RW_TAC int_ss [i2n_def,w2n_lt_full] THEN 2028 RW_TAC int_ss [INT_ADD_CALCULATE,INT_SUB_CALCULATE] THEN 2029 `w2n a = 2 ** dimindex (:'a) - 1` by 2030 (MATCH_MP_TAC (DECIDE ``a < b /\ b <= a + 1 ==> (a = b - 1n)``) THEN 2031 RW_TAC int_ss [w2n_lt_full]) THEN 2032 POP_ASSUM SUBST_ALL_TAC THEN 2033 REWRITE_TAC (SUB_EQUAL_0:: 2034 map (SIMP_RULE bool_ss 2035 [bitTheory.ZERO_LT_TWOEXP] o Q.SPEC `2 ** b`) 2036 [DECIDE ``!b. 0 < b ==> (b - (b - 1) = 1n)``,ZERO_MOD]) THEN 2037 RW_TAC int_ss [INT_ADD_CALCULATE] THEN 2038 FULL_SIMP_TAC int_ss [NOT_LESS_EQUAL,DECIDE ``a < 1 = ~(0n < a)``]); 2039 2040(*****************************************************************************) 2041(* Logical integer operations: *) 2042(*****************************************************************************) 2043 2044val NAT_IFIX = store_thm("NAT_IFIX", 2045 ``!a. ifix (nat a) = nat a``, 2046 RW_TAC int_ss [nat_def,INT_IFIX]); 2047 2048local 2049open bitTheory 2050in 2051val NAT_BIT = store_thm("NAT_BIT", 2052 ``!a b. bool (BIT a b) = acl2_logbitp (nat a) (nat b)``, 2053 RW_TAC int_ss [acl2_logbitp_def,GSYM NAT_EXPT,GSYM NAT_DIV,NAT_NFIX, 2054 NAT_IFIX,GSYM NAT_ODD,BOOL_CONG] THEN 2055 RW_TAC int_ss [BIT_def,BITS_THM,ADD1,ODD_MOD2_LEM]) 2056end 2057 2058val _ = export_theory(); 2059