tm: comparison thys/uncomputable.thy

equal deleted inserted replaced

-:01f688735b9b
+:2cae8a39803e
 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
 | "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))"
 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
 where
 "inv_begin n (s, tp) =
 (if s = 0 then inv_begin0 n tp else
 if s = 1 then inv_begin1 n tp else
 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"
 by (rule_tac x = "Suc i" in exI, simp)
 lemma inv_begin_step:
-assumes "inv_begin x cf"
+assumes "inv_begin n cf"
-and "x > 0"
+and "n > 0"
-shows "inv_begin x (step0 cf tcopy_begin)"
+shows "inv_begin n (step0 cf tcopy_begin)"
 using assms
 unfolding tcopy_begin_def
 apply(case_tac cf)
 apply(auto simp: numeral split: if_splits)
 apply(case_tac "hd c")
 apply(case_tac c)
 apply(simp_all)
 done
 lemma inv_begin_steps:
-assumes "inv_begin x cf"
+assumes "inv_begin n cf"
-and "x > 0"
+and "n > 0"
-shows "inv_begin x (steps0 cf tcopy_begin stp)"
+shows "inv_begin n (steps0 cf tcopy_begin stp)"
 apply(induct stp)
 apply(simp add: assms)
 apply(auto simp del: steps.simps)
 apply(rule_tac inv_begin_step)
 apply(simp_all add: assms)
 done
-(*
 lemma begin_partial_correctness:
-assumes "\<exists>stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
+assumes "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
 shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
-using assms
+proof(rule_tac Hoare_haltI)
-apply(auto simp add: Hoare_halt_def)
+fix l r
-apply(rule_tac x="stp" in exI)
+assume h: "0 < n" "inv_begin1 n (l, r)"
-apply(simp)
+have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
-apply(case_tac "steps0 (Suc 0, [], Oc \<up> n) tcopy_begin stp")
+using h by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps)
-apply(simp)
+then show
-apply(case_tac n)
+"\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and>
-apply(simp)
+inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
-apply(simp)
+using h assms
-apply(case_tac nat)
+apply(rule_tac x = stp in exI)
-apply(simp)
+apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
-apply(simp)
+done
-*)
+qed
 fun measure_begin_state :: "config \<Rightarrow> nat"
 where
 "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
 if s = 4 then length l
 else 0)"
 definition
-"begin_LE = measures [measure_begin_state, measure_begin_step]"
+"measure_begin = measures [measure_begin_state, measure_begin_step]"
-lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
+lemma wf_measure_begin:
-by (case_tac r, auto, case_tac a, auto)
+shows "wf measure_begin"
+unfolding measure_begin_def
+by auto
-lemma halt_lemma:
-"\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+lemma measure_begin_induct [case_names Step]:
+"\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_begin\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+using wf_measure_begin
 by (metis wf_iff_no_infinite_down_chain)
