--- a/thys2/Recs.thy	Wed May 22 13:50:20 2013 +0100
+++ b/thys2/Recs.thy	Fri May 24 15:43:10 2013 +0100
@@ -775,6 +775,8 @@
   "enclen 0 = 0"
 by (simp add: enclen_def)
 
+
+
 section {* Discrete Logarithms *}
 
 definition

--- a/thys2/UF_Rec.thy	Wed May 22 13:50:20 2013 +0100
+++ b/thys2/UF_Rec.thy	Fri May 24 15:43:10 2013 +0100
@@ -30,6 +30,18 @@
 fun Code_tp where
   "Code_tp tp = lenc (code_tp tp)"
 
+lemma code_tp_length [simp]:
+  "length (code_tp tp) = length tp"
+by (induct tp) (simp_all)
+
+lemma code_tp_nth [simp]:
+  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cell_num (tp ! n)"
+apply(induct n arbitrary: tp) 
+apply(simp_all)
+apply(case_tac [!] tp)
+apply(simp_all)
+done
+
 fun Code_conf where
   "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
 
@@ -153,23 +165,65 @@
   where
   "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1"
 
-lemma Binnum_simulate1:
-  "(Binnum z = 0) \<longleftrightarrow> (\<forall>i \<in> {..<enclen z}. ldec z i = 0)"
-by(auto simp add: Binnum_def)
+
+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))"
+
+definition
+  "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
 
-lemma Binnum_simulate2:
-  "(\<forall>i \<in> {..<enclen (Code_tp tp)}. ldec (Code_tp tp) i = 0) \<longleftrightarrow> (\<exists>k. tp = Bk \<up> k)"
+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))"
+apply(rule iffI)
+apply(erule exE)+
+apply(simp)
+apply(rule_tac x="k" in exI)
+apply(auto)[1]
+apply(simp add: nth_append)
+apply(simp add: nth_append)
+apply(erule exE)
+apply(rule_tac x="i" in exI)
+apply(rule_tac x="length tp - i" in exI)
+apply(auto)
+apply(rule sym)
+apply(subst append_eq_conv_conj)
+apply(simp)
+apply(rule conjI)
+apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)
+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)"
+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)
+apply(rule conjI)
+apply (metis Suc_eq_plus1 Suc_neq_Zero cell_num.cases cell_num.simps(1) leD less_trans linorder_neqE_nat)
+apply(auto)
+by (metis One_nat_def cell_num.cases cell_num.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)
+
+lemma left_std:
+  "(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"
+apply(simp add: left_std_def)
+apply(simp only: list_encode_inverse)
+apply(simp)
+apply(auto)
+apply(rule_tac x="length tp" in exI)
 apply(induct tp)
 apply(simp)
 apply(simp)
-apply(simp add: lessThan_Suc)
+apply(auto)
+apply(case_tac a)
+apply(auto)
 apply(case_tac a)
-apply(simp)
-defer
-apply(simp)
-oops
+apply(auto)
+by (metis Suc_less_eq nth_Cons_Suc)
 
-apply(simp add: Binnum_def)
 
 text {*
   @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 
@@ -178,8 +232,7 @@
 
 fun Std :: "nat \<Rightarrow> bool"
   where
-  "Std cf = (Binnum (Left cf) = 0 \<and> 
-            (\<exists>x\<le>(enclen (Right cf)). Binnum (Right cf) = 2 ^ x))"
+  "Std cf = (left_std (Left cf) \<and> right_std (Right cf))"
 
 text{* 
   @{text "Nostop m cf k"} means that afer @{text k} steps of 
@@ -312,6 +365,18 @@
 lemma Std_simulate:
   "Std (Conf (Code_conf cf)) = std_tape (snd 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: 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)