equal
deleted
inserted
replaced
1 theory UF_Rec |
1 theory UF_Rec |
2 imports Recs Hoare_tm |
2 imports Recs Hoare_tm2 |
3 begin |
3 begin |
4 |
4 |
5 section {* Coding of Turing Machines and Tapes*} |
5 section {* Coding of Turing Machines and Tapes*} |
6 |
6 |
7 |
7 |
10 "actnum W0 = 0" |
10 "actnum W0 = 0" |
11 | "actnum W1 = 1" |
11 | "actnum W1 = 1" |
12 | "actnum L = 2" |
12 | "actnum L = 2" |
13 | "actnum R = 3" |
13 | "actnum R = 3" |
14 |
14 |
15 |
|
16 fun cellnum :: "Block \<Rightarrow> nat" where |
15 fun cellnum :: "Block \<Rightarrow> nat" where |
17 "cellnum Bk = 0" |
16 "cellnum Bk = 0" |
18 | "cellnum Oc = 1" |
17 | "cellnum Oc = 1" |
19 |
18 |
20 |
19 |
21 (* NEED TO CODE TAPES *) |
20 (* coding programs *) |
|
21 |
|
22 thm finfun_comp_def |
|
23 term finfun_rec |
|
24 |
|
25 definition code_finfun :: "(nat \<Rightarrow>f tm_inst option) \<Rightarrow> (nat \<times> tm_inst option) list" |
|
26 where |
|
27 "code_finfun f = ([(x, f $ x). x \<leftarrow> finfun_to_list f])" |
|
28 |
|
29 fun lookup where |
|
30 "lookup [] c = None" |
|
31 | "lookup ((a, b)#xs) c = (if a = c then b else lookup xs c)" |
|
32 |
|
33 lemma |
|
34 "f $ n = lookup (code_finfun f) n" |
|
35 apply(induct f rule: finfun_weak_induct) |
|
36 apply(simp add: code_finfun_def) |
|
37 apply(simp add: finfun_to_list_const) |
|
38 thm finfun_rec_const |
|
39 apply(finfun_rec_const) |
|
40 apply(simp add: finfun_rec_def) |
|
41 apply(auto) |
|
42 thm finfun_rec_unique |
|
43 apply(rule finfun_rec_unique) |
|
44 |
22 |
45 |
23 text {* Coding tapes *} |
46 text {* Coding tapes *} |
24 |
47 |
25 fun code_tp :: "cell list \<Rightarrow> nat list" |
48 fun code_tp :: "() \<Rightarrow> nat list" |
26 where |
49 where |
27 "code_tp [] = []" |
50 "code_tp [] = []" |
28 | "code_tp (c # tp) = (cellnum c) # code_tp tp" |
51 | "code_tp (c # tp) = (cellnum c) # code_tp tp" |
29 |
52 |
30 fun Code_tp where |
53 fun Code_tp where |