-lemma begin_halt:
+lemma begin_halts:
-"x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
+assumes h: "x > 0"
-proof(rule_tac LE = begin_LE in halt_lemma)
+shows "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
-show "wf begin_LE" unfolding begin_LE_def by (auto)
+proof (induct rule: measure_begin_induct)
-next
+case (Step n)
-assume h: "0 < x"
+have "\<not> is_final (steps0 (1, [], Oc \<up> x) tcopy_begin n)" by fact
-show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
+moreover
-(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
+have "inv_begin x (steps0 (1, [], Oc \<up> x) tcopy_begin n)"
-steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
+by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps h)
-proof(rule_tac allI, rule_tac impI)
+moreover
-fix n
+obtain s l r where eq: "(steps0 (1, [], Oc \<up> x) tcopy_begin n) = (s, l, r)"
-assume a: "\<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
+by (metis measure_begin_state.cases)
-have b: "inv_begin x (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
+ultimately
-apply(rule_tac inv_begin_steps)
+have "(step0 (s, l, r) tcopy_begin, s, l, r) \<in> measure_begin"
-apply(simp_all add: inv_begin.simps h)
+apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
-done
+apply(subgoal_tac "r = [Oc]")
-obtain s l r where c: "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
+apply(auto)
-apply(case_tac "steps (1, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
+by (metis cell.exhaust list.exhaust tl.simps(2))
-done
+then
-moreover hence "inv_begin x (s, l, r)"
+show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"
-using c b by simp
+using eq by (simp only: step_red)
-ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
-steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
-using a
-proof(simp del: inv_begin.simps step.simps steps.simps)
-assume "inv_begin x (s, l, r)" "0 < s"
-thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
-apply(auto simp: begin_LE_def step.simps tcopy_begin_def numeral split: if_splits)
-apply(case_tac r, auto, case_tac a, auto)
-done
-qed
-qed
 qed
 lemma begin_correct:
-"0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
+shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
-proof(rule_tac Hoare_haltI)
+using begin_partial_correctness begin_halts by blast
-fix l r
-assume h: "0 < n" "inv_begin1 n (l, r)"
-then have "\<exists> stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
-by (rule_tac begin_halt)
-then obtain stp where "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" ..
-moreover have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
-apply(rule_tac inv_begin_steps)
-using h by(simp_all add: inv_begin.simps)
-ultimately show
-"\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and>
-inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
-using h
-apply(rule_tac x = stp in exI)
-apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
-done
-qed
 declare tm_comp.simps [simp del]
 declare adjust.simps[simp del]
 declare shift.simps[simp del]
 declare tm_wf.simps[simp del]
 declare step.simps[simp del]
 declare steps.simps[simp del]
 (* tcopy_loop *)
 fun
 inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"
+"inv_loop1_loop n (l, r) = (\<exists> i j. i + j + 1 = n \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"
-| "inv_loop1_exit x (l, r) = ((l, r) = ([], Bk#Oc#Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
+| "inv_loop1_exit n (l, r) = (0 < n \<and> (l, r) = ([], Bk#Oc#Bk\<up>n @ Oc\<up>n))"
 | "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, r) = (Oc\<up>k@Bk\<up>j@Oc\<up>i, Oc\<up>t))"
 | "inv_loop5_exit x (l, r) =
 (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Bk\<up>(j - 1)@Oc\<up>i, Bk # Oc\<up>j))"
 | "inv_loop6_loop x (l, r) =
 inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"inv_loop0 x (l, r) =  ((l, r) = ([Bk], Oc # Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
+"inv_loop0 n (l, r) =  (0 < n \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"
-| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
+| "inv_loop1 n (l, r) = (inv_loop1_loop n (l, r) \<or> inv_loop1_exit n (l, r))"
-| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"
+| "inv_loop2 n (l, r) = (\<exists> i j any. i + j = n \<and> n > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"
-| "inv_loop3 x (l, r) =
+| "inv_loop3 n (l, r) =
-(\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> (l, r) = (Bk\<up>k@Oc\<up>i, Bk\<up>t@Oc\<up>j))"
+(\<exists> i j k t. i + j = n \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> (l, r) = (Bk\<up>k@Oc\<up>i, Bk\<up>t@Oc\<up>j))"
-| "inv_loop4 x (l, r) =
+| "inv_loop4 n (l, r) =
-(\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> (l, r) = (Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i, Oc\<up>t))"
+(\<exists> i j k t. i + j = n \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> (l, r) = (Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i, Oc\<up>t))"
-| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
+| "inv_loop5 n (l, r) = (inv_loop5_loop n (l, r) \<or> inv_loop5_exit n (l, r))"
-| "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
+| "inv_loop6 n (l, r) = (inv_loop6_loop n (l, r) \<or> inv_loop6_exit n (l, r))"
 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
 where
 "inv_loop x (s, l, r) =
 (if s = 0 then inv_loop0 x (l, r)
 apply(case_tac cf, case_tac c, case_tac [2] aa)
 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 done
 lemma inv_loop_steps:
-"\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
+"\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"
-\<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"
 else if s = 4 then length r
 else if s = 5 then length l
 else if s = 6 then length l
 else 0)"
-definition loop_LE :: "(config \<times> config) set"
+definition measure_loop :: "(config \<times> config) set"
 where
-"loop_LE = measures [loop_stage, loop_state, loop_step]"
+"measure_loop = measures [loop_stage, loop_state, loop_step]"
-lemma wf_loop_le: "wf loop_LE"
+lemma wf_measure_loop: "wf measure_loop"
-unfolding loop_LE_def
+unfolding measure_loop_def
 by (auto)
+lemma measure_loop_induct [case_names Step]:
+"\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_loop\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+using wf_measure_loop
+by (metis wf_iff_no_infinite_down_chain)
 lemma [simp]: "inv_loop2 x ([], b) = False"
 by (auto simp: inv_loop2.simps)
 lemma  [simp]: "inv_loop2 x (l', []) = False"
 lemma [simp]: "inv_loop3 x (b, []) = False"
 by (auto simp: inv_loop3.simps)
 lemma [simp]: "inv_loop4 x ([], b) = False"
 by (auto simp: inv_loop4.simps)
 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>
 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:
+lemma loop_halts:
-"\<lbrakk>x > 0; inv_loop x (Suc 0, l, r)\<rbrakk> \<Longrightarrow>
+assumes h: "n > 0" "inv_loop n (1, l, r)"
-\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
+shows "\<exists> stp. is_final (steps0 (1, l, r) tcopy_loop stp)"
-proof(rule_tac LE = loop_LE in halt_lemma)
+proof (induct rule: measure_loop_induct)
-show "wf loop_LE" by(intro wf_loop_le)
+case (Step stp)
-next
+have "\<not> is_final (steps0 (1, l, r) tcopy_loop stp)" by fact
-assume h: "0 < x"  and g: "inv_loop x (Suc 0, l, r)"
+moreover
-show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n) \<longrightarrow>
+have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
-(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
+by (rule_tac inv_loop_steps) (simp_all only: h)
-proof(rule_tac allI, rule_tac impI)
+moreover
-fix n
+obtain s l' r' where eq: "(steps0 (1, l, r) tcopy_loop stp) = (s, l', r')"
-assume a: "\<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n)"
+by (metis measure_begin_state.cases)
-obtain s' l' r' where d: "(steps (Suc 0, l, r) (tcopy_loop, 0) n) = (s', l', r')"
+ultimately
-by(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) n)", auto)
+have "(step0 (s, l', r') tcopy_loop, s, l', r') \<in> measure_loop"
-hence "inv_loop x (s', l', r') \<and> s' \<noteq> 0"
+using h(1)
-using h g
+apply(case_tac r')
-apply(drule_tac stp = n in inv_loop_steps, auto)
+apply(case_tac [2] a)
-using a
+apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral measure_loop_def split: if_splits)
-apply(simp)
+done
-done
+then
-hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE"
+show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) \<in> measure_loop"
-using h
+using eq by (simp only: step_red)
-apply(case_tac r', case_tac [2] a)
-apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral loop_LE_def split: if_splits)
-done
-thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n),
-steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
-using d
-apply(simp add: step_red)
-done
-qed
 qed
 lemma loop_correct:
-"x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
+shows "0 < n \<Longrightarrow> {inv_loop1 n} tcopy_loop {inv_loop0 n}"
+using assms
 proof(rule_tac Hoare_haltI)
 fix l r
-assume h: "0 < x"
+assume h: "0 < n" "inv_loop1 n (l, r)"
-"inv_loop1 x (l, r)"
+then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)"
-hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
+using loop_halts
-apply(rule_tac loop_halt, simp_all add: inv_loop.simps)
+apply(simp add: inv_loop.simps)
+apply(blast)
 done
-then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)" ..
+moreover
-moreover have "inv_loop x (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
+have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
-apply(rule_tac inv_loop_steps)
+using h
-using h by(simp_all add: inv_loop.simps)
+by (rule_tac inv_loop_steps) (simp_all add: inv_loop.simps)
 ultimately show
-"\<exists>n. is_final (steps (1, l, r) (tcopy_loop, 0) n) \<and>
+"\<exists>stp. is_final (steps0 (1, l, r) tcopy_loop stp) \<and>
-inv_loop0 x holds_for steps (1, l, r) (tcopy_loop, 0) n"
+inv_loop0 n holds_for steps0 (1, l, r) tcopy_loop stp"
-using h
+using h(1)
 apply(rule_tac x = stp in exI)
-apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)",
+apply(case_tac "(steps0 (1, l, r) tcopy_loop stp)")
-simp add: inv_begin.simps inv_loop.simps)
+apply(simp add: inv_loop.simps)
 done
 qed
 (* tcopy_end *)
 fun
 fun
 inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool" and
 inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 inv_end5 :: "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)"
+"inv_end0 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc\<up>n @ Bk # Oc\<up>n))"
-| "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
+| "inv_end1 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"
-| "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)"
+| "inv_end2 n (l, r) = (\<exists> i j. i + j = Suc n \<and> n > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>n)"
-| "inv_end3 x (l, r) =
+| "inv_end3 n (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)"
+(\<exists> i j. n > 0 \<and> i + j = n \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>n)"
-| "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
+| "inv_end4 n (l, r) = (\<exists> any. n > 0 \<and> l = Oc\<up>n @ [Bk] \<and> r = any#Oc\<up>n)"
-| "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
+| "inv_end5 n (l, r) = (inv_end5_loop n (l, r) \<or> inv_end5_exit n (l, r))"
 fun
 inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
 where
-"inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
+"inv_end n (s, l, r) = (if s = 0 then inv_end0 n (l, r)
-else if s = 1 then inv_end1 x (l, r)
+else if s = 1 then inv_end1 n (l, r)
-else if s = 2 then inv_end2 x (l, r)
+else if s = 2 then inv_end2 n (l, r)
-else if s = 3 then inv_end3 x (l, r)
+else if s = 3 then inv_end3 n (l, r)
-else if s = 4 then inv_end4 x (l, r)
+else if s = 4 then inv_end4 n (l, r)
-else if s = 5 then inv_end5 x (l, r)
+else if s = 5 then inv_end5 n (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]
 unfolding end_LE_def
 by (auto)
 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
 by (auto simp: inv_end5.simps inv_end5_loop.simps)
+lemma halt_lemma:
+"\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
 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)
 by simp
 qed
 qed
 lemma end_correct:
-"x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
+"n > 0 \<Longrightarrow> {inv_end1 n} tcopy_end {inv_end0 n}"
 proof(rule_tac Hoare_haltI)
 fix l r
-assume h: "0 < x"
+assume h: "0 < n"
-"inv_end1 x (l, r)"
+"inv_end1 n (l, r)"
 then have "\<exists> stp. is_final (steps0 (1, l, r) tcopy_end stp)"
 by (simp add: end_halt inv_end.simps)
 then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
-moreover have "inv_end x (steps0 (1, l, r) tcopy_end stp)"
+moreover have "inv_end n (steps0 (1, l, r) tcopy_end 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>
+"\<exists>stp. is_final (steps (1, l, r) (tcopy_end, 0) stp) \<and>
-inv_end0 x holds_for steps (1, l, r) (tcopy_end, 0) n"
+inv_end0 n holds_for steps (1, l, r) (tcopy_end, 0) stp"
 using h
 apply(rule_tac x = stp in exI)
 apply(case_tac "(steps0 (1, l, r) tcopy_end stp)")
 apply(simp add: inv_end.simps)
 done
 show "{inv_begin1 x} tcopy {inv_end0 x}"
 unfolding tcopy_def
 by (rule_tac Hoare_plus_halt) (auto)
 qed
