# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369140571 -3600
# Node ID df6e8cb229951ab531584b926eb4025fcae1cde6
# Parent  04700724250f7449483e3e201d136dbb61c81877
more about the UF

diff -r 04700724250f -r df6e8cb22995 thys/Recs.thy
--- a/thys/Recs.thy	Thu May 16 07:19:26 2013 +0100
+++ b/thys/Recs.thy	Tue May 21 13:49:31 2013 +0100
@@ -587,8 +587,11 @@
 section {* Encodings using Cantor's pairing function *}
 
 text {*
-  We first have to prove that we can extract the maximal
-  triangle number using @{term prod_decode}.
+  We use Cantor's pairing function from Nat_Bijection.
+  However, we need to prove that the formulation of the
+  decoding function there is recursive. For this we first 
+  prove that we can extract the maximal triangle number 
+  using @{term prod_decode}.
 *}
 
 abbreviation Max_triangle_aux where
@@ -597,35 +600,41 @@
 abbreviation Max_triangle where
   "Max_triangle z \<equiv> Max_triangle_aux 0 z"
 
+abbreviation
+  "pdec1 z \<equiv> fst (prod_decode z)"
+
+abbreviation
+  "pdec2 z \<equiv> snd (prod_decode z)"
+
+abbreviation 
+  "penc m n \<equiv> prod_encode (m, n)"
+
 lemma fst_prod_decode: 
-  "fst (prod_decode z) = z - triangle (Max_triangle z)"
-apply(subst (3) prod_decode_inverse[symmetric]) 
-apply(simp add: prod_encode_def)
-apply(case_tac "prod_decode z")
-apply(simp add: prod_decode_def)
-done
+  "pdec1 z = z - triangle (Max_triangle z)"
+by (subst (3) prod_decode_inverse[symmetric]) 
+   (simp add: prod_encode_def prod_decode_def split: prod.split)
 
 lemma snd_prod_decode: 
-  "snd (prod_decode z) = Max_triangle z - fst (prod_decode z)"
+  "pdec2 z = Max_triangle z - pdec1 z"
 by (simp only: prod_decode_def)
 
 lemma le_triangle:
   "m \<le> triangle (n + m)"
 by (induct_tac m) (simp_all)
 
-lemma k_aux: 
-  "Max_triangle z \<le> z"
-apply(subst (8) prod_decode_inverse[symmetric])
-apply(case_tac "prod_decode z")
-apply(simp add: prod_decode_def prod_encode_def le_triangle)
-done
+lemma Max_triangle_triangle_le:
+  "triangle (Max_triangle z) \<le> z"
+by (subst (9) prod_decode_inverse[symmetric])
+   (simp add: prod_decode_def prod_encode_def split: prod.split)
 
-lemma t_aux:
-  "triangle (Max_triangle z) \<le> z"
-apply(subst (9) prod_decode_inverse[symmetric])
-apply(case_tac "prod_decode z")
-apply(simp add: prod_decode_def prod_encode_def)
-done
+lemma Max_triangle_le: 
+  "Max_triangle z \<le> z"
+proof -
+  have "Max_triangle z \<le> triangle (Max_triangle z)"
+    using le_triangle[of _ 0, simplified] by simp
+  also have "... \<le> z" by (rule Max_triangle_triangle_le)
+  finally show "Max_triangle z \<le> z" .
+qed
 
 lemma w_aux: 
   "Max_triangle (triangle k + m) = Max_triangle_aux k m"
@@ -648,8 +657,8 @@
 apply(rule Greatest_equality[symmetric])
 apply(rule disjI1)
 apply(rule conjI)
-apply(rule t_aux)
-apply(rule k_aux)
+apply(rule Max_triangle_triangle_le)
+apply(rule Max_triangle_le)
 apply(erule disjE)
 apply(erule conjE)
 apply(subst (asm) (1) le_iff_add)
@@ -686,18 +695,50 @@
   "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" 
 
 lemma pdec1_lemma [simp]:
-  "rec_eval rec_pdec1 [z] = fst (prod_decode z)"
+  "rec_eval rec_pdec1 [z] = pdec1 z"
 by (simp add: rec_pdec1_def fst_prod_decode)
 
 lemma pdec2_lemma [simp]:
-  "rec_eval rec_pdec2 [z] = snd (prod_decode z)"
+  "rec_eval rec_pdec2 [z] = pdec2 z"
 by (simp add: rec_pdec2_def snd_prod_decode)
 
 lemma penc_lemma [simp]:
-  "rec_eval rec_penc [m, n] = prod_encode (m, n)"
+  "rec_eval rec_penc [m, n] = penc m n"
 by (simp add: rec_penc_def prod_encode_def)
 
+fun 
+  lenc :: "nat list \<Rightarrow> nat" 
+where
+  "lenc [] = 0"
+| "lenc (x # xs) = penc (Suc x) (lenc xs)"
 
+fun
+  ldec :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "ldec z 0 = (pdec1 z) - 1"
+| "ldec z (Suc n) = ldec (pdec2 z) n"
+
+lemma pdec_zero_simps [simp]:
+  "pdec1 0 = 0" 
+  "pdec2 0 = 0"
+by (simp_all add: prod_decode_def prod_decode_aux.simps)
+
+lemma w:
+  "ldec 0 n = 0"
+by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps)
+
+lemma list_encode_inverse: 
+  "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)"
+apply(induct xs arbitrary: n rule: lenc.induct) 
+apply(simp_all add: w)
+apply(case_tac n)
+apply(simp_all)
+done
+
+fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+  "within z 0 = (0 < z)"
+| "within z (Suc n) = within (pdec2 z) n"
+    
 
 section {* Discrete Logarithms *}
 
