# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369227020 -3600
# Node ID 4524c5edcafb79696fd9b01166d66b6b9ba28947
# Parent  32c5e8d1f6ffea701a223706e9c8b498be62d4c7
moved new theries into a separate directory

diff -r 32c5e8d1f6ff -r 4524c5edcafb thys/Recs.thy
--- a/thys/Recs.thy	Tue May 21 13:50:15 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,828 +0,0 @@
-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"
-
-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"
-
-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) (xs @ [x])"
-| 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 {* Recursive Function Definitions *}
-
-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 = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
-
-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]))"
-
-
-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 [constn 1, 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]"
-
-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]"
-
-text {* Sigma and Accum for function with one and two arguments *}
-
-definition 
-  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
-
-definition 
-  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-
-definition 
-  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
-
-definition 
-  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-
-text {* Bounded quantifiers for one and two arguments *}
-
-definition
-  "rec_all1 f = CN rec_sign [rec_accum1 f]"
-
-definition
-  "rec_all2 f = CN rec_sign [rec_accum2 f]"
-
-definition
-  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
-
-definition
-  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
-
-text {* Dvd, Quotient, Modulo *}
-
-definition 
-  "rec_dvd = 
-     rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"  
-
-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)"
-
-definition
-  "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
-
-
-section {* Prime Numbers *}
-
-definition 
-  "rec_prime = 
-    (let conj1 = CN rec_less [constn 1, Id 1 0] in
-     let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
-     let imp   = CN rec_imp [rec_dvd, disj] in
-     let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
-     CN rec_conj [conj1, conj2])"
-
-
-section {* Correctness of Recursive Functions *}
-
-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_lemma [simp]: 
-  "rec_eval rec_fact [x] = fact x"
-by (induct x) (simp_all 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)
-
-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 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)
-
-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)
-
-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 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 dvd_alt_def:
-  fixes x y k:: nat
-  shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)"
-apply(auto simp add: dvd_def)
-apply(case_tac x)
-apply(auto)
-done
-
-lemma dvd_lemma [simp]:
-  "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
-unfolding dvd_alt_def
-by (auto simp add: rec_dvd_def)
-
-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"
-apply(induct y)
-apply(auto)
-done
-
-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)
-
-lemma rem_lemma [simp]:
-  shows "rec_eval rec_mod [y, x] = y mod x"
-by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
-
-
-section {* Prime Numbers *}
-
-lemma prime_alt_def:
-  fixes p::nat
-  shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
-apply(auto simp add: prime_nat_def dvd_def)
-apply(drule_tac x="k" in spec)
-apply(auto)
-done
-
-lemma prime_lemma [simp]: 
-  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
-by (auto simp add: rec_prime_def Let_def prime_alt_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 (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 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 (constn 0) (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]"
-
-lemma triangle_lemma [simp]:
-  "rec_eval rec_triangle [x] = triangle x"
-by (simp add: rec_triangle_def triangle_def)
- 
-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 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) 
-
-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)
-
-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 *}
-
-definition
-  "rec_lg = 
-     (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in
-      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
-      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
-      in CN rec_ifz [cond, Z, max])"
-
-definition
-  "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)"
-
-lemma lg_lemma [simp]:
-  "rec_eval rec_lg [x, y] = Lg x y"
-by (simp add: rec_lg_def Lg_def Let_def)
-
-definition
-  "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)"
-
-definition
-  "rec_lo = 
-     (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
-      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
-      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
-      in CN rec_ifz [cond, Z, max])"
-
-lemma lo_lemma [simp]:
-  "rec_eval rec_lo [x, y] = Lo x y"
-by (simp add: rec_lo_def Lo_def Let_def)
-
-section {* NextPrime number function *}
-
-text {* 
-  @{text "NextPrime x"} returns the first prime number after @{text "x"};
-  @{text "Pi i"} returns the i-th prime number. *}
-
-definition 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 NextPrime_def)
-
-lemma NextPrime_simps [simp]:
-  shows "NextPrime 2 = 3"
-  and   "NextPrime 3 = 5"
-apply(simp_all add: NextPrime_def)
-apply(rule Least_equality)
-apply(auto)
-apply(eval)
-apply(rule Least_equality)
-apply(auto)
-apply(eval)
-apply(case_tac "y = 4")
-apply(auto)
-done
-
-fun Pi :: "nat \<Rightarrow> nat"
-  where
-  "Pi 0 = 2" |
-  "Pi (Suc x) = NextPrime (Pi x)"
-
-lemma Pi_simps [simp]:
-  shows "Pi 1 = 3"
-  and   "Pi 2 = 5"
-using NextPrime_simps
-by(simp_all add: numeral_eq_Suc One_nat_def)
-
-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)
-
-end
-
diff -r 32c5e8d1f6ff -r 4524c5edcafb thys/Turing2.thy
--- a/thys/Turing2.thy	Tue May 21 13:50:15 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* 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
-
diff -r 32c5e8d1f6ff -r 4524c5edcafb thys/UF_Rec.thy
--- a/thys/UF_Rec.thy	Tue May 21 13:50:15 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,589 +0,0 @@
-theory UF_Rec
-imports Recs Turing2
-begin
-
-section {* Coding of Turing Machines and tapes*}
-
-text {*
-  The purpose of this section is to construct the coding function of Turing 
-  Machine, which is going to be named @{text "code"}. *}
-
-text {* Encoding of actions as numbers *}
-
-fun action_num :: "action \<Rightarrow> nat"
-  where
-  "action_num W0 = 0"
-| "action_num W1 = 1"
-| "action_num L  = 2"
-| "action_num R  = 3"
-| "action_num Nop = 4"
-
-fun cell_num :: "cell \<Rightarrow> nat" where
-  "cell_num Bk = 0"
-| "cell_num Oc = 1"
-
-fun code_tp :: "cell list \<Rightarrow> nat list"
-  where
-  "code_tp [] = []"
-| "code_tp (c # tp) = (cell_num c) # code_tp tp"
-
-fun Code_tp where
-  "Code_tp tp = lenc (code_tp tp)"
-
-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 (action_num (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 {* Universal Function in HOL *}
-
-
-text {* Scanning and writing the right tape *}
-
-fun Scan where
-  "Scan r = ldec r 0"
-
-fun Write where
-  "Write n r = penc n (pdec2 r)"
-
-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}.
-*}
-
-fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Newleft p r a = (if a = 0 \<or> a = 1 then p else 
-                    if a = 2 then pdec2 p else 
-                    if a = 3 then penc (pdec1 r) p
-                    else p)"
-
-fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Newright p r a  = (if a = 0 then Write 0 r
-                      else if a = 1 then Write 1 r
-                      else if a = 2 then penc (pdec1 p) r
-                      else if a = 3 then pdec2 r
-                      else r)"
-
-text {*
-  The @{text "Actn"} function given on page 92 of B book, which is used to 
-  fetch Turing Machine intructions. In @{text "Actn 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 Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Actn m q r = (if q \<noteq> 0 \<and> within m q then (actn (ldec m (q - 1)) r) else 4)"
-
-fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-  "newstat n 0 = pdec2 (pdec1 n)"
-| "newstat n _ = pdec2 (pdec2 n)"
-
-fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Newstat 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 Stat where
-  (*"Stat c = (if c = 0 then 0 else ldec c 0)"*)
-  "Stat c = ldec c 0"
-
-fun Left where
-  "Left c = ldec c 1"
-
-fun Right where
-  "Right c = ldec c 2"
-
-fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Newconf c m = Conf (Newstat m (Stat c) (Scan (Right c)), 
-                       (Newleft (Left c) (Right c) (Actn m (Stat c) (Scan (Right c))),
-                        Newright (Left c) (Right c) (Actn m (Stat c) (Scan (Right c)))))"
-
-text {*
-  @{text "Step k m r"} computes the TM configuration after @{text "k"} steps of execution
-  of TM coded as @{text "m"} starting from the initial configuration where the left 
-  number equals @{text "0"}, right number equals @{text "r"}. *}
-
-fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Steps cf p 0  = cf"
-| "Steps cf p (Suc n) = Steps (Newconf cf p) p n"
-
-text {*
-  @{text "Nstd c"} returns true if the configuration coded 
-  by @{text "c"} is not a stardard final configuration. *}
-
-fun Nstd :: "nat \<Rightarrow> bool"
-  where
-  "Nstd c = (Stat c \<noteq> 0)"
-
--- "tape conditions are missing"
-
-text{* 
-  @{text "Nostop t m r"} means that afer @{text "t"} steps of 
-  execution the TM coded by @{text "m"} is not at a stardard 
-  final configuration. *}
-
-fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-  where
-  "Nostop m l r = Nstd (Conf (m, (l, r)))"
-
-text{*
-  @{text "rec_halt"} is the recursive function calculating the steps a TM needs to 
-  execute before to reach a stardard final configuration. This recursive function is 
-  the only one using @{text "Mn"} combinator. So it is the only non-primitive recursive 
-  function needs to be used in the construction of the universal function @{text "rec_uf"}. 
-*}
-
-fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Halt m r = (LEAST t. \<not> Nostop t m r)"
-
-(*
-fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "UF c m = (Right (Conf (Halt c m) c m))"
-*)
-
-text {* reading the value is missing *}
-
-section {* The UF can simulate Turing machines *}
-
-lemma Update_left_simulate:
-  shows "Newleft (Code_tp l) (Code_tp r) (action_num 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) (action_num 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:
-  "\<lbrakk>tm_wf tp\<rbrakk> \<Longrightarrow> Newstat (Code_tprog tp) st (cell_num 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:
-  "\<lbrakk>tm_wf tp; st \<le> length tp\<rbrakk> \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (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 Scan_simulate:
-  "Scan (Code_tp tp) = cell_num (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 New_conf_simulate:
-  assumes "tm_wf tp" "st \<le> length tp"
-  shows "Newconf (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 Newconf.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: Stat.simps)
-apply(simp only: list_encode_inverse)
-apply(simp only: misc if_True)
-apply(simp only: Scan_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 Step_simulate:
-  assumes "tm_wf tp" "fst cf \<le> length 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 New_conf_simulate)
-apply(rule assms)
-defer
-apply(drule_tac x="step (a, b, c) tp" in meta_spec)
-apply(simp)
-
-
-section {* Coding of Turing Machines *}
-
-text {*
-  The purpose of this section is to construct the coding function of Turing 
-  Machine, which is going to be named @{text "code"}. *}
-
-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"
-
-lemma bl2nat_double [simp]: 
-  "bl2nat xs (Suc n) = 2 * bl2nat xs n"
-apply(induct xs arbitrary: n)
-apply(auto)
-apply(case_tac a)
-apply(auto)
-done
-
-lemma bl2nat_simps1 [simp]: 
-  shows "bl2nat (Bk \<up> y) n = 0"
-by (induct y) (auto)
-
-lemma bl2nat_simps2 [simp]: 
-  shows "bl2nat (Oc \<up> y) 0 = 2 ^ y - 1"
-apply(induct y)
-apply(auto)
-apply(case_tac "(2::nat)^ y")
-apply(auto)
-done
-
-fun Trpl_code :: "config \<Rightarrow> nat"
-  where
-  "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
-
-
-
-fun block_map :: "cell \<Rightarrow> nat"
-  where
-  "block_map Bk = 0"
-| "block_map Oc = 1"
-
-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)"
-
-
-
-section {* Universal Function as Recursive Functions *}
-
-definition 
-  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
-
-fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_listsum2 vl 0 = CN Z [Id vl 0]"
-| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"
-
-fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_strt' xs 0 = Z"
-| "rec_strt' xs (Suc n) = 
-      (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in
-       let t1 = CN rec_power [constn 2, dbound] in
-       let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in
-       CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"
-
-fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
-  where
-  "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"
-
-fun rec_strt :: "nat \<Rightarrow> recf"
-  where
-  "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"
-
-definition 
-  "rec_scan = CN rec_mod [Id 1 0, constn 2]"
-
-definition
-    "rec_newleft =
-       (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], 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_add [CN rec_mult [constn 2, Id 3 0], 
-                                CN rec_mod [Id 3 1, constn 2]] in
-        CN rec_if [cond1, Id 3 0, 
-          CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
-            CN rec_if [cond3, case3, Id 3 0]]])"
-
-definition
-    "rec_newright =
-       (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in
-        let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
-        let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
-        let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     
-                                CN rec_mod [Id 3 0, constn 2]] in
-        let case3 = CN rec_quo [Id 2 1, constn 2] in
-        CN rec_if [condn 0, case0, 
-          CN rec_if [condn 1, case1,
-            CN rec_if [condn 2, case2,
-              CN rec_if [condn 3, case3, Id 3 1]]]])"
-
-definition 
-  "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
-               let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in
-               let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
-               in CN rec_if [Id 3 1, entry, constn 4])"
-
-definition rec_newstat :: "recf"
-  where
-  "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
-                  let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in
-                  let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
-                  in CN rec_if [Id 3 1, entry, Z])"
-
-definition 
-  "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"
-
-definition
-  "rec_left = rec_pdec1"
-
-definition 
-  "rec_right = CN rec_pdec2 [rec_pdec1]"
-
-definition 
-  "rec_stat = CN rec_pdec2 [rec_pdec2]"
-
-definition 
-  "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
-                  let left = CN rec_left [Id 2 1] in
-                  let right = CN rec_right [Id 2 1] in
-                  let stat = CN rec_stat [Id 2 1] in
-                  let one = CN rec_newleft [left, right, act] in
-                  let two = CN rec_newstat [Id 2 0, stat, right] in
-                  let three = CN rec_newright [left, right, act]
-                  in CN rec_trpl [one, two, three])" 
-
-definition 
-  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
-                 (CN rec_newconf [Id 4 2 , Id 4 1])"
-
-definition 
-  "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in
-               let disj2 = CN rec_noteq [rec_left, constn 0] in
-               let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in
-               let disj3 = CN rec_noteq [rec_right, rhs] in
-               let disj4 = CN rec_eq [rec_right, constn 0] in
-               CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"
-
-definition 
-  "rec_nostop = CN rec_nstd [rec_conf]"
-
-definition 
-  "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
-
-definition 
-  "rec_halt = MN rec_nostop" 
-
-definition 
-  "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
-
-
-
-section {* Correctness Proofs for Recursive Functions *}
-
-lemma entry_lemma [simp]:
-  "rec_eval rec_entry [sr, i] = Entry sr i"
-by(simp add: rec_entry_def)
-
-lemma listsum2_lemma [simp]: 
-  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
-by (induct n) (simp_all)
-
-lemma strt'_lemma [simp]:
-  "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"
-by (induct n) (simp_all add: Let_def)
-
-lemma map_suc:
-  "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"
-proof -
-  have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)
-  then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp
-  also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp
-  also have "... = map Suc xs" by (simp add: map_nth)
-  finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .
-qed
-
-lemma strt_lemma [simp]: 
-  "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"
-by (simp add: comp_def map_suc[symmetric])
-
-lemma scan_lemma [simp]: 
-  "rec_eval rec_scan [r] = r mod 2"
-by(simp add: rec_scan_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 actn_lemma [simp]:
-  "rec_eval rec_actn [m, q, r] = Actn m q r"
-by (simp add: rec_actn_def)
-
-lemma newstat_lemma [simp]: 
-  "rec_eval rec_newstat [m, q, r] = Newstat m q r"
-by (simp add: rec_newstat_def)
-
-lemma trpl_lemma [simp]: 
-  "rec_eval rec_trpl [p, q, r] = Trpl p q r"
-apply(simp)
-apply (simp add: rec_trpl_def)
-
-lemma left_lemma [simp]:
-  "rec_eval rec_left [c] = Left c" 
-by(simp add: rec_left_def)
-
-lemma right_lemma [simp]:
-  "rec_eval rec_right [c] = Right c" 
-by(simp add: rec_right_def)
-
-lemma stat_lemma [simp]:
-  "rec_eval rec_stat [c] = Stat c" 
-by(simp add: rec_stat_def)
-
-lemma newconf_lemma [simp]: 
-  "rec_eval rec_newconf [m, c] = Newconf m c"
-by (simp add: rec_newconf_def Let_def)
-
-lemma conf_lemma [simp]: 
-  "rec_eval rec_conf [k, m, r] = Conf k m r"
-by(induct k) (simp_all add: rec_conf_def)
-
-lemma nstd_lemma [simp]:
-  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
-by(simp add: rec_nstd_def)
-
-lemma nostop_lemma [simp]:
-  "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" 
-by (simp add: rec_nostop_def)
-
-lemma value_lemma [simp]:
-  "rec_eval rec_value [x] = Value x"
-by (simp add: rec_value_def)
-
-lemma halt_lemma [simp]:
-  "rec_eval rec_halt [m, r] = Halt m r"
-by (simp add: rec_halt_def)
-
-lemma uf_lemma [simp]:
-  "rec_eval rec_uf [m, r] = UF m r"
-by (simp add: rec_uf_def)
-
-
-subsection {* Relating interperter functions to the execution of TMs *}
-
-lemma rec_step: 
-  assumes "(\<lambda> (s, l, r). s \<le> length tp div 2) c"
-  shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)"
-apply(cases c)
-apply(simp only: Trpl_code.simps)
-apply(simp only: Let_def step.simps)
-apply(case_tac "fetch tp (a - 0) (read ca)")
-apply(simp only: prod.cases)
-apply(case_tac "update aa (b, ca)")
-apply(simp only: prod.cases)
-apply(simp only: Trpl_code.simps)
-apply(simp only: Newconf.simps)
-apply(simp only: Left.simps)
-oops
-
-lemma rec_steps:
-  assumes "tm_wf0 tp"
-  shows "Trpl_code (steps0 (1, Bk \<up> l, <lm>) tp stp) = Conf stp (Code tp) (bl2wc (<lm>))"
-apply(induct stp)
-apply(simp)
-apply(simp)
-oops
-
-
-lemma F_correct: 
-  assumes tm: "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)"
-proof -
-  from least_steps[OF tm] 
-  obtain stp_least where
-    before: "\<forall>stp' < stp_least. \<not> is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" and
-    after:  "\<forall>stp' \<ge> stp_least. is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" by blast
-  have "Halt (Code tp) (bl2wc (<lm>)) = stp_least" sorry
-  show ?thesis
-    apply(simp only: uf_lemma)
-    apply(simp only: UF.simps)
-    apply(simp only: Halt.simps)
-    oops
-
-
-end
-
diff -r 32c5e8d1f6ff -r 4524c5edcafb thys2/Recs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Recs.thy	Wed May 22 13:50:20 2013 +0100
@@ -0,0 +1,863 @@
+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"
+
+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"
+
+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) (xs @ [x])"
+| 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 {* Recursive Function Definitions *}
+
+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 = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+
+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]))"
+
+
+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 [constn 1, 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]"
+
+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]"
+
+text {* Sigma and Accum for function with one and two arguments *}
+
+definition 
+  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
+
+definition 
+  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+
+definition 
+  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
+
+definition 
+  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+
+text {* Bounded quantifiers for one and two arguments *}
+
+definition
+  "rec_all1 f = CN rec_sign [rec_accum1 f]"
+
+definition
+  "rec_all2 f = CN rec_sign [rec_accum2 f]"
+
+definition
+  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
+
+definition
+  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
+
+text {* Dvd, Quotient, Modulo *}
+
+definition 
+  "rec_dvd = 
+     rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"  
+
+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)"
+
+definition
+  "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
+
+
+section {* Prime Numbers *}
+
+definition 
+  "rec_prime = 
+    (let conj1 = CN rec_less [constn 1, Id 1 0] in
+     let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
+     let imp   = CN rec_imp [rec_dvd, disj] in
+     let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
+     CN rec_conj [conj1, conj2])"
+
+
+section {* Correctness of Recursive Functions *}
+
+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_lemma [simp]: 
+  "rec_eval rec_fact [x] = fact x"
+by (induct x) (simp_all 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)
+
+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 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)
+
+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)
+
+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 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 dvd_alt_def:
+  fixes x y k:: nat
+  shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)"
+apply(auto simp add: dvd_def)
+apply(case_tac x)
+apply(auto)
+done
+
+lemma dvd_lemma [simp]:
+  "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
+unfolding dvd_alt_def
+by (auto simp add: rec_dvd_def)
+
+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"
+apply(induct y)
+apply(auto)
+done
+
+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)
+
+lemma rem_lemma [simp]:
+  shows "rec_eval rec_mod [y, x] = y mod x"
+by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
+
+
+section {* Prime Numbers *}
+
+lemma prime_alt_def:
+  fixes p::nat
+  shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
+apply(auto simp add: prime_nat_def dvd_def)
+apply(drule_tac x="k" in spec)
+apply(auto)
+done
+
+lemma prime_lemma [simp]: 
+  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
+by (auto simp add: rec_prime_def Let_def prime_alt_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 (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 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 (constn 0) (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]"
+
+lemma triangle_lemma [simp]:
+  "rec_eval rec_triangle [x] = triangle x"
+by (simp add: rec_triangle_def triangle_def)
+ 
+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 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) 
+
+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)
+
+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
+
+lemma lenc_length_le:
+  "length xs \<le> lenc xs"  
+by (induct xs) (simp_all add: prod_encode_def)
+
+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
+
+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)
+
+section {* Discrete Logarithms *}
+
+definition
+  "rec_lg = 
+     (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in
+      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
+      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
+      in CN rec_ifz [cond, Z, max])"
+
+definition
+  "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)"
+
+lemma lg_lemma [simp]:
+  "rec_eval rec_lg [x, y] = Lg x y"
+by (simp add: rec_lg_def Lg_def Let_def)
+
+definition
+  "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)"
+
+definition
+  "rec_lo = 
+     (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
+      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
+      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
+      in CN rec_ifz [cond, Z, max])"
+
+lemma lo_lemma [simp]:
+  "rec_eval rec_lo [x, y] = Lo x y"
+by (simp add: rec_lo_def Lo_def Let_def)
+
+section {* NextPrime number function *}
+
+text {* 
+  @{text "NextPrime x"} returns the first prime number after @{text "x"};
+  @{text "Pi i"} returns the i-th prime number. *}
+
+definition 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 NextPrime_def)
+
+lemma NextPrime_simps [simp]:
+  shows "NextPrime 2 = 3"
+  and   "NextPrime 3 = 5"
+apply(simp_all add: NextPrime_def)
+apply(rule Least_equality)
+apply(auto)
+apply(eval)
+apply(rule Least_equality)
+apply(auto)
+apply(eval)
+apply(case_tac "y = 4")
+apply(auto)
+done
+
+fun Pi :: "nat \<Rightarrow> nat"
+  where
+  "Pi 0 = 2" |
+  "Pi (Suc x) = NextPrime (Pi x)"
+
+lemma Pi_simps [simp]:
+  shows "Pi 1 = 3"
+  and   "Pi 2 = 5"
+using NextPrime_simps
+by(simp_all add: numeral_eq_Suc One_nat_def)
+
+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)
+
+end
+
diff -r 32c5e8d1f6ff -r 4524c5edcafb thys2/Turing2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Turing2.thy	Wed May 22 13:50:20 2013 +0100
@@ -0,0 +1,121 @@
+(* 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 tm 0 b = (Nop, 0)"
+| "fetch tm (Suc s) b = 
+     (case nth_of tm 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 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 *)
+
+fun 
+  tm_wf :: "tprog \<Rightarrow> bool"
+where
+  "tm_wf p = (1 \<le> length p \<and> (\<forall>((_, s1), (_, s2)) \<in> set p. s1 \<le> length p \<and> s2 \<le> length p))"
+
+(* short-hand notation for tapes *)
+
+abbreviation cell_replicate :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
+  where "x \<up> n \<equiv> replicate n x"
+
+class tape_of =
+  fixes tape_of :: "'a \<Rightarrow> cell list" ("<_>" [64] 67)
+
+instantiation nat :: tape_of 
+begin
+
+fun tape_of_nat where 
+  "<(n::nat)> = Oc \<up> (Suc n)"
+
+instance ..
+
+end
+
+instantiation list :: (tape_of) tape_of 
+begin
+
+fun tape_of_list :: "'a list \<Rightarrow> cell list" 
+  where 
+  "<[]> = []" |
+  "<[n]> = <n>" |
+  "<n # ns> = <n> @ [Bk] @ <ns>"
+
+instance ..
+
+end
+
+instantiation prod :: (tape_of, tape_of) tape_of 
+begin
+
+fun tape_of_prod :: "'a \<times> 'b \<Rightarrow> cell list" 
+  where 
+  "<(n, m)> = <n> @ [Bk] @ <m>" 
+
+instance ..
+
+end
+
+definition 
+  "std_tape tp \<equiv> \<exists>k l (n::nat). tp = (Bk \<up> k, <n> @ Bk \<up> l)"
+
+
+end
+
diff -r 32c5e8d1f6ff -r 4524c5edcafb thys2/UF_Rec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/UF_Rec.thy	Wed May 22 13:50:20 2013 +0100
@@ -0,0 +1,574 @@
+theory UF_Rec
+imports Recs Turing2
+begin
+
+section {* Coding of Turing Machines and tapes*}
+
+text {*
+  The purpose of this section is to construct the coding function of Turing 
+  Machine, which is going to be named @{text "code"}. *}
+
+text {* Encoding of actions as numbers *}
+
+fun action_num :: "action \<Rightarrow> nat"
+  where
+  "action_num W0 = 0"
+| "action_num W1 = 1"
+| "action_num L  = 2"
+| "action_num R  = 3"
+| "action_num Nop = 4"
+
+fun cell_num :: "cell \<Rightarrow> nat" where
+  "cell_num Bk = 0"
+| "cell_num Oc = 1"
+
+fun code_tp :: "cell list \<Rightarrow> nat list"
+  where
+  "code_tp [] = []"
+| "code_tp (c # tp) = (cell_num c) # code_tp tp"
+
+fun Code_tp where
+  "Code_tp tp = lenc (code_tp tp)"
+
+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 (action_num (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 {* 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}.
+*}
+
+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 "Actn"} function given on page 92 of B book, which is used to 
+  fetch Turing Machine intructions. In @{text "Actn 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 Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Actn m q r = (if q \<noteq> 0 \<and> within m (q - 1) then (actn (ldec m (q - 1)) r) else 4)"
+
+fun newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "newstate n 0 = pdec2 (pdec1 n)"
+| "newstate n _ = pdec2 (pdec2 n)"
+
+fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newstate m q r = (if q \<noteq> 0 then (newstate (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"
+
+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)))))"
+
+text {*
+  @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution
+  of TM coded as @{text "m"}. 
+*}
+
+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"
+
+text {*
+  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"
+
+lemma Binnum_simulate1:
+  "(Binnum z = 0) \<longleftrightarrow> (\<forall>i \<in> {..<enclen z}. ldec z i = 0)"
+by(auto simp add: Binnum_def)
+
+lemma Binnum_simulate2:
+  "(\<forall>i \<in> {..<enclen (Code_tp tp)}. ldec (Code_tp tp) i = 0) \<longleftrightarrow> (\<exists>k. tp = Bk \<up> k)"
+apply(induct tp)
+apply(simp)
+apply(simp)
+apply(simp add: lessThan_Suc)
+apply(case_tac a)
+apply(simp)
+defer
+apply(simp)
+oops
+
+apply(simp add: Binnum_def)
+
+text {*
+  @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 
+  is a stardard tape. 
+*}
+
+fun Std :: "nat \<Rightarrow> bool"
+  where
+  "Std cf = (Binnum (Left cf) = 0 \<and> 
+            (\<exists>x\<le>(enclen (Right cf)). Binnum (Right cf) = 2 ^ x))"
+
+text{* 
+  @{text "Nostop m cf k"} means that afer @{text k} steps of 
+  execution the TM coded by @{text m} and started in configuration
+  @{text cf} is not at a stardard final configuration. *}
+
+fun Final :: "nat \<Rightarrow> bool"
+  where
+    "Final cf = (State cf = 0)"
+
+fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where
+  "Nostop m cf k = (Final (Steps cf m k) \<and> \<not> 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. \<not> Nostop m cf k)"
+
+fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "UF m cf = Stknum (Right (Steps m cf (Halt m cf)))"
+
+section {* The UF can simulate Turing machines *}
+
+lemma Update_left_simulate:
+  shows "Newleft (Code_tp l) (Code_tp r) (action_num 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) (action_num 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 (cell_num 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> Actn (Code_tprog tp) st (cell_num c) = action_num (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) = cell_num (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 (snd cf)" 
+apply(case_tac cf)
+apply(simp add: std_tape_def del: Std.simps)
+apply(subst Std.simps)
+
+(* UNTIL HERE *)
+
+
+section {* Universal Function as Recursive Functions *}
+
+definition 
+  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
+
+fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
+  where
+  "rec_listsum2 vl 0 = CN Z [Id vl 0]"
+| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"
+
+fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"
+  where
+  "rec_strt' xs 0 = Z"
+| "rec_strt' xs (Suc n) = 
+      (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in
+       let t1 = CN rec_power [constn 2, dbound] in
+       let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in
+       CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"
+
+fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
+  where
+  "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"
+
+fun rec_strt :: "nat \<Rightarrow> recf"
+  where
+  "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"
+
+definition 
+  "rec_scan = CN rec_mod [Id 1 0, constn 2]"
+
+definition
+    "rec_newleft =
+       (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], 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_add [CN rec_mult [constn 2, Id 3 0], 
+                                CN rec_mod [Id 3 1, constn 2]] in
+        CN rec_if [cond1, Id 3 0, 
+          CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
+            CN rec_if [cond3, case3, Id 3 0]]])"
+
+definition
+    "rec_newright =
+       (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in
+        let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
+        let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
+        let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     
+                                CN rec_mod [Id 3 0, constn 2]] in
+        let case3 = CN rec_quo [Id 2 1, constn 2] in
+        CN rec_if [condn 0, case0, 
+          CN rec_if [condn 1, case1,
+            CN rec_if [condn 2, case2,
+              CN rec_if [condn 3, case3, Id 3 1]]]])"
+
+definition 
+  "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
+               let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in
+               let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
+               in CN rec_if [Id 3 1, entry, constn 4])"
+
+definition rec_newstat :: "recf"
+  where
+  "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
+                  let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in
+                  let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
+                  in CN rec_if [Id 3 1, entry, Z])"
+
+definition 
+  "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"
+
+definition
+  "rec_left = rec_pdec1"
+
+definition 
+  "rec_right = CN rec_pdec2 [rec_pdec1]"
+
+definition 
+  "rec_stat = CN rec_pdec2 [rec_pdec2]"
+
+definition 
+  "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
+                  let left = CN rec_left [Id 2 1] in
+                  let right = CN rec_right [Id 2 1] in
+                  let stat = CN rec_stat [Id 2 1] in
+                  let one = CN rec_newleft [left, right, act] in
+                  let two = CN rec_newstat [Id 2 0, stat, right] in
+                  let three = CN rec_newright [left, right, act]
+                  in CN rec_trpl [one, two, three])" 
+
+definition 
+  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
+                 (CN rec_newconf [Id 4 2 , Id 4 1])"
+
+definition 
+  "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in
+               let disj2 = CN rec_noteq [rec_left, constn 0] in
+               let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in
+               let disj3 = CN rec_noteq [rec_right, rhs] in
+               let disj4 = CN rec_eq [rec_right, constn 0] in
+               CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"
+
+definition 
+  "rec_nostop = CN rec_nstd [rec_conf]"
+
+definition 
+  "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
+
+definition 
+  "rec_halt = MN rec_nostop" 
+
+definition 
+  "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
+
+
+
+section {* Correctness Proofs for Recursive Functions *}
+
+lemma entry_lemma [simp]:
+  "rec_eval rec_entry [sr, i] = Entry sr i"
+by(simp add: rec_entry_def)
+
+lemma listsum2_lemma [simp]: 
+  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
+by (induct n) (simp_all)
+
+lemma strt'_lemma [simp]:
+  "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"
+by (induct n) (simp_all add: Let_def)
+
+lemma map_suc:
+  "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"
+proof -
+  have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)
+  then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp
+  also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp
+  also have "... = map Suc xs" by (simp add: map_nth)
+  finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .
+qed
+
+lemma strt_lemma [simp]: 
+  "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"
+by (simp add: comp_def map_suc[symmetric])
+
+lemma scan_lemma [simp]: 
+  "rec_eval rec_scan [r] = r mod 2"
+by(simp add: rec_scan_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 actn_lemma [simp]:
+  "rec_eval rec_actn [m, q, r] = Actn m q r"
+by (simp add: rec_actn_def)
+
+lemma newstat_lemma [simp]: 
+  "rec_eval rec_newstat [m, q, r] = Newstat m q r"
+by (simp add: rec_newstat_def)
+
+lemma trpl_lemma [simp]: 
+  "rec_eval rec_trpl [p, q, r] = Trpl p q r"
+apply(simp)
+apply (simp add: rec_trpl_def)
+
+lemma left_lemma [simp]:
+  "rec_eval rec_left [c] = Left c" 
+by(simp add: rec_left_def)
+
+lemma right_lemma [simp]:
+  "rec_eval rec_right [c] = Right c" 
+by(simp add: rec_right_def)
+
+lemma stat_lemma [simp]:
+  "rec_eval rec_stat [c] = Stat c" 
+by(simp add: rec_stat_def)
+
+lemma newconf_lemma [simp]: 
+  "rec_eval rec_newconf [m, c] = Newconf m c"
+by (simp add: rec_newconf_def Let_def)
+
+lemma conf_lemma [simp]: 
+  "rec_eval rec_conf [k, m, r] = Conf k m r"
+by(induct k) (simp_all add: rec_conf_def)
+
+lemma nstd_lemma [simp]:
+  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
+by(simp add: rec_nstd_def)
+
+lemma nostop_lemma [simp]:
+  "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" 
+by (simp add: rec_nostop_def)
+
+lemma value_lemma [simp]:
+  "rec_eval rec_value [x] = Value x"
+by (simp add: rec_value_def)
+
+lemma halt_lemma [simp]:
+  "rec_eval rec_halt [m, r] = Halt m r"
+by (simp add: rec_halt_def)
+
+lemma uf_lemma [simp]:
+  "rec_eval rec_uf [m, r] = UF m r"
+by (simp add: rec_uf_def)
+
+
+subsection {* Relating interperter functions to the execution of TMs *}
+
+lemma rec_step: 
+  assumes "(\<lambda> (s, l, r). s \<le> length tp div 2) c"
+  shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)"
+apply(cases c)
+apply(simp only: Trpl_code.simps)
+apply(simp only: Let_def step.simps)
+apply(case_tac "fetch tp (a - 0) (read ca)")
+apply(simp only: prod.cases)
+apply(case_tac "update aa (b, ca)")
+apply(simp only: prod.cases)
+apply(simp only: Trpl_code.simps)
+apply(simp only: Newconf.simps)
+apply(simp only: Left.simps)
+oops
+
+lemma rec_steps:
+  assumes "tm_wf0 tp"
+  shows "Trpl_code (steps0 (1, Bk \<up> l, <lm>) tp stp) = Conf stp (Code tp) (bl2wc (<lm>))"
+apply(induct stp)
+apply(simp)
+apply(simp)
+oops
+
+
+lemma F_correct: 
+  assumes tm: "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)"
+proof -
+  from least_steps[OF tm] 
+  obtain stp_least where
+    before: "\<forall>stp' < stp_least. \<not> is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" and
+    after:  "\<forall>stp' \<ge> stp_least. is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" by blast
+  have "Halt (Code tp) (bl2wc (<lm>)) = stp_least" sorry
+  show ?thesis
+    apply(simp only: uf_lemma)
+    apply(simp only: UF.simps)
+    apply(simp only: Halt.simps)
+    oops
+
+
+end
+