theory Recs
imports Main 
        "~~/src/HOL/Number_Theory/Primes" 
         Fact
begin

(*
  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})"

definition (in ord)
  Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
  "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"

lemma Great_equality:
  fixes x::nat
  assumes "P x" "\<And>y. P y \<Longrightarrow> y \<le> x"
  shows "Great P = x"
unfolding Great_def 
using assms by(rule_tac the_equality) (auto intro: le_antisym)

lemma BMax_rec_eq1:
 "BMax_rec R x = (GREAT z. (R z \<and> z \<le> x) \<or> z = 0)"
apply(induct x)
apply(auto intro: Great_equality Great_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

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 *}

fun log :: "nat \<Rightarrow> nat" where
  [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"

lemma log_zero [simp]:
  "log 0 = 0"
  by (simp add: log.simps)

lemma log_one [simp]:
  "log 1 = 0"
  by (simp add: log.simps)

lemma log_suc [simp]:
  "log (Suc 0) = 0"
  by (simp add: log.simps)

lemma log_rec:
  "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
  by (simp add: log.simps)

lemma log_twice [simp]:
  "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
  by (simp add: log_rec)

lemma log_half [simp]:
  "log (n div 2) = log n - 1"
proof (cases "n < 2")
  case True
  then have "n = 0 \<or> n = 1" by arith
  then show ?thesis by (auto simp del: One_nat_def)
next
  case False then show ?thesis by (simp add: log_rec)
qed

lemma log_exp [simp]:
  "log (2 ^ n) = n"
  by (induct n) simp_all

fun oddfactor :: "nat \<Rightarrow> nat" where
  [simp del]: "oddfactor n = (if n = 0 then 0 else if even n then oddfactor (n div 2) else n)"

lemma oddfactor[simp]:
  "oddfactor 0 = 0"
  "odd n \<Longrightarrow> oddfactor n = n"
  "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
apply(simp_all add: oddfactor.simps)
done

lemma oddfactor_odd:
  "oddfactor n = 0 \<or> odd (oddfactor n)" 
apply(induct n rule: nat_less_induct)
apply(case_tac "n = 0")
apply(simp)
apply(case_tac "odd n")
apply(auto)
done

lemma bigger: "oddfactor (Suc n) > 0"
apply(induct n rule: nat_less_induct)
apply(case_tac "n = 0")
apply(simp)
apply(case_tac "odd n")
apply(auto)
apply(drule_tac x="n div 2" in spec)
apply(drule mp)
apply(auto)
by (smt numeral_2_eq_2 odd_nat_plus_one_div_two)

fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1"

fun pdecode2 :: "nat \<Rightarrow> nat" where
  "pdecode2 z = (oddfactor (Suc z) - 1) div 2"

fun pdecode1 :: "nat \<Rightarrow> nat" where
  "pdecode1 z = log ((Suc z) div (oddfactor (Suc z)))"

lemma k:
  "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n"
apply(induct m)
apply(simp_all)
done

lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n"
apply(induct n rule: nat_less_induct)
apply(case_tac "n=0")
apply(simp)
apply(case_tac "odd n")
apply(simp)
apply(rule_tac x="0" in exI)
apply(simp)
apply(simp)
apply(drule_tac x="n div 2" in spec)
apply(erule impE)
apply(simp)
apply(erule exE)
apply(rule_tac x="Suc k" in exI)
apply(simp)
by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral)



lemma t:
  "(Suc (Suc m)) div 2 = Suc (m div 2)"
by (induct m) (auto)

lemma u:
  "((Suc (Suc m)) mod 2 = 0) <-> m mod 2 = 0"
by (auto)

lemma u2: 
  "0 < n ==> 2 * 2 ^ (n - 1) = (2::nat) ^ (n::nat)"
by (induct n) (simp_all)

lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y"
by simp

lemma m: "0 < n ==> 2 ^ log (n div (oddfactor n)) = n div (oddfactor n)"
apply(induct n rule: nat_less_induct)
apply(case_tac "n=0")
apply(simp)
apply(case_tac "odd n")
apply(simp)
apply(drule_tac x="n div 2" in spec)
apply(drule mp)
apply(auto)[1]
apply(drule mp)
apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat)
apply(subst (asm) oddfactor(3)[symmetric])
apply(simp)
apply(subst (asm) oddfactor(3)[symmetric])
apply(simp)
apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2")
prefer 2
apply (metis div_mult2_eq nat_mult_commute)
apply(simp only: log_half)
apply(case_tac "n div oddfactor n = 0")
apply(simp)
apply(simp del: oddfactor)
apply(drule test)
apply(subst (asm) power.simps(2)[symmetric])
apply(subgoal_tac "Suc (log (n div oddfactor n) - 1) = log (n div oddfactor n)")
prefer 2
apply (smt Recs.log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76))
apply(simp only:)
apply(subst dvd_mult_div_cancel)
apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww)
apply(simp (no_asm))
done

