1 theory UF_Rec |
1 theory UF_Rec |
2 imports Recs Turing_Hoare |
2 imports Recs Turing2 |
3 begin |
3 begin |
4 |
4 |
5 |
5 section {* Coding of Turing Machines and tapes*} |
|
6 |
|
7 text {* |
|
8 The purpose of this section is to construct the coding function of Turing |
|
9 Machine, which is going to be named @{text "code"}. *} |
|
10 |
|
11 text {* Encoding of actions as numbers *} |
|
12 |
|
13 fun action_num :: "action \<Rightarrow> nat" |
|
14 where |
|
15 "action_num W0 = 0" |
|
16 | "action_num W1 = 1" |
|
17 | "action_num L = 2" |
|
18 | "action_num R = 3" |
|
19 | "action_num Nop = 4" |
|
20 |
|
21 fun cell_num :: "cell \<Rightarrow> nat" where |
|
22 "cell_num Bk = 0" |
|
23 | "cell_num Oc = 1" |
|
24 |
|
25 fun code_tp :: "cell list \<Rightarrow> nat list" |
|
26 where |
|
27 "code_tp [] = []" |
|
28 | "code_tp (c # tp) = (cell_num c) # code_tp tp" |
|
29 |
|
30 fun Code_tp where |
|
31 "Code_tp tp = lenc (code_tp tp)" |
|
32 |
|
33 fun Code_conf where |
|
34 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)" |
|
35 |
|
36 fun code_instr :: "instr \<Rightarrow> nat" where |
|
37 "code_instr i = penc (action_num (fst i)) (snd i)" |
|
38 |
|
39 fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where |
|
40 "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))" |
|
41 |
|
42 fun code_tprog :: "tprog \<Rightarrow> nat list" |
|
43 where |
|
44 "code_tprog [] = []" |
|
45 | "code_tprog (i # tm) = Code_instr i # code_tprog tm" |
|
46 |
|
47 lemma code_tprog_length [simp]: |
|
48 "length (code_tprog tp) = length tp" |
|
49 by (induct tp) (simp_all) |
|
50 |
|
51 lemma code_tprog_nth [simp]: |
|
52 "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)" |
|
53 by (induct tp arbitrary: n) (simp_all add: nth_Cons') |
|
54 |
|
55 fun Code_tprog :: "tprog \<Rightarrow> nat" |
|
56 where |
|
57 "Code_tprog tm = lenc (code_tprog tm)" |
6 |
58 |
7 section {* Universal Function in HOL *} |
59 section {* Universal Function in HOL *} |
8 |
60 |
9 text {* |
61 |
10 @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural |
62 text {* Scanning and writing the right tape *} |
11 numbers encoded by number @{text "sr"} using Godel's coding. |
63 |
12 *} |
64 fun Scan where |
13 fun Entry where |
65 "Scan r = ldec r 0" |
14 "Entry sr i = Lo sr (Pi (Suc i))" |
66 |
15 |
67 fun Write where |
16 fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat" |
68 "Write n r = penc n (pdec2 r)" |
17 where |
69 |
18 "Listsum2 xs 0 = 0" |
70 text {* |
19 | "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n" |
71 The @{text Newleft} and @{text Newright} functions on page 91 of B book. |
20 |
72 They calculate the new left and right tape (@{text p} and @{text r}) according |
21 text {* |
73 to an action @{text a}. |
22 @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the |
74 *} |
23 B book, but this definition generalises the original one in order to deal |
|
24 with multiple input arguments. *} |
|
25 |
|
26 fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat" |
|
27 where |
|
28 "Strt' xs 0 = 0" |
|
29 | "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n |
|
30 in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))" |
|
31 |
|
32 fun Strt :: "nat list \<Rightarrow> nat" |
|
33 where |
|
34 "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))" |
|
35 |
|
36 text {* The @{text "Scan"} function on page 90 of B book. *} |
|
37 fun Scan :: "nat \<Rightarrow> nat" |
|
38 where |
|
39 "Scan r = r mod 2" |
|
40 |
|
41 text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *} |
|
42 |
75 |
43 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
76 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
44 where |
77 where |
45 "Newleft p r a = (if a = 0 \<or> a = 1 then p |
78 "Newleft p r a = (if a = 0 \<or> a = 1 then p else |
46 else if a = 2 then p div 2 |
79 if a = 2 then pdec2 p else |
47 else if a = 3 then 2 * p + r mod 2 |
80 if a = 3 then penc (pdec1 r) p |
48 else p)" |
81 else p)" |
49 |
82 |
50 fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
83 fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
51 where |
84 where |
52 "Newright p r a = (if a = 0 then r - Scan r |
85 "Newright p r a = (if a = 0 then Write 0 r |
53 else if a = 1 then r + 1 - Scan r |
86 else if a = 1 then Write 1 r |
54 else if a = 2 then 2 * r + p mod 2 |
87 else if a = 2 then penc (pdec1 p) r |
55 else if a = 3 then r div 2 |
88 else if a = 3 then pdec2 r |
56 else r)" |
89 else r)" |
57 |
90 |
58 text {* |
91 text {* |
59 The @{text "Actn"} function given on page 92 of B book, which is used to |
92 The @{text "Actn"} function given on page 92 of B book, which is used to |
60 fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is |
93 fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is |
61 the Goedel coding of a Turing Machine, @{text "q"} is the current state of |
94 the code of the Turing Machine, @{text "q"} is the current state of |
62 Turing Machine, @{text "r"} is the right number of Turing Machine tape. *} |
95 Turing Machine, and @{text "r"} is the scanned cell of is the right tape. |
|
96 *} |
|
97 |
|
98 fun actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
99 "actn n 0 = pdec1 (pdec1 n)" |
|
100 | "actn n _ = pdec1 (pdec2 n)" |
63 |
101 |
64 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
102 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
65 where |
103 where |
66 "Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)" |
104 "Actn m q r = (if q \<noteq> 0 \<and> within m q then (actn (ldec m (q - 1)) r) else 4)" |
|
105 |
|
106 fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
107 "newstat n 0 = pdec2 (pdec1 n)" |
|
108 | "newstat n _ = pdec2 (pdec2 n)" |
67 |
109 |
68 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
110 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
69 where |
111 where |
70 "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)" |
112 "Newstat m q r = (if q \<noteq> 0 then (newstat (ldec m (q - 1)) r) else 0)" |
71 |
113 |
72 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
114 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat" |
73 where |
115 where |
74 "Trpl p q r = list_encode [p, q, r]" |
116 "Conf (q, (l, r)) = lenc [q, l, r]" |
|
117 |
|
118 fun Stat where |
|
119 (*"Stat c = (if c = 0 then 0 else ldec c 0)"*) |
|
120 "Stat c = ldec c 0" |
75 |
121 |
76 fun Left where |
122 fun Left where |
77 "Left c = list_decode c ! 0" |
123 "Left c = ldec c 1" |
78 |
124 |
79 fun Right where |
125 fun Right where |
80 "Right c = list_decode c ! 1" |
126 "Right c = ldec c 2" |
81 |
|
82 fun Stat where |
|
83 "Stat c = list_decode c ! 2" |
|
84 |
|
85 lemma mod_dvd_simp: |
|
86 "(x mod y = (0::nat)) = (y dvd x)" |
|
87 by(auto simp add: dvd_def) |
|
88 |
|
89 |
|
90 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat" |
|
91 where |
|
92 "Inpt m xs = Trpl 0 1 (Strt xs)" |
|
93 |
127 |
94 fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
128 fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
95 where |
129 where |
96 "Newconf m c = Trpl (Newleft (Left c) (Right c) (Actn m (Stat c) (Right c))) |
130 "Newconf c m = Conf (Newstat m (Stat c) (Scan (Right c)), |
97 (Newstat m (Stat c) (Right c)) |
131 (Newleft (Left c) (Right c) (Actn m (Stat c) (Scan (Right c))), |
98 (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))" |
132 Newright (Left c) (Right c) (Actn m (Stat c) (Scan (Right c)))))" |
99 |
133 |
100 text {* |
134 text {* |
101 @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution |
135 @{text "Step k m r"} computes the TM configuration after @{text "k"} steps of execution |
102 of TM coded as @{text "m"} starting from the initial configuration where the left |
136 of TM coded as @{text "m"} starting from the initial configuration where the left |
103 number equals @{text "0"}, right number equals @{text "r"}. *} |
137 number equals @{text "0"}, right number equals @{text "r"}. *} |
104 |
138 |
105 fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
139 fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
106 where |
140 where |
107 "Conf 0 m r = Trpl 0 1 r" |
141 "Steps cf p 0 = cf" |
108 | "Conf (Suc k) m r = Newconf m (Conf k m r)" |
142 | "Steps cf p (Suc n) = Steps (Newconf cf p) p n" |
109 |
143 |
110 text {* |
144 text {* |
111 @{text "Nstd c"} returns true if the configuration coded |
145 @{text "Nstd c"} returns true if the configuration coded |
112 by @{text "c"} is not a stardard final configuration. *} |
146 by @{text "c"} is not a stardard final configuration. *} |
113 |
147 |
114 fun Nstd :: "nat \<Rightarrow> bool" |
148 fun Nstd :: "nat \<Rightarrow> bool" |
115 where |
149 where |
116 "Nstd c = (Stat c \<noteq> 0 \<or> |
150 "Nstd c = (Stat c \<noteq> 0)" |
117 Left c \<noteq> 0 \<or> |
151 |
118 Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> |
152 -- "tape conditions are missing" |
119 Right c = 0)" |
|
120 |
|
121 |
153 |
122 text{* |
154 text{* |
123 @{text "Nostop t m r"} means that afer @{text "t"} steps of |
155 @{text "Nostop t m r"} means that afer @{text "t"} steps of |
124 execution the TM coded by @{text "m"} is not at a stardard |
156 execution the TM coded by @{text "m"} is not at a stardard |
125 final configuration. *} |
157 final configuration. *} |
126 |
158 |
127 fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
159 fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
128 where |
160 where |
129 "Nostop t m r = Nstd (Conf t m r)" |
161 "Nostop m l r = Nstd (Conf (m, (l, r)))" |
130 |
|
131 fun Value where |
|
132 "Value x = (Lg (Suc x) 2) - 1" |
|
133 |
162 |
134 text{* |
163 text{* |
135 @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before |
164 @{text "rec_halt"} is the recursive function calculating the steps a TM needs to |
136 to reach a stardard final configuration. This recursive function is the only one |
165 execute before to reach a stardard final configuration. This recursive function is |
137 using @{text "Mn"} combinator. So it is the only non-primitive recursive function |
166 the only one using @{text "Mn"} combinator. So it is the only non-primitive recursive |
138 needs to be used in the construction of the universal function @{text "rec_uf"}. *} |
167 function needs to be used in the construction of the universal function @{text "rec_uf"}. |
|
168 *} |
139 |
169 |
140 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
170 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
141 where |
171 where |
142 "Halt m r = (LEAST t. \<not> Nostop t m r)" |
172 "Halt m r = (LEAST t. \<not> Nostop t m r)" |
143 |
173 |
|
174 (* |
144 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
175 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
145 where |
176 where |
146 "UF c m = Value (Right (Conf (Halt c m) c m))" |
177 "UF c m = (Right (Conf (Halt c m) c m))" |
|
178 *) |
|
179 |
|
180 text {* reading the value is missing *} |
|
181 |
|
182 section {* The UF can simulate Turing machines *} |
|
183 |
|
184 lemma Update_left_simulate: |
|
185 shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))" |
|
186 apply(induct a) |
|
187 apply(simp_all) |
|
188 apply(case_tac l) |
|
189 apply(simp_all) |
|
190 apply(case_tac r) |
|
191 apply(simp_all) |
|
192 done |
|
193 |
|
194 lemma Update_right_simulate: |
|
195 shows "Newright (Code_tp l) (Code_tp r) (action_num a) = Code_tp (snd (update a (l, r)))" |
|
196 apply(induct a) |
|
197 apply(simp_all) |
|
198 apply(case_tac r) |
|
199 apply(simp_all) |
|
200 apply(case_tac r) |
|
201 apply(simp_all) |
|
202 apply(case_tac l) |
|
203 apply(simp_all) |
|
204 apply(case_tac r) |
|
205 apply(simp_all) |
|
206 done |
|
207 |
|
208 lemma Fetch_state_simulate: |
|
209 "\<lbrakk>tm_wf tp\<rbrakk> \<Longrightarrow> Newstat (Code_tprog tp) st (cell_num c) = snd (fetch tp st c)" |
|
210 apply(induct tp st c rule: fetch.induct) |
|
211 apply(simp_all add: list_encode_inverse split: cell.split) |
|
212 done |
|
213 |
|
214 lemma Fetch_action_simulate: |
|
215 "\<lbrakk>tm_wf tp; st \<le> length tp\<rbrakk> \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))" |
|
216 apply(induct tp st c rule: fetch.induct) |
|
217 apply(simp_all add: list_encode_inverse split: cell.split) |
|
218 done |
|
219 |
|
220 lemma Scan_simulate: |
|
221 "Scan (Code_tp tp) = cell_num (read tp)" |
|
222 apply(case_tac tp) |
|
223 apply(simp_all) |
|
224 done |
|
225 |
|
226 lemma misc: |
|
227 "2 < (3::nat)" |
|
228 "1 < (3::nat)" |
|
229 "0 < (3::nat)" |
|
230 "length [x] = 1" |
|
231 "length [x, y] = 2" |
|
232 "length [x, y , z] = 3" |
|
233 "[x, y, z] ! 0 = x" |
|
234 "[x, y, z] ! 1 = y" |
|
235 "[x, y, z] ! 2 = z" |
|
236 apply(simp_all) |
|
237 done |
|
238 |
|
239 lemma New_conf_simulate: |
|
240 assumes "tm_wf tp" "st \<le> length tp" |
|
241 shows "Newconf (Conf (Code_conf (st, l, r))) (Code_tprog tp) = Conf (Code_conf (step (st, l, r) tp))" |
|
242 apply(subst step.simps) |
|
243 apply(simp only: Let_def) |
|
244 apply(subst Newconf.simps) |
|
245 apply(simp only: Conf.simps Code_conf.simps Right.simps Left.simps) |
|
246 apply(simp only: list_encode_inverse) |
|
247 apply(simp only: misc if_True Code_tp.simps) |
|
248 apply(simp only: prod_case_beta) |
|
249 apply(subst Fetch_state_simulate[OF assms, symmetric]) |
|
250 apply(simp only: Stat.simps) |
|
251 apply(simp only: list_encode_inverse) |
|
252 apply(simp only: misc if_True) |
|
253 apply(simp only: Scan_simulate[simplified Code_tp.simps]) |
|
254 apply(simp only: Fetch_action_simulate[OF assms]) |
|
255 apply(simp only: Update_left_simulate[simplified Code_tp.simps]) |
|
256 apply(simp only: Update_right_simulate[simplified Code_tp.simps]) |
|
257 apply(case_tac "update (fst (fetch tp st (read r))) (l, r)") |
|
258 apply(simp only: Code_conf.simps) |
|
259 apply(simp only: Conf.simps) |
|
260 apply(simp) |
|
261 done |
|
262 |
|
263 lemma Step_simulate: |
|
264 assumes "tm_wf tp" "fst cf \<le> length tp" |
|
265 shows "Steps (Conf (Code_conf cf)) (Code_tprog tp) n = Conf (Code_conf (steps cf tp n))" |
|
266 apply(induct n arbitrary: cf) |
|
267 apply(simp) |
|
268 apply(simp only: Steps.simps steps.simps) |
|
269 apply(case_tac cf) |
|
270 apply(simp only: ) |
|
271 apply(subst New_conf_simulate) |
|
272 apply(rule assms) |
|
273 defer |
|
274 apply(drule_tac x="step (a, b, c) tp" in meta_spec) |
|
275 apply(simp) |
147 |
276 |
148 |
277 |
149 section {* Coding of Turing Machines *} |
278 section {* Coding of Turing Machines *} |
150 |
279 |
151 text {* |
280 text {* |