--- a/Paper/Paper.thy Sun Jan 27 20:01:13 2013 +0000
+++ b/Paper/Paper.thy Mon Jan 28 02:38:57 2013 +0000
@@ -26,6 +26,7 @@
tcopy_loop ("copy\<^bsub>loop\<^esub>") and
tcopy_end ("copy\<^bsub>end\<^esub>") and
step0 ("step") and
+ uncomputable.tcontra ("C") and
steps0 ("steps") and
exponent ("_\<^bsup>_\<^esup>") and
(* abc_lm_v ("lookup") and
@@ -79,6 +80,12 @@
apply(auto)
done
+lemmas HR1 =
+ Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+
+lemmas HR2 =
+ Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+
(*>*)
section {* Introduction *}
@@ -118,17 +125,16 @@
The only satisfying way out of this problem in a theorem prover based
on classical logic is to formalise a theory of computability. Norrish
-provided such a formalisation for the HOL. He choose
-the $\lambda$-calculus as the starting point for his formalisation of
-computability theory, because of its ``simplicity'' \cite[Page
-297]{Norrish11}. Part of his formalisation is a clever infrastructure
-for reducing $\lambda$-terms. He also established the computational
-equivalence between the $\lambda$-calculus and recursive functions.
-Nevertheless he concluded that it would be appealing
- to have formalisations for more operational models of
-computations, such as Turing machines or register machines. One
-reason is that many proofs in the literature use them. He noted
-however that \cite[Page 310]{Norrish11}:
+provided such a formalisation for HOL4. He choose the
+$\lambda$-calculus as the starting point for his formalisation because
+of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his
+formalisation is a clever infrastructure for reducing
+$\lambda$-terms. He also established the computational equivalence
+between the $\lambda$-calculus and recursive functions. Nevertheless
+he concluded that it would be appealing to have formalisations for
+more operational models of computations, such as Turing machines or
+register machines. One reason is that many proofs in the literature
+use them. He noted however that \cite[Page 310]{Norrish11}:
\begin{quote}
\it``If register machines are unappealing because of their
@@ -185,7 +191,7 @@
our formalisation we follow mainly the proofs from the textbook
\cite{Boolos87} and found that the description there is quite
detailed. Some details are left out however: for example, constructing
-the \emph{copy Turing program} is left as an excerise to the reader; also
+the \emph{copy Turing machine} is left as an excerise to the reader; also
\cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
machines computing unary functions. We had to figure out a way to
generalise this result to $n$-ary functions. Similarly, when compiling
@@ -315,7 +321,7 @@
\noindent
We slightly deviate
- from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12}
+ from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12})
by using the @{term Nop} operation; however its use
will become important when we formalise halting computations and also universal Turing
machines. Given a tape and an action, we can define the
@@ -675,7 +681,7 @@
\noindent
whose three components are given in Figure~\ref{copy}. To the prove
- correctness of these Turing machine programs, we introduce the
+ the correctness of Turing machine programs, we introduce the
notion of total correctness defined in terms of
\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.
@@ -684,7 +690,7 @@
a tape satisfying @{term P} will after some @{text n} steps halt (have
transitioned into the halting state) with a tape satisfying @{term
Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
- realising the case that a program @{term p} started with a tape
+ implementing the case that a program @{term p} started with a tape
satisfying @{term P} will loop (never transition into the halting
state). Both notion are formally defined as
@@ -709,13 +715,13 @@
\noindent
Like Asperti and Ricciotti with their notion of realisability, we
- have set up our Hoare-style reasoning so that we can deal explicitly
+ have set up our Hoare-rules so that we can deal explicitly
with total correctness and non-terminantion, rather than have
notions for partial correctness and termination. Although the latter
would allow us to reason more uniformly (only using Hoare-triples),
- we prefer our definitions because we can derive (below) simple
+ we prefer our definitions because we can derive simple
Hoare-rules for sequentially composed Turing programs. In this way
- we can reason about the correctness of @{term "tcopy_init"}, for
+ we can reason about the correctness of @{term "tcopy_begin"}, for
example, completely separately from @{term "tcopy_loop"} and @{term
"tcopy_end"}.
@@ -792,44 +798,84 @@
to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when
started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of
a value on the tape. Reasoning about this program is substantially
- harder than about @{term dither}. To ease the burden, we can prove
- the following Hoare-rules for sequentially composed programs.
+ harder than about @{term dither}. To ease the burden, we prove
+ the following two Hoare-rules for sequentially composed programs.
\begin{center}
- \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}}
- @{thm[mode=Rule]
- Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
- &
- @{thm[mode=Rule]
- Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
+ \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{9mm}}c@ {}}
+ $\inferrule*[Right=@{thm (prem 4) HR1}]
+ {@{thm (prem 1) HR1} \\ @{thm (prem 3) HR1} \\ @{thm (prem 2) HR1}}
+ {@{thm (concl) HR1}}
+ $ &
+ $
+ \inferrule*[Right=@{thm (prem 4) HR2}]
+ {@{thm (prem 1) HR2} \\ @{thm (prem 3) HR2} \\ @{thm (prem 2) HR2}}
+ {@{thm (concl) HR2}}
+ $
\end{tabular}
\end{center}
-
+
\noindent
- The first corresponds to the usual Hoare-rule for composition of imperative
- programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for
- all tapes @{term "(l, r)"}. The second rule covers the case where rughly the
- first program terminates generating a tape for which the second program
- loops. These are two cases we need in our proof for undecidability.
-
+ The first corresponds to the usual Hoare-rule for composition of two
+ terminating programs. The premise @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means that
+ @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for all tapes @{term "(l,
+ r)"}. The second rule covers the case where the first program
+ terminates generating a tape for which the second program loops.
+ The side-condition about @{thm (prem 4) HR2} is needed in both rules
+ in order to ensure that the redirection of the halting and initial
+ state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
+
+
The Hoare-rules above allow us to prove the correctness of @{term tcopy}
by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"}
and @{term "tcopy_end"} in isolation. We will show some details for the
the program @{term "tcopy_begin"}.
- assertion holds for all tapes
-
- Hoare rule for composition
-
- For showing the undecidability of the halting problem, we need to consider
- two specific Turing machines. copying TM and dithering TM
-
- correctness of the copying TM
-
measure for the copying TM, which we however omit.
- halting problem
+ \begin{center}
+ @{thm haltP_def[where lm="ns"]}
+ \end{center}
+
+
+ Undecidability of the halting problem.
+
+ We assume a coding function from Turing machine programs to natural numbers.
+
+ @{thm (prem 2) uncomputable.h_case} implies
+ @{thm (concl) uncomputable.h_case}
+
+ @{thm (prem 2) uncomputable.nh_case} implies
+ @{thm (concl) uncomputable.nh_case}
+
+ Then contradiction
+
+ \begin{center}
+ @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
+ \end{center}
+
+ Proof
+
+ \begin{center}
+ $\inferrule*{
+ \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
+ {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
+ \\ @{term "{P\<^isub>3} dither {P\<^isub>3}"}
+ }
+ {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}}
+ $
+ \end{center}
+
+ \begin{center}
+ $\inferrule*{
+ \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {Q\<^isub>3}"}}
+ {@{term "{P\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
+ \\ @{term "{Q\<^isub>3} dither \<up>"}
+ }
+ {@{term "{P\<^isub>1} tcontra \<up>"}}
+ $
+ \end{center}
Magnus: invariants -- Section 5.4.5 on page 75.
*}
--- a/Paper/document/root.tex Sun Jan 27 20:01:13 2013 +0000
+++ b/Paper/document/root.tex Mon Jan 28 02:38:57 2013 +0000
@@ -24,7 +24,7 @@
\definecolor{mygrey}{rgb}{.80,.80,.80}
% mathpatir
-\mprset{sep=0.8em}
+\mprset{sep=0.7em}
\mprset{center=false}
\mprset{flushleft=true}
Binary file paper.pdf has changed
--- a/thys/turing_basic.thy Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/turing_basic.thy Mon Jan 28 02:38:57 2013 +0000
@@ -233,6 +233,11 @@
shows "length (A |+| B) = length A + length B"
by auto
+lemma tm_comp_wf[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 tm_comp_step:
assumes unfinal: "\<not> is_final (step0 c A)"
shows "step0 c (A |+| B) = step0 c A"
--- a/thys/turing_hoare.thy Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/turing_hoare.thy Mon Jan 28 02:38:57 2013 +0000
@@ -29,10 +29,11 @@
(* halting case *)
definition
- Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
+ Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
where
"{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))"
+
(* not halting case *)
definition
Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
--- 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"