(* 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_basic
begin
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)]"
fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_init1 x (l, r) = (l = [] \<and> r = Oc\<up>x )"
fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<up>i \<and> r = Oc\<up>j)"
fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<up>x \<and> tl r = [])"
fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc\<up>x \<and> r = [Bk, Oc]) \<or> (l = Oc\<up>(x - 1) \<and> r = [Oc, Bk, Oc])))"
fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_init0 x (l, r) = ((x > Suc 0 \<and> l = Oc\<up>(x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>
(x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
"inv_init x (s, l, r) = (
if s = 0 then inv_init0 x (l, r)
else if s = Suc 0 then inv_init1 x (l, r)
else if s = 2 then inv_init2 x (l, r)
else if s = 3 then inv_init3 x (l, r)
else if s = 4 then inv_init4 x (l, r)
else False)"
declare inv_init.simps[simp del]
lemma numeral_4_eq_4: "4 = Suc 3"
by arith
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))"
apply(case_tac cf)
apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2
numeral_3_eq_3 numeral_4_eq_4 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 Suc 0 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]"
apply(case_tac r, auto, case_tac a, auto)
done
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)
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: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2
numeral_3_eq_3 numeral_4_eq_4 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, 0) {inv_init0 x}"
proof(rule_tac HoareI)
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
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)]"
fun inv_loop1_loop :: "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)"
fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_loop1_exit x (l, r) =
(l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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)"
fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"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_loop0 :: "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 )"
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"
apply(case_tac t, auto)
done
lemma numeral_5_eq_5: "5 = Suc 4" by arith
lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith
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, [])"
apply(auto simp: inv_loop2.simps inv_loop3.simps)
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
apply(auto simp: inv_loop3.simps)
done
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_2_eq_2
numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 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_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
numeral_5_eq_5 numeral_6_eq_6 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, 0) {inv_loop0 x}"
proof(rule_tac HoareI)
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
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)]"
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_2_eq_2
numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 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_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
numeral_5_eq_5 numeral_6_eq_6 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, 0) {inv_end0 x}"
proof(rule_tac HoareI)
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
definition tcopy :: "instr list"
where
"tcopy = ((tcopy_init |+| tcopy_loop) |+| tcopy_end)"
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 length_comp
tm_comp.simps)
done
lemma tcopy_correct1:
"\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} (tcopy, 0) {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
show "tm_wf (tcopy_end, 0)" by auto
next
assume "0 < x"
thus "{inv_init1 x} (tcopy_init |+| tcopy_loop, 0) {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
show "tm_wf (tcopy_loop, 0)" by auto
next
assume "0 < x"
thus "{inv_init1 x} (tcopy_init, 0) {inv_init0 x}"
by(erule_tac init_correct)
next
assume "0 < x"
thus "{inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"
by(erule_tac loop_correct)
qed
next
assume "0 < x"
thus "{inv_end1 x} (tcopy_end, 0) {inv_end0 x}"
by(erule_tac end_correct)
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)] "
lemma dither_halt_rs:
"\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp =
(0, Bk\<up>m, [Oc, Oc])"
apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
apply(simp add: dither_def steps.simps
step.simps fetch.simps numeral_2_eq_2)
done
lemma dither_unhalt_state:
"(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp =
(Suc 0, Bk\<up>m, [Oc])) \<or>
(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
apply(induct stp, simp add: steps.simps)
apply(simp add: step_red, auto)
apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2)
done
lemma dither_unhalt_rs:
"\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)"
using dither_unhalt_state[of m stp]
apply(auto)
done
section {*
The final diagnal arguments to show 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 t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a, Oc\<up>b @ Bk\<up>c))"
lemma [intro]: "tm_wf (tcopy, 0)"
by(auto simp: tcopy_def)
lemma [intro]: "tm_wf (dither, 0)"
apply(auto simp: tm_wf.simps dither_def)
done
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 length_eq: "xs = ys \<Longrightarrow> length xs = length ys"
by auto
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 \<ge> n")
apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
apply arith
apply(drule_tac length_eq, simp)
done
lemma Hoare_weak:
"\<lbrakk>{P} (p, off) {Q}; P'\<mapsto>P; Q\<mapsto>Q'\<rbrakk> \<Longrightarrow> {P'} (p, off) {Q'}"
using Hoare_def
proof(auto simp: assert_imp_def)
fix l r
assume
ho1: "\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n)
\<and> Q holds_for steps (Suc 0, l, r) (p, off) n)"
and imp1: "\<forall>l r. P' (l, r) \<longrightarrow> P (l, r)"
and imp2: "\<forall>l r. Q (l, r) \<longrightarrow> Q' (l, r)"
and cond: "P' (l, r)"
and ho2: "\<And>P a b Q. {P} (a, b) {Q} \<equiv> \<forall>l r. P (l, r) \<longrightarrow>
(\<exists>n. is_final (steps (Suc 0, l, r) (a, b) n) \<and> Q holds_for steps (Suc 0, l, r) (a, b) n)"
have "P (l, r)"
using cond imp1 by auto
hence "(\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n)
\<and> Q holds_for steps (Suc 0, l, r) (p, off) n)"
using ho1 by auto
from this obtain n where "is_final (steps (Suc 0, l, r) (p, off) n)
\<and> Q holds_for steps (Suc 0, l, r) (p, off) n" ..
thus "\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) \<and>
Q' holds_for steps (Suc 0, l, r) (p, off) n"
apply(rule_tac x = n in exI, auto)
apply(case_tac "steps (Suc 0, l, r) (p, off) n", simp)
using imp2
by simp
qed
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_wf (H, 0)"
-- {*
The following two assumptions specifies that @{text "H"} does solve the Halting problem.
*}
and h_case:
"\<And> M n. \<lbrakk>(haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
and nh_case:
"\<And> M n. \<lbrakk>(\<not> haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
begin
lemma h_newcase:
"\<And> M n. haltP (M, 0) lm \<Longrightarrow>
\<exists> na nb. (steps (Suc 0, Bk\<up>x , <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
proof -
fix M n
assume "haltP (M, 0) lm"
hence "\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))"
apply(erule_tac h_case)
done
from this obtain na nb where
cond1:"(steps (Suc 0, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))" by blast
thus "\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
proof(rule_tac x = na in exI, case_tac "steps (Suc 0, 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 (Suc 0, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))"
by(simp add: cond1)
next
show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
by(simp add: cond2)
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 n. \<lbrakk>\<not> (haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
proof -
fix M n
assume "\<not> haltP (M, 0) lm"
hence "\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc, Oc]))"
apply(erule_tac nh_case)
done
from this obtain na nb where
cond1: "(steps (Suc 0, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc, Oc]))" by blast
thus "\<exists> na nb. (steps (Suc 0, 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 (Suc 0, 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)
next
show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
by(simp add: cond2)
qed
thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]"
by(auto elim: tinres_ex1)
qed
qed
(*
lemma haltP_weaking:
"haltP (tcontra H) (code (tcontra H)) \<Longrightarrow>
\<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>)
((tcopy |+| H) |+| dither) stp)"
apply(simp add: haltP_def, auto)
apply(rule_tac x = n in exI, simp add: isS0_def tcontra_def)
done
*)
definition tcontra :: "instr list \<Rightarrow> instr list"
where
"tcontra h \<equiv> ((tcopy |+| h) |+| dither)"
declare replicate_Suc[simp del]
lemma uh_h: "\<not> haltP (tcontra H, 0) [code (tcontra H)]
\<Longrightarrow> haltP (tcontra H, 0) [code (tcontra H)]"
proof(simp only: tcontra_def)
let ?tcontr = "(tcopy |+| H) |+| dither"
let ?cn = "Suc (code ?tcontr)"
let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))"
let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
let ?P3 = ?Q2
let ?Q3 = ?P3
assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]"
have "{?P1} (?tcontr, 0) {?Q3}"
proof(rule_tac Hoare_plus_halt, auto)
show "?Q2 \<mapsto> ?P3"
apply(simp add: assert_imp_def)
done
next
show "{?P1} (tcopy|+|H, 0) {?Q2}"
proof(rule_tac Hoare_plus_halt, auto)
show "?Q1 \<mapsto> ?P2"
apply(simp add: assert_imp_def)
done
next
show "{?P1} (tcopy, 0) {?Q1}"
proof -
have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}"
by(rule_tac tcopy_correct1, simp)
thus "?thesis"
proof(rule_tac Hoare_weak)
show "{inv_init1 ?cn} (tcopy, 0)
{inv_end0 ?cn} " using g by simp
next
show "?P1 \<mapsto> inv_init1 (?cn)"
apply(simp add: inv_init1.simps assert_imp_def)
done
next
show "inv_end0 ?cn \<mapsto> ?Q1"
apply(simp add: assert_imp_def inv_end0.simps)
done
qed
qed
next
show "{?P2} (H, 0) {?Q2}"
using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h
apply(auto)
apply(rule_tac x = na in exI)
apply(simp add: replicate_Suc tape_of_nl_abv)
done
qed
next
show "{?P3}(dither, 0){?Q3}"
using Hoare_def
proof(auto)
fix nd
show "\<exists>n. is_final (steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n) \<and>
(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])
holds_for steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n"
using dither_halt_rs[of nd]
apply(auto)
apply(rule_tac x = stp in exI, simp)
done
qed
qed
thus "False"
using h
apply(auto simp: haltP_def Hoare_def)
apply(erule_tac x = n in allE)
apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
apply(simp, auto)
apply(erule_tac x = nd in allE, erule_tac x = 2 in allE)
apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv)
apply(erule_tac x = 0 in allE, simp)
done
qed
lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)]
\<Longrightarrow> \<not> haltP (tcontra H, 0) [code (tcontra H)]"
proof(simp only: tcontra_def)
let ?tcontr = "(tcopy |+| H) |+| dither"
let ?cn = "Suc (code ?tcontr)"
let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))"
let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
let ?P3 = ?Q2
assume h: "haltP (?tcontr, 0) [code ?tcontr]"
have "{?P1} (?tcontr, 0)"
proof(rule_tac Hoare_plus_unhalt, auto)
show "?Q2 \<mapsto> ?P3"
apply(simp add: assert_imp_def)
done
next
show "{?P1} (tcopy|+|H, 0) {?Q2}"
proof(rule_tac Hoare_plus_halt, auto)
show "?Q1 \<mapsto> ?P2"
apply(simp add: assert_imp_def)
done
next
show "{?P1} (tcopy, 0) {?Q1}"
proof -
have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}"
by(rule_tac tcopy_correct1, simp)
thus "?thesis"
proof(rule_tac Hoare_weak)
show "{inv_init1 ?cn} (tcopy, 0)
{inv_end0 ?cn} " using g by simp
next
show "?P1 \<mapsto> inv_init1 (?cn)"
apply(simp add: inv_init1.simps assert_imp_def)
done
next
show "inv_end0 ?cn \<mapsto> ?Q1"
apply(simp add: assert_imp_def inv_end0.simps)
done
qed
qed
next
show "{?P2} (H, 0) {?Q2}"
using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
apply(auto)
apply(rule_tac x = na in exI)
apply(simp add: replicate_Suc tape_of_nl_abv)
done
qed
next
show "{?P3}(dither, 0)"
using Hoare_unhalt_def
proof(auto)
fix nd n
assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)"
thus "False"
using dither_unhalt_rs[of nd n]
by simp
qed
qed
thus "\<not> True"
using h
apply(auto simp: haltP_def Hoare_unhalt_def)
apply(erule_tac x = n in allE)
apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
apply(simp add: tape_of_nl_abv)
done
qed
text {*
@{text "False"} is finally derived.
*}
lemma false: "False"
using uh_h h_uh
by auto
end
end