tm: comparison thys/uncomputable.thy

equal deleted inserted replaced

-:904f9351ab94
+:c67e8ed4c865
 text {*
 The {\em Copying} TM, which duplicates its input.
 *}
 definition
-tcopy_init :: "instr list"
+tcopy_begin :: "instr list"
 where
-"tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
+"tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
 (W1, 3), (L, 4), (L, 4), (L, 0)]"
 definition
 tcopy_loop :: "instr list"
 where
 (R, 0), (L, 5)]"
 definition
 tcopy :: "instr list"
 where
-"tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end"
+"tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
-(* tcopy_init *)
+(* tcopy_begin *)
 fun
-inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+inv_begin0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+inv_begin1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>
+"inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>
 (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
-| "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
+| "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
-| "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
+| "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
-| "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
+| "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
-| "inv_init4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"
+| "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_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
+fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
 where
-"inv_init n (s, l, r) =
+"inv_begin n (s, l, r) =
-(if s = 0 then inv_init0 n (l, r) else
+(if s = 0 then inv_begin0 n (l, r) else
-if s = 1 then inv_init1 n (l, r) else
+if s = 1 then inv_begin1 n (l, r) else
-if s = 2 then inv_init2 n (l, r) else
+if s = 2 then inv_begin2 n (l, r) else
-if s = 3 then inv_init3 n (l, r) else
+if s = 3 then inv_begin3 n (l, r) else
-if s = 4 then inv_init4 n (l, r)
+if s = 4 then inv_begin4 n (l, r)
 else False)"
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
 apply(rule_tac x = "Suc i" in exI, simp)
 done
-lemma inv_init_step:
+lemma inv_begin_step:
-"\<lbrakk>inv_init x cf; x > 0\<rbrakk>
+"\<lbrakk>inv_begin x cf; x > 0\<rbrakk>
-\<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
+\<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
-unfolding tcopy_init_def
+unfolding tcopy_begin_def
 apply(case_tac cf)
-apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral split: if_splits)
+apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
-apply(case_tac "hd c", auto simp: inv_init.simps)
+apply(case_tac "hd c", auto simp: inv_begin.simps)
 apply(case_tac c, simp_all)
 done
-lemma inv_init_steps:
+lemma inv_begin_steps:
-"\<lbrakk>inv_init x (s, l, r); x > 0\<rbrakk>
+"\<lbrakk>inv_begin x (s, l, r); x > 0\<rbrakk>
-\<Longrightarrow> inv_init x (steps (s, l, r) (tcopy_init, 0) stp)"
+\<Longrightarrow> inv_begin x (steps (s, l, r) (tcopy_begin, 0) stp)"
 apply(induct stp, simp add: steps.simps)
 apply(auto simp: step_red)
-apply(rule_tac inv_init_step, simp_all)
+apply(rule_tac inv_begin_step, simp_all)
 done
 fun init_state :: "config \<Rightarrow> nat"
 where
 "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
 by (case_tac r, auto, case_tac a, auto)
-lemma wf_init_le: "wf init_LE"
+lemma wf_begin_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)"
+"x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
 proof(rule_tac LE = init_LE in halt_lemma)
-show "wf init_LE" by(simp add: wf_init_le)
+show "wf init_LE" by(simp add: wf_begin_le)
 next
 assume h: "0 < x"
-show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<longrightarrow>
+show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
-(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n),
+(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
-steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
+steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 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)"
+assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
-have b: "inv_init x (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
+have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
-apply(rule_tac inv_init_steps)
+apply(rule_tac inv_begin_steps)
-apply(simp_all add: inv_init.simps h)
+apply(simp_all add: inv_begin.simps h)
 done
-obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) = (s, l, r)"
+obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
-apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n", auto)
+apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
 done
-moreover hence "inv_init x (s, l, r)"
+moreover hence "inv_begin x (s, l, r)"
 using c b by simp
-ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n),
+ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
-steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
+steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
 using a
-proof(simp del: inv_init.simps)
+proof(simp del: inv_begin.simps)
-assume "inv_init x (s, l, r)" "0 < s"
+assume "inv_begin x (s, l, r)" "0 < s"
-thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
+thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> init_LE"
-apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
+apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
 apply(case_tac r, auto, case_tac a, auto)
 done
 qed
 qed
 qed
 lemma init_correct:
