regexp: comparison utm/UF.thy

equal deleted inserted replaced

-:1ce04eb1c8ad
+:48b231495281
 in terms of recursive functions. This @{text "rec_F"} is essentially an
 interpreter of Turing Machines. Once the correctness of @{text "rec_F"} is established,
 UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine.
 *}
+section {* Univeral Function *}
-section {* The construction of component functions *}
+subsection {* The construction of component functions *}
 text {*
 This section constructs a set of component functions used to construct @{text "rec_F"}.
 *}
 @{text "get_fstn_args n (Suc k)"} returns
 @{text "[id n 0, id n 1, id n 2, \<dots>, id n k]"},
 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 = []"
 | "get_fstn_args n (Suc y) = get_fstn_args n y @ [id n y]"
 declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]
 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)
 lemma rec_pr_0_simp_rewrite: "
 rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
 lemma rec_pr_Suc_simp_rewrite_single_param:
 "rec_exec (Pr n f g) ([Suc x]) =
 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)
 done
 qed
 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
 "quo [x, y] = (let Rr =
 (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0))
 apply(case_tac rcs, simp, simp)
 apply(case_tac "rec_exec aa xs = 0")
 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:
 "Suc (length rgs) = n" "Suc (length list) = n"
 "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
 rec_all (Cn 1 rec_minus [id 1 0, constn 1])
 (rec_all (Cn 2 rec_minus [id 2 0, Cn 2 (constn 1)
 [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:
 "rec_exec (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]])
 (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]))  [x, k] =
 done
 from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
 by simp
 qed
-text {*lemmas for power*}
 text {*
 @{text "rec_power"} is the recursive function used to implement
 power function.
 *}
 definition rec_power :: "recf"
 *}
 lemma pi_lemma: "rec_exec rec_pi [x] = Pi x"
 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)"
 declare loR.simps[simp del]
 The correctness of @{text "rec_entry"}.
 *}
 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,
 we are going to contruct the function @{text "F"},
 which is an interpreter of Turing Machines.
 apply(case_tac "a = 3", rule_tac x = "2" in exI)
 prefer 2
 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(*
+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)*)
 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)
 apply(auto simp: newleft.simps rec_newleft0_def rec_exec.simps
 rec_newleft1_def rec_newleft2_def rec_newleft3_def)
 The correctness of @{text "actn"}.
 *}
 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)
 else 0)"
 lemma nstd_lemma: "rec_exec rec_NSTD [c] = nstd c"
 using NSTD_lemma1
 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.
 *}
 fun nonstop :: "nat \<Rightarrow> nat  \<Rightarrow> nat \<Rightarrow> nat"
 definition rec_halt :: "recf"
 where
 "rec_halt = Mn (Suc (Suc 0)) (rec_nonstop)"
 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)
 lemma [elim]: "primerec f 0 \<Longrightarrow> RR"
 using h
 apply(erule_tac x = "ysb ! (Suc (Suc 0))" in allE, simp)
 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
 going to be named @{text "code"}.
 *}
 fun code :: "tprog \<Rightarrow> nat"
 where
 "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
 lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
 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
 let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
 have "finite ?setx" by auto
 lemma godel_code_get_nth:
 "i < length nl \<Longrightarrow>
 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
 lemma mod_dvd_simp: "(x mod y = (0::nat)) = (y dvd x)"
 qed
 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 =
 action_map (fst (tp ! (2 * (st - Suc 0) + r mod 2)))"
 apply(rule_tac  modify_tprog_fetch_action)
 using h
 by(auto)
 by(auto)
 qed
 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)
 using h
 by(auto)
 apply(simp add: conf_lemma)
 done
 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)
 done
 ultimately show
 qed
 qed
 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)
 apply(rule_tac x = 0 in exI, rule_tac x = 1 in exI,
 rule_tac x = "bl2wc (<lm>)" in exI)
 using halt_state_keep_steps_add[of m lm stpb "stpa - stpb"]
 apply simp
 using halt_state_keep_steps_add[of m lm stpa "stpb - stpa"]
 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.
 *}

changeset 371	48b231495281
parent 370	1ce04eb1c8ad