equal
deleted
inserted
replaced
47 |
47 |
48 datatype taction = W0 | W1 | L | R |
48 datatype taction = W0 | W1 | L | R |
49 |
49 |
50 type_synonym tstate = nat |
50 type_synonym tstate = nat |
51 |
51 |
|
52 datatype Block = Oc | Bk |
|
53 |
|
54 (* the successor state when tape symbol is Bk or Oc, respectively*) |
52 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)" |
55 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)" |
53 |
56 |
54 datatype Block = Oc | Bk |
57 (* - number of faults |
55 |
58 - TM program |
|
59 - current state |
|
60 - position of head |
|
61 - tape |
|
62 *) |
56 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
63 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
57 |
64 |
58 fun |
65 fun |
59 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
66 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
60 where |
67 where |
91 prog pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) |
98 prog pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) |
92 )" |
99 )" |
93 by (cases s) (auto split: option.splits Block.splits) |
100 by (cases s) (auto split: option.splits Block.splits) |
94 |
101 |
95 datatype tresource = |
102 datatype tresource = |
96 TM int Block |
103 TM int Block (* at the position int of the tape is a Bl or Oc *) |
97 | TC nat tm_inst |
104 | TC nat tm_inst (* at the address nat is a certain instruction *) |
98 | TAt nat |
105 | TAt nat (* TM is at state nat*) |
99 | TPos int |
106 | TPos int (* head of TM is at position int *) |
100 | TFaults nat |
107 | TFaults nat (* there are nat faults *) |
101 |
108 |
102 definition "tprog_set prog = {TC i inst | i inst. prog i = Some inst}" |
109 definition "tprog_set prog = {TC i inst | i inst. prog i = Some inst}" |
103 definition "tpc_set pc = {TAt pc}" |
110 definition "tpc_set pc = {TAt pc}" |
104 definition "tmem_set m = {TM i n | i n. m (i) = Some n}" |
111 definition "tmem_set m = {TM i n | i n. m (i) = Some n}" |
105 definition "tpos_set pos = {TPos pos}" |
112 definition "tpos_set pos = {TPos pos}" |