1(*---------------------------------------------------------------------------*) 2(* Nested reverse via step-indexing. *) 3(*---------------------------------------------------------------------------*) 4 5open arithmeticTheory optionTheory listTheory; 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 rev_orig_tm = 29 ``(rev [] = []) /\ 30 (rev (x::xs) = 31 case rev xs 32 of [] => [x] 33 | y::ys => y :: rev (x::rev ys))``; 34 35val irev_def = 36 Define 37 `irev d list = 38 if d=0 then NONE else 39 case list 40 of [] => SOME [] 41 | (x::xs) => 42 case irev (d-1) xs 43 of NONE => NONE 44 | SOME [] => SOME [x] 45 | SOME (y::ys) => 46 case irev (d-1) ys 47 of NONE => NONE 48 | SOME v => 49 case irev (d-1) (x::v) 50 of NONE => NONE 51 | SOME v => SOME (y::v)`; 52 53(*---------------------------------------------------------------------------*) 54(* Domain of the function. *) 55(*---------------------------------------------------------------------------*) 56 57val dom_def = Define `dom list = ?d. IS_SOME(irev d list)`; 58 59(*---------------------------------------------------------------------------*) 60(* Create measure function rdepth *) 61(*---------------------------------------------------------------------------*) 62 63val rev_rdepth = 64 MINCHOOSE ("rev_rdepth", "rev_rdepth", ``!list. ?d. IS_SOME(irev d list)``); 65 66(*---------------------------------------------------------------------------*) 67(* Define rev *) 68(*---------------------------------------------------------------------------*) 69 70val rev_def = Define `rev list = THE (irev (rev_rdepth list) list)`; 71 72(*---------------------------------------------------------------------------*) 73(* Lemmas about definedness *) 74(*---------------------------------------------------------------------------*) 75 76val IS_SOME_IREV = Q.prove 77(`!d list. IS_SOME (irev d list) ==> d <> 0`, 78 Cases THEN RW_TAC std_ss [Once irev_def]); 79 80val IREV_SOME = Q.prove 81(`!d l a. (irev d l = SOME a) ==> d <> 0`, 82 METIS_TAC[IS_SOME_IREV,IS_SOME_EXISTS]); 83 84val irev_dlem = Q.prove 85(`!d l. IS_SOME (irev d l) ==> (irev d l = irev (SUC d) l)`, 86 DLEM_TAC irev_def IREV_SOME); 87 88val irev_monotone = Q.prove 89(`!d1 d2 l. IS_SOME(irev d1 l) /\ d1 <= d2 ==> (irev d1 l = irev d2 l)`, 90 RW_TAC arith_ss [LESS_EQ_EXISTS] THEN 91 Induct_on `p` THEN METIS_TAC [ADD_CLAUSES,irev_dlem]); 92 93val irev_norm = Q.prove 94(`!d l. IS_SOME(irev d l) ==> (irev d l = irev (rev_rdepth l) l)`, 95 METIS_TAC [irev_monotone,rev_rdepth]); 96 97val irev_determ = Q.prove 98(`!d1 d2 l. IS_SOME(irev d1 l) /\ IS_SOME(irev d2 l) 99 ==> (irev d1 l = irev d2 l)`, 100 METIS_TAC [irev_norm]); 101 102 103(*---------------------------------------------------------------------------*) 104(* Constrained recursion equations *) 105(*---------------------------------------------------------------------------*) 106 107val rev_base = Q.prove 108(`!list. dom list /\ (list = []) ==> (rev list = [])`, 109 RW_TAC std_ss [rev_def,dom_def] THEN 110 IMP_RES_TAC rev_rdepth THEN 111 `rev_rdepth [] <> 0` by METIS_TAC [IS_SOME_IREV] THEN 112 RW_TAC arith_ss [Once irev_def]); 113 114val rev_step = Q.prove 115(`!list x xs. dom list /\ (list=x::xs) ==> 116 (rev list = case rev xs 117 of [] => [x] 118 | y::ys => y :: rev (x::rev ys))`, 119 RW_TAC std_ss [rev_def,dom_def] THEN 120 `d<>0` by METIS_TAC [IS_SOME_IREV] THEN 121 `irev d (x::xs) = 122 case irev (d - 1) xs 123 of NONE => NONE 124 | SOME [] => SOME [x] 125 | SOME (y::ys) => 126 case irev (d - 1) ys 127 of NONE => NONE 128 | SOME v'' => 129 case irev (d - 1) (x::v'') 130 of NONE => NONE 131 | SOME v => SOME (y::v)` 132 by (GEN_REWRITE_TAC LHS_CONV bool_rewrites [irev_def] THEN 133 ASM_SIMP_TAC std_ss [list_case_def]) THEN 134 POP_ASSUM MP_TAC THEN REPEAT CASE_TAC THEN 135 METIS_TAC [rev_rdepth,irev_norm, 136 NOT_SOME_NONE,IS_SOME_EXISTS,THE_DEF,NOT_CONS_NIL,CONS_11]); 137 138(*---------------------------------------------------------------------------*) 139(* Equational characterization of rev. *) 140(*---------------------------------------------------------------------------*) 141 142val rev_eqns = Q.prove 143(`!list. dom list ==> 144 (rev list = 145 case list 146 of [] => [] 147 | x::xs => case rev xs 148 of [] => [x] 149 | h::t => h::rev (x::rev t))`, 150 Cases THEN RW_TAC std_ss [] THEN METIS_TAC [rev_base, rev_step]); 151 152 153(*---------------------------------------------------------------------------*) 154(* Now derive eqns for dom *) 155(*---------------------------------------------------------------------------*) 156 157val lem = Q.prove 158(`IS_SOME (irev 1 [])`, 159 RW_TAC arith_ss [Once irev_def]); 160 161val dom_base_case = Q.prove 162(`dom []`, 163 METIS_TAC [dom_def, lem]); 164 165val lem1a = Q.prove 166(`!x xs. dom (x::xs) ==> dom xs`, 167 RW_TAC std_ss [dom_def] THEN 168 `d<>0` by METIS_TAC [IS_SOME_IREV] THEN 169 Q.EXISTS_TAC `d-1` THEN 170 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [irev_def]) THEN 171 CASE_TAC THEN RW_TAC arith_ss []); 172 173val lem2a = Q.prove 174(`!x xs h t. dom (x::xs) /\ (rev xs = h::t) ==> dom t`, 175 RW_TAC std_ss [dom_def,rev_def] THEN 176 `d<>0` by METIS_TAC [IS_SOME_IREV] THEN 177 Q.EXISTS_TAC `d-1` THEN 178 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [irev_def]) THEN 179 CASE_TAC THEN RW_TAC arith_ss [] THEN 180 POP_ASSUM MP_TAC THEN CASE_TAC THEN RW_TAC arith_ss [] THEN 181 `x = h::t` by METIS_TAC [IS_SOME_EXISTS,irev_norm,SOME_11,THE_DEF] THEN 182 RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN CASE_TAC THEN 183 RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN CASE_TAC THEN RW_TAC arith_ss []); 184 185val lem2b = Q.prove 186(`!x xs h t. dom (x::xs) /\ (rev xs = h::t) ==> dom (x::rev t)`, 187RW_TAC std_ss [dom_def,rev_def] THEN 188 `d<>0` by METIS_TAC [IS_SOME_IREV] THEN 189 Q.EXISTS_TAC `d-1` THEN 190 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [irev_def]) THEN 191 CASE_TAC THEN RW_TAC arith_ss [] THEN 192 POP_ASSUM MP_TAC THEN CASE_TAC THEN RW_TAC arith_ss [] THEN 193 `x = h::t` by METIS_TAC [IS_SOME_EXISTS,irev_norm,SOME_11,THE_DEF] THEN 194 RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN CASE_TAC THEN 195 RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN CASE_TAC THEN 196 RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN CASE_TAC THEN 197 METIS_TAC [irev_norm,IS_SOME_EXISTS,SOME_11,THE_DEF]); 198 199val lem3a = Q.prove 200(`!x xs. dom xs /\ (rev xs = []) ==> dom (x::xs)`, 201 RW_TAC std_ss [dom_def,rev_def] THEN 202 `d<>0` by METIS_TAC [IS_SOME_IREV] THEN 203 Q.EXISTS_TAC `SUC d` THEN 204 RW_TAC arith_ss [Once irev_def] THEN 205 REPEAT CASE_TAC THEN RW_TAC std_ss [] THEN 206 METIS_TAC [IS_SOME_EXISTS,irev_norm,THE_DEF,NOT_NIL_CONS]); 207 208val lem3b = Q.prove (* METIS_TAC takes ages on two goals ... *) 209(`!x xs h t. dom xs /\ (rev xs = h::t) /\ dom t /\ dom (x::rev t) ==> dom(x::xs)`, 210 RW_TAC std_ss [dom_def,rev_def] THEN 211 Q.EXISTS_TAC `SUC (MAX d (MAX d' d''))` THEN 212 RW_TAC arith_ss [Once irev_def] THEN 213 REPEAT CASE_TAC THEN RW_TAC std_ss [] THEN 214 METIS_TAC [IS_SOME_EXISTS,irev_norm,irev_monotone,MAX_LE_THM, 215 THE_DEF,NOT_SOME_NONE,CONS_11]); 216 217(*---------------------------------------------------------------------------*) 218(* Equational characterization of dom. *) 219(*---------------------------------------------------------------------------*) 220 221val dom_eqns = Q.prove 222(`(dom [] = T) /\ 223 (dom (x::xs) = dom (xs:'a list) /\ 224 (case rev xs 225 of [] => T 226 | h::t => dom t /\ dom (x::rev t)))`, 227 CONJ_TAC THENL [ALL_TAC, CASE_TAC] THEN 228 METIS_TAC [dom_base_case,lem1a,lem3a,lem1a,lem2a,lem2b,lem3b]); 229 230(*---------------------------------------------------------------------------*) 231(* So have derived a mutually recursive presentation of the partial function *) 232(* and its domain. Now prove induction. *) 233(*---------------------------------------------------------------------------*) 234 235val step2_lt = Q.prove 236(`!x xs. dom (x::xs) ==> rev_rdepth xs < rev_rdepth (x::xs)`, 237 RW_TAC std_ss [dom_def] THEN 238 `rev_rdepth (x::xs) <> 0` by METIS_TAC [IS_SOME_IREV,rev_rdepth] THEN 239 `rev_rdepth (x::xs) - 1 < rev_rdepth (x::xs)` by DECIDE_TAC THEN 240 `IS_SOME (irev (rev_rdepth (x::xs)) (x::xs))` by METIS_TAC [rev_rdepth] THEN 241 `IS_SOME(irev (rev_rdepth (x::xs) - 1) xs)` 242 by (POP_ASSUM MP_TAC THEN ASM_SIMP_TAC arith_ss [Once irev_def] THEN 243 REPEAT CASE_TAC THEN RW_TAC std_ss [] THEN 244 METIS_TAC[IS_SOME_EXISTS]) THEN 245 `rev_rdepth xs <= rev_rdepth (x::xs) - 1` by METIS_TAC [rev_rdepth] 246 THEN DECIDE_TAC); 247 248val step3_lt = Q.prove 249(`!x xs y ys. dom (x::xs) /\ (y::ys = rev xs) ==> rev_rdepth ys < rev_rdepth (x::xs)`, 250 RW_TAC std_ss [dom_def,rev_def] THEN 251 `rev_rdepth (x::xs) <> 0` by METIS_TAC [IS_SOME_IREV,rev_rdepth] THEN 252 `rev_rdepth (x::xs) - 1 < rev_rdepth (x::xs)` by DECIDE_TAC THEN 253 `IS_SOME (irev (rev_rdepth (x::xs)) (x::xs))` by METIS_TAC [rev_rdepth] THEN 254 `IS_SOME(irev (rev_rdepth (x::xs) - 1) ys)` 255 by (POP_ASSUM MP_TAC THEN ASM_SIMP_TAC arith_ss [Once irev_def] THEN 256 REPEAT CASE_TAC THEN RW_TAC std_ss [] THEN 257 METIS_TAC [IS_SOME_EXISTS,THE_DEF,NOT_CONS_NIL,irev_norm,CONS_11,NOT_SOME_NONE]) 258 THEN 259 `rev_rdepth ys <= rev_rdepth (x::xs) - 1` by METIS_TAC [rev_rdepth] 260 THEN DECIDE_TAC); 261 262val step4_lt = Q.prove 263(`!x xs y ys. dom (x::xs) /\ (y::ys = rev xs) ==> rev_rdepth (x::rev ys) < rev_rdepth (x::xs)`, 264 RW_TAC std_ss [dom_def,rev_def] THEN 265 `rev_rdepth (x::xs) <> 0` by METIS_TAC [IS_SOME_IREV,rev_rdepth] THEN 266 `rev_rdepth (x::xs) - 1 < rev_rdepth (x::xs)` by DECIDE_TAC THEN 267 `IS_SOME (irev (rev_rdepth (x::xs)) (x::xs))` by METIS_TAC [rev_rdepth] THEN 268 `IS_SOME(irev (rev_rdepth (x::xs) - 1) (x::rev ys))` 269 by (POP_ASSUM MP_TAC THEN ASM_SIMP_TAC arith_ss [Once irev_def] THEN 270 REPEAT CASE_TAC THEN RW_TAC std_ss [] THEN 271 METIS_TAC [IS_SOME_EXISTS,THE_DEF,NOT_CONS_NIL,irev_norm,CONS_11,NOT_SOME_NONE,rev_def]) 272 THEN `rev_rdepth (x::rev ys) <= rev_rdepth (x::xs) - 1` by METIS_TAC [rev_rdepth] 273 THEN RW_TAC arith_ss [GSYM rev_def]); 274 275(*---------------------------------------------------------------------------*) 276(* Induction for rev is a consequence of well-founded induction. *) 277(*---------------------------------------------------------------------------*) 278 279val ind0 = MATCH_MP relationTheory.WF_INDUCTION_THM 280 (Q.ISPEC `rev_rdepth` prim_recTheory.WF_measure); 281val ind1 = SIMP_RULE std_ss [prim_recTheory.measure_thm] ind0; 282val ind2 = SIMP_RULE std_ss [pairTheory.FORALL_PROD] 283 (Q.ISPEC `\list. dom list ==> P list` ind1); 284 285val rev_ind = Q.prove 286(`!P. P [] /\ 287 (!x xs. dom (x::xs) /\ 288 P xs /\ (!y ys. (y::ys = rev xs) ==> P ys /\ P (x::rev ys)) 289 ==> P (x::xs)) 290 ==> !list. dom list ==> P list`, 291 GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC ind2 THEN 292 Cases THENL [METIS_TAC [], ALL_TAC] THEN 293 DISCH_THEN (fn th => 294 DISCH_THEN (fn th1 => POP_ASSUM MATCH_MP_TAC THEN POP_ASSUM (K ALL_TAC) 295 THEN ASSUME_TAC (REWRITE_RULE [AND_IMP_INTRO] th) 296 THEN MP_TAC th1)) THEN 297 SIMP_TAC std_ss [] THEN 298 POP_ASSUM (fn th => RW_TAC std_ss [] THEN MATCH_MP_TAC th) THENL 299 [METIS_TAC [step2_lt,dom_eqns], IMP_RES_TAC step3_lt, IMP_RES_TAC step4_lt] THEN 300 ASM_REWRITE_TAC [] THEN Q.PAT_ASSUM `dom (h::t)` MP_TAC THEN 301 RULE_ASSUM_TAC GSYM THEN RW_TAC std_ss [Once dom_eqns]); 302 303 304(*---------------------------------------------------------------------------*) 305(* Property: rev = REVERSE *) 306(*---------------------------------------------------------------------------*) 307 308val rev_is_REVERSE = Q.prove 309(`!list. dom list ==> (rev list = REVERSE list)`, 310 HO_MATCH_MP_TAC rev_ind THEN RW_TAC list_ss [REVERSE_DEF] THENL 311 [METIS_TAC [dom_eqns,list_case_def,rev_eqns], 312 RW_TAC std_ss [Once rev_eqns] THEN CASE_TAC THEN 313 RW_TAC list_ss []]); 314 315 316(*---------------------------------------------------------------------------*) 317(* Efficient executable version of rev *) 318(*---------------------------------------------------------------------------*) 319 320val exec_def = 321 Define 322 `exec d list = 323 if d=0 then (if dom list then rev list else ARB) else 324 case list 325 of [] => [] 326 | x::xs => 327 case exec (d-1) xs 328 of [] => [x] 329 | y::ys => y :: exec (d-1) (x::exec (d-1) ys)`; 330 331val exec_equals_rev = Q.prove 332(`!d list. dom list ==> (exec d list = rev list)`, 333 Induct THEN RW_TAC std_ss [Once exec_def] THEN 334 IMP_RES_TAC rev_eqns THEN POP_ASSUM SUBST_ALL_TAC THEN 335 REPEAT CASE_TAC THENL 336 [METIS_TAC [dom_eqns,CONS_11,NOT_CONS_NIL], 337 METIS_TAC [dom_eqns,CONS_11,NOT_CONS_NIL], 338 FULL_SIMP_TAC list_ss [Once dom_eqns] THEN METIS_TAC [CONS_11,NOT_CONS_NIL]]); 339 340val BIG_def = Define `BIG = 1073741823`; 341 342val Rev_def = 343 Define 344 `Rev list = if dom list then rev list else exec BIG list`; 345 346(*---------------------------------------------------------------------------*) 347(* Theorem showing that exec BIG = Rev in the domain of the function. *) 348(*---------------------------------------------------------------------------*) 349 350val Rev_exec = Q.prove 351(`Rev list = exec BIG list`, 352 RW_TAC std_ss [Rev_def,exec_equals_rev]); 353 354val Rev_dom_eqns = Q.prove 355(`(dom [] <=> T) /\ 356 (dom (x::xs) <=> 357 dom xs /\ 358 case Rev xs 359 of [] => T 360 | h::t => dom t /\ dom (x::Rev t))`, 361 CONJ_TAC THENL 362 [METIS_TAC [dom_eqns], 363 RW_TAC list_ss [Once dom_eqns,Rev_def] THEN 364 CASE_TAC THEN METIS_TAC [dom_eqns]]); 365 366val Rev_eqns = Q.prove 367(`dom list ==> 368 (Rev list = 369 case list 370 of [] => [] 371 | x::xs => case Rev xs 372 of [] => [x] 373 | h::t => h::Rev (x::Rev t))`, 374 SIMP_TAC std_ss [Rev_def] THEN CASE_TAC THENL 375 [RW_TAC list_ss [rev_eqns], 376 STRIP_TAC THEN IMP_RES_TAC rev_eqns THEN POP_ASSUM SUBST_ALL_TAC THEN 377 NTAC 2 (CASE_TAC THEN RW_TAC list_ss []) THEN 378 METIS_TAC[lem1a,lem2a,lem2b]]); 379 380val Rev_ind = Q.prove 381(`!P. P [] /\ 382 (!x xs. dom (x::xs) /\ 383 P xs /\ (!y ys. (y::ys = Rev xs) ==> P ys /\ P (x::Rev ys)) 384 ==> P (x::xs)) 385 ==> !list. dom list ==> P list`, 386 GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC rev_ind THEN 387 ASM_REWRITE_TAC [] THEN 388 POP_ASSUM (fn th => REPEAT STRIP_TAC THEN MATCH_MP_TAC th) THEN 389 RW_TAC std_ss [Rev_def] THEN METIS_TAC [lem1a,lem2a,lem2b]); 390 391 392(*---------------------------------------------------------------------------*) 393(* Show totality directly *) 394(*---------------------------------------------------------------------------*) 395 396val LENGTH_REVERSE = Q.prove 397(`!list. LENGTH(REVERSE list) = LENGTH list`, 398 Induct THEN RW_TAC list_ss []); 399 400val total_dom = Q.prove 401(`!list. dom list`, 402 measureInduct_on `LENGTH list` THEN Cases_on `list` THENL 403 [METIS_TAC [dom_eqns], 404 RW_TAC list_ss [Once dom_eqns] THEN CASE_TAC THEN 405 `LENGTH t < LENGTH (h::t)` by RW_TAC list_ss [] THEN 406 `dom t` by METIS_TAC[] THEN 407 `LENGTH t = LENGTH (h'::t')` by METIS_TAC [rev_is_REVERSE,LENGTH_REVERSE] THEN 408 `LENGTH t' < LENGTH (h::t)` by RW_TAC list_ss [] THEN 409 CONJ_TAC THENL 410 [METIS_TAC[], 411 FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC list_ss [] THEN 412 `dom t'` by METIS_TAC [] THEN 413 METIS_TAC [rev_is_REVERSE,LENGTH_REVERSE,DECIDE ``x < SUC x``]]]); 414 415(*---------------------------------------------------------------------------*) 416(* Finally, use the totality of dom to remove restrictions. *) 417(*---------------------------------------------------------------------------*) 418 419val Rev_thm = SIMP_RULE std_ss [total_dom] Rev_eqns; 420val Rev_ind_thm = SIMP_RULE std_ss [total_dom] Rev_ind; 421