equal
deleted
inserted
replaced
429 apply(simp only: Left.simps Right.simps) |
429 apply(simp only: Left.simps Right.simps) |
430 apply(simp only: list_encode_inverse) |
430 apply(simp only: list_encode_inverse) |
431 apply(simp only: misc if_True) |
431 apply(simp only: misc if_True) |
432 apply(simp only: left_std[symmetric] right_std[symmetric]) |
432 apply(simp only: left_std[symmetric] right_std[symmetric]) |
433 apply(simp) |
433 apply(simp) |
434 apply(auto) |
434 by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc) |
435 apply(rule_tac x="ka - 1" in exI) |
435 |
436 apply(rule_tac x="l" in exI) |
|
437 apply(simp) |
|
438 apply (metis Suc_diff_le diff_Suc_Suc diff_zero replicate_Suc) |
|
439 apply(rule_tac x="n + 1" in exI) |
|
440 apply(simp) |
|
441 done |
|
442 |
436 |
443 lemma UF_simulate: |
437 lemma UF_simulate: |
444 assumes "tm_wf tm" |
438 assumes "tm_wf tm" |
445 shows "UF (Code_tprog tm) (Conf (Code_conf cf)) = |
439 shows "UF (Code_tprog tm) (Conf (Code_conf cf)) = |
446 Stknum (Right (Conf |
440 Stknum (Right (Conf |
663 |
657 |
664 lemma uf_lemma [simp]: |
658 lemma uf_lemma [simp]: |
665 "rec_eval rec_uf [m, cf] = UF m cf" |
659 "rec_eval rec_uf [m, cf] = UF m cf" |
666 by (simp add: rec_uf_def) |
660 by (simp add: rec_uf_def) |
667 |
661 |
668 |
662 value "size rec_uf" |
669 end |
663 end |
670 |
664 |