1214 apply(simp add: t_twice_def mopup.simps t_twice_compile_def) |
1214 apply(simp add: t_twice_def mopup.simps t_twice_compile_def) |
1215 done |
1215 done |
1216 |
1216 |
1217 declare start_of.simps[simp del] |
1217 declare start_of.simps[simp del] |
1218 |
1218 |
1219 lemma twice_lemma: "rec_eval rec_twice [rs] = 2*rs" |
1219 lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs" |
1220 by(auto simp: rec_twice_def rec_eval.simps) |
1220 by(auto simp: rec_twice_def rec_exec.simps) |
1221 |
1221 |
1222 lemma t_twice_correct: |
1222 lemma t_twice_correct: |
1223 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
1223 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
1224 (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp = |
1224 (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp = |
1225 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" |
1225 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" |
1226 proof(case_tac "rec_ci rec_twice") |
1226 proof(case_tac "rec_ci rec_twice") |
1227 fix a b c |
1227 fix a b c |
1228 assume h: "rec_ci rec_twice = (a, b, c)" |
1228 assume h: "rec_ci rec_twice = (a, b, c)" |
1229 have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup (length [rs])) |
1229 have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup (length [rs])) |
1230 (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval rec_twice [rs])) @ Bk\<up>(l))" |
1230 (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_twice [rs])) @ Bk\<up>(l))" |
1231 thm recursive_compile_to_tm_correct1 |
1231 thm recursive_compile_to_tm_correct1 |
1232 proof(rule_tac recursive_compile_to_tm_correct1) |
1232 proof(rule_tac recursive_compile_to_tm_correct1) |
1233 show "rec_ci rec_twice = (a, b, c)" by (simp add: h) |
1233 show "rec_ci rec_twice = (a, b, c)" by (simp add: h) |
1234 next |
1234 next |
1235 show "terminates rec_twice [rs]" |
1235 show "terminate rec_twice [rs]" |
1236 apply(rule_tac primerec_terminates, auto) |
1236 apply(rule_tac primerec_terminate, auto) |
1237 apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2) |
1237 apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2) |
1238 by(auto) |
1238 by(auto) |
1239 next |
1239 next |
1240 show "tm_of abc_twice = tm_of (a [+] dummy_abc (length [rs]))" |
1240 show "tm_of abc_twice = tm_of (a [+] dummy_abc (length [rs]))" |
1241 using h |
1241 using h |
1242 by(simp add: abc_twice_def) |
1242 by(simp add: abc_twice_def) |
1243 qed |
1243 qed |
1244 thus "?thesis" |
1244 thus "?thesis" |
1245 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_eval.simps twice_lemma) |
1245 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma) |
1246 done |
1246 done |
1247 qed |
1247 qed |
1248 |
1248 |
1249 declare adjust.simps[simp] |
1249 declare adjust.simps[simp] |
1250 |
1250 |
2003 |
2003 |
2004 lemma [intro]: "primerec rec_fourtimes (Suc 0)" |
2004 lemma [intro]: "primerec rec_fourtimes (Suc 0)" |
2005 apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps) |
2005 apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps) |
2006 by auto |
2006 by auto |
2007 |
2007 |
2008 lemma fourtimes_lemma: "rec_eval rec_fourtimes [rs] = 4 * rs" |
2008 lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs" |
2009 by(simp add: rec_eval.simps rec_fourtimes_def) |
2009 by(simp add: rec_exec.simps rec_fourtimes_def) |
2010 |
2010 |
2011 |
2011 |
2012 lemma t_fourtimes_correct: |
2012 lemma t_fourtimes_correct: |
2013 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
2013 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
2014 (tm_of abc_fourtimes @ shift (mopup 1) (length (tm_of abc_fourtimes) div 2)) stp = |
2014 (tm_of abc_fourtimes @ shift (mopup 1) (length (tm_of abc_fourtimes) div 2)) stp = |
2015 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" |
2015 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" |
2016 proof(case_tac "rec_ci rec_fourtimes") |
2016 proof(case_tac "rec_ci rec_fourtimes") |
2017 fix a b c |
2017 fix a b c |
2018 assume h: "rec_ci rec_fourtimes = (a, b, c)" |
2018 assume h: "rec_ci rec_fourtimes = (a, b, c)" |
2019 have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs])) |
2019 have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs])) |
2020 (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval rec_fourtimes [rs])) @ Bk\<up>(l))" |
2020 (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_fourtimes [rs])) @ Bk\<up>(l))" |
2021 thm recursive_compile_to_tm_correct1 |
2021 thm recursive_compile_to_tm_correct1 |
2022 proof(rule_tac recursive_compile_to_tm_correct1) |
2022 proof(rule_tac recursive_compile_to_tm_correct1) |
2023 show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h) |
2023 show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h) |
2024 next |
2024 next |
2025 show "terminates rec_fourtimes [rs]" |
2025 show "terminate rec_fourtimes [rs]" |
2026 apply(rule_tac primerec_terminates) |
2026 apply(rule_tac primerec_terminate) |
2027 by auto |
2027 by auto |
2028 next |
2028 next |
2029 show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))" |
2029 show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))" |
2030 using h |
2030 using h |
2031 by(simp add: abc_fourtimes_def) |
2031 by(simp add: abc_fourtimes_def) |
4727 shows "\<exists>stp m n. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = |
4727 shows "\<exists>stp m n. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = |
4728 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))" |
4728 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))" |
4729 proof - |
4729 proof - |
4730 obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)" |
4730 obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)" |
4731 by (metis prod_cases3) |
4731 by (metis prod_cases3) |
4732 moreover have b: "rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
4732 moreover have b: "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
4733 using assms |
4733 using assms |
4734 apply(rule_tac F_correct, simp_all) |
4734 apply(rule_tac F_correct, simp_all) |
4735 done |
4735 done |
4736 have "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4736 have "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4737 (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp |
4737 (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp |
4738 = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" |
4738 = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" |
4739 proof(rule_tac recursive_compile_to_tm_correct1) |
4739 proof(rule_tac recursive_compile_to_tm_correct1) |
4740 show "rec_ci rec_F = (ap, arity, fp)" using a by simp |
4740 show "rec_ci rec_F = (ap, arity, fp)" using a by simp |
4741 next |
4741 next |
4742 show "terminates rec_F [code tp, bl2wc (<lm>)]" |
4742 show "terminate rec_F [code tp, bl2wc (<lm>)]" |
4743 using assms |
4743 using assms |
4744 by(rule_tac terminates_F, simp_all) |
4744 by(rule_tac terminate_F, simp_all) |
4745 next |
4745 next |
4746 show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))" |
4746 show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))" |
4747 using a |
4747 using a |
4748 apply(simp add: F_tprog_def F_aprog_def numeral_2_eq_2) |
4748 apply(simp add: F_tprog_def F_aprog_def numeral_2_eq_2) |
4749 done |
4749 done |
4750 qed |
4750 qed |
4751 then obtain stp m l where |
4751 then obtain stp m l where |
4752 "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4752 "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4753 (F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp |
4753 (F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp |
4754 = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast |
4754 = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast |
4755 hence "\<exists> m. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4755 hence "\<exists> m. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4756 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp |
4756 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp |
4757 = (0, Bk\<up>m, Oc\<up>Suc (rs - 1) @ Bk\<up>l)" |
4757 = (0, Bk\<up>m, Oc\<up>Suc (rs - 1) @ Bk\<up>l)" |
4758 proof - |
4758 proof - |
4759 assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk \<up> i) |
4759 assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk \<up> i) |
4760 (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp = |
4760 (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp = |
4761 (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_eval rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)" |
4761 (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_exec rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)" |
4762 moreover have "tinres [Bk, Bk] [Bk]" |
4762 moreover have "tinres [Bk, Bk] [Bk]" |
4763 apply(auto simp: tinres_def) |
4763 apply(auto simp: tinres_def) |
4764 done |
4764 done |
4765 moreover obtain sa la ra where "steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4765 moreover obtain sa la ra where "steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i) |
4766 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp = (sa, la, ra)" |
4766 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp = (sa, la, ra)" |
4934 apply(auto) |
4934 apply(auto) |
4935 apply(drule_tac lg_bin, simp_all) |
4935 apply(drule_tac lg_bin, simp_all) |
4936 done |
4936 done |
4937 |
4937 |
4938 lemma NSTD_1: "\<not> TSTD (a, b, c) |
4938 lemma NSTD_1: "\<not> TSTD (a, b, c) |
4939 \<Longrightarrow> rec_eval rec_NSTD [trpl_code (a, b, c)] = Suc 0" |
4939 \<Longrightarrow> rec_exec rec_NSTD [trpl_code (a, b, c)] = Suc 0" |
4940 using NSTD_lemma1[of "trpl_code (a, b, c)"] |
4940 using NSTD_lemma1[of "trpl_code (a, b, c)"] |
4941 NSTD_lemma2[of "trpl_code (a, b, c)"] |
4941 NSTD_lemma2[of "trpl_code (a, b, c)"] |
4942 apply(simp add: TSTD_def) |
4942 apply(simp add: TSTD_def) |
4943 apply(erule_tac disjE, erule_tac nstd_case1) |
4943 apply(erule_tac disjE, erule_tac nstd_case1) |
4944 apply(erule_tac disjE, erule_tac nstd_case2) |
4944 apply(erule_tac disjE, erule_tac nstd_case2) |
4947 |
4947 |
4948 lemma nonstop_t_uhalt_eq: |
4948 lemma nonstop_t_uhalt_eq: |
4949 "\<lbrakk>tm_wf (tp, 0); |
4949 "\<lbrakk>tm_wf (tp, 0); |
4950 steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp = (a, b, c); |
4950 steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp = (a, b, c); |
4951 \<not> TSTD (a, b, c)\<rbrakk> |
4951 \<not> TSTD (a, b, c)\<rbrakk> |
4952 \<Longrightarrow> rec_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0" |
4952 \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0" |
4953 apply(simp add: rec_nonstop_def rec_eval.simps) |
4953 apply(simp add: rec_nonstop_def rec_exec.simps) |
4954 apply(subgoal_tac |
4954 apply(subgoal_tac |
4955 "rec_eval rec_conf [code tp, bl2wc (<lm>), stp] = |
4955 "rec_exec rec_conf [code tp, bl2wc (<lm>), stp] = |
4956 trpl_code (a, b, c)", simp) |
4956 trpl_code (a, b, c)", simp) |
4957 apply(erule_tac NSTD_1) |
4957 apply(erule_tac NSTD_1) |
4958 using rec_t_eq_steps[of tp l lm stp] |
4958 using rec_t_eq_steps[of tp l lm stp] |
4959 apply(simp) |
4959 apply(simp) |
4960 done |
4960 done |
4961 |
4961 |
4962 lemma nonstop_true: |
4962 lemma nonstop_true: |
4963 "\<lbrakk>tm_wf (tp, 0); |
4963 "\<lbrakk>tm_wf (tp, 0); |
4964 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk> |
4964 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk> |
4965 \<Longrightarrow> \<forall>y. rec_eval rec_nonstop ([code tp, bl2wc (<lm>), y]) = (Suc 0)" |
4965 \<Longrightarrow> \<forall>y. rec_exec rec_nonstop ([code tp, bl2wc (<lm>), y]) = (Suc 0)" |
4966 apply(rule_tac allI, erule_tac x = y in allE) |
4966 apply(rule_tac allI, erule_tac x = y in allE) |
4967 apply(case_tac "steps0 (Suc 0, Bk\<up>(l), <lm>) tp y", simp) |
4967 apply(case_tac "steps0 (Suc 0, Bk\<up>(l), <lm>) tp y", simp) |
4968 apply(rule_tac nonstop_t_uhalt_eq, simp_all) |
4968 apply(rule_tac nonstop_t_uhalt_eq, simp_all) |
4969 done |
4969 done |
4970 |
4970 |
5019 fix anything |
5019 fix anything |
5020 have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>" |
5020 have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>" |
5021 using e f |
5021 using e f |
5022 proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def) |
5022 proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def) |
5023 fix i |
5023 fix i |
5024 show "terminates rec_nonstop [code tp, bl2wc (<lm>), i]" |
5024 show "terminate rec_nonstop [code tp, bl2wc (<lm>), i]" |
5025 by(rule_tac primerec_terminates, auto) |
5025 by(rule_tac primerec_terminate, auto) |
5026 next |
5026 next |
5027 fix i |
5027 fix i |
5028 show "0 < rec_eval rec_nonstop [code tp, bl2wc (<lm>), i]" |
5028 show "0 < rec_exec rec_nonstop [code tp, bl2wc (<lm>), i]" |
5029 using assms |
5029 using assms |
5030 by(drule_tac nonstop_true, auto) |
5030 by(drule_tac nonstop_true, auto) |
5031 qed |
5031 qed |
5032 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>" by simp |
5032 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>" by simp |
5033 next |
5033 next |
5034 fix apj arj ftj j anything |
5034 fix apj arj ftj j anything |
5035 assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)" |
5035 assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)" |
5036 hence "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ftj - arj) @ anything} apj |
5036 hence "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ftj - arj) @ anything} apj |
5037 {\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ |
5037 {\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ |
5038 rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # |
5038 rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # |
5039 0 \<up> (ftj - Suc arj) @ anything}" |
5039 0 \<up> (ftj - Suc arj) @ anything}" |
5040 apply(rule_tac recursive_compile_correct) |
5040 apply(rule_tac recursive_compile_correct) |
5041 apply(case_tac j, auto) |
5041 apply(case_tac j, auto) |
5042 apply(rule_tac [!] primerec_terminates) |
5042 apply(rule_tac [!] primerec_terminate) |
5043 by(auto) |
5043 by(auto) |
5044 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ftj - arj) @ anything} apj |
5044 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ftj - arj) @ anything} apj |
5045 {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_eval ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) |
5045 {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) |
5046 (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 0 \<up> (ftj - Suc arj) @ anything}" |
5046 (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 0 \<up> (ftj - Suc arj) @ anything}" |
5047 by simp |
5047 by simp |
5048 next |
5048 next |
5049 fix j |
5049 fix j |
5050 assume "(j::nat) < 2" |
5050 assume "(j::nat) < 2" |
5051 thus "terminates ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) |
5051 thus "terminate ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) |
5052 [code tp, bl2wc (<lm>)]" |
5052 [code tp, bl2wc (<lm>)]" |
5053 by(case_tac j, auto intro!: primerec_terminates) |
5053 by(case_tac j, auto intro!: primerec_terminate) |
5054 qed |
5054 qed |
5055 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>" |
5055 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>" |
5056 by simp |
5056 by simp |
5057 qed |
5057 qed |
5058 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>" by simp |
5058 thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>" by simp |