(* Title: Turing machine's definition and its charater
Author: XuJian <xujian817@hotmail.com>
Maintainer: Xujian
*)
header {* Undeciablity of the {\em Halting problem} *}
theory uncomputable
imports Main turing_hoare
begin
declare tm_comp.simps [simp del]
declare adjust.simps[simp del]
declare shift.simps[simp del]
declare tm_wf.simps[simp del]
declare step.simps[simp del]
declare steps.simps[simp del]
lemma numeral:
shows "1 = Suc 0"
and "2 = Suc 1"
and "3 = Suc 2"
and "4 = Suc 3"
and "5 = Suc 4"
and "6 = Suc 5" by arith+
text {*
The {\em Copying} TM, which duplicates its input.
*}
definition
tcopy_init :: "instr list"
where
"tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
(W1, 3), (L, 4), (L, 4), (L, 0)]"
definition
tcopy_loop :: "instr list"
where
"tcopy_loop \<equiv> [(R, 0), (R, 2), (R, 3), (W0, 2),
(R, 3), (R, 4), (W1, 5), (R, 4),
(L, 6), (L, 5), (L, 6), (L, 1)]"
definition
tcopy_end :: "instr list"
where
"tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),
(R, 2), (R, 2), (L, 5), (W0, 4),
(R, 0), (L, 5)]"
definition
tcopy :: "instr list"
where
"tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end"
(* tcopy_init *)
fun
inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>
(n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
| "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
| "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
| "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
| "inv_init4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"
fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
"inv_init n (s, l, r) =
(if s = 0 then inv_init0 n (l, r) else
if s = 1 then inv_init1 n (l, r) else
if s = 2 then inv_init2 n (l, r) else
if s = 3 then inv_init3 n (l, r) else
if s = 4 then inv_init4 n (l, r)
else False)"
lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
\<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
apply(rule_tac x = "Suc i" in exI, simp)
done
lemma inv_init_step:
"\<lbrakk>inv_init x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
unfolding tcopy_init_def
apply(case_tac cf)
apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral split: if_splits)
apply(case_tac "hd c", auto simp: inv_init.simps)
apply(case_tac c, simp_all)
done
lemma inv_init_steps:
"\<lbrakk>inv_init x (s, l, r); x > 0\<rbrakk>
\<Longrightarrow> inv_init x (steps (s, l, r) (tcopy_init, 0) stp)"
apply(induct stp, simp add: steps.simps)
apply(auto simp: step_red)
apply(rule_tac inv_init_step, simp_all)
done
fun init_state :: "config \<Rightarrow> nat"
where
"init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
fun init_step :: "config \<Rightarrow> nat"
where
"init_step (s, l, r) =
(if s = 2 then length r else
if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
if s = 4 then length l
else 0)"
fun init_measure :: "config \<Rightarrow> nat \<times> nat"
where
"init_measure c = (init_state c, init_step c)"
definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
where
"lex_pair \<equiv> less_than <*lex*> less_than"
definition init_LE :: "(config \<times> config) set"
where
"init_LE \<equiv> (inv_image lex_pair init_measure)"
lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
by (case_tac r, auto, case_tac a, auto)
lemma wf_init_le: "wf init_LE"
by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
lemma init_halt:
"x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
proof(rule_tac LE = init_LE in halt_lemma)
show "wf init_LE" by(simp add: wf_init_le)
next
assume h: "0 < x"
show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<longrightarrow>
(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n),
steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
proof(rule_tac allI, rule_tac impI)
fix n
assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
have b: "inv_init x (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
apply(rule_tac inv_init_steps)
apply(simp_all add: inv_init.simps h)
done
obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) = (s, l, r)"
apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n", auto)
done
moreover hence "inv_init x (s, l, r)"
using c b by simp
ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n),
steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
using a
proof(simp del: inv_init.simps)
assume "inv_init x (s, l, r)" "0 < s"
thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
qed
qed
lemma init_correct:
"x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
proof(rule_tac Hoare_haltI)
fix l r
assume h: "0 < x"
"inv_init1 x (l, r)"
hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
by(erule_tac init_halt)
then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)" ..
moreover have "inv_init x (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
apply(rule_tac inv_init_steps)
using h by(simp_all add: inv_init.simps)
ultimately show
"\<exists>n. is_final (steps (1, l, r) (tcopy_init, 0) n) \<and>
inv_init0 x holds_for steps (1, l, r) (tcopy_init, 0) n"
using h
apply(rule_tac x = stp in exI)
apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) stp)", simp add: inv_init.simps)
done
qed
(* tcopy_loop *)
fun
inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop5 :: "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_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 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_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)"
| "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)"
| "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)"
| "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)"
| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
"inv_loop x (s, l, r) =
(if s = 0 then inv_loop0 x (l, r)
else if s = 1 then inv_loop1 x (l, r)
else if s = 2 then inv_loop2 x (l, r)
else if s = 3 then inv_loop3 x (l, r)
else if s = 4 then inv_loop4 x (l, r)
else if s = 5 then inv_loop5 x (l, r)
else if s = 6 then inv_loop6 x (l, r)
else False)"
declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
inv_loop2.simps[simp del] inv_loop3.simps[simp del]
inv_loop4.simps[simp del] inv_loop5.simps[simp del]
inv_loop6.simps[simp del]
lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
by (case_tac t, auto)
lemma [simp]: "inv_loop1 x (b, []) = False"
by(simp add: inv_loop1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop2.simps inv_loop3.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop3.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
apply(rule_tac [!] x = i in exI,
rule_tac [!] x = "Suc j" in exI, simp_all)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
done
lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
apply(auto simp: inv_loop6.simps)
done
thm inv_loop6_exit.simps
lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR"
apply(auto simp: inv_loop6.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
apply(auto simp: inv_loop1.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
apply(auto simp: inv_loop1.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop2.simps inv_loop3.simps)
apply(rule_tac [!] x = i in exI, rule_tac [!] x = j in exI, simp_all)
done
lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
apply(case_tac j, simp_all)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop3.simps)
apply(rule_tac [!] x = i in exI,
rule_tac [!] x = j in exI, simp_all)
apply(case_tac [!] t, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
apply(auto simp: inv_loop6.simps inv_loop5.simps)
done
lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
apply(auto simp: inv_loop5_loop.simps)
done
lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
apply(auto simp: inv_loop6.simps)
done
declare inv_loop5_loop.simps[simp del] inv_loop5_exit.simps[simp del]
inv_loop6_loop.simps[simp del] inv_loop6_exit.simps[simp del]
lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
apply(erule_tac exE)+
apply(rule_tac x = i in exI,
rule_tac x = j in exI,
rule_tac x = "j - Suc (Suc 0)" in exI,
rule_tac x = "Suc 0" in exI, auto)
apply(case_tac [!] j, simp_all)
apply(case_tac [!] nat, simp_all)
done
lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
apply(auto simp: inv_loop6_loop.simps)
done
lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_loop6_exit x (tl b, Oc # Bk # list)"
apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
apply(erule_tac exE)+
apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
apply(case_tac j, auto)
apply(case_tac [!] nat, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
apply(simp add: inv_loop5.simps inv_loop6.simps)
apply(case_tac "hd b", simp_all, auto)
done
lemma [simp]: "inv_loop6 x ([], Bk # xs) = False"
apply(simp add: inv_loop6.simps inv_loop6_loop.simps
inv_loop6_exit.simps)
apply(auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
apply(simp)
done
lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
apply(simp add: inv_loop6_exit.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
apply(simp only: inv_loop6_loop.simps)
apply(erule_tac exE)+
apply(rule_tac x = i in exI, rule_tac x = j in exI,
rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
apply(case_tac [!] k, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk>
\<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
apply(erule_tac exE)+
apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
apply(case_tac [!] k, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
apply(simp add: inv_loop6.simps)
apply(case_tac "hd b", simp_all, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
apply(auto simp: inv_loop1.simps inv_loop2.simps)
apply(rule_tac x = "Suc i" in exI, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
apply(auto simp: inv_loop2.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop3.simps inv_loop4.simps)
apply(rule_tac [!] x = i in exI, auto)
apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
apply(case_tac [!] t, auto)
apply(case_tac [!] j, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop4.simps)
apply(rule_tac [!] x = "i" in exI, auto)
apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
apply(case_tac [!] t, simp_all)
done
lemma [simp]: "inv_loop5 x ([], list) = False"
apply(auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
done
lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
apply(auto simp: inv_loop5_exit.simps)
done
lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
apply(erule_tac exE)+
apply(rule_tac x = i in exI, auto)
apply(case_tac [!] k, auto)
done
lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk>
\<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
apply(simp only: inv_loop5_loop.simps)
apply(erule_tac exE)+
apply(rule_tac x = i in exI, rule_tac x = j in exI)
apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
apply(case_tac [!] k, auto)
done
lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_loop5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_loop5.simps)
apply(case_tac "hd b", simp_all, auto)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
inv_loop1 x ([], Bk # Oc # list)"
apply(auto simp: inv_loop6.simps inv_loop1.simps
inv_loop6_loop.simps inv_loop6_exit.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk>
\<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
apply(auto simp: inv_loop6.simps inv_loop1.simps
inv_loop6_loop.simps inv_loop6_exit.simps)
done
lemma inv_loop_step:
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
done
lemma inv_loop_steps:
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"
apply(induct stp, simp add: steps.simps, simp)
apply(erule_tac inv_loop_step, simp)
done
fun loop_stage :: "config \<Rightarrow> nat"
where
"loop_stage (s, l, r) = (if s = 0 then 0
else (Suc (length (takeWhile (\<lambda>a. a = Oc) (rev l @ r)))))"
fun loop_state :: "config \<Rightarrow> nat"
where
"loop_state (s, l, r) = (if s = 2 \<and> hd r = Oc then 0
else if s = 1 then 1
else 10 - s)"
fun loop_step :: "config \<Rightarrow> nat"
where
"loop_step (s, l, r) = (if s = 3 then length r
else if s = 4 then length r
else if s = 5 then length l
else if s = 6 then length l
else 0)"
definition lex_triple ::
"((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
where
"lex_triple \<equiv> less_than <*lex*> lex_pair"
lemma wf_lex_triple: "wf lex_triple"
by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
where
"loop_measure c =
(loop_stage c, loop_state c, loop_step c)"
definition loop_LE :: "(config \<times> config) set"
where
"loop_LE \<equiv> (inv_image lex_triple loop_measure)"
lemma wf_loop_le: "wf loop_LE"
by(auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
lemma [simp]: "inv_loop2 x ([], b) = False"
apply(auto simp: inv_loop2.simps)
done
lemma [simp]: "inv_loop2 x (l', []) = False"
apply(auto simp: inv_loop2.simps)
done
lemma [simp]: "inv_loop3 x (b, []) = False"
apply(auto simp: inv_loop3.simps)
done
lemma [simp]: "inv_loop4 x ([], b) = False"
apply(auto simp: inv_loop4.simps)
done
lemma [elim]:
"\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
apply(auto simp: inv_loop4.simps)
apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
done
lemma [elim]:
"\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
apply(auto simp: inv_loop4.simps)
done
lemma takeWhile_replicate_append:
"P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
apply(induct x, auto)
done
lemma takeWhile_replicate:
"P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
by(induct x, auto)
lemma [elim]:
"\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
apply(case_tac [!] j, simp_all)
apply(case_tac [!] "nat", simp_all)
apply(case_tac nata, simp_all add: List.takeWhile_tail)
apply(simp add: takeWhile_replicate_append takeWhile_replicate)
apply(case_tac nata, simp_all add: List.takeWhile_tail)
done
lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
apply(auto simp: inv_loop1.simps)
done
lemma [elim]:
"\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
apply(auto simp: inv_loop6.simps)
apply(case_tac l', simp_all)
done
lemma [elim]:
"\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
apply(auto simp: inv_loop2.simps)
apply(simp_all add: takeWhile_tail takeWhile_replicate_append
takeWhile_replicate)
done
lemma [elim]:
"\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
apply(auto simp: inv_loop5.simps)
apply(case_tac l', auto)
done
lemma[elim]:
"\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
\<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
apply(case_tac l')
apply(auto simp: inv_loop6.simps)
done
lemma loop_halt:
"\<lbrakk>x > 0; inv_loop x (Suc 0, l, r)\<rbrakk> \<Longrightarrow>
\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
proof(rule_tac LE = loop_LE in halt_lemma)
show "wf loop_LE" by(intro wf_loop_le)
next
assume h: "0 < x" and g: "inv_loop x (Suc 0, l, r)"
show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n) \<longrightarrow>
(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
proof(rule_tac allI, rule_tac impI)
fix n
assume a: "\<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n)"
obtain s' l' r' where d: "(steps (Suc 0, l, r) (tcopy_loop, 0) n) = (s', l', r')"
by(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) n)", auto)
hence "inv_loop x (s', l', r') \<and> s' \<noteq> 0"
using h g
apply(drule_tac stp = n in inv_loop_steps, auto)
using a
apply(simp)
done
hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE"
using h
apply(case_tac r', case_tac [2] a)
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def
numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits)
done
thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n),
steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
using d
apply(simp add: step_red)
done
qed
qed
lemma loop_correct:
"x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
proof(rule_tac Hoare_haltI)
fix l r
assume h: "0 < x"
"inv_loop1 x (l, r)"
hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
apply(rule_tac loop_halt, simp_all add: inv_loop.simps)
done
then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)" ..
moreover have "inv_loop x (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
apply(rule_tac inv_loop_steps)
using h by(simp_all add: inv_loop.simps)
ultimately show
"\<exists>n. is_final (steps (1, l, r) (tcopy_loop, 0) n) \<and>
inv_loop0 x holds_for steps (1, l, r) (tcopy_loop, 0) n"
using h
apply(rule_tac x = stp in exI)
apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)",
simp add: inv_init.simps inv_loop.simps)
done
qed
(* tcopy_end *)
fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end3 x (l, r) =
(\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )"
fun inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
fun inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end5_loop x (l, r) =
(\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
fun inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
fun inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
fun inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
fun inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
"inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
else if s = 1 then inv_end1 x (l, r)
else if s = 2 then inv_end2 x (l, r)
else if s = 3 then inv_end3 x (l, r)
else if s = 4 then inv_end4 x (l, r)
else if s = 5 then inv_end5 x (l, r)
else False)"
declare inv_end.simps[simp del] inv_end1.simps[simp del]
inv_end0.simps[simp del] inv_end2.simps[simp del]
inv_end3.simps[simp del] inv_end4.simps[simp del]
inv_end5.simps[simp del]
lemma [simp]: "inv_end1 x (b, []) = False"
apply(auto simp: inv_end1.simps)
done
lemma [simp]: "inv_end2 x (b, []) = False"
apply(auto simp: inv_end2.simps)
done
lemma [simp]: "inv_end3 x (b, []) = False"
apply(auto simp: inv_end3.simps)
done
thm inv_end4.simps
lemma [simp]: "inv_end4 x (b, []) = False"
apply(auto simp: inv_end4.simps)
done
lemma [simp]: "inv_end5 x (b, []) = False"
apply(auto simp: inv_end5.simps)
done
lemma [simp]: "inv_end1 x ([], list) = False"
apply(auto simp: inv_end1.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
\<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
apply(auto simp: inv_end1.simps inv_end0.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
\<Longrightarrow> inv_end3 x (b, Oc # list)"
apply(auto simp: inv_end2.simps inv_end3.simps)
apply(rule_tac x = "j - 1" in exI)
apply(case_tac j, simp_all)
apply(case_tac x, simp_all)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
apply(auto simp: inv_end2.simps inv_end3.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
inv_end5 x ([], Bk # Bk # list)"
apply(auto simp: inv_end4.simps inv_end5.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Bk # list)"
apply(auto simp: inv_end4.simps inv_end5.simps)
apply(rule_tac x = 1 in exI, simp)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
apply(auto simp: inv_end5.simps inv_end0.simps)
apply(case_tac [!] j, simp_all)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
apply(auto simp: inv_end1.simps inv_end2.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
inv_end4 x ([], Bk # Oc # list)"
apply(auto simp: inv_end2.simps inv_end4.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end4 x (tl b, hd b # Oc # list)"
apply(auto simp: inv_end2.simps inv_end4.simps)
apply(case_tac [!] j, simp_all)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
apply(auto simp: inv_end2.simps inv_end3.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
apply(auto simp: inv_end2.simps inv_end4.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
apply(auto simp: inv_end2.simps inv_end5.simps)
done
declare inv_end5_loop.simps[simp del]
inv_end5_exit.simps[simp del]
lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
apply(auto simp: inv_end5_exit.simps)
done
lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
apply(auto simp: inv_end5_loop.simps)
apply(case_tac [!] j, simp_all)
done
lemma [elim]:
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
inv_end5_exit x (tl b, Bk # Oc # list)"
apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
apply(case_tac [!] i, simp_all)
done
lemma [elim]:
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_end5_loop x (tl b, Oc # Oc # list)"
apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
apply(erule_tac exE)+
apply(rule_tac x = "i - 1" in exI,
rule_tac x = "Suc j" in exI, auto)
apply(case_tac [!] i, simp_all)
done
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_end2.simps inv_end5.simps)
apply(case_tac "hd b", simp_all, auto)
done
lemma inv_end_step:
"\<lbrakk>x > 0;
inv_end x cf\<rbrakk>
\<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
done
lemma inv_end_steps:
"\<lbrakk>x > 0; inv_end x cf\<rbrakk>
\<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
apply(induct stp, simp add:steps.simps, simp)
apply(erule_tac inv_end_step, simp)
done
fun end_state :: "config \<Rightarrow> nat"
where
"end_state (s, l, r) =
(if s = 0 then 0
else if s = 1 then 5
else if s = 2 \<or> s = 3 then 4
else if s = 4 then 3
else if s = 5 then 2
else 0)"
fun end_stage :: "config \<Rightarrow> nat"
where
"end_stage (s, l, r) =
(if s = 2 \<or> s = 3 then (length r)
else 0)"
fun end_step :: "config \<Rightarrow> nat"
where
"end_step (s, l, r) =
(if s = 4 then (if hd r = Oc then 1 else 0)
else if s = 5 then length l
else if s = 2 then 1
else if s = 3 then 0
else 0)"
fun end_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
where
"end_measure c =
(end_state c, end_stage c, end_step c)"
definition end_LE :: "(config \<times> config) set"
where
"end_LE \<equiv> (inv_image lex_triple end_measure)"
lemma wf_end_le: "wf end_LE"
by(auto intro:wf_inv_image simp: end_LE_def wf_lex_triple)
lemma [simp]: "inv_end5 x ([], Oc # list) = False"
apply(auto simp: inv_end5.simps inv_end5_loop.simps)
done
lemma end_halt:
"\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow>
\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
proof(rule_tac LE = end_LE in halt_lemma)
show "wf end_LE" by(intro wf_end_le)
next
assume great: "0 < x"
and inv_start: "inv_end x (Suc 0, l, r)"
show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n) \<longrightarrow>
(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
proof(rule_tac allI, rule_tac impI)
fix n
assume notfinal: "\<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"
obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"
apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)
done
hence "inv_end x (s', l', r') \<and> s' \<noteq> 0"
using great inv_start notfinal
apply(drule_tac stp = n in inv_end_steps, auto)
done
hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
apply(case_tac r', case_tac [2] a)
apply(auto simp: inv_end.simps step.simps tcopy_end_def
numeral end_LE_def lex_triple_def lex_pair_def split: if_splits)
done
thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n),
steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
using d
by simp
qed
qed
lemma end_correct:
"x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
proof(rule_tac Hoare_haltI)
fix l r
assume h: "0 < x"
"inv_end1 x (l, r)"
hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
apply(rule_tac end_halt, simp_all add: inv_end.simps)
done
then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)" ..
moreover have "inv_end x (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
apply(rule_tac inv_end_steps)
using h by(simp_all add: inv_end.simps)
ultimately show
"\<exists>n. is_final (steps (1, l, r) (tcopy_end, 0) n) \<and>
inv_end0 x holds_for steps (1, l, r) (tcopy_end, 0) n"
using h
apply(rule_tac x = stp in exI)
apply(case_tac "(steps (Suc 0, l, r) (tcopy_end, 0) stp)",
simp add: inv_end.simps)
done
qed
(* tcopy *)
lemma [intro]: "tm_wf (tcopy_init, 0)"
by(auto simp: tm_wf.simps tcopy_init_def)
lemma [intro]: "tm_wf (tcopy_loop, 0)"
by(auto simp: tm_wf.simps tcopy_loop_def)
lemma [intro]: "tm_wf (tcopy_end, 0)"
by(auto simp: tm_wf.simps tcopy_end_def)
lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
tm_comp.simps)
done
lemma tcopy_correct1:
"\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}"
proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
show "inv_loop0 x \<mapsto> inv_end1 x"
by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
next
show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto
next
assume "0 < x"
thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}"
proof(rule_tac Hoare_plus_halt)
show "inv_init0 x \<mapsto> inv_loop1 x"
apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def)
apply(rule_tac x = "Suc 0" in exI, auto)
done
next
show "tm_wf (tcopy_init, 0)" by auto
next
assume "0 < x"
thus "{inv_init1 x} tcopy_init {inv_init0 x}"
by(erule_tac init_correct)
next
assume "0 < x"
thus "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
by(erule_tac loop_correct)
qed
next
assume "0 < x"
thus "{inv_end1 x} tcopy_end {inv_end0 x}"
by(erule_tac end_correct)
qed
abbreviation
"pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[n::nat]>)"
abbreviation
"post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[n, n::nat]>)"
lemma tcopy_correct2:
shows "{pre_tcopy n} tcopy {post_tcopy n}"
proof -
have "{inv_init1 (Suc n)} tcopy {inv_end0 (Suc n)}"
by (rule tcopy_correct1) (simp)
moreover
have "pre_tcopy n \<mapsto> inv_init1 (Suc n)"
by (simp add: assert_imp_def tape_of_nl_abv)
moreover
have "inv_end0 (Suc n) \<mapsto> post_tcopy n"
by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
ultimately
show "{pre_tcopy n} tcopy {post_tcopy n}"
by (rule Hoare_weaken)
qed
section {* The {\em Dithering} Turing Machine *}
text {*
The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
terminate.
*}
definition dither :: "instr list"
where
"dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
(* invariants of dither *)
abbreviation
"dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
abbreviation
"dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
lemma dither_loops_aux:
"(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
(steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
apply(induct stp)
apply(auto simp: steps.simps step.simps dither_def numeral)
done
lemma dither_loops:
shows "{dither_unhalt_inv} dither \<up>"
apply(rule Hoare_unhaltI)
using dither_loops_aux
apply(auto simp add: numeral)
by (metis Suc_neq_Zero is_final_eq)
lemma dither_halts_aux:
shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])"
unfolding dither_def
by (simp add: steps.simps step.simps numeral)
lemma dither_halts:
shows "{dither_halt_inv} dither {dither_halt_inv}"
apply(rule Hoare_haltI)
using dither_halts_aux
apply(auto)
by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
section {* The diagnal argument below shows the undecidability of Halting problem *}
text {*
@{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
and the final configuration is standard.
*}
definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
where
"haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a, Oc \<up> b @ Bk \<up> c)"
abbreviation
"haltP0 p lm \<equiv> haltP (p, 0) lm"
lemma [intro, simp]: "tm_wf0 tcopy"
by(auto simp: tcopy_def)
lemma [intro, simp]: "tm_wf0 dither"
by (auto simp: tm_wf.simps dither_def)
text {*
The following lemma shows the meaning of @{text "tinres"} with respect to
one step execution.
*}
lemma tinres_step:
"\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra);
step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
\<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")
apply(auto simp: step.simps fetch.simps
split: if_splits )
apply(case_tac [!] "t ! (2 * nat)",
auto simp: tinres_def split: if_splits)
apply(case_tac [1-8] a, auto split: if_splits)
apply(case_tac [!] "t ! (2 * nat)",
auto simp: tinres_def split: if_splits)
apply(case_tac [1-4] a, auto split: if_splits)
apply(case_tac [!] "t ! Suc (2 * nat)",
auto simp: if_splits)
apply(case_tac [!] aa, auto split: if_splits)
done
text {*
The following lemma shows the meaning of @{text "tinres"} with respect to
many step execution.
*}
lemma tinres_steps:
"\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra);
steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk>
\<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)
apply(simp add: step_red)
apply(case_tac "(steps (ss, l, r) (t, 0) stp)")
apply(case_tac "(steps (ss, l', r) (t, 0) stp)")
proof -
fix stp sa la ra sb lb rb a b c aa ba ca
assume ind: "\<And>sa la ra sb lb rb. \<lbrakk>steps (ss, l, r) (t, 0) stp = (sa, (la::cell list), ra);
steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
and h: " tinres l l'" "step (steps (ss, l, r) (t, 0) stp) (t, 0) = (sa, la, ra)"
"step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)"
"steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"
have "tinres b ba \<and> c = ca \<and> a = aa"
apply(rule_tac ind, simp_all add: h)
done
thus "tinres la lb \<and> ra = rb \<and> sa = sb"
apply(rule_tac l = b and l' = ba and r = c and ss = a
and t = t in tinres_step)
using h
apply(simp, simp, simp)
done
qed
lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb"
apply(auto simp: tinres_def replicate_add[THEN sym])
apply(case_tac "nb > n")
apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
apply arith
by (metis Nil_is_append_conv add_diff_inverse append_assoc nat_add_commute replicate_0 replicate_add
self_append_conv2)
text {*
The following locale specifies that TM @{text "H"} can be used to solve
the {\em Halting Problem} and @{text "False"} is going to be derived
under this locale. Therefore, the undecidability of {\em Halting Problem}
is established.
*}
locale uncomputable =
-- {* The coding function of TM, interestingly, the detailed definition of this
funciton @{text "code"} does not affect the final result. *}
fixes code :: "instr list \<Rightarrow> nat"
-- {*
The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
*}
and H :: "instr list"
assumes h_wf[intro]: "tm_wf0 H"
-- {*
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, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
and nh_case:
"\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow>
\<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
begin
lemma h_newcase:
"\<And> M lm. haltP0 M lm \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk \<up> x , <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
proof -
fix M lm
assume "haltP (M, 0) lm"
hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))"
by (rule h_case)
from this obtain na nb where
cond1:"(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))" by blast
thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
fix a b c
assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
have "tinres (Bk\<up>nb) b \<and> [Oc] = c \<and> 0 = a"
proof(rule_tac tinres_steps)
show "tinres [] (Bk\<up>x)"
apply(simp add: tinres_def)
apply(auto)
done
next
show "(steps (1, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))"
by(simp add: cond1[simplified])
next
show "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
by(simp add: cond2[simplified])
qed
thus "a = 0 \<and> (\<exists>nb. b = (Bk\<up>nb)) \<and> c = [Oc]"
by(auto elim: tinres_ex1)
qed
qed
lemma nh_newcase:
"\<And> M lm. \<not> (haltP (M, 0) lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk\<up>x, <code M # lm>) H na = (0, Bk\<up>nb, [Oc, Oc]))"
proof -
fix M lm
assume "\<not> haltP (M, 0) lm"
hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
by (rule nh_case)
from this obtain na nb where
cond1: "(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))" by blast
thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
fix a b c
assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
have "tinres (Bk\<up>nb) b \<and> [Oc, Oc] = c \<and> 0 = a"
proof(rule_tac tinres_steps)
show "tinres [] (Bk\<up>x)"
apply(auto simp: tinres_def)
done
next
show "(steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
by(simp add: cond1[simplified])
next
show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
by(simp add: cond2[simplified])
qed
thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]"
by(auto elim: tinres_ex1)
qed
qed
(* invariants for H *)
abbreviation
"pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code M, n]>)"
abbreviation
"post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
abbreviation
"post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
lemma H_halt_inv:
assumes "\<not> haltP0 M [n]"
shows "{pre_H_inv M n} H {post_H_halt_inv}"
proof -
obtain stp i
where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
using nh_newcase[of "M" "[n]" "1", OF assms] by auto
then show "{pre_H_inv M n} H {post_H_halt_inv}"
unfolding Hoare_halt_def
apply(auto)
apply(rule_tac x = stp in exI)
apply(auto)
done
qed
lemma H_unhalt_inv:
assumes "haltP0 M [n]"
shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
proof -
obtain stp i
where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
using h_newcase[of "M" "[n]" "1", OF assms] by auto
then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
unfolding Hoare_halt_def
apply(auto)
apply(rule_tac x = stp in exI)
apply(auto)
done
qed
(* TM that produces the contradiction and its code *)
abbreviation
"tcontra \<equiv> (tcopy |+| H) |+| dither"
abbreviation
"code_tcontra \<equiv> code tcontra"
(* assume tcontra does not halt on its code *)
lemma tcontra_unhalt:
assumes "\<not> haltP0 tcontra [code tcontra]"
shows "False"
proof -
(* invariants *)
def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
(*
{P1} tcopy {P2} {P2} H {P3}
----------------------------
{P1} (tcopy |+| H) {P3} {P3} dither {P3}
------------------------------------------------
{P1} tcontra {P3}
*)
have H_wf: "tm_wf0 (tcopy |+| H)" by auto
(* {P1} (tcopy |+| H) {P3} *)
have first: "{P1} (tcopy |+| H) {P3}"
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
by (simp) (rule tcopy_correct2)
next
case B_halt (* of H *)
show "{P2} H {P3}"
unfolding P2_def P3_def
using assms by (simp) (rule H_halt_inv)
qed (simp)
(* {P3} dither {P3} *)
have second: "{P3} dither {P3}" unfolding P3_def
by (rule dither_halts)
(* {P1} tcontra {P3} *)
have "{P1} tcontra {P3}"
by (rule Hoare_plus_halt_simple[OF first second H_wf])
with assms show "False"
unfolding P1_def P3_def
unfolding haltP_def
unfolding Hoare_halt_def
apply(auto)
apply(erule_tac x = n in allE)
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)
done
qed
(* asumme tcontra halts on its code *)
lemma tcontra_halt:
assumes "haltP0 tcontra [code tcontra]"
shows "False"
proof -
(* invariants *)
def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
(*
{P1} tcopy {P2} {P2} H {P3}
----------------------------
{P1} (tcopy |+| H) {P3} {P3} dither loops
------------------------------------------------
{P1} tcontra loops
*)
have H_wf: "tm_wf0 (tcopy |+| H)" by auto
(* {P1} (tcopy |+| H) {P3} *)
have first: "{P1} (tcopy |+| H) {P3}"
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
by (simp) (rule tcopy_correct2)
next
case B_halt (* of H *)
then show "{P2} H {P3}"
unfolding P2_def P3_def
using assms by (simp) (rule H_unhalt_inv)
qed (simp)
(* {P3} dither loops *)
have second: "{P3} dither \<up>" unfolding P3_def
by (rule dither_loops)
(* {P1} tcontra loops *)
have "{P1} tcontra \<up>"
by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
with assms show "False"
unfolding P1_def
unfolding haltP_def
unfolding Hoare_unhalt_def
by (auto, metis is_final_eq)
qed
text {*
@{text "False"} can finally derived.
*}
lemma false: "False"
using tcontra_halt tcontra_unhalt
by auto
end
declare replicate_Suc[simp del]
end