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