Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Uncomputable.thy
changeset 288 a9003e6d0463
parent 169 6013ca0e6e22
child 291 93db7414931d
equal deleted inserted replaced
287:d5a0e25c4742 288:a9003e6d0463 
     1 (* Title: thys/Uncomputable.thy
 
     1 (* Title: thys/Uncomputable.thy
 
     2    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 
     2    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 
     3 *)
 
     3 *)
 
     4 
     4 
     5 header {* Undeciablity of the Halting Problem *}
 
     5 chapter {* Undeciablity of the Halting Problem *}
 
     6 
     6 
     7 theory Uncomputable
 
     7 theory Uncomputable
 
     8 imports Turing_Hoare
 
     8 imports Turing_Hoare
 
     9 begin
 
     9 begin
 
    10 
    10 
    17   and "6 = Suc 5" 
    17   and "6 = Suc 5" 
    18   and "7 = Suc 6"
 
    18   and "7 = Suc 6"
 
    19   and "8 = Suc 7" 
    19   and "8 = Suc 7" 
    20   and "9 = Suc 8" 
    20   and "9 = Suc 8" 
    21   and "10 = Suc 9"
 
    21   and "10 = Suc 9"
 
       
    22   and "11 = Suc 10"
 
       
    23   and "12 = Suc 11"
 
    22 by simp_all
 
    24 by simp_all
 
    23 
    25 
    24 text {* The Copying TM, which duplicates its input. *}
 
    26 text {* The Copying TM, which duplicates its input. *}
 
    25 
    27 
    26 definition 
    28 definition 
   161   ultimately 
   163   ultimately 
   162   have "(step0 (s, l, r) tcopy_begin, s, l, r) \<in> measure_begin"
 
   164   have "(step0 (s, l, r) tcopy_begin, s, l, r) \<in> measure_begin"
 
   163     apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
 
   165     apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
 
   164     apply(subgoal_tac "r = [Oc]")
 
   166     apply(subgoal_tac "r = [Oc]")
 
   165     apply(auto)
 
   167     apply(auto)
 
   166     by (metis cell.exhaust list.exhaust tl.simps(2))
 
   168     by (metis cell.exhaust list.exhaust list.sel(3))
 
   167   then 
   169   then 
   168   show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"
 
   170   show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"
 
   169     using eq by (simp only: step_red)
 
   171     using eq by (simp only: step_red)
 
   170 qed
 
   172 qed
 
   171 
   173 
   594   show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) \<in> measure_loop"
 
   596   show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) \<in> measure_loop"
 
   595     using eq by (simp only: step_red)
 
   597     using eq by (simp only: step_red)
 
   596 qed
 
   598 qed
 
   597 
   599 
   598 lemma loop_correct:
 
   600 lemma loop_correct:
 
   599   shows "0 < n \<Longrightarrow> {inv_loop1 n} tcopy_loop {inv_loop0 n}"
 
   601   assumes "0 < n"
 
       
   602   shows "{inv_loop1 n} tcopy_loop {inv_loop0 n}"
 
   600   using assms
 
   603   using assms
 
   601 proof(rule_tac Hoare_haltI)
 
   604 proof(rule_tac Hoare_haltI)
 
   602   fix l r
 
   605   fix l r
 
   603   assume h: "0 < n" "inv_loop1 n (l, r)"
 
   606   assume h: "0 < n" "inv_loop1 n (l, r)"
 
   604   then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)" 
   607   then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)" 
   916     unfolding tcopy_def
 
   919     unfolding tcopy_def
 
   917     by (rule_tac Hoare_plus_halt) (auto)
 
   920     by (rule_tac Hoare_plus_halt) (auto)
 
   918 qed
 
   921 qed
 
   919 
   922 
   920 abbreviation (input)
 
   923 abbreviation (input)
 
   921   "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <(n::nat)>)"
 
   924   "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, Oc \<up> (Suc n))"
 
   922 abbreviation (input)
 
   925 abbreviation (input)
 
   923   "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"
 
   926   "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"
 
   924 
   927 
   925 lemma tcopy_correct:
 
   928 lemma tcopy_correct:
 
   926   shows "{pre_tcopy n} tcopy {post_tcopy n}"
 
   929   shows "{pre_tcopy n} tcopy {post_tcopy n}"
 
   927 proof -
 
   930 proof -
 
   928   have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 
   931   have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 
   929     by (rule tcopy_correct1) (simp)
 
   932     by (rule tcopy_correct1) (simp)
 
   930   moreover
 
   933   moreover
 
   931   have "pre_tcopy n = inv_begin1 (Suc n)" 
   934   have "pre_tcopy n = inv_begin1 (Suc n)"
 
   932     by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
 
   935     by (auto)
 
   933   moreover
 
   936   moreover
 
   934   have "inv_end0 (Suc n) = post_tcopy n" 
   937   have "inv_end0 (Suc n) = post_tcopy n"
 
   935     by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair)
 
   938     unfolding fun_eq_iff
 
       
   939     by (auto simp add: inv_end0.simps tape_of_nat_def tape_of_prod_def)
 
   936   ultimately
 
   940   ultimately
 
   937   show "{pre_tcopy n} tcopy {post_tcopy n}" 
   941   show "{pre_tcopy n} tcopy {post_tcopy n}" 
   938     by simp
 
   942     by simp
 
   939 qed
 
   943 qed
 
   940 
   944 
   959 
   963 
   960 lemma dither_loops_aux: 
   964 lemma dither_loops_aux: 
   961   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
   965   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
   962    (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
 
   966    (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
 
   963   apply(induct stp)
 
   967   apply(induct stp)
 
   964   apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)
 
   968   apply(auto simp: steps.simps step.simps dither_def numeral)
 
   965   done
 
   969   done
 
   966 
   970 
   967 lemma dither_loops:
 
   971 lemma dither_loops:
 
   968   shows "{dither_unhalt_inv} dither \<up>" 
   972   shows "{dither_unhalt_inv} dither \<up>" 
   969 apply(rule Hoare_unhaltI)
 
   973 apply(rule Hoare_unhaltI)
 
   970 using dither_loops_aux
 
   974 using dither_loops_aux
 
   971 apply(auto simp add: numeral tape_of_nat_abv)
 
   975 apply(auto simp add: numeral tape_of_nat_def)
 
   972 by (metis Suc_neq_Zero is_final_eq)
 
   976 by (metis Suc_neq_Zero is_final_eq)
 
   973 
   977 
   974 lemma dither_halts_aux: 
   978 lemma dither_halts_aux: 
   975   shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
 
   979   shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
 
   976 unfolding dither_def
 
   980 unfolding dither_def
 
   978 
   982 
   979 lemma dither_halts:
 
   983 lemma dither_halts:
 
   980   shows "{dither_halt_inv} dither {dither_halt_inv}" 
   984   shows "{dither_halt_inv} dither {dither_halt_inv}" 
   981 apply(rule Hoare_haltI)
 
   985 apply(rule Hoare_haltI)
 
   982 using dither_halts_aux
 
   986 using dither_halts_aux
 
   983 apply(auto simp add: tape_of_nat_abv)
 
   987 apply(auto simp add: tape_of_nat_def)
 
   984 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
   988 by (metis (lifting, mono_tags) holds_for.simps is_final_eq)
 
   985 
   989 
   986 
   990 
   987 section {* The diagnal argument below shows the undecidability of Halting problem *}
 
   991 section {* The diagnal argument below shows the undecidability of Halting problem *}
 
   988 
   992 
   989 text {*
 
   993 text {*
 
  1007   under this locale. Therefore, the undecidability of {\em Halting Problem}
 
  1011   under this locale. Therefore, the undecidability of {\em Halting Problem}
 
  1008   is established. 
  1012   is established. 
  1009 *}
 
  1013 *}
 
  1010 
  1014 
  1011 locale uncomputable = 
  1015 locale uncomputable = 
  1012   -- {* The coding function of TM, interestingly, the detailed definition of this 
  1016   (* The coding function of TM, interestingly, the detailed definition of this 
  1013   funciton @{text "code"} does not affect the final result. *}
 
  1017   funciton @{text "code"} does not affect the final result. *)
 
  1014   fixes code :: "instr list \<Rightarrow> nat" 
  1018   fixes code :: "instr list \<Rightarrow> nat" 
  1015   -- {* 
  1019   (* 
  1016   The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
 
  1020   The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
 
  1017   *}
 
  1021   *)
 
  1018   and H :: "instr list"
 
  1022   and H :: "instr list"
 
  1019   assumes h_wf[intro]: "tm_wf0 H"
 
  1023   assumes h_wf[intro]: "tm_wf0 H"
 
  1020   -- {*
 
  1024   (*
 
  1021   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 
  1025   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 
  1022   *}
 
  1026   *)
 
  1023   and h_case: 
  1027   and h_case: 
  1024   "\<And> M ns. halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
 
  1028   "\<And> M ns. halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
 
  1025   and nh_case: 
  1029   and nh_case: 
  1026   "\<And> M ns. \<not> halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
 
  1030   "\<And> M ns. \<not> halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
 
  1027 begin
 
  1031 begin
 
  1058 lemma tcontra_unhalt: 
  1062 lemma tcontra_unhalt: 
  1059   assumes "\<not> halts tcontra [code tcontra]"
 
  1063   assumes "\<not> halts tcontra [code tcontra]"
 
  1060   shows "False"
 
  1064   shows "False"
 
  1061 proof -
 
  1065 proof -
 
  1062   (* invariants *)
 
  1066   (* invariants *)
 
  1063   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
 
  1067   define P1 where "P1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
 
  1064   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
 
  1068   define P2 where "P2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
 
  1065   def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 
  1069   define P3 where "P3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 
  1066 
  1070 
  1067   (*
 
  1071   (*
 
  1068   {P1} tcopy {P2}  {P2} H {P3} 
  1072   {P1} tcopy {P2}  {P2} H {P3} 
  1069   ----------------------------
 
  1073   ----------------------------
 
  1070      {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
 
  1074      {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
 
  1076 
  1080 
  1077   (* {P1} (tcopy |+| H) {P3} *)
 
  1081   (* {P1} (tcopy |+| H) {P3} *)
 
  1078   have first: "{P1} (tcopy |+| H) {P3}" 
  1082   have first: "{P1} (tcopy |+| H) {P3}" 
  1079   proof (cases rule: Hoare_plus_halt)
 
  1083   proof (cases rule: Hoare_plus_halt)
 
  1080     case A_halt (* of tcopy *)
 
  1084     case A_halt (* of tcopy *)
 
  1081     show "{P1} tcopy {P2}" unfolding P1_def P2_def 
  1085     show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
 
  1082       by (rule tcopy_correct)
 
  1086       by (rule tcopy_correct)
 
  1083   next
 
  1087   next
 
  1084     case B_halt (* of H *)
 
  1088     case B_halt (* of H *)
 
  1085     show "{P2} H {P3}"
 
  1089     show "{P2} H {P3}"
 
  1086       unfolding P2_def P3_def 
  1090       unfolding P2_def P3_def 
  1087       using H_halt_inv[OF assms]
 
  1091       using H_halt_inv[OF assms]
 
  1088       by (simp add: tape_of_nat_pair tape_of_nl_abv)
 
  1092       by (simp add: tape_of_prod_def tape_of_list_def)
 
  1089   qed (simp)
 
  1093   qed (simp)
 
  1090 
  1094 
  1091   (* {P3} dither {P3} *)
 
  1095   (* {P3} dither {P3} *)
 
  1092   have second: "{P3} dither {P3}" unfolding P3_def 
  1096   have second: "{P3} dither {P3}" unfolding P3_def 
  1093     by (rule dither_halts)
 
  1097     by (rule dither_halts)
 
  1102     unfolding halts_def
 
  1106     unfolding halts_def
 
  1103     unfolding Hoare_halt_def 
  1107     unfolding Hoare_halt_def 
  1104     apply(auto)    
  1108     apply(auto)    
  1105     apply(drule_tac x = n in spec)
 
  1109     apply(drule_tac x = n in spec)
 
  1106     apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
 
  1110     apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
 
  1107     apply(auto simp add: tape_of_nl_abv)
 
  1111     apply(auto simp add: tape_of_list_def)
 
  1108     by (metis append_Nil2 replicate_0)
 
  1112     by (metis append_Nil2 replicate_0)
 
  1109 qed
 
  1113 qed
 
  1110 
  1114 
  1111 (* asumme tcontra halts on its code *)
 
  1115 (* asumme tcontra halts on its code *)
 
  1112 lemma tcontra_halt: 
  1116 lemma tcontra_halt: 
  1113   assumes "halts tcontra [code tcontra]"
 
  1117   assumes "halts tcontra [code tcontra]"
 
  1114   shows "False"
 
  1118   shows "False"
 
  1115 proof - 
  1119 proof - 
  1116   (* invariants *)
 
  1120   (* invariants *)
 
  1117   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
 
  1121   define P1 where "P1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
 
  1118   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
 
  1122   define P2 where "P2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
 
  1119   def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 
  1123   define Q3 where "Q3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 
  1120 
  1124 
  1121   (*
 
  1125   (*
 
  1122   {P1} tcopy {P2}  {P2} H {Q3} 
  1126   {P1} tcopy {P2}  {P2} H {Q3} 
  1123   ----------------------------
 
  1127   ----------------------------
 
  1124      {P1} (tcopy |+| H) {Q3}     {Q3} dither loops
 
  1128      {P1} (tcopy |+| H) {Q3}     {Q3} dither loops
 
  1130 
  1134 
  1131   (* {P1} (tcopy |+| H) {Q3} *)
 
  1135   (* {P1} (tcopy |+| H) {Q3} *)
 
  1132   have first: "{P1} (tcopy |+| H) {Q3}" 
  1136   have first: "{P1} (tcopy |+| H) {Q3}" 
  1133   proof (cases rule: Hoare_plus_halt)
 
  1137   proof (cases rule: Hoare_plus_halt)
 
  1134     case A_halt (* of tcopy *)
 
  1138     case A_halt (* of tcopy *)
 
  1135     show "{P1} tcopy {P2}" unfolding P1_def P2_def
 
  1139     show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
 
  1136       by (rule tcopy_correct)
 
  1140       by (rule tcopy_correct)
 
  1137   next
 
  1141   next
 
  1138     case B_halt (* of H *)
 
  1142     case B_halt (* of H *)
 
  1139     then show "{P2} H {Q3}"
 
  1143     then show "{P2} H {Q3}"
 
  1140       unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
 
  1144       unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
 
  1141       by(simp add: tape_of_nat_pair tape_of_nl_abv)
 
  1145       by(simp add: tape_of_prod_def tape_of_list_def)
 
  1142   qed (simp)
 
  1146   qed (simp)
 
  1143 
  1147 
  1144   (* {P3} dither loops *)
 
  1148   (* {P3} dither loops *)
 
  1145   have second: "{Q3} dither \<up>" unfolding Q3_def 
  1149   have second: "{Q3} dither \<up>" unfolding Q3_def 
  1146     by (rule dither_loops)
 
  1150     by (rule dither_loops)
 
  1152 
  1156 
  1153   with assms show "False"
 
  1157   with assms show "False"
 
  1154     unfolding P1_def
 
  1158     unfolding P1_def
 
  1155     unfolding halts_def
 
  1159     unfolding halts_def
 
  1156     unfolding Hoare_halt_def Hoare_unhalt_def
 
  1160     unfolding Hoare_halt_def Hoare_unhalt_def
 
  1157     by (auto simp add: tape_of_nl_abv)
 
  1161     by (auto simp add: tape_of_list_def)
 
  1158 qed
 
  1162 qed
 
  1159 
  1163 
  1160       
  1164       
  1161 text {*
 
  1165 text {*
 
  1162   @{text "False"} can finally derived.
 
  1166   @{text "False"} can finally derived.
tm