1(*****************************************************************************) 2(* File: translateScript.sml *) 3(* Author: James Reynolds *) 4(* *) 5(* Provides theories and definitions for conversion between s-expressions *) 6(* and native HOL *) 7(*****************************************************************************) 8 9(*****************************************************************************) 10(* Load files for interactive sessions *) 11(*****************************************************************************) 12 13(* 14val _ = app (* load infrastructure *) 15 load 16 ["sexp", 17 "sexpTheory", 18 "hol_defaxiomsTheory", 19 "intLib","listLib","translateLib"]; 20 21quietdec := true; 22use "translateScript.sml" handle _ => quietdec := false; 23quietdec := false; 24*) 25 26(*****************************************************************************) 27(* Load base theories *) 28(*****************************************************************************) 29 30open sexp sexpTheory arithmeticTheory fracTheory ratTheory integerTheory intLib 31 complex_rationalTheory intExtensionTheory combinTheory 32 hol_defaxiomsTheory rich_listTheory listTheory translateLib; 33 34(*****************************************************************************) 35(* Start new theory "translate" *) 36(*****************************************************************************) 37 38val _ = new_theory "translate"; 39 40(*****************************************************************************) 41(* General theorems for translation schemes (see add_translation_scheme) : *) 42(* SEXP_REDUCE - A theorem of the following form, specialised to sexp: *) 43(* |- !x. P x ==> M (L x) < M x /\ M (R x) < M x *) 44(* SEXP_TERMINAL - A theorem of the following form: *) 45(* |- P t = F *) 46(*****************************************************************************) 47 48val sexp_size_def = 49 snd (TypeBase.size_of ``:sexp``) handle e => 50 sexpTheory.sexp_size_def; 51 52val SEXP_REDUCE = store_thm("SEXP_REDUCE", 53 ``!x. (|= consp x) ==> 54 sexp_size (car x) < sexp_size x /\ 55 sexp_size (cdr x) < sexp_size x``, 56 Cases THEN RW_TAC arith_ss [sexp_size_def,car_def, 57 cdr_def,consp_def,ACL2_TRUE,t_def,nil_def]); 58 59val SEXP_TERMINAL = save_thm("SEXP_TERMINAL", 60 REWRITE_CONV [ACL2_TRUE,REWRITE_CONV [nil_def] ``consp nil``,consp_def] 61 ``|= consp nil``); 62 63(*****************************************************************************) 64(* Induction over s-expressions, as performed by lists. *) 65(*****************************************************************************) 66 67val sexp_list_ind = store_thm("sexp_list_ind", 68 ``!P0 P1. 69 (!x. P1 x ==> P0 x) /\ 70 (!x. (|= consp x) /\ P0 (cdr x) ==> P1 x) /\ 71 (!x. ~(|= consp x) ==> P1 x) ==> 72 (!x. P0 x) /\ (!x. P1 x)``, 73 REPEAT STRIP_TAC THEN Induct_on `x` THEN 74 TRY (METIS_TAC [sexpTheory.ACL2_TRUE,sexpTheory.consp_def]) THEN 75 PAT_ASSUM ``!x. ~p ==> q`` (K ALL_TAC) THEN 76 REPEAT (FIRST_ASSUM MATCH_MP_TAC) THEN 77 ASM_REWRITE_TAC [consp_def,cdr_def,EVAL ``|= t``] THEN 78 METIS_TAC []); 79 80(*****************************************************************************) 81(* Extra encoding functions: *) 82(*****************************************************************************) 83 84val rat_def = Define `rat a = num (com a rat_0)`; 85 86val bool_def = Define `(bool T = t) /\ (bool F = nil)`; 87 88(*****************************************************************************) 89(* Extra fix funtions: *) 90(* *) 91(*****************************************************************************) 92 93val fix_bool_def = Define `fix_bool x = if |= booleanp x then x else bool T`; 94 95val fix_rat_def = Define `fix_rat x = if |= rationalp x then x else rat 0`; 96 97val fix_char_def = 98 Define `fix_char x = if |= characterp x then x else chr #"a"`; 99 100val fix_string_def = Define `fix_string x = if |= stringp x then x else str ""`; 101 102(*****************************************************************************) 103(* Decoding functions: *) 104(* *) 105(* Inverse to ``num : complex_rational -> sexp`` *) 106(* Inverse to ``int : int -> sexp`` *) 107(* Inverse to ``nat : num -> sexp`` *) 108(* Inverse to ``rat : rat -> sexp`` *) 109(* Inverse to ``bool : bool -> sexp`` *) 110(* Inverse to ``chr : char -> sexp`` *) 111(* Inverse to ``str : string -> sexp`` *) 112(*****************************************************************************) 113 114val sexp_to_com_def = 115 Define 116 `(sexp_to_com (num a) = a) /\ (sexp_to_com _ = com_0)`; 117 118val sexp_to_int_def = 119 Define 120 `(sexp_to_int (num (com a b)) = 121 if |= integerp (num (com a b)) 122 then (rat_nmr a) / (rat_dnm a) else 0) /\ 123 (sexp_to_int _ = 0)`; 124 125val sexp_to_nat_def = 126 Define 127 `sexp_to_nat a = if |= natp a then Num (sexp_to_int a) else 0`; 128 129val sexp_to_rat_def = 130 Define 131 `(sexp_to_rat (num (com a b)) = 132 if |= rationalp (num (com a b)) then a else 0) /\ 133 (sexp_to_rat _ = 0)`; 134 135val sexp_to_bool_def = Define `sexp_to_bool x = |= x`; 136 137val sexp_to_char_def = 138 Define `(sexp_to_char (chr x) = x) /\ 139 (sexp_to_char _ = #"a")`; 140 141val sexp_to_string_def = 142 Define `(sexp_to_string (str x) = x) /\ 143 (sexp_to_string _ = "")`; 144 145(*****************************************************************************) 146(* Encoding and decoding pairs *) 147(* *) 148(* pair : ('a -> sexp) -> ('b -> sexp) -> ('a # 'b) -> sexp *) 149(* sexp_to_pair : (sexp -> 'a) -> (sexp -> 'a) -> sexp -> ('a # 'b) *) 150(* pairp : (sexp -> bool) -> (sexp -> bool) -> sexp -> bool *) 151(* all_pair : ('a -> bool) -> ('b -> bool) -> 'a # 'b -> bool *) 152(* fix_pair : (sexp -> sexp) -> (sexp -> sexp) -> sexp -> sexp *) 153(* *) 154(* Eg: pair nat int (1,2) = cons (nat 1) (int 2) *) 155(* and pairp (sexp_to_bool o natp) integerp (cons (nat 1) (int 2) = T *) 156(*****************************************************************************) 157 158val pair_def = Define `pair f g p = cons (f (FST p)) (g (SND p))`; 159 160val pair_thm = save_thm("pair_thm", 161 GEN_ALL (REWRITE_RULE [pairTheory.FST,pairTheory.SND] 162 (Q.SPECL [`f`,`g`,`(a,b)`] pair_def))); 163 164val pairp_def = 165 Define `!f g. pairp f g x = 166 if (|= consp x) then f (car x) /\ g (cdr x) else F`; 167 168val sexp_to_pair_def = 169 Define `!f g x. sexp_to_pair f g x = 170 if (|= consp x) then (f (car x),g (cdr x)) else (f nil,g nil)`; 171 172val all_pair_def = Define `all_pair P1 P2 (a,b) = P1 a /\ P2 b`; 173 174val fix_pair_def = Define `fix_pair f g x = 175 if |= consp x then (cons (f (car x)) (g (cdr x))) else pair f g (nil,nil)`; 176 177(*****************************************************************************) 178(* Encoding and decoding lists *) 179(* *) 180(* list : ('a -> sexp) -> 'a list -> sexp *) 181(* sexp_to_list : (sexp -> 'a) -> sexp -> 'a list *) 182(* listp : (sexp -> bool) -> sexp -> bool *) 183(* *) 184(* Eg: list nat [1;2;3] = cons (nat 1) (cons (nat 2) (cons (nat 3) nil)) *) 185(* and listp (sexp_to_bool o natp) *) 186(* (cons (nat 1) (cons (nat 2) (cons (nat 3) nil))) = T *) 187(*****************************************************************************) 188 189val list_def = Define 190 `(list f (x::xs) = cons (f x) (list f xs)) /\ (list f [] = nil)`; 191 192val sexp_to_list_def = 193 tDefine "sexp_to_list" 194 `(sexp_to_list f (cons x xs) = 195 (f x)::(sexp_to_list f xs)) /\ 196 (sexp_to_list f _ = [])` 197 (WF_REL_TAC `measure (sexp_size o SND)` THEN 198 RW_TAC arith_ss [sexp_size_def]); 199 200val sexp_to_list_thm = store_thm("sexp_to_list_thm", 201 ``!f x. sexp_to_list f x = 202 if (|= consp x) 203 then let (a,b) = sexp_to_pair f (sexp_to_list f) x in (a::b) 204 else []``, 205 GEN_TAC THEN Induct THEN 206 RW_TAC (std_ss ++ boolSimps.LET_ss) 207 [sexp_to_list_def,consp_def,ACL2_TRUE,t_def,nil_def, 208 car_def,cdr_def,sexp_to_pair_def]); 209 210val list_thm = store_thm("list_thm", 211 ``(!f x xs. list f (x::xs) = pair f (list f) (x,xs)) /\ 212 (!f. list f [] = nil)``, 213 REWRITE_TAC [list_def,pair_def,pairTheory.FST,pairTheory.SND]); 214 215val listp_def = tDefine "listp" 216 `(listp f (cons a b) = f a /\ listp f b) /\ 217 (listp f x = (x = nil))` 218 (WF_REL_TAC `measure (sexp_size o SND)` THEN 219 RW_TAC arith_ss [sexp_size_def]); 220 221val listp_thm = store_thm("listp_thm", 222 ``!f g x. listp f x = if (|= consp x) then 223 pairp f (listp f) x else (x = list I [])``, 224 NTAC 2 GEN_TAC THEN Induct THEN 225 REWRITE_TAC [list_def,pairp_def,listp_def,consp_def,ACL2_TRUE, 226 car_def,cdr_def,t_def,nil_def,sexp_distinct,sexp_11, 227 EVAL ``"T" = "NIL"``]); 228 229val fix_list_def = 230 tDefine "fix_list" 231 `(fix_list f (cons a b) = cons (f a) (fix_list f b)) /\ 232 (fix_list f x = list I [])` 233 (WF_REL_TAC `measure (sexp_size o SND)` THEN 234 RW_TAC arith_ss [sexp_size_def]); 235 236val fix_list_thm = store_thm("fix_list_thm", 237 ``!f x. fix_list f x = 238 if pairp (K T) (K T) x then fix_pair f (fix_list f) x else list I []``, 239 GEN_TAC THEN Induct THEN 240 REWRITE_TAC [fix_list_def,fix_pair_def,consp_def,ACL2_TRUE,EVAL ``t = nil``, 241 car_def,cdr_def,pairp_def,K_THM]); 242 243(*****************************************************************************) 244(* Source theorem all_id: all (K T) ... (K T) = K T *) 245(* Should really be moved into the respective theories... *) 246(*****************************************************************************) 247 248val ALLID_PAIR = store_thm("ALLID_PAIR", 249 ``all_pair (K T) (K T) = K T``, 250 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN 251 REWRITE_TAC [K_THM,all_pair_def]); 252 253val ALLID_LIST = store_thm("ALLID_LIST", 254 ``EVERY (K T) = K T``, 255 REWRITE_TAC [FUN_EQ_THM] THEN Induct THEN 256 ASM_REWRITE_TAC [EVERY_DEF,K_THM]); 257 258val proves = ref ([]:(int * term) list); 259val stores = ref ([]:(int * string) list); 260 261fun prove (term,tactic) = 262let val start = Time.now(); 263 val proof = Tactical.prove(term,tactic); 264 val end_t = Time.now(); 265 val diff = Time.toMilliseconds (Time.-(end_t,start)) 266in 267 (proves := (diff,term) :: (!proves) ; proof) 268end; 269 270fun store_thm (string,term,tactic) = 271let val start = Time.now(); 272 val proof = Tactical.store_thm(string,term,tactic); 273 val end_t = Time.now(); 274 val diff = Time.toMilliseconds (Time.-(end_t,start)) 275in 276 (stores := (diff,string) :: (!stores) ; proof) 277end; 278 279(*****************************************************************************) 280(* IS_INT_EXISTS : *) 281(* *) 282(* |- !a b. *) 283(* IS_INT (com a b) = (b = rat_0) /\ ?c. a = abs_rat (abs_frac (c,1)) *) 284(*****************************************************************************) 285 286val int_pos = prove(``0 < a ==> 0 < Num a``, 287 METIS_TAC [INT_OF_NUM,INT_LT,INT_LT_IMP_LE]); 288 289val int_mod_eq_thm = prove( 290 ``0 < b ==> ((Num (ABS a) MOD Num b = 0) = (a % b = 0))``, 291 ONCE_REWRITE_TAC [GSYM INT_EQ_CALCULATE] THEN 292 RW_TAC std_ss [GSYM INT_MOD,int_pos,DECIDE ``0 < a ==> ~(a = 0n)``, 293 snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)),INT_LT_IMP_LE, 294 INT_ABS_POS] THEN 295 RW_TAC int_ss [INT_ABS,INT_MOD_EQ0,INT_LT_IMP_NE] THEN 296 EQ_TAC THEN STRIP_TAC THEN 297 Q.EXISTS_TAC `~k` THEN 298 intLib.ARITH_TAC); 299 300val IS_INT_select = prove( 301 ``!a b. IS_INT (com a b) ==> (b = rat_0) /\ 302 ?c. a = abs_rat (abs_frac(c,1))``, 303 RW_TAC std_ss [IS_INT_def,DIVIDES_def,rat_nmr_def,rat_dnm_def,FRAC_DNMPOS, 304 INT_ABS_CALCULATE_POS,int_mod_eq_thm,INT_MOD_EQ0, 305 INT_LT_IMP_NE] THEN 306 Q.EXISTS_TAC `rat_nmr a / rat_dnm a` THEN 307 SUBGOAL_THEN ``?a'. a = abs_rat a'`` (CHOOSE_THEN SUBST_ALL_TAC) THEN1 308 (Q.EXISTS_TAC `rep_rat a` THEN MATCH_ACCEPT_TAC (GSYM ratTheory.RAT)) THEN 309 RW_TAC int_ss [rat_nmr_def,rat_dnm_def,RAT_EQ,DNM,NMR,INT_LT_01, 310 INT_DIV_RMUL,FRAC_DNMPOS,INT_LT_IMP_NE] THEN 311 SUBGOAL_THEN ``?c d. (a' = abs_frac (c,d)) /\ 0 < d`` STRIP_ASSUME_TAC THEN1 312 (Q.EXISTS_TAC `frac_nmr a'` THEN Q.EXISTS_TAC `frac_dnm a'` THEN 313 REWRITE_TAC [FRAC,FRAC_DNMPOS]) THEN 314 RW_TAC std_ss [NMR,DNM] THEN 315 RAT_CONG_TAC THEN 316 PAT_ASSUM ``0i < d`` (fn th => (RULE_ASSUM_TAC 317 (SIMP_RULE std_ss [th,NMR,DNM]))) THEN 318 PAT_ASSUM ``frac_nmr a = b * c:int`` SUBST_ALL_TAC THEN 319 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [ 320 CONV_RULE bool_EQ_CONV (AC_CONV(INT_MUL_ASSOC,INT_MUL_COMM) 321 ``a * b * c = (a * c) * b:int``)]) THEN 322 IMP_RES_TAC (fst (EQ_IMP_RULE (SPEC_ALL INT_EQ_RMUL))) THEN 323 MP_TAC (SPEC ``x:frac`` FRAC_DNMPOS) THEN ASM_REWRITE_TAC [INT_LT_REFL]); 324 325val IS_INT_eq = prove(``!a. IS_INT (com (abs_rat (abs_frac(a,1))) rat_0)``, 326 RW_TAC std_ss [IS_INT_def,DIVIDES_def,rat_nmr_def,rat_dnm_def,FRAC_DNMPOS, 327 INT_ABS_CALCULATE_POS,int_mod_eq_thm,INT_LT_IMP_NE] THEN 328 RAT_CONG_TAC THEN 329 FULL_SIMP_TAC int_ss [NMR,DNM,INT_LT_01,INT_MOD_COMMON_FACTOR,INT_LT_IMP_NE, 330 FRAC_DNMPOS]); 331 332val IS_INT_EXISTS = store_thm("IS_INT_EXISTS", 333 ``!a b. IS_INT (com a b) = (b = rat_0) /\ 334 ?c. a = abs_rat (abs_frac(c,1))``, 335 METIS_TAC [IS_INT_select,IS_INT_eq]); 336 337(*****************************************************************************) 338(* Congruence theorems to make proofs easier... *) 339(*****************************************************************************) 340 341val NAT_CONG = store_thm("NAT_CONG", 342 ``!a b. (nat a = nat b) = (a = b)``, 343 RW_TAC intLib.int_ss [nat_def,int_def,cpx_def,sexpTheory.rat_def, 344 ratTheory.RAT_EQ,fracTheory.NMR,fracTheory.DNM]); 345 346val INT_CONG = store_thm("INT_CONG", 347 ``!a b. (int a = int b) = (a = b)``, 348 RW_TAC intLib.int_ss [nat_def,int_def,cpx_def,sexpTheory.rat_def, 349 ratTheory.RAT_EQ,fracTheory.NMR,fracTheory.DNM]); 350 351val BOOL_CONG = store_thm("BOOL_CONG", 352 ``!a b. (bool a = bool b) = (a = b)``, 353 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN TRY AP_TERM_TAC THEN 354 Cases_on `a` THEN Cases_on `b` THEN POP_ASSUM MP_TAC THEN 355 RW_TAC std_ss [bool_def,nil_def,t_def]); 356 357(*****************************************************************************) 358(* Make sure all 'p' functions operate on |= instead of nil or t *) 359(*****************************************************************************) 360 361val nil_t = CONV_RULE bool_EQ_CONV (EVAL ``~(nil = t)``); 362val true_t = CONV_RULE bool_EQ_CONV (EVAL ``|= t``); 363val false_f = CONV_RULE bool_EQ_CONV (EVAL ``~(|= nil)``); 364val nil_nil = prove(``(x = nil) = ~|= x``, 365 EQ_TAC THEN RW_TAC std_ss [false_f] THEN 366 REPEAT (POP_ASSUM MP_TAC THEN 367 RW_TAC std_ss [ACL2_TRUE_def,ite_def,equal_def,nil_t])); 368 369val TRUTH_REWRITES = save_thm("TRUTH_REWRITES",LIST_CONJ 370 (map (fn x => 371 prove(x,TRY (Cases_on `a`) THEN 372 RW_TAC std_ss [ite_def,nil_t,true_t,false_f,bool_def, 373 consp_def,AP_TERM ``consp`` nil_def,nil_nil])) 374 [``~(nil = t)``,``(|= (if a then b else c)) = a /\ (|= b) \/ ~a /\ |= c``, 375 ``(consp nil = nil)``,``ite nil a b = b``,``ite t a b = a``, 376 ``(x = nil) = ~(|= x)``,``~(x = nil) = (|= x)``,``|= t``,``~(|= nil)``, 377 ``(|= bool a) = a``])); 378 379val ANDL_JUDGEMENT = prove( 380 ``(|= andl []) /\ !a b. (|= a) /\ (|= andl b) ==> (|= andl (a::b))``, 381 STRIP_TAC THENL [ALL_TAC,GEN_TAC THEN Induct] THEN 382 RW_TAC std_ss [andl_def,TRUTH_REWRITES,ite_def]); 383 384val ANDL_REWRITE = store_thm("ANDL_REWRITE", 385 ``!a b. (|= andl []) /\ ((|= andl (a::b)) = (|= a) /\ (|= andl b))``, 386 GEN_TAC THEN Cases THEN RW_TAC std_ss [andl_def,TRUTH_REWRITES,ite_def]); 387 388val NOT_REWRITE = store_thm("NOT_REWRITE", 389 ``(|= not a) = ~|= a``,RW_TAC std_ss [not_def,TRUTH_REWRITES,ite_def]); 390 391(*****************************************************************************) 392(* Encode, detect, all theorems (ENCDETALL). *) 393(*****************************************************************************) 394 395val ENCDETALL_BOOL = store_thm("ENCDETALL_BOOL", 396 ``(sexp_to_bool o booleanp) o bool = K T``, 397 REWRITE_TAC [FUN_EQ_THM] THEN 398 Cases THEN RW_TAC std_ss [K_THM,ite_def,bool_def,booleanp_def, 399 TRUTH_REWRITES,equal_def,sexp_to_bool_def]); 400 401val ENCDETALL_INT = store_thm("ENCDETALL_INT", 402 ``(sexp_to_bool o integerp) o int = K T``, 403 REWRITE_TAC [FUN_EQ_THM] THEN 404 RW_TAC std_ss [integerp_def,int_def,cpx_def,IS_INT_EXISTS,TRUTH_REWRITES, 405 K_THM,sexpTheory.rat_def,rat_0_def,frac_0_def, 406 sexp_to_bool_def] THEN 407 PROVE_TAC []); 408 409 val natp_int_lem = prove(``(|= (natp (int x))) = 0 <= x``, 410 RW_TAC arith_ss [natp_def,nat_def, 411 REWRITE_RULE [o_THM,FUN_EQ_THM,sexp_to_bool_def] ENCDETALL_INT, 412 TRUTH_REWRITES,andl_def,not_def,ite_def] THEN 413 RW_TAC int_ss [int_def,less_def,cpx_def,TRUTH_REWRITES] THEN 414 RW_TAC int_ss [sexpTheory.rat_def,RAT_LES_CALCULATE,NMR,DNM,INT_NOT_LT]); 415 416val ENCDETALL_NAT = store_thm("ENCDETALL_NAT", 417 ``(sexp_to_bool o natp) o nat = K T``, 418 RW_TAC int_ss [nat_def,o_THM,FUN_EQ_THM,natp_int_lem,sexp_to_bool_def]); 419 420val ENCDETALL_RAT = store_thm("ENCDETALL_RAT", 421 ``(sexp_to_bool o rationalp) o rat = K T``, 422 RW_TAC std_ss [FUN_EQ_THM,o_THM,rationalp_def,rat_def,TRUTH_REWRITES, 423 sexp_to_bool_def]); 424 425val ENCDETALL_COM = store_thm("ENCDETALL_COM", 426 ``(sexp_to_bool o acl2_numberp) o num = K T``, 427 RW_TAC std_ss [acl2_numberp_def,TRUTH_REWRITES,K_THM,o_THM, 428 sexp_to_bool_def,FUN_EQ_THM]); 429 430val ENCDETALL_PAIR = store_thm("ENCDETALL_PAIR", 431 ``(pairp p0 p1 o pair f0 f1) = all_pair (p0 o f0) (p1 o f1)``, 432 REWRITE_TAC [FUN_EQ_THM,pair_def,pairp_def,o_THM] THEN Cases THEN 433 REWRITE_TAC [o_THM,all_pair_def,consp_def,car_def,cdr_def,TRUTH_REWRITES]); 434 435val ENCDETALL_LIST = store_thm("ENCDETALL_LIST", 436 ``(listp p o list f) = EVERY (p o f)``, 437 REWRITE_TAC [FUN_EQ_THM] THEN Induct THEN 438 ASM_REWRITE_TAC [list_def,o_THM,EVERY_DEF,listp_def,nil_def] THEN 439 PROVE_TAC [o_THM]); 440 441val ENCDETALL_CHAR = store_thm("ENCDETALL_CHAR", 442 ``(sexp_to_bool o characterp) o chr = K T``, 443 RW_TAC std_ss [sexp_to_bool_def,FUN_EQ_THM,o_THM,K_THM,characterp_def, 444 TRUTH_REWRITES]); 445 446val ENCDETALL_STRING = store_thm("ENCDETALL_STRING", 447 ``(sexp_to_bool o stringp) o str = K T``, 448 RW_TAC std_ss [sexp_to_bool_def,FUN_EQ_THM,o_THM,K_THM, 449 stringp_def,TRUTH_REWRITES]); 450 451(*****************************************************************************) 452(* Encode, decode, map (ENCDECMAP) proofs *) 453(*****************************************************************************) 454 455 456local 457 458(* Ugly patch by MJCG: was failing with the RAT_CONG_TAC in translateLib *) 459val RAT_CONG_TAC = 460 REPEAT (POP_ASSUM MP_TAC) THEN 461 REPEAT (Q.PAT_ABBREV_TAC 462 `x''''' = rep_rat (abs_rat (abs_frac (a''''',b''''')))`) THEN 463 REPEAT (DISCH_TAC) THEN 464 EVERY_ASSUM (fn th => 465 (ASSUME_TAC o Rewrite.REWRITE_RULE [ratTheory.RAT] o 466 AP_TERM ``abs_rat``) 467 (Rewrite.REWRITE_RULE [markerTheory.Abbrev_def] th) 468 handle e => ALL_TAC) THEN 469 RULE_ASSUM_TAC (Rewrite.REWRITE_RULE [ratTheory.RAT_EQ]) 470 471in 472 473val ENCDECMAP_INT = store_thm("ENCDECMAP_INT", 474 ``(sexp_to_int o int) = I``, 475 REWRITE_TAC [FUN_EQ_THM,o_THM,I_THM] THEN 476 RW_TAC int_ss [sexp_to_int_def,int_def,cpx_def, 477 sexpTheory.rat_def] THEN 478 RULE_ASSUM_TAC (REWRITE_RULE [GSYM int_def,GSYM cpx_def, 479 GSYM sexpTheory.rat_def,REWRITE_RULE [FUN_EQ_THM,o_THM, 480 sexp_to_bool_def] ENCDETALL_INT,K_THM]) THEN 481 REWRITE_TAC [rat_nmr_def,rat_dnm_def] THEN 482 RAT_CONG_TAC THEN 483 POP_ASSUM MP_TAC THEN RW_TAC int_ss [NMR,DNM] THEN 484 POP_ASSUM SUBST_ALL_TAC THEN 485 MATCH_MP_TAC INT_DIV_RMUL THEN 486 PROVE_TAC [INT_POS_NZ,FRAC_DNMPOS]) 487 488end; 489 490val ENCDECMAP_NAT = store_thm("ENCDECMAP_NAT", 491 ``(sexp_to_nat o nat) = I``, 492 RW_TAC int_ss [o_THM,sexp_to_nat_def,nat_def,natp_int_lem,FUN_EQ_THM,I_THM, 493 REWRITE_RULE [FUN_EQ_THM,I_THM,o_THM] ENCDECMAP_INT]); 494 495val ENCDECMAP_RAT = store_thm("ENCDECMAP_RAT", 496 ``(sexp_to_rat o rat) = I``, 497 RW_TAC int_ss [sexp_to_rat_def,rat_def,I_THM,o_THM,FUN_EQ_THM, 498 rationalp_def,TRUTH_REWRITES]); 499 500val ENCDECMAP_COM = store_thm("ENCDECMAP_COM", 501 ``(sexp_to_com o num) = I``, 502 RW_TAC std_ss [FUN_EQ_THM,o_THM,I_THM,sexp_to_com_def]); 503 504val ENCDECMAP_PAIR = store_thm("ENCDECMAP_PAIR", 505 ``(sexp_to_pair f0 f1 o pair g0 g1) = ((f0 o g0) ## (f1 o g1))``, 506 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN 507 REWRITE_TAC [pairTheory.PAIR_MAP,pair_def,sexp_to_pair_def,o_THM,consp_def, 508 car_def,cdr_def,TRUTH_REWRITES]); 509 510val ENCDECMAP_LIST = store_thm("ENCDECMAP_LIST", 511 ``(sexp_to_list f o list g) = MAP (f o g)``, 512 REWRITE_TAC [FUN_EQ_THM] THEN Induct THEN 513 ASM_REWRITE_TAC [MAP,o_THM,list_def,sexp_to_list_def,nil_def] THEN 514 PROVE_TAC [o_THM]); 515 516val ENCDECMAP_BOOL = store_thm("ENCDECMAP_BOOL", 517 ``(sexp_to_bool o bool) = I``, 518 REWRITE_TAC [FUN_EQ_THM,o_THM,I_THM] THEN 519 Cases THEN RW_TAC std_ss [bool_def,sexp_to_bool_def,TRUTH_REWRITES]); 520 521val ENCDECMAP_CHAR = store_thm("ENCDECMAP_CHAR", 522 ``(sexp_to_char o chr) = I``, 523 RW_TAC std_ss [sexp_to_char_def,FUN_EQ_THM,o_THM,I_THM]); 524 525val ENCDECMAP_STRING = store_thm("ENCDECMAP_STRING", 526 ``(sexp_to_string o str) = I``, 527 RW_TAC std_ss [sexp_to_string_def,FUN_EQ_THM,o_THM,I_THM]); 528 529(*****************************************************************************) 530(* Decode, Encode, Fix (DECENCFIX) theorems *) 531(*****************************************************************************) 532 533val DECENCFIX_BOOL = store_thm("DECENCFIX_BOOL", 534 ``(bool o sexp_to_bool) = fix_bool``, 535 RW_TAC int_ss [bool_def,sexp_to_bool_def,fix_bool_def,o_THM,FUN_EQ_THM, 536 ACL2_TRUE,booleanp_def,ite_def,equal_def] THEN 537 Cases_on `x = nil` THEN RW_TAC arith_ss [bool_def] THEN 538 PROVE_TAC []); 539 540val DECENCFIX_INT = store_thm("DECENCFIX_INT", 541 ``(int o sexp_to_int) = ifix``, 542 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN TRY (Cases_on `c`) THEN 543 RW_TAC int_ss [ifix_def,sexp_to_int_def,o_THM,ite_def,nat_def,integerp_def, 544 ACL2_TRUE] THEN POP_ASSUM MP_TAC THEN 545 RW_TAC int_ss [TRUTH_REWRITES] THEN IMP_RES_TAC IS_INT_EXISTS THEN 546 RW_TAC int_ss [int_def,cpx_def,sexpTheory.rat_def,rat_0_def,frac_0_def, 547 rat_nmr_def,rat_dnm_def] THEN 548 RAT_CONG_TAC THEN 549 FULL_SIMP_TAC int_ss [DNM,NMR] THEN RW_TAC int_ss [] THEN 550 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN 551 MATCH_MP_TAC INT_DIV_RMUL THEN 552 PROVE_TAC [INT_POS_NZ,FRAC_DNMPOS]); 553 554val DECENCFIX_NAT = store_thm("DECENCFIX_NAT", 555 ``(nat o sexp_to_nat) = nfix``, 556 RW_TAC int_ss [nat_def,sexp_to_nat_def,FUN_EQ_THM,o_THM,nfix_def,natp_def, 557 ite_def,ISPEC ``int`` COND_RAND, 558 ISPEC ``$& : num -> int`` COND_RAND,ACL2_TRUE] THEN 559 RW_TAC int_ss [ACL2_TRUE] THEN RES_TAC THEN 560 POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN 561 RW_TAC int_ss [andl_def,ite_def,GSYM ACL2_TRUE,TRUTH_REWRITES] THEN 562 `?c. x = int c` by Q.EXISTS_TAC `sexp_to_int x` THEN 563 ASM_REWRITE_TAC [REWRITE_RULE [o_THM,FUN_EQ_THM] DECENCFIX_INT,ifix_def, 564 ite_def,TRUTH_REWRITES] THEN 565 POP_ASSUM SUBST_ALL_TAC THEN 566 FULL_SIMP_TAC int_ss [REWRITE_RULE [o_THM,FUN_EQ_THM] ENCDECMAP_INT] THEN 567 POP_ASSUM MP_TAC THEN 568 RW_TAC int_ss [int_def,less_def,cpx_def,sexpTheory.rat_def,not_def, 569 TRUTH_REWRITES,RAT_LES_CALCULATE,NMR,DNM] THEN 570 PROVE_TAC [INT_OF_NUM,INT_NOT_LT]); 571 572val DECENCFIX_RAT = store_thm("DECENCFIX_RAT", 573 ``(rat o sexp_to_rat) = fix_rat``, 574 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN TRY (Cases_on `c`) THEN 575 REWRITE_TAC [fix_rat_def,rat_def,sexp_to_rat_def,o_THM,rationalp_def, 576 TRUTH_REWRITES,sexp_to_rat_def] THEN 577 PROVE_TAC []); 578 579val DECENCFIX_COM = store_thm("DECENCFIX_COM", 580 ``(num o sexp_to_com) = fix``, 581 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN 582 RW_TAC int_ss [fix_def,sexp_to_com_def,acl2_numberp_def,ite_def, 583 TRUTH_REWRITES,com_0_def,cpx_def,sexpTheory.rat_def, 584 rat_0_def,frac_0_def]); 585 586val DECENCFIX_CHAR = store_thm("DECENCFIX_CHAR", 587 ``(chr o sexp_to_char) = fix_char``, 588 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN 589 REWRITE_TAC [sexp_to_char_def,o_THM,fix_char_def,characterp_def, 590 TRUTH_REWRITES]); 591 592val DECENCFIX_STRING = store_thm("DECENCFIX_STRING", 593 ``(str o sexp_to_string) = fix_string``, 594 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN 595 REWRITE_TAC [sexp_to_string_def,o_THM,fix_string_def,stringp_def, 596 TRUTH_REWRITES]); 597 598val DECENCFIX_PAIR = store_thm("DECENCFIX_PAIR", 599 ``(pair f0 f1 o sexp_to_pair g0 g1) = fix_pair (f0 o g0) (f1 o g1)``, 600 REWRITE_TAC [FUN_EQ_THM] THEN Cases THEN 601 RW_TAC int_ss [fix_pair_def,o_THM,sexp_to_pair_def,pair_def]); 602 603val DECENCFIX_LIST = store_thm("DECENCFIX_LIST", 604 ``(list f o sexp_to_list g) = fix_list (f o g)``, 605 REWRITE_TAC [FUN_EQ_THM] THEN Induct THEN 606 RW_TAC int_ss [fix_list_def,sexp_to_list_def,list_def] THEN 607 PROVE_TAC [o_THM]); 608 609(*****************************************************************************) 610(* Encode map encode (ENCMAPENC) fusion theorems. *) 611(*****************************************************************************) 612 613val ENCMAPENC_LIST = store_thm("ENCMAPENC_LIST", 614 ``list f o MAP g = list (f o g)``, 615 REWRITE_TAC [FUN_EQ_THM] THEN Induct THEN 616 REWRITE_TAC [o_THM,MAP,list_def] THEN METIS_TAC [o_THM]); 617 618val ENCMAPENC_PAIR = store_thm("ENCMAPENC_PAIR", 619 ``pair f1 f2 o (g1 ## g2) = pair (f1 o g1) (f2 o g2)``, 620 REWRITE_TAC [FUN_EQ_THM,o_THM,pairTheory.PAIR_MAP,pair_def]); 621 622(*****************************************************************************) 623(* Fix identity (FIXID) theorems. *) 624(*****************************************************************************) 625 626val FIXID_BOOL = store_thm("FIXID_BOOL", 627 ``!x. (sexp_to_bool o booleanp) x ==> (fix_bool x = x)``, 628 RW_TAC int_ss [fix_bool_def,booleanp_def,sexp_to_bool_def]); 629 630val FIXID_INT = store_thm("FIXID_INT", 631 ``!x. (sexp_to_bool o integerp) x ==> (ifix x = x)``, 632 RW_TAC int_ss [sexp_to_bool_def,integerp_def,ifix_def,ite_def, 633 TRUTH_REWRITES]); 634 635val FIXID_NAT = store_thm("FIXID_NAT", 636 ``!x. (sexp_to_bool o natp) x ==> (nfix x = x)``, 637 RW_TAC int_ss [sexp_to_bool_def,natp_def,nfix_def,ite_def, 638 TRUTH_REWRITES]); 639 640val FIXID_RAT = store_thm("FIXID_RAT", 641 ``!x. (sexp_to_bool o rationalp) x ==> (fix_rat x = x)``, 642 RW_TAC int_ss [sexp_to_bool_def,rationalp_def,fix_rat_def,ite_def, 643 TRUTH_REWRITES]); 644 645val FIXID_COM = store_thm("FIXID_COM", 646 ``!x. (sexp_to_bool o acl2_numberp) x ==> (fix x = x)``, 647 RW_TAC int_ss [sexp_to_bool_def,acl2_numberp_def,fix_def,ite_def, 648 TRUTH_REWRITES]); 649 650val FIXID_CHAR = store_thm("FIXID_CHAR", 651 ``!x. (sexp_to_bool o characterp) x ==> (fix_char x = x)``, 652 RW_TAC int_ss [sexp_to_bool_def,characterp_def,fix_char_def,ite_def, 653 TRUTH_REWRITES]); 654 655val FIXID_STRING = store_thm("FIXID_STRING", 656 ``!x. (sexp_to_bool o stringp) x ==> (fix_string x = x)``, 657 RW_TAC int_ss [sexp_to_bool_def,stringp_def,fix_string_def,ite_def, 658 TRUTH_REWRITES]); 659 660val FIXID_PAIR = store_thm("FIXID_PAIR", 661 ``(!x. p0 x ==> (f0 x = x)) /\ 662 (!x. p1 x ==> (f1 x = x)) ==> 663 (!x. pairp p0 p1 x ==> (fix_pair f0 f1 x = x))``, 664 STRIP_TAC THEN Cases THEN RW_TAC int_ss [fix_pair_def,pairp_def,consp_def, 665 TRUTH_REWRITES,car_def,cdr_def]); 666 667val FIXID_LIST = store_thm("FIXID_LIST", 668 ``(!x. p x ==> (f x = x)) ==> 669 (!x. listp p x ==> (fix_list f x = x))``, 670 STRIP_TAC THEN Induct THEN RW_TAC int_ss [fix_list_def,listp_def,list_def]); 671 672(*****************************************************************************) 673(* Simple encode then decode theorems. *) 674(*****************************************************************************) 675 676fun make_encdec x = REWRITE_RULE [I_THM,o_THM,FUN_EQ_THM] x; 677 678val SEXP_TO_INT_OF_INT = save_thm("SEXP_TO_INT_OF_INT", 679 make_encdec ENCDECMAP_INT); 680val SEXP_TO_NAT_OF_NAT = save_thm("SEXP_TO_NAT_OF_NAT", 681 make_encdec ENCDECMAP_NAT); 682 683(*****************************************************************************) 684(* Simple decode then encode theorems. *) 685(*****************************************************************************) 686 687val list = ref ([]:thm list); 688fun make_decenc x y = 689let val r = 690 GEN_ALL (DISCH_ALL (TRANS (SPEC_ALL (REWRITE_RULE [FUN_EQ_THM,o_THM] x)) 691 (UNDISCH (SPEC_ALL y)))); 692in (list := r :: !list ; r) 693end; 694 695val DECENC_BOOL = save_thm("DECENC_BOOL",make_decenc DECENCFIX_BOOL FIXID_BOOL); 696val DECENC_INT = save_thm("DECENC_INT",make_decenc DECENCFIX_INT FIXID_INT); 697val DECENC_NAT = save_thm("DECENC_NAT",make_decenc DECENCFIX_NAT FIXID_NAT); 698val DECENC_RAT = save_thm("DECENC_RAT",make_decenc DECENCFIX_RAT FIXID_RAT); 699val DECENC_COM = save_thm("DECENC_COM",make_decenc DECENCFIX_COM FIXID_COM); 700val DECENC_CHAR = save_thm("DECENC_CHAR",make_decenc DECENCFIX_CHAR FIXID_CHAR); 701val DECENC_STRING = save_thm("DECENC_STRING", 702 make_decenc DECENCFIX_STRING FIXID_STRING); 703 704val INT_OF_SEXP_TO_INT = save_thm("INT_OF_SEXP_TO_INT", 705 REWRITE_RULE [combinTheory.o_THM,sexp_to_bool_def] DECENC_INT); 706 707val NAT_OF_SEXP_TO_NAT = save_thm("NAT_OF_SEXP_TO_NAT", 708 REWRITE_RULE [combinTheory.o_THM,sexp_to_bool_def] DECENC_NAT); 709 710val RAT_OF_SEXP_TO_RAT = save_thm("RAT_OF_SEXP_TO_RAT", 711 REWRITE_RULE [combinTheory.o_THM,sexp_to_bool_def] DECENC_RAT); 712 713val _ = list := [INT_OF_SEXP_TO_INT,NAT_OF_SEXP_TO_NAT] @ (!list); 714 715val CHOOSEP_TAC = translateLib.CHOOSEP_TAC (!list); 716 717(*****************************************************************************) 718(* Simple encode then detect theorems. *) 719(*****************************************************************************) 720 721fun make_encdet x = 722 CONV_RULE (STRIP_QUANT_CONV (REWR_CONV o_THM)) 723 (REWRITE_RULE [FUN_EQ_THM,K_THM] x); 724 725val ENCDET_BOOL = save_thm("ENCDET_BOOL",make_encdet ENCDETALL_BOOL); 726val ENCDET_INT = save_thm("ENCDET_INT",make_encdet ENCDETALL_INT); 727val ENCDET_NAT = save_thm("ENCDET_NAT",make_encdet ENCDETALL_NAT); 728val ENCDET_RAT = save_thm("ENCDET_RAT",make_encdet ENCDETALL_RAT); 729val ENCDET_COM = save_thm("ENCDET_COM",make_encdet ENCDETALL_COM); 730val ENCDET_CHAR = save_thm("ENCDET_CHAR",make_encdet ENCDETALL_CHAR); 731val ENCDET_STRING = save_thm("ENCDET_STRING", 732 make_encdet ENCDETALL_STRING); 733 734fun make_ii x = REWRITE_RULE [o_THM,sexp_to_bool_def] x; 735 736val INTEGERP_INT = save_thm("INTEGERP_INT",make_ii ENCDET_INT); 737val NATP_NAT = save_thm("NATP_NAT",make_ii ENCDET_NAT); 738val BOOLEANP_BOOL = save_thm("BOOLEANP_BOOL",make_ii ENCDET_BOOL); 739val ACL2_NUMBERP_NUM = save_thm("ACL2_NUMBERP_NUM",make_ii ENCDET_COM); 740val RATIONALP_RAT = save_thm("RATIONALP_RAT",make_ii ENCDET_RAT); 741 742(*****************************************************************************) 743(* detect dead theorems: *) 744(* Theorems stating that the bottom value, nil, is not recursive. *) 745(* This is required for the future encoding of compound types. *) 746(* *) 747(*****************************************************************************) 748 749val DETDEAD_PAIR = store_thm("DETDEAD_PAIR", 750 ``~pairp f g nil``, 751 REWRITE_TAC [pairp_def,consp_def,TRUTH_REWRITES]); 752 753val DETDEAD_LIST = store_thm("DETDEAD_LIST", 754 ``listp p nil``, 755 REWRITE_TAC [listp_def,pairp_def,nil_def]); 756 757val DETDEAD_NAT = store_thm("DETDEAD_NAT", 758 ``~sexp_to_bool (natp nil)``, 759 REWRITE_TAC [ACL2_TRUE,natp_def,nil_def,integerp_def,sexp_to_bool_def, 760 andl_def,ite_def]); 761 762val DETDEAD_INT = store_thm("DETDEAD_INT", 763 ``~sexp_to_bool (integerp nil)``, 764 REWRITE_TAC [ACL2_TRUE,natp_def,nil_def,integerp_def,sexp_to_bool_def]); 765 766val DETDEAD_RAT = store_thm("DETDEAD_RAT", 767 ``~sexp_to_bool (rationalp nil)``, 768 REWRITE_TAC [ACL2_TRUE,rationalp_def,sexp_to_bool_def,nil_def]); 769 770val DETDEAD_COM = store_thm("DETDEAD_COM", 771 ``~sexp_to_bool (acl2_numberp nil)``, 772 REWRITE_TAC [ACL2_TRUE,acl2_numberp_def,sexp_to_bool_def,nil_def]); 773 774val DETDEAD_CHAR = store_thm("DETDEAD_CHAR", 775 ``~sexp_to_bool (characterp nil)``, 776 REWRITE_TAC [ACL2_TRUE,characterp_def,sexp_to_bool_def,nil_def]); 777 778val DETDEAD_STRING = store_thm("DETDEAD_STRING", 779 ``~sexp_to_bool (stringp nil)``, 780 REWRITE_TAC [ACL2_TRUE,stringp_def,sexp_to_bool_def,nil_def]); 781 782val DETDEAD_BOOL = store_thm("DETDEAD_BOOL", 783 ``sexp_to_bool (booleanp nil)``, 784 REWRITE_TAC [sexp_to_bool_def,booleanp_def,ite_def, 785 TRUTH_REWRITES,equal_def]); 786 787(*****************************************************************************) 788(* General detect theorems: !x. detect p x ==> detect (K T) x *) 789(*****************************************************************************) 790 791val GENERAL_DETECT_PAIR = store_thm("GENERAL_DETECT_PAIR", 792 ``!f g x. pairp f g x ==> pairp (K T) (K T) x``, 793 REWRITE_TAC [pairp_def,K_THM] THEN METIS_TAC []); 794 795val GENERAL_DETECT_LIST = store_thm("GENERAL_DETECT_LIST", 796 ``!f x. listp f x ==> listp (K T) x``, 797 GEN_TAC THEN Induct THEN REWRITE_TAC [listp_def] THEN METIS_TAC [K_THM]); 798 799(*****************************************************************************) 800(* Boolean theorems and definitions *) 801(*****************************************************************************) 802 803val FLATTEN_BOOL = store_thm("FLATTEN_BOOL", 804 ``!a. bool ((sexp_to_bool o booleanp) a) = booleanp (I a)``, 805 RW_TAC std_ss [booleanp_def,ite_def,equal_def,TRUTH_REWRITES, 806 sexp_to_bool_def,bool_def]); 807 808val COND_REWRITE = store_thm("COND_REWRITE", 809 ``T ==> 810 (bool p = P) /\ (p ==> (f a = A)) /\ (~p ==> (f b = B)) ==> 811 (f (if p then a else b) = ite P A B)``, 812 Cases_on `p` THEN 813 RW_TAC arith_ss [ite_def,bool_def,TRUTH_REWRITES] THEN 814 METIS_TAC [TRUTH_REWRITES]); 815 816val COND_T = store_thm("COND_T", 817 ``p ==> (f (if p then a else b) = f a)``, 818 METIS_TAC []); 819 820val COND_F = store_thm("COND_F", 821 ``~p ==> (f (if p then a else b) = f b)``, 822 METIS_TAC []); 823 824val BOOLEANP_EQUAL = prove(``!a b. |= booleanp (equal a b)``,RW_TAC std_ss [equal_def,booleanp_def,ite_def,TRUTH_REWRITES]); 825 826val BOOLEANP_LESS = prove(``!a b. |= booleanp (less a b)``, 827 REWRITE_TAC [booleanp_def,ite_def,equal_def,TRUTH_REWRITES] THEN 828 Cases THEN Cases THEN TRY (Cases_on `c`) THEN TRY (Cases_on `c'`) THEN RW_TAC std_ss [less_def,TRUTH_REWRITES]); 829 830 831val BOOLEANP_NOT = prove(``!a. |= booleanp (not a)``, 832 RW_TAC std_ss [booleanp_def,equal_def,ite_def,TRUTH_REWRITES,not_def]); 833 834val BOOLEANP_IF = prove(``!a b. (|= booleanp a) /\ (|= booleanp b) ==> |= booleanp (ite p a b)``, 835 REPEAT GEN_TAC THEN Cases_on `a = nil` THEN Cases_on `b = nil` THEN RW_TAC std_ss [booleanp_def,equal_def,ite_def,TRUTH_REWRITES]); 836 837val BOOLEANP_CONSP = prove(``!a. |= booleanp (consp a)``,Cases THEN RW_TAC std_ss [booleanp_def,consp_def,ite_def,TRUTH_REWRITES,equal_def]); 838 839val BOOLEANP_ZP = prove(``!a. |= booleanp (zp a)``, 840 RW_TAC std_ss [booleanp_def,ite_def,equal_def,zp_def,TRUTH_REWRITES,GSYM (SPEC ``0i`` int_def)] THEN 841 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [TRUTH_REWRITES,not_def,ite_def]); 842 843val BOOLEANP_NATP = prove(``!a. |= booleanp (natp a)``, 844 Cases_on `a` THEN RW_TAC std_ss [booleanp_def,natp_def,ite_def,TRUTH_REWRITES,integerp_def,equal_def,andl_def,not_def]); 845 846val BOOLEANP_IMPLIES = prove(``!a b. (|= booleanp a) /\ (|= booleanp b) ==> (|= booleanp (implies a b))``, 847 RW_TAC std_ss [implies_def,booleanp_def,andl_def,ite_def,equal_def,TRUTH_REWRITES,ANDL_REWRITE,not_def]); 848 849val BOOLEANP_ANDL = prove(``!a b. (|= booleanp a) /\ (|= booleanp (andl b)) ==> (|= booleanp (andl (a::b)))``, 850 GEN_TAC THEN Induct THEN RW_TAC std_ss [implies_def,booleanp_def,andl_def,ite_def,equal_def,TRUTH_REWRITES]); 851 852val BOOLEANP_ANDL_NULL = prove(``|= booleanp (andl [])``, 853 RW_TAC std_ss [andl_def,booleanp_def,ite_def,equal_def,TRUTH_REWRITES]); 854 855val BOOL_LEFT_AND = store_thm("BOOL_LEFT_AND", 856 ``!a b. T ==> (bool a = A) /\ (a ==> (bool b = B)) ==> 857 (bool (a /\ b) = andl [A; B])``, 858 REPEAT Cases THEN 859 RW_TAC arith_ss [TRUTH_REWRITES,ite_def,bool_def,andl_def]); 860 861val BOOL_RIGHT_AND = store_thm("BOOL_RIGHT_AND", 862 ``!a b. T ==> (bool b = B) /\ (b ==> (bool a = A)) ==> 863 (bool (a /\ b) = andl [B; A])``, 864 REPEAT Cases THEN 865 RW_TAC arith_ss [TRUTH_REWRITES,ite_def,bool_def,andl_def]); 866 867val BOOL_LEFT_OR = store_thm("BOOL_LEFT_OR", 868 ``!a b. T ==> (bool ~a = A) /\ (~a ==> (bool ~b = B)) ==> 869 (bool (a \/ b) = not (andl [A ; B]))``, 870 REPEAT Cases THEN 871 RW_TAC arith_ss [TRUTH_REWRITES,ite_def,bool_def,andl_def,not_def] THEN 872 PROVE_TAC []); 873 874val BOOL_RIGHT_OR = store_thm("BOOL_RIGHT_OR", 875 ``!a b. T ==> (bool ~b = B) /\ (~b ==> (bool ~a = A)) ==> 876 (bool (a \/ b) = not (andl [B ; A]))``, 877 REPEAT Cases THEN 878 RW_TAC arith_ss [TRUTH_REWRITES,ite_def,bool_def,andl_def,not_def] THEN 879 PROVE_TAC []); 880 881val BOOL_IMPLIES = store_thm("BOOL_IMPLIES", 882 ``!a b. T ==> (bool a = A) /\ (a ==> (bool b = B)) ==> 883 (bool (a ==> b) = implies A B)``, 884 REPEAT Cases THEN 885 RW_TAC arith_ss [implies_def,bool_def,andl_def,TRUTH_REWRITES,ite_def] THEN 886 METIS_TAC [TRUTH_REWRITES,ACL2_TRUE]); 887 888val BOOL_EQUALITY = store_thm("BOOL_EQUALITY", 889 ``(!x. g (f x) = x) ==> (bool (a = b) = equal (f a) (f b))``, 890 Cases_on `a = b` THEN 891 RW_TAC arith_ss [equal_def,bool_def,TRUTH_REWRITES] THEN PROVE_TAC []); 892 893val BOOL_NOT = store_thm("BOOL_NOT", 894 ``!a. bool (~a) = not (bool a)``, 895 Cases THEN RW_TAC std_ss [not_def,TRUTH_REWRITES,bool_def]); 896 897val BOOL_T = save_thm("BOOL_T",CONJUNCT1 bool_def); 898 899val BOOL_F = save_thm("BOOL_F",CONJUNCT2 bool_def); 900 901val BOOL_PAIR = store_thm("BOOL_PAIR", 902 ``!x. bool (|= consp x) = consp x``, 903 Cases THEN REWRITE_TAC [consp_def,bool_def,ACL2_TRUE,EVAL ``t = nil``]); 904 905val BOOL_PAIRP = save_thm("BOOL_PAIRP", 906 (REWRITE_CONV [pairp_def] ``bool (pairp x y z)``)); 907 908val BOOL_KT = save_thm("BOOL_KT", 909 (REWRITE_CONV [combinTheory.K_THM] ``bool (K T x)``)); 910 911val I_ENCODE = store_thm("I_ENCODE", 912 ``T ==> (encode a = A) ==> (I (encode a) = A)``, 913 RW_TAC std_ss [combinTheory.I_THM]); 914 915(*****************************************************************************) 916(* Integer theorems: *) 917(*****************************************************************************) 918 919val FLATTEN_INT = store_thm("FLATTEN_INT", 920 ``!a. bool ((sexp_to_bool o integerp) a) = integerp (I a)``, 921 Cases THEN RW_TAC std_ss [integerp_def,sexp_to_bool_def, 922 TRUTH_REWRITES,bool_def]); 923 924val INTEGERP_ADD = store_thm("INTEGERP_ADD",``!a b. (|= integerp a) /\ (|= integerp b) ==> |= integerp (add a b)``, 925 Cases THEN Cases THEN 926 RW_TAC std_ss [sexpTheory.rat_def,int_def,integerp_def,cpx_def,rat_0_def,frac_0_def,add_def,TRUTH_REWRITES] THEN 927 Cases_on `c` THEN Cases_on `c'` THEN 928 FULL_SIMP_TAC std_ss [IS_INT_EXISTS,COMPLEX_ADD_def,RAT_ADD_RID,rat_0_def,GSYM rat_0] THEN 929 Q.EXISTS_TAC `c + c'` THEN 930 RW_TAC std_ss [rat_add_def,frac_add_def] THEN 931 RAT_CONG_TAC THEN 932 FULL_SIMP_TAC int_ss [INT_LT_01,DNM,NMR] THEN 933 RW_TAC int_ss [RAT_EQ,FRAC_DNMPOS,INT_MUL_POS_SIGN,NMR,DNM,INT_LT_01,INT_RDISTRIB,INT_MUL_ASSOC] THEN 934 ARITH_TAC); 935 936val INTEGERP_MULT = store_thm("INTEGERP_MULT",``!a b. (|= integerp a) /\ (|= integerp b) ==> |= integerp (mult a b)``, 937 Cases THEN Cases THEN 938 RW_TAC std_ss [sexpTheory.rat_def,int_def,integerp_def,cpx_def,rat_0_def,frac_0_def,mult_def,TRUTH_REWRITES] THEN 939 Cases_on `c` THEN Cases_on `c'` THEN 940 FULL_SIMP_TAC std_ss [IS_INT_EXISTS,COMPLEX_MULT_def,RAT_ADD_RID,rat_0_def,GSYM rat_0,RAT_MUL_LZERO,RAT_MUL_RZERO,RAT_ADD_RID,RAT_SUB_RID] THEN 941 Q.EXISTS_TAC `c * c'` THEN 942 RW_TAC std_ss [rat_mul_def,frac_mul_def] THEN 943 RAT_CONG_TAC THEN 944 FULL_SIMP_TAC int_ss [INT_LT_01,DNM,NMR] THEN 945 RW_TAC int_ss [RAT_EQ,FRAC_DNMPOS,INT_MUL_POS_SIGN,NMR,DNM,INT_LT_01,INT_RDISTRIB,INT_MUL_ASSOC] THEN 946 ARITH_TAC); 947 948val INTEGERP_UNARY_MINUS = store_thm("INTEGERP_UNARY_MINUS",``!a. (|= integerp a) ==> |= integerp (unary_minus a)``, 949 Cases THEN 950 RW_TAC std_ss [sexpTheory.rat_def,int_def,integerp_def,cpx_def,rat_0_def,frac_0_def,unary_minus_def,TRUTH_REWRITES] THEN 951 Cases_on `c` THEN 952 FULL_SIMP_TAC std_ss [IS_INT_EXISTS,COMPLEX_SUB_def,RAT_ADD_RID,rat_0_def,GSYM rat_0,com_0_def] THEN 953 POP_ASSUM MP_TAC THEN RW_TAC std_ss [RAT_SUB_RID,RAT_SUB_LID,RAT_AINV_0] THEN 954 Q.EXISTS_TAC `~c` THEN 955 RW_TAC std_ss [RAT_AINV_CALCULATE,frac_ainv_def,NMR,INT_LT_01,DNM]); 956 957val INT_ADD = store_thm("INT_ADD",``!a b. int (a + b) = add (int a) (int b)``, 958 RW_TAC int_ss [add_def,int_def,cpx_def,sexpTheory.rat_def,COMPLEX_ADD_def,rat_add_def,frac_add_def,RAT_EQ,NMR,DNM,INT_LT_01] THEN 959 RAT_CONG_TAC THEN 960 FULL_SIMP_TAC int_ss [NMR,DNM,INT_LT_01,RAT_EQ,FRAC_DNMPOS,INT_MUL_POS_SIGN,GSYM INT_ADD] THEN ARITH_TAC); 961 962val INT_MULT = store_thm("INT_MULT",``!a b. int (a * b) = mult (int a) (int b)``, 963 RW_TAC std_ss [mult_def,int_def,cpx_def,sexpTheory.rat_def,GSYM rat_0,GSYM frac_0_def,COMPLEX_MULT_def, 964 RAT_MUL_RZERO,RAT_SUB_RID,RAT_MUL_LZERO,RAT_ADD_RID] THEN 965 RW_TAC int_ss [RAT_EQ,rat_mul_def,frac_mul_def,DNM,NMR,INT_LT_01] THEN 966 RAT_CONG_TAC THEN 967 FULL_SIMP_TAC int_ss [DNM,NMR,INT_LT_01,FRAC_DNMPOS,INT_MUL_POS_SIGN] THEN ARITH_TAC); 968 969val INT_UNARY_MINUS = store_thm("INT_UNARY_MINUS",``!a. int (~a) = unary_minus (int a)``, 970 RW_TAC int_ss [unary_minus_def,int_def,cpx_def,sexpTheory.rat_def,GSYM rat_0,GSYM frac_0_def,COMPLEX_SUB_def,com_0_def, 971 rat_0_def,GSYM rat_0,RAT_SUB_LID,RAT_AINV_CALCULATE,RAT_AINV_0,FRAC_AINV_CALCULATE]); 972 973val INT_EQUAL = store_thm("INT_EQUAL", 974 ``!a b. bool (a = b) = equal (int a) (int b)``, 975 RW_TAC std_ss [INT_CONG,equal_def,bool_def,TRUTH_REWRITES]); 976 977val INT_LT = store_thm("INT_LT",``!a b. bool (a < b) = less (int a) (int b)``, 978 RW_TAC intLib.int_ss [nat_def,int_def,cpx_def,sexpTheory.rat_def,ratTheory.RAT_EQ,fracTheory.NMR,fracTheory.DNM,less_def,RAT_LES_CALCULATE,bool_def]); 979 980(*****************************************************************************) 981(* Nat theorems: *) 982(*****************************************************************************) 983 984val FLATTEN_NAT = store_thm("FLATTEN_NAT", 985 ``bool ((sexp_to_bool o natp) a) = natp (I a)``, 986 REPEAT (RW_TAC arith_ss [natp_def,bool_def,less_def,andl_def,not_def, 987 ite_def,TRUTH_REWRITES,sexp_to_bool_def])); 988 989val NAT_EQUAL = store_thm("NAT_EQUAL",``!a b. bool (a = b) = equal (nat a) (nat b)``, 990 RW_TAC int_ss [NAT_CONG,equal_def,bool_def]); 991 992val NAT_EQUAL_0 = store_thm("NAT_EQUAL_0",``!a. bool (a = 0n) = zp (nat a)``, 993 Cases THEN RW_TAC int_ss [bool_def,zp_def,nat_def,INTEGERP_INT, 994 TRUTH_REWRITES,ite_def,GSYM int_def,GSYM INT_LT,not_def]); 995 996val NAT_0_LT = store_thm("NAT_0_LT", 997 ``!a. bool (0n < a) = not (zp (nat a))``, 998 Cases THEN RW_TAC int_ss [bool_def,zp_def,nat_def,INTEGERP_INT, 999 TRUTH_REWRITES,ite_def,GSYM int_def,GSYM INT_LT,not_def]); 1000 1001val NAT_ADD = store_thm("NAT_ADD", 1002 ``!a b. nat (a + b) = add (nat a) (nat b)``, 1003 RW_TAC std_ss [nat_def,add_def,int_def,cpx_def,sexpTheory.rat_def, 1004 COMPLEX_ADD_def,rat_0_def,GSYM rat_0,GSYM frac_0_def,RAT_ADD_RID, 1005 rat_add_def,frac_add_def] THEN 1006 RAT_CONG_TAC THEN 1007 FULL_SIMP_TAC int_ss [NMR,DNM,INT_LT_01,RAT_EQ,FRAC_DNMPOS, 1008 INT_MUL_POS_SIGN,INT_LT_IMP_NE] THEN ARITH_TAC); 1009 1010val NAT_SUC = store_thm("NAT_SUC",``!a. nat (SUC a) = add (nat a) (nat 1)``, 1011 RW_TAC std_ss [NAT_ADD,ADD1]); 1012 1013val NAT_PRE = store_thm("NAT_PRE",``!a. (?d. a = SUC d) ==> 1014 (nat (PRE a) = add (nat a) (unary_minus (nat 1)))``, 1015 Cases THEN 1016 RW_TAC arith_ss [nat_def,GSYM INT_UNARY_MINUS,GSYM INT_ADD] THEN 1017 AP_TERM_TAC THEN RW_TAC int_ss [ADD1,GSYM integerTheory.INT_ADD] THEN 1018 ARITH_TAC); 1019 1020val NAT_SUC_PRE = store_thm("NAT_SUC_PRE", 1021 ``!a. (?d. a = SUC d) ==> (nat (SUC (PRE a)) = nat a)``, 1022 Cases THEN REPEAT STRIP_TAC THEN AP_TERM_TAC THEN RW_TAC arith_ss [ADD1]); 1023 1024val NAT_MULT = store_thm("NAT_MULT", 1025 ``!a b. nat (a * b) = mult (nat a) (nat b)``, 1026 RW_TAC std_ss [nat_def,mult_def,int_def,cpx_def,sexpTheory.rat_def, 1027 COMPLEX_MULT_def,rat_0_def,GSYM rat_0,GSYM frac_0_def, 1028 RAT_MUL_RZERO,RAT_SUB_RID,rat_mul_def,frac_mul_def,RAT_ADD_RID] THEN 1029 RAT_CONG_TAC THEN 1030 FULL_SIMP_TAC int_ss [NMR,DNM,INT_LT_01,RAT_EQ,FRAC_DNMPOS, 1031 INT_MUL_POS_SIGN,INT_LT_IMP_NE,rat_0,frac_0_def,RAT_NMREQ0_CONG] THEN 1032 ARITH_TAC); 1033 1034val NAT_NUM = store_thm("NAT_NUM", 1035 ``!a b. 0 <= a ==> (nat (Num a) = int a)``, 1036 RW_TAC int_ss [nat_def,INT_OF_NUM,INT_CONG]); 1037 1038(*****************************************************************************) 1039(* Rational theorems: *) 1040(*****************************************************************************) 1041 1042val FLATTEN_RAT = store_thm("FLATTEN_RAT", 1043 ``!a. bool ((sexp_to_bool o rationalp) a) = rationalp (I a)``, 1044 Cases THEN MAP_EVERY (TRY o Cases_on) [`c`,`c'`] THEN 1045 RW_TAC std_ss [rationalp_def,sexp_to_bool_def, 1046 TRUTH_REWRITES,bool_def]); 1047 1048val RATIONALP_ADD = store_thm("RATIONALP_ADD",``!a b. (|= rationalp a) /\ (|= rationalp b) ==> |= rationalp (add a b)``, 1049 Cases THEN Cases THEN RW_TAC std_ss [rationalp_def,add_def,TRUTH_REWRITES] THEN 1050 Cases_on `c` THEN Cases_on `c'` THEN FULL_SIMP_TAC std_ss [rationalp_def,COMPLEX_ADD_def,TRUTH_REWRITES,rat_0_def,GSYM rat_0,RAT_ADD_RID]); 1051 1052val RATIONALP_MULT = store_thm("RATIONALP_MULT",``!a b. (|= rationalp a) /\ (|= rationalp b) ==> |= rationalp (mult a b)``, 1053 Cases THEN Cases THEN RW_TAC std_ss [rationalp_def,mult_def,TRUTH_REWRITES] THEN 1054 Cases_on `c` THEN Cases_on `c'` THEN FULL_SIMP_TAC std_ss [rationalp_def,COMPLEX_MULT_def,TRUTH_REWRITES,rat_0_def,GSYM rat_0,RAT_ADD_RID,RAT_MUL_RZERO,RAT_MUL_LZERO]); 1055 1056val RATIONALP_UNARY_MINUS = store_thm("RATIONALP_UNARY_MINUS",``!a. (|= rationalp a) ==> |= rationalp (unary_minus a)``, 1057 Cases THEN RW_TAC std_ss [rationalp_def,unary_minus_def,TRUTH_REWRITES] THEN 1058 Cases_on `c` THEN FULL_SIMP_TAC std_ss [rationalp_def,TRUTH_REWRITES,rat_0_def,GSYM rat_0,com_0_def,COMPLEX_SUB_def,RAT_SUB_RID]); 1059 1060val RATIONALP_RECIPROCAL = store_thm("RATIONALP_RECIPROCAL",``!a. (|= rationalp a) ==> |= rationalp (reciprocal a)``, 1061 Cases THEN RW_TAC std_ss [rationalp_def,reciprocal_def,TRUTH_REWRITES,int_def,com_0_def,cpx_def,sexpTheory.rat_def,rat_0_def, GSYM rat_0,GSYM frac_0_def] THEN 1062 Cases_on `c` THEN FULL_SIMP_TAC std_ss [COMPLEX_RECIPROCAL_def,complex_rational_11,rationalp_def,TRUTH_REWRITES,rat_0_def, 1063 GSYM rat_0,RAT_MUL_RZERO,RAT_ADD_RID,RAT_AINV_0,RAT_LDIV_EQ,RAT_NO_ZERODIV_NEG]); 1064 1065 1066val RAT_ADD = store_thm("RAT_ADD",``!a b. rat (a + b) = add (rat a) (rat b)``, 1067 RW_TAC std_ss [add_def,COMPLEX_ADD_def,rat_0_def,GSYM rat_0,RAT_ADD_RID,rat_def]); 1068 1069val RAT_MULT = store_thm("RAT_MULT",``!a b. rat (a * b) = mult (rat a) (rat b)``, 1070 RW_TAC std_ss [mult_def,COMPLEX_MULT_def,rat_0_def,GSYM rat_0,rat_def,RAT_SUB_RID,RAT_MUL_LZERO,RAT_MUL_RZERO,RAT_ADD_RID]); 1071 1072val RAT_UNARY_MINUS = store_thm("RAT_UNARY_MINUS",``!a. rat (~a) = unary_minus (rat a)``, 1073 RW_TAC std_ss [rat_def,unary_minus_def,com_0_def,COMPLEX_SUB_def,rat_0_def,GSYM rat_0,RAT_SUB_LID,RAT_AINV_0]); 1074 1075val rat_divshiftthm = prove(``a * (b / c) = a * b / c:rat``, 1076 RW_TAC std_ss [RAT_DIV_MULMINV,RAT_MUL_ASSOC]); 1077 1078val RAT_DIV = store_thm("RAT_DIV", 1079 ``!a b. ~(b = 0) ==> (rat (a / b) = mult (rat a) (reciprocal (rat b)))``, 1080 RW_TAC std_ss [rat_def,mult_def,reciprocal_def,COMPLEX_RECIPROCAL_def, 1081 rat_0_def,GSYM rat_0,COMPLEX_MULT_def,RAT_MUL_RZERO, 1082 RAT_ADD_RID,RAT_MUL_LZERO,RAT_ADD_LID,RAT_AINV_0,int_def, 1083 RAT_SUB_RID,com_0_def,complex_rational_11,cpx_def,sexpTheory.rat_def, 1084 GSYM frac_0_def,RAT_LDIV_EQ,rat_divshiftthm,RAT_NO_ZERODIV_NEG, 1085 RAT_RDIV_EQ,RAT_MUL_ASSOC] THEN 1086 CONV_TAC (AC_CONV (RAT_MUL_ASSOC,RAT_MUL_COMM))); 1087 1088val RAT_SUB = store_thm("RAT_SUB",``!a b. rat (a - b) = add (rat a) (unary_minus (rat b))``, 1089 RW_TAC std_ss [rat_def,add_def,unary_minus_def,com_0_def,rat_0_def,GSYM rat_0,COMPLEX_SUB_def,COMPLEX_ADD_def,RAT_SUB_LID,RAT_ADD_RID,RAT_AINV_0,RAT_SUB_ADDAINV]); 1090 1091val RAT_EQUAL = store_thm("RAT_EQUAL",``!a b. bool (a = b) = equal (rat a) (rat b)``,RW_TAC std_ss [bool_def,equal_def,rat_def,RAT_LES_REF]); 1092 1093(*****************************************************************************) 1094(* Complex (general number) theorems: *) 1095(*****************************************************************************) 1096 1097val ACL2_NUMBERP_COM = store_thm("ACL2_NUMBERP_COM",``!a. |= acl2_numberp (num a)``,RW_TAC std_ss [acl2_numberp_def,TRUTH_REWRITES]); 1098 1099val ACL2_NUMBERP_ADD = store_thm("ACL2_NUMBERP_ADD",``!a b. |= acl2_numberp (add a b)``, 1100 Cases THEN Cases THEN RW_TAC std_ss [acl2_numberp_def,add_def,TRUTH_REWRITES,int_def,cpx_def]); 1101 1102val ACL2_NUMBERP_MULT = store_thm("ACL2_NUMBERP_MULT",``!a b. |= acl2_numberp (mult a b)``, 1103 Cases THEN Cases THEN RW_TAC std_ss [acl2_numberp_def,mult_def,TRUTH_REWRITES,int_def,cpx_def]); 1104 1105val ACL2_NUMBERP_UNARY_MINUS = store_thm("ACL2_NUMBERP_UNARY_MINUS",``!a. |= acl2_numberp (unary_minus a)``, 1106 Cases_on `a` THEN RW_TAC std_ss [acl2_numberp_def,unary_minus_def,TRUTH_REWRITES,int_def,cpx_def]); 1107 1108val ACL2_NUMBERP_RECIPROCAL = store_thm("ACL2_NUMBERP_RECIPROCAL",``!a. |= acl2_numberp (reciprocal a)``, 1109 Cases_on `a` THEN RW_TAC std_ss [acl2_numberp_def,reciprocal_def,TRUTH_REWRITES,int_def,cpx_def]); 1110 1111val COM_ADD = store_thm("COM_ADD",``!a b. num (a + b) = add (num a) (num b)``,RW_TAC std_ss [add_def]); 1112 1113val COM_MULT = store_thm("COM_MULT",``!a b. num (a * b) = mult (num a) (num b)``,RW_TAC std_ss [mult_def]); 1114 1115val COM_UNARY_MINUS = store_thm("COM_UNARY_MINUS",``!a. num (~a) = unary_minus (num a)``,RW_TAC std_ss [unary_minus_def,COMPLEX_NEG_def]); 1116 1117val COM_SUB = store_thm("COM_SUB",``num (a - b) = add (num a) (unary_minus (num b))``, 1118 RW_TAC std_ss [unary_minus_def,add_def,com_0_def] THEN 1119 Cases_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [COMPLEX_ADD_def,COMPLEX_SUB_def,rat_0_def,GSYM rat_0,RAT_SUB_LID,RAT_LSUB_EQ] THEN 1120 METIS_TAC [RAT_ADD_COMM,RAT_ADD_ASSOC,RAT_ADD_RINV,RAT_ADD_RID]); 1121 1122val COM_DIV = store_thm("COM_DIV",``!a b. ~(b = com_0) ==> (num (a / b) = mult (num a) (reciprocal (num b)))``, 1123 RW_TAC std_ss [mult_def,reciprocal_def,COMPLEX_DIV_def]); 1124 1125val COM_EQUAL = store_thm("COM_EQUAL",``bool (a = b) = equal (num a) (num b)``, 1126 Cases_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [bool_def,equal_def,TRUTH_REWRITES,complex_rational_11]); 1127 1128val FIX_NUM = store_thm("FIX_NUM",``(!a. fix (num a) = num a) /\ (!a. fix (rat a) = rat a) /\ (!a. fix (int a) = int a) /\ (!a. fix (nat a) = nat a)``, 1129 RW_TAC std_ss [fix_def,ACL2_NUMBERP_NUM,ite_def,TRUTH_REWRITES,rat_def,int_def,nat_def,cpx_def]); 1130 1131val NAT_NFIX = store_thm("NAT_NFIX",``nfix (nat a) = nat a``, 1132 RW_TAC std_ss [nfix_def,ite_def,TRUTH_REWRITES,nat_def,ANDL_REWRITE,INTEGERP_INT,GSYM INT_LT,GSYM BOOL_NOT] THEN 1133 METIS_TAC [INT_POS,INT_NOT_LT]); 1134 1135val INT_IFIX = store_thm("INT_IFIX",``ifix (int a) = int a``,RW_TAC std_ss [ifix_def,ite_def,TRUTH_REWRITES,INTEGERP_INT]); 1136 1137(*****************************************************************************) 1138(* Pair theorems: *) 1139(*****************************************************************************) 1140 1141val PAIR_FST = store_thm("PAIR_FST", 1142 ``f (FST x) = car (pair f g x)``, 1143 RW_TAC std_ss [pairTheory.FST,pair_def,car_def]); 1144 1145val PAIR_SND = store_thm("PAIR_SND", 1146 ``g (SND x) = cdr (pair f g x)``, 1147 RW_TAC std_ss [pairTheory.SND,pair_def,cdr_def]); 1148 1149val PAIR_CASE = store_thm("PAIR_CASE", 1150 ``f (pair_case g x) = f ((\(a,b). g a b) x)``, 1151 Cases_on `x` THEN REWRITE_TAC [TypeBase.case_def_of ``:'a # 'b``] THEN 1152 pairLib.GEN_BETA_TAC THEN REWRITE_TAC []); 1153 1154(*****************************************************************************) 1155(* List theorems: *) 1156(*****************************************************************************) 1157 1158val LIST_HD = store_thm("LIST_HD", 1159 ``(?a b. l = a::b) ==> (encode (HD l) = car (list encode l))``, 1160 Induct_on `l` THEN RW_TAC std_ss [list_def,HD,car_def]); 1161 1162val LIST_TL = store_thm("LIST_TL", 1163 ``(?a b. l = a :: b) ==> (list encode (TL l) = cdr (list encode l))``, 1164 Induct_on `l` THEN RW_TAC std_ss [list_def,TL,cdr_def]); 1165 1166val LIST_NULL = store_thm("LIST_NULL", 1167 ``!l. bool (NULL l) = atom (list f l)``, 1168 Cases THEN 1169 RW_TAC arith_ss [bool_def,hol_defaxiomsTheory.atom_def,list_def,NULL, 1170 TRUTH_REWRITES,hol_defaxiomsTheory.not_def,consp_def]); 1171 1172val LIST_LENGTH = store_thm("LIST_LENGTH", 1173 ``nat (LENGTH l) = len (list f l)``, 1174 Induct_on `l` THEN ONCE_REWRITE_TAC [len_def] THEN 1175 RW_TAC std_ss [LENGTH,list_def,consp_def,ite_def, 1176 TRUTH_REWRITES,NAT_SUC,cdr_def] THEN 1177 POP_ASSUM (SUBST_ALL_TAC o GSYM) THEN 1178 RW_TAC arith_ss [GSYM NAT_ADD]); 1179 1180(*****************************************************************************) 1181(* String theorems: *) 1182(*****************************************************************************) 1183 1184val list_rewrite = prove(``list_to_sexp = list``,REWRITE_TAC [FUN_EQ_THM] THEN GEN_TAC THEN Induct THEN METIS_TAC [list_def,list_to_sexp_def]); 1185 1186val STRING_EXPLODE = store_thm("STRING_EXPLODE",``list chr (EXPLODE s) = coerce (str s) (sym "COMMON-LISP" "LIST")``, 1187 RW_TAC std_ss [coerce_def,coerce_string_to_list_def,list_rewrite]); 1188 1189val STRING_IMPLODE = store_thm("STRING_IMPLODE",``str (IMPLODE l) = coerce (list chr l) (sym "COMMON-LISP" "STRING")``, 1190 Induct_on `l` THEN RW_TAC std_ss [coerce_def,coerce_list_to_string_def,list_rewrite,list_def, 1191 nil_def,stringTheory.IMPLODE_EQNS,make_character_list_def] THEN 1192 Cases_on `list chr l` THEN POP_ASSUM MP_TAC THEN Cases_on `l` THEN 1193 REPEAT (RW_TAC std_ss [coerce_def,list_def,nil_def,stringTheory.IMPLODE_EQNS, 1194 make_character_list_def,coerce_list_to_string_def] THEN REPEAT (POP_ASSUM MP_TAC))); 1195 1196val coerce_rewrite = CONJ (GSYM STRING_EXPLODE) (GSYM STRING_IMPLODE); 1197 1198val STRING_LENGTH = store_thm("STRING_LENGTH",``nat (STRLEN s) = length (str s)``, 1199 RW_TAC std_ss [stringp_def,ite_def,TRUTH_REWRITES,length_def,coerce_def,coerce_string_to_list_def, 1200 stringTheory.STRLEN_THM,GSYM LIST_LENGTH,list_rewrite,csym_def,COMMON_LISP_def, 1201 GSYM stringTheory.STRLEN_EXPLODE_THM]); 1202 1203 1204(*****************************************************************************) 1205(* Case theorems *) 1206(*****************************************************************************) 1207 1208val NUM_CONSTRUCT = store_thm("NUM_CONSTRUCT", 1209 ``!a. bool (?d. a = SUC d) = bool (0 < a)``, 1210 Cases THEN RW_TAC arith_ss []); 1211 1212val NUM_CASE = store_thm("NUM_CASE", 1213 ``!X a b. f (num_case a b X) = 1214 f (if X = 0 then a else b (PRE X))``, 1215 Cases THEN REWRITE_TAC [TypeBase.case_def_of ``:num``] THEN 1216 RW_TAC arith_ss []); 1217 1218val LIST_CASE = store_thm("LIST_CASE", 1219 ``!l. f (list_case n c l) = 1220 f (if (l = []) then n else c (HD l) (TL l))``, 1221 Cases THEN RW_TAC arith_ss [NULL,HD,TL]); 1222 1223val LIST_CONSTRUCT1 = store_thm("LIST_CONSTRUCT1", 1224 ``!l. bool (l = []) = bool (NULL l)``, 1225 Cases THEN REWRITE_TAC [NULL,GSYM (TypeBase.distinct_of ``:'a list``)]); 1226 1227val LIST_CONSTRUCT2 = store_thm("LIST_CONSTRUCT2", 1228 ``!l. bool (?a b. l = a::b) = bool (~NULL l)``, 1229 Cases THEN REWRITE_TAC [NULL] THEN 1230 AP_TERM_TAC THEN EQ_TAC THEN METIS_TAC [TypeBase.distinct_of ``:'a list``]); 1231 1232(*****************************************************************************) 1233(* Comparison theorems: *) 1234(*****************************************************************************) 1235 1236(* LT, LE, GT, GE *) 1237 1238val NAT_LT = store_thm("NAT_LT",``!a b. bool (a < b) = less (nat a) (nat b)``, 1239 RW_TAC int_ss [nat_def,GSYM INT_LT,bool_def]); 1240 1241val RAT_LT = store_thm("RAT_LT",``!a b. bool (a < b) = less (rat a) (rat b)``,RW_TAC std_ss [bool_def,less_def,rat_def,RAT_LES_REF]); 1242 1243val COM_LT = store_thm("COM_LT",``bool (a < b) = less (num a) (num b)``, 1244 Cases_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [bool_def,less_def,TRUTH_REWRITES,COMPLEX_LT_def]); 1245 1246 1247val COM_NOT_LT = store_thm("COM_NOT_LT",``!a b. ~(a < b) = b <= a:complex_rational``, 1248 Cases_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [COMPLEX_LT_def,COMPLEX_LE_def,RAT_LEQ_LES,rat_leq_def] THEN METIS_TAC [RAT_LES_IMP_NEQ]); 1249 1250val NAT_LE = store_thm("NAT_LE",``bool (a <= b) = not (less (nat b) (nat a))``,RW_TAC std_ss [bool_def,TRUTH_REWRITES,not_def,ite_def,GSYM NAT_LT,NOT_LESS]); 1251 1252val INT_LE = store_thm("INT_LE",``bool (a <= b) = not (less (int b) (int a))``,RW_TAC int_ss [bool_def,TRUTH_REWRITES,not_def,ite_def,GSYM INT_LT,INT_NOT_LT]); 1253 1254val RAT_LE = store_thm("RAT_LE",``bool (a <= b) = not (less (rat b) (rat a))``,RW_TAC std_ss [bool_def,TRUTH_REWRITES,not_def,ite_def,GSYM RAT_LT,RAT_LEQ_LES]); 1255 1256val COM_LE = store_thm("COM_LE",``bool (a <= b) = not (less (num b) (num a))``,RW_TAC std_ss [bool_def,TRUTH_REWRITES,not_def,ite_def,GSYM COM_LT,COM_NOT_LT]); 1257 1258 1259val NAT_GE = store_thm("NAT_GE",``bool (a >= b) = bool (b <= a:num)``,AP_TERM_TAC THEN DECIDE_TAC); 1260val INT_GE = store_thm("INT_GE",``bool (a >= b) = bool (b <= a:int)``,AP_TERM_TAC THEN ARITH_TAC); 1261val RAT_GE = store_thm("RAT_GE",``bool (a >= b) = bool (b <= a:rat)``,REWRITE_TAC [rat_geq_def]); 1262val COM_GE = store_thm("COM_GE",``bool (a >= b) = bool (b <= a:complex_rational)``, 1263 AP_TERM_TAC THEN Cases_on `a` THEN Cases_on `b` THEN 1264 REWRITE_TAC [COMPLEX_LE_def,COMPLEX_GE_def,rat_gre_def,rat_geq_def] THEN 1265 EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []); 1266 1267val NAT_GT = store_thm("NAT_GT",``bool (a > b) = bool (b < a:num)``,AP_TERM_TAC THEN DECIDE_TAC); 1268val INT_GT = store_thm("INT_GT",``bool (a > b) = bool (b < a:int)``,AP_TERM_TAC THEN ARITH_TAC); 1269val RAT_GT = store_thm("RAT_GT",``bool (a > b) = bool (b < a:rat)``,REWRITE_TAC [rat_gre_def]); 1270val COM_GT = store_thm("COM_GT",``bool (a > b) = bool (b < a:complex_rational)``, 1271 AP_TERM_TAC THEN Cases_on `a` THEN Cases_on `b` THEN 1272 REWRITE_TAC [COMPLEX_LT_def,COMPLEX_GT_def,rat_gre_def,rat_geq_def] THEN 1273 EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []); 1274 1275(*****************************************************************************) 1276(* Subtraction theorems: *) 1277(*****************************************************************************) 1278 1279val INT_SUB = store_thm("INT_SUB",``!a b. int (a - b) = add (int a) (unary_minus (int b))``, 1280 RW_TAC int_ss [GSYM INT_ADD,GSYM INT_UNARY_MINUS,int_sub]); 1281 1282val NAT_SUB = store_thm("NAT_SUB", 1283 ``!a b. nat (a - b) = nfix (add (nat a) (unary_minus (nat b)))``, 1284 RW_TAC int_ss [nat_def,GSYM INT_SUB,nfix_def,ite_def,TRUTH_REWRITES, 1285 natp_def,INTEGERP_INT,GSYM INT_EQUAL, 1286 GSYM INT_LT,INT_CONG,GSYM BOOL_NOT,ANDL_REWRITE] THEN 1287 FULL_SIMP_TAC int_ss [INT_NOT_LT,INT_LE_SUB_RADD,INT_LT_SUB_LADD, 1288 integerTheory.INT_SUB,INT_LE_SUB_LADD,INT_LT_SUB_RADD] ); 1289 1290val RAT_SUB = store_thm("RAT_SUB",``rat (a - b) = add (rat a) (unary_minus (rat b))``, 1291 RW_TAC std_ss [rat_sub_def,frac_sub_def,GSYM RAT_ADD,GSYM RAT_UNARY_MINUS,rat_ainv_def,rat_add_def,frac_ainv_def,RAT_ADD_CONG]); 1292val COM_SUB = store_thm("COM_SUB",``num (a - b) = add (num a) (unary_minus (num b))``, 1293 Cases_on `a` THEN Cases_on `b` THEN RW_TAC std_ss [COMPLEX_SUB_def,GSYM COM_UNARY_MINUS,GSYM COM_ADD, 1294 COMPLEX_NEG_def,COMPLEX_ADD_def,com_0_def,RAT_SUB_LID,rat_0_def,GSYM rat_0,RAT_SUB_ADDAINV]); 1295 1296val NAT_SUB_COND = store_thm("NAT_SUB_COND",``!a b. b <= a ==> (nat (a - b) = add (nat a) (unary_minus (nat b)))``, 1297 RW_TAC int_ss [nat_def,GSYM INT_SUB,nfix_def,ite_def,TRUTH_REWRITES,natp_def,INTEGERP_INT,GSYM INT_EQUAL,GSYM INT_LT,INT_CONG] THEN 1298 FULL_SIMP_TAC int_ss [INT_NOT_LT,INT_LE_SUB_RADD,INT_LT_SUB_LADD,integerTheory.INT_SUB] THEN FULL_SIMP_TAC int_ss [INT_EQ_SUB_LADD]); 1299 1300val MK_THMS = LIST_CONJ o (map GEN_ALL); 1301 1302(*****************************************************************************) 1303(* Natural number judgement theorems: *) 1304(*****************************************************************************) 1305 1306val NATP_ADD = store_thm("NATP_ADD", 1307 ``!a b. (|= natp a) /\ (|= natp b) ==> |= natp (add a b)``, 1308 REPEAT STRIP_TAC THEN CHOOSEP_TAC THEN 1309 RW_TAC std_ss [GSYM NAT_ADD,NATP_NAT]); 1310 1311val NATP_MULT = store_thm("NATP_MULT", 1312 ``!a b. (|= natp a) /\ (|= natp b) ==> |= natp (mult a b)``, 1313 REPEAT STRIP_TAC THEN CHOOSEP_TAC THEN 1314 RW_TAC std_ss [GSYM NAT_MULT,NATP_NAT]); 1315 1316val NATP_PRE = store_thm("NATP_PRE", 1317 ``!a. (|= natp a) ==> ~(a = nat 0) ==> 1318 |= natp (add a (unary_minus (nat 1)))``, 1319 REPEAT STRIP_TAC THEN CHOOSEP_TAC THEN 1320 FULL_SIMP_TAC int_ss [nat_def,GSYM INT_ADD,GSYM INT_UNARY_MINUS, 1321 INT_ADD_CALCULATE,natp_def,ANDL_REWRITE,INTEGERP_INT,GSYM INT_LT, 1322 not_def,TRUTH_REWRITES,ite_def,INT_CONG]); 1323 1324val NATP_SUB = store_thm("NATP_SUB", 1325 ``!a b. (|= natp a) /\ (|= natp b) /\ (|= not (less a b)) ==> 1326 |= natp (add a (unary_minus b))``, 1327 REPEAT STRIP_TAC THEN CHOOSEP_TAC THEN 1328 FULL_SIMP_TAC int_ss [nat_def,GSYM INT_ADD,GSYM INT_UNARY_MINUS, 1329 INT_ADD_CALCULATE,natp_def,ANDL_REWRITE,INTEGERP_INT,GSYM INT_LT, 1330 not_def,TRUTH_REWRITES,ite_def,INT_CONG]); 1331 1332val NATP_NFIX = store_thm("NATP_NFIX", 1333 ``!a. |= natp (nfix a)``, 1334 RW_TAC std_ss [natp_def,nfix_def,ite_def,TRUTH_REWRITES, 1335 ANDL_REWRITE,nat_def] THEN 1336 FULL_SIMP_TAC std_ss [INTEGERP_INT,GSYM INT_LT,GSYM INT_EQUAL, 1337 TRUTH_REWRITES] THEN 1338 CHOOSEP_TAC THEN 1339 FULL_SIMP_TAC std_ss [GSYM BOOL_NOT,INTEGERP_INT,GSYM INT_LT, 1340 GSYM INT_EQUAL,TRUTH_REWRITES] THEN 1341 ARITH_TAC); 1342 1343(*****************************************************************************) 1344(* Grouped theorems for export. *) 1345(*****************************************************************************) 1346 1347val NAT_THMS = save_thm("NAT_THMS", 1348 MK_THMS [NAT_EQUAL_0,NAT_EQUAL,NAT_0_LT,NAT_LT,NAT_LE,NAT_GE,NAT_GT, 1349 NAT_ADD,NAT_SUC_PRE,NAT_PRE,NAT_SUC,NAT_MULT,NAT_SUB]); 1350 1351val INT_THMS = save_thm("INT_THMS", 1352 MK_THMS [INT_EQUAL,INT_LT,INT_LE,INT_GE,INT_GT, 1353 INT_ADD,INT_MULT,INT_UNARY_MINUS,INT_SUB]); 1354 1355val RAT_THMS = save_thm("RAT_THMS", 1356 MK_THMS [RAT_EQUAL,RAT_LT,RAT_LE,RAT_GE,RAT_GT, 1357 RAT_ADD,RAT_MULT,RAT_UNARY_MINUS,RAT_DIV,RAT_SUB]); 1358 1359val COM_THMS = save_thm("COM_THMS", 1360 MK_THMS [COM_EQUAL,COM_LT,COM_LE,COM_GE,COM_GT, 1361 COM_ADD,COM_MULT,COM_UNARY_MINUS,COM_DIV,COM_SUB]); 1362 1363val BOOL_THMS = save_thm("BOOL_THMS", 1364 MK_THMS [BOOL_EQUALITY,BOOL_NOT,BOOL_T,BOOL_F]); 1365 1366val LIST_THMS = save_thm("LIST_THMS", 1367 MK_THMS [LIST_HD,LIST_TL,LIST_LENGTH]); 1368 1369val PAIR_THMS = save_thm("PAIR_THMS", 1370 MK_THMS [PAIR_FST,PAIR_SND]); 1371 1372val STRING_THMS = save_thm("STRING_THMS", 1373 MK_THMS [STRING_EXPLODE,STRING_IMPLODE,STRING_LENGTH]); 1374 1375val JUDGEMENT_THMS = save_thm("JUDGEMENT_THMS", 1376 MK_THMS [CONJUNCT1 ANDL_JUDGEMENT,CONJUNCT2 ANDL_JUDGEMENT, 1377 NATP_NAT,INTEGERP_INT,RATIONALP_RAT,ACL2_NUMBERP_NUM,BOOLEANP_BOOL, 1378 NATP_ADD,NATP_PRE,NATP_SUB,NATP_NFIX,NATP_MULT, 1379 BOOLEANP_IMPLIES,BOOLEANP_ANDL,BOOLEANP_ANDL_NULL, 1380 BOOLEANP_EQUAL,BOOLEANP_LESS,BOOLEANP_NOT,BOOLEANP_CONSP, 1381 BOOLEANP_IF, 1382 INTEGERP_ADD,INTEGERP_MULT,INTEGERP_UNARY_MINUS, 1383 RATIONALP_ADD,RATIONALP_MULT,RATIONALP_RECIPROCAL, 1384 RATIONALP_UNARY_MINUS, 1385 ACL2_NUMBERP_ADD,ACL2_NUMBERP_MULT,ACL2_NUMBERP_RECIPROCAL, 1386 ACL2_NUMBERP_UNARY_MINUS]); 1387 1388 1389val _ = export_theory(); 1390