# HG changeset patch # User Christian Urban <christian dot urban at kcl dot ac dot uk> # Date 1360834279 0 # Node ID eccd79a974aee799a6107bfc896b03c106aa249a # Parent 6013ca0e6e22d12902990b9ea9eafb570a4b53fc updated some files diff -r 6013ca0e6e22 -r eccd79a974ae Paper/Paper.thy --- a/Paper/Paper.thy Wed Feb 13 20:08:14 2013 +0000 +++ b/Paper/Paper.thy Thu Feb 14 09:31:19 2013 +0000 @@ -66,7 +66,6 @@ code_tcontra ("code contra") and steps0 ("steps") and exponent ("_\<^bsup>_\<^esup>") and - haltP ("halts") and tcopy ("copy") and tape_of ("\<langle>_\<rangle>") and tm_comp ("_ \<oplus> _") and @@ -1045,7 +1044,7 @@ number is defined as \begin{center} - @{thm haltP_def} + @{thm halts_def} \end{center} \noindent diff -r 6013ca0e6e22 -r eccd79a974ae paper.pdf Binary file paper.pdf has changed diff -r 6013ca0e6e22 -r eccd79a974ae thys/Abacus.thy --- a/thys/Abacus.thy Wed Feb 13 20:08:14 2013 +0000 +++ b/thys/Abacus.thy Thu Feb 14 09:31:19 2013 +0000 @@ -1082,11 +1082,11 @@ where "inv_stop (as, lm) (s, l, r) ires= (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @ Bk\<up>rn)" - lemma halt_lemma2': "\<lbrakk>wf LE; \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE)); Q (f 0)\<rbrakk> \<Longrightarrow> \<exists> n. P (f n)" + apply(intro exCI, simp) apply(subgoal_tac "\<forall> n. Q (f n)", simp) apply(drule_tac f = f in wf_inv_image) @@ -1162,7 +1162,7 @@ "findnth_LE \<equiv> (inv_image lex_pair findnth_measure)" lemma wf_findnth_LE: "wf findnth_LE" -by(auto intro:wf_inv_image simp: findnth_LE_def lex_pair_def) +by(auto simp: findnth_LE_def lex_pair_def) declare findnth_inv.simps[simp del] @@ -1318,20 +1318,6 @@ apply(case_tac mr, simp_all, auto) done -(* -lemma zero_and_nil[intro]: "(Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup> @ Bk # <lm::nat list> @ - Bk\<^bsup>rn \<^esup>) \<or> (lm2 = [] \<and> Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup>) - \<Longrightarrow> mr = 0 \<and> lm = []" -apply(rule context_conjI) -apply(case_tac mr, auto simp:exponent_def) -apply(insert BkCons_nil[of "replicate (n - 1) Bk" lm rn]) -apply(case_tac n, auto simp: exponent_def Bk_def tape_of_nl_nil_eq) -done - -lemma tape_of_nat_def: "<[m::nat]> = Oc # Oc\<^bsup>m\<^esup>" -apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) -done -*) lemma [simp]: "<[x::nat]> = Oc\<up>(Suc x)" apply(simp add: tape_of_nat_abv tape_of_nl_abv) done @@ -4454,20 +4440,20 @@ else if s = 2*n + 4 then 2 else 0)" -fun abc_mopup_measure :: "(config \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)" - where - "abc_mopup_measure (c, n) = - (abc_mopup_stage1 c n, abc_mopup_stage2 c n, - abc_mopup_stage3 c n)" - -definition abc_mopup_LE :: - "(((nat \<times> cell list \<times> cell list) \<times> nat) \<times> - ((nat \<times> cell list \<times> cell list) \<times> nat)) set" - where - "abc_mopup_LE \<equiv> (inv_image lex_triple abc_mopup_measure)" - -lemma wf_abc_mopup_le[intro]: "wf abc_mopup_LE" -by(auto intro:wf_inv_image simp:abc_mopup_LE_def lex_triple_def lex_pair_def) +definition + "abc_mopup_measure = measures [\<lambda>(c, n). abc_mopup_stage1 c n, + \<lambda>(c, n). abc_mopup_stage2 c n, + \<lambda>(c, n). abc_mopup_stage3 c n]" + +lemma wf_abc_mopup_measure: + shows "wf abc_mopup_measure" +unfolding abc_mopup_measure_def +by auto + +lemma abc_mopup_measure_induct [case_names Step]: + "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" +using wf_abc_mopup_measure +by (metis wf_iff_no_infinite_down_chain) lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False" apply(auto simp: mopup_bef_erase_a.simps) @@ -4494,12 +4480,6 @@ apply(rule mopup_a_nth, auto) done -(* FIXME: is also in uncomputable *) -lemma halt_lemma: - "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" -by (metis wf_iff_no_infinite_down_chain) - - lemma mopup_halt: assumes less: "n < length lm" @@ -4507,39 +4487,35 @@ and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" and P: "P = (\<lambda> (c, n). is_final c)" shows "\<exists> stp. P (f stp)" -proof(rule_tac LE = abc_mopup_LE in halt_lemma) - show "wf abc_mopup_LE" by(auto) -next - show "\<forall>n. \<not> P (f n) \<longrightarrow> (f (Suc n), f n) \<in> abc_mopup_LE" - proof(rule_tac allI, rule_tac impI) - fix na - assume h: "\<not> P (f na)" - show "(f (Suc na), f na) \<in> abc_mopup_LE" - proof(simp add: f) - obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" - apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) - done - then have "mopup_inv (a, b, c) lm n ires" - using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] - apply(simp) - done - moreover have "a > 0" - using h g - apply(simp add: f P) - done - ultimately have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_LE" - apply(case_tac c, case_tac [2] aa) - apply(auto split:if_splits simp add:step.simps mopup_inv.simps) - apply(simp_all add: mopupfetchs abc_mopup_LE_def lex_triple_def lex_pair_def ) - done - thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) - (mopup_a n @ shift mopup_b (2 * n), 0), n), - steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) - \<in> abc_mopup_LE" - using g by simp - qed +proof (induct rule: abc_mopup_measure_induct) + case (Step na) + have h: "\<not> P (f na)" by fact + show "(f (Suc na), f na) \<in> abc_mopup_measure" + proof(simp add: f) + obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" + apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) + done + then have "mopup_inv (a, b, c) lm n ires" + using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] + apply(simp) + done + moreover have "a > 0" + using h g + apply(simp add: f P) + done + ultimately + have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure" + apply(case_tac c, case_tac [2] aa) + apply(auto split:if_splits simp add:step.simps mopup_inv.simps) + apply(simp_all add: mopupfetchs abc_mopup_measure_def lex_triple_def lex_pair_def ) + done + thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) + (mopup_a n @ shift mopup_b (2 * n), 0), n), + steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) + \<in> abc_mopup_measure" + using g by simp qed -qed +qed lemma mopup_inv_start: "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" @@ -4689,44 +4665,45 @@ lemma compile_correct_unhalt: assumes layout: "ly = layout_of ap" and compile: "tp = tm_of ap" - and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" + and crsp: "crsp ly (0, lm) (1, l, r) ires" and off: "off = length tp div 2" and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)" - shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)" + shows "\<forall> stp.\<not> is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stp)" using assms proof(rule_tac allI, rule_tac notI) fix stp - assume h: "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)" + assume h: "is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stp)" obtain as am where a: "abc_steps_l (0, lm) ap stp = (as, am)" by(case_tac "abc_steps_l (0, lm) ap stp", auto) then have b: "as < length ap" using abc_unhalt by(erule_tac x = stp in allE, simp) - have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires " + have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (1, l, r) (tp, 0) stpa) ires " using assms b a - apply(rule_tac crsp_steps2, simp_all) + apply(simp add: numeral) + apply(rule_tac crsp_steps2) + apply(simp_all) done - then obtain stpa where - "stpa\<ge>stp \<and> crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" .. - then obtain s' l' r' where b: "(steps (Suc 0, l, r) (tp, 0) stpa) = (s', l', r') \<and> + then obtain stpa where + "stpa\<ge>stp \<and> crsp ly (as, am) (steps (1, l, r) (tp, 0) stpa) ires" .. + then obtain s' l' r' where b: "(steps (1, l, r) (tp, 0) stpa) = (s', l', r') \<and> stpa\<ge>stp \<and> crsp ly (as, am) (s', l', r') ires" - by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto) + by(case_tac "steps (1, l, r) (tp, 0) stpa", auto) hence c: - "(steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" + "(steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps) from b have d: "s' > 0 \<and> stpa \<ge> stp" by(simp add: crsp.simps) then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add) obtain s'' l'' r'' where f: - "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" + "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" using h - by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto) + by(case_tac "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp", auto) then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" by(auto intro: after_is_final) - then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)" - using e - by(simp add: steps_add f) + then have "is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa)" + using e f by simp from this and c d show "False" by simp qed diff -r 6013ca0e6e22 -r eccd79a974ae thys/UTM.thy --- a/thys/UTM.thy Wed Feb 13 20:08:14 2013 +0000 +++ b/thys/UTM.thy Thu Feb 14 09:31:19 2013 +0000 @@ -5086,16 +5086,16 @@ lemma tutm_uhalt': assumes tm_wf: "tm_wf (tp,0)" - and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))" - shows "\<forall> stp. \<not> is_final (steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)" -apply(simp add: t_utm_def) + and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (1, Bk\<up>(l), <lm>) tp stp))" + shows "\<forall> stp. \<not> is_final (steps0 (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)" +unfolding t_utm_def proof(rule_tac compile_correct_unhalt) show "layout_of F_aprog = layout_of F_aprog" by simp next show "F_tprog = tm_of F_aprog" by(simp add: F_tprog_def) next - show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) []" + show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) []" by(auto simp: crsp.simps start_of.simps) next show "length F_tprog div 2 = length F_tprog div 2" by simp @@ -5154,7 +5154,7 @@ \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))\<rbrakk> \<Longrightarrow> \<forall> stp. \<not> is_final (steps0 (Suc 0, Bk\<up>(m), <[code tp, bl2wc (<args>)]> @ Bk\<up>(n)) t_utm stp)" apply(rule_tac tape_normalize) -apply(rule_tac tutm_uhalt', simp_all) +apply(rule_tac tutm_uhalt'[simplified], simp_all) done lemma UTM_uhalt_lemma_pre: