| changeset 168 | d7570dbf9f06 |
| parent 163 | 67063c5365e1 |
| child 169 | 6013ca0e6e22 |
| 167:641512ab0f6c | 168:d7570dbf9f06 |
|---|---|
1 (* Title: Turing machine's definition and its charater |
1 (* Title: thys/Uncomputable.thy |
2 Author: XuJian <xujian817@hotmail.com> |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
3 Maintainer: Xujian |
|
4 *) |
3 *) |
5 |
4 |
6 header {* Undeciablity of the {\em Halting problem} *} |
5 header {* Undeciablity of the Halting Problem *} |
7 |
6 |
8 theory Uncomputable |
7 theory Uncomputable |
9 imports Turing_Hoare |
8 imports Turing_Hoare |
10 begin |
9 begin |
11 |
10 |
17 and "5 = Suc 4" |
16 and "5 = Suc 4" |
18 and "6 = Suc 5" |
17 and "6 = Suc 5" |
19 and "7 = Suc 6" |
18 and "7 = Suc 6" |
20 and "8 = Suc 7" |
19 and "8 = Suc 7" |
21 and "9 = Suc 8" |
20 and "9 = Suc 8" |
22 and "10 = Suc 9" |
21 and "10 = Suc 9" |
23 by arith+ |
22 by simp_all |
24 |
23 |
25 text {* |
24 text {* The Copying TM, which duplicates its input. *} |
26 The {\em Copying} TM, which duplicates its input. |
|
27 *} |
|
28 |
25 |
29 definition |
26 definition |
30 tcopy_begin :: "instr list" |
27 tcopy_begin :: "instr list" |
31 where |
28 where |
32 "tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2), |
29 "tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2), |
86 assumes "inv_begin n cf" |
83 assumes "inv_begin n cf" |
87 and "n > 0" |
84 and "n > 0" |
88 shows "inv_begin n (step0 cf tcopy_begin)" |
85 shows "inv_begin n (step0 cf tcopy_begin)" |
89 using assms |
86 using assms |
90 unfolding tcopy_begin_def |
87 unfolding tcopy_begin_def |
91 apply(case_tac cf) |
88 apply(cases cf) |
92 apply(auto simp: numeral split: if_splits) |
89 apply(auto simp: numeral split: if_splits) |
93 apply(case_tac "hd c") |
90 apply(case_tac "hd c") |
94 apply(auto) |
91 apply(auto) |
95 apply(case_tac c) |
92 apply(case_tac c) |
96 apply(simp_all) |
93 apply(simp_all) |