--- a/thys/uncomputable.thy Fri Jan 25 22:12:01 2013 +0000
+++ b/thys/uncomputable.thy Sat Jan 26 01:36:48 2013 +0000
@@ -204,16 +204,16 @@
inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "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)"
-| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+ "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)"
+| "inv_loop1_exit x (l, r) = ((l, r) = ([], Bk#Oc#Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
| "inv_loop5_loop x (l, r) =
- (\<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)"
+ (\<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))"
| "inv_loop5_exit x (l, r) =
- (\<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)"
+ (\<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))"
| "inv_loop6_loop x (l, r) =
- (\<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)"
+ (\<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))"
| "inv_loop6_exit x (l, r) =
- (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
+ (\<exists> i j. i + j = x \<and> j > 0 \<and> (l, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"
fun
inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
@@ -224,13 +224,13 @@
inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_loop0 x (l, r) = (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
+ "inv_loop0 x (l, r) = ((l, r) = ([Bk], Oc # Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
-| "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)"
+| "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))"
| "inv_loop3 x (l, r) =
- (\<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)"
+ (\<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))"
| "inv_loop4 x (l, r) =
- (\<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)"
+ (\<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))"
| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
| "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
@@ -1026,7 +1026,7 @@
definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
where
- "haltP p lm \<equiv> \<exists>n a b c. steps (1, [], <lm>) p n = (0, Bk \<up> a, Oc \<up> b @ Bk \<up> c)"
+ "haltP p lm \<equiv> \<exists>n a m. steps (1, [], <lm>) p n = (0, Bk \<up> a, <m::nat>)"
abbreviation
"haltP0 p lm \<equiv> haltP (p, 0) lm"
@@ -1057,9 +1057,9 @@
The following two assumptions specifies that @{text "H"} does solve the Halting problem.
*}
and h_case:
- "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
+ "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc]))"
and nh_case:
- "\<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]))"
+ "\<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]))"
begin
(* invariants for H *)
@@ -1079,7 +1079,7 @@
proof -
obtain stp i
where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
- using nh_case[of "M" "[n]", OF assms] by auto
+ using nh_case assms by blast
then show "{pre_H_inv M n} H {post_H_halt_inv}"
unfolding Hoare_halt_def
apply(auto)
@@ -1094,7 +1094,7 @@
proof -
obtain stp i
where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
- using h_case[of "M" "[n]", OF assms] by auto
+ using h_case assms by blast
then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
unfolding Hoare_halt_def
apply(auto)
@@ -1156,11 +1156,11 @@
unfolding haltP_def
unfolding Hoare_halt_def
apply(auto)
- apply(erule_tac x = n in allE)
+ apply(drule_tac x = n in spec)
apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
- apply(simp, auto)
- apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
- apply(simp add: numeral)
+ apply(auto)
+ apply(drule_tac x = 1 in spec)
+ apply(simp add: numeral tape_of_nat_abv)
done
qed