diff -r 89ed51d72e4a -r aea02b5a58d2 thys/UF_Rec.thy
--- 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