diff -r 04700724250f -r df6e8cb22995 thys/Turing2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Turing2.thy	Tue May 21 13:49:31 2013 +0100
@@ -0,0 +1,69 @@
+(* Title: thys/Turing.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Turing Machines *}
+
+theory Turing2
+imports Main
+begin
+
+section {* Basic definitions of Turing machine *}
+
+datatype action = W0 | W1 | L | R | Nop
+
+datatype cell = Bk | Oc
+
+type_synonym tape = "cell list \<times> cell list"
+
+type_synonym state = nat
+
+type_synonym instr = "action \<times> state"
+
+type_synonym tprog = "(instr \<times> instr) list"
+
+type_synonym config = "state \<times> tape"
+
+fun nth_of where
+  "nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))"
+
+fun 
+  fetch :: "tprog \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"
+where
+  "fetch p 0 b = (Nop, 0)"
+| "fetch p (Suc s) b = 
+     (case nth_of p s of
+        Some i \<Rightarrow> (case b of Bk \<Rightarrow> fst i | Oc \<Rightarrow> snd i)
+      | None \<Rightarrow> (Nop, 0))"
+
+fun 
+  update :: "action \<Rightarrow> tape \<Rightarrow> tape"
+where 
+  "update W0 (l, r) = (l, Bk # (tl r))" 
+| "update W1 (l, r) = (l, Oc # (tl r))"
+| "update L  (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" 
+| "update R  (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" 
+| "update Nop (l, r) = (l, r)"
+
+abbreviation 
+  "read r == if (r = []) then Bk else hd r"
+
+fun step :: "config \<Rightarrow> tprog \<Rightarrow> config"
+  where 
+  "step (s, l, r) p = 
+     (let (a, s') = fetch p s (read r) in (s', update a (l, r)))"
+
+fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config"
+  where
+  "steps c p 0 = c" |
+  "steps c p (Suc n) = steps (step c p) p n"
+
+(* well-formedness of Turing machine programs *)
+
+fun 
+  tm_wf :: "tprog \<Rightarrow> bool"
+where
+  "tm_wf p = (length p \<ge> 1 \<and> (\<forall>((_, s1), (_, s2)) \<in> set p. s1 \<le> length p \<and> s2 \<le> length p))"
+
+end
+