# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1396526143 -3600
# Node ID e3ecf558aef254d512fdcc8709dfc676b2ff2955
# Parent  23eeaac32d210cc6dc31000659e088bd1685a735
recursive function theories / UF_rec still need coding of tapes and programs

diff -r 23eeaac32d21 -r e3ecf558aef2 thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Thu Apr 03 12:47:07 2014 +0100
+++ b/thys/Hoare_tm.thy	Thu Apr 03 12:55:43 2014 +0100
@@ -63,6 +63,7 @@
 *)
 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
 
+(* updates the position/tape according to an action *)
 fun 
   next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"
 where 
diff -r 23eeaac32d21 -r e3ecf558aef2 thys/Recs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Recs.thy	Thu Apr 03 12:55:43 2014 +0100
@@ -0,0 +1,860 @@
+theory Recs
+imports Main Fact 
+        "~~/src/HOL/Number_Theory/Primes" 
+        "~~/src/HOL/Library/Nat_Bijection"
+        "~~/src/HOL/Library/Discrete"
+begin
+
+declare One_nat_def[simp del]
+
+(*
+  some definitions from 
+
+    A Course in Formal Languages, Automata and Groups
+    I M Chiswell 
+
+  and
+
+    Lecture on undecidability
+    Michael M. Wolf 
+*)
+
+lemma if_zero_one [simp]:
+  "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
+  "(0::nat) < (if P then 1 else 0) = P"
+  "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))"
+by (simp_all)
+
+lemma nth:
+  "(x # xs) ! 0 = x"
+  "(x # y # xs) ! 1 = y"
+  "(x # y # z # xs) ! 2 = z"
+  "(x # y # z # u # xs) ! 3 = u"
+by (simp_all)
+
+
+section {* Some auxiliary lemmas about @{text "\<Sum>"} and @{text "\<Prod>"} *}
+
+lemma setprod_atMost_Suc[simp]: 
+  "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
+by(simp add:atMost_Suc mult_ac)
+
+lemma setprod_lessThan_Suc[simp]: 
+  "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
+by (simp add:lessThan_Suc mult_ac)
+
+lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
+  setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
+apply(subst setsum_Un_disjoint[symmetric])
+apply(auto simp add: ivl_disj_un_one)
+done
+
+lemma setsum_eq_zero [simp]:
+  fixes f::"nat \<Rightarrow> nat"
+  shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
+        "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
+by (auto)
+
+lemma setprod_eq_zero [simp]:
+  fixes f::"nat \<Rightarrow> nat"
+  shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
+        "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
+by (auto)
+
+lemma setsum_one_less:
+  fixes n::nat
+  assumes "\<forall>i < n. f i \<le> 1" 
+  shows "(\<Sum>i < n. f i) \<le> n"  
+using assms
+by (induct n) (auto)
+
+lemma setsum_one_le:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i \<le> 1" 
+  shows "(\<Sum>i \<le> n. f i) \<le> Suc n"  
+using assms
+by (induct n) (auto)
+
+lemma setsum_eq_one_le:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i = 1" 
+  shows "(\<Sum>i \<le> n. f i) = Suc n"  
+using assms
+by (induct n) (auto)
+
+lemma setsum_least_eq:
+  fixes f::"nat \<Rightarrow> nat"
+  assumes h0: "p \<le> n"
+  assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
+  assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
+  shows "(\<Sum>i \<le> n. f i) = p"  
+proof -
+  have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" 
+    using h1 by (induct p) (simp_all)
+  have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" 
+    using h2 by auto
+  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)"
+    using h0 by (simp add: setsum_add_nat_ivl2) 
+  also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp
+  finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp
+qed
+
+lemma nat_mult_le_one:
+  fixes m n::nat
+  assumes "m \<le> 1" "n \<le> 1"
+  shows "m * n \<le> 1"
+using assms by (induct n) (auto)
+
+lemma setprod_one_le:
+  fixes f::"nat \<Rightarrow> nat"
+  assumes "\<forall>i \<le> n. f i \<le> 1" 
+  shows "(\<Prod>i \<le> n. f i) \<le> 1" 
+using assms 
+by (induct n) (auto intro: nat_mult_le_one)
+
+lemma setprod_greater_zero:
+  fixes f::"nat \<Rightarrow> nat"
+  assumes "\<forall>i \<le> n. f i \<ge> 0" 
+  shows "(\<Prod>i \<le> n. f i) \<ge> 0" 
+using assms by (induct n) (auto)
+
+lemma setprod_eq_one:
+  fixes f::"nat \<Rightarrow> nat"
+  assumes "\<forall>i \<le> n. f i = Suc 0" 
+  shows "(\<Prod>i \<le> n. f i) = Suc 0" 
+using assms by (induct n) (auto)
+
+lemma setsum_cut_off_less:
+  fixes f::"nat \<Rightarrow> nat"
+  assumes h1: "m \<le> n"
+  and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
+  shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
+proof -
+  have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 
+    using h2 by auto
+  have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)"
+    using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) 
+  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
+  finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp
+qed
+
+lemma setsum_cut_off_le:
+  fixes f::"nat \<Rightarrow> nat"
+  assumes h1: "m \<le> n"
+  and     h2: "\<forall>i \<in> {m..n}. f i = 0"
+  shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
+proof -
+  have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" 
+    using h2 by auto
+  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)"
+    using h1 by (simp add: setsum_add_nat_ivl2)
+  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
+  finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp
+qed
+
+lemma setprod_one [simp]:
+  fixes n::nat
+  shows "(\<Prod>i < n. Suc 0) = Suc 0"
+        "(\<Prod>i \<le> n. Suc 0) = Suc 0"
+by (induct n) (simp_all)
+
+
+
+section {* Recursive Functions *}
+
+datatype recf =  Z
+              |  S
+              |  Id nat nat
+              |  Cn nat recf "recf list"
+              |  Pr nat recf recf
+              |  Mn nat recf 
+
+fun arity :: "recf \<Rightarrow> nat"
+  where
+  "arity Z = 1" 
+| "arity S = 1"
+| "arity (Id m n) = m"
+| "arity (Cn n f gs) = n"
+| "arity (Pr n f g) = Suc n"
+| "arity (Mn n f) = n"
+
+text {* Abbreviations for calculating the arity of the constructors *}
+
+abbreviation
+  "CN f gs \<equiv> Cn (arity (hd gs)) f gs"
+
+abbreviation
+  "PR f g \<equiv> Pr (arity f) f g"
+
+abbreviation
+  "MN f \<equiv> Mn (arity f - 1) f"
+
+text {* the evaluation function and termination relation *}
+
+fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
+  where
+  "rec_eval Z xs = 0" 
+| "rec_eval S xs = Suc (xs ! 0)" 
+| "rec_eval (Id m n) xs = xs ! n" 
+| "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 
+| "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"
+| "rec_eval (Pr n f g) (Suc x # xs) = 
+     rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)"
+| "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)"
+
+inductive 
+  terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
+where
+  termi_z: "terminates Z [n]"
+| termi_s: "terminates S [n]"
+| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (Id m n) xs"
+| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
+              \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
+| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
+              terminates f xs;
+              length xs = n\<rbrakk> 
+              \<Longrightarrow> terminates (Pr n f g) (x # xs)"
+| termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
+              rec_eval f (r # xs) = 0;
+              \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
+
+
+section {* Arithmetic Functions *}
+
+text {*
+  @{text "constn n"} is the recursive function which computes 
+  natural number @{text "n"}.
+*}
+fun constn :: "nat \<Rightarrow> recf"
+  where
+  "constn 0 = Z"  |
+  "constn (Suc n) = CN S [constn n]"
+
+definition
+  "rec_swap f = CN f [Id 2 1, Id 2 0]"
+
+definition
+  "rec_add = PR (Id 1 0) (CN S [Id 3 1])"
+
+definition 
+  "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
+
+definition 
+  "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
+
+definition 
+  "rec_fact_aux = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+
+definition
+  "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
+
+definition 
+  "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
+
+definition 
+  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
+
+lemma constn_lemma [simp]: 
+  "rec_eval (constn n) xs = n"
+by (induct n) (simp_all)
+
+lemma swap_lemma [simp]:
+  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
+by (simp add: rec_swap_def)
+
+lemma add_lemma [simp]: 
+  "rec_eval rec_add [x, y] =  x + y"
+by (induct x) (simp_all add: rec_add_def)
+
+lemma mult_lemma [simp]: 
+  "rec_eval rec_mult [x, y] = x * y"
+by (induct x) (simp_all add: rec_mult_def)
+
+lemma power_lemma [simp]: 
+  "rec_eval rec_power [x, y] = x ^ y"
+by (induct y) (simp_all add: rec_power_def)
+
+lemma fact_aux_lemma [simp]: 
+  "rec_eval rec_fact_aux [x, y] = fact x"
+by (induct x) (simp_all add: rec_fact_aux_def)
+
+lemma fact_lemma [simp]: 
+  "rec_eval rec_fact [x] = fact x"
+by (simp add: rec_fact_def)
+
+lemma pred_lemma [simp]: 
+  "rec_eval rec_pred [x] =  x - 1"
+by (induct x) (simp_all add: rec_pred_def)
+
+lemma minus_lemma [simp]: 
+  "rec_eval rec_minus [x, y] = x - y"
+by (induct y) (simp_all add: rec_minus_def)
+
+
+section {* Logical functions *}
+
+text {* 
+  The @{text "sign"} function returns 1 when the input argument 
+  is greater than @{text "0"}. *}
+
+definition 
+  "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
+
+definition 
+  "rec_not = CN rec_minus [constn 1, Id 1 0]"
+
+text {*
+  @{text "rec_eq"} compares two arguments: returns @{text "1"}
+  if they are equal; @{text "0"} otherwise. *}
+definition 
+  "rec_eq = CN rec_minus [CN (constn 1) [Id 2 0], CN rec_add [rec_minus, rec_swap rec_minus]]"
+
+definition 
+  "rec_noteq = CN rec_not [rec_eq]"
+
+definition 
+  "rec_conj = CN rec_sign [rec_mult]"
+
+definition 
+  "rec_disj = CN rec_sign [rec_add]"
+
+definition 
+  "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
+
+text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
+  y otherwise;  @{term "rec_if [z, x, y]"} returns x if z is *not*
+  zero, y otherwise *}
+
+definition 
+  "rec_ifz = PR (Id 2 0) (Id 4 3)"
+
+definition 
+  "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
+
+
+lemma sign_lemma [simp]: 
+  "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
+by (simp add: rec_sign_def)
+
+lemma not_lemma [simp]: 
+  "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
+by (simp add: rec_not_def)
+
+lemma eq_lemma [simp]: 
+  "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
+by (simp add: rec_eq_def)
+
+lemma noteq_lemma [simp]: 
+  "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
+by (simp add: rec_noteq_def)
+
+lemma conj_lemma [simp]: 
+  "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by (simp add: rec_conj_def)
+
+lemma disj_lemma [simp]: 
+  "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by (simp add: rec_disj_def)
+
+lemma imp_lemma [simp]: 
+  "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
+by (simp add: rec_imp_def)
+
+lemma ifz_lemma [simp]:
+  "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" 
+by (case_tac z) (simp_all add: rec_ifz_def)
+
+lemma if_lemma [simp]:
+  "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
+by (simp add: rec_if_def)
+
+section {* Less and Le Relations *}
+
+text {*
+  @{text "rec_less"} compares two arguments and returns @{text "1"} if
+  the first is less than the second; otherwise returns @{text "0"}. *}
+
+definition 
+  "rec_less = CN rec_sign [rec_swap rec_minus]"
+
+definition 
+  "rec_le = CN rec_disj [rec_less, rec_eq]"
+
+lemma less_lemma [simp]: 
+  "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
+by (simp add: rec_less_def)
+
+lemma le_lemma [simp]: 
+  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+by(simp add: rec_le_def)
+
+
+section {* Summation and Product Functions *}
+
+definition 
+  "rec_sigma1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
+                     (CN rec_add [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
+
+definition 
+  "rec_sigma2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
+                     (CN rec_add [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
+
+definition 
+  "rec_accum1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
+                     (CN rec_mult [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
+
+definition 
+  "rec_accum2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
+                     (CN rec_mult [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
+
+definition 
+  "rec_accum3 f = PR (CN f [CN Z [Id 3 0], Id 3 0, Id 3 1, Id 3 2]) 
+                     (CN rec_mult [Id 5 1, CN f [CN S [Id 5 0], Id 5 2, Id 5 3, Id 5 4]])"
+
+
+lemma sigma1_lemma [simp]: 
+  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])"
+by (induct x) (simp_all add: rec_sigma1_def)
+
+lemma sigma2_lemma [simp]: 
+  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f  [z, y1, y2])"
+by (induct x) (simp_all add: rec_sigma2_def)
+
+lemma accum1_lemma [simp]: 
+  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f  [z, y])"
+by (induct x) (simp_all add: rec_accum1_def)
+
+lemma accum2_lemma [simp]: 
+  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f  [z, y1, y2])"
+by (induct x) (simp_all add: rec_accum2_def)
+
+lemma accum3_lemma [simp]: 
+  shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
+by (induct x) (simp_all add: rec_accum3_def)
+
+
+section {* Bounded Quantifiers *}
+
+definition
+  "rec_all1 f = CN rec_sign [rec_accum1 f]"
+
+definition
+  "rec_all2 f = CN rec_sign [rec_accum2 f]"
+
+definition
+  "rec_all3 f = CN rec_sign [rec_accum3 f]"
+
+definition
+  "rec_all1_less f = (let cond1 = CN rec_eq [Id 3 0, Id 3 1] in
+                      let cond2 = CN f [Id 3 0, Id 3 2] 
+                      in CN (rec_all2 (CN rec_disj [cond1, cond2])) [Id 2 0, Id 2 0, Id 2 1])"
+
+definition
+  "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in 
+                      let cond2 = CN f [Id 4 0, Id 4 2, Id 4 3] in 
+                      CN (rec_all3 (CN rec_disj [cond1, cond2])) [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
+
+definition
+  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
+
+definition
+  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
+
+
+lemma ex1_lemma [simp]:
+ "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
+by (simp add: rec_ex1_def)
+
+lemma ex2_lemma [simp]:
+ "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+by (simp add: rec_ex2_def)
+
+lemma all1_lemma [simp]:
+ "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
+by (simp add: rec_all1_def)
+
+lemma all2_lemma [simp]:
+ "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+by (simp add: rec_all2_def)
+
+lemma all3_lemma [simp]:
+ "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
+by (simp add: rec_all3_def)
+
+lemma all1_less_lemma [simp]:
+  "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)"
+apply(auto simp add: Let_def rec_all1_less_def)
+apply (metis nat_less_le)+
+done
+
+lemma all2_less_lemma [simp]:
+  "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+apply(auto simp add: Let_def rec_all2_less_def)
+apply(metis nat_less_le)+
+done
+
+section {* Quotients *}
+
+definition
+  "rec_quo = (let lhs = CN S [Id 3 0] in
+              let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
+              let cond = CN rec_eq [lhs, rhs] in
+              let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
+              in PR Z if_stmt)"
+
+fun Quo where
+  "Quo x 0 = 0"
+| "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)"
+
+lemma Quo0:
+  shows "Quo 0 y = 0"
+by (induct y) (auto)
+
+lemma Quo1:
+  "x * (Quo x y) \<le> y"
+by (induct y) (simp_all)
+
+lemma Quo2: 
+  "b * (Quo b a) + a mod b = a"
+by (induct a) (auto simp add: mod_Suc)
+
+lemma Quo3:
+  "n * (Quo n m) = m - m mod n"
+using Quo2[of n m] by (auto)
+
+lemma Quo4:
+  assumes h: "0 < x"
+  shows "y < x + x * Quo x y"
+proof -
+  have "x - (y mod x) > 0" using mod_less_divisor assms by auto
+  then have "y < y + (x - (y mod x))" by simp
+  then have "y < x + (y - (y mod x))" by simp
+  then show "y < x + x * (Quo x y)" by (simp add: Quo3) 
+qed
+
+lemma Quo_div: 
+  shows "Quo x y = y div x"
+apply(case_tac "x = 0")
+apply(simp add: Quo0)
+apply(subst split_div_lemma[symmetric])
+apply(auto intro: Quo1 Quo4)
+done
+
+lemma Quo_rec_quo:
+  shows "rec_eval rec_quo [y, x] = Quo x y"
+by (induct y) (simp_all add: rec_quo_def)
+
+lemma quo_lemma [simp]:
+  shows "rec_eval rec_quo [y, x] = y div x"
+by (simp add: Quo_div Quo_rec_quo)
+
+
+section {* Iteration *}
+
+definition
+   "rec_iter f = PR (Id 1 0) (CN f [Id 3 1])"
+
+fun Iter where
+  "Iter f 0 = id"
+| "Iter f (Suc n) = f \<circ> (Iter f n)"
+
+lemma Iter_comm:
+  "(Iter f n) (f x) = f ((Iter f n) x)"
+by (induct n) (simp_all)
+
+lemma iter_lemma [simp]:
+  "rec_eval (rec_iter f) [n, x] =  Iter (\<lambda>x. rec_eval f [x]) n x"
+by (induct n) (simp_all add: rec_iter_def)
+
+
+section {* Bounded Maximisation *}
+
+
+fun BMax_rec where
+  "BMax_rec R 0 = 0"
+| "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"
+
+definition 
+  BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
+where 
+  "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
+
+lemma BMax_rec_eq1:
+ "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)"
+apply(induct x)
+apply(auto intro: Greatest_equality Greatest_equality[symmetric])
+apply(simp add: le_Suc_eq)
+by metis
+
+lemma BMax_rec_eq2:
+  "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
+apply(induct x)
+apply(auto intro: Max_eqI Max_eqI[symmetric])
+apply(simp add: le_Suc_eq)
+by metis
+
+lemma BMax_rec_eq3:
+  "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
+by (simp add: BMax_rec_eq2 Set.filter_def)
+
+definition 
+  "rec_max1 f = PR Z (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 3 0], Id 3 1])"
+ 
+lemma max1_lemma [simp]:
+  "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
+by (induct x) (simp_all add: rec_max1_def)
+
+definition 
+  "rec_max2 f = PR Z (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
+ 
+lemma max2_lemma [simp]:
+  "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
+by (induct x) (simp_all add: rec_max2_def)
+
+
+section {* Encodings using Cantor's pairing function *}
+
+text {*
+  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
+  "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)"
+
+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: 
+  "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: 
+  "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 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 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"
+by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add)
+
+lemma y_aux: "y \<le> Max_triangle_aux y k"
+apply(induct k arbitrary: y rule: nat_less_induct)
+apply(subst (1 2) prod_decode_aux.simps)
+apply(simp)
+apply(rule impI)
+apply(drule_tac x="n - Suc y" in spec)
+apply(drule mp)
+apply(auto)[1]
+apply(drule_tac x="Suc y" in spec)
+apply(erule Suc_leD)
+done
+
+lemma Max_triangle_greatest: 
+  "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"
+apply(rule Greatest_equality[symmetric])
+apply(rule disjI1)
+apply(rule conjI)
+apply(rule Max_triangle_triangle_le)
+apply(rule Max_triangle_le)
+apply(erule disjE)
+apply(erule conjE)
+apply(subst (asm) (1) le_iff_add)
+apply(erule exE)
+apply(clarify)
+apply(simp only: w_aux)
+apply(rule y_aux)
+apply(simp)
+done
+
+
+definition 
+  "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]"
+
+definition
+  "rec_max_triangle = 
+       (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in
+        CN (rec_max1 cond) [Id 1 0, Id 1 0])"
+
+
+lemma triangle_lemma [simp]:
+  "rec_eval rec_triangle [x] = triangle x"
+by (simp add: rec_triangle_def triangle_def)
+ 
+lemma max_triangle_lemma [simp]:
+  "rec_eval rec_max_triangle [x] = Max_triangle x"
+by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) 
+
+
+text {* Encodings for Products *}
+
+definition
+  "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
+
+definition 
+  "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]" 
+
+definition 
+  "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] = pdec1 z"
+by (simp add: rec_pdec1_def fst_prod_decode)
+
+lemma pdec2_lemma [simp]:
+  "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] = penc m n"
+by (simp add: rec_penc_def prod_encode_def)
+
+
+text {* Encodings of Lists *}
+
+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 ldec_zero:
+  "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)"
+by (induct xs arbitrary: n rule: lenc.induct) 
+   (auto simp add: ldec_zero nth_Cons split: nat.splits)
+
+lemma lenc_length_le:
+  "length xs \<le> lenc xs"  
+by (induct xs) (simp_all add: prod_encode_def)
+
+
+text {* Membership for the List Encoding *}
+
+fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+  "within z 0 = (0 < z)"
+| "within z (Suc n) = within (pdec2 z) n"
+    
+definition enclen :: "nat \<Rightarrow> nat" where
+  "enclen z = BMax_rec (\<lambda>x. within z (x - 1)) z"
+
+lemma within_False [simp]:
+  "within 0 n = False"
+by (induct n) (simp_all)
+
+lemma within_length [simp]:
+  "within (lenc xs) s = (s < length xs)"
+apply(induct s arbitrary: xs)
+apply(case_tac xs)
+apply(simp_all add: prod_encode_def)
+apply(case_tac xs)
+apply(simp_all)
+done
+
+text {* Length of Encoded Lists *}
+
+lemma enclen_length [simp]:
+  "enclen (lenc xs) = length xs"
+unfolding enclen_def
+apply(simp add: BMax_rec_eq1)
+apply(rule Greatest_equality)
+apply(auto simp add: lenc_length_le)
+done
+
+lemma enclen_penc [simp]:
+  "enclen (penc (Suc x) (lenc xs)) = Suc (enclen (lenc xs))"
+by (simp only: lenc.simps[symmetric] enclen_length) (simp)
+
+lemma enclen_zero [simp]:
+  "enclen 0 = 0"
+by (simp add: enclen_def)
+
+
+text {* Recursive Definitions for List Encodings *}
+
+fun 
+  rec_lenc :: "recf list \<Rightarrow> recf" 
+where
+  "rec_lenc [] = Z"
+| "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]"
+
+definition 
+  "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
+
+definition 
+  "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
+
+definition
+  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]"
+
+lemma ldec_iter:
+  "ldec z n = pdec1 (Iter pdec2 n z) - 1"
+by (induct n arbitrary: z) (simp | subst Iter_comm)+
+
+lemma within_iter:
+  "within z n = (0 < Iter pdec2 n z)"
+by (induct n arbitrary: z) (simp | subst Iter_comm)+
+
+lemma lenc_lemma [simp]:
+  "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)"
+by (induct fs) (simp_all)
+
+lemma ldec_lemma [simp]:
+  "rec_eval rec_ldec [z, n] = ldec z n"
+by (simp add: ldec_iter rec_ldec_def)
+
+lemma within_lemma [simp]:
+  "rec_eval rec_within [z, n] = (if within z n then 1 else 0)"
+by (simp add: within_iter rec_within_def)
+
+lemma enclen_lemma [simp]:
+  "rec_eval rec_enclen [z] = enclen z"
+by (simp add: rec_enclen_def enclen_def)
+
+
+end
+
diff -r 23eeaac32d21 -r e3ecf558aef2 thys/UF_Rec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/UF_Rec.thy	Thu Apr 03 12:55:43 2014 +0100
@@ -0,0 +1,667 @@
+theory UF_Rec
+imports Recs Hoare_tm
+begin
+
+section {* Coding of Turing Machines and Tapes*}
+
+
+fun actnum :: "taction \<Rightarrow> nat"
+  where
+  "actnum W0 = 0"
+| "actnum W1 = 1"
+| "actnum L  = 2"
+| "actnum R  = 3"
+
+
+fun cellnum :: "Block \<Rightarrow> nat" where
+  "cellnum Bk = 0"
+| "cellnum Oc = 1"
+
+
+(* NEED TO CODE TAPES *)
+
+text {* Coding tapes *}
+
+fun code_tp :: "cell list \<Rightarrow> nat list"
+  where
+  "code_tp [] = []"
+| "code_tp (c # tp) = (cellnum c) # code_tp tp"
+
+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)
+
+lemma code_tp_nth [simp]:
+  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"
+apply(induct n arbitrary: tp) 
+apply(simp_all)
+apply(case_tac [!] tp)
+apply(simp_all)
+done
+
+lemma code_tp_replicate [simp]:
+  "code_tp (c \<up> n) = (cellnum c) \<up> n"
+by(induct n) (simp_all)
+
+text {* Coding Configurations and TMs *}
+
+fun Code_conf where
+  "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
+
+fun code_instr :: "instr \<Rightarrow> nat" where
+  "code_instr i = penc (actnum (fst i)) (snd i)"
+  
+fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where
+  "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"
+
+fun code_tprog :: "tprog \<Rightarrow> nat list"
+  where
+  "code_tprog [] =  []"
+| "code_tprog (i # tm) = Code_instr i # code_tprog tm"
+
+lemma code_tprog_length [simp]:
+  "length (code_tprog tp) = length tp"
+by (induct tp) (simp_all)
+
+lemma code_tprog_nth [simp]:
+  "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)"
+by (induct tp arbitrary: n) (simp_all add: nth_Cons')
+
+fun Code_tprog :: "tprog \<Rightarrow> nat"
+  where 
+  "Code_tprog tm = lenc (code_tprog tm)"
+
+
+section {* An Universal Function in HOL *}
+
+text {* Reading and writing the encoded tape *}
+
+fun Read where
+  "Read tp = ldec tp 0"
+
+fun Write where
+  "Write n tp = penc (Suc n) (pdec2 tp)"
+
+text {* 
+  The @{text Newleft} and @{text Newright} functions on page 91 of B book. 
+  They calculate the new left and right tape (@{text p} and @{text r}) 
+  according to an action @{text a}. Adapted to our encoding functions.
+*}
+
+fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newleft l r a = (if a = 0 then l else 
+                    if a = 1 then l else 
+                    if a = 2 then pdec2 l else 
+                    if a = 3 then penc (Suc (Read r)) l
+                    else l)"
+
+fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newright l r a  = (if a = 0 then Write 0 r
+                      else if a = 1 then Write 1 r
+                      else if a = 2 then penc (Suc (Read l)) r
+                      else if a = 3 then pdec2 r
+                      else r)"
+
+text {*
+  The @{text "Action"} function given on page 92 of B book, which is used to 
+  fetch Turing Machine intructions. In @{text "Action m q r"}, @{text "m"} is 
+  the code of the Turing Machine, @{text "q"} is the current state of 
+  Turing Machine, and @{text "r"} is the scanned cell of is the right tape. 
+*}
+
+fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "Actn n 0 = pdec1 (pdec1 n)"
+| "Actn n _ = pdec1 (pdec2 n)"
+
+fun Action :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Action m q c = (if q \<noteq> 0 \<and> within m (q - 1) then Actn (ldec m (q - 1)) c else 4)"
+
+fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "Newstat n 0 = pdec2 (pdec1 n)"
+| "Newstat n _ = pdec2 (pdec2 n)"
+
+fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newstate m q r = (if q \<noteq> 0 then Newstat (ldec m (q - 1)) r else 0)"
+
+fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
+  where
+  "Conf (q, l, r) = lenc [q, l, r]"
+
+fun State where
+  "State cf = ldec cf 0"
+
+fun Left where
+  "Left cf = ldec cf 1"
+
+fun Right where
+  "Right cf = ldec cf 2"
+
+text {*
+  @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of 
+  execution of TM coded as @{text "m"}. @{text Step} is a single step of the TM.
+*}
+
+fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 
+                     Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
+                     Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"
+
+fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Steps cf p 0  = cf"
+| "Steps cf p (Suc n) = Steps (Step cf p) p n"
+
+lemma Step_Steps_comm:
+  "Step (Steps cf p n) p = Steps (Step cf p) p n"
+by (induct n arbitrary: cf) (simp_all only: Steps.simps)
+
+
+text {* Decoding tapes back into numbers. *}
+
+definition Stknum :: "nat \<Rightarrow> nat"
+  where
+  "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)"
+
+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: cellnum.simps)
+apply(simp only: Stknum_up)
+apply(simp)
+done
+
+
+section  {* Standard Tapes *}
+
+definition
+  "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. 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)
+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. 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(auto)
+apply(rule_tac x="i" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Suc_eq_plus1 Suc_neq_Zero cellnum.cases cellnum.simps(1) leD less_trans linorder_neqE_nat)
+apply(auto)
+by (metis One_nat_def cellnum.cases cellnum.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(auto)
+apply(case_tac a)
+apply(auto)
+apply(case_tac a)
+apply(auto)
+by (metis Suc_less_eq nth_Cons_Suc)
+
+
+section {* Standard- and Final Configurations, the Universal Function *}
+
+text {*
+  @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 
+  is a stardard tape. 
+*}
+
+fun Std :: "nat \<Rightarrow> bool"
+  where
+  "Std cf = (left_std (Left cf) \<and> right_std (Right cf))"
+
+text{* 
+  @{text "Stop m cf k"} means that afer @{text k} steps of 
+  execution the TM coded by @{text m} and started in configuration
+  @{text cf} is in a stardard final configuration. *}
+
+fun Final :: "nat \<Rightarrow> bool"
+  where
+    "Final cf = (State cf = 0)"
+
+fun Stop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where
+  "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 
+  execute before reaching a stardard final configuration. This recursive 
+  function is the only one that uses unbounded minimization. So it is the 
+  only non-primitive recursive function needs to be used in the construction 
+  of the universal function @{text "UF"}. 
+*}
+
+fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Halt m cf = (LEAST k. Stop m cf k)"
+
+fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
+
+
+section {* The UF simulates Turing machines *}
+
+lemma Update_left_simulate:
+  shows "Newleft (Code_tp l) (Code_tp r) (actnum a) = Code_tp (fst (update a (l, r)))"
+apply(induct a)
+apply(simp_all)
+apply(case_tac l)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+done
+
+lemma Update_right_simulate:
+  shows "Newright (Code_tp l) (Code_tp r) (actnum a) = Code_tp (snd (update a (l, r)))"
+apply(induct a)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+apply(case_tac l)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+done
+
+lemma Fetch_state_simulate:
+  "tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cellnum c) = snd (fetch tp st c)"
+apply(induct tp st c rule: fetch.induct)
+apply(simp_all add: list_encode_inverse split: cell.split)
+done
+
+lemma Fetch_action_simulate:
+  "tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cellnum c) = actnum (fst (fetch tp st c))"
+apply(induct tp st c rule: fetch.induct)
+apply(simp_all add: list_encode_inverse split: cell.split)
+done
+
+lemma Read_simulate:
+  "Read (Code_tp tp) = cellnum (read tp)"
+apply(case_tac tp)
+apply(simp_all)
+done
+
+lemma misc:
+  "2 < (3::nat)"
+  "1 < (3::nat)"
+  "0 < (3::nat)" 
+  "length [x] = 1"
+  "length [x, y] = 2"
+  "length [x, y , z] = 3"
+  "[x, y, z] ! 0 = x"
+  "[x, y, z] ! 1 = y"
+  "[x, y, z] ! 2 = z"
+apply(simp_all)
+done
+
+lemma Step_simulate:
+  assumes "tm_wf tp"
+  shows "Step (Conf (Code_conf (st, l, r))) (Code_tprog tp) = Conf (Code_conf (step (st, l, r) tp))"
+apply(subst step.simps) 
+apply(simp only: Let_def)
+apply(subst Step.simps)
+apply(simp only: Conf.simps Code_conf.simps Right.simps Left.simps)
+apply(simp only: list_encode_inverse)
+apply(simp only: misc if_True Code_tp.simps)
+apply(simp only: prod_case_beta) 
+apply(subst Fetch_state_simulate[OF assms, symmetric])
+apply(simp only: State.simps)
+apply(simp only: list_encode_inverse)
+apply(simp only: misc if_True)
+apply(simp only: Read_simulate[simplified Code_tp.simps])
+apply(simp only: Fetch_action_simulate[OF assms])
+apply(simp only: Update_left_simulate[simplified Code_tp.simps])
+apply(simp only: Update_right_simulate[simplified Code_tp.simps])
+apply(case_tac "update (fst (fetch tp st (read r))) (l, r)")
+apply(simp only: Code_conf.simps)
+apply(simp only: Conf.simps)
+apply(simp)
+done
+
+lemma Steps_simulate:
+  assumes "tm_wf tp" 
+  shows "Steps (Conf (Code_conf cf)) (Code_tprog tp) n = Conf (Code_conf (steps cf tp n))"
+apply(induct n arbitrary: cf) 
+apply(simp)
+apply(simp only: Steps.simps steps.simps)
+apply(case_tac cf)
+apply(simp only: )
+apply(subst Step_simulate)
+apply(rule assms)
+apply(drule_tac x="step (a, b, c) tp" in meta_spec)
+apply(simp)
+done
+
+lemma Final_simulate:
+  "Final (Conf (Code_conf cf)) = is_final cf"
+by (case_tac cf) (simp)
+
+lemma Std_simulate:
+  "Std (Conf (Code_conf cf)) = std_tape cf" 
+apply(case_tac cf)
+apply(simp only: std_tape_def)
+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: left_std[symmetric] right_std[symmetric])
+apply(simp)
+by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc)
+
+
+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
+
+
+section {* Universal Function as Recursive Functions *}
+
+definition 
+  "rec_read = CN rec_ldec [Id 1 0, constn 0]"
+
+definition 
+  "rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]"
+
+definition
+    "rec_newleft =
+       (let cond0 = CN rec_eq [Id 3 2, constn 0] in 
+        let cond1 = CN rec_eq [Id 3 2, constn 1] in
+        let cond2 = CN rec_eq [Id 3 2, constn 2] in
+        let cond3 = CN rec_eq [Id 3 2, constn 3] in
+        let case3 = CN rec_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in
+        CN rec_if [cond0, Id 3 0,
+          CN rec_if [cond1, Id 3 0,  
+            CN rec_if [cond2, CN rec_pdec2 [Id 3 0],
+              CN rec_if [cond3, case3, Id 3 0]]]])"
+
+definition
+    "rec_newright =
+       (let cond0 = CN rec_eq [Id 3 2, constn 0] in
+        let cond1 = CN rec_eq [Id 3 2, constn 1] in
+        let cond2 = CN rec_eq [Id 3 2, constn 2] in
+        let cond3 = CN rec_eq [Id 3 2, constn 3] in
+        let case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in
+        CN rec_if [cond0, CN rec_write [constn 0, Id 3 1], 
+          CN rec_if [cond1, CN rec_write [constn 1, Id 3 1],
+            CN rec_if [cond2, case2,
+              CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])"
+
+definition
+  "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]])
+                           (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))"
+
+definition 
+  "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in 
+                 let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in
+                 let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
+                 in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])"
+
+definition
+  "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]])
+                              (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))"
+
+definition
+  "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in
+                   let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
+                   in CN rec_if [cond, if_branch, Z])"
+
+definition
+  "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]"
+
+definition 
+  "rec_state = CN rec_ldec [Id 1 0, Z]"
+
+definition
+  "rec_left = CN rec_ldec [Id 1 0, constn 1]"
+
+definition 
+  "rec_right = CN rec_ldec [Id 1 0, constn 2]"
+
+definition 
+  "rec_step = (let left = CN rec_left [Id 2 0] in
+               let right = CN rec_right [Id 2 0] in
+               let state = CN rec_state [Id 2 0] in
+               let read = CN rec_read [right] in
+               let action = CN rec_action [Id 2 1, state, read] in
+               let newstate = CN rec_newstate [Id 2 1, state, read] in
+               let newleft = CN rec_newleft [left, right, action] in
+               let newright = CN rec_newright [left, right, action] 
+               in CN rec_conf [newstate, newleft, newright])" 
+
+definition 
+  "rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])"
+
+definition
+  "rec_stknum = CN rec_minus 
+                  [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
+                   CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"
+
+definition
+  "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
+                    let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in
+                    let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
+                    let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
+                    let cond3 = CN (rec_all2_less 
+                                     (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) 
+                                [bound2, Id 2 0, Id 2 1] in
+                    CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])"
+
+definition
+  "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
+                   in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"
+
+definition
+  "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
+                          CN rec_right_std [CN rec_right [Id 1 0]]]"
+
+definition 
+  "rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]"
+
+definition 
+  "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
+               CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"
+
+definition
+  "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
+
+definition 
+  "rec_uf = CN rec_pred 
+              [CN rec_stknum 
+                  [CN rec_right 
+                     [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
+
+lemma read_lemma [simp]:
+  "rec_eval rec_read [x] = Read x"
+by (simp add: rec_read_def)
+
+lemma write_lemma [simp]:
+  "rec_eval rec_write [x, y] = Write x y"
+by (simp add: rec_write_def)
+
+lemma newleft_lemma [simp]:
+  "rec_eval rec_newleft [p, r, a] = Newleft p r a"
+by (simp add: rec_newleft_def Let_def)
+
+lemma newright_lemma [simp]:
+  "rec_eval rec_newright [p, r, a] = Newright p r a"
+by (simp add: rec_newright_def Let_def)
+
+lemma act_lemma [simp]:
+  "rec_eval rec_actn [n, c] = Actn n c"
+apply(simp add: rec_actn_def)
+apply(case_tac c)
+apply(simp_all)
+done
+
+lemma action_lemma [simp]:
+  "rec_eval rec_action [m, q, c] = Action m q c"
+by (simp add: rec_action_def)
+
+lemma newstat_lemma [simp]:
+  "rec_eval rec_newstat [n, c] = Newstat n c"
+apply(simp add: rec_newstat_def)
+apply(case_tac c)
+apply(simp_all)
+done
+
+lemma newstate_lemma [simp]:
+  "rec_eval rec_newstate [m, q, r] = Newstate m q r"
+by (simp add: rec_newstate_def)
+
+lemma conf_lemma [simp]:
+  "rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
+by(simp add: rec_conf_def)
+
+lemma state_lemma [simp]:
+  "rec_eval rec_state [cf] = State cf"
+by (simp add: rec_state_def)
+
+lemma left_lemma [simp]:
+  "rec_eval rec_left [cf] = Left cf"
+by (simp add: rec_left_def)
+
+lemma right_lemma [simp]:
+  "rec_eval rec_right [cf] = Right cf"
+by (simp add: rec_right_def)
+
+lemma step_lemma [simp]:
+  "rec_eval rec_step [cf, m] = Step cf m"
+by (simp add: Let_def rec_step_def)
+
+lemma steps_lemma [simp]:
+  "rec_eval rec_steps [n, cf, p] = Steps cf p n"
+by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
+
+lemma stknum_lemma [simp]:
+  "rec_eval rec_stknum [z] = Stknum z"
+by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
+
+lemma left_std_lemma [simp]:
+  "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
+by (simp add: Let_def rec_left_std_def left_std_def)
+
+lemma right_std_lemma [simp]:
+  "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
+by (simp add: Let_def rec_right_std_def right_std_def)
+
+lemma std_lemma [simp]:
+  "rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
+by (simp add: rec_std_def)
+
+lemma final_lemma [simp]:
+  "rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
+by (simp add: rec_final_def)
+
+lemma stop_lemma [simp]:
+  "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
+by (simp add: Let_def rec_stop_def)
+
+lemma halt_lemma [simp]:
+  "rec_eval rec_halt [m, cf] = Halt m cf"
+by (simp add: rec_halt_def del: Stop.simps)
+
+lemma uf_lemma [simp]:
+  "rec_eval rec_uf [m, cf] = UF m cf"
+by (simp add: rec_uf_def)
+
+(* value "size rec_uf" *)
+end
+