equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Undeciablity of the {\em Halting problem} *} |
6 header {* Undeciablity of the {\em Halting problem} *} |
7 |
7 |
8 theory uncomputable |
8 theory uncomputable |
9 imports Main turing_basic |
9 imports Main turing_hoare |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 The {\em Copying} TM, which duplicates its input. |
13 The {\em Copying} TM, which duplicates its input. |
14 *} |
14 *} |
1141 apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add) |
1141 apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add) |
1142 apply arith |
1142 apply arith |
1143 apply(drule_tac length_eq, simp) |
1143 apply(drule_tac length_eq, simp) |
1144 done |
1144 done |
1145 |
1145 |
1146 lemma Hoare_weak: |
|
1147 fixes p::tprog0 |
|
1148 assumes a: "{P} p {Q}" |
|
1149 and b: "P' \<mapsto> P" |
|
1150 and c: "Q \<mapsto> Q'" |
|
1151 shows "{P'} p {Q'}" |
|
1152 using assms |
|
1153 unfolding Hoare_def assert_imp_def |
|
1154 by (blast intro: holds_for_imp[simplified assert_imp_def]) |
|
1155 |
1146 |
1156 text {* |
1147 text {* |
1157 The following locale specifies that TM @{text "H"} can be used to solve |
1148 The following locale specifies that TM @{text "H"} can be used to solve |
1158 the {\em Halting Problem} and @{text "False"} is going to be derived |
1149 the {\em Halting Problem} and @{text "False"} is going to be derived |
1159 under this locale. Therefore, the undecidability of {\em Halting Problem} |
1150 under this locale. Therefore, the undecidability of {\em Halting Problem} |