168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1 |
(* Title: thys/Turing.thy
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
2 |
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
|
292
293e9c6f22e1
Added myself to the comments at the start of all files
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
3 |
Modifications: Sebastiaan Joosten
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
4 |
*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
5 |
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
6 |
chapter {* Turing Machines *}
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
|
163
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
theory Turing
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
imports Main
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
section {* Basic definitions of Turing machine *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
datatype action = W0 | W1 | L | R | Nop
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
datatype cell = Bk | Oc
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
type_synonym tape = "cell list \<times> cell list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
type_synonym state = nat
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
type_synonym instr = "action \<times> state"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
type_synonym tprog = "instr list \<times> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
|
54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
type_synonym tprog0 = "instr list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
type_synonym config = "state \<times> tape"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
fun nth_of where
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
"nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
lemma nth_of_map [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
shows "nth_of (map f p) n = (case (nth_of p n) of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
apply(induct p arbitrary: n)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
apply(case_tac n)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
fetch :: "instr list \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
"fetch p 0 b = (Nop, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
| "fetch p (Suc s) Bk =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
(case nth_of p (2 * s) of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
Some i \<Rightarrow> i
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
| None \<Rightarrow> (Nop, 0))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
|"fetch p (Suc s) Oc =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
(case nth_of p ((2 * s) + 1) of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
Some i \<Rightarrow> i
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
| None \<Rightarrow> (Nop, 0))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
lemma fetch_Nil [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
shows "fetch [] s b = (Nop, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
apply(case_tac s)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
apply(case_tac b)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
update :: "action \<Rightarrow> tape \<Rightarrow> tape"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
"update W0 (l, r) = (l, Bk # (tl r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
| "update W1 (l, r) = (l, Oc # (tl r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
| "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
| "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
| "update Nop (l, r) = (l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
71 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
"read r == if (r = []) then Bk else hd r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
fun step :: "config \<Rightarrow> tprog \<Rightarrow> config"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
76 |
"step (s, l, r) (p, off) =
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
(let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
"step0 c p \<equiv> step c (p, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
83 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
"steps c p 0 = c" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
"steps c p (Suc n) = steps (step c p) p n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
|
54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
"steps0 c p n \<equiv> steps c (p, 0) n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
lemma step_red [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
shows "steps c p (Suc n) = step (steps c p n) p"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
by (induct n arbitrary: c) (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
lemma steps_add [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
shows "steps c p (m + n) = steps (steps c p m) p n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
by (induct m arbitrary: c) (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
lemma step_0 [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
shows "step (0, (l, r)) p = (0, (l, r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
by (case_tac p, simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
lemma steps_0 [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
shows "steps (0, (l, r)) p n = (0, (l, r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
by (induct n) (simp_all)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
is_final :: "config \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
"is_final (s, l, r) = (s = 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
lemma is_final_eq:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
shows "is_final (s, tp) = (s = 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
by (case_tac tp) (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
|
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
115 |
lemma is_finalI [intro]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
shows "is_final (0, tp)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
by (simp add: is_final_eq)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
lemma after_is_final:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
assumes "is_final c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
shows "is_final (steps c p n)"
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
using assms
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
123 |
apply(induct n)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
apply(case_tac [!] c)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
125 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
done
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
|
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
128 |
lemma is_final:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
assumes a: "is_final (steps c p n1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
and b: "n1 \<le> n2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
shows "is_final (steps c p n2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
proof -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
obtain n3 where eq: "n2 = n1 + n3" using b by (metis le_iff_add)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
134 |
from a show "is_final (steps c p n2)" unfolding eq
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
by (simp add: after_is_final)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
136 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
lemma not_is_final:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
assumes a: "\<not> is_final (steps c p n1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
and b: "n2 \<le> n1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
shows "\<not> is_final (steps c p n2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
proof (rule notI)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
assume "is_final (steps c p n2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
then have "is_final (steps c p n1)" unfolding eq
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
by (simp add: after_is_final)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
with a show "False" by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
qed
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
149 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
(* if the machine is in the halting state, there must have
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
been a state just before the halting state *)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
lemma before_final:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
assumes "steps0 (1, tp) A n = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
using assms
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
proof(induct n arbitrary: tp')
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
157 |
case (0 tp')
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
next
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
case (Suc n tp')
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
by (auto intro: is_final.cases)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
proof (cases "s = 0")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
case True (* in halting state *)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
then have "steps0 (1, tp) A n = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
using asm cases by (simp del: steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
then show ?thesis using ih by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
next
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
175 |
case False (* not in halting state *)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
176 |
then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
177 |
using asm cases by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
178 |
then show ?thesis by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
179 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
180 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
181 |
|
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
182 |
lemma least_steps:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
183 |
assumes "steps0 (1, tp) A n = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
shows "\<exists> n'. (\<forall>n'' < n'. \<not> is_final (steps0 (1, tp) A n'')) \<and>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
(\<forall>n'' \<ge> n'. is_final (steps0 (1, tp) A n''))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
186 |
proof -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
187 |
from before_final[OF assms]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
obtain n' where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
189 |
before: "\<not> is_final (steps0 (1, tp) A n')" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
190 |
final: "steps0 (1, tp) A (Suc n') = (0, tp')" by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
from before
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
192 |
have "\<forall>n'' < Suc n'. \<not> is_final (steps0 (1, tp) A n'')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
193 |
using not_is_final by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
moreover
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
from final
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
have "\<forall>n'' \<ge> Suc n'. is_final (steps0 (1, tp) A n'')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
197 |
using is_final[of _ _ "Suc n'"] by (auto simp add: is_final_eq)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
ultimately
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
show "\<exists> n'. (\<forall>n'' < n'. \<not> is_final (steps0 (1, tp) A n'')) \<and> (\<forall>n'' \<ge> n'. is_final (steps0 (1, tp) A n''))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
by blast
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
(* well-formedness of Turing machine programs *)
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
206 |
abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
tm_wf :: "tprog \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
where
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
211 |
"tm_wf (p, off) = (length p \<ge> 2 \<and> is_even (length p) \<and>
|
54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
(\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
"tm_wf0 p \<equiv> tm_wf (p, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
where "x \<up> n == replicate n x"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
220 |
class tape =
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
221 |
fixes tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)
|
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
|
47
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
224 |
instantiation nat::tape begin
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
225 |
definition tape_of_nat where "tape_of_nat (n::nat) \<equiv> Oc \<up> (Suc n)"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
226 |
instance by standard
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
227 |
end
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
228 |
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
229 |
type_synonym nat_list = "nat list"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
230 |
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
231 |
instantiation list::(tape) tape begin
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
232 |
fun tape_of_nat_list :: "('a::tape) list \<Rightarrow> cell list"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
233 |
where
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
234 |
"tape_of_nat_list [] = []" |
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
235 |
"tape_of_nat_list [n] = <n>" |
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
236 |
"tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
237 |
definition tape_of_list where "tape_of_list \<equiv> tape_of_nat_list"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
238 |
instance by standard
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
239 |
end
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
240 |
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
241 |
instantiation prod:: (tape, tape) tape begin
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
242 |
fun tape_of_nat_prod :: "('a::tape) \<times> ('b::tape) \<Rightarrow> cell list"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
243 |
where "tape_of_nat_prod (n, m) = <n> @ [Bk] @ <m>"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
244 |
definition tape_of_prod where "tape_of_prod \<equiv> tape_of_nat_prod"
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
245 |
instance by standard
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
246 |
end
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
248 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
249 |
shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
250 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
251 |
"shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
252 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
253 |
fun
|
190
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
254 |
adjust :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
255 |
where
|
190
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
256 |
"adjust p e = map (\<lambda> (a, s). (a, if s = 0 then e else s)) p"
|
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
|
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
abbreviation
|
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
"adjust0 p \<equiv> adjust p (Suc (length p div 2))"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
|
54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
lemma length_shift [simp]:
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
shows "length (shift p n) = length p"
|
54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
263 |
by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
264 |
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
265 |
lemma length_adjust [simp]:
|
190
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
shows "length (adjust p n) = length p"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
by (induct p) (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
(* composition of two Turing machines *)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
271 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
272 |
tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
where
|
190
f1ecb4a68a54
renamed sete definition to adjust and old special case of adjust to adjust0
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
"tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
276 |
lemma tm_comp_length:
|
54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
277 |
shows "length (A |+| B) = length A + length B"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
278 |
by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
279 |
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
280 |
lemma tm_comp_wf[intro]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
281 |
"\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
282 |
by (fastforce)
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
283 |
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
284 |
lemma tm_comp_step:
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
assumes unfinal: "\<not> is_final (step0 c A)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
286 |
shows "step0 c (A |+| B) = step0 c A"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
287 |
proof -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
288 |
obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
have "\<not> is_final (step0 (s, l, r) A)" using unfinal eq by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
290 |
then have "case (fetch A s (read r)) of (a, s) \<Rightarrow> s \<noteq> 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
291 |
by (auto simp add: is_final_eq)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
292 |
then have "fetch (A |+| B) s (read r) = fetch A s (read r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
293 |
apply(case_tac [!] "read r")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
294 |
apply(case_tac [!] s)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
apply(auto simp: tm_comp_length nth_append)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
then show "step0 c (A |+| B) = step0 c A" by (simp add: eq)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
298 |
qed
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
299 |
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
300 |
lemma tm_comp_steps:
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
301 |
assumes "\<not> is_final (steps0 c A n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
302 |
shows "steps0 c (A |+| B) n = steps0 c A n"
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
303 |
using assms
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
304 |
proof(induct n)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
305 |
case 0
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
306 |
then show "steps0 c (A |+| B) 0 = steps0 c A 0" by auto
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
307 |
next
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
308 |
case (Suc n)
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
309 |
have ih: "\<not> is_final (steps0 c A n) \<Longrightarrow> steps0 c (A |+| B) n = steps0 c A n" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
310 |
have fin: "\<not> is_final (steps0 c A (Suc n))" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
then have fin1: "\<not> is_final (step0 (steps0 c A n) A)"
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
312 |
by (auto simp only: step_red)
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
then have fin2: "\<not> is_final (steps0 c A n)"
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
314 |
by (metis is_final_eq step_0 surj_pair)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)"
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
317 |
by (simp only: step_red)
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
318 |
also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2])
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1])
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
320 |
finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)"
|
58
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
by (simp only: step_red)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
322 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
323 |
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
324 |
lemma tm_comp_fetch_in_A:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
325 |
assumes h1: "fetch A s x = (a, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
and h2: "s \<le> length A div 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
327 |
and h3: "s \<noteq> 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
328 |
shows "fetch (A |+| B) s x = (a, Suc (length A div 2))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
using h1 h2 h3
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
apply(case_tac s)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
331 |
apply(case_tac [!] x)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
332 |
apply(auto simp: tm_comp_length nth_append)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
333 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
lemma tm_comp_exec_after_first:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
336 |
assumes h1: "\<not> is_final c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
337 |
and h2: "step0 c A = (0, tp)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
338 |
and h3: "fst c \<le> length A div 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
339 |
shows "step0 c (A |+| B) = (Suc (length A div 2), tp)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
340 |
using h1 h2 h3
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
341 |
apply(case_tac c)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
342 |
apply(auto simp del: tm_comp.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
343 |
apply(case_tac "fetch A a Bk")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
344 |
apply(simp del: tm_comp.simps)
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
345 |
apply(subst tm_comp_fetch_in_A;force)
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
346 |
apply(case_tac "fetch A a (hd ca)")
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
apply(simp del: tm_comp.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
apply(subst tm_comp_fetch_in_A)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
apply(auto)[4]
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
lemma step_in_range:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
assumes h1: "\<not> is_final (step0 c A)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
and h2: "tm_wf (A, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
shows "fst (step0 c A) \<le> length A div 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
using h1 h2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
apply(case_tac c)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
apply(case_tac a)
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
359 |
apply(auto simp add: Let_def case_prod_beta')
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
360 |
apply(case_tac "hd ca")
|
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
361 |
apply(auto simp add: case_prod_beta')
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
363 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
lemma steps_in_range:
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
assumes h1: "\<not> is_final (steps0 (1, tp) A stp)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
and h2: "tm_wf (A, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
367 |
shows "fst (steps0 (1, tp) A stp) \<le> length A div 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
using h1
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
proof(induct stp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
case 0
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
then show "fst (steps0 (1, tp) A 0) \<le> length A div 2" using h2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
by (auto simp add: steps.simps tm_wf.simps)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
next
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
case (Suc stp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
375 |
have ih: "\<not> is_final (steps0 (1, tp) A stp) \<Longrightarrow> fst (steps0 (1, tp) A stp) \<le> length A div 2" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
have h: "\<not> is_final (steps0 (1, tp) A (Suc stp))" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) \<le> length A div 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
by (metis step_in_range step_red)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
379 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
380 |
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
381 |
(* if A goes into the final state, then A |+| B will go into the first state of B *)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
lemma tm_comp_next:
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
383 |
assumes a_ht: "steps0 (1, tp) A n = (0, tp')"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
and a_wf: "tm_wf (A, 0)"
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')"
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
proof -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis"
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
388 |
obtain stp' where fin: "\<not> is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
389 |
using before_final[OF a_ht] by blast
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'"
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
391 |
by (rule tm_comp_steps)
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
392 |
from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
393 |
by (simp only: step_red)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
394 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
395 |
have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
396 |
by (simp only: step_red)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
397 |
also have "... = step0 (steps0 (1, tp) A stp') (A |+| B)" using h1 by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
398 |
also have "... = (Suc (length A div 2), tp')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
399 |
by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]])
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
finally show thesis using a by blast
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
401 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
402 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
403 |
lemma tm_comp_fetch_second_zero:
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
404 |
assumes h1: "fetch B s x = (a, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
405 |
and hs: "tm_wf (A, 0)" "s \<noteq> 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
406 |
shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
407 |
using h1 hs
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
408 |
apply(case_tac x)
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
409 |
apply(case_tac [!] s)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
410 |
apply(auto simp: tm_comp_length nth_append)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
411 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
412 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
413 |
lemma tm_comp_fetch_second_inst:
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
414 |
assumes h1: "fetch B sa x = (a, s)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
415 |
and hs: "tm_wf (A, 0)" "sa \<noteq> 0" "s \<noteq> 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
416 |
shows "fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
417 |
using h1 hs
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
418 |
apply(case_tac x)
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
419 |
apply(case_tac [!] sa)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
420 |
apply(auto simp: tm_comp_length nth_append)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
421 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
422 |
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
423 |
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
424 |
lemma tm_comp_second:
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
425 |
assumes a_wf: "tm_wf (A, 0)"
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
426 |
and steps: "steps0 (1, l, r) B stp = (s', l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
427 |
shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
428 |
= (if s' = 0 then 0 else s' + length A div 2, l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
429 |
using steps
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
430 |
proof(induct stp arbitrary: s' l' r')
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
431 |
case 0
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
432 |
then show ?case by (simp add: steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
433 |
next
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
434 |
case (Suc stp s' l' r')
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
435 |
obtain s'' l'' r'' where a: "steps0 (1, l, r) B stp = (s'', l'', r'')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
436 |
by (metis is_final.cases)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
437 |
then have ih1: "s'' = 0 \<Longrightarrow> steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l'', r'')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
438 |
and ih2: "s'' \<noteq> 0 \<Longrightarrow> steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (s'' + length A div 2, l'', r'')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
439 |
using Suc by (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
440 |
have h: "steps0 (1, l, r) B (Suc stp) = (s', l', r')" by fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
441 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
442 |
{ assume "s'' = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
443 |
then have ?case using a h ih1 by (simp del: steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
444 |
} moreover
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
445 |
{ assume as: "s'' \<noteq> 0" "s' = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
446 |
from as a h
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
447 |
have "step0 (s'', l'', r'') B = (0, l', r')" by (simp del: steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
448 |
with as have ?case
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
449 |
apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
450 |
apply(case_tac "fetch B s'' (read r'')")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
451 |
apply(auto simp add: tm_comp_fetch_second_zero[OF _ a_wf] simp del: tm_comp.simps)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
452 |
done
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
453 |
} moreover
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
454 |
{ assume as: "s'' \<noteq> 0" "s' \<noteq> 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
455 |
from as a h
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
456 |
have "step0 (s'', l'', r'') B = (s', l', r')" by (simp del: steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
457 |
with as have ?case
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
458 |
apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
459 |
apply(case_tac "fetch B s'' (read r'')")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
460 |
apply(auto simp add: tm_comp_fetch_second_inst[OF _ a_wf as] simp del: tm_comp.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
461 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
462 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
463 |
ultimately show ?case by blast
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
464 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
465 |
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
466 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
467 |
lemma tm_comp_final:
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
468 |
assumes "tm_wf (A, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
469 |
and "steps0 (1, l, r) B stp = (0, l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
470 |
shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')"
|
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
471 |
using tm_comp_second[OF assms] by (simp)
|
43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
472 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
473 |
end
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
474 |
|