1open HolKernel Parse boolLib boolTheory;
2
3infix THEN THENL;
4
5val _ = new_theory "num";
6
7val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false;
8
9(*---------------------------------------------------------------------------
10 * Define successor `SUC_REP:ind->ind` on ind.
11 *---------------------------------------------------------------------------*)
12
13val SUC_REP_DEF = new_specification
14   ("SUC_REP_DEF",["SUC_REP"], boolTheory.INFINITY_AX);
15
16
17val ZERO_REP_EXISTS = prove(
18  Term`?z. !y. ~(z = SUC_REP y)`,
19  Q.X_CHOOSE_THEN `zrep` ASSUME_TAC ((CONV_RULE NOT_FORALL_CONV o
20                                      REWRITE_RULE [ONTO_THM] o
21                                      CONJUNCT2) SUC_REP_DEF) THEN
22  POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN
23  Q.EXISTS_TAC `zrep` THEN POP_ASSUM ACCEPT_TAC);
24
25(*---------------------------------------------------------------------------
26 * `ZERO_REP:ind` represents `0:num`
27 *---------------------------------------------------------------------------*)
28
29val ZERO_REP_DEF = new_specification
30  ("ZERO_REP_DEF",["ZERO_REP"], ZERO_REP_EXISTS);
31
32
33(*---------------------------------------------------------------------------*)
34(* `IS_NUM:ind->bool` defines the subset of `:ind` used to represent         *)
35(* numbers.  It is the smallest subset containing `ZERO_REP` and closed      *)
36(* under `SUC_REP`.                                                          *)
37(*---------------------------------------------------------------------------*)
38
39val IS_NUM_REP = new_definition("IS_NUM_REP",
40     ���IS_NUM_REP m =
41      !P:ind->bool. (P ZERO_REP /\ (!n. P n ==> P(SUC_REP n))) ==> P m���);
42
43(*---------------------------------------------------------------------------
44 * Prove that there is a representation in :ind of at least one number.
45 *---------------------------------------------------------------------------*)
46
47val EXISTS_NUM_REP = TAC_PROOF(([],���?n. IS_NUM_REP n���),
48     PURE_REWRITE_TAC [IS_NUM_REP] THEN
49     EXISTS_TAC (���ZERO_REP���) THEN
50     REPEAT STRIP_TAC);
51
52(*---------------------------------------------------------------------------
53 * Make the type definition.
54 *---------------------------------------------------------------------------*)
55
56val num_TY_DEF = new_type_definition ("num", EXISTS_NUM_REP);
57
58val num_ISO_DEF = define_new_type_bijections
59                   {name = "num_ISO_DEF",
60                    ABS = "ABS_num",
61                    REP = "REP_num",
62                    tyax =  num_TY_DEF};
63
64val R_11   = prove_rep_fn_one_one num_ISO_DEF
65and R_ONTO = prove_rep_fn_onto    num_ISO_DEF
66and A_11   = prove_abs_fn_one_one num_ISO_DEF
67and A_ONTO = prove_abs_fn_onto    num_ISO_DEF;
68
69(*---------------------------------------------------------------------------
70 * Define ZERO.
71 *---------------------------------------------------------------------------*)
72
73val zero = mk_var("0", mk_thy_type{Tyop="num",Thy="num",Args=[]});
74
75val ZERO_DEF = new_definition("ZERO_DEF", ���^zero = ABS_num ZERO_REP���);
76
77
78(*---------------------------------------------------------------------------
79 * Define the successor function on num.
80 *---------------------------------------------------------------------------*)
81
82val SUC_DEF = new_definition("SUC_DEF",
83 ���SUC m = ABS_num(SUC_REP(REP_num m))���);
84
85local open OpenTheoryMap in
86val ns = ["Number","Natural"]
87val _ = OpenTheory_tyop_name{tyop={Thy="num",Tyop="num"},name=(ns,"natural")}
88val _ = OpenTheory_const_name{const={Thy="num",Name="0"},name=(ns,"zero")}
89val _ = OpenTheory_const_name{const={Thy="num",Name="SUC"},name=(ns,"suc")}
90end
91
92(*---------------------------------------------------------------------------
93 * Prove that IS_NUM_REP ZERO_REP.
94 *---------------------------------------------------------------------------*)
95
96val IS_NUM_REP_ZERO =
97    TAC_PROOF
98    (([], ���IS_NUM_REP ZERO_REP���),
99     REWRITE_TAC [IS_NUM_REP] THEN REPEAT STRIP_TAC);
100
101(*---------------------------------------------------------------------------
102 * Prove that IS_NUM_REP (SUC_REP x).
103 *---------------------------------------------------------------------------*)
104
105val IS_NUM_SUC_REP =
106    TAC_PROOF
107    (([], ���!i. IS_NUM_REP i ==> IS_NUM_REP (SUC_REP i)���),
108     REWRITE_TAC [IS_NUM_REP] THEN
109     REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC);
110
111val IS_NUM_REP_SUC_REP =
112    TAC_PROOF
113    (([], ���!n. IS_NUM_REP(SUC_REP(REP_num n))���),
114      GEN_TAC THEN MATCH_MP_TAC IS_NUM_SUC_REP THEN
115      REWRITE_TAC [R_ONTO] THEN
116      EXISTS_TAC (���n:num���) THEN REFL_TAC);
117
118(*---------------------------------------------------------------------------
119 * |- !x1 x2. (SUC_REP x1 = SUC_REP x2) ==> (x1 = x2)
120 *---------------------------------------------------------------------------*)
121
122val SUC_REP_11 = CONJUNCT1 (REWRITE_RULE [ONE_ONE_THM] SUC_REP_DEF);
123
124(*---------------------------------------------------------------------------
125 *  |- !x. ~(SUC_REP x = ZERO_REP)
126 *---------------------------------------------------------------------------*)
127
128val NOT_SUC_ZERO = GSYM ZERO_REP_DEF;
129
130(*----------------------------------------------------------------------*)
131(* Proof of NOT_SUC : |- !n. ~(SUC n = ZERO)                            *)
132(* ---------------------------------------------------------------------*)
133
134val NOT_SUC = store_thm("NOT_SUC",
135    ���!n. ~(SUC n = 0)���,
136     PURE_REWRITE_TAC [SUC_DEF,ZERO_DEF] THEN GEN_TAC THEN
137     MP_TAC (SPECL [���SUC_REP(REP_num n)���,���ZERO_REP���] A_11) THEN
138     REWRITE_TAC [IS_NUM_REP_ZERO,IS_NUM_REP_SUC_REP] THEN
139     DISCH_THEN SUBST1_TAC THEN
140     MATCH_ACCEPT_TAC NOT_SUC_ZERO);
141
142(* ---------------------------------------------------------------------*)
143(* Prove that |-  !m n. (SUC m = SUC n) ==> (m = n)                     *)
144(* ---------------------------------------------------------------------*)
145
146val INV_SUC = store_thm("INV_SUC",
147    ���!m n. (SUC m = SUC n) ==> (m = n)���,
148     REPEAT GEN_TAC THEN REWRITE_TAC [SUC_DEF] THEN
149     MP_TAC (SPECL [���SUC_REP(REP_num m)���,
150                    ���SUC_REP(REP_num n)���] A_11) THEN
151     REWRITE_TAC [IS_NUM_REP_SUC_REP] THEN DISCH_THEN SUBST1_TAC THEN
152     DISCH_THEN (MP_TAC o MATCH_MP SUC_REP_11) THEN
153     REWRITE_TAC [R_11]);
154
155(* ---------------------------------------------------------------------*)
156(* Prove induction theorem.                                             *)
157(* ---------------------------------------------------------------------*)
158
159val ind_lemma1 =
160    TAC_PROOF
161    (([], ���!P. P ZERO_REP /\ (!i. P i ==> P(SUC_REP i))
162                 ==>
163              !i. IS_NUM_REP i ==> P i���),
164     PURE_ONCE_REWRITE_TAC [IS_NUM_REP] THEN
165     REPEAT STRIP_TAC THEN RES_TAC);
166
167val lemma =
168    TAC_PROOF(([], ���(A ==> (A /\ B)) = (A ==> B)���),
169               ASM_CASES_TAC (���A:bool���) THEN ASM_REWRITE_TAC []);
170
171val ind_lemma2 = TAC_PROOF(([],
172  ���!P. P ZERO_REP /\ (!i. IS_NUM_REP i /\ P i ==> P(SUC_REP i))
173           ==>
174         !i. IS_NUM_REP i ==> P i���),
175     GEN_TAC THEN STRIP_TAC THEN
176     MP_TAC (SPEC ���\i. IS_NUM_REP i /\ P i��� ind_lemma1) THEN
177     CONV_TAC(DEPTH_CONV BETA_CONV) THEN
178     REWRITE_TAC [lemma] THEN DISCH_THEN MATCH_MP_TAC THEN
179     ASM_REWRITE_TAC [IS_NUM_REP_ZERO] THEN
180     REPEAT STRIP_TAC THEN IMP_RES_TAC IS_NUM_SUC_REP THEN
181     RES_TAC);
182
183val lemma1 =
184    TAC_PROOF
185    (([], ���(!i. IS_NUM_REP i ==> P(ABS_num i)) = (!n. P n)���),
186     EQ_TAC THEN REPEAT STRIP_TAC THENL
187     [STRIP_ASSUME_TAC (SPEC (���n:num���) A_ONTO) THEN
188      RES_TAC THEN ASM_REWRITE_TAC [],
189      POP_ASSUM MP_TAC THEN REWRITE_TAC [R_ONTO] THEN
190      STRIP_GOAL_THEN (STRIP_THM_THEN SUBST1_TAC) THEN
191      ASM_REWRITE_TAC []]);
192
193val INDUCTION = store_thm("INDUCTION",
194    ���!P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n���,
195     GEN_TAC THEN STRIP_TAC THEN
196     MP_TAC (SPEC ���\i. ((P(ABS_num i)):bool)��� ind_lemma2) THEN
197     CONV_TAC(DEPTH_CONV BETA_CONV) THEN
198     REWRITE_TAC [SYM ZERO_DEF,lemma1] THEN
199     DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL
200     [FIRST_ASSUM ACCEPT_TAC,
201      REWRITE_TAC [R_ONTO] THEN
202      GEN_TAC THEN  CONV_TAC ANTE_CONJ_CONV THEN
203      DISCH_THEN (STRIP_THM_THEN SUBST1_TAC) THEN
204      ASM_REWRITE_TAC [num_ISO_DEF,SYM (SPEC_ALL SUC_DEF)]]);
205
206val _ = export_theory();
207