--- a/Paper/Paper.thy Tue Jan 29 13:00:51 2013 +0000
+++ b/Paper/Paper.thy Tue Jan 29 16:37:38 2013 +0000
@@ -719,13 +719,13 @@
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 simple
+ we prefer our definitions because we can derive below some simple
Hoare-rules for sequentially composed Turing programs. In this way
we can reason about the correctness of @{term "tcopy_begin"}, for
example, completely separately from @{term "tcopy_loop"} and @{term
"tcopy_end"}.
- It is realatively straightforward to prove that the Turing program
+ It is realatively straightforward to prove that the small Turing program
@{term "dither"} shown in \eqref{dither} is correct. This program
should be the ``identity'' when started with a standard tape representing
@{text "1"} but loop when started with @{text 0} instead, as pictured
@@ -795,12 +795,13 @@
The first is by a simple calculation. The second is by induction on the
number of steps we can perform starting from the input tape.
- The purpose of the @{term tcopy} program defined in \eqref{tcopy} is
- 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 prove
- the following two Hoare-rules for sequentially composed programs.
+ The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
+ its purpose is 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 prove the following two Hoare-rules for sequentially
+ composed programs.
\begin{center}
\begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
@@ -827,8 +828,17 @@
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 the details for the
- the program @{term "tcopy_begin"}.
+ and @{term "tcopy_end"} in isolation. We will show the details for
+ the program @{term "tcopy_begin"}. We found the following invariants for each
+ state:
+
+ \begin{center}
+ @{thm inv_begin0.simps}\\
+ @{thm inv_begin1.simps}\\
+ @{thm inv_begin2.simps}\\
+ @{thm inv_begin3.simps}\\
+ @{thm inv_begin4.simps}
+ \end{center}
measure for the copying TM, which we however omit.
--- a/thys/uncomputable.thy Tue Jan 29 13:00:51 2013 +0000
+++ b/thys/uncomputable.thy Tue Jan 29 16:37:38 2013 +0000
@@ -9,14 +9,6 @@
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"
@@ -92,9 +84,11 @@
using assms
unfolding tcopy_begin_def
apply(case_tac cf)
-apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
-apply(case_tac "hd c", auto simp: inv_begin.simps)
-apply(case_tac c, simp_all)
+apply(auto simp: numeral split: if_splits)
+apply(case_tac "hd c")
+apply(auto)
+apply(case_tac c)
+apply(simp_all)
done
lemma inv_begin_steps:
@@ -102,48 +96,34 @@
and "x > 0"
shows "inv_begin x (steps0 cf tcopy_begin stp)"
apply(induct stp)
-apply(simp add: steps.simps assms)
-apply(auto simp: step_red)
+apply(simp add: assms)
+apply(auto simp del: steps.simps)
apply(rule_tac inv_begin_step)
apply(simp_all add: assms)
done
-fun begin_state :: "config \<Rightarrow> nat"
+fun measure_begin_state :: "config \<Rightarrow> nat"
where
- "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
+ "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
-fun begin_step :: "config \<Rightarrow> nat"
+fun measure_begin_step :: "config \<Rightarrow> nat"
where
- "begin_step (s, l, r) =
+ "measure_begin_step (s, l, r) =
(if s = 2 then length r else
if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
if s = 4 then length l
else 0)"
-fun begin_measure :: "config \<Rightarrow> nat \<times> nat"
- where
- "begin_measure c = (begin_state c, begin_step c)"
-
-
-definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
- where
- "lex_pair \<equiv> less_than <*lex*> less_than"
-
-definition begin_LE :: "(config \<times> config) set"
- where
- "begin_LE \<equiv> (inv_image lex_pair begin_measure)"
+definition
+ "begin_LE = measures [measure_begin_state, measure_begin_step]"
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_begin_le: "wf begin_LE"
-by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
-
lemma begin_halt:
"x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)"
proof(rule_tac LE = begin_LE in halt_lemma)
- show "wf begin_LE" by(simp add: wf_begin_le)
+ show "wf begin_LE" unfolding begin_LE_def by (auto)
next
assume h: "0 < x"
show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
@@ -164,10 +144,10 @@
ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
using a
- proof(simp del: inv_begin.simps)
+ proof(simp del: inv_begin.simps step.simps steps.simps)
assume "inv_begin x (s, l, r)" "0 < s"
thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
- apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
+ apply(auto simp: begin_LE_def step.simps tcopy_begin_def numeral split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
@@ -194,6 +174,13 @@
done
qed
+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]
+
(* tcopy_loop *)
@@ -477,25 +464,13 @@
else if s = 6 then length l
else 0)"
-definition lex_triple ::
- "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
- where
- "lex_triple \<equiv> less_than <*lex*> lex_pair"
-
-lemma wf_lex_triple: "wf lex_triple"
- by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
-
-fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
- where
- "loop_measure c =
- (loop_stage c, loop_state c, loop_step c)"
-
definition loop_LE :: "(config \<times> config) set"
where
- "loop_LE \<equiv> (inv_image lex_triple loop_measure)"
+ "loop_LE = measures [loop_stage, loop_state, loop_step]"
lemma wf_loop_le: "wf loop_LE"
-by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
+unfolding loop_LE_def
+by (auto)
lemma [simp]: "inv_loop2 x ([], b) = False"
by (auto simp: inv_loop2.simps)
@@ -615,8 +590,7 @@
hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE"
using h
apply(case_tac r', case_tac [2] a)
- apply(auto simp: inv_loop.simps step.simps tcopy_loop_def
- numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits)
+ apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral loop_LE_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"
@@ -833,17 +807,13 @@
else if s = 3 then 0
else 0)"
-fun end_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
- where
- "end_measure c =
- (end_state c, end_stage c, end_step c)"
-
definition end_LE :: "(config \<times> config) set"
where
- "end_LE \<equiv> (inv_image lex_triple end_measure)"
+ "end_LE = measures [end_state, end_stage, end_step]"
lemma wf_end_le: "wf end_LE"
-by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple)
+unfolding end_LE_def
+by (auto)
lemma [simp]: "inv_end5 x ([], Oc # list) = False"
by (auto simp: inv_end5.simps inv_end5_loop.simps)
@@ -870,8 +840,7 @@
done
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 end_LE_def lex_triple_def lex_pair_def split: if_splits)
+ apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_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"