-"x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
+"x > 0 \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
 proof(rule_tac Hoare_haltI)
 fix l r
 assume h: "0 < x"
-"inv_init1 x (l, r)"
+"inv_begin1 x (l, r)"
-hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
+hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
 by(erule_tac init_halt)
-then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)" ..
+then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
-moreover have "inv_init x (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
+moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
-apply(rule_tac inv_init_steps)
+apply(rule_tac inv_begin_steps)
-using h by(simp_all add: inv_init.simps)
+using h by(simp_all add: inv_begin.simps)
 ultimately show
-"\<exists>n. is_final (steps (1, l, r) (tcopy_init, 0) n) \<and>
+"\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and>
-inv_init0 x holds_for steps (1, l, r) (tcopy_init, 0) n"
+inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 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)
+apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
 done
 qed
 (* tcopy_loop *)
 "\<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)
+simp add: inv_begin.simps inv_loop.simps)
 done
 qed
 (* tcopy_end *)
 done
 qed
 (* tcopy *)
-lemma [intro]: "tm_wf (tcopy_init, 0)"
+lemma [intro]: "tm_wf (tcopy_begin, 0)"
-by (auto simp: tm_wf.simps tcopy_init_def)
+by (auto simp: tm_wf.simps tcopy_begin_def)
 lemma [intro]: "tm_wf (tcopy_loop, 0)"
 by (auto simp: tm_wf.simps tcopy_loop_def)
 lemma [intro]: "tm_wf (tcopy_end, 0)"
 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
 by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
 lemma tcopy_correct1:
-"\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}"
+"\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_begin1 x} tcopy {inv_end0 x}"
 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
 show "inv_loop0 x \<mapsto> inv_end1 x"
 by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
 next
-show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto
+show "tm_wf (tcopy_begin |+| tcopy_loop, 0)" by auto
 next
 assume "0 < x"
-thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}"
+thus "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
 proof(rule_tac Hoare_plus_halt)
-show "inv_init0 x \<mapsto> inv_loop1 x"
+show "inv_begin0 x \<mapsto> inv_loop1 x"
-apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def)
+apply(auto simp: inv_begin0.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
+show "tm_wf (tcopy_begin, 0)" by auto
 next
 assume "0 < x"
-thus "{inv_init1 x} tcopy_init {inv_init0 x}"
+thus "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
 by(erule_tac init_correct)
 next
 assume "0 < x"
 thus "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
 by(erule_tac loop_correct)
 thus "{inv_end1 x} tcopy_end {inv_end0 x}"
 by(erule_tac end_correct)
 qed
 abbreviation
-"pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([], <[n::nat]>))"
+"pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <[n::nat]>)"
 abbreviation
-"post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[n, n::nat]>))"
+"post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <[n, n::nat]>)"
 lemma tcopy_correct2:
 shows "{pre_tcopy n} tcopy {post_tcopy n}"
 proof -
-have "{inv_init1 (Suc n)} tcopy {inv_end0 (Suc n)}"
+have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 by (rule tcopy_correct1) (simp)
 moreover
-have "pre_tcopy n \<mapsto> inv_init1 (Suc n)"
+have "pre_tcopy n \<mapsto> inv_begin1 (Suc n)"
 by (simp add: assert_imp_def tape_of_nl_abv)
 moreover
 have "inv_end0 (Suc n) \<mapsto> post_tcopy n"
 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
 ultimately
 where
 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
 (* invariants of dither *)
 abbreviation
-"dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
+"dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
 abbreviation
-"dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
+"dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 lemma dither_loops_aux:
 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
 apply(induct stp)
-apply(auto simp: steps.simps step.simps dither_def numeral)
+apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)
 done
 lemma dither_loops:
 shows "{dither_unhalt_inv} dither \<up>"
 apply(rule Hoare_unhaltI)
 using dither_loops_aux
-apply(auto simp add: numeral)
+apply(auto simp add: numeral tape_of_nat_abv)
 by (metis Suc_neq_Zero is_final_eq)
 lemma dither_halts_aux:
 shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])"
 lemma dither_halts:
 shows "{dither_halt_inv} dither {dither_halt_inv}"
 apply(rule Hoare_haltI)
 using dither_halts_aux
-apply(auto)
+apply(auto simp add: tape_of_nat_abv)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 section {* The diagnal argument below shows the undecidability of Halting problem *}
 text {*
 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
 and the final configuration is standard.
 *}
-definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
+definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
 where
-"haltP p lm \<equiv> \<exists>n a m. steps (1, [], <lm>) p n = (0, Bk \<up> a,  <m::nat>)"
+"haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k m. tp = (Bk \<up> k,  <m::nat>)))}"
-abbreviation
-"haltP0 p lm \<equiv> haltP (p, 0) lm"
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
 lemma [intro, simp]: "tm_wf0 dither"
 assumes h_wf[intro]: "tm_wf0 H"
 -- {*
 The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 *}
 and h_case:
-"\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc]))"
+"\<And> M lm. haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>))}"
 and nh_case:
-"\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc, Oc]))"
+"\<And> M lm. \<not> haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>))}"
 begin
 (* invariants for H *)
 abbreviation
-"pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
+"pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)"
 abbreviation
-"post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
+"post_H_halt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
 abbreviation
-"post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
+"post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
 lemma H_halt_inv:
-assumes "\<not> haltP0 M [n]"
+assumes "\<not> haltP M [n]"
 shows "{pre_H_inv M n} H {post_H_halt_inv}"
-proof -
+using assms nh_case by auto
-obtain stp i
-where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
-using nh_case assms by blast
-then show "{pre_H_inv M n} H {post_H_halt_inv}"
-unfolding Hoare_halt_def
-apply(auto)
-apply(rule_tac x = stp in exI)
-apply(auto)
-done
-qed
 lemma H_unhalt_inv:
-assumes "haltP0 M [n]"
+assumes "haltP M [n]"
 shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
-proof -
+using assms h_case by auto
-obtain stp i
-where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
-using h_case assms by blast
-then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
-unfolding Hoare_halt_def
-apply(auto)
-apply(rule_tac x = stp in exI)
-apply(auto)
-done
-qed
 (* TM that produces the contradiction and its code *)
 abbreviation
 "tcontra \<equiv> (tcopy |+| H) |+| dither"
 abbreviation
 "code_tcontra \<equiv> code tcontra"
 (* assume tcontra does not halt on its code *)
 lemma tcontra_unhalt:
-assumes "\<not> haltP0 tcontra [code tcontra]"
+assumes "\<not> haltP tcontra [code tcontra]"
 shows "False"
 proof -
 (* invariants *)
-def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
-def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
+def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
 (*
 {P1} tcopy {P2}  {P2} H {P3}
 ----------------------------
 {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
 by (rule tcopy_correct2)
 next
 case B_halt (* of H *)
 show "{P2} H {P3}"
 unfolding P2_def P3_def
-using assms by (rule H_halt_inv)
+by (rule H_halt_inv[OF assms])
 qed (simp)
 (* {P3} dither {P3} *)
 have second: "{P3} dither {P3}" unfolding P3_def
 by (rule dither_halts)
 unfolding Hoare_halt_def
 apply(auto)
 apply(drule_tac x = n in spec)
 apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
 apply(auto)
-apply(drule_tac x = 1 in spec)
-apply(simp add: numeral tape_of_nat_abv)
 done
 qed
 (* asumme tcontra halts on its code *)
 lemma tcontra_halt:
-assumes "haltP0 tcontra [code tcontra]"
+assumes "haltP tcontra [code tcontra]"
 shows "False"
 proof -
 (* invariants *)
-def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
-def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
+def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 (*
 {P1} tcopy {P2}  {P2} H {P3}
 ----------------------------
 {P1} (tcopy |+| H) {P3}     {P3} dither loops
 by (rule tcopy_correct2)
 next
 case B_halt (* of H *)
 then show "{P2} H {P3}"
 unfolding P2_def P3_def
-using assms by (rule H_unhalt_inv)
+by (rule H_unhalt_inv[OF assms])
 qed (simp)
 (* {P3} dither loops *)
 have second: "{P3} dither \<up>" unfolding P3_def
 by (rule dither_loops)
 by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
 with assms show "False"
 unfolding P1_def
 unfolding haltP_def
-unfolding Hoare_unhalt_def
+unfolding Hoare_halt_def Hoare_unhalt_def
-by (auto, metis is_final_eq)
+by auto
 qed
 text {*
 @{text "False"} can finally derived.
 *}

changeset 89	c67e8ed4c865
parent 84	4c8325c64dab
child 91	2068654bdf54