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