--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/uncomputable.thy Wed Jan 16 10:12:43 2013 +0000
@@ -0,0 +1,1451 @@
+(* 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>)"
+
+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.
+*}
+
+
+fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" ("< _ >" [0] 100)
+ where
+ "tape_of_nat_list [] = []" |
+ "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
+ "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
+
+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)
+ 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 = 2 in allE, erule_tac x = 0 in allE)
+ apply(simp add: numeral_2_eq_2 replicate_Suc)
+ 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)
+ 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", simp)
+ done
+qed
+
+text {*
+ @{text "False"} is finally derived.
+*}
+
+lemma false: "False"
+using uh_h h_uh
+by auto
+end
+
+end
+