lemma m1: "n div oddfactor n * oddfactor n = n"
apply(induct n rule: nat_less_induct)
apply(case_tac "n=0")
apply(simp)
apply(case_tac "odd n")
apply(simp)
apply(simp)
apply(drule_tac x="n div 2" in spec)
apply(drule mp)
apply(auto)[1]
by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)


lemma m2: "0 < n ==> 2 ^ log (n div (oddfactor n)) * (oddfactor n) = n"
apply(subst m)
apply(simp)
apply(subst m1)
apply(simp)
done

lemma y1:
  "pdecode2 (pencode m n) = n"
apply(simp)
apply(subst k)
apply(auto)
done

lemma y2:
  "pdecode1 (pencode m n) = m"
using [[simp_trace]]
apply(simp)
apply(subst k)
apply(auto)[1]
using [[simp_trace_depth_limit=10]]
apply(simp)
done

lemma yy: 
  "pencode (pdecode1 m) (pdecode2 m) = m"
apply(induct m rule: nat_less_induct)
apply(simp (no_asm))
apply(case_tac "n = 0")
apply(simp)
apply(subst dvd_mult_div_cancel)
using oddfactor_odd
apply -
apply(drule_tac x="Suc n" in meta_spec)
apply(erule disjE)
apply(auto)[1]
apply (metis even_num_iff nat_even_iff_2_dvd odd_pos)
using bigger
apply -
apply(rotate_tac 3)
apply(drule_tac x="n" in meta_spec)
apply(simp del: pencode.simps pdecode2.simps pdecode1.simps)
apply(subst m2)
apply(simp)
apply(simp)
done

fun penc where
 "penc (m, n) = pencode m n"

fun pdec where
 "pdec m = (pdecode1 m, pdecode2 m)"

lemma q1: "penc (pdec m) = m"
apply(simp only: penc.simps pdec.simps)
apply(rule yy)
done

lemma q2: "pdec (penc m) = m"
apply(simp only: penc.simps pdec.simps)
apply(case_tac m)
apply(simp only: penc.simps pdec.simps)
apply(subst y1)
apply(subst y2)
apply(simp)
done

lemma inj_penc: "inj_on penc A"
apply(rule inj_on_inverseI)
apply(rule q2)
done

lemma inj_pdec: "inj_on pdec A"
apply(rule inj_on_inverseI)
apply(rule q1)
done

lemma surj_penc: "surj penc"
apply(rule surjI)
apply(rule q1)
done

lemma surj_pdec: "surj pdec"
apply(rule surjI)
apply(rule q2)
done

lemma 
  "bij pdec"
by(simp add: bij_def surj_pdec inj_pdec)

lemma 
  "bij penc"
by(simp add: bij_def surj_penc inj_penc)

lemma "a \<le> penc (a, 0)"
apply(induct a)
apply(simp)
apply(simp)
by (smt nat_one_le_power)

lemma "penc(a, 0) \<le> penc (a, b)"
apply(simp)
by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute)

lemma "b \<le> penc (a, b)"
apply(simp)
proof -
  have f1: "(1\<Colon>nat) + 1 = 2"
    by (metis mult_2 nat_mult_1_right)
  have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2"
    by (metis mult_le_mono2 nat_mult_1_right)
  have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"
    by (metis le_add1 le_trans nat_add_left_cancel_le)
  hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"
    using f2 by (metis le_add1 le_trans one_le_power)
  hence "b \<le> 2 ^ a * (b + b + 1) - 1"
    using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute)
  thus "b \<le> 2 ^ a * (2 * b + 1) - 1"
    by (metis mult_2)
qed

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)



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

(*

lemma rec_minr2_le_Suc:
  "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"
apply(simp add: rec_minr2_def)
apply(auto intro!: setsum_one_le setprod_one_le)
done

lemma rec_minr2_eq_Suc:
  assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
  shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
using assms by (simp add: rec_minr2_def)

lemma rec_minr2_le:
  assumes h1: "y \<le> x" 
  and     h2: "0 < rec_eval f [y, y1, y2]" 
  shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y"
apply(simp add: rec_minr2_def)
apply(subst setsum_cut_off_le[OF h1])
using h2 apply(auto)
apply(auto intro!: setsum_one_less setprod_one_le)
done

(* ??? *)
lemma setsum_eq_one_le2:
  fixes n::nat
  assumes "\<forall>i \<le> n. f i \<le> 1" 
  shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)"  
using assms
apply(induct n)
apply(simp add: One_nat_def)
apply(simp)
apply(auto simp add: One_nat_def)
apply(drule_tac x="Suc n" in spec)
apply(auto)
by (metis le_Suc_eq)


lemma rec_min2_not:
  assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
  shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
