equal
deleted
inserted
replaced
29 |
29 |
30 method_setup prune = |
30 method_setup prune = |
31 {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} |
31 {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} |
32 "pruning parameters" |
32 "pruning parameters" |
33 |
33 |
34 lemma int_add_C :"x + (y::int) = y + x" |
34 lemma int_add_C: |
|
35 "x + (y::int) = y + x" |
35 by simp |
36 by simp |
36 |
37 |
37 lemma int_add_A : "(x + y) + z = x + (y + (z::int))" |
38 lemma int_add_A : "(x + y) + z = x + (y + (z::int))" |
38 by simp |
39 by simp |
39 |
40 |
49 |
50 |
50 type_synonym tstate = nat |
51 type_synonym tstate = nat |
51 |
52 |
52 datatype Block = Oc | Bk |
53 datatype Block = Oc | Bk |
53 |
54 |
54 (* the successor state when tape symbol is Bk or Oc, respectively*) |
55 (* the successor state when tape symbol is Bk or Oc, respectively *) |
55 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)" |
56 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)" |
56 |
57 |
57 (* - number of faults |
58 (* - number of faults (nat) |
58 - TM program |
59 - TM program (nat \<rightharpoonup> tm_inst) |
59 - current state |
60 - current state (nat) |
60 - position of head |
61 - position of head (int) |
61 - tape |
62 - tape (int \<rightharpoonup> Block) |
62 *) |
63 *) |
63 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
64 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
64 |
65 |
65 fun |
66 fun |
66 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
67 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |