theory Recs
imports Main Fact "~~/src/HOL/Number_Theory/Primes"
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_swap = PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2])"
definition
"rec_power = rec_swap rec_power_swap"
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_swap = (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
definition
"rec_minus = rec_swap rec_minus_swap"
text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
definition
"rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
definition
"rec_not = CN rec_minus [constn 1, Id 1 0]"
text {*
@{text "rec_eq"} compares two arguments: returns @{text "1"}
if they are equal; @{text "0"} otherwise. *}
definition
"rec_eq = CN rec_minus
[CN (constn 1) [Id 2 0],
CN rec_add [rec_minus, rec_swap rec_minus]]"
definition
"rec_noteq = CN rec_not [rec_eq]"
definition
"rec_conj = CN rec_sign [rec_mult]"
definition
"rec_disj = CN rec_sign [rec_add]"
definition
"rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
y otherwise *}
definition
"rec_ifz = PR (Id 2 0) (Id 4 3)"
text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero,
y otherwise *}
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, Reminder *}
definition
"rec_dvd_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_dvd = rec_swap rec_dvd_swap"
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_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
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_swap_lemma [simp]:
"rec_eval rec_power_swap [y, x] = x ^ y"
by (induct y) (simp_all add: rec_power_swap_def)
lemma power_lemma [simp]:
"rec_eval rec_power [x, y] = x ^ y"
by (simp 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_swap_lemma [simp]:
"rec_eval rec_minus_swap [x, y] = y - x"
by (induct x) (simp_all add: rec_minus_swap_def)
lemma minus_lemma [simp]:
"rec_eval rec_minus [x, y] = x - y"
by (simp 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_swap_lemma [simp]:
"rec_eval rec_dvd_swap [x, y] = (if y dvd x then 1 else 0)"
unfolding dvd_alt_def
by (auto simp add: rec_dvd_swap_def)
lemma dvd_lemma [simp]:
"rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
by (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_rem [y, x] = y mod x"
by (simp add: rec_rem_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
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])"
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 Min and 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. 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. 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 {* 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_rem [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 {* Universal Function *}
text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *}
fun 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)
fun Pi :: "nat \<Rightarrow> nat"
where
"Pi 0 = 2" |
"Pi (Suc x) = NextPrime (Pi x)"
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)
fun Left where
"Left c = Lo c (Pi 0)"
definition
"rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"
lemma left_lemma [simp]:
"rec_eval rec_left [c] = Left c"
by(simp add: rec_left_def)
fun Right where
"Right c = Lo c (Pi 2)"
definition
"rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"
lemma right_lemma [simp]:
"rec_eval rec_right [c] = Right c"
by(simp add: rec_right_def)
fun Stat where
"Stat c = Lo c (Pi 1)"
definition
"rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"
lemma stat_lemma [simp]:
"rec_eval rec_stat [c] = Stat c"
by(simp add: rec_stat_def)
text{* coding of the configuration *}
text {*
@{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural
numbers encoded by number @{text "sr"} using Godel's coding.
*}
fun Entry where
"Entry sr i = Lo sr (Pi (Suc i))"
definition
"rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
lemma entry_lemma [simp]:
"rec_eval rec_entry [sr, i] = Entry sr i"
by(simp add: rec_entry_def)
fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
where
"Listsum2 xs 0 = 0"
| "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"
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]"
lemma listsum2_lemma [simp]:
"length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
by (induct n) (simp_all)
text {*
@{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the
B book, but this definition generalises the original one to deal with multiple
input arguments.
*}
fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
where
"Strt' xs 0 = 0"
| "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n
in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))"
fun Strt :: "nat list \<Rightarrow> nat"
where
"Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"
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)"
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])
text {* The @{text "Scan"} function on page 90 of B book. *}
fun Scan :: "nat \<Rightarrow> nat"
where
"Scan r = r mod 2"
definition
"rec_scan = CN rec_rem [Id 1 0, constn 2]"
lemma scan_lemma [simp]:
"rec_eval rec_scan [r] = r mod 2"
by(simp add: rec_scan_def)
text {* The specifation of the mutli-way branching statement on
page 79 of Boolos's book. *}
type_synonym ftype = "nat list \<Rightarrow> nat"
type_synonym rtype = "nat list \<Rightarrow> bool"
fun Embranch :: "(ftype * rtype) list \<Rightarrow> nat list \<Rightarrow> nat"
where
"Embranch [] xs = 0" |
"Embranch ((g, c) # gcs) xs = (if c xs then g xs else Embranch gcs xs)"
fun rec_embranch' :: "(recf * recf) list \<Rightarrow> nat \<Rightarrow> recf"
where
"rec_embranch' [] xs = Z" |
"rec_embranch' ((g, c) # gcs) xs =
CN rec_add [CN rec_mult [g, c], rec_embranch' gcs xs]"
fun rec_embranch :: "(recf * recf) list \<Rightarrow> recf"
where
"rec_embranch [] = Z"
| "rec_embranch ((rg, rc) # rgcs) = (let vl = arity rg in
rec_embranch' ((rg, rc) # rgcs) vl)"
(*
lemma embranch_lemma [simp]:
shows "rec_eval (rec_embranch (zip rgs rcs)) xs =
Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs"
apply(induct rcs arbitrary: rgs)
apply(simp)
apply(simp)
apply(case_tac rgs)
apply(simp)
apply(simp)
apply(case_tac rcs)
apply(simp_all)
apply(rule conjI)
*)
fun Newleft0 :: "nat list \<Rightarrow> nat"
where
"Newleft0 [p, r] = p"
definition rec_newleft0 :: "recf"
where
"rec_newleft0 = Id 2 0"
fun Newrgt0 :: "nat list \<Rightarrow> nat"
where
"Newrgt0 [p, r] = r - Scan r"
definition rec_newrgt0 :: "recf"
where
"rec_newrgt0 = CN rec_minus [Id 2 1, CN rec_scan [Id 2 1]]"
(*newleft1, newrgt1: left rgt number after execute on step*)
fun Newleft1 :: "nat list \<Rightarrow> nat"
where
"Newleft1 [p, r] = p"
definition rec_newleft1 :: "recf"
where
"rec_newleft1 = Id 2 0"
fun Newrgt1 :: "nat list \<Rightarrow> nat"
where
"Newrgt1 [p, r] = r + 1 - Scan r"
definition
"rec_newrgt1 = CN rec_minus [CN rec_add [Id 2 1, constn 1], CN rec_scan [Id 2 1]]"
fun Newleft2 :: "nat list \<Rightarrow> nat"
where
"Newleft2 [p, r] = p div 2"
definition
"rec_newleft2 = CN rec_quo [Id 2 0, constn 2]"
fun Newrgt2 :: "nat list \<Rightarrow> nat"
where
"Newrgt2 [p, r] = 2 * r + p mod 2"
definition
"rec_newrgt2 = CN rec_add [CN rec_mult [constn 2, Id 2 1],
CN rec_rem [Id 2 0, constn 2]]"
fun Newleft3 :: "nat list \<Rightarrow> nat"
where
"Newleft3 [p, r] = 2 * p + r mod 2"
definition rec_newleft3 :: "recf"
where
"rec_newleft3 = CN rec_add [CN rec_mult [constn 2, Id 2 0],
CN rec_rem [Id 2 1, constn 2]]"
fun Newrgt3 :: "nat list \<Rightarrow> nat"
where
"Newrgt3 [p, r] = r div 2"
definition
"rec_newrgt3 = CN rec_quo [Id 2 1, constn 2]"
text {* The @{text "new_left"} function on page 91 of B book. *}
fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"Newleft p r a = (if a = 0 \<or> a = 1 then Newleft0 [p, r]
else if a = 2 then Newleft2 [p, r]
else if a = 3 then Newleft3 [p, r]
else p)"
definition
"rec_newleft =
(let g0 = CN rec_newleft0 [Id 3 0, Id 3 1] in
let g1 = CN rec_newleft2 [Id 3 0, Id 3 1] in
let g2 = CN rec_newleft3 [Id 3 0, Id 3 1] in
let g3 = Id 3 0 in
let r0 = CN rec_disj [CN rec_eq [Id 3 2, constn 0],
CN rec_eq [Id 3 2, constn 1]] in
let r1 = CN rec_eq [Id 3 2, constn 2] in
let r2 = CN rec_eq [Id 3 2, constn 3] in
let r3 = CN rec_less [constn 3, Id 3 2] in
let gs = [g0, g1, g2, g3] in
let rs = [r0, r1, r2, r3] in
rec_embranch (zip gs rs))"
fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
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 \<or> Left c \<noteq> 0 \<or>
Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or>
Right c = 0)"
text {*
@{text "Conf m r k"} computes the TM configuration after
@{text "k"} steps of execution of the TM coded as @{text "m"}
starting from the initial configuration where the left number
equals @{text "0"} and the right number equals @{text "r"}.
*}
fun Conf
where
"Conf m r 0 = Trpl 0 (Suc 0) r"
| "Conf m r (Suc t) = Newconf m (Conf m r t)"
text{*
@{text "Nonstop m r t"} means that afer @{text "t"} steps of
execution, the TM coded by @{text "m"} is not at a stardard
final configuration.
*}
fun Nostop
where
"Nostop m r t = Nstd (Conf m r t)"
fun Value where
"Value x = (Lg (Suc x) 2) - 1"
definition
"rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
lemma value_lemma [simp]:
"rec_eval rec_value [x] = Value x"
by (simp add: rec_value_def)
definition
"rec_UF = CN rec_value [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]"
end
(*
fun mtest where
"mtest R 0 = if R 0 then 0 else 1"
| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
lemma
"rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
apply(simp only: rec_maxr2_def)
apply(case_tac x)
apply(clarify)
apply(subst rec_eval.simps)
apply(simp only: constn_lemma)
defer
apply(clarify)
apply(subst rec_eval.simps)
apply(simp only: rec_maxr2_def[symmetric])
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
apply(subst rec_eval.simps)
apply(simp only: map.simps nth)
definition
"rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
definition
"rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
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
*)