using assms
apply(simp add: rec_minr2_def)
apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)")
apply(simp)
apply (metis atMost_iff le_refl zero_neq_one)
apply(rule setsum_eq_one_le2)
apply(auto)
apply(rule setprod_one_le)
apply(auto)
done

lemma disjCI2:
  assumes "~P ==> Q" shows "P|Q"
apply (rule classical)
apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
done

lemma minr_lemma [simp]:
shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
apply(induct x)
apply(rule Least_equality[symmetric])
apply(simp add: rec_minr2_def)
apply(erule disjE)
apply(rule rec_minr2_le)
apply(auto)[2]
apply(simp)
apply(rule rec_minr2_le_Suc)
apply(simp)

apply(rule rec_minr2_le)


apply(rule rec_minr2_le_Suc)
apply(rule disjCI)
apply(simp add: rec_minr2_def)

apply(ru le setsum_one_less)
apply(clarify)
apply(rule setprod_one_le)
apply(auto)[1]
apply(simp)
apply(rule setsum_one_le)
apply(clarify)
apply(rule setprod_one_le)
apply(auto)[1]
thm disj_CE
apply(auto)

lemma minr_lemma:
shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
apply(simp only: Minr_def)
apply(rule sym)
apply(rule Min_eqI)
apply(auto)[1]
apply(simp)
apply(erule disjE)
apply(simp)
apply(rule rec_minr2_le_Suc)
apply(rule rec_minr2_le)
apply(auto)[2]
apply(simp)
apply(induct x)
apply(simp add: rec_minr2_def)
apply(
apply(rule disjCI)
apply(rule rec_minr2_eq_Suc)
apply(simp)
apply(auto)

apply(rule setsum_one_le)
apply(auto)[1]
apply(rule setprod_one_le)
apply(auto)[1]
apply(subst setsum_cut_off_le)
apply(auto)[2]
apply(rule setsum_one_less)
apply(auto)[1]
apply(rule setprod_one_le)
apply(auto)[1]
apply(simp)
thm setsum_eq_one_le
apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>
                   (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")
prefer 2
apply(auto)[1]
apply(erule disjE)
apply(rule disjI1)
apply(rule setsum_eq_one_le)
apply(simp)
apply(rule disjI2)
apply(simp)
apply(clarify)
apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")
defer
apply metis
apply(erule exE)
apply(subgoal_tac "l \<le> x")
defer
apply (metis not_leE not_less_Least order_trans)
apply(subst setsum_least_eq)
apply(rotate_tac 4)
apply(assumption)
apply(auto)[1]
apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
prefer 2
apply(auto)[1]
apply(rotate_tac 5)
apply(drule not_less_Least)
apply(auto)[1]
apply(auto)
apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)
apply(simp)
apply (metis LeastI_ex)
apply(subst setsum_least_eq)
apply(rotate_tac 3)
apply(assumption)
apply(simp)
apply(auto)[1]
apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
prefer 2
apply(auto)[1]
apply (metis neq0_conv not_less_Least)
apply(auto)[1]
apply (metis (mono_tags) LeastI_ex)
by (metis LeastI_ex)

lemma minr_lemma:
shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
apply(simp only: Minr_def rec_minr2_def)
apply(simp)
apply(rule sym)
apply(rule Min_eqI)
apply(auto)[1]
apply(simp)
apply(erule disjE)
apply(simp)
apply(rule setsum_one_le)
apply(auto)[1]
apply(rule setprod_one_le)
apply(auto)[1]
apply(subst setsum_cut_off_le)
apply(auto)[2]
apply(rule setsum_one_less)
apply(auto)[1]
apply(rule setprod_one_le)
apply(auto)[1]
apply(simp)
thm setsum_eq_one_le
apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>
                   (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")
prefer 2
apply(auto)[1]
apply(erule disjE)
apply(rule disjI1)
apply(rule setsum_eq_one_le)
apply(simp)
apply(rule disjI2)
apply(simp)
apply(clarify)
apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")
defer
apply metis
apply(erule exE)
apply(subgoal_tac "l \<le> x")
defer
apply (metis not_leE not_less_Least order_trans)
apply(subst setsum_least_eq)
apply(rotate_tac 4)
apply(assumption)
apply(auto)[1]
apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
prefer 2
apply(auto)[1]
apply(rotate_tac 5)
apply(drule not_less_Least)
apply(auto)[1]
apply(auto)
apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)
apply(simp)
apply (metis LeastI_ex)
apply(subst setsum_least_eq)
apply(rotate_tac 3)
apply(assumption)
apply(simp)
apply(auto)[1]
apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
prefer 2
apply(auto)[1]
apply (metis neq0_conv not_less_Least)
apply(auto)[1]
apply (metis (mono_tags) LeastI_ex)
by (metis LeastI_ex)

lemma disjCI2:
  assumes "~P ==> Q" shows "P|Q"
apply (rule classical)
apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
done


lemma minr_lemma [simp]:
shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
(*apply(simp add: rec_minr2_def)*)
apply(rule Least_equality[symmetric])
prefer 2
apply(erule disjE)
apply(rule rec_minr2_le)
apply(auto)[2]
apply(clarify)
apply(rule rec_minr2_le_Suc)
apply(rule disjCI)
apply(simp add: rec_minr2_def)

apply(ru le setsum_one_less)
apply(clarify)
apply(rule setprod_one_le)
apply(auto)[1]
apply(simp)
apply(rule setsum_one_le)
apply(clarify)
apply(rule setprod_one_le)
apply(auto)[1]
thm disj_CE
apply(auto)
apply(auto)
prefer 2
apply(rule le_tran

apply(rule le_trans)
apply(simp)
defer
apply(auto)
apply(subst setsum_cut_off_le)


lemma 
  "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))" 
apply(simp add: Minr_def)
apply(rule Min_eqI)
apply(auto)[1]
apply(simp)
apply(rule Least_le)
apply(auto)[1]
apply(rule LeastI2_wellorder)
apply(auto)
done

definition (in ord)
  Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
  "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"

(*
lemma Great_equality:
  assumes "P x"
    and "\<And>y. P y \<Longrightarrow> y \<le> x"
  shows "Great P = x"
unfolding Great_def 
apply(rule the_equality)
apply(blast intro: assms)
*)



lemma 
  "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))" 
apply(simp add: Maxr_def)
apply(rule Max_eqI)
apply(auto)[1]
apply(simp)
thm Least_le Greatest_le
oops

lemma
  "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys"
apply(simp add: Maxr_def Minr_def)
apply(rule Max_eqI)
apply(auto)[1]
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto)[1]
defer
apply(simp)
apply(auto)[1]
thm Min_insert
defer
oops



definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  where
  "quo x y = (if y = 0 then 0 else x div y)"


definition 
  "rec_quo = CN rec_mult [CN rec_sign [Id 2 1],  
      CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]])) 
                [Id 2 0, Id 2 0, Id 2 1]]"

