--- a/thys/uncomputable.thy Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/uncomputable.thy Mon Jan 28 02:38:57 2013 +0000
@@ -881,11 +881,10 @@
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)"
+ 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)"
apply(rule_tac inv_end_steps)
using h by(simp_all add: inv_end.simps)
ultimately show
@@ -893,8 +892,8 @@
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)
+ apply(case_tac "(steps0 (1, l, r) tcopy_end stp)")
+ apply(simp add: inv_end.simps)
done
qed
@@ -909,39 +908,32 @@
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}"
-proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
- show "inv_loop0 x \<mapsto> inv_end1 x"
+ assumes "0 < x"
+ shows "{inv_begin1 x} tcopy {inv_end0 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
- show "tm_wf (tcopy_begin |+| tcopy_loop, 0)" by auto
-next
- assume "0 < x"
- 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)
+ ultimately
+ show "{inv_begin1 x} tcopy {inv_end0 x}"
+ unfolding tcopy_def
+ by (rule_tac Hoare_plus_halt) (auto)
qed
abbreviation
@@ -949,20 +941,20 @@
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)"
- by (simp add: assert_imp_def tape_of_nl_abv)
+ have "pre_tcopy n = inv_begin1 (Suc n)"
+ by (auto simp add: 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)
+ have "inv_end0 (Suc n) = post_tcopy n"
+ 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
@@ -1022,7 +1014,7 @@
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)
@@ -1077,7 +1069,8 @@
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"
@@ -1106,8 +1099,8 @@
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)
+ show "{P1} tcopy {P2}" unfolding P1_def P2_def
+ by (rule tcopy_correct)
next
case B_halt (* of H *)
show "{P2} H {P3}"
@@ -1121,6 +1114,7 @@
(* {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"
@@ -1142,37 +1136,38 @@
(* 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} *)
- have first: "{P1} (tcopy |+| H) {P3}"
+ (* {P1} (tcopy |+| H) {Q3} *)
+ 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}"
- unfolding P2_def P3_def
+ then show "{P2} H {Q3}"
+ 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"