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