--- a/Paper/Paper.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/Paper/Paper.thy Mon Apr 22 08:26:16 2013 +0100
@@ -300,14 +300,13 @@
%represented as inductively defined predicates too.
\noindent
-One concete model of computation are Turing machines. We use them
-in the theorem prover Isabelle/HOL for mechanising results from
-computability theory, for example the undecidability of the halting problem.
-Reasoning about decidability is not as straightforward as one might think
-in Isabelle/HOL and other HOL theorem provers,
-since they are based on classical logic where the law of excluded
-middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
-matter whether the predicate @{text P} is constructed by computable means.
+We like to enable Isabelle/HOL users to reason about computability
+theory. Reasoning about decidability of predicates, for example, is not as
+straightforward as one might think in Isabelle/HOL and other HOL
+theorem provers, since they are based on classical logic where the law
+of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always
+provable no matter whether the predicate @{text P} is constructed by
+computable means.
Norrish formalised computability
theory in HOL4. He choose the $\lambda$-calculus as the starting point
@@ -419,7 +418,7 @@
\cite{AspertiRicciotti12}, instead follow the proof in
\cite{Boolos87} by translating abacus machines to Turing machines and in
turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed by translating from a recursive function.
+machine can then be constructed by translating from a (universal) recursive function.
The part of mechanising the translation of recursive function to register
machines has already been done by Zammit in HOL \cite{Zammit99},
although his register machines use a slightly different instruction
@@ -675,14 +674,9 @@
\noindent
where @{term "read r"} returns the head of the list @{text r}, or if
- @{text r} is empty it returns @{term Bk}. It is impossible in
- Isabelle/HOL to lift the @{term step}-function in order to realise a
- general evaluation function for Turing machines programs. The reason
- is that functions in HOL-based provers need to be terminating, and
- clearly there are programs that are not.\footnote{There is the alternative
- to use partial functions, which do not necessarily need to terminate, but
- this does not provide us with a useful induction principle \cite{Krauss10}.} We can however define a
- recursive evaluation function that performs exactly @{text n} steps:
+ @{text r} is empty it returns @{term Bk}.
+ We lift this definition to an evaluation function that performs
+ exactly @{text n} steps:
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -1657,17 +1651,19 @@
text {*
In previous works we were unable to formalise results about
- computability because in Isabelle/HOL we cannot represent the
- decidability of a predicate @{text P}, say, as the formula @{term "P
- \<or> \<not>P"}. For reasoning about computability we need to formalise a
- concrete model of computations. We could have followed Norrish
- \cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,
- but then we would still have
- %to reimplement his infrastructure for
- %reducing $\lambda$-terms on the ML-level.
- %We would still need
- to connect his work to Turing machines for proofs that make essential use of them
- (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
+ computability because in Isabelle/HOL we cannot, for example,
+ represent the decidability of a predicate @{text P}, say, as the
+ formula @{term "P \<or> \<not>P"}. For reasoning about computability we need
+ to formalise a concrete model of computations. We could have
+ followed Norrish \cite{Norrish11} using the $\lambda$-calculus as
+ the starting point for computability theory, but then we would have
+ to reimplement on the ML-level his infrastructure for rewriting
+ $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that
+ can rewrite terms modulo an arbitrary equivalence relation, which
+ Isabelle unfortunately does not yet have. Even though we would
+ still need to connect $\lambda$-terms somehow to Turing machines for
+ proofs that make essential use of them (for example the
+ undecidability proof for Wang's tiling problem \cite{Robinson71}).
We therefore have formalised Turing machines in the first place and the main
computability results from Chapters 3 to 8 in the textbook by Boolos
@@ -1679,33 +1675,31 @@
if the Turing machine loops \emph{or} halts with a non-standard
tape. Whereas in Chapter 8 about the universal Turing machine, the
Turing machines will \emph{not} halt unless the tape is in standard
- form. If the title had not already been taken in \cite{Nipkow98}, we could
- have titled our paper ``Boolos et al are (almost)
- Right''. We have not attempted to formalise everything precisely as
+ form. Like Nipkow \cite{Nipkow98} observed with his formalisation
+ of a textbook, we found that Boolos et al are (almost)
+ right. We have not attempted to formalise everything precisely as
Boolos et al present it, but use definitions that make our
mechanised proofs manageable. For example our definition of the
halting state performing @{term Nop}-operations seems to be
non-standard, but very much suited to a formalisation in a theorem
prover where the @{term steps}-function needs to be total.
- %The most closely related work is by Norrish \cite{Norrish11}, and by
- %Asperti and Ricciotti \cite{AspertiRicciotti12}.
- Norrish mentions
- that formalising Turing machines would be a ``\emph{daunting prospect}''
- \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to
- some slick mechanised proofs, our experience is that Turing machines
- are not too daunting if one is only concerned with formalising the
- undecidability of the halting problem for Turing machines. As a point of
- comparison, the halting problem
- took us around 1500 loc of Isar-proofs, which is just one-and-a-half
- times of a mechanised proof pearl about the Myhill-Nerode
- theorem. So our conclusion is that this part is not as daunting
- as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
- involved with constructing a universal Turing machine via recursive
- functions and abacus machines, we agree, is not a project
- one wants to undertake too many times (our formalisation of abacus
- machines and their correct translation is approximately 4600 loc;
- recursive functions 2800 loc and the universal Turing machine 10000 loc).
+ Norrish mentions that formalising Turing machines would be a
+ ``\emph{daunting prospect}'' \cite[Page 310]{Norrish11}. While
+ $\lambda$-terms indeed lead to some slick mechanised proofs, our
+ experience is that Turing machines are not too daunting if one is
+ only concerned with formalising the undecidability of the halting
+ problem for Turing machines. As a point of comparison, the halting
+ problem took us around 1500 loc of Isar-proofs, which is just
+ one-and-a-half times of a mechanised proof pearl about the
+ Myhill-Nerode theorem. So our conclusion is that this part is not as
+ daunting as we estimated when reading the paper by Norrish
+ \cite{Norrish11}. The work involved with constructing a universal
+ Turing machine via recursive functions and abacus machines, we
+ agree, is not a project one wants to undertake too many times (our
+ formalisation of abacus machines and their correct translation is
+ approximately 4600 loc; recursive functions 2800 loc and the
+ universal Turing machine 10000 loc).
Our work is also very much inspired by the formalisation of Turing
machines of Asperti and Ricciotti \cite{AspertiRicciotti12} in the
@@ -1738,21 +1732,22 @@
weeks.
Our reasoning about the invariants is not much supported by the
- automation beyond the standard automation tools available in Isabelle/HOL.
- There is however a tantalising connection
- between our work and very recent work by Jensen et al \cite{Jensen13} on verifying
- X86 assembly code that might change that. They observed a similar phenomenon with assembly
- programs where Hoare-style reasoning is sometimes possible, but
- sometimes it is not. In order to ease their reasoning, they
- introduced a more primitive specification logic, on which
- Hoare-rules can be provided for special cases. It remains to be
- seen whether their specification logic for assembly code can make it
- easier to reason about our Turing programs. Myreen ??? That would be an
- attractive result, because Turing machine programs are very much
- like assembly programs and it would connect some very classic work on
- Turing machines to very cutting-edge work on machine code
- verification. In order to try out such ideas, our formalisation provides the
- ``playground''. The code of our formalisation is available from the
+ automation beyond the standard automation tools available in
+ Isabelle/HOL. There is however a tantalising connection between our
+ work and very recent work by Jensen et al \cite{Jensen13} on
+ verifying X86 assembly code that might change that. They observed a
+ similar phenomenon with assembly programs where Hoare-style
+ reasoning is sometimes possible, but sometimes it is not. In order
+ to ease their reasoning, they introduced a more primitive
+ specification logic, on which Hoare-rules can be provided for
+ special cases. It remains to be seen whether their specification
+ logic for assembly code can make it easier to reason about our
+ Turing programs. That would be an attractive result, because Turing
+ machine programs are very much like assembly programs and it would
+ connect some very classic work on Turing machines to very
+ cutting-edge work on machine code verification. In order to try out
+ such ideas, our formalisation provides the ``playground''. The code
+ of our formalisation is available from the
Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}.
\medskip
--- a/Paper/document/root.tex Fri Apr 05 09:18:17 2013 +0100
+++ b/Paper/document/root.tex Mon Apr 22 08:26:16 2013 +0100
@@ -49,7 +49,7 @@
\begin{abstract}
-We present a formalised theory of computability in the theorem prover
+We formalise results from computability theory in the theorem prover
Isabelle/HOL.
%This theorem prover is based on classical logic which
%precludes \emph{direct} reasoning about computability: every boolean
--- a/README Fri Apr 05 09:18:17 2013 +0100
+++ b/README Mon Apr 22 08:26:16 2013 +0100
@@ -26,5 +26,7 @@
Literature - related work
+isabelle build -d . UTM
isabelle make utm -- creates the big session file
+
isabelle make itp -- creates paper
\ No newline at end of file
Binary file paper.pdf has changed
--- a/thys/Rec_Def.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/Rec_Def.thy Mon Apr 22 08:26:16 2013 +0100
@@ -47,4 +47,16 @@
\<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
+inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
+
+inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
+
+inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
+
+inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
+
+inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
+
+inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
+
end
\ No newline at end of file
--- a/thys/Recursive.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/Recursive.thy Mon Apr 22 08:26:16 2013 +0100
@@ -6,6 +6,7 @@
where
"addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
+(* moves register m to register n *)
fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"mv_box m n = [Dec m 3, Inc n, Goto 0]"
@@ -18,7 +19,7 @@
text {* The compilation of @{text "s"}-operator. *}
definition rec_ci_s :: "abc_inst list"
where
- "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
+ "rec_ci_s \<equiv> addition 0 1 2 [+] [Inc 1]"
text {* The compilation of @{text "id i j"}-operator *}
@@ -36,8 +37,7 @@
"empty_boxes 0 = []" |
"empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"
-fun cn_merge_gs ::
- "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+fun cn_merge_gs :: "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"cn_merge_gs [] p = []" |
"cn_merge_gs (g # gs) p =
@@ -91,20 +91,7 @@
declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del]
abc_step_l.simps[simp del]
-inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
-
-inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
-
-inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
-
-inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
-
-inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
-
-inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
-
-fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
- nat list \<Rightarrow> bool"
+fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
where
"addition_inv (as, lm') m n p lm =
(let sn = lm ! n in
@@ -153,21 +140,18 @@
else if as = 4 then 0
else 0)"
-fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow>
- (nat \<times> nat \<times> nat)"
+fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
where
"addition_measure ((as, lm), m, p) =
(addition_stage1 (as, lm) m p,
addition_stage2 (as, lm) m p,
addition_stage3 (as, lm) m p)"
-definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
- ((nat \<times> nat list) \<times> nat \<times> nat)) set"
+definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> ((nat \<times> nat list) \<times> nat \<times> nat)) set"
where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
lemma [simp]: "wf addition_LE"
-by(auto simp: wf_inv_image addition_LE_def lex_triple_def
- lex_pair_def)
+by(auto simp: wf_inv_image addition_LE_def lex_triple_def lex_pair_def)
declare addition_inv.simps[simp del]
@@ -329,12 +313,18 @@
qed
lemma compile_s_correct':
- "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
+ "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything}
+ addition 0 (Suc 0) 2 [+] [Inc (Suc 0)]
+ {\<lambda>nl. nl = n # Suc n # 0 # anything}"
proof(rule_tac abc_Hoare_plus_halt)
- show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 {\<lambda> nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}"
+ show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything}
+ addition 0 (Suc 0) 2
+ {\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}"
by(rule_tac addition_correct, auto simp: numeral_2_eq_2)
next
- show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)} [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
+ show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}
+ [Inc (Suc 0)]
+ {\<lambda>nl. nl = n # Suc n # 0 # anything}"
by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps
abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps)
qed
--- a/thys/UF.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/UF.thy Mon Apr 22 08:26:16 2013 +0100
@@ -152,93 +152,58 @@
Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1)
@ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"
-text {*
- @{text "rec_exec"} is the interpreter function for
- reursive functions. The function is defined such that
- it always returns meaningful results for primitive recursive
- functions.
- *}
declare rec_exec.simps[simp del] constn.simps[simp del]
-text {*
- Correctness of @{text "rec_add"}.
- *}
-lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] = x + y"
+
+section {* Correctness of various recursive functions *}
+
+
+lemma add_lemma: "rec_exec rec_add [x, y] = x + y"
by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-text {*
- Correctness of @{text "rec_mult"}.
- *}
-lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"
+lemma mult_lemma: "rec_exec rec_mult [x, y] = x * y"
by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-text {*
- Correctness of @{text "rec_pred"}.
- *}
-lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] = x - 1"
+lemma pred_lemma: "rec_exec rec_pred [x] = x - 1"
by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
-text {*
- Correctness of @{text "rec_minus"}.
- *}
-lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"
+lemma minus_lemma: "rec_exec rec_minus [x, y] = x - y"
by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
-text {*
- Correctness of @{text "rec_sg"}.
- *}
-lemma sg_lemma: "\<And> x. rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
+lemma sg_lemma: "rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)
-text {*
- Correctness of @{text "constn"}.
- *}
lemma constn_lemma: "rec_exec (constn n) [x] = n"
by(induct n, auto simp: rec_exec.simps constn.simps)
-text {*
- Correctness of @{text "rec_less"}.
- *}
-lemma less_lemma: "\<And> x y. rec_exec rec_less [x, y] =
- (if x < y then 1 else 0)"
+lemma less_lemma: "rec_exec rec_less [x, y] = (if x < y then 1 else 0)"
by(induct_tac y, auto simp: rec_exec.simps
rec_less_def minus_lemma sg_lemma)
-text {*
- Correctness of @{text "rec_not"}.
- *}
-lemma not_lemma:
- "\<And> x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
+lemma not_lemma: "rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
by(induct_tac x, auto simp: rec_exec.simps rec_not_def
constn_lemma minus_lemma)
+lemma eq_lemma: "rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
+by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
+
+lemma conj_lemma: "rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
+
+lemma disj_lemma: "rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
+
+declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
+ minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
+ less_lemma[simp] not_lemma[simp] eq_lemma[simp]
+ conj_lemma[simp] disj_lemma[simp]
+
text {*
- Correctness of @{text "rec_eq"}.
- *}
-lemma eq_lemma: "\<And> x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-
-text {*
- Correctness of @{text "rec_conj"}.
+ @{text "primrec recf n"} is true iff @{text "recf"} is a primitive
+ recursive function with arity @{text "n"}.
*}
-lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0
- else 1)"
-by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
-text {*
- Correctness of @{text "rec_disj"}.
- *}
-lemma disj_lemma: "\<And> x y. rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0
- else 1)"
-by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
-
-
-text {*
- @{text "primrec recf n"} is true iff
- @{text "recf"} is a primitive recursive function
- with arity @{text "n"}.
- *}
+
inductive primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
where
prime_z[intro]: "primerec z (Suc 0)" |
@@ -259,10 +224,7 @@
inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m"
inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m"
-declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
- minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
- less_lemma[simp] not_lemma[simp] eq_lemma[simp]
- conj_lemma[simp] disj_lemma[simp]
+
text {*
@{text "Sigma"} is the logical specification of
@@ -271,17 +233,16 @@
function Sigma :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"
where
"Sigma g xs = (if last xs = 0 then g xs
- else (Sigma g (butlast xs @ [last xs - 1]) +
- g xs)) "
+ else (Sigma g (butlast xs @ [last xs - 1]) + g xs)) "
by pat_completeness auto
+
termination
proof
show "wf (measure (\<lambda> (f, xs). last xs))" by auto
next
fix g xs
assume "last (xs::nat list) \<noteq> 0"
- thus "((g, butlast xs @ [last xs - 1]), g, xs)
- \<in> measure (\<lambda>(f, xs). last xs)"
+ thus "((g, butlast xs @ [last xs - 1]), g, xs) \<in> measure (\<lambda>(f, xs). last xs)"
by auto
qed
@@ -290,25 +251,22 @@
rec_sigma.simps[simp del]
lemma [simp]: "arity z = 1"
- by(simp add: arity.simps)
+ by(simp add: arity.simps)
lemma rec_pr_0_simp_rewrite: "
rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_exec.simps)
+ by(simp add: rec_exec.simps)
lemma rec_pr_0_simp_rewrite_single_param: "
rec_exec (Pr n f g) [0] = rec_exec f []"
-by(simp add: rec_exec.simps)
+ by(simp add: rec_exec.simps)
lemma rec_pr_Suc_simp_rewrite:
- "rec_exec (Pr n f g) (xs @ [Suc x]) =
- rec_exec g (xs @ [x] @
- [rec_exec (Pr n f g) (xs @ [x])])"
+ "rec_exec (Pr n f g) (xs @ [Suc x]) = rec_exec g (xs @ [x] @ [rec_exec (Pr n f g) (xs @ [x])])"
by(simp add: rec_exec.simps)
lemma rec_pr_Suc_simp_rewrite_single_param:
- "rec_exec (Pr n f g) ([Suc x]) =
- rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
+ "rec_exec (Pr n f g) ([Suc x]) = rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
by(simp add: rec_exec.simps)
lemma Sigma_0_simp_rewrite_single_param:
@@ -748,10 +706,9 @@
text {*
The correctness of @{text "rec_Minr"}.
*}
-lemma Minr_lemma: "
- \<lbrakk>primerec rf (Suc (length xs))\<rbrakk>
- \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) =
- Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+lemma Minr_lemma:
+ assumes h: "primerec rf (Suc (length xs))"
+ shows "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
proof -
let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
let ?rf = "(Cn (Suc (Suc (length xs)))
@@ -760,15 +717,13 @@
[recf.id (Suc (Suc (length xs)))
(Suc ((length xs)))])])"
let ?rq = "(rec_all ?rt ?rf)"
- assume h: "primerec rf (Suc (length xs))"
have h1: "primerec ?rq (Suc (length xs))"
apply(rule_tac primerec_all_iff)
apply(auto simp: h nth_append)+
done
moreover have "arity rf = Suc (length xs)"
using h by auto
- ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) =
- Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+ ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def
sigma_lemma all_lemma)
apply(rule_tac sigma_minr_lemma)
@@ -789,7 +744,7 @@
The correctness of @{text "rec_le"}.
*}
lemma le_lemma:
- "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+ "rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
by(auto simp: rec_le_def rec_exec.simps)
text {*
@@ -857,8 +812,7 @@
done
lemma [simp]:
- "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =
- ys @ [ys ! n]"
+ "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) = ys @ [ys ! n]"
apply(simp)
apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)
apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)