1(*--------------------------------------------------------------------------- 2 A battery of tests for the "Define" function in bossLib. 3 ---------------------------------------------------------------------------*) 4 5(*--------------------------------------------------------------------------- 6 First, a few straightforward recursions, some with 7 extended pattern matching. 8 ---------------------------------------------------------------------------*) 9 10val fact_def = Define `fact x = if x = 0 then 1 else x * fact(x-1)`; 11 12val Fib_def = 13 Define `(Fib 0 = 1) 14 /\ (Fib (SUC 0) = 1) 15 /\ (Fib (SUC(SUC x)) = Fib x + Fib (SUC x))`; 16 17val assoc_def = 18 Define 19 `assoc (x:'a) ((a,y)::t) = if x=a then y else assoc x t`; 20 21Define`step x = x`; 22 23val SM = Define `SM s n = if n=0 then s else SM (step s) (n-1)`; 24 25Hol_datatype `tau = Ctr of bool # bool # bool`; 26Define `goo(Ctr(d,_,_)) = d`; 27 28(*--------------------------------------------------------------------------- 29 For the following 3, a "normal" size measure like LENGTH wouldn't 30 allow termination to be proved. Our parameterized size measure 31 does work, however. 32 ---------------------------------------------------------------------------*) 33 34val flatten_def = 35 Define `(flatten [] = []) 36 /\ (flatten ([]::rst) = flatten rst) 37 /\ (flatten ((h::t)::rst) = h::flatten(t::rst))`; 38 39val Tot_def = 40 Define 41 `(Tot [] = 0) /\ 42 (Tot (0::t) = Tot t) /\ 43 (Tot (SUC n::t) = 1 + Tot (n::t))`; 44 45val Tot_def = 46 Define 47 `(Tot [] = 0) /\ 48 (Tot (0::t) = Tot t) /\ 49 (Tot (n::t) = 1 + Tot (n-1::t))`; 50 51val gcd_def = 52Define 53 `(gcd (0,y) = y) 54 /\ (gcd (SUC x, 0) = SUC x) 55 /\ (gcd (SUC x, SUC y) = 56 if y <= x then gcd(x-y, SUC y) 57 else gcd(SUC x, y-x))`; 58 59val gcd_def = (* curried *) 60 Define 61 `(gcd 0 y = y) /\ 62 (gcd (SUC x) 0 = SUC x) /\ 63 (gcd (SUC x) (SUC y) = 64 if y <= x then gcd (x-y) (SUC y) 65 else gcd (SUC x) (y-x))`; 66 67val gcd_def = (* using MOD *) 68 Define 69 `gcd a b = if a = 0 then b else gcd (b MOD a) a`; 70 71(* Should fail with informative error message *) 72val percent2 = 73 Define 74 `(%% 0 y = y) /\ 75 (%% (SUC x) 0 = SUC x) /\ 76 (%% (SUC x) (SUC y) = if y <= x then %% (x-y) (SUC y) 77 else %% (SUC x) (y-x))`; 78 79val percent2 = 80 xDefine "percentpercent" 81 `(%% 0 y = y) /\ 82 (%% (SUC x) 0 = SUC x) /\ 83 (%% (SUC x) (SUC y) = if y <= x then %% (x-y) (SUC y) 84 else %% (SUC x) (y-x))`; 85val map2_def = 86 Define 87 `(map2(f, []:'a list,L:'b list) = []:'c list) /\ 88 (map2(f, h::t, []) = []) /\ 89 (map2(f, h1::t1, h2::t2) = f h1 h2::map2 (f, t1, t2))`; 90 91val sorted_def = 92 Define 93 `(sorted (R, []) = T) /\ 94 (sorted (R, [x]) = T) /\ 95 (sorted (R, x::y::rst) = R x y /\ sorted (R, y::rst))`; 96 97val part_def = 98Define 99 `(part (P, [], l1,l2) = (l1,l2)) /\ 100 (part (P, h::rst, l1,l2) 101 = if P h then part(P,rst, h::l1, l2) 102 else part(P,rst, l1, h::l2))`; 103 104val div_def = Define 105 `(div (0,x) = (0,0)) /\ 106 (div (SUC x, y) = 107 let (q,r) = div(x,y) 108 in (if y <= SUC r then (SUC q,0) else (q, SUC r)))`; 109 110(* Test nested lets *) 111val div_def = Define 112 `(Div(0,x) = (0,0)) /\ 113 (Div(SUC x, y) = 114 let q = FST(Div(x,y)) 115 and r = SND(Div(x,y)) 116 in 117 if y <= SUC r then (SUC q,0) else (q, SUC r))`; 118 119(* Test nested ifs *) 120val smaller_def = Define 121 `(smaller((0,i), z) = (i:num)) /\ 122 (smaller((SUC x, i), (0,j)) = j) /\ 123 (smaller((SUC x, i), (SUC y,j)) = 124 if SUC y = i then i else 125 if SUC x = j then j 126 else smaller((x,i), (y,j)))`; 127 128val min_def = Define 129 `(min (SUC x) (SUC y) = min x y + 1) 130 /\ (min x y = 0)`; 131 132 133(*---------------------------------------------------------------------------* 134 * Dutch National Flag by functional programming. Similar to bubble sort. * 135 *---------------------------------------------------------------------------*) 136 137Hol_datatype `colour = Red | White | Blue`; 138 139val Swap_def = 140 Define 141 `(Swap [] = NONE) 142 /\ (Swap (White::Red::rst) = SOME(Red::White::rst)) 143 /\ (Swap (Blue::Red::rst) = SOME(Red::Blue::rst)) 144 /\ (Swap (Blue::White::rst) = SOME(White::Blue::rst)) 145 /\ (Swap (x::rst) = OPTION_MAP (CONS x) (Swap rst))`; 146 147val Swap_def' = 148 let val Swap_NIL = CONJUNCT1 Swap_def 149 in 150 CONJ Swap_NIL 151 (REWRITE_RULE [Swap_NIL,optionTheory.OPTION_MAP_DEF] 152 (CONJUNCT2 Swap_def)) 153 end; 154 155val Flag_defn = Hol_defn 156 "Flag" 157 `Flag list = case Swap list 158 of NONE => list 159 | SOME slist => Flag slist`; 160 161 162(*--------------------------------------------------------------------------- 163 Primitive recursion 164 ---------------------------------------------------------------------------*) 165 166val Fact_def = Define 167 `(Fact 0 = 1) /\ 168 (Fact (SUC x) = Fact x * SUC x)`; 169 170val mem_def = 171 Define 172 `(mem x [] = F) /\ 173 (mem x (h::t) = (x=h) \/ mem x t)`; 174 175val filter_def = 176 Define 177 `(filter P [] = []) /\ 178 (filter P (h::t) = if P h then h::filter P t else filter P t)`; 179 180val part_def = 181 Define 182 `(part P [] l1 l2 = (l1,l2)) /\ 183 (part P (h::rst) l1 l2 = 184 if P h then part P rst (h::l1) l2 185 else part P rst l1 (h::l2))`; 186 187val fold_def = 188 Define 189 `(fold b f [] = b) /\ 190 (fold b f (h::t) = f h (fold b f t))`; 191 192val exists_def = 193 Define 194 `(exists P [] = F) /\ 195 (exists P (h::t) = (P h) \/ exists P t)`; 196 197val sumf_def = 198 Define 199 `(sumf f [] = 0) /\ 200 (sumf f (h::t) = f h + sumf f t)`; 201 202(*--------------------------------------------------------------------------- 203 Iterated primitive recursion (see it_prim_rec) 204 ---------------------------------------------------------------------------*) 205 206val Ack_def = 207 Define 208 `(Ack (0,n) = n+1) /\ 209 (Ack (SUC m,0) = Ack (m, 1)) /\ 210 (Ack (SUC m, SUC n) = Ack (m, Ack (SUC m, n)))`; 211 212val Sudan_def = 213 Define 214 `(Sudan 0 (x,y) = x+y) 215 /\ (Sudan (SUC n) (x,0) = x) 216 /\ (Sudan (SUC n) (x,SUC y) = Sudan n (Sudan (SUC n) (x,y), 217 Sudan (SUC n) (x,y) + SUC y))`; 218 219val V_def = 220 Define 221 `(V (SUC 0, n, m) = n) 222/\ (V (SUC(SUC k), n, SUC 0) = V (SUC k, SUC n, SUC n)) 223/\ (V (SUC(SUC k), n, SUC (SUC m)) = V (SUC k, V(SUC(SUC k),n,SUC m)+1, 224 V(SUC(SUC k),n,SUC m)+1))`; 225 226(*--------------------------------------------------------------------------- 227 Schematic definitions 228 ---------------------------------------------------------------------------*) 229 230val While = TotalDefn.DefineSchema `While s = if B s then While (C s) else s`; 231 232 233Hol_datatype `btree = LEAF 234 | NODE of btree => 'a => btree`; 235 236val btreeRec_def = 237 Define 238 `(btreeRec LEAF (v:'a) (f:'a->'b->'a->'a) = v) 239 /\ (btreeRec (NODE t1 M t2) v f = f (btreeRec t1 v f) M (btreeRec t2 v f))`; 240 241 242val unfold_def = 243 TotalDefn.DefineSchema 244 `unfold (x:'a) = 245 if more x 246 then let (y1,b,y2) = dest x 247 in 248 NODE (unfold y1) b (unfold y2) 249 else LEAF`; 250 251val fusion_def = 252 TotalDefn.DefineSchema 253 `fusion (x:'a) = 254 if more x 255 then let (y,i,z) = dest x 256 in 257 g (fusion y) (i:'b) (fusion z) 258 else (c:'c)`; 259 260val linRec_def = 261 TotalDefn.DefineSchema 262 `linRec (x:'a) = 263 if atomic x then A x 264 else join (linRec (dest x)) (D x:'b)`; 265 266val accRec_def0 = 267 TotalDefn.DefineSchema 268 `accRec (x:'a, u:'b) = 269 if atomic x 270 then join (A x) u 271 else accRec (dest x, join (D x:'b) u)`; 272 273(*--------------------------------------------------------------------------- 274 Binary recursive schema. 275 ---------------------------------------------------------------------------*) 276 277val binRec_def = 278 TotalDefn.DefineSchema 279 `binRec (x:'a) = 280 if atomic x then (A x:'b) 281 else join (binRec (left x)) 282 (binRec (right x))`; 283 284(*--------------------------------------------------------------------------- 285 General tail recursive schema for lists. 286 ---------------------------------------------------------------------------*) 287 288val baRec_def = 289 TotalDefn.DefineSchema 290 `(baRec ([],v) = (v:'b)) 291 /\ (baRec (h::t, v) = 292 if atomic h 293 then baRec (t, join v (A h:'b)) 294 else baRec (dest (h:'a) ++ t, v))`; 295 296(* Has failed in the past *) 297val baRec_def = 298 TotalDefn.DefineSchema 299 `(baRec [] v = (v:'b)) 300 /\ (baRec (h::t) v = 301 if atomic h 302 then baRec t (join v (A h:'b)) 303 else baRec (dest (h:'a) ++ t) v)`; 304 305 306(*--------------------------------------------------------------------------- 307 Non-recursive, curried, complex patterns, wildcards 308 ---------------------------------------------------------------------------*) 309 310 311Define `(g2 0 _ = 1) /\ 312 (g2 _ 0 = 2)`; 313 314Define `(g3 0 _ _ = 1) /\ 315 (g3 _ 0 _ = 2) /\ 316 (g3 _ _ 0 = 3)`; 317 318Define `(g4 (0,_,_,_) = 1) /\ 319 (g4 (_,0,_,_) = 2) /\ 320 (g4 (_,_,0,_) = 3) /\ 321 (g4 (_,_,_,0) = 4)`; 322 323Define `(g5 (0,_,_,_,_) = 1) /\ 324 (g5 (_,0,_,_,_) = 2) /\ 325 (g5 (_,_,0,_,_) = 3) /\ 326 (g5 (_,_,_,0,_) = 4) /\ 327 (g5 (_,_,_,_,0) = 5)`; 328 329(*--------------------------------------------------------------------------- 330 Some simple cases where termination is not yet proved automatically. 331 ---------------------------------------------------------------------------*) 332 333val qsort_def = 334 Hol_defn "qsort" 335 `(qsort(ord,[]) = []) /\ 336 (qsort(ord, x::rst) = 337 qsort(ord,FILTER ($~ o ord x) rst) ++ [x] ++ 338 qsort(ord,FILTER(ord x) rst))`; 339 340val fqsort_def = 341 Hol_defn "fqsort" 342 `(fqsort ord [] = []) /\ 343 (fqsort ord (x::rst) = 344 let (l1,l2) = part (ord x) rst [] [] 345 in 346 fqsort ord l1 ++ [x] ++ fqsort ord l2)`; 347 348val variant_def = 349 Hol_defn "variant" 350 `variant x L = if MEM x L then variant (x+1) L else x`; 351 352 353(*--------------------------------------------------------------------------- 354 Wang's algorithm for propositional logic. 355 ---------------------------------------------------------------------------*) 356 357Hol_datatype `prop = VAR of 'a 358 | NOT of prop 359 | AND of prop => prop 360 | OR of prop => prop`; 361 362val Pr_def = 363 Hol_defn "Pr" 364 `(Pr vl [] (VAR v::r) vr = Pr vl [] r (v::vr)) 365 /\ (Pr vl [] (NOT x::r) vr = Pr vl [x] r vr) 366 /\ (Pr vl [] (OR x y::r) vr = Pr vl [] (x::y::r) vr) 367 /\ (Pr vl [] (AND x y::r) vr = Pr vl [] (x::r) vr /\ Pr vl [] (y::r) vr) 368 369 /\ (Pr vl (VAR v::l) r vr = Pr (v::vl) l r vr) 370 /\ (Pr vl (NOT x::l) r vr = Pr vl l (x::r) vr) 371 /\ (Pr vl (AND x y::l) r vr = Pr vl (x::y::l) r vr) 372 /\ (Pr vl (OR x y::l) r vr = Pr vl (x::l) r vr /\ Pr vl (y::l) r vr) 373 374 /\ (Pr vl [] [] vr = EXISTS (\y. MEM y vl) vr)`; 375 376 377val Prove_def = Define `Prove P = Pr [] [] [P] []`; 378 379(*--------------------------------------------------------------------------- 380 Termination of Pr. We need a subsidiary measure function on 381 propositions which makes a 2-argument proposition bigger than a 382 list of 2 propositions. 383 ---------------------------------------------------------------------------*) 384 385val Meas_def = 386 Define 387 `(Meas (VAR v) = 0) 388 /\ (Meas (NOT x) = SUC (Meas x)) 389 /\ (Meas (AND x y) = Meas x + Meas y + 2) 390 /\ (Meas (OR x y) = Meas x + Meas y + 2)`; 391 392(*---------------------------------------------------------------------------* 393 * Termination of Pr. * 394 *---------------------------------------------------------------------------*) 395 396val (Pr_eqns, Pr_ind) = Defn.tprove 397(Pr_def, 398 WF_REL_TAC `measure \(w:'a list, x:'a prop list, y:'a prop list, z:'a list). 399 list_size Meas x + list_size Meas y` 400 THEN RW_TAC arith_ss [Meas_def,listTheory.list_size_def]); 401 402 403(*--------------------------------------------------------------------------- 404 Binary trees (again). 405 ---------------------------------------------------------------------------*) 406 407Hol_datatype 408 `Btree = Leaf of 'a 409 | Brh of 'a => Btree => Btree`; 410 411(* prim. rec. *) 412Define 413 `(upheap R w (Leaf x) = Brh w (Leaf x) (Leaf x)) /\ 414 (upheap R w (Brh v p q) = 415 if R w v then Brh w (upheap R v q) p 416 else Brh v (upheap R w q) p)`; 417 418(*--------------------------------------------------------------------------- 419 Not sure if this actually does anything useful. It might be nicer 420 to define this schematically on R, and still have termination proved. 421 ---------------------------------------------------------------------------*) 422 423TotalDefn.DefineSchema 424 `(merge_heap R (Leaf x) b = b) 425 /\ (merge_heap R (Brh v b1 b2) (Leaf x) = Brh v b1 b2) 426 /\ (merge_heap R (Brh v b1 b2) (Brh w c1 c2) 427 = if R v w 428 then Brh v (merge_heap R b1 b2) (Brh w c1 c2) 429 else Brh w (Brh v b1 b2) (merge_heap R c1 c2))`; 430 431TotalDefn.DefineSchema 432 `(merge_heap (Leaf x) b = b) 433 /\ (merge_heap (Brh v b1 b2) (Leaf x) = Brh v b1 b2) 434 /\ (merge_heap (Brh v b1 b2) (Brh w c1 c2) 435 = if R v w 436 then Brh v (merge_heap b1 b2) (Brh w c1 c2) 437 else Brh w (Brh v b1 b2) (merge_heap c1 c2))`; 438 439(*---------------------------------------------------------------------------* 440 * This one fails, because you need to know a relation between term_size and * 441 * list_size. Might work with multiset ordering. * 442 *---------------------------------------------------------------------------*) 443 444val V_def = 445Define 446 `(V [] acc = acc) 447 /\ (V (Leaf s::rst) acc = V rst ([Leaf s]::acc)) 448 /\ (V (Brh x tm1 tm2::rst) acc = V (tm1::tm2::rst) acc)`; 449 450TypeBasePure.type_size (TypeBase.theTypeBase()) (Type`:'a Btree list`); 451 452(*---------------------------------------------------------------------------* 453 * This one fails because the size of the tree is not changed. * 454 * Termination is provable with the following interpretation "Int": * 455 * * 456 * Int (Leaf) = 0 * 457 * Int (Brh x y) = 2 * Int x + Int y + 1 * 458 *---------------------------------------------------------------------------*) 459 460val Lin_def = 461 Define 462 `(Lin (Leaf x) = Leaf x) 463 /\ (Lin (Brh a (Leaf x) bt) = Brh a (Leaf x) (Lin bt)) 464 /\ (Lin (Brh a (Brh x bt1 bt2) bt) = Lin (Brh x bt1 (Brh a bt2 bt)))`; 465 466 467(*--------------------------------------------------------------------------- 468 Majority vote, in a variety of slightly different presentations, 469 some of which at one time or other made our naive termination 470 prover fail. 471 ---------------------------------------------------------------------------*) 472 473Define 474 `(Maj [] (winner,lead) = (winner,lead)) 475/\ (Maj (h::t) (leader,0) = if h=leader then Maj t (leader,1) else Maj t (h,1)) 476/\ (Maj (h::t) (leader, SUC m) = 477 if h=leader then Maj t (leader, m+2) else Maj t (leader, m))`; 478 479(* Alternative formulation *) 480Define 481 `(Maj [] (winner,lead) = (winner,lead)) 482 /\ (Maj (h::t) (leader,0) = Maj t (if h=leader then (leader,1) else (h,1))) 483 /\ (Maj (h::t) (leader, SUC m) = 484 if h=leader then Maj t (leader, m+2) 485 else Maj t (leader, m))`; 486 487(* Alternative formulation ... fails at the moment *) 488Define 489 `(Maj [] (winner,lead) = (winner,lead)) 490 /\ (Maj (h::t) (leader,0) = Maj t (if h=leader then (leader,1) else (h,1))) 491 /\ (Maj (h::t) (leader,SUC m) = Maj t (leader, if h=leader then m+2 else m))`; 492 493Define (* fails at the moment *) 494 `(Maj [] (winner,lead) = (winner,lead)) 495 /\ (Maj (h::t) (leader,0) = Maj t ((if h=leader then leader else h),1)) 496 /\ (Maj (h::t) (leader,SUC m) = Maj t (leader, if h=leader then m+2 else m))`; 497 498Define 499 `(Maj [] (winner,lead) = (winner,lead)) 500 /\ (Maj (h::t) (leader,0) = Maj t (h,1)) 501 /\ (Maj (h::t) (leader,SUC m) = Maj t (leader, if h=leader then m+2 else m))`; 502 503(* Wildcards. *) 504Define 505 `(Maj [] (winner,lead) = (winner,lead)) 506 /\ (Maj (h::t) (_,0) = Maj t (h,1)) 507 /\ (Maj (h::t) (leader, SUC m) 508 = Maj t (leader, (if h=leader then m+2 else m)))`; 509 510 511(*--------------------------------------------------------------------------- 512 Nested recursion 513 ---------------------------------------------------------------------------*) 514 515val N = Define `N x = if x>100 then x-10 else N(N(x+11))`; (* Fails *) 516val Ndef = Hol_defn "ninety1" 517 `N x = if x>100 then x-10 else N(N(x+11))`; 518 519xDefine "percentage" `% x = if x>100 then x-10 else %(%(x+11))`; 520 521(*--------------------------------------------------------------------------- 522 Mutual recursion 523 ---------------------------------------------------------------------------*) 524 525val even_odd = 526 xDefine "even_odd" 527 `(even 0 = T) 528 /\ (even (SUC n) = odd n) 529 /\ (odd 0 = F) 530 /\ (odd (SUC n) = even n)`; 531 532val even_odd = 533xDefine "even_odd_again" 534 `(&& 0 = T) /\ 535 (&& (SUC n) = !! n) /\ 536 (!! 0 = F) /\ 537 (!! (SUC n) = && n)`; 538 539val nnf_mutrec_eqns = 540 xDefine "nnfs" 541 `(nnfpos (VAR x) = VAR x) 542 /\ (nnfpos (NOT p) = nnfneg p) 543 /\ (nnfpos (AND p q) = AND (nnfpos p) (nnfpos q)) 544 /\ (nnfpos (OR p q) = OR (nnfpos p) (nnfpos q)) 545 546 /\ (nnfneg (VAR x) = NOT (VAR x)) 547 /\ (nnfneg (NOT p) = nnfpos p) 548 /\ (nnfneg (AND p q) = OR (nnfneg p) (nnfneg q)) 549 /\ (nnfneg (OR p q) = AND (nnfneg p) (nnfneg q))`; 550 551 552(*--------------------------------------------------------------------------- 553 Higher order recursion. First we prove and install a 554 congruence rule for sum. Congruence rules for common 555 higher-order list functions (MAP, EXISTS) have already 556 been installed. 557 ---------------------------------------------------------------------------*) 558 559val sumf_cong = Q.prove 560(`!l1 l2 f f'. 561 (l1=l2) /\ (!x. MEM x l2 ==> (f x = f' x)) 562 ==> 563 (sumf f l1 = sumf f' l2)`, 564Induct THEN NTAC 2 (RW_TAC list_ss [sumf_def,listTheory.MEM])); 565 566DefnBase.add_cong sumf_cong; 567 568 569(*--------------------------------------------------------------------------- 570 Now some "higher-order recursive" functions over a type of 571 labelled n-ary trees (built from constructor "Node"). 572 ---------------------------------------------------------------------------*) 573 574app load ["numLib"]; open numLib listTheory; 575 576val _ = Hol_datatype `ltree = LNODE of 'a => ltree list`; 577 578val ltree_size_def = snd (TypeBase.size_of ``:'a ltree``); 579 580val ltree_map_def = 581 tDefine 582 "ltree_map" 583 `ltree_map f (LNODE v tl) = LNODE (f v) (MAP (ltree_map f) tl)` 584 (WF_REL_TAC `measure \(v,y). ltree_size (\v. 0) y` 585 THEN Induct 586 THEN RW_TAC list_ss [MEM,list_size_def,ltree_size_def] 587 THENL [ARITH_TAC, 588 METIS_TAC [DECIDE ``x < 1+y ==> x < y + (z + 2)``]]); 589 590val ltree_map_ind = fetch "-" "ltree_map_ind"; 591 592val ltree_map_o = Q.prove( 593`!g t f. ltree_map f (ltree_map g t) = ltree_map (f o g) t`, 594recInduct ltree_map_ind 595 THEN RW_TAC std_ss [ltree_map_def] 596 THEN Induct_on `tl` 597 THEN ZAP_TAC list_ss [MEM]); 598 599val ltree_occurs_def = 600 Hol_defn "ltree_occurs" 601 `ltree_occurs x (LNODE v tl) = (x=v) \/ EXISTS (ltree_occurs x) tl`; 602 603(*--------------------------------------------------------------------------- 604 Can also obtain the same result with the schematic : 605 606 `ltree_occurs (LNODE v tl) = (x=v) \/ EXISTS ltree_occurs tl` 607 ---------------------------------------------------------------------------*) 608 609val collect_def = 610 tDefine 611 "collect" 612 `collect f (LNODE v tl) = FOLDR (\h a. collect f h ++ a) [f v] tl` 613 (WF_REL_TAC `measure (ltree_size (\v.0) o SND)` 614 THEN Induct 615 THEN RW_TAC list_ss [MEM,list_size_def,ltree_size_def] 616 THENL [ARITH_TAC, 617 PROVE_TAC [DECIDE ``x < 1+y ==> x < y + (z + 2)``]]); 618 619val collect_ind = fetch "-" "collect_ind"; 620 621val ltree_size_def2 = 622 Hol_defn "ltree_size2" 623 `ltree_size2 f (LNODE v tl) = 1 + f v + SUM (MAP (ltree_size2 f) tl)`; 624 625val ltree_SIZE_def = 626 Hol_defn 627 "ltree_SIZE" 628 `ltree_SIZE f (LNODE v tl) = 1 + f v + sumf (ltree_SIZE f) tl`; 629 630(*--------------------------------------------------------------------------- 631 TC extraction, case of regexp matching 632 ---------------------------------------------------------------------------*) 633 634load "stringTheory"; 635 636Hol_datatype `regexp = 637 Any (* Any character *) 638 | Epsilon (* Empty string *) 639 | Atom of char (* Specific character *) 640 | Or of regexp => regexp (* Union *) 641 | Then of regexp => regexp (* Concatenation *) 642 | Repeat of regexp`; (* Iterated concat, >= 0 *) 643 644 645val SPLIT_def = Define 646 `(SPLIT P [] acc = NONE) /\ 647 (SPLIT P (h::t) acc = if P h then SOME (acc, h, t) 648 else SPLIT P t (acc++[h]))`; 649 650val csp_def = Define 651 `(csp [] ns = []) 652/\ (csp ((Repeat r::cdr, w, s)::b::c) ns = 653 if b = (r::Repeat r::cdr, w, SOME (Repeat r::cdr)) 654 then (Repeat r::cdr, w, ns)::b::c 655 else (Repeat r::cdr, w, ns)::csp (b::c) ns) 656/\ (csp ((Any::cdr, w, s)::c) ns = (Any::cdr, w, ns)::c) 657/\ (csp ((Atom c1::cdr, w, s)::c) ns = (Atom c1::cdr, w, ns) :: c) 658/\ (csp ((rl,w,s)::c) ns = (rl,w,ns)::csp c ns)`; 659 660val nS_defn = Hol_defn 661 "nS" 662 `nS ms = 663 case SPLIT (\x. ?r l w. x = (Repeat r::l, w, SOME (Repeat r::l))) ms [] 664 of NONE => ms 665 | SOME (l1, (bad_r, bad_w, bad_s), z) => 666 case SPLIT (\x. ?s. x = (bad_r, bad_w, s)) l1 [] 667 of NONE => [] 668 | SOME (x1, (rl,w1,s1), y) => nS (x1 ++ [(rl, w1, s1)] ++ csp z s1)`; 669 670val defn = 671 Hol_defn 672 "foo" 673 `foo L = 674 case SPLIT ($= 3) L [] 675 of NONE => L 676 | SOME(L1,x,L2) => 677 case SPLIT ($=2) L1 [] 678 of NONE => [] 679 | SOME (L1a, y, L1b) => foo (L1a ++ [y] ++ L2)`; 680 681Defn.tgoal defn; 682e (RW_TAC list_ss []); 683 684 685val defn = 686 Hol_defn 687 "foo1" 688 `foo1 L = 689 case SPLIT ($= 3) L [] 690 of NONE => L 691 | SOME(L1,_,L2) => 692 case SPLIT ($=2) L1 [] 693 of NONE => [] 694 | SOME (L1a, y, _) => foo1 (L1a ++ [y] ++ L2)`; 695 696val defn = 697 Hol_defn 698 "bar" 699 `bar L = case L 700 of [] => 1 701 | h::t => case t 702 of [] => 2 703 | h1::t1 => bar t1`; 704 705 706(*---------------------------------------------------------------------------*) 707(* Multiple rebindings of variables *) 708(*---------------------------------------------------------------------------*) 709 710load "wordsTheory"; 711 712val _ = Define ` 713 field_neg (r1:word32,r10:word32) = 714 if r1 = 0w then (r1,r10) else 715 let r1 = r10 - r1 in (r1,r10)`; 716 717val _ = Define ` 718 field_add (r0:word32,r1:word32,r10:word32) = 719 let r0 = r1 + r0 in 720 if r0 < r10 then (r0,r10) else 721 let r0 = r0 - r10 in 722 (r0,r10)`; 723 724val _ = Define ` 725 field_sub (r0,r1,r10) = 726 let (r1,r10) = field_neg (r1,r10) in 727 let (r0,r10) = field_add (r0,r1,r10) in 728 (r0,r10)`; 729 730val _ = Define ` 731 field_add222 (r2:word32,r10:word32) = 732 let r2 = r2 + r2 in 733 if r2 < r10 then (r2,r10) else 734 let r2 = r2 - r10 in 735 (r2,r10)`; 736 737val _ = Define ` 738 field_add424 (r2:word32,r4:word32,r10:word32) = 739 let r4 = r4 + r2 in 740 if r4 < r10 then (r2,r4,r10) else 741 let r4 = r4 - r10 in 742 (r2,r4,r10)`; 743 744val _ = Define ` 745 field_mult_aux (r2:word32,r3:word32,r4:word32,r10:word32) = 746 if r3 = 0w then (r4,r10) else 747 if r3 && 1w = 0w then 748 let r3 = r3 >>> 1 in 749 let (r2,r10) = field_add222 (r2,r10) in 750 field_mult_aux (r2:word32,r3:word32,r4:word32,r10:word32) 751 else 752 let r3 = r3 >>> 1 in 753 let (r2,r4,r10) = field_add424 (r2,r4,r10) in 754 let (r2,r10) = field_add222 (r2,r10) in 755 field_mult_aux (r2:word32,r3:word32,r4:word32,r10:word32)`; 756 757val _ = Define ` 758 field_mult (r2,r3,r10) = 759 let r4 = 0w in 760 let (r4,r10) = field_mult_aux (r2,r3,r4,r10) in 761 (r4,r10)`; 762 763Define` 764 field_exp_aux (r5:word32,r6:word32,r7:word32,r10) = 765 if r6 = 0w then (r7,r10) else 766 if r6 && 1w = 0w then 767 let r6 = r6 >>> 1 in 768 let r2 = r5 in 769 let r3 = r5 in 770 let (r4,r10) = field_mult (r2,r3,r10) in 771 let r5 = r4 in 772 field_exp_aux (r5:word32,r6:word32,r7:word32,r10) 773 else 774 let r6 = r6 >>> 1 in 775 let r2 = r7 in 776 let r3 = r5 in 777 let (r4,r10) = field_mult (r2,r3,r10) in 778 let r7 = r4 in 779 let r2 = r5 in 780 let r3 = r5 in 781 let (r4,r10) = field_mult (r2,r3,r10) in 782 let r5 = r4 in 783 field_exp_aux (r5:word32,r6:word32,r7:word32,r10)`; 784 785Define` 786 field_exp_aux (r5:word32,r6:word32,r7:word32,r10) = 787 if r6 = 0w then (r7,r10) else 788 if r6 && 1w = 0w then 789 let r6 = r6 >>> 1 in 790 let r2 = r5 in 791 let r3 = r5 in 792 let (r4,r10) = field_mult (r2,r3,r10) in 793 let r5 = r4 in 794 field_exp_aux (r5:word32,r6:word32,r7:word32,r10) 795 else 796 let r6 = r6 >>> 1 in 797 let r2 = r7 in 798 let r3 = r5 in 799 let (r4,r10) = field_mult (r2,r3,r10) in 800 let r7 = r4 in 801 let r2 = r5 in 802 let r3 = r5 in 803 let (r4,r10) = field_mult (r2,r3,r10) in 804 let r5 = r4 in 805 field_exp_aux (r5:word32,r6:word32,r7:word32,r10)`; 806 807(*---------------------------------------------------------------------------*) 808(* Exercising multiDefine *) 809(*---------------------------------------------------------------------------*) 810 811TotalDefn.multiDefine 812 `(fact x = if zerop x then 1 else mult x (sub1 x)) /\ 813 (zerop x = (x=0)) /\ 814 (sub1 x = x-1) /\ 815 (mult x y = x * y)`; 816 817TotalDefn.multiDefine (* fails because of sub1 in rec. call *) 818 `(fact x = if zerop x then 1 else mult x (fact (sub1 x))) /\ 819 (zerop x = (x=0)) /\ 820 (sub1 x = x-1) /\ 821 (mult x y = x * y)`; 822 823TotalDefn.multiDefine 824 `(fact x = if x=0 then 1 else mult x (fact (x-1))) /\ 825 (mult x y = x * y) /\ 826 (even 0 = T) /\ 827 (even (SUC n) = odd n) /\ 828 (odd 0 = F) /\ 829 (odd (SUC n) = even n)`; 830 831TotalDefn.multiDefine 832 `(even 0 = T) /\ 833 (even (SUC n) = odd n) /\ 834 (fact x = if x=0 then 1 else mult x (fact (x-1))) /\ 835 (mult x y = x * y) /\ 836 (odd 0 = F) /\ 837 (odd (SUC n) = even n)`; 838 839TotalDefn.multiDefine 840 `(example 1 = F) /\ 841 (example 2 = T)`; 842 843(*---------------------------------------------------------------------------*) 844(* Bug from mjcg. ZIP_DELTA gave funky result. *) 845(*---------------------------------------------------------------------------*) 846 847val LOOKUP_def = 848 Define 849 `(LOOKUP [] v = NONE) 850 /\ 851 (LOOKUP (p :: l) v = if (FST p = v) then SOME p else LOOKUP l v)`; 852 853val ZIP_DELTA_def = 854 Define 855 `(ZIP_DELTA b d1 [] = d1) 856 /\ 857 (ZIP_DELTA b [] d2 = d2) 858 /\ 859 (ZIP_DELTA b ((v1,x1)::d1) ((v2,x2)::d2) = 860 if v1 = v2 861 then (v1,x1) :: ZIP_DELTA b d1 d2 862 else case LOOKUP d2 v1 of 863 SOME(v,x) => (v1, if b then x1 else x) :: ZIP_DELTA b d1 d2 864 | NONE => (v1,x1) :: ZIP_DELTA b d1 ((v2,x2)::d2))`; 865 866val test_def = 867 Define 868 `(test d1 [] = d1) /\ 869 (test [] d2 = d2) /\ 870 (test (p1::d1) (p2::d2) = 871 case LOOKUP d2 (FST p1) of 872 NONE => p1 :: test d1 (p2::d2) 873 | SOME(v,x) => (FST p1,x) :: test d1 d2)`; 874 875 876(*---------------------------------------------------------------------------*) 877(* Prim. rec. defns over nested recursive types should always succeed. *) 878(*---------------------------------------------------------------------------*) 879 880val _ = Hol_datatype `exp = Or of exp => exp 881 | And of exp => exp 882 | Lf of bool` 883 884val _ = Hol_datatype `code = Assign of bool 885 | PosCond of code list 886 | NegCond of code list` 887 888val exp_eval_def = 889 Define` 890 (exp_eval (Or e1 e2) = exp_eval e1 \/ exp_eval e2) /\ 891 (exp_eval (And e1 e2) = exp_eval e1 /\ exp_eval e2) /\ 892 (exp_eval (Lf b) = b) 893`; 894 895val code_eval_defn = Hol_defn "code_eval" ` 896 (code_eval v [] = v) /\ 897 (code_eval v (cod :: rest) = 898 case cod of 899 Assign b => code_eval (SOME b) rest 900 | PosCond c => 901 (case v of 902 NONE => NONE 903 | SOME T => code_eval (code_eval v c) rest 904 | SOME F => code_eval v rest) 905 | NegCond c => 906 (case v of 907 NONE => NONE 908 | SOME F => code_eval (code_eval v c) rest 909 | SOME T => code_eval v rest)) 910`; 911 912val code1_size = prove(``code1_size = list_size code_size``, 913 SRW_TAC [][FUN_EQ_THM] THEN 914 Induct_on `x` THEN 915 SRW_TAC [][definition "code_size_def", 916 listTheory.list_size_def]); 917 918val (code_eval_def, code_eval_ind) = Defn.tprove( 919 code_eval_defn, 920 WF_REL_TAC `inv_image (measure (list_size code_size)) SND` THEN 921 SRW_TAC [ARITH_ss][definition "code_size_def", code1_size]); 922 923(*---------------------------------------------------------------------------*) 924(* Problem (now solved) with production of ind. thm with patterns having *) 925(* literals. *) 926(*---------------------------------------------------------------------------*) 927 928Hol_datatype `ty = C1 of num => bool`; 929Define `foo (C1 15 b) = 1`; 930 931(*---------------------------------------------------------------------------*) 932(* More test involving literal patterns. *) 933(*---------------------------------------------------------------------------*) 934 935Define 936 `(bar (2,3) = 3) /\ 937 (bar (2,4) = 6) /\ 938 (bar (2,5) = 9) /\ 939 (bar (3,x) = 25)`; 940 941load "wordsLib"; 942 943val _ = Hol_datatype `RName = 944 RName_0usr | RName_1usr | RName_2usr | RName_3usr 945 | RName_4usr | RName_5usr | RName_6usr | RName_7usr 946 | RName_8usr | RName_8fiq | RName_9usr | RName_9fiq 947 | RName_10usr | RName_10fiq | RName_11usr | RName_11fiq 948 | RName_12usr | RName_12fiq 949 | RName_SPusr | RName_SPfiq | RName_SPirq | RName_SPsvc 950 | RName_SPabt | RName_SPund | RName_SPmon 951 | RName_LRusr | RName_LRfiq | RName_LRirq | RName_LRsvc 952 | RName_LRabt | RName_LRund | RName_LRmon 953 | RName_PC`; 954 955val RevLookUpRName_def = Define` 956 (RevLookUpRName (0w:word4,0b10000w:word5) = RName_0usr) /\ 957 (RevLookUpRName (1w, 0b10000w) = RName_1usr) /\ 958 (RevLookUpRName (2w, 0b10000w) = RName_2usr) /\ 959 (RevLookUpRName (3w, 0b10000w) = RName_3usr) /\ 960 (RevLookUpRName (4w, 0b10000w) = RName_4usr) /\ 961 (RevLookUpRName (5w, 0b10000w) = RName_5usr) /\ 962 (RevLookUpRName (6w, 0b10000w) = RName_6usr) /\ 963 (RevLookUpRName (7w, 0b10000w) = RName_7usr) /\ 964 (RevLookUpRName (8w, 0b10000w) = RName_8usr) /\ 965 (RevLookUpRName (8w, 0b10001w) = RName_8fiq) /\ 966 (RevLookUpRName (9w, 0b10000w) = RName_9usr) /\ 967 (RevLookUpRName (9w, 0b10001w) = RName_9fiq) /\ 968 (RevLookUpRName (10w,0b10000w) = RName_10usr) /\ 969 (RevLookUpRName (10w,0b10001w) = RName_10fiq) /\ 970 (RevLookUpRName (11w,0b10000w) = RName_11usr) /\ 971 (RevLookUpRName (11w,0b10001w) = RName_11fiq) /\ 972 (RevLookUpRName (12w,0b10000w) = RName_12usr) /\ 973 (RevLookUpRName (12w,0b10001w) = RName_12fiq) /\ 974 (RevLookUpRName (13w,0b10000w) = RName_SPusr) /\ 975 (RevLookUpRName (13w,0b10001w) = RName_SPfiq) /\ 976 (RevLookUpRName (13w,0b10010w) = RName_SPirq) /\ 977 (RevLookUpRName (13w,0b10011w) = RName_SPsvc) /\ 978 (RevLookUpRName (13w,0b10111w) = RName_SPabt) /\ 979 (RevLookUpRName (13w,0b11011w) = RName_SPund) /\ 980 (RevLookUpRName (13w,0b10110w) = RName_SPmon) /\ 981 (RevLookUpRName (14w,0b10000w) = RName_LRusr) /\ 982 (RevLookUpRName (14w,0b10001w) = RName_LRfiq) /\ 983 (RevLookUpRName (14w,0b10010w) = RName_LRirq) /\ 984 (RevLookUpRName (14w,0b10011w) = RName_LRsvc) /\ 985 (RevLookUpRName (14w,0b10111w) = RName_LRabt) /\ 986 (RevLookUpRName (14w,0b11011w) = RName_LRund) /\ 987 (RevLookUpRName (14w,0b10110w) = RName_LRmon) /\ 988 (RevLookUpRName (15w,0b10000w) = RName_PC)`; 989 990Define `t1 (17w,a,b) = a /\ b`; 991Define `t2 (17w,18w,a,b) = a /\ b`; 992Define `t3 (17w,a,18w,b,19w,c) = a /\ b /\ c`; 993Define `t4 (a,17w,18w,b,19w,c) = a /\ b /\ c`; 994Define `t5 (a,17w,18w,b,c,19w) = a /\ b /\ c`; 995Define `t6 (a,17w,18w,19w,b,c) = a /\ b /\ c`; 996 997 998(*---------------------------------------------------------------------------*) 999(* Comparison function on first order terms. *) 1000(*---------------------------------------------------------------------------*) 1001 1002load "stringLib"; 1003open comparisonTheory; (* source in HOLDIR/src/enumfset *) 1004 1005val _ = Hol_datatype 1006 `term 1007 = Var of string 1008 | App of string => term list`; 1009 1010val term_size_def = fetch "-" "term_size_def"; 1011 1012val term_cmp_def = 1013 tDefine 1014 "term_cmp" 1015 `(term_cmp (Var x1) (Var x2) = string_cmp x1 x2) ��� 1016 (term_cmp (Var _) (App _ _) = Less) ��� 1017 (term_cmp (App _ _) (Var _) = Greater) ��� 1018 (term_cmp (App x1 ts1) (App x2 ts2) = 1019 pair_cmp string_cmp (list_cmp term_cmp) (x1,ts1) (x2,ts2))` 1020 (RW_TAC list_ss [] THEN 1021 WF_REL_TAC `measure (term_size o FST)` THEN 1022 Induct_on `ts1` THEN RW_TAC list_ss [term_size_def] THENL 1023 [ALL_TAC, RES_TAC THEN POP_ASSUM (MP_TAC o SPEC_ALL)] THEN DECIDE_TAC); 1024 1025(*---------------------------------------------------------------------------*) 1026(* Monadic-style definitions. From Anthony Fox. *) 1027(*---------------------------------------------------------------------------*) 1028 1029load "state_transformerTheory"; 1030 1031val foo_def = 1032 Define 1033 `foo n = BIND (UNIT (n - 1)) 1034 (\k. if n = 0 then UNIT T else foo k)`; 1035 1036val eta_free = REWRITE_RULE [ETA_THM] foo_def; 1037 1038val test_def = Define` 1039 test n = BIND (UNIT (n - 1)) 1040 (\a. BIND (UNIT a) 1041 (\b. if n = 0 then UNIT T else test a))` 1042 1043 1044val test_def = Define` 1045 test n = BIND (UNIT (n - 1)) 1046 (\a. BIND (UNIT a) 1047 (\b. if n = 0 then UNIT T else test b))`; 1048