lemma div_lemma [simp]:
  "rec_eval rec_quo [x, y] = quo x y"
apply(simp add: rec_quo_def quo_def)
apply(rule impI)
apply(rule Min_eqI)
apply(auto)[1]
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto)[1]
apply (metis div_le_dividend le_SucI)
defer
apply(simp)
apply(auto)[1]
apply (metis mult_Suc_right nat_mult_commute split_div_lemma)
apply(auto)[1]

apply (smt div_le_dividend fst_divmod_nat)
apply(simp add: quo_def)
apply(auto)[1]

apply(auto)

fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 
                        if (setx = {}) then (Suc x) else (Min setx))"

definition
  "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))"

lemma minr_lemma [simp]:
shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y"
apply(simp only: rec_minr_def)
apply(simp only: sigma1_lemma)
apply(simp only: accum1_lemma)
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
apply(simp only: Minr.simps Let_def)
apply(auto simp del: not_lemma)
apply(simp)
apply(simp only: not_lemma sign_lemma)
apply(rule sym)
apply(rule Min_eqI)
apply(auto)[1]
apply(simp)
apply(subst setsum_cut_off_le[where m="ya"])
apply(simp)
apply(simp)
apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
apply(rule setsum_one_less)
apply(default)
apply(rule impI)
apply(rule setprod_one_le)
apply(auto split: if_splits)[1]
apply(simp)
apply(rule conjI)
apply(subst setsum_cut_off_le[where m="xa"])
apply(simp)
apply(simp)
apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
apply(rule le_trans)
apply(rule setsum_one_less)
apply(default)
apply(rule impI)
apply(rule setprod_one_le)
apply(auto split: if_splits)[1]
apply(simp)
apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])")
defer
apply metis
apply(erule exE)
apply(subgoal_tac "l \<le> x")
defer
apply (metis not_leE not_less_Least order_trans)
apply(subst setsum_least_eq)
apply(rotate_tac 3)
apply(assumption)
prefer 3
apply (metis LeastI_ex)
apply(auto)[1]
apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])")
prefer 2
apply(auto)[1]
apply(rotate_tac 5)
apply(drule not_less_Least)
apply(auto)[1]
apply(auto)
by (metis (mono_tags) LeastI_ex)


fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
  where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 
                        Min (setx \<union> {Suc x}))"

lemma Minr2_Minr: 
  "Minr2 R x y = Minr R x y"
apply(auto)
apply (metis (lifting, no_types) Min_singleton empty_Collect_eq)
apply(rule min_absorb2)
apply(subst Min_le_iff)
apply(auto)  
done
 *)