# HG changeset patch # User Christian Urban # Date 1358609241 0 # Node ID 0838b0ac52ab88f3141b78fdd2d5a817da67bf83 # Parent cd4ef33c8fb1a4c88bc81230bd1a94f9fdfb3832 some small changes to turing and uncomputable diff -r cd4ef33c8fb1 -r 0838b0ac52ab paper.pdf Binary file paper.pdf has changed diff -r cd4ef33c8fb1 -r 0838b0ac52ab thys/turing_basic.thy --- a/thys/turing_basic.thy Sat Jan 19 14:44:07 2013 +0000 +++ b/thys/turing_basic.thy Sat Jan 19 15:27:21 2013 +0000 @@ -95,6 +95,65 @@ shows "steps c p (m + n) = steps (steps c p m) p n" by (induct m arbitrary: c) (auto) +lemma step_0 [simp]: + shows "step (0, (l, r)) p = (0, (l, r))" +by (case_tac p, simp) + +lemma steps_0 [simp]: + shows "steps (0, (l, r)) p n = (0, (l, r))" +by (induct n) (simp_all) + + + +fun + is_final :: "config \ bool" +where + "is_final (s, l, r) = (s = 0)" + +lemma is_final_eq: + shows "is_final (s, tp) = (s = 0)" +by (case_tac tp) (auto) + +lemma is_final_steps: + assumes "is_final (s, l, r)" + shows "is_final (steps (s, l, r) (p, off) n)" +using assms +by (induct n) (auto) + + +(* if the machine is in the halting state, there must have + been a state just before the halting state *) +lemma before_final: + assumes "steps0 (1, tp) A n = (0, tp')" + shows "\ n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" +using assms +proof(induct n arbitrary: tp') + case (0 tp') + have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact + then show "\n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" + by simp +next + case (Suc n tp') + have ih: "\tp'. steps0 (1, tp) A n = (0, tp') \ + \n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" by fact + have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact + obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)" + by (auto intro: is_final.cases) + then show "\n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" + proof (cases "s = 0") + case True (* in halting state *) + then have "steps0 (1, tp) A n = (0, tp')" + using asm cases by (simp del: steps.simps) + then show ?thesis using ih by simp + next + case False (* not in halting state *) + then have "\ is_final (steps0 (1, tp) A n) \ steps0 (1, tp) A (Suc n) = (0, tp')" + using asm cases by simp + then show ?thesis by auto + qed +qed + +(* well-formedness of Turing machine programs *) fun tm_wf :: "tprog \ bool" where @@ -135,117 +194,54 @@ "adjust p = map (\ (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p" lemma length_shift [simp]: - "length (shift p n) = length p" + shows "length (shift p n) = length p" by simp -lemma length_adjust[simp]: +lemma length_adjust [simp]: shows "length (adjust p) = length p" by (induct p) (auto) + +(* composition of two Turing machines *) fun tm_comp :: "instr list \ instr list \ instr list" ("_ |+| _" [0, 0] 100) where "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" -lemma step_0 [simp]: - shows "step (0, (l, r)) p = (0, (l, r))" -by (case_tac p, simp) - -lemma steps_0 [simp]: - shows "steps (0, (l, r)) p n = (0, (l, r))" -by (induct n) (simp_all) - -fun - is_final :: "config \ bool" -where - "is_final (s, l, r) = (s = 0)" - -lemma is_final_steps: - assumes "is_final (s, l, r)" - shows "is_final (steps (s, l, r) (p, off) n)" -using assms by (induct n) (auto) - - - -(* if the machine is in the halting state, there must have - been a state just before the halting state *) -lemma before_final: - assumes "steps0 (1, tp) A n = (0, tp')" - shows "\ n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" -using assms -proof(induct n arbitrary: tp') - case (0 tp') - have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact - then show "\n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" - by simp -next - case (Suc n tp') - have ih: "\tp'. steps0 (1, tp) A n = (0, tp') \ - \n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" by fact - have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact - obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)" - by (auto intro: is_final.cases) - then show "\n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" - proof (cases "s = 0") - case True (* in halting state *) - then have "steps0 (1, tp) A n = (0, tp')" - using asm cases by (simp del: steps.simps) - then show ?thesis using ih by simp - next - case False (* not in halting state *) - then have "\ is_final (steps0 (1, tp) A n) \ steps0 (1, tp) A (Suc n) = (0, tp')" - using asm cases by simp - then show ?thesis by auto - qed -qed - - -lemma length_comp: +lemma tm_comp_length: shows "length (A |+| B) = length A + length B" by auto -declare steps.simps[simp del] -declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] - - -lemma tmcomp_fetch_in_first: +lemma tm_comp_fetch_in_first: assumes "case (fetch A a x) of (ac, ns) \ ns \ 0" shows "fetch (A |+| B) a x = fetch A a x" using assms -apply(case_tac a, case_tac [!] x, -auto simp: length_comp tm_comp.simps length_adjust nth_append) -apply(simp_all add: adjust.simps) -done - - -lemma is_final_eq: "is_final (ba, tp) = (ba = 0)" -apply(case_tac tp, simp add: is_final.simps) +apply(case_tac a) +apply(case_tac [!] x) +apply(auto simp: tm_comp_length nth_append) done lemma t_merge_pre_eq_step: - assumes step: "step (a, b, c) (A, 0) = cf" + assumes step: "step0 (s, l, r) A = cf" and tm_wf: "tm_wf (A, 0)" and unfinal: "\ is_final cf" - shows "step (a, b, c) (A |+| B, 0) = cf" + shows "step0 (s, l, r) (A |+| B) = cf" proof - - have "fetch (A |+| B) a (read c) = fetch A a (read c)" - proof(rule_tac tmcomp_fetch_in_first) - from step and unfinal show "case fetch A a (read c) of (ac, ns) \ ns \ 0" - apply(auto simp: is_final.simps) - apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq) - done - qed - thus "?thesis" - using step - apply(auto simp: step.simps is_final.simps) - done + from step unfinal + have "\ is_final (step0 (s, l, r) A)" by simp + then have "fetch (A |+| B) s (read r) = fetch A s (read r)" + by (rule_tac tm_comp_fetch_in_first) (auto simp add: is_final_eq) + then show ?thesis + using step by auto qed +declare steps.simps[simp del] +declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] declare tm_wf.simps[simp del] step.simps[simp del] lemma t_merge_pre_eq: - "\steps (Suc 0, tp) (A, 0) stp = cf; \ is_final cf; tm_wf (A, 0)\ - \ steps (Suc 0, tp) (A |+| B, 0) stp = cf" + "\steps0 (Suc 0, tp) A stp = cf; \ is_final cf; tm_wf (A, 0)\ + \ steps0 (Suc 0, tp) (A |+| B) stp = cf" proof(induct stp arbitrary: cf, simp add: steps.simps) fix stp cf assume ind: "\cf. \steps (Suc 0, tp) (A, 0) stp = cf; \ is_final cf; tm_wf (A, 0)\ @@ -280,7 +276,7 @@ shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))" using assms apply(case_tac a, case_tac [!] x, -auto simp: length_comp tm_comp.simps length_adjust nth_append) +auto simp: tm_comp_length tm_comp.simps length_adjust nth_append) apply(simp_all add: adjust.simps) done @@ -376,7 +372,7 @@ \ fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)" apply(case_tac x) apply(case_tac [!] sa', - auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps + auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps tm_wf.simps shift.simps split: if_splits) done @@ -385,7 +381,7 @@ \ fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" apply(case_tac x) apply(case_tac [!] sa, - auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps + auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps tm_wf.simps shift.simps split: if_splits) done diff -r cd4ef33c8fb1 -r 0838b0ac52ab thys/turing_hoare.thy --- a/thys/turing_hoare.thy Sat Jan 19 14:44:07 2013 +0000 +++ b/thys/turing_hoare.thy Sat Jan 19 15:27:21 2013 +0000 @@ -2,8 +2,6 @@ imports turing_basic begin - - type_synonym assert = "tape \ bool" definition @@ -11,8 +9,6 @@ where "P \ Q \ \l r. P (l, r) \ Q (l, r)" - - fun holds_for :: "(tape \ bool) \ config \ bool" ("_ holds'_for _" [100, 99] 100) where @@ -48,8 +44,8 @@ text {* - {P1} A {Q1} {P2} B {Q2} Q1 \ P2 - ----------------------------------- + {P1} A {Q1} {P2} B {Q2} Q1 \ P2 A, B well-formed + ------------------------------------------------------ {P1} A |+| B {Q2} *} @@ -79,12 +75,12 @@ where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)" using B_halt unfolding Hoare_def by auto then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" - by (case_tac "steps0 (1, l', r') B n2", auto) + by (case_tac "steps0 (1, l', r') B n2") (auto) then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')" by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf) ultimately show "\n. is_final (steps0 (1, l, r) (A |+| B) n) \ Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" - using g + using g apply(rule_tac x = "stpa + n2" in exI) apply(simp add: steps_add) done @@ -93,8 +89,7 @@ definition Hoare_unhalt :: "assert \ tprog0 \ bool" ("({(1_)}/ (_))" 50) where - "{P} p \ - (\l r. P (l, r) \ (\ n . \ (is_final (steps0 (1, (l, r)) p n))))" + "{P} p \ (\l r. P (l, r) \ (\ n . \ (is_final (steps0 (1, (l, r)) p n))))" lemma Hoare_unhalt_I: assumes "\l r. P (l, r) \ \ n. \ is_final (steps0 (1, (l, r)) p n)" diff -r cd4ef33c8fb1 -r 0838b0ac52ab thys/uncomputable.thy --- a/thys/uncomputable.thy Sat Jan 19 14:44:07 2013 +0000 +++ b/thys/uncomputable.thy Sat Jan 19 15:27:21 2013 +0000 @@ -984,7 +984,7 @@ by(auto simp: tm_wf.simps tcopy_end_def) lemma [intro]: "\tm_wf (A, 0); tm_wf (B, 0)\ \ tm_wf (A |+| B, 0)" -apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp +apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps) done