5084 done |
5084 done |
5085 qed |
5085 qed |
5086 |
5086 |
5087 lemma tutm_uhalt': |
5087 lemma tutm_uhalt': |
5088 assumes tm_wf: "tm_wf (tp,0)" |
5088 assumes tm_wf: "tm_wf (tp,0)" |
5089 and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))" |
5089 and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (1, Bk\<up>(l), <lm>) tp stp))" |
5090 shows "\<forall> stp. \<not> is_final (steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)" |
5090 shows "\<forall> stp. \<not> is_final (steps0 (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)" |
5091 apply(simp add: t_utm_def) |
5091 unfolding t_utm_def |
5092 proof(rule_tac compile_correct_unhalt) |
5092 proof(rule_tac compile_correct_unhalt) |
5093 show "layout_of F_aprog = layout_of F_aprog" by simp |
5093 show "layout_of F_aprog = layout_of F_aprog" by simp |
5094 next |
5094 next |
5095 show "F_tprog = tm_of F_aprog" |
5095 show "F_tprog = tm_of F_aprog" |
5096 by(simp add: F_tprog_def) |
5096 by(simp add: F_tprog_def) |
5097 next |
5097 next |
5098 show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) []" |
5098 show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) []" |
5099 by(auto simp: crsp.simps start_of.simps) |
5099 by(auto simp: crsp.simps start_of.simps) |
5100 next |
5100 next |
5101 show "length F_tprog div 2 = length F_tprog div 2" by simp |
5101 show "length F_tprog div 2 = length F_tprog div 2" by simp |
5102 next |
5102 next |
5103 show "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp of (as, am) \<Rightarrow> as < length F_aprog" |
5103 show "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp of (as, am) \<Rightarrow> as < length F_aprog" |
5152 lemma tutm_uhalt: |
5152 lemma tutm_uhalt: |
5153 "\<lbrakk>tm_wf (tp,0); |
5153 "\<lbrakk>tm_wf (tp,0); |
5154 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))\<rbrakk> |
5154 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))\<rbrakk> |
5155 \<Longrightarrow> \<forall> stp. \<not> is_final (steps0 (Suc 0, Bk\<up>(m), <[code tp, bl2wc (<args>)]> @ Bk\<up>(n)) t_utm stp)" |
5155 \<Longrightarrow> \<forall> stp. \<not> is_final (steps0 (Suc 0, Bk\<up>(m), <[code tp, bl2wc (<args>)]> @ Bk\<up>(n)) t_utm stp)" |
5156 apply(rule_tac tape_normalize) |
5156 apply(rule_tac tape_normalize) |
5157 apply(rule_tac tutm_uhalt', simp_all) |
5157 apply(rule_tac tutm_uhalt'[simplified], simp_all) |
5158 done |
5158 done |
5159 |
5159 |
5160 lemma UTM_uhalt_lemma_pre: |
5160 lemma UTM_uhalt_lemma_pre: |
5161 assumes tm_wf: "tm_wf (tp, 0)" |
5161 assumes tm_wf: "tm_wf (tp, 0)" |
5162 and exec: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))" |
5162 and exec: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))" |