45 lemmas int_add_ac = int_add_A int_add_C int_add_LC |
45 lemmas int_add_ac = int_add_A int_add_C int_add_LC |
46 |
46 |
47 |
47 |
48 section {* Operational Semantics of TM *} |
48 section {* Operational Semantics of TM *} |
49 |
49 |
50 datatype taction = W0 | W1 | L | R |
50 datatype action = W0 | W1 | L | R |
51 |
51 |
52 type_synonym tstate = nat |
52 type_synonym state = nat |
53 |
53 |
|
54 (* FIXME: I think Block should be changed to cell *) |
54 datatype Block = Oc | Bk |
55 datatype Block = Oc | Bk |
55 |
56 |
56 (* the successor state when tape symbol is Bk or Oc, respectively *) |
57 (* the successor state when tape symbol is Bk or Oc, respectively *) |
57 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)" |
58 type_synonym tm_inst = "(action \<times> state) \<times> (action \<times> state)" |
58 |
59 |
59 (* - number of faults (nat) |
60 (* - number of faults (nat) |
60 - TM program (nat \<rightharpoonup> tm_inst) |
61 - TM program (nat f\<rightharpoonup> tm_inst) |
61 - current state (nat) |
62 - current state (nat) |
62 - position of head (int) |
63 - position of head (int) |
63 - tape (int \<rightharpoonup> Block) |
64 - tape (int f\<rightharpoonup> Block) |
64 *) |
65 *) |
65 type_synonym tconf = "nat \<times> (nat f\<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int f\<rightharpoonup> Block)" |
66 type_synonym tconf = "nat \<times> (nat f\<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int f\<rightharpoonup> Block)" |
66 |
67 |
67 (* updates the position/tape according to an action *) |
68 (* updates the position/tape according to an action *) |
68 fun |
69 fun |
69 next_tape :: "taction \<Rightarrow> (int \<times> (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int f\<rightharpoonup> Block))" |
70 next_tape :: "action \<Rightarrow> (int \<times> (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int f\<rightharpoonup> Block))" |
70 where |
71 where |
71 "next_tape W0 (pos, m) = (pos, m(pos f\<mapsto> Bk))" | |
72 "next_tape W0 (pos, m) = (pos, m(pos f\<mapsto> Bk))" | |
72 "next_tape W1 (pos, m) = (pos, m(pos f\<mapsto> Oc))" | |
73 "next_tape W1 (pos, m) = (pos, m(pos f\<mapsto> Oc))" | |
73 "next_tape L (pos, m) = (pos - 1, m)" | |
74 "next_tape L (pos, m) = (pos - 1, m)" | |
74 "next_tape R (pos, m) = (pos + 1, m)" |
75 "next_tape R (pos, m) = (pos + 1, m)" |