diff --git a/metadata/entries/Universal_Turing_Machine.toml b/metadata/entries/Universal_Turing_Machine.toml
--- a/metadata/entries/Universal_Turing_Machine.toml
+++ b/metadata/entries/Universal_Turing_Machine.toml
@@ -1,66 +1,67 @@
title = "Universal Turing Machine"
date = 2019-02-08
topics = [
"Logic/Computability",
"Computer science/Automata and formal languages",
]
abstract = """
-This entry formalises results from computability theory: recursive functions,
-undecidability of the halting problem, and the existence of a
-universal Turing machine. This formalisation is the AFP entry
+
This entry formalises results from computability theory,
+for example recursive functions,
+undecidability of the halting problem, the existence of a
+universal Turing machine and so on. This formalisation is the AFP entry
corresponding to the paper Mechanising Turing Machines and Computability Theory
-in Isabelle/HOL, ITP 2013. The main book used for this formalisation is
-by Boolos, Burgess, and Jeffrey on Computability and Logic.
+in Isabelle/HOL from ITP 2013. The main book used for this formalisation is
+by Boolos, Burgess, and Jeffrey on Computability and Logic.
-Joosten contributed mainly by making the files ready for the
-AFP. His need for a formalisation of Turing Machines arose from
+Joosten contributed by making the files ready for the
+AFP in 2019. His need for a formalisation of Turing Machines arose from
realising that the current formalisation of saturation graphs
(also in the AFP) was missing a key undecidability result
-present in his paper on Finding models through graph saturation.
+present in his paper on Finding models through graph saturation.
-Regensburger contributed by adding definitions for
+Regensburger contributed in 2022 by adding definitions for
concepts like Turing Decidability, Turing Computability and Turing Reducibility
for problem reduction. He also enhanced the result about the
undecidability of the General Halting Problem given in the original AFP entry
by first proving the undecidability of the Special Halting Problem and then
proving its reducibility to the general problem. The original version of this
AFP entry did only prove a weak form of the undecidability theorem.
The main motivation behind this contribution is to make the AFP entry
-accessible for bachelor and master students.
+accessible for bachelor and master students.
"""
license = "bsd"
note = ""
[authors]
[authors.xu]
[authors.zhangx]
[authors.urban]
homepage = "urban_homepage"
[authors.joosten]
homepage = "joosten_homepage"
[authors.regensburger]
homepage = "regensburger_homepage"
[contributors]
[notify]
joosten = "joosten_email1"
urban = "urban_email"
regensburger = "regensburger_email"
[history]
2019-01-16 = """
Sebastiaan Joosten made the code ready for the AFP.
"""
2022-09-07 = """
Franz Regensburger added substantial material and made some modifications.
"""
[extra]
[related]
diff --git a/thys/Universal_Turing_Machine/Recursive.thy b/thys/Universal_Turing_Machine/Recursive.thy
--- a/thys/Universal_Turing_Machine/Recursive.thy
+++ b/thys/Universal_Turing_Machine/Recursive.thy
@@ -1,2869 +1,2869 @@
(* Title: thys/Recursive.thy
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
Modifications: Sebastiaan Joosten
Modifications: Franz Regensburger (FABR) 08/2022
Added LaTeX sections and comments
*)
section \Compilation of Recursive Functions into Abacus Programs\
theory Recursive
imports Abacus Rec_Def Abacus_Hoare
begin
fun addition :: "nat \ nat \ nat \ abc_prog"
where
"addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
fun mv_box :: "nat \ nat \ abc_prog"
where
"mv_box m n = [Dec m 3, Inc n, Goto 0]"
text \The compilation of \z\-operator.\
definition rec_ci_z :: "abc_inst list"
where
"rec_ci_z \ [Goto 1]"
text \The compilation of \s\-operator.\
definition rec_ci_s :: "abc_inst list"
where
"rec_ci_s \ (addition 0 1 2 [+] [Inc 1])"
text \The compilation of \id i j\-operator\
fun rec_ci_id :: "nat \ nat \ abc_inst list"
where
"rec_ci_id i j = addition j i (i + 1)"
fun mv_boxes :: "nat \ nat \ nat \ abc_inst list"
where
"mv_boxes ab bb 0 = []" |
"mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)"
fun empty_boxes :: "nat \ abc_inst list"
where
"empty_boxes 0 = []" |
"empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"
fun cn_merge_gs ::
"(abc_inst list \ nat \ nat) list \ nat \ abc_inst list"
where
"cn_merge_gs [] p = []" |
"cn_merge_gs (g # gs) p =
(let (gprog, gpara, gn) = g in
gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"
subsection \Definition of the compiler rec\_ci\
text \
The compiler of recursive functions, where \rec_ci recf\ return
\(ap, arity, fp)\, where \ap\ is the Abacus program, \arity\ is the
arity of the recursive function \recf\,
\fp\ is the amount of memory which is going to be
used by \ap\ for its execution.
\
fun rec_ci :: "recf \ abc_inst list \ nat \ nat"
where
"rec_ci z = (rec_ci_z, 1, 2)" |
"rec_ci s = (rec_ci_s, 1, 3)" |
"rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |
"rec_ci (Cn n f gs) =
(let cied_gs = map (\ g. rec_ci g) gs in
let (fprog, fpara, fn) = rec_ci f in
let pstr = Max (set (Suc n # fn # (map (\ (aprog, p, n). n) cied_gs))) in
let qstr = pstr + Suc (length gs) in
(cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+]
mv_boxes pstr 0 (length gs) [+] fprog [+]
mv_box fpara pstr [+] empty_boxes (length gs) [+]
mv_box pstr n [+] mv_boxes qstr 0 n, n, qstr + n))" |
"rec_ci (Pr n f g) =
(let (fprog, fpara, fn) = rec_ci f in
let (gprog, gpara, gn) = rec_ci g in
let p = Max (set ([n + 3, fn, gn])) in
let e = length gprog + 7 in
(mv_box n p [+] fprog [+] mv_box n (Suc n) [+]
(([Dec p e] [+] gprog [+]
[Inc n, Dec (Suc n) 3, Goto 1]) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),
Suc n, p + 1))" |
"rec_ci (Mn n f) =
(let (fprog, fpara, fn) = rec_ci f in
let len = length (fprog) in
(fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"
subsection \Correctness of the compiler rec\_ci\
declare rec_ci.simps [simp del] rec_ci_s_def[simp del]
rec_ci_z_def[simp del] rec_ci_id.simps[simp del]
mv_boxes.simps[simp del]
mv_box.simps[simp del] addition.simps[simp del]
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 \ nat list \ nat \ nat \ nat \
nat list \ bool"
where
"addition_inv (as, lm') m n p lm =
(let sn = lm ! n in
let sm = lm ! m in
lm ! p = 0 \
(if as = 0 then \ x. x \ lm ! m \ lm' = lm[m := x,
n := (sn + sm - x), p := (sm - x)]
else if as = 1 then \ x. x < lm ! m \ lm' = lm[m := x,
n := (sn + sm - x - 1), p := (sm - x - 1)]
else if as = 2 then \ x. x < lm ! m \ lm' = lm[m := x,
n := (sn + sm - x), p := (sm - x - 1)]
else if as = 3 then \ x. x < lm ! m \ lm' = lm[m := x,
n := (sn + sm - x), p := (sm - x)]
else if as = 4 then \ x. x \ lm ! m \ lm' = lm[m := x,
n := (sn + sm), p := (sm - x)]
else if as = 5 then \ x. x < lm ! m \ lm' = lm[m := x,
n := (sn + sm), p := (sm - x - 1)]
else if as = 6 then \ x. x < lm ! m \ lm' =
lm[m := Suc x, n := (sn + sm), p := (sm - x - 1)]
else if as = 7 then lm' = lm[m := sm, n := (sn + sm)]
else False))"
fun addition_stage1 :: "nat \ nat list \ nat \ nat \ nat"
where
"addition_stage1 (as, lm) m p =
(if as = 0 \ as = 1 \ as = 2 \ as = 3 then 2
else if as = 4 \ as = 5 \ as = 6 then 1
else 0)"
fun addition_stage2 :: "nat \ nat list \ nat \ nat \ nat"
where
"addition_stage2 (as, lm) m p =
(if 0 \ as \ as \ 3 then lm ! m
else if 4 \ as \ as \ 6 then lm ! p
else 0)"
fun addition_stage3 :: "nat \ nat list \ nat \ nat \ nat"
where
"addition_stage3 (as, lm) m p =
(if as = 1 then 4
else if as = 2 then 3
else if as = 3 then 2
else if as = 0 then 1
else if as = 5 then 2
else if as = 6 then 1
else if as = 4 then 0
else 0)"
fun addition_measure :: "((nat \ nat list) \ nat \ nat) \
(nat \ nat \ 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 \ nat list) \ nat \ nat) \
((nat \ nat list) \ nat \ nat)) set"
where "addition_LE \ (inv_image lex_triple addition_measure)"
lemma wf_additon_LE[simp]: "wf addition_LE"
by(auto simp: addition_LE_def lex_triple_def lex_pair_def)
declare addition_inv.simps[simp del]
lemma update_zero_to_zero[simp]: "\am ! n = (0::nat); n < length am\ \ am[n := 0] = am"
apply(simp add: list_update_same_conv)
done
lemma addition_inv_init:
"\m \ n; max m n < p; length lm > p; lm ! p = 0\ \
addition_inv (0, lm) m n p lm"
apply(simp add: addition_inv.simps Let_def )
apply(rule_tac x = "lm ! m" in exI, simp)
done
lemma abs_fetch[simp]:
"abc_fetch 0 (addition m n p) = Some (Dec m 4)"
"abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
"abc_fetch 2 (addition m n p) = Some (Inc p)"
"abc_fetch 3 (addition m n p) = Some (Goto 0)"
"abc_fetch 4 (addition m n p) = Some (Dec p 7)"
"abc_fetch 5 (addition m n p) = Some (Inc m)"
"abc_fetch 6 (addition m n p) = Some (Goto 4)"
by(simp_all add: abc_fetch.simps addition.simps)
lemma exists_small_list_elem1[simp]:
"\m \ n; p < length lm; lm ! p = 0; m < p; n < p; x \ lm ! m; 0 < x\
\ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\
\ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\
\ \xam \ n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\
\ \xa\lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
p := lm ! m - x] =
lm[m := xa, n := lm ! n + lm ! m - xa,
p := lm ! m - xa]"
apply(rule_tac x = x in exI, simp)
done
lemma exists_small_list_elem5[simp]:
"\m \ n; p < length lm; lm ! p = 0; m < p; n < p;
x \ lm ! m; lm ! m \ x\
\ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\
\ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\
\ \xa\lm ! m. lm[m := Suc x, n := lm ! n + lm ! m,
p := lm ! m - Suc x]
= lm[m := xa, n := lm ! n + lm ! m, p := lm ! m - xa]"
apply(rule_tac x = "Suc x" in exI, simp)
done
lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm"
apply(cases asm, simp add: abc_steps_l.simps)
done
lemma list_double_update_2:
"lm[a := x, b := y, a := z] = lm[b := y, a:=z]"
by (metis list_update_overwrite list_update_swap)
declare Let_def[simp]
lemma addition_halt_lemma:
"\m \ n; max m n < p; length lm > p\ \
\na. \ (\(as, lm') (m, p). as = 7)
(abc_steps_l (0, lm) (addition m n p) na) (m, p) \
addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm
\ addition_inv (abc_steps_l (0, lm) (addition m n p)
(Suc na)) m n p lm
\ ((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p),
abc_steps_l (0, lm) (addition m n p) na, m, p) \ addition_LE"
proof -
assume assms_1: "m\n" and assms_2: "max m n < p" and assms_3: "length lm > p"
{ fix na
obtain a b where ab:"abc_steps_l (0, lm) (addition m n p) na = (a, b)" by force
assume assms2: "\ (\(as, lm') (m, p). as = 7)
(abc_steps_l (0, lm) (addition m n p) na) (m, p)"
"addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm"
have r1:"addition_inv (abc_steps_l (0, lm) (addition m n p)
(Suc na)) m n p lm" using assms_1 assms_2 assms_3 assms2
unfolding abc_step_red2 ab abc_step_l.simps abc_lm_v.simps abc_lm_s.simps
addition_inv.simps
by (auto split:if_splits simp add: addition_inv.simps Suc_diff_Suc)
have r2:"((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p),
abc_steps_l (0, lm) (addition m n p) na, m, p) \ addition_LE" using assms_1 assms_2 assms_3 assms2
unfolding abc_step_red2 ab
apply(auto split:if_splits simp add: addition_inv.simps abc_steps_zero)
by(auto simp add: addition_LE_def lex_triple_def lex_pair_def
abc_step_l.simps abc_lm_v.simps abc_lm_s.simps split: if_splits)
note r1 r2
}
thus ?thesis by auto
qed
lemma addition_correct':
"\m \ n; max m n < p; length lm > p; lm ! p = 0\ \
\ stp. (\ (as, lm'). as = 7 \ addition_inv (as, lm') m n p lm)
(abc_steps_l (0, lm) (addition m n p) stp)"
apply(insert halt_lemma2[of addition_LE
"\ ((as, lm'), m, p). addition_inv (as, lm') m n p lm"
"\ stp. (abc_steps_l (0, lm) (addition m n p) stp, m, p)"
"\ ((as, lm'), m, p). as = 7"],
simp add: abc_steps_zero addition_inv_init)
apply(drule_tac addition_halt_lemma,force,force)
apply (simp,erule_tac exE)
apply(rename_tac na)
apply(rule_tac x = na in exI)
apply(auto)
done
lemma length_addition[simp]: "length (addition a b c) = 7"
by(auto simp: addition.simps)
lemma addition_correct:
assumes "m \ n" "max m n < p" "length lm > p" "lm ! p = 0"
shows "\\ a. a = lm\ (addition m n p) \\ nl. addition_inv (7, nl) m n p lm\"
using assms
proof(rule_tac abc_Hoare_haltI, simp)
fix lma
assume "m \ n" "m < p \ n < p" "p < length lm" "lm ! p = 0"
then have "\ stp. (\ (as, lm'). as = 7 \ addition_inv (as, lm') m n p lm)
(abc_steps_l (0, lm) (addition m n p) stp)"
by(rule_tac addition_correct', auto simp: addition_inv.simps)
then obtain stp where "(\ (as, lm'). as = 7 \ addition_inv (as, lm') m n p lm)
(abc_steps_l (0, lm) (addition m n p) stp)"
using exE by presburger
thus "\na. abc_final (abc_steps_l (0, lm) (addition m n p) na) (addition m n p) \
(\nl. addition_inv (7, nl) m n p lm) abc_holds_for abc_steps_l (0, lm) (addition m n p) na"
by(auto intro:exI[of _ stp])
qed
subsubsection \Correctness of compilation for constructor s\
lemma compile_s_correct':
"\\nl. nl = n # 0 \ 2 @ anything\ addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] \\nl. nl = n # Suc n # 0 # anything\"
proof(rule_tac abc_Hoare_plus_halt)
show "\\nl. nl = n # 0 \ 2 @ anything\ addition 0 (Suc 0) 2 \\ nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)\"
by(rule_tac addition_correct, auto simp: numeral_2_eq_2)
next
show "\\nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \ 2 @ anything)\ [Inc (Suc 0)] \\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
declare rec_exec.simps[simp del]
lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)"
apply(auto simp: abc_comp.simps abc_shift.simps)
apply(rename_tac x)
apply(case_tac x, auto)
done
lemma compile_s_correct:
"\rec_ci s = (ap, arity, fp); rec_exec s [n] = r\ \
\\nl. nl = n # 0 \ (fp - arity) @ anything\ ap \\nl. nl = n # r # 0 \ (fp - Suc arity) @ anything\"
apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_exec.simps)
done
subsubsection \Correctness of compilation for constructor z\
lemma compile_z_correct:
"\rec_ci z = (ap, arity, fp); rec_exec z [n] = r\ \
\\nl. nl = n # 0 \ (fp - arity) @ anything\ ap \\nl. nl = n # r # 0 \ (fp - Suc arity) @ anything\"
apply(rule_tac abc_Hoare_haltI)
apply(rule_tac x = 1 in exI)
apply(auto simp: abc_steps_l.simps rec_ci.simps rec_ci_z_def
numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_exec.simps)
done
subsubsection \