--- a/Paper/Paper.thy Tue Jan 22 14:46:02 2013 +0000
+++ b/Paper/Paper.thy Wed Jan 23 08:01:35 2013 +0100
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports "../thys/recursive"
+imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar"
begin
(*
@@ -21,6 +21,7 @@
W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
update2 ("update") and
+ tm_wf0 ("wf") and
(* abc_lm_v ("lookup") and
abc_lm_s ("set") and*)
haltP ("stdhalt") and
@@ -90,7 +91,7 @@
of register machines) and recursive functions. To see the difficulties
involved with this work, one has to understand that Turing machine
programs can be completely \emph{unstructured}, behaving
-similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
+similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
general case a compositional Hoare-style reasoning about Turing
programs. We provide such Hoare-rules for when it \emph{is} possible to
reason in a compositional manner (which is fortunately quite often), but also tackle
@@ -309,14 +310,14 @@
%states.\footnote{The usual disjoint union operation in Isabelle/HOL
%cannot be used as it does not preserve types.} This renaming can be
%quite cumbersome to reason about.
- We followed the choice made by \cite{AspertiRicciotti12}
+ We followed the choice made in \cite{AspertiRicciotti12}
representing a state by a natural number and the states of a Turing
machine by the initial segment of natural numbers starting from @{text 0}.
In doing so we can compose two Turing machine by
shifting the states of one by an appropriate amount to a higher
segment and adjusting some ``next states'' in the other. {\it composition here?}
- An \emph{instruction} @{term i} of a Turing machine is a pair consisting of
+ An \emph{instruction} of a Turing machine is a pair consisting of
an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
machine is then a list of such pairs. Using as an example the following Turing machine
program, which consists of four instructions
@@ -398,13 +399,12 @@
configuration and a program, we can calculate
what the next configuration is by fetching the appropriate action and next state
from the program, and by updating the state and tape accordingly.
- This single step of execution is defined as the function @{term tstep}
+ This single step of execution is defined as the function @{term step}
\begin{center}
- \begin{tabular}{l}
- @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\
- \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\
- \hspace{10mm}@{text "in (s', update (l, r) a)"}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\
+ & & @{text "in (s', update (l, r) a)"}
\end{tabular}
\end{center}
@@ -540,6 +540,20 @@
halting problem
*}
+text {*
+ \begin{center}
+ \begin{tabular}{@ {}p{3cm}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"]}
+ \end{tabular}
+ \end{center}
+
+
+*}
+
section {* Abacus Machines *}
text {*
--- a/Paper/ROOT.ML Tue Jan 22 14:46:02 2013 +0000
+++ b/Paper/ROOT.ML Wed Jan 23 08:01:35 2013 +0100
@@ -1,7 +1,7 @@
no_document
-use_thys ["../thys/turing_basic"(*,
+use_thys ["../thys/turing_basic",
"../thys/turing_hoare",
- "../thys/uncomputable",
+ "../thys/uncomputable"(*,
"../thys/abacus",
"../thys/rec_def",
"../thys/recursive"*)];
--- a/Paper/document/root.tex Tue Jan 22 14:46:02 2013 +0000
+++ b/Paper/document/root.tex Wed Jan 23 08:01:35 2013 +0100
@@ -5,6 +5,7 @@
\usepackage{times}
\usepackage{amssymb}
\usepackage{amsmath}
+\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{pdfsetup}
\usepackage{tikz}
@@ -18,6 +19,11 @@
\urlstyle{rm}
\isabellestyle{it}
+% mathpatir
+\mprset{sep=0.8em}
+\mprset{center=false}
+\mprset{flushleft=true}
+
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
Binary file paper.pdf has changed
--- a/thys/abacus.thy Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/abacus.thy Wed Jan 23 08:01:35 2013 +0100
@@ -3,7 +3,7 @@
*}
theory abacus
-imports Main turing_hoare
+imports Main turing_basic
begin
text {*
--- a/thys/turing_basic.thy Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/turing_basic.thy Wed Jan 23 08:01:35 2013 +0100
@@ -174,6 +174,10 @@
"tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and>
(\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
+abbreviation
+ "tm_wf0 p \<equiv> tm_wf (p, 0)"
+
+
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)
--- a/thys/turing_hoare.thy Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/turing_hoare.thy Wed Jan 23 08:01:35 2013 +0100
@@ -53,17 +53,17 @@
text {*
- {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A, B well-formed
- ------------------------------------------------------
+ {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A well-formed
+ ---------------------------------------------------
{P1} A |+| B {Q2}
*}
lemma Hoare_plus_halt:
- assumes a_imp: "Q1 \<mapsto> P2"
+ assumes A_halt : "{P1} A {Q1}"
+ and B_halt : "{P2} B {Q2}"
+ and a_imp: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
- and A_halt : "{P1} A {Q1}"
- and B_halt : "{P2} B {Q2}"
shows "{P1} A |+| B {Q2}"
proof(rule HoareI)
fix l r
@@ -103,10 +103,10 @@
lemma Hoare_plus_unhalt:
- assumes a_imp: "Q1 \<mapsto> P2"
+ assumes A_halt: "{P1} A {Q1}"
+ and B_uhalt: "{P2} B \<up>"
+ and a_imp: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
- and A_halt : "{P1} A {Q1}"
- and B_uhalt : "{P2} B \<up>"
shows "{P1} (A |+| B) \<up>"
proof(rule_tac Hoare_unhalt_I)
fix n l r
@@ -155,13 +155,5 @@
by (metis holds_for.simps surj_pair)
-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]
-
-
end
\ No newline at end of file
--- a/thys/uncomputable.thy Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/uncomputable.thy Wed Jan 23 08:01:35 2013 +0100
@@ -9,6 +9,24 @@
imports Main turing_hoare
begin
+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]
+
+
+lemma numeral:
+ shows "1 = Suc 0"
+ and "2 = Suc 1"
+ and "3 = Suc 2"
+ and "4 = Suc 3"
+ and "5 = Suc 4"
+ and "6 = Suc 5" by arith+
+
+
+
text {*
The {\em Copying} TM, which duplicates its input.
*}
@@ -51,8 +69,6 @@
declare inv_init.simps[simp del]
-lemma numeral_4_eq_4: "4 = Suc 3"
-by arith
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"
@@ -62,9 +78,9 @@
lemma inv_init_step:
"\<lbrakk>inv_init x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
+unfolding tcopy_init_def
apply(case_tac cf)
-apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral split: if_splits)
apply(case_tac "hd c", auto simp: inv_init.simps)
apply(case_tac c, simp_all)
done
@@ -137,8 +153,8 @@
proof(simp)
assume "inv_init x (s, l, r)" "0 < s"
thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
- apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+ apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral
+ split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
@@ -254,9 +270,6 @@
apply(case_tac t, auto)
done
-lemma numeral_5_eq_5: "5 = Suc 4" by arith
-
-lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith
lemma [simp]: "inv_loop1 x (b, []) = False"
by(simp add: inv_loop1.simps)
@@ -472,8 +485,7 @@
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
-apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 split: if_splits)
+apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
done
lemma inv_loop_steps:
@@ -648,8 +660,7 @@
using h
apply(case_tac r', case_tac [2] a)
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def
- numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
- numeral_5_eq_5 numeral_6_eq_6 loop_LE_def lex_triple_def lex_pair_def split: if_splits)
+ numeral loop_LE_def lex_triple_def lex_pair_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"
@@ -862,8 +873,7 @@
inv_end x cf\<rbrakk>
\<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
-apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 split: if_splits)
+apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
done
lemma inv_end_steps:
@@ -937,8 +947,7 @@
hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
apply(case_tac r', case_tac [2] a)
apply(auto simp: inv_end.simps step.simps tcopy_end_def
- numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
- numeral_5_eq_5 numeral_6_eq_6 end_LE_def lex_triple_def lex_pair_def split: if_splits)
+ numeral end_LE_def lex_triple_def lex_pair_def split: if_splits)
done
thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n),
steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
@@ -1037,7 +1046,7 @@
(0, Bk\<up>m, [Oc, Oc])"
apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
apply(simp add: dither_def steps.simps
- step.simps fetch.simps numeral_2_eq_2)
+ step.simps fetch.simps numeral)
done
lemma dither_unhalt_state:
@@ -1046,7 +1055,7 @@
(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
apply(induct stp, simp add: steps.simps)
apply(simp add: step_red, auto)
- apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2)
+ apply(auto simp: step.simps fetch.simps dither_def numeral)
done
lemma dither_unhalt_rs:
@@ -1324,14 +1333,17 @@
apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
apply(simp, auto)
apply(erule_tac x = nd in allE, erule_tac x = 2 in allE)
- apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv)
+ apply(simp add: numeral replicate_Suc tape_of_nl_abv)
apply(erule_tac x = 0 in allE, simp)
done
qed
-lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)]
- \<Longrightarrow> \<not> haltP (tcontra H, 0) [code (tcontra H)]"
+
+
+lemma h_uh:
+ assumes "haltP (tcontra H, 0) [code (tcontra H)]"
+ shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]"
proof(simp only: tcontra_def)
let ?tcontr = "(tcopy |+| H) |+| dither"
let ?cn = "Suc (code ?tcontr)"
@@ -1340,7 +1352,6 @@
let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
let ?P3 = ?Q2
- assume h: "haltP (?tcontr, 0) [code ?tcontr]"
have "{?P1} ?tcontr \<up>"
proof(rule_tac Hoare_plus_unhalt, auto)
show "?Q2 \<mapsto> ?P3"
@@ -1373,7 +1384,8 @@
qed
next
show "{?P2} H {?Q2}"
- using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
+ using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] assms
+ unfolding tcontra_def
apply(auto)
apply(rule_tac x = na in exI)
apply(simp add: replicate_Suc tape_of_nl_abv)
@@ -1390,8 +1402,9 @@
by simp
qed
qed
- thus "\<not> True"
- using h
+ thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]"
+ using assms
+ unfolding tcontra_def
apply(auto simp: haltP_def Hoare_unhalt_def)
apply(erule_tac x = n in allE)
apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
@@ -1399,6 +1412,7 @@
done
qed
+
text {*
@{text "False"} is finally derived.
*}
@@ -1406,6 +1420,7 @@
lemma false: "False"
using uh_h h_uh
by auto
+
end
end