369 |
338 |
370 |
339 |
371 definition |
340 definition |
372 "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]" |
341 "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]" |
373 |
342 |
|
343 text {* |
|
344 The correctness of @{text "rec_uf"}, nonhalt case. |
|
345 *} |
|
346 |
|
347 subsection {* Coding function of TMs *} |
|
348 |
|
349 text {* |
|
350 The purpose of this section is to get the coding function of Turing Machine, |
|
351 which is going to be named @{text "code"}. |
|
352 *} |
|
353 |
|
354 fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat" |
|
355 where |
|
356 "bl2nat [] n = 0" |
|
357 | "bl2nat (Bk # bl) n = bl2nat bl (Suc n)" |
|
358 | "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)" |
|
359 |
|
360 fun bl2wc :: "cell list \<Rightarrow> nat" |
|
361 where |
|
362 "bl2wc xs = bl2nat xs 0" |
|
363 |
|
364 fun trpl_code :: "config \<Rightarrow> nat" |
|
365 where |
|
366 "trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)" |
|
367 |
|
368 fun action_map :: "action \<Rightarrow> nat" |
|
369 where |
|
370 "action_map W0 = 0" |
|
371 | "action_map W1 = 1" |
|
372 | "action_map L = 2" |
|
373 | "action_map R = 3" |
|
374 | "action_map Nop = 4" |
|
375 |
|
376 fun action_map_iff :: "nat \<Rightarrow> action" |
|
377 where |
|
378 "action_map_iff (0::nat) = W0" |
|
379 | "action_map_iff (Suc 0) = W1" |
|
380 | "action_map_iff (Suc (Suc 0)) = L" |
|
381 | "action_map_iff (Suc (Suc (Suc 0))) = R" |
|
382 | "action_map_iff n = Nop" |
|
383 |
|
384 fun block_map :: "cell \<Rightarrow> nat" |
|
385 where |
|
386 "block_map Bk = 0" |
|
387 | "block_map Oc = 1" |
|
388 |
|
389 fun Goedel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat" |
|
390 where |
|
391 "Goedel_code' [] n = 1" |
|
392 | "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) " |
|
393 |
|
394 fun Goedel_code :: "nat list \<Rightarrow> nat" |
|
395 where |
|
396 "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)" |
|
397 |
|
398 fun modify_tprog :: "instr list \<Rightarrow> nat list" |
|
399 where |
|
400 "modify_tprog [] = []" |
|
401 | "modify_tprog ((a, s) # nl) = action_map a # s # modify_tprog nl" |
|
402 |
|
403 text {* @{text "Code tp"} gives the Goedel coding of TM program @{text "tp"}. *} |
|
404 fun Code :: "instr list \<Rightarrow> nat" |
|
405 where |
|
406 "Code tp = Goedel_code (modify_tprog tp)" |
|
407 |
|
408 subsection {* Relating interperter functions to the execution of TMs *} |
|
409 |
|
410 |
|
411 lemma F_correct: |
|
412 assumes tp: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)" |
|
413 and wf: "tm_wf0 tp" "0 < rs" |
|
414 shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)" |
|
415 |
|
416 |
374 end |
417 end |
375 |
418 |
376 |
|
377 (* |
|
378 |
|
379 |
|
380 |
|
381 fun mtest where |
|
382 "mtest R 0 = if R 0 then 0 else 1" |
|
383 | "mtest R (Suc n) = (if R n then mtest R n else (Suc n))" |
|
384 |
|
385 |
|
386 lemma |
|
387 "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX" |
|
388 apply(simp only: rec_maxr2_def) |
|
389 apply(case_tac x) |
|
390 apply(clarify) |
|
391 apply(subst rec_eval.simps) |
|
392 apply(simp only: constn_lemma) |
|
393 defer |
|
394 apply(clarify) |
|
395 apply(subst rec_eval.simps) |
|
396 apply(simp only: rec_maxr2_def[symmetric]) |
|
397 apply(subst rec_eval.simps) |
|
398 apply(simp only: map.simps nth) |
|
399 apply(subst rec_eval.simps) |
|
400 apply(simp only: map.simps nth) |
|
401 apply(subst rec_eval.simps) |
|
402 apply(simp only: map.simps nth) |
|
403 apply(subst rec_eval.simps) |
|
404 apply(simp only: map.simps nth) |
|
405 apply(subst rec_eval.simps) |
|
406 apply(simp only: map.simps nth) |
|
407 apply(subst rec_eval.simps) |
|
408 apply(simp only: map.simps nth) |
|
409 |
|
410 |
|
411 definition |
|
412 "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))" |
|
413 |
|
414 definition |
|
415 "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])" |
|
416 |
|
417 definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat" |
|
418 where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})" |
|
419 |
|
420 definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat" |
|
421 where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})" |
|
422 |
|
423 lemma rec_minr2_le_Suc: |
|
424 "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x" |
|
425 apply(simp add: rec_minr2_def) |
|
426 apply(auto intro!: setsum_one_le setprod_one_le) |
|
427 done |
|
428 |
|
429 lemma rec_minr2_eq_Suc: |
|
430 assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0" |
|
431 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x" |
|
432 using assms by (simp add: rec_minr2_def) |
|
433 |
|
434 lemma rec_minr2_le: |
|
435 assumes h1: "y \<le> x" |
|
436 and h2: "0 < rec_eval f [y, y1, y2]" |
|
437 shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y" |
|
438 apply(simp add: rec_minr2_def) |
|
439 apply(subst setsum_cut_off_le[OF h1]) |
|
440 using h2 apply(auto) |
|
441 apply(auto intro!: setsum_one_less setprod_one_le) |
|
442 done |
|
443 |
|
444 (* ??? *) |
|
445 lemma setsum_eq_one_le2: |
|
446 fixes n::nat |
|
447 assumes "\<forall>i \<le> n. f i \<le> 1" |
|
448 shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)" |
|
449 using assms |
|
450 apply(induct n) |
|
451 apply(simp add: One_nat_def) |
|
452 apply(simp) |
|
453 apply(auto simp add: One_nat_def) |
|
454 apply(drule_tac x="Suc n" in spec) |
|
455 apply(auto) |
|
456 by (metis le_Suc_eq) |
|
457 |
|
458 |
|
459 lemma rec_min2_not: |
|
460 assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x" |
|
461 shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0" |
|
462 using assms |
|
463 apply(simp add: rec_minr2_def) |
|
464 apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)") |
|
465 apply(simp) |
|
466 apply (metis atMost_iff le_refl zero_neq_one) |
|
467 apply(rule setsum_eq_one_le2) |
|
468 apply(auto) |
|
469 apply(rule setprod_one_le) |
|
470 apply(auto) |
|
471 done |
|
472 |
|
473 lemma disjCI2: |
|
474 assumes "~P ==> Q" shows "P|Q" |
|
475 apply (rule classical) |
|
476 apply (iprover intro: assms disjI1 disjI2 notI elim: notE) |
|
477 done |
|
478 |
|
479 lemma minr_lemma [simp]: |
|
480 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)" |
|
481 apply(induct x) |
|
482 apply(rule Least_equality[symmetric]) |
|
483 apply(simp add: rec_minr2_def) |
|
484 apply(erule disjE) |
|
485 apply(rule rec_minr2_le) |
|
486 apply(auto)[2] |
|
487 apply(simp) |
|
488 apply(rule rec_minr2_le_Suc) |
|
489 apply(simp) |
|
490 |
|
491 apply(rule rec_minr2_le) |
|
492 |
|
493 |
|
494 apply(rule rec_minr2_le_Suc) |
|
495 apply(rule disjCI) |
|
496 apply(simp add: rec_minr2_def) |
|
497 |
|
498 apply(ru le setsum_one_less) |
|
499 apply(clarify) |
|
500 apply(rule setprod_one_le) |
|
501 apply(auto)[1] |
|
502 apply(simp) |
|
503 apply(rule setsum_one_le) |
|
504 apply(clarify) |
|
505 apply(rule setprod_one_le) |
|
506 apply(auto)[1] |
|
507 thm disj_CE |
|
508 apply(auto) |
|
509 |
|
510 lemma minr_lemma: |
|
511 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]" |
|
512 apply(simp only: Minr_def) |
|
513 apply(rule sym) |
|
514 apply(rule Min_eqI) |
|
515 apply(auto)[1] |
|
516 apply(simp) |
|
517 apply(erule disjE) |
|
518 apply(simp) |
|
519 apply(rule rec_minr2_le_Suc) |
|
520 apply(rule rec_minr2_le) |
|
521 apply(auto)[2] |
|
522 apply(simp) |
|
523 apply(induct x) |
|
524 apply(simp add: rec_minr2_def) |
|
525 apply( |
|
526 apply(rule disjCI) |
|
527 apply(rule rec_minr2_eq_Suc) |
|
528 apply(simp) |
|
529 apply(auto) |
|
530 |
|
531 apply(rule setsum_one_le) |
|
532 apply(auto)[1] |
|
533 apply(rule setprod_one_le) |
|
534 apply(auto)[1] |
|
535 apply(subst setsum_cut_off_le) |
|
536 apply(auto)[2] |
|
537 apply(rule setsum_one_less) |
|
538 apply(auto)[1] |
|
539 apply(rule setprod_one_le) |
|
540 apply(auto)[1] |
|
541 apply(simp) |
|
542 thm setsum_eq_one_le |
|
543 apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or> |
|
544 (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") |
|
545 prefer 2 |
|
546 apply(auto)[1] |
|
547 apply(erule disjE) |
|
548 apply(rule disjI1) |
|
549 apply(rule setsum_eq_one_le) |
|
550 apply(simp) |
|
551 apply(rule disjI2) |
|
552 apply(simp) |
|
553 apply(clarify) |
|
554 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
555 defer |
|
556 apply metis |
|
557 apply(erule exE) |
|
558 apply(subgoal_tac "l \<le> x") |
|
559 defer |
|
560 apply (metis not_leE not_less_Least order_trans) |
|
561 apply(subst setsum_least_eq) |
|
562 apply(rotate_tac 4) |
|
563 apply(assumption) |
|
564 apply(auto)[1] |
|
565 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
566 prefer 2 |
|
567 apply(auto)[1] |
|
568 apply(rotate_tac 5) |
|
569 apply(drule not_less_Least) |
|
570 apply(auto)[1] |
|
571 apply(auto) |
|
572 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) |
|
573 apply(simp) |
|
574 apply (metis LeastI_ex) |
|
575 apply(subst setsum_least_eq) |
|
576 apply(rotate_tac 3) |
|
577 apply(assumption) |
|
578 apply(simp) |
|
579 apply(auto)[1] |
|
580 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
581 prefer 2 |
|
582 apply(auto)[1] |
|
583 apply (metis neq0_conv not_less_Least) |
|
584 apply(auto)[1] |
|
585 apply (metis (mono_tags) LeastI_ex) |
|
586 by (metis LeastI_ex) |
|
587 |
|
588 lemma minr_lemma: |
|
589 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]" |
|
590 apply(simp only: Minr_def rec_minr2_def) |
|
591 apply(simp) |
|
592 apply(rule sym) |
|
593 apply(rule Min_eqI) |
|
594 apply(auto)[1] |
|
595 apply(simp) |
|
596 apply(erule disjE) |
|
597 apply(simp) |
|
598 apply(rule setsum_one_le) |
|
599 apply(auto)[1] |
|
600 apply(rule setprod_one_le) |
|
601 apply(auto)[1] |
|
602 apply(subst setsum_cut_off_le) |
|
603 apply(auto)[2] |
|
604 apply(rule setsum_one_less) |
|
605 apply(auto)[1] |
|
606 apply(rule setprod_one_le) |
|
607 apply(auto)[1] |
|
608 apply(simp) |
|
609 thm setsum_eq_one_le |
|
610 apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or> |
|
611 (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") |
|
612 prefer 2 |
|
613 apply(auto)[1] |
|
614 apply(erule disjE) |
|
615 apply(rule disjI1) |
|
616 apply(rule setsum_eq_one_le) |
|
617 apply(simp) |
|
618 apply(rule disjI2) |
|
619 apply(simp) |
|
620 apply(clarify) |
|
621 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
622 defer |
|
623 apply metis |
|
624 apply(erule exE) |
|
625 apply(subgoal_tac "l \<le> x") |
|
626 defer |
|
627 apply (metis not_leE not_less_Least order_trans) |
|
628 apply(subst setsum_least_eq) |
|
629 apply(rotate_tac 4) |
|
630 apply(assumption) |
|
631 apply(auto)[1] |
|
632 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
633 prefer 2 |
|
634 apply(auto)[1] |
|
635 apply(rotate_tac 5) |
|
636 apply(drule not_less_Least) |
|
637 apply(auto)[1] |
|
638 apply(auto) |
|
639 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) |
|
640 apply(simp) |
|
641 apply (metis LeastI_ex) |
|
642 apply(subst setsum_least_eq) |
|
643 apply(rotate_tac 3) |
|
644 apply(assumption) |
|
645 apply(simp) |
|
646 apply(auto)[1] |
|
647 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
648 prefer 2 |
|
649 apply(auto)[1] |
|
650 apply (metis neq0_conv not_less_Least) |
|
651 apply(auto)[1] |
|
652 apply (metis (mono_tags) LeastI_ex) |
|
653 by (metis LeastI_ex) |
|
654 |
|
655 lemma disjCI2: |
|
656 assumes "~P ==> Q" shows "P|Q" |
|
657 apply (rule classical) |
|
658 apply (iprover intro: assms disjI1 disjI2 notI elim: notE) |
|
659 done |
|
660 |
|
661 |
|
662 lemma minr_lemma [simp]: |
|
663 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)" |
|
664 (*apply(simp add: rec_minr2_def)*) |
|
665 apply(rule Least_equality[symmetric]) |
|
666 prefer 2 |
|
667 apply(erule disjE) |
|
668 apply(rule rec_minr2_le) |
|
669 apply(auto)[2] |
|
670 apply(clarify) |
|
671 apply(rule rec_minr2_le_Suc) |
|
672 apply(rule disjCI) |
|
673 apply(simp add: rec_minr2_def) |
|
674 |
|
675 apply(ru le setsum_one_less) |
|
676 apply(clarify) |
|
677 apply(rule setprod_one_le) |
|
678 apply(auto)[1] |
|
679 apply(simp) |
|
680 apply(rule setsum_one_le) |
|
681 apply(clarify) |
|
682 apply(rule setprod_one_le) |
|
683 apply(auto)[1] |
|
684 thm disj_CE |
|
685 apply(auto) |
|
686 apply(auto) |
|
687 prefer 2 |
|
688 apply(rule le_tran |
|
689 |
|
690 apply(rule le_trans) |
|
691 apply(simp) |
|
692 defer |
|
693 apply(auto) |
|
694 apply(subst setsum_cut_off_le) |
|
695 |
|
696 |
|
697 lemma |
|
698 "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))" |
|
699 apply(simp add: Minr_def) |
|
700 apply(rule Min_eqI) |
|
701 apply(auto)[1] |
|
702 apply(simp) |
|
703 apply(rule Least_le) |
|
704 apply(auto)[1] |
|
705 apply(rule LeastI2_wellorder) |
|
706 apply(auto) |
|
707 done |
|
708 |
|
709 definition (in ord) |
|
710 Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where |
|
711 "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))" |
|
712 |
|
713 (* |
|
714 lemma Great_equality: |
|
715 assumes "P x" |
|
716 and "\<And>y. P y \<Longrightarrow> y \<le> x" |
|
717 shows "Great P = x" |
|
718 unfolding Great_def |
|
719 apply(rule the_equality) |
|
720 apply(blast intro: assms) |
|
721 *) |
|
722 |
|
723 |
|
724 |
|
725 lemma |
|
726 "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))" |
|
727 apply(simp add: Maxr_def) |
|
728 apply(rule Max_eqI) |
|
729 apply(auto)[1] |
|
730 apply(simp) |
|
731 thm Least_le Greatest_le |
|
732 oops |
|
733 |
|
734 lemma |
|
735 "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys" |
|
736 apply(simp add: Maxr_def Minr_def) |
|
737 apply(rule Max_eqI) |
|
738 apply(auto)[1] |
|
739 apply(simp) |
|
740 apply(erule disjE) |
|
741 apply(simp) |
|
742 apply(auto)[1] |
|
743 defer |
|
744 apply(simp) |
|
745 apply(auto)[1] |
|
746 thm Min_insert |
|
747 defer |
|
748 oops |
|
749 |
|
750 |
|
751 |
|
752 definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
753 where |
|
754 "quo x y = (if y = 0 then 0 else x div y)" |
|
755 |
|
756 |
|
757 definition |
|
758 "rec_quo = CN rec_mult [CN rec_sign [Id 2 1], |
|
759 CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]])) |
|
760 [Id 2 0, Id 2 0, Id 2 1]]" |
|
761 |
|
762 lemma div_lemma [simp]: |
|
763 "rec_eval rec_quo [x, y] = quo x y" |
|
764 apply(simp add: rec_quo_def quo_def) |
|
765 apply(rule impI) |
|
766 apply(rule Min_eqI) |
|
767 apply(auto)[1] |
|
768 apply(simp) |
|
769 apply(erule disjE) |
|
770 apply(simp) |
|
771 apply(auto)[1] |
|
772 apply (metis div_le_dividend le_SucI) |
|
773 defer |
|
774 apply(simp) |
|
775 apply(auto)[1] |
|
776 apply (metis mult_Suc_right nat_mult_commute split_div_lemma) |
|
777 apply(auto)[1] |
|
778 |
|
779 apply (smt div_le_dividend fst_divmod_nat) |
|
780 apply(simp add: quo_def) |
|
781 apply(auto)[1] |
|
782 |
|
783 apply(auto) |
|
784 |
|
785 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
786 where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
|
787 if (setx = {}) then (Suc x) else (Min setx))" |
|
788 |
|
789 definition |
|
790 "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))" |
|
791 |
|
792 lemma minr_lemma [simp]: |
|
793 shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y" |
|
794 apply(simp only: rec_minr_def) |
|
795 apply(simp only: sigma1_lemma) |
|
796 apply(simp only: accum1_lemma) |
|
797 apply(subst rec_eval.simps) |
|
798 apply(simp only: map.simps nth) |
|
799 apply(simp only: Minr.simps Let_def) |
|
800 apply(auto simp del: not_lemma) |
|
801 apply(simp) |
|
802 apply(simp only: not_lemma sign_lemma) |
|
803 apply(rule sym) |
|
804 apply(rule Min_eqI) |
|
805 apply(auto)[1] |
|
806 apply(simp) |
|
807 apply(subst setsum_cut_off_le[where m="ya"]) |
|
808 apply(simp) |
|
809 apply(simp) |
|
810 apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) |
|
811 apply(rule setsum_one_less) |
|
812 apply(default) |
|
813 apply(rule impI) |
|
814 apply(rule setprod_one_le) |
|
815 apply(auto split: if_splits)[1] |
|
816 apply(simp) |
|
817 apply(rule conjI) |
|
818 apply(subst setsum_cut_off_le[where m="xa"]) |
|
819 apply(simp) |
|
820 apply(simp) |
|
821 apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) |
|
822 apply(rule le_trans) |
|
823 apply(rule setsum_one_less) |
|
824 apply(default) |
|
825 apply(rule impI) |
|
826 apply(rule setprod_one_le) |
|
827 apply(auto split: if_splits)[1] |
|
828 apply(simp) |
|
829 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])") |
|
830 defer |
|
831 apply metis |
|
832 apply(erule exE) |
|
833 apply(subgoal_tac "l \<le> x") |
|
834 defer |
|
835 apply (metis not_leE not_less_Least order_trans) |
|
836 apply(subst setsum_least_eq) |
|
837 apply(rotate_tac 3) |
|
838 apply(assumption) |
|
839 prefer 3 |
|
840 apply (metis LeastI_ex) |
|
841 apply(auto)[1] |
|
842 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])") |
|
843 prefer 2 |
|
844 apply(auto)[1] |
|
845 apply(rotate_tac 5) |
|
846 apply(drule not_less_Least) |
|
847 apply(auto)[1] |
|
848 apply(auto) |
|
849 by (metis (mono_tags) LeastI_ex) |
|
850 |
|
851 |
|
852 fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
853 where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
|
854 Min (setx \<union> {Suc x}))" |
|
855 |
|
856 lemma Minr2_Minr: |
|
857 "Minr2 R x y = Minr R x y" |
|
858 apply(auto) |
|
859 apply (metis (lifting, no_types) Min_singleton empty_Collect_eq) |
|
860 apply(rule min_absorb2) |
|
861 apply(subst Min_le_iff) |
|
862 apply(auto) |
|
863 done |
|
864 *) |
|