tm: comparison thys/uncomputable.thy

equal deleted inserted replaced

-:b9d0dd18c81e
+:f2bda6ba4952
 "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
 proof(rule_tac Hoare_haltI)
 fix l r
 assume h: "0 < x"
 "inv_end1 x (l, r)"
-hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
+then have "\<exists> stp. is_final (steps0 (1, l, r) tcopy_end stp)"
-apply(rule_tac end_halt, simp_all add: inv_end.simps)
+by (simp add: end_halt inv_end.simps)
-done
+then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
-then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)" ..
+moreover have "inv_end x (steps0 (1, l, r) tcopy_end 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)",
+apply(case_tac "(steps0 (1, l, r) tcopy_end stp)")
-simp add:  inv_end.simps)
+apply(simp add: inv_end.simps)
 done
 qed
 (* tcopy *)
 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)"
-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_begin1 x} tcopy {inv_end0 x}"
+assumes "0 < x"
-proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
+shows "{inv_begin1 x} tcopy {inv_end0 x}"
-show "inv_loop0 x \<mapsto> inv_end1 x"
+proof -
+have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
+by (metis assms init_correct)
+moreover
+have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
+by (metis assms loop_correct)
+moreover
+have "inv_begin0 x \<mapsto> inv_loop1 x"
+by (auto simp: inv_begin0.simps inv_loop1.simps assert_imp_def)
+(rule_tac x = "Suc 0" in exI, auto)
+ultimately
+have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
+by (rule_tac Hoare_plus_halt) (auto)
+moreover
+have "{inv_end1 x} tcopy_end {inv_end0 x}"
+by (metis assms end_correct)
+moreover
+have "inv_loop0 x \<mapsto> inv_end1 x"
 by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
-next
+ultimately
-show "tm_wf (tcopy_begin |+| tcopy_loop, 0)" by auto
+show "{inv_begin1 x} tcopy {inv_end0 x}"
-next
+unfolding tcopy_def
-assume "0 < x"
+by (rule_tac Hoare_plus_halt) (auto)
-thus "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
-proof(rule_tac Hoare_plus_halt)
-show "inv_begin0 x \<mapsto> inv_loop1 x"
-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_begin, 0)" by auto
-next
-assume "0 < 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)
-qed
-next
-assume "0 < x"
-thus "{inv_end1 x} tcopy_end {inv_end0 x}"
-by(erule_tac end_correct)
 qed
 abbreviation
 "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <[n::nat]>)"
 abbreviation
 "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <[n, n::nat]>)"
-lemma tcopy_correct2:
+lemma tcopy_correct:
 shows "{pre_tcopy n} tcopy {post_tcopy n}"
 proof -
 have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 by (rule tcopy_correct1) (simp)
 moreover
-have "pre_tcopy n \<mapsto> inv_begin1 (Suc n)"
+have "pre_tcopy n = inv_begin1 (Suc n)"
-by (simp add: assert_imp_def tape_of_nl_abv)
+by (auto simp add: tape_of_nl_abv)
 moreover
-have "inv_end0 (Suc n) \<mapsto> post_tcopy n"
+have "inv_end0 (Suc n) = post_tcopy n"
-by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
+by (auto simp add: inv_end0.simps tape_of_nl_abv)
 ultimately
 show "{pre_tcopy n} tcopy {post_tcopy n}"
-by (rule Hoare_weaken)
+by simp
 qed
 section {* The {\em Dithering} Turing Machine *}
 and the final configuration is standard.
 *}
 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
 where
-"haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k m. tp = (Bk \<up> k,  <m::nat>)))}"
+"haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k,  <n::nat>)))}"
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
 lemma [intro, simp]: "tm_wf0 dither"
 assumes "haltP M [n]"
 shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
 using assms h_case by auto
 (* TM that produces the contradiction and its code *)
-abbreviation
+definition
 "tcontra \<equiv> (tcopy |+| H) |+| dither"
 abbreviation
 "code_tcontra \<equiv> code tcontra"
 (* assume tcontra does not halt on its code *)
 (* {P1} (tcopy |+| H) {P3} *)
 have first: "{P1} (tcopy |+| H) {P3}"
 proof (cases rule: Hoare_plus_halt_simple)
 case A_halt (* of tcopy *)
 show "{P1} tcopy {P2}" unfolding P1_def P2_def
-by (rule tcopy_correct2)
+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])
 have second: "{P3} dither {P3}" unfolding P3_def
 by (rule dither_halts)
 (* {P1} tcontra {P3} *)
 have "{P1} tcontra {P3}"
+unfolding tcontra_def
 by (rule Hoare_plus_halt_simple[OF first second H_wf])
 with assms show "False"
 unfolding P1_def P3_def
 unfolding haltP_def
 shows "False"
 proof -
 (* invariants *)
 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
+def Q3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 (*
-{P1} tcopy {P2}  {P2} H {P3}
+{P1} tcopy {P2}  {P2} H {Q3}
 ----------------------------
-{P1} (tcopy |+| H) {P3}     {P3} dither loops
+{P1} (tcopy |+| H) {Q3}     {Q3} dither loops
 ------------------------------------------------
 {P1} tcontra loops
 *)
 have H_wf: "tm_wf0 (tcopy |+| H)" by auto
-(* {P1} (tcopy |+| H) {P3} *)
+(* {P1} (tcopy |+| H) {Q3} *)
-have first: "{P1} (tcopy |+| H) {P3}"
+have first: "{P1} (tcopy |+| H) {Q3}"
 proof (cases rule: Hoare_plus_halt_simple)
 case A_halt (* of tcopy *)
 show "{P1} tcopy {P2}" unfolding P1_def P2_def
-by (rule tcopy_correct2)
+by (rule tcopy_correct)
 next
 case B_halt (* of H *)
-then show "{P2} H {P3}"
+then show "{P2} H {Q3}"
-unfolding P2_def P3_def
+unfolding P2_def Q3_def
 by (rule H_unhalt_inv[OF assms])
 qed (simp)
 (* {P3} dither loops *)
-have second: "{P3} dither \<up>" unfolding P3_def
+have second: "{Q3} dither \<up>" unfolding Q3_def
 by (rule dither_loops)
 (* {P1} tcontra loops *)
 have "{P1} tcontra \<up>"
+unfolding tcontra_def
 by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
 with assms show "False"
 unfolding P1_def
 unfolding haltP_def

changeset 93	f2bda6ba4952
parent 92	b9d0dd18c81e
child 94	aeaf1374dc67