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