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 84 4c8325c64dab
parent 83 8dc659af1bd2
child 89 c67e8ed4c865
equal deleted inserted replaced
83:8dc659af1bd2 84:4c8325c64dab 
   202   inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   202   inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   203   inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   203   inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   204   inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   204   inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   205   inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   205   inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   206 where
 
   206 where
 
   207   "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
 
   207   "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"
 
   208 | "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
 
   208 | "inv_loop1_exit x (l, r) = ((l, r) = ([], Bk#Oc#Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
 
   209 | "inv_loop5_loop x (l, r) = 
   209 | "inv_loop5_loop x (l, r) = 
   210      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
 
   210      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> (l, r) = (Oc\<up>k@Bk\<up>j@Oc\<up>i, Oc\<up>t))"
 
   211 | "inv_loop5_exit x (l, r) = 
   211 | "inv_loop5_exit x (l, r) = 
   212      (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
 
   212      (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Bk\<up>(j - 1)@Oc\<up>i, Bk # Oc\<up>j))"
 
   213 | "inv_loop6_loop x (l, r) = 
   213 | "inv_loop6_loop x (l, r) = 
   214      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
 
   214      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> (l, r) = (Bk\<up>k @ Oc\<up>i, Bk\<up>(Suc t) @ Oc\<up>j))"
 
   215 | "inv_loop6_exit x (l, r) = 
   215 | "inv_loop6_exit x (l, r) = 
   216      (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
 
   216      (\<exists> i j. i + j = x \<and> j > 0 \<and> (l, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"
 
   217 
   217 
   218 fun 
   218 fun 
   219   inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   219   inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   220   inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   220   inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   221   inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   221   inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   222   inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   222   inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   223   inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   223   inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   224   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   224   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   225   inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   225   inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   226 where
 
   226 where
 
   227   "inv_loop0 x (l, r) =  (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
 
   227   "inv_loop0 x (l, r) =  ((l, r) = ([Bk], Oc # Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
 
   228 | "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
 
   228 | "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
 
   229 | "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
 
   229 | "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"
 
   230 | "inv_loop3 x (l, r) = 
   230 | "inv_loop3 x (l, r) = 
   231      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
 
   231      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> (l, r) = (Bk\<up>k@Oc\<up>i, Bk\<up>t@Oc\<up>j))"
 
   232 | "inv_loop4 x (l, r) = 
   232 | "inv_loop4 x (l, r) = 
   233      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
 
   233      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> (l, r) = (Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i, Oc\<up>t))"
 
   234 | "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 
   234 | "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 
   235 | "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
   235 | "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
   236 
   236 
   237 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
   237 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
   238   where
 
   238   where
 
  1024   and the final configuration is standard.
 
  1024   and the final configuration is standard.
 
  1025 *}
 
  1025 *}
 
  1026 
  1026 
  1027 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
 
  1027 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
 
  1028   where
 
  1028   where
 
  1029   "haltP p lm \<equiv> \<exists>n a b c. steps (1, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
 
  1029   "haltP p lm \<equiv> \<exists>n a m. steps (1, [], <lm>) p n = (0, Bk \<up> a,  <m::nat>)"
 
  1030 
  1030 
  1031 abbreviation
 
  1031 abbreviation
 
  1032   "haltP0 p lm \<equiv> haltP (p, 0) lm" 
  1032   "haltP0 p lm \<equiv> haltP (p, 0) lm" 
  1033 
  1033 
  1034 lemma [intro, simp]: "tm_wf0 tcopy"
 
  1034 lemma [intro, simp]: "tm_wf0 tcopy"
 
  1055   assumes h_wf[intro]: "tm_wf0 H"
 
  1055   assumes h_wf[intro]: "tm_wf0 H"
 
  1056   -- {*
 
  1056   -- {*
 
  1057   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 
  1057   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 
  1058   *}
 
  1058   *}
 
  1059   and h_case: 
  1059   and h_case: 
  1060   "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
 
  1060   "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc]))"
 
  1061   and nh_case: 
  1061   and nh_case: 
  1062   "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
 
  1062   "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc, Oc]))"
 
  1063 begin
 
  1063 begin
 
  1064 
  1064 
  1065 (* invariants for H *)
 
  1065 (* invariants for H *)
 
  1066 abbreviation
 
  1066 abbreviation
 
  1067   "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
 
  1067   "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
 
  1077   assumes "\<not> haltP0 M [n]" 
  1077   assumes "\<not> haltP0 M [n]" 
  1078   shows "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1078   shows "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1079 proof -
 
  1079 proof -
 
  1080   obtain stp i
 
  1080   obtain stp i
 
  1081     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
 
  1081     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
 
  1082     using nh_case[of "M" "[n]", OF assms] by auto
 
  1082     using nh_case assms by blast
 
  1083   then show "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1083   then show "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1084     unfolding Hoare_halt_def
 
  1084     unfolding Hoare_halt_def
 
  1085     apply(auto)
 
  1085     apply(auto)
 
  1086     apply(rule_tac x = stp in exI)
 
  1086     apply(rule_tac x = stp in exI)
 
  1087     apply(auto)
 
  1087     apply(auto)
 
  1092   assumes "haltP0 M [n]" 
  1092   assumes "haltP0 M [n]" 
  1093   shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1093   shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1094 proof -
 
  1094 proof -
 
  1095   obtain stp i
 
  1095   obtain stp i
 
  1096     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
 
  1096     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
 
  1097     using h_case[of "M" "[n]", OF assms] by auto 
  1097     using h_case assms by blast
 
  1098   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1098   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1099     unfolding Hoare_halt_def
 
  1099     unfolding Hoare_halt_def
 
  1100     apply(auto)
 
  1100     apply(auto)
 
  1101     apply(rule_tac x = stp in exI)
 
  1101     apply(rule_tac x = stp in exI)
 
  1102     apply(auto)
 
  1102     apply(auto)
 
  1154   with assms show "False"
 
  1154   with assms show "False"
 
  1155     unfolding P1_def P3_def
 
  1155     unfolding P1_def P3_def
 
  1156     unfolding haltP_def
 
  1156     unfolding haltP_def
 
  1157     unfolding Hoare_halt_def 
  1157     unfolding Hoare_halt_def 
  1158     apply(auto)
 
  1158     apply(auto)
 
  1159     apply(erule_tac x = n in allE)
 
  1159     apply(drule_tac x = n in spec)
 
  1160     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
 
  1160     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
 
  1161     apply(simp, auto)
 
  1161     apply(auto)
 
  1162     apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
 
  1162     apply(drule_tac x = 1 in spec)
 
  1163     apply(simp add: numeral)
 
  1163     apply(simp add: numeral tape_of_nat_abv)
 
  1164     done
 
  1164     done
 
  1165 qed
 
  1165 qed
 
  1166 
  1166 
  1167 (* asumme tcontra halts on its code *)
 
  1167 (* asumme tcontra halts on its code *)
 
  1168 lemma tcontra_halt: 
  1168 lemma tcontra_halt:
tm