--- a/utm/UF.thy Sat Sep 29 12:38:12 2012 +0000
+++ b/utm/UF.thy Mon Oct 15 13:23:52 2012 +0000
@@ -9,8 +9,9 @@
UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine.
*}
-
-section {* The construction of component functions *}
+section {* Univeral Function *}
+
+subsection {* The construction of component functions *}
text {*
This section constructs a set of component functions used to construct @{text "rec_F"}.
@@ -126,7 +127,7 @@
the effect of which is to take out the first @{text "Suc k"}
arguments out of the @{text "n"} input arguments.
*}
-(* get_fstn_args *)
+
fun get_fstn_args :: "nat \<Rightarrow> nat \<Rightarrow> recf list"
where
"get_fstn_args n 0 = []"
@@ -341,9 +342,6 @@
arity.simps[simp del] Sigma.simps[simp del]
rec_sigma.simps[simp del]
-
-section {* Properties of @{text rec_sigma} *}
-
lemma [simp]: "arity z = 1"
by(simp add: arity.simps)
@@ -366,8 +364,6 @@
rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
by(simp add: rec_exec.simps)
-thm Sigma.simps
-
lemma Sigma_0_simp_rewrite_single_param:
"Sigma f [0] = f [0]"
by(simp add: Sigma.simps)
@@ -1106,7 +1102,7 @@
qed
text {*
- @text "quo"} is the formal specification of division.
+ @{text "quo"} is the formal specification of division.
*}
fun quo :: "nat list \<Rightarrow> nat"
where
@@ -1415,7 +1411,6 @@
apply(case_tac [!] "zip rgs list = []", simp)
apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_exec.simps rec_embranch.simps)
apply(rule_tac zip_null_iff, simp, simp, simp)
-thm Embranch.simps
proof -
fix aa list
assume g:
@@ -1565,13 +1560,6 @@
[id 2 0]]) (Cn 3 rec_noteq
[Cn 3 rec_mult [id 3 1, id 3 2], id 3 0]))]"
-(*
-lemma prime_lemma1:
- "(rec_exec rec_prime [x] = Suc 0) \<or>
- (rec_exec rec_prime [x] = 0)"
-apply(auto simp: rec_exec.simps rec_prime_def)
-done
-*)
declare numeral_2_eq_2[simp del] numeral_3_eq_3[simp del]
lemma exec_tmp:
@@ -1842,7 +1830,6 @@
by simp
qed
-text {*lemmas for power*}
text {*
@{text "rec_power"} is the recursive function used to implement
power function.
@@ -1888,7 +1875,6 @@
apply(simp add: rec_pi_def rec_exec.simps pi_dummy_lemma)
done
-text{*follows: lemmas for lo*}
fun loR :: "nat list \<Rightarrow> bool"
where
"loR [x, y, u] = (x mod (y^u) = 0)"
@@ -2175,7 +2161,8 @@
lemma entry_lemma: "rec_exec rec_entry [str, i] = Entry str i"
by(simp add: rec_entry_def rec_exec.simps lo_lemma pi_lemma)
-section {* The construction of @{text "F"} *}
+
+subsection {* The construction of F *}
text {*
Using the auxilliary functions obtained in last section,
@@ -2460,10 +2447,7 @@
apply(case_tac "a > 3", rule_tac x = "3" in exI, auto)
apply(auto simp: rec_exec.simps)
apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_exec.simps)
- done(*
- have "Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]
- = Embranch (zip ?gs ?rs) [p, r, a]"
- apply(simp add)*)
+ done
have k2: "Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newleft p r a"
apply(simp add: Embranch.simps)
apply(simp add: rec_exec.simps)
@@ -2613,8 +2597,6 @@
lemma actn_lemma: "rec_exec rec_actn [m, q, r] = actn m q r"
by(auto simp: rec_actn_def rec_exec.simps entry_lemma scan_lemma)
-(* Stop point *)
-
fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"newstat m q r = (if q \<noteq> 0 then Entry m (4*(q - 1) + 2*scan r + 1)
@@ -2919,8 +2901,6 @@
apply(simp add: NSTD_lemma2, auto)
done
-text {* GGGGGGGGGGGGGGGGGGGGGGG *}
-
text{*
@{text "nonstep m r t"} means afer @{text "t"} steps of execution, the TM coded by @{text "m"}
is not at a stardard final configuration.
@@ -2957,8 +2937,6 @@
declare nonstop.simps[simp del]
-(* when mn, use rec_calc_rel instead of rec_exec*)
-
lemma primerec_not0: "primerec f n \<Longrightarrow> n > 0"
by(induct f n rule: primerec.induct, auto)
@@ -3494,7 +3472,8 @@
done
qed
-section {* Coding function of TMs *}
+
+subsection {* Coding function of TMs *}
text {*
The purpose of this section is to get the coding function of Turing Machine, which is
@@ -3562,7 +3541,7 @@
"code tp = (let nl = modify_tprog tp in
godel_code nl)"
-section {* Relating interperter functions to the execution of TMs *}
+subsection {* Relating interperter functions to the execution of TMs *}
lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
term trpl
@@ -3571,7 +3550,6 @@
apply(simp add: fetch.simps)
done
-thm entry_lemma
lemma Pi_gr_1[simp]: "Pi n > Suc 0"
proof(induct n, auto simp: Pi.simps Np.simps)
fix n
@@ -3978,8 +3956,6 @@
Max {u. Pi (Suc i) ^ u dvd godel_code nl} = nl ! i"
by(simp add: godel_code.simps godel_code'_get_nth)
-thm trpl.simps
-
lemma "trpl l st r = godel_code' [l, st, r] 0"
apply(simp add: trpl.simps godel_code'.simps)
done
@@ -4218,8 +4194,7 @@
"Entry (godel_code (modify_tprog tp))?i =
(modify_tprog tp) ! ?i"
by(erule_tac godel_decode)
- thm modify_tprog.simps
- moreover have
+ moreover have
"modify_tprog tp ! ?i =
action_map (fst (tp ! (2 * (st - Suc 0) + r mod 2)))"
apply(rule_tac modify_tprog_fetch_action)
@@ -4307,8 +4282,7 @@
hence "Entry (godel_code (modify_tprog tp)) (?i) =
(modify_tprog tp) ! ?i"
by(erule_tac godel_decode)
- thm modify_tprog.simps
- moreover have
+ moreover have
"modify_tprog tp ! ?i =
(snd (tp ! (2 * (st - Suc 0) + r mod 2)))"
apply(rule_tac modify_tprog_fetch_state)
@@ -4606,7 +4580,6 @@
moreover hence
"trpl_code (tstep (a, b, c) tp) =
rec_exec rec_newconf [code tp, trpl_code (a, b, c)]"
- thm rec_t_eq_step
apply(rule_tac rec_t_eq_step)
using h g
apply(simp add: s_keep)
@@ -4783,18 +4756,6 @@
qed
qed
-(*
-lemma halt_steps_ex:
- "\<lbrakk>steps (Suc 0, Bk\<^bsup>l\<^esup>, <lm>) tp stp = (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>rs\<^esup> @ Bk\<^bsup>n\<^esup>);
- lm \<noteq> []; turing_basic.t_correct tp; 0<rs\<rbrakk> \<Longrightarrow>
- \<exists> t. rec_calc_rel (rec_halt (length lm)) (code tp # lm) t"
-apply(drule_tac halt_least_step, auto)
-apply(rule_tac x = stp in exI)
-apply(simp add: halt_lemma nonstop_lemma)
-apply(auto)
-done*)
-thm loR.simps
-
lemma conf_trpl_ex: "\<exists> p q r. conf m (bl2wc (<lm>)) stp = trpl p q r"
apply(induct stp, auto simp: conf.simps inpt.simps trpl.simps
newconf.simps)
@@ -4862,8 +4823,6 @@
apply(simp)
done
-thm halt_lemma
-
text {*
The correntess of @{text "rec_F"} which relates the interpreter function @{text "rec_F"} with the
execution of of TMs.