1(* 2 This file defines a rose tree data structure as a co-inductive 3 datatype called 'a ltree, which is short for lazy tree. This 4 co-datatype has one constructor, called Branch that has type: 5 6 Branch : 'a -> 'a ltree llist -> 'a ltree 7 8 Note that this tree data structure allows for both infinite depth 9 and infinite breadth. 10*) 11open HolKernel Parse boolLib bossLib term_tactic; 12open arithmeticTheory listTheory llistTheory alistTheory optionTheory; 13open mp_then pred_setTheory relationTheory pairTheory combinTheory; 14 15val _ = new_theory "ltree"; 16 17(* make type definition *) 18 19Type ltree_rep[local] = ``:num list -> 'a # num option``; 20 21Overload NOTHING[local] = ``(ARB:'a, SOME (0:num))``; 22 23Definition ltree_rep_ok_def: 24 ltree_rep_ok f <=> 25 !path x n. 26 f path = (x, SOME n) ==> 27 !pos rest. f (path ++ pos::rest) <> NOTHING ==> pos < n 28End 29 30Theorem type_inhabited[local]: 31 ?f. ltree_rep_ok f 32Proof 33 qexists_tac `\p. NOTHING` \\ fs [ltree_rep_ok_def] \\ rw [] 34QED 35 36val ltree_tydef = new_type_definition ("ltree", type_inhabited); 37 38val repabs_fns = define_new_type_bijections 39 { name = "ltree_absrep", 40 ABS = "ltree_abs", 41 REP = "ltree_rep", 42 tyax = ltree_tydef}; 43 44 45(* prove basic theorems about rep and abs functions *) 46 47val ltree_absrep = CONJUNCT1 repabs_fns 48val ltree_repabs = CONJUNCT2 repabs_fns 49 50Theorem ltree_rep_ok_ltree_rep[local,simp]: 51 ltree_rep_ok (ltree_rep f) 52Proof 53 fs [ltree_repabs, ltree_absrep] 54QED 55 56Theorem ltree_abs_11[local]: 57 ltree_rep_ok r1 /\ ltree_rep_ok r2 ==> ((ltree_abs r1 = ltree_abs r2) = (r1 = r2)) 58Proof 59 fs [ltree_repabs, EQ_IMP_THM] \\ metis_tac [] 60QED 61 62Theorem ltree_rep_11[local]: 63 (ltree_rep t1 = ltree_rep t2) = (t1 = t2) 64Proof 65 fs [EQ_IMP_THM] \\ metis_tac [ltree_absrep] 66QED 67 68Theorem every_ltree_rep_ok[local]: 69 !ts. every ltree_rep_ok (LMAP ltree_rep ts) 70Proof 71 rw [] \\ qspec_then `ts` strip_assume_tac fromList_fromSeq 72 \\ rw [LMAP_fromList,every_fromList_EVERY,EVERY_MEM,MEM_MAP] 73 \\ fs [ltree_rep_ok_ltree_rep] 74QED 75 76Theorem LMAP_ltree_rep_11[local]: 77 LMAP ltree_rep ts1 = LMAP ltree_rep ts2 <=> ts1 = ts2 78Proof 79 rw [] 80 \\ qspec_then `ts1` strip_assume_tac fromList_fromSeq \\ rw [] 81 \\ qspec_then `ts2` strip_assume_tac fromList_fromSeq \\ rw [] 82 \\ fs [LMAP_fromList] 83 \\ fs [Once FUN_EQ_THM,ltree_rep_11] \\ fs [FUN_EQ_THM] 84 \\ rename [`MAP _ l1 = MAP _ l2`] 85 \\ qid_spec_tac `l1` 86 \\ qid_spec_tac `l2` 87 \\ Induct \\ Cases_on `l1` \\ fs [ltree_rep_11] 88QED 89 90Theorem LMAP_ltree_rep_ltree_abs[local]: 91 every ltree_rep_ok ts ==> 92 LMAP ltree_rep (LMAP ltree_abs ts) = ts 93Proof 94 rw [] \\ qspec_then `ts` strip_assume_tac fromList_fromSeq 95 \\ fs [LMAP_fromList,every_fromList_EVERY,MEM_MAP, 96 LMAP_fromList,MAP_MAP_o] 97 \\ rw [ltree_repabs,FUN_EQ_THM] \\ fs [ltree_repabs] 98 \\ Induct_on `l` \\ fs [ltree_repabs] 99QED 100 101 102(* define the only constructor: Branch *) 103 104Definition Branch_rep_def: 105 Branch_rep (x:'a) (xs:('a ltree_rep) llist) = 106 \path. case path of 107 | [] => (x, LLENGTH xs) 108 | (n::rest) => case LNTH n xs of SOME t => t rest | NONE => NOTHING 109End 110 111Definition Branch: 112 Branch a ts = ltree_abs (Branch_rep a (LMAP ltree_rep ts)) 113End 114 115Theorem ltree_rep_ok_Branch_rep_every[local]: 116 ltree_rep_ok (Branch_rep a ts) = every ltree_rep_ok ts 117Proof 118 fs [Branch_rep_def,ltree_rep_ok_def] 119 \\ rw [] \\ reverse (qspec_then `ts` strip_assume_tac fromList_fromSeq) 120 \\ rw [ltree_rep_ok_def] 121 \\ eq_tac \\ rpt strip_tac 122 THEN1 123 (first_x_assum (qspecl_then [`i::path`,`x`,`n`] mp_tac) 124 \\ fs [] \\ disch_then drule \\ fs []) 125 THEN1 126 (Cases_on `path` \\ fs [] 127 \\ first_x_assum drule 128 \\ disch_then drule \\ fs []) 129 \\ fs [every_fromList_EVERY,LNTH_fromList] 130 THEN1 131 (rw [EVERY_EL,ltree_rep_ok_def] 132 \\ first_x_assum (qspec_then `n::path` mp_tac) \\ fs [] 133 \\ disch_then drule \\ fs []) 134 \\ fs [EVERY_EL,ltree_rep_ok_def] 135 \\ Cases_on `path` \\ fs [] 136 \\ rw [] \\ fs [AllCaseEqs()] 137 \\ res_tac \\ fs [] 138QED 139 140Theorem ltree_rep_ok_Branch_rep[local]: 141 every ltree_rep_ok ts ==> ltree_rep_ok (Branch_rep a ts) 142Proof 143 fs [ltree_rep_ok_Branch_rep_every] 144QED 145 146Theorem ltree_rep_ok_Branch_rep_IMP[local]: 147 ltree_rep_ok (Branch_rep a ts) ==> every ltree_rep_ok ts 148Proof 149 fs [ltree_rep_ok_Branch_rep_every] 150QED 151 152 153(* prove injectivity *) 154 155Theorem Branch_rep_11[local]: 156 !a1 a2 ts1 ts2. Branch_rep a1 ts1 = Branch_rep a2 ts2 <=> a1 = a2 /\ ts1 = ts2 157Proof 158 fs [Branch_rep_def,FUN_EQ_THM] 159 \\ rpt gen_tac \\ eq_tac \\ simp [] 160 \\ strip_tac 161 \\ first_assum (qspec_then `[]` assume_tac) \\ fs [] \\ rw [] 162 \\ reverse (qspec_then `ts1` strip_assume_tac fromList_fromSeq) \\ rw [] 163 \\ reverse (qspec_then `ts2` strip_assume_tac fromList_fromSeq) \\ rw [] 164 \\ fs [LLENGTH_fromSeq,LLENGTH_fromList] 165 THEN1 166 (fs [FUN_EQ_THM] \\ rw [] 167 \\ first_x_assum (qspec_then `x::x'` mp_tac) \\ fs []) 168 \\ fs [LNTH_fromList] 169 \\ fs [LIST_EQ_REWRITE] \\ rw [] 170 \\ rw [FUN_EQ_THM] 171 \\ first_x_assum (qspec_then `x::x'` mp_tac) \\ fs [] 172QED 173 174Theorem Branch_11: 175 !a1 a2 ts1 ts2. Branch a1 ts1 = Branch a2 ts2 <=> a1 = a2 /\ ts1 = ts2 176Proof 177 rw [Branch] \\ eq_tac \\ strip_tac \\ fs [] 178 \\ qspec_then `ts1` assume_tac every_ltree_rep_ok 179 \\ drule ltree_rep_ok_Branch_rep 180 \\ qspec_then `ts2` assume_tac every_ltree_rep_ok 181 \\ drule ltree_rep_ok_Branch_rep 182 \\ strip_tac \\ strip_tac 183 \\ fs [ltree_abs_11] 184 \\ fs [LMAP_ltree_rep_11,Branch_rep_11] 185QED 186 187 188(* prove cases theorem *) 189 190Theorem Branch_rep_exists[local]: 191 ltree_rep_ok f ==> ?a ts. f = Branch_rep a ts 192Proof 193 fs [ltree_rep_ok_def] \\ rw [] 194 \\ Cases_on `f []` \\ fs [] 195 \\ rename [`_ = (a,ts)`] 196 \\ qexists_tac `a` 197 \\ qexists_tac `LGENLIST (\n path. f (n::path)) ts` 198 \\ fs [Branch_rep_def,FUN_EQ_THM] 199 \\ Cases \\ fs [LNTH_LGENLIST] 200 \\ Cases_on `f (h::t)` \\ fs [] 201 \\ Cases_on `ts` \\ fs [] 202 \\ IF_CASES_TAC \\ fs [] 203 \\ first_x_assum drule \\ fs [] 204 \\ disch_then (qspecl_then [`h`,`t`] mp_tac) \\ fs [] 205QED 206 207Theorem ltree_cases: 208 !t. ?a ts. t = Branch a ts 209Proof 210 fs [Branch] \\ fs [GSYM ltree_rep_11] \\ rw [] 211 \\ qspec_then `ts1` assume_tac every_ltree_rep_ok 212 \\ qabbrev_tac `f = ltree_rep t` 213 \\ `ltree_rep_ok f` by fs [Abbr`f`] 214 \\ drule Branch_rep_exists \\ rw [] 215 \\ qexists_tac `a` \\ qexists_tac `LMAP ltree_abs ts` 216 \\ imp_res_tac ltree_rep_ok_Branch_rep_IMP 217 \\ fs [LMAP_ltree_rep_ltree_abs,ltree_repabs] 218QED 219 220 221(* define ltree_CASE constant *) 222 223Definition dest_Branch_rep_def: 224 dest_Branch_rep (l:'a ltree_rep) = 225 let (x,len) = l [] in 226 (x, LGENLIST (\n path. l (n::path)) len) 227End 228 229Theorem dest_Branch_rep_Branch_rep[local]: 230 dest_Branch_rep (Branch_rep x xs) = (x,xs) 231Proof 232 fs [Branch_rep_def,dest_Branch_rep_def] 233 \\ qspec_then `xs` strip_assume_tac fromList_fromSeq \\ fs [] 234 \\ fs [LGENLIST_EQ_fromSeq,FUN_EQ_THM,LGENLIST_EQ_fromList] 235 \\ fs [LNTH_fromList] 236 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM GENLIST_ID])) 237 \\ fs [GENLIST_FUN_EQ,FUN_EQ_THM] 238QED 239 240Definition ltree_CASE[nocompute]: 241 ltree_CASE t f = 242 let (a,ts) = dest_Branch_rep (ltree_rep t) in 243 f a (LMAP ltree_abs ts) 244End 245 246Theorem ltree_CASE[compute]: 247 ltree_CASE (Branch a ts) f = f a ts 248Proof 249 fs [ltree_CASE,Branch] 250 \\ qspec_then `ts` assume_tac every_ltree_rep_ok 251 \\ drule ltree_rep_ok_Branch_rep 252 \\ fs [ltree_repabs,dest_Branch_rep_Branch_rep] 253 \\ fs [LMAP_MAP] \\ rw [] \\ AP_TERM_TAC 254 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq 255 \\ fs [LMAP_fromList,LMAP_fromSeq,FUN_EQ_THM,ltree_absrep] 256 \\ rpt (pop_assum kall_tac) 257 \\ Induct_on `l` \\ fs [ltree_absrep] 258QED 259 260Theorem ltree_CASE_eq: 261 ltree_CASE t f = v <=> ?a ts. t = Branch a ts /\ f a ts = v 262Proof 263 qspec_then `t` strip_assume_tac ltree_cases \\ rw [] 264 \\ fs [Branch_11,ltree_CASE] 265QED 266 267 268(* ltree generator *) 269 270Definition path_ok_def: 271 path_ok path f <=> 272 !xs n ys k a. 273 path = xs ++ n::ys /\ f xs = (a,SOME k) ==> n < k 274End 275 276Definition make_ltree_rep_def: 277 make_ltree_rep f = 278 \path. if path_ok path f then f path else NOTHING 279End 280 281Theorem ltree_rep_ok_make_ltree_rep[local]: 282 !f. ltree_rep_ok (make_ltree_rep f) 283Proof 284 fs [ltree_rep_ok_def,make_ltree_rep_def] \\ rw [] 285 THEN1 286 (fs [AllCaseEqs()] \\ fs [] 287 \\ fs [path_ok_def] \\ metis_tac []) 288 \\ fs [AllCaseEqs()] \\ fs [] 289 \\ CCONTR_TAC \\ fs [] \\ fs [] 290 \\ fs [path_ok_def] \\ rw [] 291 \\ first_x_assum (qspecl_then [`xs`,`n`,`ys ++ pos::rest`] mp_tac) 292 \\ fs [] 293QED 294 295Definition gen_ltree_def[nocompute]: 296 gen_ltree f = ltree_abs (make_ltree_rep f) 297End 298 299Theorem gen_ltree: 300 gen_ltree f = 301 let (a,len) = f [] in 302 Branch a (LGENLIST (\n. gen_ltree (\path. f (n::path))) len) 303Proof 304 fs [UNCURRY,gen_ltree_def,Branch,o_DEF] 305 \\ qspec_then `f` assume_tac ltree_rep_ok_make_ltree_rep 306 \\ fs [REWRITE_RULE [ltree_rep_ok_make_ltree_rep] 307 (Q.SPEC `make_ltree_rep f` ltree_repabs)] 308 \\ AP_TERM_TAC \\ Cases_on `f []` \\ fs [] 309 \\ fs [Branch_rep_def,FUN_EQ_THM] 310 \\ Cases \\ fs [] 311 THEN1 fs [make_ltree_rep_def,path_ok_def] 312 \\ Cases_on `r` \\ fs [] 313 \\ fs [LNTH_LGENLIST] 314 THEN1 315 (fs [make_ltree_rep_def] 316 \\ AP_THM_TAC \\ AP_THM_TAC \\ AP_TERM_TAC 317 \\ fs [path_ok_def] 318 \\ rw [] \\ eq_tac \\ rw [] 319 THEN1 320 (first_x_assum match_mp_tac 321 \\ goal_assum (first_assum o mp_then.mp_then mp_then.Any mp_tac) 322 \\ qexists_tac `ys` \\ fs []) 323 \\ Cases_on `xs` \\ fs [] \\ rw [] 324 \\ metis_tac []) 325 \\ fs [make_ltree_rep_def] 326 \\ reverse (Cases_on `h < x`) \\ fs [] 327 THEN1 (rw [] \\ fs [path_ok_def] \\ metis_tac [APPEND]) 328 \\ AP_THM_TAC \\ AP_THM_TAC \\ AP_TERM_TAC 329 \\ fs [path_ok_def] 330 \\ rw [] \\ eq_tac \\ rw [] 331 THEN1 332 (first_x_assum match_mp_tac 333 \\ goal_assum (first_assum o mp_then.mp_then mp_then.Any mp_tac) 334 \\ qexists_tac `ys` \\ fs []) 335 \\ Cases_on `xs` \\ fs [] \\ rw [] 336 \\ metis_tac [] 337QED 338 339Theorem gen_ltree_LNIL: 340 gen_ltree f = Branch a LNIL <=> f [] = (a, SOME 0) 341Proof 342 simp [Once gen_ltree,UNCURRY] 343 \\ Cases_on `f []` \\ fs [Branch_11] 344QED 345 346 347(* ltree unfold *) 348 349Definition make_unfold_def: 350 make_unfold f seed [] = 351 (let (a,seeds) = f seed in (a,LLENGTH seeds)) /\ 352 make_unfold f seed (n::path) = 353 let (a,seeds) = f seed in 354 make_unfold f (THE (LNTH n seeds)) path 355End 356 357Definition ltree_unfold: 358 ltree_unfold f seed = 359 gen_ltree (make_unfold f seed) 360End 361 362Theorem ltree_unfold: 363 ltree_unfold f seed = 364 let (a,seeds) = f seed in 365 Branch a (LMAP (ltree_unfold f) seeds) 366Proof 367 fs [ltree_unfold] 368 \\ once_rewrite_tac [gen_ltree] 369 \\ simp [Once make_unfold_def] 370 \\ Cases_on `f seed` 371 \\ fs [Branch_11] 372 \\ reverse (qspec_then `r` strip_assume_tac fromList_fromSeq) 373 \\ fs [LGENLIST_EQ_fromSeq] 374 THEN1 375 (fs [FUN_EQ_THM,ltree_unfold] \\ rw [] 376 \\ AP_TERM_TAC \\ fs [FUN_EQ_THM] \\ rw [] 377 \\ fs [make_unfold_def]) 378 \\ fs [LGENLIST_EQ_fromList,LMAP_fromList] 379 \\ fs [LIST_EQ_REWRITE,EL_MAP] \\ rw [] 380 \\ rw [ltree_unfold] \\ rw [] 381 \\ AP_TERM_TAC \\ fs [FUN_EQ_THM] \\ rw [] 382 \\ fs [make_unfold_def,LNTH_fromList] 383QED 384 385 386(* lemmas for proving equivalences *) 387 388Definition ltree_el_def: 389 ltree_el t [] = 390 ltree_CASE t (\a ts. SOME (a, LLENGTH ts)) /\ 391 ltree_el t (n::ns) = 392 ltree_CASE t (\a ts. 393 case LNTH n ts of 394 | NONE => NONE 395 | SOME t => ltree_el t ns) 396End 397 398Theorem ltree_el_def: 399 ltree_el (Branch a ts) [] = SOME (a, LLENGTH ts) /\ 400 ltree_el (Branch a ts) (n::ns) = 401 case LNTH n ts of 402 | NONE => NONE 403 | SOME t => ltree_el t ns 404Proof 405 qspec_then `t` strip_assume_tac ltree_cases 406 \\ fs [ltree_el_def,ltree_CASE] 407QED 408 409 410Theorem ltree_el_eqv: 411 !t1 t2. t1 = t2 <=> !path. ltree_el t1 path = ltree_el t2 path 412Proof 413 rw [] \\ eq_tac \\ rw [] 414 \\ fs [GSYM ltree_rep_11,FUN_EQ_THM] \\ rw [] 415 \\ pop_assum mp_tac 416 \\ qid_spec_tac `t1` \\ qid_spec_tac `t2` 417 \\ Induct_on `x` \\ rw [] 418 \\ `ltree_rep_ok (ltree_rep t1) /\ ltree_rep_ok (ltree_rep t2)` 419 by fs [ltree_rep_ok_ltree_rep] 420 \\ qspec_then `t1` strip_assume_tac ltree_cases 421 \\ qspec_then `t2` strip_assume_tac ltree_cases 422 \\ rpt BasicProvers.var_eq_tac \\ simp [Branch] 423 \\ `ltree_rep_ok (Branch_rep a (LMAP ltree_rep ts)) /\ 424 ltree_rep_ok (Branch_rep a' (LMAP ltree_rep ts'))` by 425 (rw [ltree_rep_ok_Branch_rep_every] 426 \\ rename [`LMAP _ ts2`] 427 \\ qspec_then `ts2` strip_assume_tac fromList_fromSeq \\ fs [] 428 \\ fs [LMAP_fromList,every_fromList_EVERY,EVERY_MEM] 429 \\ fs [MEM_MAP,PULL_EXISTS]) 430 \\ fs [ltree_repabs] 431 \\ simp [Branch_rep_def,LLENGTH_MAP] 432 \\ last_assum (qspec_then `[]` mp_tac) 433 \\ rewrite_tac [ltree_el_def] \\ fs [] \\ rw [] 434 \\ Cases_on `LNTH h ts` \\ Cases_on `LNTH h ts'` \\ fs [] 435 THEN1 (qspec_then `ts` strip_assume_tac fromList_fromSeq 436 \\ qspec_then `ts'` strip_assume_tac fromList_fromSeq 437 \\ rw [] \\ fs [LNTH_fromList]) 438 THEN1 (qspec_then `ts` strip_assume_tac fromList_fromSeq 439 \\ qspec_then `ts'` strip_assume_tac fromList_fromSeq 440 \\ rw [] \\ fs [LNTH_fromList]) 441 \\ last_x_assum match_mp_tac \\ rw [] 442 \\ last_x_assum (qspec_then `h::path` mp_tac) 443 \\ fs [ltree_el_def] 444QED 445 446Definition ltree_rel_def: 447 ltree_rel R x y <=> 448 !path. 449 OPTREL (\x y. R (FST x) (FST y) /\ SND x = SND y) 450 (ltree_el x path) (ltree_el y path) 451End 452 453Theorem ltree_rel: 454 ltree_rel R (Branch a ts) (Branch b us) <=> 455 R a b /\ llist_rel (ltree_rel R) ts us 456Proof 457 fs [ltree_rel_def,llist_rel_def] \\ rw [] \\ eq_tac \\ rw [] 458 THEN1 (first_x_assum (qspec_then `[]` mp_tac) \\ fs [ltree_el_def]) 459 THEN1 (first_x_assum (qspec_then `[]` mp_tac) \\ fs [ltree_el_def]) 460 THEN1 (first_x_assum (qspec_then `i::path` mp_tac) \\ fs [ltree_el_def]) 461 \\ Cases_on `path` \\ fs [ltree_el_def] 462 \\ Cases_on `LNTH h ts` \\ fs [] 463 \\ Cases_on `LNTH h us` \\ fs [] 464 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq 465 \\ qspec_then `us` strip_assume_tac fromList_fromSeq 466 \\ rw [] \\ fs [LNTH_fromList] \\ metis_tac [] 467QED 468 469Theorem ltree_rel_eq: 470 ltree_rel (=) x y <=> x = y 471Proof 472 fs [ltree_rel_def,ltree_el_eqv] \\ eq_tac \\ rw [] 473 \\ first_x_assum (qspec_then `path` mp_tac) 474 \\ Cases_on `ltree_el x path` \\ Cases_on `ltree_el y path` \\ fs [] 475 \\ fs [UNCURRY] 476 \\ rename [`FST y = FST z`] 477 \\ Cases_on `y` \\ Cases_on `z` \\ fs [] 478QED 479 480Theorem ltree_bisimulation: 481 !t1 t2. 482 t1 = t2 <=> 483 ?R. R t1 t2 /\ 484 !a ts a' ts'. 485 R (Branch a ts) (Branch a' ts') ==> 486 a = a' /\ llist_rel R ts ts' 487Proof 488 rw [] \\ eq_tac \\ rw [] 489 THEN1 (qexists_tac `(=)` \\ fs [Branch_11,llist_rel_def] \\ rw [] \\ fs []) 490 \\ simp [ltree_el_eqv] 491 \\ strip_tac 492 \\ last_x_assum mp_tac \\ qid_spec_tac `t1` \\ qid_spec_tac `t2` 493 \\ Induct_on `path` \\ rw [] 494 \\ qspec_then `t1` strip_assume_tac ltree_cases 495 \\ qspec_then `t2` strip_assume_tac ltree_cases 496 \\ fs [] 497 THEN1 (fs [ltree_el_def] \\ res_tac \\ fs [llist_rel_def]) 498 \\ rw [] \\ fs [ltree_el_def] 499 \\ res_tac \\ rw [] 500 \\ fs [llist_rel_def] 501 \\ pop_assum (qspec_then `h` mp_tac) 502 \\ Cases_on `LNTH h ts` \\ fs [] 503 \\ Cases_on `LNTH h ts'` \\ fs [] 504 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq 505 \\ qspec_then `ts'` strip_assume_tac fromList_fromSeq 506 \\ rw [] \\ fs [LNTH_fromList] 507QED 508 509 510(* misc *) 511 512Definition ltree_lookup_def: 513 ltree_lookup t [] = SOME t /\ 514 ltree_lookup t (n::ns) = 515 ltree_CASE t (\a ts. 516 case LNTH n ts of 517 | NONE => NONE 518 | SOME t => ltree_lookup t ns) 519End 520 521Theorem ltree_lookup_def: 522 ltree_lookup t [] = SOME t /\ 523 ltree_lookup (Branch a ts) (n::ns) = 524 case LNTH n ts of 525 | NONE => NONE 526 | SOME t => ltree_lookup t ns 527Proof 528 qspec_then `t` strip_assume_tac ltree_cases 529 \\ fs [ltree_lookup_def,ltree_CASE] 530QED 531 532Definition subtrees_def: 533 subtrees t = { u | ?path. ltree_lookup t path = SOME u } 534End 535 536Theorem subtrees: 537 subtrees (Branch a ts) = 538 Branch a ts INSERT BIGUNION (IMAGE subtrees (LSET ts)) 539Proof 540 fs [subtrees_def,Once EXTENSION,PULL_EXISTS] \\ rw [] 541 \\ qspec_then `x` strip_assume_tac ltree_cases 542 \\ fs [Branch_11] \\ rw [] \\ reverse eq_tac \\ rw [] 543 THEN1 (qexists_tac `[]` \\ fs [ltree_lookup_def]) 544 THEN1 (fs [LSET_def,IN_DEF] \\ qexists_tac `n::path` \\ fs [ltree_lookup_def]) 545 \\ Cases_on `path` \\ fs [] 546 \\ fs [ltree_lookup_def,Branch_11] 547 \\ Cases_on `LNTH h ts` \\ fs [] \\ disj2_tac 548 \\ fs [LSET_def,IN_DEF,PULL_EXISTS] 549 \\ rpt (goal_assum (first_assum o mp_then Any mp_tac)) 550QED 551 552Definition ltree_set_def: 553 ltree_set t = { a | ?ts. Branch a ts IN subtrees t } 554End 555 556Theorem ltree_set: 557 ltree_set (Branch a ts) = 558 a INSERT BIGUNION (IMAGE ltree_set (LSET ts)) 559Proof 560 fs [ltree_set_def,subtrees,Once EXTENSION,Branch_11] 561 \\ rw [] \\ Cases_on `a = x` \\ fs [] \\ fs [PULL_EXISTS] \\ metis_tac [] 562QED 563 564Definition ltree_map_def: 565 ltree_map f = ltree_unfold (\t. ltree_CASE t (\a ts. (f a,ts))) 566End 567 568Theorem ltree_map: 569 ltree_map f (Branch a xs) = Branch (f a) (LMAP (ltree_map f) xs) 570Proof 571 fs [ltree_map_def,ltree_unfold,ltree_CASE] 572QED 573 574Theorem ltree_map_id: 575 ltree_map I t = t 576Proof 577 fs [ltree_el_eqv] \\ qid_spec_tac `t` 578 \\ Induct_on `path` \\ rw [] \\ fs [ltree_el_def] 579 \\ qspec_then `t` strip_assume_tac ltree_cases 580 \\ fs [ltree_map,ltree_el_def,LLENGTH_MAP] 581 \\ rw [] \\ Cases_on `LNTH h ts` \\ fs [] 582QED 583 584Theorem ltree_map_map: 585 ltree_map f (ltree_map g t) = ltree_map (f o g) t 586Proof 587 fs [ltree_el_eqv] \\ qid_spec_tac `t` 588 \\ Induct_on `path` \\ rw [] \\ fs [ltree_el_def] 589 \\ qspec_then `t` strip_assume_tac ltree_cases 590 \\ fs [ltree_map,ltree_el_def,LLENGTH_MAP] 591 \\ rw [] \\ Cases_on `LNTH h ts` \\ fs [] 592QED 593 594Triviality ltree_lookup_map: 595 ltree_lookup (ltree_map f t) path = 596 case ltree_lookup t path of 597 | NONE => NONE 598 | SOME t => ltree_CASE t (\a ts. SOME (Branch (f a) (LMAP (ltree_map f) ts))) 599Proof 600 qid_spec_tac `t` \\ Induct_on `path` \\ fs [ltree_lookup_def] \\ rw [] 601 \\ qspec_then `t` strip_assume_tac ltree_cases 602 \\ fs [ltree_map,ltree_el_def,LLENGTH_MAP,ltree_CASE] 603 \\ fs [ltree_lookup_def] 604 \\ Cases_on `LNTH h ts` \\ fs [] 605QED 606 607Theorem ltree_set_map: 608 ltree_set (ltree_map f t) = IMAGE f (ltree_set t) 609Proof 610 fs [EXTENSION,ltree_set_def,subtrees_def] 611 \\ fs [ltree_lookup_map,AllCaseEqs(),ltree_CASE_eq,PULL_EXISTS,Branch_11] 612 \\ metis_tac [] 613QED 614 615Theorem ltree_rel_O: 616 ltree_rel R1 O ltree_rel R2 RSUBSET ltree_rel (R1 O R2) 617Proof 618 fs [ltree_rel_def,RSUBSET,O_DEF,PULL_EXISTS] 619 \\ rw [] \\ rpt (first_x_assum (qspec_then `path` mp_tac)) \\ rw [] 620 \\ Cases_on `ltree_el x path` \\ Cases_on `ltree_el y path` \\ fs [OPTREL_def] 621 \\ fs [UNCURRY] \\ metis_tac [] 622QED 623 624 625(* update TypeBase *) 626 627Theorem ltree_CASE_cong: 628 !M M' f f'. 629 M = M' /\ 630 (!a ts. M' = Branch a ts ==> f a ts = f' a ts) ==> 631 ltree_CASE M f = ltree_CASE M' f' 632Proof 633 rw [] \\ qspec_then `M` strip_assume_tac ltree_cases 634 \\ rw [] \\ fs [ltree_CASE] 635QED 636 637Overload "case" = ���ltree_CASE��� 638val _ = TypeBase.export 639 [TypeBasePure.mk_datatype_info 640 { ax = TypeBasePure.ORIG TRUTH, 641 induction = TypeBasePure.ORIG ltree_bisimulation, 642 case_def = ltree_CASE, 643 case_cong = ltree_CASE_cong, 644 case_eq = ltree_CASE_eq, 645 nchotomy = ltree_cases, 646 size = NONE, 647 encode = NONE, 648 lift = NONE, 649 one_one = SOME Branch_11, 650 distinct = NONE, 651 fields = [], 652 accessors = [], 653 updates = [], 654 destructors = [], 655 recognizers = [] } ] 656 657Theorem datatype_ltree: 658 DATATYPE ((ltree Branch):bool) 659Proof 660 rw [boolTheory.DATATYPE_TAG_THM] 661QED 662 663 664(* prove that every finite ltree is an inductively defined rose tree *) 665 666Inductive ltree_finite: 667 EVERY ltree_finite ts ==> ltree_finite (Branch a (fromList ts)) 668End 669 670fun tidy_up ind = ind 671 |> Q.SPEC `P` |> UNDISCH |> Q.SPEC `t` |> Q.GEN `t` |> DISCH_ALL |> Q.GEN `P`; 672 673Theorem ltree_finite_ind = tidy_up ltree_finite_ind; 674Theorem ltree_finite_strongind = tidy_up ltree_finite_strongind; 675 676Theorem ltree_finite: 677 ltree_finite (Branch a ts) <=> 678 LFINITE ts /\ !t. t IN LSET ts ==> ltree_finite t 679Proof 680 simp [Once ltree_finite_cases] 681 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq 682 \\ fs [LSET_def,IN_DEF,LNTH_fromList,PULL_EXISTS,LFINITE_fromList,EVERY_EL] 683QED 684 685Datatype: 686 rose_tree = Rose 'a (rose_tree list) 687End 688 689Definition from_rose_def: 690 from_rose (Rose a ts) = Branch a (fromList (MAP from_rose ts)) 691Termination 692 WF_REL_TAC `measure (rose_tree_size (K 0))` \\ rw [] 693 \\ qsuff_tac 694 `!a ts. MEM a ts ==> rose_tree_size (K 0) a <= rose_tree1_size (K 0) ts` 695 THEN1 (rw [] \\ res_tac \\ fs []) \\ rpt (pop_assum kall_tac) 696 \\ Induct_on `ts` \\ fs [] \\ rw [] \\ res_tac 697 \\ fs [fetch "-" "rose_tree_size_def"] 698End 699 700Theorem rose_tree_induction = from_rose_ind; 701 702Theorem ltree_finite_from_rose: 703 ltree_finite t <=> ?r. from_rose r = t 704Proof 705 eq_tac \\ qid_spec_tac `t` THEN1 706 (ho_match_mp_tac ltree_finite_ind \\ fs [EVERY_MEM] \\ rw [] 707 \\ qsuff_tac `?rs. ts = MAP from_rose rs` THEN1 708 (strip_tac \\ qexists_tac `Rose a rs` \\ fs [from_rose_def] 709 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs []) 710 \\ Induct_on `ts` \\ fs [] \\ rw [] 711 \\ first_assum (qspec_then `h` assume_tac) \\ fs [] 712 \\ qexists_tac `r::rs` \\ fs []) 713 \\ fs [PULL_EXISTS] 714 \\ ho_match_mp_tac from_rose_ind \\ rw [] 715 \\ once_rewrite_tac [ltree_finite_cases] 716 \\ fs [from_rose_def,Branch_11] 717 \\ CONV_TAC (DEPTH_CONV ETA_CONV) 718 \\ fs [EVERY_MEM,MEM_MAP,PULL_EXISTS] 719QED 720 721 722(* tidy up theory exports *) 723 724val _ = List.app Theory.delete_binding 725 ["Branch_rep_def", "dest_Branch_rep_def", "make_ltree_rep_def", 726 "make_unfold_def", "path_ok_def", "ltree_absrep", "ltree_absrep", 727 "gen_ltree_def", "ltree_rep_ok_def", "Branch", 728 "from_rose_def_primitive", "ltree_finite_def"]; 729 730val _ = export_theory(); 731