-abbreviation
+abbreviation (input)
-"pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <[n::nat]>)"
+"pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <(n::nat)>)"
-abbreviation
+abbreviation (input)
-"post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <[n, n::nat]>)"
+"post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"
 lemma tcopy_correct:
 shows "{pre_tcopy n} tcopy {post_tcopy n}"
 proof -
 have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 moreover
 have "pre_tcopy n = inv_begin1 (Suc n)"
 by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
 moreover
 have "inv_end0 (Suc n) = post_tcopy n"
-by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nl_abv)
+by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair)
 ultimately
 show "{pre_tcopy n} tcopy {post_tcopy n}"
 by simp
 qed
 assumes h_wf[intro]: "tm_wf0 H"
 -- {*
 The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 *}
 and h_case:
-"\<And> M ns. haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
+"\<And> M ns. haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
 and nh_case:
-"\<And> M ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
+"\<And> M ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
 begin
 (* invariants for H *)
-abbreviation
+abbreviation (input)
-"pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)"
+"pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)"
-abbreviation
+abbreviation (input)
 "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
-abbreviation
+abbreviation (input)
 "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 lemma H_halt_inv:
-assumes "\<not> haltP M [n]"
+assumes "\<not> haltP M ns"
-shows "{pre_H_inv M n} H {post_H_halt_inv}"
+shows "{pre_H_inv M ns} H {post_H_halt_inv}"
 using assms nh_case by auto
 lemma H_unhalt_inv:
-assumes "haltP M [n]"
+assumes "haltP M ns"
-shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
+shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"
 using assms h_case by auto
 (* TM that produces the contradiction and its code *)
 definition
 lemma tcontra_unhalt:
 assumes "\<not> haltP tcontra [code tcontra]"
 shows "False"
 proof -
 (* invariants *)
-def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
+def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
-def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
+def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
 def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 (*
 {P1} tcopy {P2}  {P2} H {P3}
 ----------------------------
 show "{P1} tcopy {P2}" unfolding P1_def P2_def
 by (rule tcopy_correct)
 next
 case B_halt (* of H *)
 show "{P2} H {P3}"
 unfolding P2_def P3_def
-by (rule H_halt_inv[OF assms])
+using H_halt_inv[OF assms]
+by (simp add: tape_of_nat_pair tape_of_nl_abv)
 qed (simp)
 (* {P3} dither {P3} *)
 have second: "{P3} dither {P3}" unfolding P3_def
 by (rule dither_halts)
 with assms show "False"
 unfolding P1_def P3_def
 unfolding haltP_def
 unfolding Hoare_halt_def
 apply(auto)
 apply(drule_tac x = n in spec)
-apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
+apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
-apply(auto)
+apply(auto simp add: tape_of_nl_abv)
 done
 qed
 (* asumme tcontra halts on its code *)
 lemma tcontra_halt:
 assumes "haltP tcontra [code tcontra]"
 shows "False"
 proof -
 (* invariants *)
-def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
+def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
-def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
+def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
 def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 (*
 {P1} tcopy {P2}  {P2} H {Q3}
 ----------------------------
 show "{P1} tcopy {P2}" unfolding P1_def P2_def
 by (rule tcopy_correct)
 next
 case B_halt (* of H *)
 then show "{P2} H {Q3}"
-unfolding P2_def Q3_def
+unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
-by (rule H_unhalt_inv[OF assms])
+by(simp add: tape_of_nat_pair tape_of_nl_abv)
 qed (simp)
 (* {P3} dither loops *)
 have second: "{Q3} dither \<up>" unfolding Q3_def
 by (rule dither_loops)
 with assms show "False"
 unfolding P1_def
 unfolding haltP_def
 unfolding Hoare_halt_def Hoare_unhalt_def
-by auto
+by (auto simp add: tape_of_nl_abv)
 qed
 text {*
 @{text "False"} can finally derived.
 *}

changeset 105	2cae8a39803e
parent 103	294576baaeed
child 109	4635641e77cb