equal
deleted
inserted
replaced
56 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
56 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
57 where |
57 where |
58 "steps cf p 0 = cf" | |
58 "steps cf p 0 = cf" | |
59 "steps cf p (Suc n) = steps (step cf p) p n" |
59 "steps cf p (Suc n) = steps (step cf p) p n" |
60 |
60 |
61 fun |
|
62 is_final :: "config \<Rightarrow> bool" |
|
63 where |
|
64 "is_final cf = (fst cf = 0)" |
|
65 |
|
66 |
61 |
67 (* well-formedness of Turing machine programs *) |
62 (* well-formedness of Turing machine programs *) |
68 |
63 |
69 fun |
64 fun |
70 tm_wf :: "tprog \<Rightarrow> bool" |
65 tm_wf :: "tprog \<Rightarrow> bool" |
112 instance .. |
107 instance .. |
113 |
108 |
114 end |
109 end |
115 |
110 |
116 definition |
111 definition |
117 "std_tape tp \<equiv> \<exists>k l (n::nat). tp = (Bk \<up> k, <n> @ Bk \<up> l)" |
112 "std_tape tp \<equiv> \<exists>k (n::nat) l. snd tp = (Bk \<up> k, <n> @ Bk \<up> l)" |
|
113 |
|
114 fun |
|
115 is_final :: "config \<Rightarrow> bool" |
|
116 where |
|
117 "is_final cf = (fst cf = 0)" |
|
118 |
118 |
119 |
119 |
120 |
120 end |
121 end |
121 |
122 |