18 section {* Universal Function *} |
18 section {* Universal Function *} |
19 |
19 |
20 subsection {* The construction of component functions *} |
20 subsection {* The construction of component functions *} |
21 |
21 |
22 text {* |
22 text {* |
23 The recursive function used to do arithmatic addition. |
23 The recursive function used to do arithmetic addition. |
24 *} |
24 *} |
25 definition rec_add :: "recf" |
25 definition rec_add :: "recf" |
26 where |
26 where |
27 "rec_add \<equiv> Pr 1 (id 1 0) (Cn 3 s [id 3 2])" |
27 "rec_add \<equiv> Pr 1 (id 1 0) (Cn 3 s [id 3 2])" |
28 |
28 |
29 text {* |
29 text {* |
30 The recursive function used to do arithmatic multiplication. |
30 The recursive function used to do arithmetic multiplication. |
31 *} |
31 *} |
32 definition rec_mult :: "recf" |
32 definition rec_mult :: "recf" |
33 where |
33 where |
34 "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])" |
34 "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])" |
35 |
35 |
36 text {* |
36 text {* |
37 The recursive function used to do arithmatic precede. |
37 The recursive function used to do arithmetic precede. |
38 *} |
38 *} |
39 definition rec_pred :: "recf" |
39 definition rec_pred :: "recf" |
40 where |
40 where |
41 "rec_pred = Cn 1 (Pr 1 z (id 3 1)) [id 1 0, id 1 0]" |
41 "rec_pred = Cn 1 (Pr 1 z (id 3 1)) [id 1 0, id 1 0]" |
42 |
42 |
43 text {* |
43 text {* |
44 The recursive function used to do arithmatic subtraction. |
44 The recursive function used to do arithmetic subtraction. |
45 *} |
45 *} |
46 definition rec_minus :: "recf" |
46 definition rec_minus :: "recf" |
47 where |
47 where |
48 "rec_minus = Pr 1 (id 1 0) (Cn 3 rec_pred [id 3 2])" |
48 "rec_minus = Pr 1 (id 1 0) (Cn 3 rec_pred [id 3 2])" |
49 |
49 |
287 |
287 |
288 declare rec_exec.simps[simp del] get_fstn_args.simps[simp del] |
288 declare rec_exec.simps[simp del] get_fstn_args.simps[simp del] |
289 arity.simps[simp del] Sigma.simps[simp del] |
289 arity.simps[simp del] Sigma.simps[simp del] |
290 rec_sigma.simps[simp del] |
290 rec_sigma.simps[simp del] |
291 |
291 |
292 lemma rec_pr_0_simp_rewrite: " |
|
293 rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs" |
|
294 by(simp add: rec_exec.simps) |
|
295 |
|
296 lemma rec_pr_0_simp_rewrite_single_param: " |
|
297 rec_exec (Pr n f g) [0] = rec_exec f []" |
|
298 by(simp add: rec_exec.simps) |
|
299 |
|
300 lemma rec_pr_Suc_simp_rewrite: |
292 lemma rec_pr_Suc_simp_rewrite: |
301 "rec_exec (Pr n f g) (xs @ [Suc x]) = |
293 "rec_exec (Pr n f g) (xs @ [Suc x]) = |
302 rec_exec g (xs @ [x] @ |
294 rec_exec g (xs @ [x] @ |
303 [rec_exec (Pr n f g) (xs @ [x])])" |
295 [rec_exec (Pr n f g) (xs @ [x])])" |
304 by(simp add: rec_exec.simps) |
296 by(simp add: rec_exec.simps) |
305 |
297 |
306 lemma rec_pr_Suc_simp_rewrite_single_param: |
|
307 "rec_exec (Pr n f g) ([Suc x]) = |
|
308 rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])" |
|
309 by(simp add: rec_exec.simps) |
|
310 |
|
311 lemma Sigma_0_simp_rewrite_single_param: |
|
312 "Sigma f [0] = f [0]" |
|
313 by(simp add: Sigma.simps) |
|
314 |
|
315 lemma Sigma_0_simp_rewrite: |
298 lemma Sigma_0_simp_rewrite: |
316 "Sigma f (xs @ [0]) = f (xs @ [0])" |
299 "Sigma f (xs @ [0]) = f (xs @ [0])" |
317 by(simp add: Sigma.simps) |
300 by(simp add: Sigma.simps) |
318 |
301 |
319 lemma Sigma_Suc_simp_rewrite: |
302 lemma Sigma_Suc_simp_rewrite: |
320 "Sigma f (xs @ [Suc x]) = Sigma f (xs @ [x]) + f (xs @ [Suc x])" |
303 "Sigma f (xs @ [Suc x]) = Sigma f (xs @ [x]) + f (xs @ [Suc x])" |
321 by(simp add: Sigma.simps) |
304 by(simp add: Sigma.simps) |
322 |
305 |
323 lemma Sigma_Suc_simp_rewrite_single: |
306 lemma append_access_1[simp]: "(xs @ ys) ! (Suc (length xs)) = ys ! 1" |
324 "Sigma f ([Suc x]) = Sigma f ([x]) + f ([Suc x])" |
|
325 by(simp add: Sigma.simps) |
|
326 |
|
327 lemma [simp]: "(xs @ ys) ! (Suc (length xs)) = ys ! 1" |
|
328 by(simp add: nth_append) |
307 by(simp add: nth_append) |
329 |
308 |
330 lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow> |
309 lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow> |
331 map (\<lambda> f. rec_exec f xs) (get_fstn_args m n)= take n xs" |
310 map (\<lambda> f. rec_exec f xs) (get_fstn_args m n)= take n xs" |
332 proof(induct n) |
311 proof(induct n) |
600 apply(erule_tac prime_cn_reverse, simp) |
579 apply(erule_tac prime_cn_reverse, simp) |
601 apply(erule_tac prime_cn_reverse, simp) |
580 apply(erule_tac prime_cn_reverse, simp) |
602 apply(erule_tac x = n in allE, simp add: nth_append primerec_accum) |
581 apply(erule_tac x = n in allE, simp add: nth_append primerec_accum) |
603 done |
582 done |
604 |
583 |
605 lemma min_Suc_Suc[simp]: "min (Suc (Suc x)) x = x" |
|
606 by auto |
|
607 |
|
608 declare numeral_3_eq_3[simp] |
584 declare numeral_3_eq_3[simp] |
609 |
585 |
610 lemma primerec_rec_pred_1[intro]: "primerec rec_pred (Suc 0)" |
586 lemma primerec_rec_pred_1[intro]: "primerec rec_pred (Suc 0)" |
611 apply(simp add: rec_pred_def) |
587 apply(simp add: rec_pred_def) |
612 apply(rule_tac prime_cn, auto) |
588 apply(rule_tac prime_cn, auto) |
657 "\<lbrakk>primerec rt n; primerec rf (Suc n); n > 0\<rbrakk> \<Longrightarrow> |
633 "\<lbrakk>primerec rt n; primerec rf (Suc n); n > 0\<rbrakk> \<Longrightarrow> |
658 primerec (rec_all rt rf) n" |
634 primerec (rec_all rt rf) n" |
659 apply(simp add: rec_all.simps, auto) |
635 apply(simp add: rec_all.simps, auto) |
660 apply(auto, simp add: nth_append, auto) |
636 apply(auto, simp add: nth_append, auto) |
661 done |
637 done |
662 |
|
663 lemma min_P0[simp]: "Rr (xs @ [0]) \<Longrightarrow> |
|
664 Min {x. x = (0::nat) \<and> Rr (xs @ [x])} = 0" |
|
665 by(rule_tac Min_eqI, simp, simp, simp) |
|
666 |
638 |
667 lemma primerec_rec_not_1[intro]: "primerec rec_not (Suc 0)" |
639 lemma primerec_rec_not_1[intro]: "primerec rec_not (Suc 0)" |
668 apply(simp add: rec_not_def) |
640 apply(simp add: rec_not_def) |
669 apply(rule prime_cn, auto) |
641 apply(rule prime_cn, auto) |
670 apply(case_tac i, auto intro: prime_id) |
642 apply(case_tac i, auto intro: prime_id) |
843 lemma primerec_rec_le_2[intro]: "primerec rec_le (Suc (Suc 0))" |
813 lemma primerec_rec_le_2[intro]: "primerec rec_le (Suc (Suc 0))" |
844 apply(simp add: rec_le_def) |
814 apply(simp add: rec_le_def) |
845 apply(rule_tac prime_cn, auto) |
815 apply(rule_tac prime_cn, auto) |
846 apply(case_tac i, auto) |
816 apply(case_tac i, auto) |
847 done |
817 done |
848 |
|
849 lemma take_butlast_list_plus_two[simp]: |
|
850 "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) = |
|
851 ys @ [ys ! n]" |
|
852 apply(simp) |
|
853 apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto) |
|
854 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI) |
|
855 apply(case_tac "ys = []", simp_all) |
|
856 done |
|
857 |
|
858 lemma Maxr_Suc_simp: |
|
859 "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w |
|
860 else Maxr Rr xs w)" |
|
861 apply(auto simp: Maxr.simps expand_conj_in_set) |
|
862 apply(rule_tac Max_eqI, auto) |
|
863 done |
|
864 |
|
865 lemma min_Suc_1[simp]: "min (Suc n) n = n" by simp |
|
866 |
818 |
867 lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> |
819 lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> |
868 Sigma f (xs @ [n]) = 0" |
820 Sigma f (xs @ [n]) = 0" |
869 apply(induct n, simp add: Sigma.simps) |
821 apply(induct n, simp add: Sigma.simps) |
870 apply(simp add: Sigma_Suc_simp_rewrite) |
822 apply(simp add: Sigma_Suc_simp_rewrite) |
1581 fun fac :: "nat \<Rightarrow> nat" ("_!" [100] 99) |
1533 fun fac :: "nat \<Rightarrow> nat" ("_!" [100] 99) |
1582 where |
1534 where |
1583 "fac 0 = 1" | |
1535 "fac 0 = 1" | |
1584 "fac (Suc x) = (Suc x) * fac x" |
1536 "fac (Suc x) = (Suc x) * fac x" |
1585 |
1537 |
1586 lemma rec_exec_rec_dummyfac_0: "rec_exec rec_dummyfac [0, 0] = Suc 0" |
|
1587 by(simp add: rec_dummyfac_def rec_exec.simps) |
|
1588 |
|
1589 lemma rec_cn_simp: "rec_exec (Cn n f gs) xs = |
|
1590 (let rgs = map (\<lambda> g. rec_exec g xs) gs in |
|
1591 rec_exec f rgs)" |
|
1592 by(simp add: rec_exec.simps) |
|
1593 |
|
1594 lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" |
|
1595 by(simp add: rec_exec.simps) |
|
1596 |
|
1597 lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !" |
1538 lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !" |
1598 apply(induct y) |
1539 apply(induct y) |
1599 apply(auto simp: rec_dummyfac_def rec_exec.simps) |
1540 apply(auto simp: rec_dummyfac_def rec_exec.simps) |
1600 done |
1541 done |
1601 |
1542 |
1802 |
1743 |
1803 declare loR.simps[simp del] |
1744 declare loR.simps[simp del] |
1804 |
1745 |
1805 text {* |
1746 text {* |
1806 @{text "Lo"} specifies the @{text "lo"} function given on page 79 of |
1747 @{text "Lo"} specifies the @{text "lo"} function given on page 79 of |
1807 Boolos's book. It is one of the two notions of integeral logarithmatic |
1748 Boolos's book. It is one of the two notions of integeral logarithmetic |
1808 operation on that page. The other is @{text "lg"}. |
1749 operation on that page. The other is @{text "lg"}. |
1809 *} |
1750 *} |
1810 fun lo :: " nat \<Rightarrow> nat \<Rightarrow> nat" |
1751 fun lo :: " nat \<Rightarrow> nat \<Rightarrow> nat" |
1811 where |
1752 where |
1812 "lo x y = (if x > 1 \<and> y > 1 \<and> {u. loR [x, y, u]} \<noteq> {} then Max {u. loR [x, y, u]} |
1753 "lo x y = (if x > 1 \<and> y > 1 \<and> {u. loR [x, y, u]} \<noteq> {} then Max {u. loR [x, y, u]} |
1813 else 0)" |
1754 else 0)" |
1814 |
1755 |
1815 declare lo.simps[simp del] |
1756 declare lo.simps[simp del] |
1816 |
|
1817 lemma primerec_then_ge_0[elim]: "primerec rf n \<Longrightarrow> n > 0" |
|
1818 apply(induct rule: primerec.induct, auto) |
|
1819 done |
|
1820 |
1757 |
1821 lemma primerec_sigma[intro!]: |
1758 lemma primerec_sigma[intro!]: |
1822 "\<lbrakk>n > Suc 0; primerec rf n\<rbrakk> \<Longrightarrow> |
1759 "\<lbrakk>n > Suc 0; primerec rf n\<rbrakk> \<Longrightarrow> |
1823 primerec (rec_sigma rf) n" |
1760 primerec (rec_sigma rf) n" |
1824 apply(simp add: rec_sigma.simps) |
1761 apply(simp add: rec_sigma.simps) |
1883 Maxr loR [x, y] x" |
1820 Maxr loR [x, y] x" |
1884 apply(simp) |
1821 apply(simp) |
1885 done |
1822 done |
1886 qed |
1823 qed |
1887 |
1824 |
1888 lemma MaxloR0[simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0" |
|
1889 apply(rule_tac Max_eqI, auto simp: loR.simps) |
|
1890 done |
|
1891 |
|
1892 lemma two_less_square[simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y" |
|
1893 by(induct y, auto) |
|
1894 |
|
1895 lemma less_mult: "\<lbrakk>x > 0; y > Suc 0\<rbrakk> \<Longrightarrow> x < y * x" |
|
1896 apply(case_tac y, simp, simp) |
|
1897 done |
|
1898 |
|
1899 lemma x_less_exp: "\<lbrakk>y > Suc 0\<rbrakk> \<Longrightarrow> x < y^x" |
1825 lemma x_less_exp: "\<lbrakk>y > Suc 0\<rbrakk> \<Longrightarrow> x < y^x" |
1900 apply(induct x, simp, simp) |
1826 apply(induct x, simp, simp) |
1901 apply(case_tac x, simp, auto) |
1827 apply(case_tac x, simp, auto) |
1902 apply(rule_tac y = "y* y^nat" in le_less_trans, simp) |
1828 apply(rule_tac y = "y* y^nat" in le_less_trans, simp) |
1903 apply(rule_tac less_mult, auto) |
1829 apply(rule_tac n_less_m_mult_n, auto) |
1904 done |
1830 done |
1905 |
|
1906 lemma le_mult: "y \<noteq> (0::nat) \<Longrightarrow> x \<le> x * y" |
|
1907 by(induct y, simp, simp) |
|
1908 |
1831 |
1909 lemma uplimit_loR: |
1832 lemma uplimit_loR: |
1910 assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]" |
1833 assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]" |
1911 shows "xa \<le> x" |
1834 shows "xa \<le> x" |
1912 proof - |
1835 proof - |
1953 where |
1876 where |
1954 "lgR [x, y, u] = (y^u \<le> x)" |
1877 "lgR [x, y, u] = (y^u \<le> x)" |
1955 |
1878 |
1956 text {* |
1879 text {* |
1957 @{text "lg"} specifies the @{text "lg"} function given on page 79 of |
1880 @{text "lg"} specifies the @{text "lg"} function given on page 79 of |
1958 Boolos's book. It is one of the two notions of integeral logarithmatic |
1881 Boolos's book. It is one of the two notions of integeral logarithmetic |
1959 operation on that page. The other is @{text "lo"}. |
1882 operation on that page. The other is @{text "lo"}. |
1960 *} |
1883 *} |
1961 fun lg :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
1884 fun lg :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
1962 where |
1885 where |
1963 "lg x y = (if x > 1 \<and> y > 1 \<and> {u. lgR [x, y, u]} \<noteq> {} then |
1886 "lg x y = (if x > 1 \<and> y > 1 \<and> {u. lgR [x, y, u]} \<noteq> {} then |
2836 where |
2759 where |
2837 "rec_halt = Mn (Suc (Suc 0)) (rec_nonstop)" |
2760 "rec_halt = Mn (Suc (Suc 0)) (rec_nonstop)" |
2838 |
2761 |
2839 declare nonstop.simps[simp del] |
2762 declare nonstop.simps[simp del] |
2840 |
2763 |
2841 lemma primerec_not0: "primerec f n \<Longrightarrow> n > 0" |
|
2842 by(induct f n rule: primerec.induct, auto) |
|
2843 |
|
2844 lemma primerec_not0E[elim]: "primerec f 0 \<Longrightarrow> RR" |
|
2845 apply(drule_tac primerec_not0, simp) |
|
2846 done |
|
2847 |
|
2848 lemma length_butlast[simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n" |
|
2849 apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]",force) |
|
2850 apply(rule_tac x = "last xs" in exI) |
|
2851 apply(rule_tac x = "butlast xs" in exI) |
|
2852 apply(case_tac "xs = []", auto) |
|
2853 done |
|
2854 |
|
2855 text {* |
2764 text {* |
2856 The lemma relates the interpreter of primitive functions with |
2765 The lemma relates the interpreter of primitive functions with |
2857 the calculation relation of general recursive functions. |
2766 the calculation relation of general recursive functions. |
2858 *} |
2767 *} |
2859 |
2768 |
2888 rec_all.simps rec_sigma.simps rec_accum.simps) |
2797 rec_all.simps rec_sigma.simps rec_accum.simps) |
2889 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, @{thm prime_pr}] 1*} |
2798 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, @{thm prime_pr}] 1*} |
2890 ;(simp add:primerec_rec_pi_helpers primrec_dummyfac)?)+ |
2799 ;(simp add:primerec_rec_pi_helpers primrec_dummyfac)?)+ |
2891 by fastforce+ |
2800 by fastforce+ |
2892 |
2801 |
2893 lemma primerec_rec_trpl[intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))" |
|
2894 apply(simp add: rec_trpl_def) |
|
2895 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
|
2896 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ |
|
2897 done |
|
2898 |
|
2899 lemma primerec_rec_listsum2[intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl" |
|
2900 apply(induct n) |
|
2901 apply(simp_all add: rec_strt'.simps Let_def rec_listsum2.simps) |
|
2902 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
|
2903 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ |
|
2904 done |
|
2905 |
|
2906 lemma primerec_rec_strt': "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl" |
|
2907 apply(induct n) |
|
2908 apply(simp_all add: rec_strt'.simps Let_def) |
|
2909 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
|
2910 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+) |
|
2911 done |
|
2912 |
|
2913 lemma primerec_rec_strt: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl" |
|
2914 apply(simp add: rec_strt.simps rec_strt'.simps) |
|
2915 by(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
|
2916 @{thm prime_id}, @{thm prime_pr}] 1*}; force elim:primerec_rec_strt') |
|
2917 |
|
2918 lemma primerec_map_vl: |
|
2919 "i < vl \<Longrightarrow> primerec ((map (\<lambda>i. recf.id (Suc vl) (i)) |
|
2920 [Suc 0..<vl] @ [recf.id (Suc vl) (vl)]) ! i) (Suc vl)" |
|
2921 apply(induct i, auto simp: nth_append) |
|
2922 done |
|
2923 |
|
2924 lemma primerec_recs[intro]: |
2802 lemma primerec_recs[intro]: |
|
2803 "primerec rec_trpl (Suc (Suc (Suc 0)))" |
2925 "primerec rec_newleft0 (Suc (Suc 0))" |
2804 "primerec rec_newleft0 (Suc (Suc 0))" |
2926 "primerec rec_newleft1 (Suc (Suc 0))" |
2805 "primerec rec_newleft1 (Suc (Suc 0))" |
2927 "primerec rec_newleft2 (Suc (Suc 0))" |
2806 "primerec rec_newleft2 (Suc (Suc 0))" |
2928 "primerec rec_newleft3 ((Suc (Suc 0)))" |
2807 "primerec rec_newleft3 (Suc (Suc 0))" |
2929 "primerec rec_newleft (Suc (Suc (Suc 0)))" |
2808 "primerec rec_newleft (Suc (Suc (Suc 0)))" |
2930 "primerec rec_left (Suc 0)" |
2809 "primerec rec_left (Suc 0)" |
2931 "primerec rec_actn (Suc (Suc (Suc 0)))" |
2810 "primerec rec_actn (Suc (Suc (Suc 0)))" |
2932 "primerec rec_stat (Suc 0)" |
2811 "primerec rec_stat (Suc 0)" |
2933 "primerec rec_newstat (Suc (Suc (Suc 0)))" |
2812 "primerec rec_newstat (Suc (Suc (Suc 0)))" |
2934 apply(simp_all add: rec_newleft_def rec_embranch.simps rec_left_def rec_lo_def rec_entry_def |
2813 apply(simp_all add: rec_newleft_def rec_embranch.simps rec_left_def rec_lo_def rec_entry_def |
2935 rec_actn_def Let_def arity.simps rec_newleft0_def rec_stat_def rec_newstat_def |
2814 rec_actn_def Let_def arity.simps rec_newleft0_def rec_stat_def rec_newstat_def |
2936 rec_newleft1_def rec_newleft2_def rec_newleft3_def) |
2815 rec_newleft1_def rec_newleft2_def rec_newleft3_def rec_trpl_def) |
2937 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
2816 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
2938 @{thm prime_id}, @{thm prime_pr}] 1*};force)+ |
2817 @{thm prime_id}, @{thm prime_pr}] 1*};force)+ |
2939 done |
2818 done |
2940 |
2819 |
2941 lemma primerec_rec_newrght[intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))" |
2820 lemma primerec_rec_newrght[intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))" |
2948 |
2827 |
2949 lemma primerec_rec_newconf[intro]: "primerec rec_newconf (Suc (Suc 0))" |
2828 lemma primerec_rec_newconf[intro]: "primerec rec_newconf (Suc (Suc 0))" |
2950 apply(simp add: rec_newconf_def) |
2829 apply(simp add: rec_newconf_def) |
2951 by(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
2830 by(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
2952 @{thm prime_id}, @{thm prime_pr}] 1*};force) |
2831 @{thm prime_id}, @{thm prime_pr}] 1*};force) |
2953 |
|
2954 lemma primerec_rec_inpt[intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)" |
|
2955 apply(simp add: rec_inpt_def) |
|
2956 apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
|
2957 @{thm prime_id}, @{thm prime_pr}] 1*}; fastforce elim:primerec_rec_strt primerec_map_vl) |
|
2958 done |
|
2959 |
2832 |
2960 lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))" |
2833 lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))" |
2961 apply(simp add: rec_conf_def) |
2834 apply(simp add: rec_conf_def) |
2962 by(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
2835 by(tactic {* resolve_tac @{context} [@{thm prime_cn}, |
2963 @{thm prime_id}, @{thm prime_pr}] 1*};force simp: numeral) |
2836 @{thm prime_id}, @{thm prime_pr}] 1*};force simp: numeral) |
3059 definition rec_F :: "recf" |
2932 definition rec_F :: "recf" |
3060 where |
2933 where |
3061 "rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) |
2934 "rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) |
3062 rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]" |
2935 rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]" |
3063 |
2936 |
3064 lemma get_fstn_args_nth[simp]: |
|
3065 "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)" |
|
3066 apply(induct n, simp) |
|
3067 apply(case_tac "k = n", simp_all add: get_fstn_args.simps |
|
3068 nth_append) |
|
3069 done |
|
3070 |
|
3071 lemma get_fstn_args_is_id[simp]: |
|
3072 "\<lbrakk>ys \<noteq> []; |
|
3073 k < length ys\<rbrakk> \<Longrightarrow> |
|
3074 (get_fstn_args (length ys) (length ys) ! k) = |
|
3075 id (length ys) (k)" |
|
3076 by(erule_tac get_fstn_args_nth) |
|
3077 |
|
3078 lemma terminate_halt_lemma: |
2937 lemma terminate_halt_lemma: |
3079 "\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0; |
2938 "\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0; |
3080 \<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]" |
2939 \<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]" |
3081 apply(simp add: rec_halt_def) |
2940 apply(simp add: rec_halt_def) |
3082 apply(rule_tac termi_mn, auto) |
2941 apply(rule_tac termi_mn, auto) |
3608 apply(rule_tac dvd_power_le, auto) |
3467 apply(rule_tac dvd_power_le, auto) |
3609 done |
3468 done |
3610 next |
3469 next |
3611 show "l \<in> ?setx" by simp |
3470 show "l \<in> ?setx" by simp |
3612 qed |
3471 qed |
3613 qed |
3472 qed |
3614 |
|
3615 lemma conf_decode2: |
|
3616 "\<lbrakk>m \<noteq> n; m \<noteq> k; n \<noteq> k; |
|
3617 \<not> Suc 0 < Pi m ^ l * Pi n ^ st * Pi k ^ r\<rbrakk> \<Longrightarrow> l = 0" |
|
3618 apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto) |
|
3619 done |
|
3620 |
3473 |
3621 lemma left_trpl_fst[simp]: "left (trpl l st r) = l" |
3474 lemma left_trpl_fst[simp]: "left (trpl l st r) = l" |
3622 apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp) |
3475 apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp) |
3623 apply(auto simp: conf_decode1) |
3476 apply(auto simp: conf_decode1) |
3624 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r") |
3477 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r") |
3806 qed |
3659 qed |
3807 |
3660 |
3808 lemma fetch_zero_zero[simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0" |
3661 lemma fetch_zero_zero[simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0" |
3809 by(simp add: fetch.simps) |
3662 by(simp add: fetch.simps) |
3810 |
3663 |
3811 lemma Five_Suc: "5 = Suc 4" by simp |
|
3812 |
|
3813 lemma modify_tprog_fetch_state: |
3664 lemma modify_tprog_fetch_state: |
3814 "\<lbrakk>st \<le> length tp div 2; st > 0; b = 1 \<or> b = 0\<rbrakk> \<Longrightarrow> |
3665 "\<lbrakk>st \<le> length tp div 2; st > 0; b = 1 \<or> b = 0\<rbrakk> \<Longrightarrow> |
3815 modify_tprog tp ! Suc (4 * (st - Suc 0) + 2 * b) = |
3666 modify_tprog tp ! Suc (4 * (st - Suc 0) + 2 * b) = |
3816 (snd (tp ! (2 * (st - Suc 0) + b)))" |
3667 (snd (tp ! (2 * (st - Suc 0) + b)))" |
3817 proof(induct st arbitrary: tp, simp) |
3668 proof(induct st arbitrary: tp, simp) |
4018 bl2nat xs 0 + bl2nat ys (length xs)" |
3866 bl2nat xs 0 + bl2nat ys (length xs)" |
4019 apply(case_tac k, simp_all add: bl2nat.simps) |
3867 apply(case_tac k, simp_all add: bl2nat.simps) |
4020 apply(simp_all only: bl2nat_cons_bk bl2nat_cons_oc) |
3868 apply(simp_all only: bl2nat_cons_bk bl2nat_cons_oc) |
4021 done |
3869 done |
4022 qed |
3870 qed |
4023 |
|
4024 lemma bl2nat_exp: "n \<noteq> 0 \<Longrightarrow> bl2nat bl n = 2^n * bl2nat bl 0" |
|
4025 apply(induct bl) |
|
4026 apply(auto simp: bl2nat.simps) |
|
4027 apply(case_tac a, auto simp: bl2nat.simps bl2nat_double) |
|
4028 done |
|
4029 |
|
4030 lemma nat_minus_eq: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> a - c = b - d" |
|
4031 by auto |
|
4032 |
|
4033 lemma tape_of_nat_list_butlast_last: |
|
4034 "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y" |
|
4035 apply(induct ys, simp, simp) |
|
4036 apply(case_tac "ys = []", simp add: tape_of_list_def tape_of_nat_def) |
|
4037 apply(simp add: tape_of_nl_cons tape_of_nat_def) |
|
4038 done |
|
4039 |
|
4040 lemma listsum2_append: |
|
4041 "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> listsum2 (xs @ ys) n = listsum2 xs n" |
|
4042 apply(induct n) |
|
4043 apply(auto simp: listsum2.simps nth_append) |
|
4044 done |
|
4045 |
|
4046 lemma strt'_append: |
|
4047 "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> strt' xs n = strt' (xs @ ys) n" |
|
4048 proof(induct n arbitrary: xs ys) |
|
4049 fix xs ys |
|
4050 show "strt' xs 0 = strt' (xs @ ys) 0" by(simp add: strt'.simps) |
|
4051 next |
|
4052 fix n xs ys |
|
4053 assume ind: |
|
4054 "\<And> xs ys. n \<le> length xs \<Longrightarrow> strt' xs n = strt' (xs @ ys) n" |
|
4055 and h: "Suc n \<le> length (xs::nat list)" |
|
4056 show "strt' xs (Suc n) = strt' (xs @ ys) (Suc n)" |
|
4057 using ind[of xs ys] h |
|
4058 apply(simp add: strt'.simps nth_append listsum2_append) |
|
4059 done |
|
4060 qed |
|
4061 |
|
4062 lemma length_listsum2_eq: |
|
4063 "\<lbrakk>length (ys::nat list) = k\<rbrakk> |
|
4064 \<Longrightarrow> length (<ys>) = listsum2 (map Suc ys) k + k - 1" |
|
4065 apply(induct k arbitrary: ys, simp_all add: listsum2.simps) |
|
4066 apply(subgoal_tac "\<exists> xs x. ys = xs @ [x]", auto) |
|
4067 proof - |
|
4068 fix xs x |
|
4069 assume ind: "\<And>ys. length ys = length xs \<Longrightarrow> length (<ys>) |
|
4070 = listsum2 (map Suc ys) (length xs) + |
|
4071 length (xs::nat list) - Suc 0" |
|
4072 have "length (<xs>) |
|
4073 = listsum2 (map Suc xs) (length xs) + length xs - Suc 0" |
|
4074 apply(rule_tac ind, simp) |
|
4075 done |
|
4076 thus "length (<xs @ [x]>) = |
|
4077 Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)" |
|
4078 apply(case_tac "xs = []") |
|
4079 apply(simp add: tape_of_list_def listsum2.simps |
|
4080 tape_of_nat_list.simps tape_of_nat_def) |
|
4081 apply(simp add: tape_of_nat_list_butlast_last) |
|
4082 using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"] |
|
4083 apply(simp) |
|
4084 done |
|
4085 next |
|
4086 fix k ys |
|
4087 assume "length ys = Suc k" |
|
4088 thus "\<exists>xs x. ys = xs @ [x]" |
|
4089 apply(rule_tac x = "butlast ys" in exI, |
|
4090 rule_tac x = "last ys" in exI) |
|
4091 apply(case_tac ys, auto) |
|
4092 done |
|
4093 qed |
|
4094 |
|
4095 lemma tape_of_nat_list_length: |
|
4096 "length (<(ys::nat list)>) = |
|
4097 listsum2 (map Suc ys) (length ys) + length ys - 1" |
|
4098 using length_listsum2_eq[of ys "length ys"] |
|
4099 apply(simp) |
|
4100 done |
|
4101 |
3871 |
4102 lemma trpl_code_simp[simp]: |
3872 lemma trpl_code_simp[simp]: |
4103 "trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) = |
3873 "trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) = |
4104 rec_exec rec_conf [code tp, bl2wc (<lm>), 0]" |
3874 rec_exec rec_conf [code tp, bl2wc (<lm>), 0]" |
4105 apply(simp add: steps.simps rec_exec.simps conf_lemma conf.simps |
3875 apply(simp add: steps.simps rec_exec.simps conf_lemma conf.simps |
4449 |
4219 |
4450 lemma F_correct: |
4220 lemma F_correct: |
4451 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
4221 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
4452 tm_wf (tp,0); 0<rs\<rbrakk> |
4222 tm_wf (tp,0); 0<rs\<rbrakk> |
4453 \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
4223 \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
4454 thm halt_least_step nonstop_t_eq nonstop_lemma rec_t_eq_steps conf_lemma |
|
4455 apply(frule_tac halt_least_step, auto) |
4224 apply(frule_tac halt_least_step, auto) |
4456 apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) |
4225 apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) |
4457 using rec_t_eq_steps[of tp l lm stp] |
4226 using rec_t_eq_steps[of tp l lm stp] |
4458 apply(simp add: conf_lemma) |
4227 apply(simp add: conf_lemma) |
4459 proof - |
4228 proof - |