893 assumes "0 < x" |
893 assumes "0 < x" |
894 shows "{inv_begin1 x} tcopy {inv_end0 x}" |
894 shows "{inv_begin1 x} tcopy {inv_end0 x}" |
895 proof - |
895 proof - |
896 have "{inv_begin1 x} tcopy_begin {inv_begin0 x}" |
896 have "{inv_begin1 x} tcopy_begin {inv_begin0 x}" |
897 by (metis assms begin_correct) |
897 by (metis assms begin_correct) |
898 moreover |
898 moreover |
899 have "{inv_loop1 x} tcopy_loop {inv_loop0 x}" |
|
900 by (metis assms loop_correct) |
|
901 moreover |
|
902 have "inv_begin0 x \<mapsto> inv_loop1 x" |
899 have "inv_begin0 x \<mapsto> inv_loop1 x" |
903 unfolding assert_imp_def |
900 unfolding assert_imp_def |
904 unfolding inv_begin0.simps inv_loop1.simps |
901 unfolding inv_begin0.simps inv_loop1.simps |
905 unfolding inv_loop1_loop.simps inv_loop1_exit.simps |
902 unfolding inv_loop1_loop.simps inv_loop1_exit.simps |
906 apply(auto simp add: numeral Cons_eq_append_conv) |
903 apply(auto simp add: numeral Cons_eq_append_conv) |
907 by (rule_tac x = "Suc 0" in exI, auto) |
904 by (rule_tac x = "Suc 0" in exI, auto) |
|
905 ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}" |
|
906 by (rule_tac Hoare_consequence) (auto) |
|
907 moreover |
|
908 have "{inv_loop1 x} tcopy_loop {inv_loop0 x}" |
|
909 by (metis assms loop_correct) |
908 ultimately |
910 ultimately |
909 have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}" |
911 have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}" |
910 by (rule_tac Hoare_plus_halt) (auto) |
912 by (rule_tac Hoare_plus_halt) (auto) |
911 moreover |
913 moreover |
912 have "{inv_end1 x} tcopy_end {inv_end0 x}" |
914 have "{inv_end1 x} tcopy_end {inv_end0 x}" |
913 by (metis assms end_correct) |
915 by (metis assms end_correct) |
914 moreover |
916 moreover |
915 have "inv_loop0 x \<mapsto> inv_end1 x" |
917 have "inv_loop0 x = inv_end1 x" |
916 by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def) |
918 by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def) |
917 ultimately |
919 ultimately |
918 show "{inv_begin1 x} tcopy {inv_end0 x}" |
920 show "{inv_begin1 x} tcopy {inv_end0 x}" |
919 unfolding tcopy_def |
921 unfolding tcopy_def |
920 by (rule_tac Hoare_plus_halt) (auto) |
922 by (rule_tac Hoare_plus_halt) (auto) |
953 where |
955 where |
954 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] " |
956 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] " |
955 |
957 |
956 (* invariants of dither *) |
958 (* invariants of dither *) |
957 abbreviation (input) |
959 abbreviation (input) |
958 "dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))" |
960 "dither_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)" |
959 |
961 |
960 abbreviation (input) |
962 abbreviation (input) |
961 "dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))" |
963 "dither_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)" |
962 |
964 |
963 lemma dither_loops_aux: |
965 lemma dither_loops_aux: |
964 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
966 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
965 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
967 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
966 apply(induct stp) |
968 apply(induct stp) |
972 apply(rule Hoare_unhaltI) |
974 apply(rule Hoare_unhaltI) |
973 using dither_loops_aux |
975 using dither_loops_aux |
974 apply(auto simp add: numeral tape_of_nat_abv) |
976 apply(auto simp add: numeral tape_of_nat_abv) |
975 by (metis Suc_neq_Zero is_final_eq) |
977 by (metis Suc_neq_Zero is_final_eq) |
976 |
978 |
977 |
|
978 lemma dither_halts_aux: |
979 lemma dither_halts_aux: |
979 shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])" |
980 shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])" |
980 unfolding dither_def |
981 unfolding dither_def |
981 by (simp add: steps.simps step.simps numeral) |
982 by (simp add: steps.simps step.simps numeral) |
982 |
983 |
986 using dither_halts_aux |
987 using dither_halts_aux |
987 apply(auto simp add: tape_of_nat_abv) |
988 apply(auto simp add: tape_of_nat_abv) |
988 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) |
989 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) |
989 |
990 |
990 |
991 |
991 |
|
992 section {* The diagnal argument below shows the undecidability of Halting problem *} |
992 section {* The diagnal argument below shows the undecidability of Halting problem *} |
993 |
993 |
994 text {* |
994 text {* |
995 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
995 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
996 and the final configuration is standard. |
996 and the final configuration is standard. |
997 *} |
997 *} |
998 |
998 |
999 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool" |
999 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool" |
1000 where |
1000 where |
1001 "haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k, <n::nat>)))}" |
1001 "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k, <n::nat>)))}" |
1002 |
1002 |
1003 lemma [intro, simp]: "tm_wf0 tcopy" |
1003 lemma [intro, simp]: "tm_wf0 tcopy" |
1004 by (auto simp: tcopy_def) |
1004 by (auto simp: tcopy_def) |
1005 |
1005 |
1006 lemma [intro, simp]: "tm_wf0 dither" |
1006 lemma [intro, simp]: "tm_wf0 dither" |
1024 assumes h_wf[intro]: "tm_wf0 H" |
1024 assumes h_wf[intro]: "tm_wf0 H" |
1025 -- {* |
1025 -- {* |
1026 The following two assumptions specifies that @{text "H"} does solve the Halting problem. |
1026 The following two assumptions specifies that @{text "H"} does solve the Halting problem. |
1027 *} |
1027 *} |
1028 and h_case: |
1028 and h_case: |
1029 "\<And> M lm. haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>))}" |
1029 "\<And> M ns. haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}" |
1030 and nh_case: |
1030 and nh_case: |
1031 "\<And> M lm. \<not> haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>))}" |
1031 "\<And> M ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}" |
1032 begin |
1032 begin |
1033 |
1033 |
1034 (* invariants for H *) |
1034 (* invariants for H *) |
1035 abbreviation |
1035 abbreviation |
1036 "pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)" |
1036 "pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)" |
1037 |
1037 |
1038 abbreviation |
1038 abbreviation |
1039 "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)" |
1039 "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)" |
1040 |
1040 |
1041 abbreviation |
1041 abbreviation |
1042 "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)" |
1042 "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)" |
1043 |
1043 |
1044 |
1044 |
1045 lemma H_halt_inv: |
1045 lemma H_halt_inv: |
1046 assumes "\<not> haltP M [n]" |
1046 assumes "\<not> haltP M [n]" |
1047 shows "{pre_H_inv M n} H {post_H_halt_inv}" |
1047 shows "{pre_H_inv M n} H {post_H_halt_inv}" |
1065 shows "False" |
1065 shows "False" |
1066 proof - |
1066 proof - |
1067 (* invariants *) |
1067 (* invariants *) |
1068 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)" |
1068 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)" |
1069 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)" |
1069 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)" |
1070 def P3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)" |
1070 def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)" |
1071 |
1071 |
1072 (* |
1072 (* |
1073 {P1} tcopy {P2} {P2} H {P3} |
1073 {P1} tcopy {P2} {P2} H {P3} |
1074 ---------------------------- |
1074 ---------------------------- |
1075 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1075 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1079 |
1079 |
1080 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1080 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1081 |
1081 |
1082 (* {P1} (tcopy |+| H) {P3} *) |
1082 (* {P1} (tcopy |+| H) {P3} *) |
1083 have first: "{P1} (tcopy |+| H) {P3}" |
1083 have first: "{P1} (tcopy |+| H) {P3}" |
1084 proof (cases rule: Hoare_plus_halt_simple) |
1084 proof (cases rule: Hoare_plus_halt) |
1085 case A_halt (* of tcopy *) |
1085 case A_halt (* of tcopy *) |
1086 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1086 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1087 by (rule tcopy_correct) |
1087 by (rule tcopy_correct) |
1088 next |
1088 next |
1089 case B_halt (* of H *) |
1089 case B_halt (* of H *) |
1097 by (rule dither_halts) |
1097 by (rule dither_halts) |
1098 |
1098 |
1099 (* {P1} tcontra {P3} *) |
1099 (* {P1} tcontra {P3} *) |
1100 have "{P1} tcontra {P3}" |
1100 have "{P1} tcontra {P3}" |
1101 unfolding tcontra_def |
1101 unfolding tcontra_def |
1102 by (rule Hoare_plus_halt_simple[OF first second H_wf]) |
1102 by (rule Hoare_plus_halt[OF first second H_wf]) |
1103 |
1103 |
1104 with assms show "False" |
1104 with assms show "False" |
1105 unfolding P1_def P3_def |
1105 unfolding P1_def P3_def |
1106 unfolding haltP_def |
1106 unfolding haltP_def |
1107 unfolding Hoare_halt_def |
1107 unfolding Hoare_halt_def |
1118 shows "False" |
1118 shows "False" |
1119 proof - |
1119 proof - |
1120 (* invariants *) |
1120 (* invariants *) |
1121 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)" |
1121 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)" |
1122 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)" |
1122 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)" |
1123 def Q3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)" |
1123 def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)" |
1124 |
1124 |
1125 (* |
1125 (* |
1126 {P1} tcopy {P2} {P2} H {Q3} |
1126 {P1} tcopy {P2} {P2} H {Q3} |
1127 ---------------------------- |
1127 ---------------------------- |
1128 {P1} (tcopy |+| H) {Q3} {Q3} dither loops |
1128 {P1} (tcopy |+| H) {Q3} {Q3} dither loops |
1132 |
1132 |
1133 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1133 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1134 |
1134 |
1135 (* {P1} (tcopy |+| H) {Q3} *) |
1135 (* {P1} (tcopy |+| H) {Q3} *) |
1136 have first: "{P1} (tcopy |+| H) {Q3}" |
1136 have first: "{P1} (tcopy |+| H) {Q3}" |
1137 proof (cases rule: Hoare_plus_halt_simple) |
1137 proof (cases rule: Hoare_plus_halt) |
1138 case A_halt (* of tcopy *) |
1138 case A_halt (* of tcopy *) |
1139 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1139 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1140 by (rule tcopy_correct) |
1140 by (rule tcopy_correct) |
1141 next |
1141 next |
1142 case B_halt (* of H *) |
1142 case B_halt (* of H *) |
1150 by (rule dither_loops) |
1150 by (rule dither_loops) |
1151 |
1151 |
1152 (* {P1} tcontra loops *) |
1152 (* {P1} tcontra loops *) |
1153 have "{P1} tcontra \<up>" |
1153 have "{P1} tcontra \<up>" |
1154 unfolding tcontra_def |
1154 unfolding tcontra_def |
1155 by (rule Hoare_plus_unhalt_simple[OF first second H_wf]) |
1155 by (rule Hoare_plus_unhalt[OF first second H_wf]) |
1156 |
1156 |
1157 with assms show "False" |
1157 with assms show "False" |
1158 unfolding P1_def |
1158 unfolding P1_def |
1159 unfolding haltP_def |
1159 unfolding haltP_def |
1160 unfolding Hoare_halt_def Hoare_unhalt_def |
1160 unfolding Hoare_halt_def Hoare_unhalt_def |