# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369424128 -3600
# Node ID ca1fe315cb0a970494d1f4c7583f484c3a8812dd
# Parent  1e45b5b6482af6b2f74b6ac82c21088bc7dfcafe
completed the UF-simulation lemmas

diff -r 1e45b5b6482a -r ca1fe315cb0a thys2/Turing2.thy
--- a/thys2/Turing2.thy	Fri May 24 15:43:10 2013 +0100
+++ b/thys2/Turing2.thy	Fri May 24 20:35:28 2013 +0100
@@ -58,11 +58,6 @@
   "steps cf p 0 = cf" |
   "steps cf p (Suc n) = steps (step cf p) p n"
 
-fun
-  is_final :: "config \<Rightarrow> bool"
-where
-  "is_final cf = (fst cf = 0)"
-
 
 (* well-formedness of Turing machine programs *)
 
@@ -114,7 +109,13 @@
 end
 
 definition 
-  "std_tape tp \<equiv> \<exists>k l (n::nat). tp = (Bk \<up> k, <n> @ Bk \<up> l)"
+  "std_tape tp \<equiv> \<exists>k (n::nat) l. snd tp = (Bk \<up> k, <n> @ Bk \<up> l)"
+
+fun
+  is_final :: "config \<Rightarrow> bool"
+where
+  "is_final cf = (fst cf = 0)"
+
 
 
 end
diff -r 1e45b5b6482a -r ca1fe315cb0a thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Fri May 24 15:43:10 2013 +0100
+++ b/thys2/UF_Rec.thy	Fri May 24 20:35:28 2013 +0100
@@ -30,6 +30,10 @@
 fun Code_tp where
   "Code_tp tp = lenc (code_tp tp)"
 
+lemma code_tp_append [simp]:
+  "code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2"
+by(induct tp1) (simp_all)
+
 lemma code_tp_length [simp]:
   "length (code_tp tp) = length tp"
 by (induct tp) (simp_all)
@@ -42,6 +46,11 @@
 apply(simp_all)
 done
 
+lemma code_tp_replicate [simp]:
+  "code_tp (c \<up> n) = (cell_num c) \<up> n"
+by(induct n) (simp_all)
+
+
 fun Code_conf where
   "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
 
@@ -126,7 +135,7 @@
 
 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
   where
-  "Conf (q, (l, r)) = lenc [q, l, r]"
+  "Conf (q, l, r) = lenc [q, l, r]"
 
 fun State where
   "State cf = ldec cf 0"
@@ -140,8 +149,8 @@
 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 
-                    (Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))),
-                     Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf)))))"
+                     Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))),
+                     Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))))"
 
 text {*
   @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution
@@ -157,24 +166,20 @@
   Decoding tapes into binary or stroke numbers.
 *}
 
-definition Binnum :: "nat \<Rightarrow> nat"
-  where
-  "Binnum z \<equiv> (\<Sum>i < enclen z. ldec z i * 2 ^ i)"
-
 definition Stknum :: "nat \<Rightarrow> nat"
   where
-  "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1"
+  "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)"
 
 
 definition
-  "right_std z \<equiv> (\<exists>i \<le> enclen z. (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
+  "right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
 
 definition
   "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
 
 lemma ww:
- "(\<exists>k l. tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> 
-  (\<exists>i\<le>length tp. (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
+ "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> 
+  (\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
 apply(rule iffI)
 apply(erule exE)+
 apply(simp)
@@ -194,11 +199,11 @@
 by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)
 
 lemma right_std:
-  "(\<exists>k l. tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
+  "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
+apply(simp only: ww)
 apply(simp add: right_std_def)
 apply(simp only: list_encode_inverse)
 apply(simp)
-apply(simp add: ww)
 apply(auto)
 apply(rule_tac x="i" in exI)
 apply(simp)
@@ -225,6 +230,52 @@
 by (metis Suc_less_eq nth_Cons_Suc)
 
 
+lemma Stknum_append:
+  "Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)"
+apply(simp only: Code_tp.simps)
+apply(simp only: code_tp_append)
+apply(simp only: Stknum_def)
+apply(simp only: enclen_length length_append code_tp_length)
+apply(simp only: list_encode_inverse)
+apply(simp only: enclen_length length_append code_tp_length)
+apply(simp)
+apply(subgoal_tac "{..<length tp1 + length tp2} = {..<length tp1} \<union> {length tp1 ..<length tp1 + length tp2}")
+prefer 2
+apply(auto)[1]
+apply(simp only:)
+apply(subst setsum_Un_disjoint)
+apply(auto)[2]
+apply (metis ivl_disj_int_one(2))
+apply(simp add: nth_append)
+apply(subgoal_tac "{length tp1..<length tp1 + length tp2} = (\<lambda>x. x + length tp1) ` {0..<length tp2}")
+prefer 2
+apply(simp only: image_add_atLeastLessThan)
+apply (metis comm_monoid_add_class.add.left_neutral nat_add_commute)
+apply(simp only:)
+apply(subst setsum_reindex)
+prefer 2
+apply(simp add: comp_def)
+apply (metis atLeast0LessThan)
+apply(simp add: inj_on_def)
+done
+
+lemma Stknum_up:
+  "Stknum (lenc (a \<up> n)) = n * a"
+apply(induct n)
+apply(simp_all add: Stknum_def list_encode_inverse del: replicate.simps)
+done
+
+lemma result:
+  "Stknum (Code_tp (<n> @ Bk \<up> l)) - 1 = n"
+apply(simp only: Stknum_append)
+apply(simp only: tape_of_nat.simps)
+apply(simp only: Code_tp.simps)
+apply(simp only: code_tp_replicate)
+apply(simp only: cell_num.simps)
+apply(simp only: Stknum_up)
+apply(simp)
+done
+
 text {*
   @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 
   is a stardard tape. 
@@ -243,9 +294,9 @@
   where
     "Final cf = (State cf = 0)"
 
-fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+fun Stop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   where
-  "Nostop m cf k = (Final (Steps cf m k) \<and> \<not> Std (Steps cf m k))"
+  "Stop m cf k = (Final (Steps cf m k) \<and> Std (Steps cf m k))"
 
 text{*
   @{text "Halt"} is the function calculating the steps a TM needs to 
@@ -257,11 +308,11 @@
 
 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Halt m cf = (LEAST k. \<not> Nostop m cf k)"
+  "Halt m cf = (LEAST k. Stop m cf k)"
 
 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "UF m cf = Stknum (Right (Steps m cf (Halt m cf)))"
+  "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
 
 section {* The UF can simulate Turing machines *}
 
@@ -363,25 +414,41 @@
 by (case_tac cf) (simp)
 
 lemma Std_simulate:
-  "Std (Conf (Code_conf cf)) = std_tape (snd cf)" 
+  "Std (Conf (Code_conf cf)) = std_tape cf" 
 apply(case_tac cf)
-apply(simp only: )
 apply(simp only: std_tape_def)
-apply(rule trans)
-defer
-apply(simp)
-apply(subst Std.simps)
-apply(simp only: Left.simps Right.simps)
 apply(simp only: Code_conf.simps)
 apply(simp only: Conf.simps)
+apply(simp only: Std.simps)
+apply(simp only: Left.simps Right.simps)
 apply(simp only: list_encode_inverse)
 apply(simp only: misc if_True)
-apply(simp only: Binnum_simulate)
-apply(simp add: std_tape_def del: Std.simps)
-apply(subst Std.simps)
+apply(simp only: left_std[symmetric] right_std[symmetric])
+apply(simp)
+apply(auto)
+apply(rule_tac x="ka - 1" in exI)
+apply(rule_tac x="l" in exI)
+apply(simp)
+apply (metis Suc_diff_le diff_Suc_Suc diff_zero replicate_Suc)
+apply(rule_tac x="n + 1" in exI)
+apply(simp)
+done
 
-(* UNTIL HERE *)
+lemma UF_simulate:
+  assumes "tm_wf tm"
+  shows "UF (Code_tprog tm) (Conf (Code_conf cf)) = 
+  Stknum (Right (Conf 
+  (Code_conf (steps cf tm (LEAST n. is_final (steps cf tm n) \<and> std_tape (steps cf tm n)))))) - 1" 
+apply(simp only: UF.simps)
+apply(subst Steps_simulate[symmetric, OF assms])
+apply(subst Final_simulate[symmetric])
+apply(subst Std_simulate[symmetric])
+apply(simp only: Halt.simps)
+apply(simp only: Steps_simulate[symmetric, OF assms])
+apply(simp only: Stop.simps[symmetric])
+done
 
+text {* UNTIL HERE *}
 
 section {* Universal Function as Recursive Functions *}