1(*---------------------------------------------------------------------------*)
2(* Constant zero function.                                                   *)
3(*---------------------------------------------------------------------------*)
4
5set_trace "Unicode" 0;
6set_trace "pp_annotations" 0;
7
8use (HOLDIR^"/src/pfl/defchoose");
9use (HOLDIR^"/src/pfl/tactics.sml");
10
11quietdec := true;
12open arithmeticTheory optionTheory;
13quietdec := false;
14
15(*---------------------------------------------------------------------------*)
16(* General purpose support.                                                  *)
17(*---------------------------------------------------------------------------*)
18
19val MAX_LE_THM = Q.prove
20(`!m n. m <= MAX m n /\ n <= MAX m n`,
21 RW_TAC arith_ss [MAX_DEF]);
22
23val IS_SOME_EXISTS = Q.prove
24(`!x. IS_SOME x = ?y. x = SOME y`,
25 Cases THEN METIS_TAC [optionTheory.IS_SOME_DEF]);
26
27(*---------------------------------------------------------------------------*)
28(* Indexed function definition                                               *)
29(*---------------------------------------------------------------------------*)
30
31val izero_def =
32 Define
33  `izero d x =
34    if d=0 then NONE else
35    if x=0 then SOME 0
36     else case izero (d-1) (x-1)
37           of NONE -> NONE
38           || SOME n -> izero (d-1) n`;
39
40(*---------------------------------------------------------------------------*)
41(* Domain of the function.                                                   *)
42(*---------------------------------------------------------------------------*)
43
44val dom_def = Define `dom x = ?d. IS_SOME(izero d x)`;
45
46(*---------------------------------------------------------------------------*)
47(* Measure on recursion depth.                                               *)
48(*---------------------------------------------------------------------------*)
49
50val rdepth_thm =
51 MINCHOOSE ("rdepth_thm", "rdepth",
52            ``!x. ?d. IS_SOME (izero d x)``);
53
54(*---------------------------------------------------------------------------*)
55(* Define zero                                                               *)
56(*---------------------------------------------------------------------------*)
57
58val zero_0_def = Define `zero_0 x = THE (izero (rdepth x) x)`;
59
60(*---------------------------------------------------------------------------*)
61(* Lemmas about izero and definedness                                        *)
62(*---------------------------------------------------------------------------*)
63
64val IS_SOME_IZERO = Q.prove
65(`!d n. IS_SOME (izero d n) ==> d <> 0`,
66 Cases THEN RW_TAC std_ss [Once izero_def]);
67
68val IZERO_SOME = Q.prove
69(`!d n a. (izero d n = SOME a) ==> d <> 0`,
70 Cases THEN RW_TAC std_ss [Once izero_def]);
71
72val izero_dlem = Q.prove
73(`!d n. IS_SOME (izero d n) ==> (izero d n = izero (SUC d) n)`,
74 DLEM_TAC izero_def IZERO_SOME);
75
76val izero_monotone = Q.prove
77(`!d1 d2 n. IS_SOME(izero d1 n) /\ d1 <= d2 ==> (izero d1 n = izero d2 n)`,
78 RW_TAC arith_ss [LESS_EQ_EXISTS] THEN
79 Induct_on `p` THEN METIS_TAC [ADD_CLAUSES,izero_dlem]);
80
81val izero_norm = Q.prove
82(`!d n. IS_SOME(izero d n) ==> (izero d n = izero (rdepth n) n)`,
83 METIS_TAC [izero_monotone,rdepth_thm]);
84
85val izero_determ = Q.prove
86(`!d1 d2 n. IS_SOME(izero d1 n) /\ IS_SOME(izero d2 n)
87            ==> (izero d1 n = izero d2 n)`,
88 METIS_TAC [izero_norm]);
89
90(*---------------------------------------------------------------------------*)
91(* Recursion equations for zero                                              *)
92(*---------------------------------------------------------------------------*)
93
94val zero_base = Q.prove
95(`!n. dom n /\ (n=0) ==> (zero_0 n = 0)`,
96 RW_TAC std_ss [zero_0_def,dom_def] THEN
97 `rdepth 0 <> 0` by METIS_TAC [IS_SOME_IZERO,rdepth_thm] THEN
98 RW_TAC arith_ss [Once izero_def]);
99
100val zero_step = Q.prove
101(`!n. dom n /\ n<>0 ==> (zero_0 n = zero_0 (zero_0 (n-1)))`,
102 RW_TAC std_ss [zero_0_def,dom_def] THEN
103 `d <> 0` by METIS_TAC [IS_SOME_IZERO] THEN
104 `izero d n = case izero (d-1) (n-1) of
105                NONE -> NONE
106             || SOME v -> izero (d - 1) v` by METIS_TAC [izero_def] THEN
107 POP_ASSUM MP_TAC THEN CASE_TAC THEN
108 METIS_TAC [IS_SOME_EXISTS,NOT_SOME_NONE,THE_DEF,izero_norm]);
109
110(*---------------------------------------------------------------------------*)
111(* Equational characterization of zero.                                       *)
112(*---------------------------------------------------------------------------*)
113
114val zero_0_eqns = Q.prove
115(`!n. dom n ==> (zero_0 n = if n=0 then 0 else zero_0(zero_0(n-1)))`,
116 METIS_TAC [zero_base, zero_step]);
117
118(*---------------------------------------------------------------------------*)
119(* Now derive eqns for dom                                                   *)
120(*---------------------------------------------------------------------------*)
121
122val lem = Q.prove
123(`IS_SOME (izero 1 0)`,
124 RW_TAC arith_ss [Once izero_def]);
125
126val dom_base_case = Q.prove
127(`dom 0`,
128 METIS_TAC [dom_def, lem]);
129
130val step2_lem1a = Q.prove
131(`!n. n<>0 /\ dom n ==> dom (n-1)`,
132 RW_TAC std_ss [dom_def] THEN
133 `d<>0` by METIS_TAC [IS_SOME_IZERO] THEN
134 Q.EXISTS_TAC `d-1` THEN
135 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [izero_def]) THEN
136 CASE_TAC THEN RW_TAC arith_ss []);
137
138val step2_lem1b = Q.prove
139(`!n. n<>0 /\ dom n ==> dom (zero_0(n-1))`,
140 RW_TAC std_ss [dom_def,zero_0_def] THEN
141 `d<>0` by METIS_TAC [IS_SOME_IZERO] THEN
142 Q.EXISTS_TAC `d-1` THEN
143 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [izero_def]) THEN
144 CASE_TAC THEN RW_TAC arith_ss [] THEN
145 METIS_TAC [izero_norm,IS_SOME_EXISTS,THE_DEF]);
146
147val step2_lem2 = Q.prove
148(`!n. n<>0 /\ dom (n-1) /\ dom (zero_0(n-1)) ==> dom n`,
149 RW_TAC std_ss [dom_def,zero_0_def] THEN
150 Q.EXISTS_TAC `SUC (MAX d d')` THEN
151 RW_TAC arith_ss [Once izero_def] THEN
152 CASE_TAC THENL
153 [METIS_TAC [izero_monotone,MAX_LE_THM,NOT_SOME_NONE],
154  METIS_TAC [izero_monotone,IS_SOME_EXISTS,MAX_LE_THM,izero_norm,THE_DEF]]);
155
156(*---------------------------------------------------------------------------*)
157(* Equational characterization of dom.                                       *)
158(*---------------------------------------------------------------------------*)
159
160val dom_eqns = Q.prove
161(`dom n =
162    if n=0 then T
163    else dom (n-1) /\ dom (zero_0 (n-1))`,
164 METIS_TAC [dom_base_case, step2_lem1a,step2_lem1b,step2_lem2]);
165
166(*---------------------------------------------------------------------------*)
167(* Now prove induction theorem. This is based on using rdepth as a measure   *)
168(* on the recursion. Thus we first have some lemmas about how rdepth         *)
169(* decreases in recursive calls.                                             *)
170(*---------------------------------------------------------------------------*)
171
172val inner_lt = Q.prove
173(`!n. dom n /\ n<>0 ==> rdepth (n-1) < rdepth n`,
174 RW_TAC std_ss [dom_def] THEN IMP_RES_TAC rdepth_thm THEN
175   `rdepth n <> 0` by METIS_TAC [IS_SOME_IZERO] THEN
176   `rdepth n - 1 < rdepth n` by DECIDE_TAC THEN
177   `IS_SOME (izero (rdepth n - 1) (n-1))`
178     by (Q.PAT_ASSUM `IS_SOME (izero (rdepth n) n)` MP_TAC THEN
179         SIMP_TAC arith_ss [Once izero_def] THEN CASE_TAC THEN
180         SIMP_TAC std_ss [IS_SOME_DEF]) THEN
181   `rdepth (n-1) <= rdepth n - 1` by METIS_TAC [rdepth_thm] THEN
182 DECIDE_TAC);
183
184val outer_lt = Q.prove
185(`!n. dom n /\ n<>0 ==> rdepth (zero_0 (n-1)) < rdepth n`,
186 RW_TAC std_ss [dom_def] >> IMP_RES_TAC rdepth_thm >>
187   `rdepth n <> 0` by METIS_TAC [IS_SOME_IZERO] >>
188   `rdepth n - 1 < rdepth n` by DECIDE_TAC >>
189   `IS_SOME (izero (rdepth n - 1) (zero_0 (n-1)))`
190     by (Q.PAT_ASSUM `IS_SOME (izero (rdepth n) n)` MP_TAC >>
191         SIMP_TAC arith_ss [Once izero_def] >> CASE_TAC >>
192         RW_TAC std_ss [zero_0_def] >>
193        `IS_SOME (izero (rdepth n - 1) (n-1))` by METIS_TAC [IS_SOME_EXISTS] >>
194        `IS_SOME (izero (rdepth (n-1)) (n-1))` by METIS_TAC [rdepth_thm] >>
195        METIS_TAC [izero_determ,THE_DEF]) >>
196   `rdepth (zero_0(n-1)) <= rdepth n - 1` by METIS_TAC [rdepth_thm] >>
197 DECIDE_TAC);
198
199(*---------------------------------------------------------------------------*)
200(* Induction for f91 is obtained by instantiating the well-founded induction *)
201(* theorem with the rdepth measure and then simplifying.                     *)
202(*---------------------------------------------------------------------------*)
203
204val ind0 = MATCH_MP relationTheory.WF_INDUCTION_THM
205                    (Q.ISPEC `rdepth` prim_recTheory.WF_measure);
206val ind1 = SIMP_RULE std_ss [prim_recTheory.measure_thm] ind0;
207val ind2 = SIMP_RULE std_ss [pairTheory.FORALL_PROD]
208                    (Q.ISPEC `\n. dom n ==> P n` ind1);
209
210val zero_0_ind = Q.prove
211(`!P.
212   (!n. dom n /\
213          (n<>0 ==> P (n-1))  /\
214          (n<>0 ==> P (zero_0 (n-1)))
215         ==> P n)
216  ==> !n. dom n ==> P n`,
217 GEN_TAC THEN DISCH_TAC THEN HO_MATCH_MP_TAC ind2 THEN
218 POP_ASSUM (fn th => REPEAT STRIP_TAC THEN MATCH_MP_TAC th) THEN
219 RULE_ASSUM_TAC (REWRITE_RULE [AND_IMP_INTRO]) THEN
220 METIS_TAC [inner_lt,outer_lt,dom_eqns]);
221
222(*---------------------------------------------------------------------------*)
223(* Trivial examples                                                          *)
224(*---------------------------------------------------------------------------*)
225
226val closed_form = Q.prove
227(`!n. dom n ==> (zero_0 n = 0)`,
228 HO_MATCH_MP_TAC zero_0_ind THEN
229   REPEAT STRIP_TAC THEN
230   RW_TAC arith_ss [Once zero_0_eqns]);
231
232(*---------------------------------------------------------------------------*)
233(* Termination                                                               *)
234(*---------------------------------------------------------------------------*)
235
236val zero_total = Q.prove
237(`!n. dom n`,
238  Induct THEN
239    RW_TAC arith_ss [Once dom_eqns] THEN
240    METIS_TAC [closed_form,dom_eqns]);
241
242(*---------------------------------------------------------------------------*)
243(* Efficient executable version of zero                                      *)
244(*---------------------------------------------------------------------------*)
245
246val exec_def =
247 Define
248 `exec d n =
249    if d=0 then (if dom n then zero_0 n else ARB) else
250    if n=0 then 0
251       else exec (d-1) (exec (d-1) (n-1))`;
252
253val exec_equals_zero_0 = Q.prove
254(`!d n. dom n ==> (exec d n = zero_0 n)`,
255 Induct THEN RW_TAC std_ss [Once exec_def]
256 THEN METIS_TAC [zero_0_eqns,dom_eqns]);
257
258val BIG_def = Define `BIG = 1073741823`;
259
260(*---------------------------------------------------------------------------*)
261(* Final version                                                             *)
262(*---------------------------------------------------------------------------*)
263
264val zero_def =
265 Define
266   `zero n = if dom n then zero_0 n else exec BIG n`;
267
268(*---------------------------------------------------------------------------*)
269(* Theorem showing that exec BIG = zero in the domain of the function.       *)
270(*---------------------------------------------------------------------------*)
271
272val zero_exec = Q.prove
273(`zero n = exec BIG n`,
274 RW_TAC std_ss [zero_def,exec_equals_zero_0]);
275
276val zero_dom_eqns = Q.prove
277(`dom n <=> if n=0 then T else dom (n-1) /\ dom (zero(n-1))`,
278 METIS_TAC [dom_eqns,zero_def]);
279
280val zero_eqns = Q.prove
281(`dom n ==>
282   (zero n = if n=0 then 0 else zero (zero (n-1)))`,
283 RW_TAC std_ss [zero_def] THEN METIS_TAC [zero_0_eqns,dom_eqns]);
284
285val zero_ind = Q.prove
286(`!P.
287   (!n. dom n /\
288          (n<>0 ==> P (n-1))  /\
289          (n<>0 ==> P (zero (n-1)))
290         ==> P n)
291  ==> !n. dom n ==> P n`,
292 GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC zero_0_ind THEN
293 POP_ASSUM (fn th => REPEAT STRIP_TAC THEN MATCH_MP_TAC th) THEN
294 RW_TAC std_ss [zero_def] THEN METIS_TAC [zero_dom_eqns]);
295