--- a/thys/UF_Rec.thy Thu May 02 12:49:15 2013 +0100
+++ b/thys/UF_Rec.thy Thu May 02 12:49:33 2013 +0100
@@ -1,40 +1,9 @@
theory UF_Rec
-imports Recs
+imports Recs Turing_Hoare
begin
section {* Universal Function *}
-text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *}
-
-fun NextPrime ::"nat \<Rightarrow> nat"
- where
- "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)"
-
-definition rec_nextprime :: "recf"
- where
- "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in
- let conj2 = CN rec_less [Id 2 1, Id 2 0] in
- let conj3 = CN rec_prime [Id 2 0] in
- let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3]
- in MN (CN rec_not [conjs]))"
-
-lemma nextprime_lemma [simp]:
- "rec_eval rec_nextprime [x] = NextPrime x"
-by (simp add: rec_nextprime_def Let_def)
-
-
-fun Pi :: "nat \<Rightarrow> nat"
- where
- "Pi 0 = 2" |
- "Pi (Suc x) = NextPrime (Pi x)"
-
-definition
- "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])"
-
-lemma pi_lemma [simp]:
- "rec_eval rec_pi [x] = Pi x"
-by (induct x) (simp_all add: rec_pi_def)
-
text{* coding of the configuration *}
@@ -371,494 +340,79 @@
definition
"rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
-end
-
-
-(*
-
+text {*
+ The correctness of @{text "rec_uf"}, nonhalt case.
+ *}
+subsection {* Coding function of TMs *}
-fun mtest where
- "mtest R 0 = if R 0 then 0 else 1"
-| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
-
+text {*
+ The purpose of this section is to get the coding function of Turing Machine,
+ which is going to be named @{text "code"}.
+ *}
-lemma
- "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
-apply(simp only: rec_maxr2_def)
-apply(case_tac x)
-apply(clarify)
-apply(subst rec_eval.simps)
-apply(simp only: constn_lemma)
-defer
-apply(clarify)
-apply(subst rec_eval.simps)
-apply(simp only: rec_maxr2_def[symmetric])
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
+fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat"
+ where
+ "bl2nat [] n = 0"
+| "bl2nat (Bk # bl) n = bl2nat bl (Suc n)"
+| "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)"
+
+fun bl2wc :: "cell list \<Rightarrow> nat"
+ where
+ "bl2wc xs = bl2nat xs 0"
-
-definition
- "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
-
-definition
- "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
+fun trpl_code :: "config \<Rightarrow> nat"
+ where
+ "trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
-definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
- where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
-
-definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
- where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
-
-lemma rec_minr2_le_Suc:
- "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"
-apply(simp add: rec_minr2_def)
-apply(auto intro!: setsum_one_le setprod_one_le)
-done
+fun action_map :: "action \<Rightarrow> nat"
+ where
+ "action_map W0 = 0"
+| "action_map W1 = 1"
+| "action_map L = 2"
+| "action_map R = 3"
+| "action_map Nop = 4"
-lemma rec_minr2_eq_Suc:
- assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
- shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
-using assms by (simp add: rec_minr2_def)
-
-lemma rec_minr2_le:
- assumes h1: "y \<le> x"
- and h2: "0 < rec_eval f [y, y1, y2]"
- shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y"
-apply(simp add: rec_minr2_def)
-apply(subst setsum_cut_off_le[OF h1])
-using h2 apply(auto)
-apply(auto intro!: setsum_one_less setprod_one_le)
-done
+fun action_map_iff :: "nat \<Rightarrow> action"
+ where
+ "action_map_iff (0::nat) = W0"
+| "action_map_iff (Suc 0) = W1"
+| "action_map_iff (Suc (Suc 0)) = L"
+| "action_map_iff (Suc (Suc (Suc 0))) = R"
+| "action_map_iff n = Nop"
-(* ??? *)
-lemma setsum_eq_one_le2:
- fixes n::nat
- assumes "\<forall>i \<le> n. f i \<le> 1"
- shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)"
-using assms
-apply(induct n)
-apply(simp add: One_nat_def)
-apply(simp)
-apply(auto simp add: One_nat_def)
-apply(drule_tac x="Suc n" in spec)
-apply(auto)
-by (metis le_Suc_eq)
-
+fun block_map :: "cell \<Rightarrow> nat"
+ where
+ "block_map Bk = 0"
+| "block_map Oc = 1"
-lemma rec_min2_not:
- assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
- shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
-using assms
-apply(simp add: rec_minr2_def)
-apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)")
-apply(simp)
-apply (metis atMost_iff le_refl zero_neq_one)
-apply(rule setsum_eq_one_le2)
-apply(auto)
-apply(rule setprod_one_le)
-apply(auto)
-done
+fun Goedel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
+ where
+ "Goedel_code' [] n = 1"
+| "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) "
+
+fun Goedel_code :: "nat list \<Rightarrow> nat"
+ where
+ "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)"
-lemma disjCI2:
- assumes "~P ==> Q" shows "P|Q"
-apply (rule classical)
-apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
-done
+fun modify_tprog :: "instr list \<Rightarrow> nat list"
+ where
+ "modify_tprog [] = []"
+| "modify_tprog ((a, s) # nl) = action_map a # s # modify_tprog nl"
-lemma minr_lemma [simp]:
-shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
-apply(induct x)
-apply(rule Least_equality[symmetric])
-apply(simp add: rec_minr2_def)
-apply(erule disjE)
-apply(rule rec_minr2_le)
-apply(auto)[2]
-apply(simp)
-apply(rule rec_minr2_le_Suc)
-apply(simp)
+text {* @{text "Code tp"} gives the Goedel coding of TM program @{text "tp"}. *}
+fun Code :: "instr list \<Rightarrow> nat"
+ where
+ "Code tp = Goedel_code (modify_tprog tp)"
-apply(rule rec_minr2_le)
+subsection {* Relating interperter functions to the execution of TMs *}
-apply(rule rec_minr2_le_Suc)
-apply(rule disjCI)
-apply(simp add: rec_minr2_def)
-
-apply(ru le setsum_one_less)
-apply(clarify)
-apply(rule setprod_one_le)
-apply(auto)[1]
-apply(simp)
-apply(rule setsum_one_le)
-apply(clarify)
-apply(rule setprod_one_le)
-apply(auto)[1]
-thm disj_CE
-apply(auto)
-
-lemma minr_lemma:
-shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
-apply(simp only: Minr_def)
-apply(rule sym)
-apply(rule Min_eqI)
-apply(auto)[1]
-apply(simp)
-apply(erule disjE)
-apply(simp)
-apply(rule rec_minr2_le_Suc)
-apply(rule rec_minr2_le)
-apply(auto)[2]
-apply(simp)
-apply(induct x)
-apply(simp add: rec_minr2_def)
-apply(
-apply(rule disjCI)
-apply(rule rec_minr2_eq_Suc)
-apply(simp)
-apply(auto)
-
-apply(rule setsum_one_le)
-apply(auto)[1]
-apply(rule setprod_one_le)
-apply(auto)[1]
-apply(subst setsum_cut_off_le)
-apply(auto)[2]
-apply(rule setsum_one_less)
-apply(auto)[1]
-apply(rule setprod_one_le)
-apply(auto)[1]
-apply(simp)
-thm setsum_eq_one_le
-apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>
- (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")
-prefer 2
-apply(auto)[1]
-apply(erule disjE)
-apply(rule disjI1)
-apply(rule setsum_eq_one_le)
-apply(simp)
-apply(rule disjI2)
-apply(simp)
-apply(clarify)
-apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")
-defer
-apply metis
-apply(erule exE)
-apply(subgoal_tac "l \<le> x")
-defer
-apply (metis not_leE not_less_Least order_trans)
-apply(subst setsum_least_eq)
-apply(rotate_tac 4)
-apply(assumption)
-apply(auto)[1]
-apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
-prefer 2
-apply(auto)[1]
-apply(rotate_tac 5)
-apply(drule not_less_Least)
-apply(auto)[1]
-apply(auto)
-apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)
-apply(simp)
-apply (metis LeastI_ex)
-apply(subst setsum_least_eq)
-apply(rotate_tac 3)
-apply(assumption)
-apply(simp)
-apply(auto)[1]
-apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
-prefer 2
-apply(auto)[1]
-apply (metis neq0_conv not_less_Least)
-apply(auto)[1]
-apply (metis (mono_tags) LeastI_ex)
-by (metis LeastI_ex)
-
-lemma minr_lemma:
-shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
-apply(simp only: Minr_def rec_minr2_def)
-apply(simp)
-apply(rule sym)
-apply(rule Min_eqI)
-apply(auto)[1]
-apply(simp)
-apply(erule disjE)
-apply(simp)
-apply(rule setsum_one_le)
-apply(auto)[1]
-apply(rule setprod_one_le)
-apply(auto)[1]
-apply(subst setsum_cut_off_le)
-apply(auto)[2]
-apply(rule setsum_one_less)
-apply(auto)[1]
-apply(rule setprod_one_le)
-apply(auto)[1]
-apply(simp)
-thm setsum_eq_one_le
-apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>
- (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")
-prefer 2
-apply(auto)[1]
-apply(erule disjE)
-apply(rule disjI1)
-apply(rule setsum_eq_one_le)
-apply(simp)
-apply(rule disjI2)
-apply(simp)
-apply(clarify)
-apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")
-defer
-apply metis
-apply(erule exE)
-apply(subgoal_tac "l \<le> x")
-defer
-apply (metis not_leE not_less_Least order_trans)
-apply(subst setsum_least_eq)
-apply(rotate_tac 4)
-apply(assumption)
-apply(auto)[1]
-apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
-prefer 2
-apply(auto)[1]
-apply(rotate_tac 5)
-apply(drule not_less_Least)
-apply(auto)[1]
-apply(auto)
-apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)
-apply(simp)
-apply (metis LeastI_ex)
-apply(subst setsum_least_eq)
-apply(rotate_tac 3)
-apply(assumption)
-apply(simp)
-apply(auto)[1]
-apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
-prefer 2
-apply(auto)[1]
-apply (metis neq0_conv not_less_Least)
-apply(auto)[1]
-apply (metis (mono_tags) LeastI_ex)
-by (metis LeastI_ex)
-
-lemma disjCI2:
- assumes "~P ==> Q" shows "P|Q"
-apply (rule classical)
-apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
-done
+lemma F_correct:
+ assumes tp: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"
+ and wf: "tm_wf0 tp" "0 < rs"
+ shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"
-lemma minr_lemma [simp]:
-shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
-(*apply(simp add: rec_minr2_def)*)
-apply(rule Least_equality[symmetric])
-prefer 2
-apply(erule disjE)
-apply(rule rec_minr2_le)
-apply(auto)[2]
-apply(clarify)
-apply(rule rec_minr2_le_Suc)
-apply(rule disjCI)
-apply(simp add: rec_minr2_def)
-
-apply(ru le setsum_one_less)
-apply(clarify)
-apply(rule setprod_one_le)
-apply(auto)[1]
-apply(simp)
-apply(rule setsum_one_le)
-apply(clarify)
-apply(rule setprod_one_le)
-apply(auto)[1]
-thm disj_CE
-apply(auto)
-apply(auto)
-prefer 2
-apply(rule le_tran
-
-apply(rule le_trans)
-apply(simp)
-defer
-apply(auto)
-apply(subst setsum_cut_off_le)
-
-
-lemma
- "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))"
-apply(simp add: Minr_def)
-apply(rule Min_eqI)
-apply(auto)[1]
-apply(simp)
-apply(rule Least_le)
-apply(auto)[1]
-apply(rule LeastI2_wellorder)
-apply(auto)
-done
-
-definition (in ord)
- Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
- "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"
-
-(*
-lemma Great_equality:
- assumes "P x"
- and "\<And>y. P y \<Longrightarrow> y \<le> x"
- shows "Great P = x"
-unfolding Great_def
-apply(rule the_equality)
-apply(blast intro: assms)
-*)
-
-
-
-lemma
- "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))"
-apply(simp add: Maxr_def)
-apply(rule Max_eqI)
-apply(auto)[1]
-apply(simp)
-thm Least_le Greatest_le
-oops
-
-lemma
- "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys"
-apply(simp add: Maxr_def Minr_def)
-apply(rule Max_eqI)
-apply(auto)[1]
-apply(simp)
-apply(erule disjE)
-apply(simp)
-apply(auto)[1]
-defer
-apply(simp)
-apply(auto)[1]
-thm Min_insert
-defer
-oops
-
-
-
-definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- where
- "quo x y = (if y = 0 then 0 else x div y)"
-
-
-definition
- "rec_quo = CN rec_mult [CN rec_sign [Id 2 1],
- CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]]))
- [Id 2 0, Id 2 0, Id 2 1]]"
+end
-lemma div_lemma [simp]:
- "rec_eval rec_quo [x, y] = quo x y"
-apply(simp add: rec_quo_def quo_def)
-apply(rule impI)
-apply(rule Min_eqI)
-apply(auto)[1]
-apply(simp)
-apply(erule disjE)
-apply(simp)
-apply(auto)[1]
-apply (metis div_le_dividend le_SucI)
-defer
-apply(simp)
-apply(auto)[1]
-apply (metis mult_Suc_right nat_mult_commute split_div_lemma)
-apply(auto)[1]
-
-apply (smt div_le_dividend fst_divmod_nat)
-apply(simp add: quo_def)
-apply(auto)[1]
-
-apply(auto)
-
-fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
- where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in
- if (setx = {}) then (Suc x) else (Min setx))"
-
-definition
- "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))"
-
-lemma minr_lemma [simp]:
-shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y"
-apply(simp only: rec_minr_def)
-apply(simp only: sigma1_lemma)
-apply(simp only: accum1_lemma)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(simp only: Minr.simps Let_def)
-apply(auto simp del: not_lemma)
-apply(simp)
-apply(simp only: not_lemma sign_lemma)
-apply(rule sym)
-apply(rule Min_eqI)
-apply(auto)[1]
-apply(simp)
-apply(subst setsum_cut_off_le[where m="ya"])
-apply(simp)
-apply(simp)
-apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
-apply(rule setsum_one_less)
-apply(default)
-apply(rule impI)
-apply(rule setprod_one_le)
-apply(auto split: if_splits)[1]
-apply(simp)
-apply(rule conjI)
-apply(subst setsum_cut_off_le[where m="xa"])
-apply(simp)
-apply(simp)
-apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
-apply(rule le_trans)
-apply(rule setsum_one_less)
-apply(default)
-apply(rule impI)
-apply(rule setprod_one_le)
-apply(auto split: if_splits)[1]
-apply(simp)
-apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])")
-defer
-apply metis
-apply(erule exE)
-apply(subgoal_tac "l \<le> x")
-defer
-apply (metis not_leE not_less_Least order_trans)
-apply(subst setsum_least_eq)
-apply(rotate_tac 3)
-apply(assumption)
-prefer 3
-apply (metis LeastI_ex)
-apply(auto)[1]
-apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])")
-prefer 2
-apply(auto)[1]
-apply(rotate_tac 5)
-apply(drule not_less_Least)
-apply(auto)[1]
-apply(auto)
-by (metis (mono_tags) LeastI_ex)
-
-
-fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
- where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in
- Min (setx \<union> {Suc x}))"
-
-lemma Minr2_Minr:
- "Minr2 R x y = Minr R x y"
-apply(auto)
-apply (metis (lifting, no_types) Min_singleton empty_Collect_eq)
-apply(rule min_absorb2)
-apply(subst Min_le_iff)
-apply(auto)
-done
- *)
\ No newline at end of file