Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Abacus.thy
changeset 190 f1ecb4a68a54
parent 181 4d54702229fd
child 285 447b433b67fa
equal deleted inserted replaced
189:5974111de158 190:f1ecb4a68a54 
   145               (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
 
   145               (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
 
   146               (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
 
   146               (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
 
   147               (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
 
   147               (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
 
   148               (R, 0), (W0, 16)]"
 
   148               (R, 0), (W0, 16)]"
 
   149 
   149 
   150 text {*
 
       
   151   @{text "sete tp e"} attaches the termination edges (edges leading to state @{text "0"}) 
       
   152   of TM @{text "tp"} to the intruction labelled by @{text "e"}.
 
       
   153   *}
 
       
   154 
       
   155 fun sete :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
 
       
   156   where
 
       
   157   "sete tp e = map (\<lambda> (action, state). (action, if state = 0 then e else state)) tp"
 
       
   158 
   150 
   159 text {*
 
   151 text {*
 
   160   @{text "tdec ss n label"} returns the TM which simulates the execution of 
   152   @{text "tdec ss n label"} returns the TM which simulates the execution of 
   161   Abacus instruction @{text "Dec n label"}, assuming that TM is located at
 
   153   Abacus instruction @{text "Dec n label"}, assuming that TM is located at
 
   162   location @{text "ss"} in the final TM complied from the whole
 
   154   location @{text "ss"} in the final TM complied from the whole
 
   163   Abacus program.
 
   155   Abacus program.
 
   164 *}
 
   156 *}
 
   165 
   157 
   166 fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
 
   158 fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
 
   167   where
 
   159   where
 
   168   "tdec ss n e = shift (findnth n) (ss - 1) @ sete (shift (shift tdec_b (2 * n)) (ss - 1)) e"
 
   160   "tdec ss n e = shift (findnth n) (ss - 1) @ adjust (shift (shift tdec_b (2 * n)) (ss - 1)) e"
 
   169  
   161  
   170 text {*
 
   162 text {*
 
   171   @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction
 
   163   @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction
 
   172   @{text "Goto label"}, where @{text "f(label)"} is the corresponding location of
 
   164   @{text "Goto label"}, where @{text "f(label)"} is the corresponding location of
 
   173   @{text "label"} in the final TM compiled from the overall Abacus program.
 
   165   @{text "label"} in the final TM compiled from the overall Abacus program.
 
   253   "length (findnth n) = 4 * n"
 
   245   "length (findnth n) = 4 * n"
 
   254 by (induct n, auto)
 
   246 by (induct n, auto)
 
   255 
   247 
   256 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
 
   248 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
 
   257 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
 
   249 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
 
   258                  split: abc_inst.splits)
 
   250                  split: abc_inst.splits simp del: adjust.simps)
 
       
   251 
   259 done
 
   252 done
 
   260 
   253 
   261 subsection {* Representation of Abacus memory by TM tapes *}
 
   254 subsection {* Representation of Abacus memory by TM tapes *}
 
   262 
   255 
   263 text {*
 
   256 text {*
 
  2116     apply(auto simp: crsp.simps abc_step_l.simps fetch start_of_Suc1)
 
  2109     apply(auto simp: crsp.simps abc_step_l.simps fetch start_of_Suc1)
 
  2117     done
 
  2110     done
 
  2118 qed
 
  2111 qed
 
  2119     
  2112     
  2120 subsection{* Crsp of Dec n e*}
 
  2113 subsection{* Crsp of Dec n e*}
 
  2121 declare sete.simps[simp del]
 
  2114 declare adjust.simps[simp del]
 
  2122 
  2115 
  2123 type_synonym dec_inv_t = "(nat * nat list) \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow>  bool"
 
  2116 type_synonym dec_inv_t = "(nat * nat list) \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow>  bool"
 
  2124 
  2117 
  2125 fun dec_first_on_right_moving :: "nat \<Rightarrow> dec_inv_t"
 
  2118 fun dec_first_on_right_moving :: "nat \<Rightarrow> dec_inv_t"
 
  2126   where
 
  2119   where
 
  2221 
  2214 
  2222 declare fetch.simps[simp del]
 
  2215 declare fetch.simps[simp del]
 
  2223 lemma [simp]:
 
  2216 lemma [simp]:
 
  2224   "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1,  start_of ly as + 2 *n)"
 
  2217   "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1,  start_of ly as + 2 *n)"
 
  2225 apply(auto simp: fetch.simps length_ci_dec)
 
  2218 apply(auto simp: fetch.simps length_ci_dec)
 
  2226 apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def)
 
  2219 apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def)
 
  2227 using startof_not0[of ly as] by simp
 
  2220 using startof_not0[of ly as] by simp
 
  2228 
  2221 
  2229 lemma [simp]:
 
  2222 lemma [simp]:
 
  2230   "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R,  Suc (start_of ly as) + 2 *n)"
 
  2223   "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R,  Suc (start_of ly as) + 2 *n)"
 
  2231 apply(auto simp: fetch.simps length_ci_dec)
 
  2224 apply(auto simp: fetch.simps length_ci_dec)
 
  2232 apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def)
 
  2225 apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def)
 
  2233 done
 
  2226 done
 
  2234 
  2227 
  2235 lemma [simp]: 
  2228 lemma [simp]: 
  2236   "\<lbrakk>r = [] \<or> hd r = Bk; inv_locate_a (as, lm) (n, l, r) ires\<rbrakk>
 
  2229   "\<lbrakk>r = [] \<or> hd r = Bk; inv_locate_a (as, lm) (n, l, r) ires\<rbrakk>
 
  2237     \<Longrightarrow> \<exists>stp la ra.
 
  2230     \<Longrightarrow> \<exists>stp la ra.
 
  2377 done
 
  2370 done
 
  2378 
  2371 
  2379 lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
 
  2372 lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
 
  2380   = (R, start_of ly as + 2*n + 1)"
 
  2373   = (R, start_of ly as + 2*n + 1)"
 
  2381 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2374 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2382                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2375                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2383 done
 
  2376 done
 
  2384 
  2377 
  2385 lemma [simp]: "(start_of ly as = 0) = False"
 
  2378 lemma [simp]: "(start_of ly as = 0) = False"
 
  2386 apply(simp add: start_of.simps)
 
  2379 apply(simp add: start_of.simps)
 
  2387 done
 
  2380 done
 
  2388 
  2381 
  2389 lemma [simp]: "fetch (ci (ly) 
  2382 lemma [simp]: "fetch (ci (ly) 
  2390   (start_of ly as) (Dec n e)) (Suc (2 * n))  Bk
 
  2383   (start_of ly as) (Dec n e)) (Suc (2 * n))  Bk
 
  2391   = (W1, start_of ly as + 2*n)"
 
  2384   = (W1, start_of ly as + 2*n)"
 
  2392 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2385 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2393                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2386                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2394 done
 
  2387 done
 
  2395 
  2388 
  2396 lemma [simp]: 
  2389 lemma [simp]: 
  2397   "fetch (ci (ly) 
  2390   "fetch (ci (ly) 
  2398                 (start_of ly as) (Dec n e)) (Suc (Suc (2 * n)))  Oc
 
  2391                 (start_of ly as) (Dec n e)) (Suc (Suc (2 * n)))  Oc
 
  2399       = (R, start_of ly as + 2*n + 2)"
 
  2392       = (R, start_of ly as + 2*n + 2)"
 
  2400 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2393 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2401                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2394                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2402 done
 
  2395 done
 
  2403 
  2396 
  2404 
  2397 
  2405 lemma [simp]: "fetch (ci (ly) 
  2398 lemma [simp]: "fetch (ci (ly) 
  2406                   (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
 
  2399                   (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk
 
  2407       = (L, start_of ly as + 2*n + 13)"
 
  2400       = (L, start_of ly as + 2*n + 13)"
 
  2408 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2401 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2409                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2402                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2410 done
 
  2403 done
 
  2411 
  2404 
  2412 
  2405 
  2413 lemma [simp]: "fetch (ci (ly) 
  2406 lemma [simp]: "fetch (ci (ly) 
  2414              (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n))))  Oc
 
  2407              (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n))))  Oc
 
  2415      = (R, start_of ly as + 2*n + 2)"
 
  2408      = (R, start_of ly as + 2*n + 2)"
 
  2416 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2409 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2417                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2410                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2418 done
 
  2411 done
 
  2419 
  2412 
  2420 
  2413 
  2421 lemma [simp]: "fetch (ci (ly) (start_of ly as) (Dec n e)) 
  2414 lemma [simp]: "fetch (ci (ly) (start_of ly as) (Dec n e)) 
  2422                              (Suc (Suc (Suc (2 * n))))  Bk
 
  2415                              (Suc (Suc (Suc (2 * n))))  Bk
 
  2423      = (L, start_of ly as + 2*n + 3)"
 
  2416      = (L, start_of ly as + 2*n + 3)"
 
  2424 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2417 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2425                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2418                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2426 done
 
  2419 done
 
  2427 
  2420 
  2428 lemma [simp]:
 
  2421 lemma [simp]:
 
  2429      "fetch (ci (ly) 
  2422      "fetch (ci (ly) 
  2430                       (start_of ly as) (Dec n e)) (2 * n + 4) Oc
 
  2423                       (start_of ly as) (Dec n e)) (2 * n + 4) Oc
 
  2431     = (W0, start_of ly as + 2*n + 3)"
 
  2424     = (W0, start_of ly as + 2*n + 3)"
 
  2432 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
 
  2425 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
 
  2433 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2426 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2434                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2427                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2435 done
 
  2428 done
 
  2436 
  2429 
  2437 lemma [simp]: "fetch (ci (ly) 
  2430 lemma [simp]: "fetch (ci (ly) 
  2438                    (start_of ly as) (Dec n e)) (2 * n + 4) Bk
 
  2431                    (start_of ly as) (Dec n e)) (2 * n + 4) Bk
 
  2439     = (R, start_of ly as + 2*n + 4)"
 
  2432     = (R, start_of ly as + 2*n + 4)"
 
  2440 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
 
  2433 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
 
  2441 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2434 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2442                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2435                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2443 done
 
  2436 done
 
  2444 
  2437 
  2445 lemma [simp]:"fetch (ci (ly) 
  2438 lemma [simp]:"fetch (ci (ly) 
  2446                           (start_of ly as) (Dec n e)) (2 * n + 5) Bk
 
  2439                           (start_of ly as) (Dec n e)) (2 * n + 5) Bk
 
  2447     = (R, start_of ly as + 2*n + 5)"
 
  2440     = (R, start_of ly as + 2*n + 5)"
 
  2448 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
 
  2441 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
 
  2449 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2442 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2450                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2443                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2451 done
 
  2444 done
 
  2452 
  2445 
  2453 
  2446 
  2454 lemma [simp]: 
  2447 lemma [simp]: 
  2455   "fetch (ci (ly)
 
  2448   "fetch (ci (ly)
 
  2456                 (start_of ly as) (Dec n e)) (2 * n + 6) Bk
 
  2449                 (start_of ly as) (Dec n e)) (2 * n + 6) Bk
 
  2457     = (L, start_of ly as + 2*n + 6)"
 
  2450     = (L, start_of ly as + 2*n + 6)"
 
  2458 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
 
  2451 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
 
  2459 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2452 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2460                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2453                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2461 done
 
  2454 done
 
  2462 
  2455 
  2463 lemma [simp]: 
  2456 lemma [simp]: 
  2464   "fetch (ci (ly) (start_of ly as) 
  2457   "fetch (ci (ly) (start_of ly as) 
  2465                       (Dec n e)) (2 * n + 6) Oc
 
  2458                       (Dec n e)) (2 * n + 6) Oc
 
  2466     = (L, start_of ly as + 2*n + 7)"
 
  2459     = (L, start_of ly as + 2*n + 7)"
 
  2467 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
 
  2460 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
 
  2468 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2461 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2469                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2462                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2470 done
 
  2463 done
 
  2471 
  2464 
  2472 lemma [simp]:"fetch (ci (ly) 
  2465 lemma [simp]:"fetch (ci (ly) 
  2473              (start_of ly as) (Dec n e)) (2 * n + 7) Bk
 
  2466              (start_of ly as) (Dec n e)) (2 * n + 7) Bk
 
  2474     = (L, start_of ly as + 2*n + 10)"
 
  2467     = (L, start_of ly as + 2*n + 10)"
 
  2475 apply(subgoal_tac "2*n + 7 = Suc (2*n + 6)", simp only: fetch.simps)
 
  2468 apply(subgoal_tac "2*n + 7 = Suc (2*n + 6)", simp only: fetch.simps)
 
  2476 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2469 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2477                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2470                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2478 done
 
  2471 done
 
  2479 
  2472 
  2480 lemma [simp]:
 
  2473 lemma [simp]:
 
  2481   "fetch (ci (ly) 
  2474   "fetch (ci (ly) 
  2482                    (start_of ly as) (Dec n e)) (2 * n + 8) Bk
 
  2475                    (start_of ly as) (Dec n e)) (2 * n + 8) Bk
 
  2483     = (W1, start_of ly as + 2*n + 7)"
 
  2476     = (W1, start_of ly as + 2*n + 7)"
 
  2484 apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
 
  2477 apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
 
  2485 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2478 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2486                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2479                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2487 done
 
  2480 done
 
  2488 
  2481 
  2489 
  2482 
  2490 lemma [simp]: 
  2483 lemma [simp]: 
  2491   "fetch (ci (ly) 
  2484   "fetch (ci (ly) 
  2492                    (start_of ly as) (Dec n e)) (2 * n + 8) Oc
 
  2485                    (start_of ly as) (Dec n e)) (2 * n + 8) Oc
 
  2493     = (R, start_of ly as + 2*n + 8)"
 
  2486     = (R, start_of ly as + 2*n + 8)"
 
  2494 apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
 
  2487 apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps)
 
  2495 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2488 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2496                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2489                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2497 done
 
  2490 done
 
  2498 
  2491 
  2499 lemma [simp]: 
  2492 lemma [simp]: 
  2500   "fetch (ci (ly) 
  2493   "fetch (ci (ly) 
  2501   (start_of ly as) (Dec n e)) (2 * n + 9) Bk
 
  2494   (start_of ly as) (Dec n e)) (2 * n + 9) Bk
 
  2502   = (L, start_of ly as + 2*n + 9)"
 
  2495   = (L, start_of ly as + 2*n + 9)"
 
  2503 apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
 
  2496 apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
 
  2504 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2497 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2505                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2498                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2506 done
 
  2499 done
 
  2507 
  2500 
  2508 lemma [simp]: 
  2501 lemma [simp]: 
  2509   "fetch (ci (ly) 
  2502   "fetch (ci (ly) 
  2510   (start_of ly as) (Dec n e)) (2 * n + 9) Oc
 
  2503   (start_of ly as) (Dec n e)) (2 * n + 9) Oc
 
  2511   = (R, start_of ly as + 2*n + 8)"
 
  2504   = (R, start_of ly as + 2*n + 8)"
 
  2512 apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
 
  2505 apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps)
 
  2513 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2506 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2514                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2507                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2515 done
 
  2508 done
 
  2516 
  2509 
  2517 
  2510 
  2518 lemma [simp]: 
  2511 lemma [simp]: 
  2519   "fetch (ci (ly) 
  2512   "fetch (ci (ly) 
  2520   (start_of ly as) (Dec n e)) (2 * n + 10) Bk
 
  2513   (start_of ly as) (Dec n e)) (2 * n + 10) Bk
 
  2521   = (R, start_of ly as + 2*n + 4)" 
  2514   = (R, start_of ly as + 2*n + 4)" 
  2522 apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
 
  2515 apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
 
  2523 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2516 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2524                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2517                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2525 done
 
  2518 done
 
  2526 
  2519 
  2527 lemma [simp]: "fetch (ci (ly) 
  2520 lemma [simp]: "fetch (ci (ly) 
  2528              (start_of ly as) (Dec n e)) (2 * n + 10) Oc
 
  2521              (start_of ly as) (Dec n e)) (2 * n + 10) Oc
 
  2529     = (W0, start_of ly as + 2*n + 9)"
 
  2522     = (W0, start_of ly as + 2*n + 9)"
 
  2530 apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
 
  2523 apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps)
 
  2531 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2524 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2532                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2525                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2533 done
 
  2526 done
 
  2534 
  2527 
  2535 
  2528 
  2536 lemma [simp]: 
  2529 lemma [simp]: 
  2537   "fetch (ci (ly) 
  2530   "fetch (ci (ly) 
  2538   (start_of ly as) (Dec n e)) (2 * n + 11) Oc
 
  2531   (start_of ly as) (Dec n e)) (2 * n + 11) Oc
 
  2539   = (L, start_of ly as + 2*n + 10)"
 
  2532   = (L, start_of ly as + 2*n + 10)"
 
  2540 apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
 
  2533 apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
 
  2541 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2534 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2542                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2535                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2543 done
 
  2536 done
 
  2544 
  2537 
  2545 
  2538 
  2546 lemma [simp]: 
  2539 lemma [simp]: 
  2547   "fetch (ci (ly) 
  2540   "fetch (ci (ly) 
  2548   (start_of ly as) (Dec n e)) (2 * n + 11) Bk
 
  2541   (start_of ly as) (Dec n e)) (2 * n + 11) Bk
 
  2549   = (L, start_of ly as + 2*n + 11)"
 
  2542   = (L, start_of ly as + 2*n + 11)"
 
  2550 apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
 
  2543 apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps)
 
  2551 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2544 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2552                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2545                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2553 done
 
  2546 done
 
  2554 
  2547 
  2555 lemma [simp]:
 
  2548 lemma [simp]:
 
  2556   "fetch (ci (ly) 
  2549   "fetch (ci (ly) 
  2557   (start_of ly as) (Dec n e)) (2 * n + 12) Oc
 
  2550   (start_of ly as) (Dec n e)) (2 * n + 12) Oc
 
  2558   = (L, start_of ly as + 2*n + 10)"
 
  2551   = (L, start_of ly as + 2*n + 10)"
 
  2559 apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
 
  2552 apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
 
  2560 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2553 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2561                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2554                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2562 done
 
  2555 done
 
  2563 
  2556 
  2564 
  2557 
  2565 lemma [simp]: 
  2558 lemma [simp]: 
  2566   "fetch (ci (ly) 
  2559   "fetch (ci (ly) 
  2567   (start_of ly as) (Dec n e)) (2 * n + 12) Bk
 
  2560   (start_of ly as) (Dec n e)) (2 * n + 12) Bk
 
  2568   = (R, start_of ly as + 2*n + 12)"
 
  2561   = (R, start_of ly as + 2*n + 12)"
 
  2569 apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
 
  2562 apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps)
 
  2570 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2563 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2571                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2564                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2572 done
 
  2565 done
 
  2573 
  2566 
  2574 lemma [simp]: 
  2567 lemma [simp]: 
  2575   "fetch (ci (ly) 
  2568   "fetch (ci (ly) 
  2576   (start_of ly as) (Dec n e)) (2 * n + 13) Bk
 
  2569   (start_of ly as) (Dec n e)) (2 * n + 13) Bk
 
  2577   = (R, start_of ly as + 2*n + 16)"
 
  2570   = (R, start_of ly as + 2*n + 16)"
 
  2578 apply(subgoal_tac "2*n + 13 = Suc (2*n + 12)", simp only: fetch.simps)
 
  2571 apply(subgoal_tac "2*n + 13 = Suc (2*n + 12)", simp only: fetch.simps)
 
  2579 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2572 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2580                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2573                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2581 done
 
  2574 done
 
  2582 
  2575 
  2583 
  2576 
  2584 lemma [simp]: 
  2577 lemma [simp]: 
  2585   "fetch (ci (ly) 
  2578   "fetch (ci (ly) 
  2586   (start_of ly as) (Dec n e)) (14 + 2 * n) Oc
 
  2579   (start_of ly as) (Dec n e)) (14 + 2 * n) Oc
 
  2587   = (L, start_of ly as + 2*n + 13)"
 
  2580   = (L, start_of ly as + 2*n + 13)"
 
  2588 apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
 
  2581 apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
 
  2589 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2582 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2590                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2583                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2591 done
 
  2584 done
 
  2592 
  2585 
  2593 lemma [simp]: 
  2586 lemma [simp]: 
  2594   "fetch (ci (ly) 
  2587   "fetch (ci (ly) 
  2595   (start_of ly as) (Dec n e)) (14 + 2 * n) Bk
 
  2588   (start_of ly as) (Dec n e)) (14 + 2 * n) Bk
 
  2596   = (L, start_of ly as + 2*n + 14)"
 
  2589   = (L, start_of ly as + 2*n + 14)"
 
  2597 apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
 
  2590 apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps)
 
  2598 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2591 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2599                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2592                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2600 done
 
  2593 done
 
  2601 
  2594 
  2602 lemma [simp]: 
  2595 lemma [simp]: 
  2603   "fetch (ci (ly) 
  2596   "fetch (ci (ly) 
  2604   (start_of ly as) (Dec n e)) (15 + 2 * n)  Oc
 
  2597   (start_of ly as) (Dec n e)) (15 + 2 * n)  Oc
 
  2605   = (L, start_of ly as + 2*n + 13)"
 
  2598   = (L, start_of ly as + 2*n + 13)"
 
  2606 apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
 
  2599 apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
 
  2607 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2600 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2608                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2601                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2609 done
 
  2602 done
 
  2610 
  2603 
  2611 lemma [simp]: 
  2604 lemma [simp]: 
  2612   "fetch (ci (ly) 
  2605   "fetch (ci (ly) 
  2613   (start_of ly as) (Dec n e)) (15 + 2 * n)  Bk
 
  2606   (start_of ly as) (Dec n e)) (15 + 2 * n)  Bk
 
  2614  = (R, start_of ly as + 2*n + 15)"
 
  2607  = (R, start_of ly as + 2*n + 15)"
 
  2615 apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
 
  2608 apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps)
 
  2616 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2609 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2617                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2610                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2618 done
 
  2611 done
 
  2619 
  2612 
  2620 lemma [simp]: 
  2613 lemma [simp]: 
  2621   "abc_fetch as aprog = Some (Dec n e) \<Longrightarrow> 
  2614   "abc_fetch as aprog = Some (Dec n e) \<Longrightarrow> 
  2622      fetch (ci (ly) (start_of (ly) as) 
  2615      fetch (ci (ly) (start_of (ly) as) 
  2623               (Dec n e)) (16 + 2 * n)  Bk
 
  2616               (Dec n e)) (16 + 2 * n)  Bk
 
  2624  = (R, start_of (ly) e)"
 
  2617  = (R, start_of (ly) e)"
 
  2625 apply(subgoal_tac "16 + 2*n = Suc (2*n + 15)", simp only: fetch.simps)
 
  2618 apply(subgoal_tac "16 + 2*n = Suc (2*n + 15)", simp only: fetch.simps)
 
  2626 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2619 apply(auto simp: ci.simps findnth.simps fetch.simps
 
  2627                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps)
 
  2620                   nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
 
  2628 done
 
  2621 done
 
  2629 
  2622 
  2630 declare dec_inv_1.simps[simp del]
 
  2623 declare dec_inv_1.simps[simp del]
 
  2631 
  2624 
  2632 
  2625 
  3531   shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
 
  3524   shows "\<exists>stp > 0. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
 
  3532   (steps (s, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
 
  3525   (steps (s, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
 
  3533 proof(simp add: ci.simps)
 
  3526 proof(simp add: ci.simps)
 
  3534   let ?off = "start_of ly as - Suc 0"
 
  3527   let ?off = "start_of ly as - Suc 0"
 
  3535   let ?A = "findnth n"
 
  3528   let ?A = "findnth n"
 
  3536   let ?B = "sete (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)"
 
  3529   let ?B = "adjust (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)"
 
  3537   have "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra)
 
  3530   have "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra)
 
  3538                     \<and> inv_locate_a (as, lm) (n, la, ra) ires"
 
  3531                     \<and> inv_locate_a (as, lm) (n, la, ra) ires"
 
  3539   proof -
 
  3532   proof -
 
  3540     have "\<exists>stp l' r'. steps (Suc 0, l, r) (?A, 0) stp = (Suc (2 * n), l', r') \<and> 
  3533     have "\<exists>stp l' r'. steps (Suc 0, l, r) (?A, 0) stp = (Suc (2 * n), l', r') \<and> 
  3541                      inv_locate_a (as, lm) (n, l', r') ires"
 
  3534                      inv_locate_a (as, lm) (n, l', r') ires"
 
  3691 
  3684 
  3692 lemma map_length_ci:
 
  3685 lemma map_length_ci:
 
  3693   "(map (length \<circ> (\<lambda>(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) = 
  3686   "(map (length \<circ> (\<lambda>(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) = 
  3694   (map (length \<circ> (\<lambda>(x, y). ci (layout_of xs) x y)) (tpairs_of xs)) "
 
  3687   (map (length \<circ> (\<lambda>(x, y). ci (layout_of xs) x y)) (tpairs_of xs)) "
 
  3695 apply(auto)
 
  3688 apply(auto)
 
  3696 apply(case_tac b, auto simp: ci.simps sete.simps)
 
  3689 apply(case_tac b, auto simp: ci.simps adjust.simps)
 
  3697 done
 
  3690 done
 
  3698 
  3691 
  3699 lemma length_tp'[simp]: 
  3692 lemma length_tp'[simp]: 
  3700   "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
 
  3693   "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
 
  3701        length tp = 2 * listsum (take (length ap) (layout_of ap))"
 
  3694        length tp = 2 * listsum (take (length ap) (layout_of ap))"
 
  3719   thus "length tp = 2 * 
  3712   thus "length tp = 2 * 
  3720     listsum (take (length (xs @ [x])) (layout_of (xs @ [x])))"
 
  3713     listsum (take (length (xs @ [x])) (layout_of (xs @ [x])))"
 
  3721     using tp b
 
  3714     using tp b
 
  3722     apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci)
 
  3715     apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci)
 
  3723     apply(case_tac x)
 
  3716     apply(case_tac x)
 
  3724     apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth sete.simps length_of.simps
 
  3717     apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps
 
  3725                  split: abc_inst.splits)
 
  3718                  split: abc_inst.splits)
 
  3726     done
 
  3719     done
 
  3727 qed
 
  3720 qed
 
  3728 
  3721 
  3729 lemma [simp]: 
  3722 lemma [simp]:
tm