# HG changeset patch # User Christian Urban # Date 1360676227 0 # Node ID d7570dbf9f06e1d129dc86b78c3e60432ba008d7 # Parent 641512ab0f6c18e692b765b897556caf68e0422e small changes diff -r 641512ab0f6c -r d7570dbf9f06 thys/Turing.thy --- a/thys/Turing.thy Mon Feb 11 08:46:24 2013 +0000 +++ b/thys/Turing.thy Tue Feb 12 13:37:07 2013 +0000 @@ -1,8 +1,9 @@ -(* Title: Turing machines - Author: Xu Jian - Maintainer: Xu Jian +(* Title: thys/Turing.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) +header {* Turing Machines *} + theory Turing imports Main begin @@ -26,8 +27,7 @@ type_synonym config = "state \ tape" fun nth_of where - "nth_of xs i = (if i \ length xs then None - else Some (xs ! i))" + "nth_of xs i = (if i \ length xs then None else Some (xs ! i))" lemma nth_of_map [simp]: shows "nth_of (map f p) n = (case (nth_of p n) of None \ None | Some x \ Some (f x))" @@ -75,15 +75,14 @@ "step (s, l, r) (p, off) = (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" +abbreviation + "step0 c p \ step c (p, 0)" + fun steps :: "config \ tprog \ nat \ config" where "steps c p 0 = c" | "steps c p (Suc n) = steps (step c p) p n" - -abbreviation - "step0 c p \ step c (p, 0)" - abbreviation "steps0 c p n \ steps c (p, 0) n" @@ -103,8 +102,6 @@ shows "steps (0, (l, r)) p n = (0, (l, r))" by (induct n) (simp_all) - - fun is_final :: "config \ bool" where @@ -233,8 +230,7 @@ lemma tm_comp_wf[intro]: "\tm_wf (A, 0); tm_wf (B, 0)\ \ tm_wf (A |+| B, 0)" -by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps) - +by (auto) lemma tm_comp_step: assumes unfinal: "\ is_final (step0 c A)" @@ -334,7 +330,8 @@ by (metis step_in_range step_red) qed -lemma tm_comp_pre_halt_same: +(* if A goes into the final state, then A |+| B will go into the first state of B *) +lemma tm_comp_next: assumes a_ht: "steps0 (1, tp) A n = (0, tp')" and a_wf: "tm_wf (A, 0)" obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')" @@ -376,7 +373,7 @@ done -lemma tm_comp_second_same: +lemma tm_comp_second: assumes a_wf: "tm_wf (A, 0)" and steps: "steps0 (1, l, r) B stp = (s', l', r')" shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp @@ -418,11 +415,12 @@ ultimately show ?case by blast qed -lemma tm_comp_second_halt_same: + +lemma tm_comp_final: assumes "tm_wf (A, 0)" and "steps0 (1, l, r) B stp = (0, l', r')" shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" -using tm_comp_second_same[OF assms] by (simp) +using tm_comp_second[OF assms] by (simp) end diff -r 641512ab0f6c -r d7570dbf9f06 thys/Turing_Hoare.thy --- a/thys/Turing_Hoare.thy Mon Feb 11 08:46:24 2013 +0000 +++ b/thys/Turing_Hoare.thy Tue Feb 12 13:37:07 2013 +0000 @@ -1,3 +1,9 @@ +(* Title: thys/Turing_Hoare.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban +*) + +header {* Hoare Rules for TMs *} + theory Turing_Hoare imports Turing begin @@ -37,7 +43,6 @@ where "{P} p {Q} \ \tp. P tp \ (\n. is_final (steps0 (1, tp) p n) \ Q holds_for (steps0 (1, tp) p n))" - (* not halting case *) definition Hoare_unhalt :: "assert \ tprog0 \ bool" ("({(1_)}/ (_)) \" 50) @@ -83,7 +88,7 @@ by (metis is_final_eq surj_pair) then obtain n2 where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" - using A_wf by (rule_tac tm_comp_pre_halt_same) + using A_wf by (rule_tac tm_comp_next) moreover from a1 a2 have "Q (l', r')" by (simp) then obtain n3 l'' r'' @@ -93,7 +98,7 @@ using B_halt unfolding Hoare_halt_def by (metis is_final_eq surj_pair) then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n3 = (0, l'', r'')" - using A_wf by (rule_tac tm_comp_second_halt_same) + using A_wf by (rule_tac tm_comp_final) ultimately show "\n. is_final (steps0 (1, l, r) (A |+| B) n) \ S holds_for (steps0 (1, l, r) (A |+| B) n)" using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) @@ -120,7 +125,7 @@ using A_halt unfolding Hoare_halt_def by (metis is_final_eq surj_pair) then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" - using A_wf by (rule_tac tm_comp_pre_halt_same) + using A_wf by (rule_tac tm_comp_next) then show "\ is_final (steps0 (1, l, r) (A |+| B) n)" proof(cases "n2 \ n") case True @@ -132,7 +137,7 @@ where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" and "\ is_final (s'', l'', r'')" by (metis surj_pair) then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" - using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps) + using A_wf by (auto dest: tm_comp_second simp del: tm_wf.simps) then have "\ is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) then show "\ is_final (steps0 (1, l, r) (A |+| B) n)" diff -r 641512ab0f6c -r d7570dbf9f06 thys/Uncomputable.thy --- a/thys/Uncomputable.thy Mon Feb 11 08:46:24 2013 +0000 +++ b/thys/Uncomputable.thy Tue Feb 12 13:37:07 2013 +0000 @@ -1,9 +1,8 @@ -(* Title: Turing machine's definition and its charater - Author: XuJian - Maintainer: Xujian +(* Title: thys/Uncomputable.thy + Author: Jian Xu, Xingyuan Zhang, and Christian Urban *) -header {* Undeciablity of the {\em Halting problem} *} +header {* Undeciablity of the Halting Problem *} theory Uncomputable imports Turing_Hoare @@ -19,12 +18,10 @@ and "7 = Suc 6" and "8 = Suc 7" and "9 = Suc 8" - and "10 = Suc 9" - by arith+ + and "10 = Suc 9" +by simp_all -text {* - The {\em Copying} TM, which duplicates its input. -*} +text {* The Copying TM, which duplicates its input. *} definition tcopy_begin :: "instr list" @@ -88,7 +85,7 @@ shows "inv_begin n (step0 cf tcopy_begin)" using assms unfolding tcopy_begin_def -apply(case_tac cf) +apply(cases cf) apply(auto simp: numeral split: if_splits) apply(case_tac "hd c") apply(auto)