246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory UF_Rec
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
2 |
imports Recs Turing_Hoare
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
section {* Universal Function *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
text{* coding of the configuration *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
@{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
numbers encoded by number @{text "sr"} using Godel's coding.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
fun Entry where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
"Entry sr i = Lo sr (Pi (Suc i))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
"rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
lemma entry_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
"rec_eval rec_entry [sr, i] = Entry sr i"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
by(simp add: rec_entry_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
"Listsum2 xs 0 = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
| "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
"rec_listsum2 vl 0 = CN Z [Id vl 0]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
lemma listsum2_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
"length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
by (induct n) (simp_all)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
@{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
B book, but this definition generalises the original one to deal with multiple
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
input arguments.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
"Strt' xs 0 = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
| "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
fun Strt :: "nat list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
"Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
"rec_strt' xs 0 = Z"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
| "rec_strt' xs (Suc n) =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
(let dbound = CN rec_add [rec_listsum2 xs n, constn n] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
let t1 = CN rec_power [constn 2, dbound] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
"rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
fun rec_strt :: "nat \<Rightarrow> recf"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
"rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
lemma strt'_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
"length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
by (induct n) (simp_all add: Let_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
lemma map_suc:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
"map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
proof -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
also have "... = map Suc xs" by (simp add: map_nth)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
86 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
lemma strt_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
"length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
by (simp add: comp_def map_suc[symmetric])
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
91 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
text {* The @{text "Scan"} function on page 90 of B book. *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
fun Scan :: "nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
"Scan r = r mod 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
97 |
definition
|
249
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
"rec_scan = CN rec_mod [Id 1 0, constn 2]"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
lemma scan_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
"rec_eval rec_scan [r] = r mod 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
by(simp add: rec_scan_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
103 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
"Newleft p r a = (if a = 0 \<or> a = 1 then p
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
else if a = 2 then p div 2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
else if a = 3 then 2 * p + r mod 2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
else p)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
"Newright p r a = (if a = 0 then r - Scan r
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
else if a = 1 then r + 1 - Scan r
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
else if a = 2 then 2 * r + p mod 2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
else if a = 3 then r div 2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
else r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
"rec_newleft =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
(let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
let cond2 = CN rec_eq [Id 3 2, constn 2] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
let cond3 = CN rec_eq [Id 3 2, constn 3] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0],
|
249
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
CN rec_mod [Id 3 1, constn 2]] in
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
CN rec_if [cond1, Id 3 0,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
CN rec_if [cond3, case3, Id 3 0]]])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
"rec_newright =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
(let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
137 |
let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],
|
249
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
CN rec_mod [Id 3 0, constn 2]] in
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
139 |
let case3 = CN rec_quo [Id 2 1, constn 2] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
140 |
CN rec_if [condn 0, case0,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
CN rec_if [condn 1, case1,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
CN rec_if [condn 2, case2,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
CN rec_if [condn 3, case3, Id 3 1]]]])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
144 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
145 |
lemma newleft_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
146 |
"rec_eval rec_newleft [p, r, a] = Newleft p r a"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
147 |
by (simp add: rec_newleft_def Let_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
148 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
149 |
lemma newright_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
150 |
"rec_eval rec_newright [p, r, a] = Newright p r a"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
151 |
by (simp add: rec_newright_def Let_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
152 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
153 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
154 |
The @{text "Actn"} function given on page 92 of B book, which is used to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
155 |
fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
156 |
the Goedel coding of a Turing Machine, @{text "q"} is the current state of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
Turing Machine, @{text "r"} is the right number of Turing Machine tape.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
159 |
fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
161 |
"Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
162 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
163 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
"rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
in CN rec_if [Id 3 1, entry, constn 4])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
168 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
169 |
lemma actn_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
170 |
"rec_eval rec_actn [m, q, r] = Actn m q r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
171 |
by (simp add: rec_actn_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
172 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
174 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
"Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
176 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
definition rec_newstat :: "recf"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
179 |
"rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
180 |
let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
181 |
let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
in CN rec_if [Id 3 1, entry, Z])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
lemma newstat_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
185 |
"rec_eval rec_newstat [m, q, r] = Newstat m q r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
186 |
by (simp add: rec_newstat_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
187 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
188 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
189 |
fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
190 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
191 |
"Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
192 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
193 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
194 |
"rec_trpl = CN rec_mult [CN rec_mult
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
195 |
[CN rec_power [constn (Pi 0), Id 3 0],
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
196 |
CN rec_power [constn (Pi 1), Id 3 1]],
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
197 |
CN rec_power [constn (Pi 2), Id 3 2]]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
198 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
199 |
lemma trpl_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
200 |
"rec_eval rec_trpl [p, q, r] = Trpl p q r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
201 |
by (simp add: rec_trpl_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
202 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
203 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
204 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
205 |
fun Left where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
206 |
"Left c = Lo c (Pi 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
207 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
208 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
209 |
"rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
210 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
211 |
lemma left_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
212 |
"rec_eval rec_left [c] = Left c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
213 |
by(simp add: rec_left_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
214 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
215 |
fun Right where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
216 |
"Right c = Lo c (Pi 2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
217 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
218 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
219 |
"rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
220 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
221 |
lemma right_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
222 |
"rec_eval rec_right [c] = Right c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
223 |
by(simp add: rec_right_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
224 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
225 |
fun Stat where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
226 |
"Stat c = Lo c (Pi 1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
227 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
228 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
229 |
"rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
230 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
231 |
lemma stat_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
232 |
"rec_eval rec_stat [c] = Stat c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
233 |
by(simp add: rec_stat_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
234 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
235 |
fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
236 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
237 |
"Inpt m xs = Trpl 0 1 (Strt xs)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
238 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
239 |
fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
240 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
241 |
"Newconf m c = Trpl (Newleft (Left c) (Right c) (Actn m (Stat c) (Right c)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
242 |
(Newstat m (Stat c) (Right c))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
243 |
(Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
244 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
245 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
246 |
"rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
247 |
let left = CN rec_left [Id 2 1] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
248 |
let right = CN rec_right [Id 2 1] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
249 |
let stat = CN rec_stat [Id 2 1] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
250 |
let one = CN rec_newleft [left, right, act] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
251 |
let two = CN rec_newstat [Id 2 0, stat, right] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
252 |
let three = CN rec_newright [left, right, act]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
253 |
in CN rec_trpl [one, two, three])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
254 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
255 |
lemma newconf_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
256 |
"rec_eval rec_newconf [m, c] = Newconf m c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
257 |
by (simp add: rec_newconf_def Let_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
258 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
259 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
260 |
@{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
261 |
of TM coded as @{text "m"} starting from the initial configuration where the left
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
262 |
number equals @{text "0"}, right number equals @{text "r"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
263 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
264 |
fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
265 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
266 |
"Conf 0 m r = Trpl 0 1 r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
267 |
| "Conf (Suc k) m r = Newconf m (Conf k m r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
268 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
269 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
270 |
"rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
271 |
(CN rec_newconf [Id 4 2 , Id 4 1])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
272 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
273 |
lemma conf_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
274 |
"rec_eval rec_conf [k, m, r] = Conf k m r"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
275 |
by(induct k) (simp_all add: rec_conf_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
276 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
277 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
278 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
279 |
@{text "Nstd c"} returns true if the configuration coded
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
280 |
by @{text "c"} is not a stardard final configuration.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
281 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
282 |
fun Nstd :: "nat \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
283 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
284 |
"Nstd c = (Stat c \<noteq> 0 \<or>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
285 |
Left c \<noteq> 0 \<or>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
286 |
Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
287 |
Right c = 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
288 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
289 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
290 |
"rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
291 |
let disj2 = CN rec_noteq [rec_left, constn 0] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
292 |
let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
293 |
let disj3 = CN rec_noteq [rec_right, rhs] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
294 |
let disj4 = CN rec_eq [rec_right, constn 0] in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
295 |
CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
296 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
297 |
lemma nstd_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
298 |
"rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
299 |
by(simp add: rec_nstd_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
300 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
301 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
302 |
text{*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
303 |
@{text "Nostop t m r"} means that afer @{text "t"} steps of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
304 |
execution, the TM coded by @{text "m"} is not at a stardard
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
305 |
final configuration.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
306 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
307 |
fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
308 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
309 |
"Nostop t m r = Nstd (Conf t m r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
310 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
311 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
312 |
"rec_nostop = CN rec_nstd [rec_conf]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
313 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
314 |
lemma nostop_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
315 |
"rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
316 |
by (simp add: rec_nostop_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
317 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
318 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
319 |
fun Value where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
320 |
"Value x = (Lg (Suc x) 2) - 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
321 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
322 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
323 |
"rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
324 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
325 |
lemma value_lemma [simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
326 |
"rec_eval rec_value [x] = Value x"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
327 |
by (simp add: rec_value_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
328 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
329 |
text{*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
330 |
@{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
331 |
to reach a stardard final configuration. This recursive function is the only one
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
332 |
using @{text "Mn"} combinator. So it is the only non-primitive recursive function
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
333 |
needs to be used in the construction of the universal function @{text "rec_uf"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
334 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
335 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
336 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
337 |
"rec_halt = MN rec_nostop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
338 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
339 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
340 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
341 |
"rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
342 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
343 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
344 |
The correctness of @{text "rec_uf"}, nonhalt case.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
345 |
*}
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
346 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
subsection {* Coding function of TMs *}
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
348 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
The purpose of this section is to get the coding function of Turing Machine,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
which is going to be named @{text "code"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
*}
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
353 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
"bl2nat [] n = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
| "bl2nat (Bk # bl) n = bl2nat bl (Suc n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
| "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
fun bl2wc :: "cell list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
"bl2wc xs = bl2nat xs 0"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
363 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
fun trpl_code :: "config \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
"trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
367 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
fun action_map :: "action \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
"action_map W0 = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
| "action_map W1 = 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
| "action_map L = 2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
| "action_map R = 3"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
| "action_map Nop = 4"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
375 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
fun action_map_iff :: "nat \<Rightarrow> action"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
"action_map_iff (0::nat) = W0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
379 |
| "action_map_iff (Suc 0) = W1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
380 |
| "action_map_iff (Suc (Suc 0)) = L"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
381 |
| "action_map_iff (Suc (Suc (Suc 0))) = R"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
| "action_map_iff n = Nop"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
383 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
fun block_map :: "cell \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
"block_map Bk = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
| "block_map Oc = 1"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
388 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
389 |
fun Goedel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
391 |
"Goedel_code' [] n = 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
392 |
| "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) "
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
393 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
394 |
fun Goedel_code :: "nat list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
395 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
396 |
"Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
397 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
398 |
fun modify_tprog :: "instr list \<Rightarrow> nat list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
399 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
"modify_tprog [] = []"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
401 |
| "modify_tprog ((a, s) # nl) = action_map a # s # modify_tprog nl"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
402 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
403 |
text {* @{text "Code tp"} gives the Goedel coding of TM program @{text "tp"}. *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
404 |
fun Code :: "instr list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
405 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
406 |
"Code tp = Goedel_code (modify_tprog tp)"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
407 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
408 |
subsection {* Relating interperter functions to the execution of TMs *}
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
409 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
410 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
411 |
lemma F_correct:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
412 |
assumes tp: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
413 |
and wf: "tm_wf0 tp" "0 < rs"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
414 |
shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
415 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
416 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
417 |
end
|
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
418 |
|