1 (* |
1 (* |
2 turing_basic.thy : The basic definitions of Turing Machine. |
2 turing_basic.thy : The basic definitions of Turing Machine. |
3 uncomputable.thy : The existence of Turing uncomputable functions. |
3 uncomputable.thy : The existence of Turing uncomputable functions. |
4 abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and |
4 abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and |
5 the compilation of Abacus machines into Turing Machines. |
5 the compilation of Abacus machines into Turing Machines. |
6 recursive.thy : The basic defintions of Recursive Functions and the compilation of Recursive Functions into |
6 rec_def.thy: The basic definitions of Recursive Functions. |
|
7 recursive.thy : The compilation of Recursive Functions into |
7 Abacus machines. |
8 Abacus machines. |
8 UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness. |
9 UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness. |
9 UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some |
10 UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some |
10 initialization and termination processing Turing Machines. |
11 initialization and termination processing Turing Machines. |
11 *) |
12 *) |
12 no_document use_thys ["turing_basic", "uncomputable", "abacus", "recursive", "UF", "UTM"] |
13 use_thys ["turing_basic", "uncomputable", "abacus", "rec_def", "recursive", "UF", "UTM"] |