1(*****************************************************************************) 2(* HOL proofs of defthms in defaxioms.lisp.trans. *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* Ignore everything up to "END BOILERPLATE" *) 7(*****************************************************************************) 8 9(*****************************************************************************) 10(* START BOILERPLATE NEEDED FOR COMPILATION *) 11(*****************************************************************************) 12 13(****************************************************************************** 14* Load theories 15******************************************************************************) 16(* The commented out stuff below should be loaded in interactive sessions 17quietdec := true; 18map 19 load 20 ["stringLib","complex_rationalTheory","gcdTheory", 21 "sexp","sexpTheory","hol_defaxiomsTheory"]; 22open stringLib complex_rationalTheory gcdTheory 23 sexp sexpTheory hol_defaxiomsTheory; 24Globals.checking_const_names := false; 25quietdec := false; 26*) 27 28(****************************************************************************** 29* Boilerplate needed for compilation: open HOL4 systems modules. 30******************************************************************************) 31open HolKernel Parse boolLib bossLib; 32 33(****************************************************************************** 34* Open theories (including ratTheory from Jens Brandt). 35******************************************************************************) 36open stringLib complex_rationalTheory gcdTheory 37 sexp sexpTheory hol_defaxiomsTheory; 38 39(*****************************************************************************) 40(* END BOILERPLATE *) 41(*****************************************************************************) 42 43val _ = new_theory "hol_defaxioms_thms"; 44 45 46(* 47 [oracles: DEFTHM ACL2::CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP] 48 [axioms: ] [] |- |= implies (character_listp x) (eqlable_listp x), 49*) 50 51val character_listp_forward_to_eqlable_listp_defthm = 52 store_thm 53 ("character_listp_forward_to_eqlable_listp_defaxiom", 54 ``|= implies (character_listp x) (eqlable_listp x)``, 55 SIMP_TAC arith_ss [implies] 56 THEN Induct_on `x` 57 THENL 58 [ACL2_SIMP_TAC [itel_def], 59 ACL2_SIMP_TAC [itel_def], 60 ACL2_SIMP_TAC [itel_def], 61 ACL2_SIMP_TAC [itel_def], 62 ONCE_REWRITE_TAC[character_listp_def,eqlable_listp_def] 63 THEN ACL2_SIMP_TAC [itel_def] 64 THEN FULL_SIMP_TAC arith_ss [GSYM ACL2_TRUE,GSYM nil_def] 65 THEN Cases_on `x` 66 THEN ACL2_FULL_SIMP_TAC [characterp_def]]); 67 68(* 69 [oracles: DEFTHM ACL2::STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP] 70 [axioms: ] [] |- |= implies (standard_char_listp x) (character_listp x), 71*) 72 73val standard_char_listp_forward_to_character_listp_defthm = 74 store_thm 75 ("standard_char_listp_forward_to_character_listp_defaxiom", 76 ``|= implies (standard_char_listp x) (character_listp x)``, 77 SIMP_TAC arith_ss [implies] 78 THEN Induct_on `x` 79 THEN ONCE_REWRITE_TAC[character_listp_def,standard_char_listp_def] 80 THENL 81 [ACL2_SIMP_TAC [], 82 ACL2_SIMP_TAC [], 83 ACL2_SIMP_TAC [], 84 ACL2_SIMP_TAC [], 85 ACL2_SIMP_TAC [] 86 THEN FULL_SIMP_TAC std_ss [GSYM nil_def,GSYM ACL2_TRUE]]); 87 88 89(* 90 [oracles: DEFAXIOM ACL2::CHARACTER-LISTP-COERCE, DISK_THM] [axioms: ] [] 91 |- |= character_listp (coerce acl2_str (csym "LIST")), 92*) 93 94val character_listp_list_to_sexp = 95 store_thm 96 ("character_listp_list_to_sexp", 97 ``!l. |= character_listp(list_to_sexp chr l)``, 98 Induct 99 THEN ACL2_SIMP_TAC[list_to_sexp_def] 100 THEN ACL2_FULL_SIMP_TAC[ACL2_TRUE,nil_def]); 101 102val character_listp_coerce_defaxiom = 103 store_thm 104 ("character_listp_coerce_defaxiom", 105 ``|= character_listp (coerce acl2_str (csym "LIST"))``, 106 Cases_on `acl2_str` 107 THEN ACL2_SIMP_TAC 108 [csym_def,COMMON_LISP_def,coerce_string_to_list_def, 109 coerce_list_to_string_def,list_to_sexp_def, 110 EVAL ``EXPLODE ""``,stringTheory.EXPLODE_EQNS, 111 make_character_list_def] 112 THEN PROVE_TAC[character_listp_list_to_sexp,nil_def,ACL2_TRUE]); 113 114val assoc_nil = 115 store_thm 116 ("assoc_nil", 117 ``assoc x nil = nil``, 118 CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[assoc_def])) 119 THEN ACL2_SIMP_TAC[itel_def]); 120 121val assoc_cons = 122 store_thm 123 ("assoc_cons", 124 ``assoc x (cons (cons x' y) l) = 125 if |= equal x x' then cons x' y else assoc x l``, 126 CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[assoc_def])) 127 THEN ACL2_SIMP_TAC[itel_def]); 128 129(* 130val lower_case_p_char_downcase_defaxiom = 131 store_thm 132 ("lower_case_p_char_downcase_defaxiom", 133 ``|= implies (andl [upper_case_p x; characterp x]) 134 (lower_case_p (char_downcase x))``, 135 REWRITE_TAC[implies] 136 THEN STRIP_TAC 137 THEN SIMP_TAC std_ss [char_downcase_def,assoc_cons,List_def] 138 THEN CONV_TAC(DEPTH_CONV(pairLib.let_CONV)) 139 THEN SIMP_TAC std_ss [itel_def,ite_def] 140 THEN ACL2_FULL_SIMP_TAC[assoc_cons,assoc_nil] 141 THEN REWRITE_TAC[COND_RAND] 142*) 143 144 145val _ = export_acl2_theory(); 146 147