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