equal
deleted
inserted
replaced
|
1 (* Title: thys/UF.thy |
|
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
|
3 *) |
|
4 |
|
5 header {* Construction of a Universal Function *} |
|
6 |
1 theory UF |
7 theory UF |
2 imports Rec_Def GCD Abacus |
8 imports Rec_Def GCD Abacus |
3 begin |
9 begin |
4 |
10 |
5 text {* |
11 text {* |
7 in terms of recursive functions. This @{text "rec_F"} is essentially an |
13 in terms of recursive functions. This @{text "rec_F"} is essentially an |
8 interpreter of Turing Machines. Once the correctness of @{text "rec_F"} is established, |
14 interpreter of Turing Machines. Once the correctness of @{text "rec_F"} is established, |
9 UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine. |
15 UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine. |
10 *} |
16 *} |
11 |
17 |
12 section {* Univeral Function *} |
18 section {* Universal Function *} |
13 |
19 |
14 subsection {* The construction of component functions *} |
20 subsection {* The construction of component functions *} |
15 |
21 |
16 text {* |
22 text {* |
17 The recursive function used to do arithmatic addition. |
23 The recursive function used to do arithmatic addition. |