Theory Recs_alt_Def
chapter ‹An alternative modelling of Recursive Functions›
theory Recs_alt_Def
imports Main
"HOL-Library.Nat_Bijection"
"HOL-Library.Discrete"
begin
text‹
A more streamlined and cleaned-up version of Recursive
Functions following
A Course in Formal Languages, Automata and Groups
I. M. Chiswell
and
Lecture on Undecidability
Michael M. Wolf
›
declare One_nat_def[simp del]
lemma if_zero_one [simp]:
"(if P then 1 else 0) = (0::nat) ⟷ ¬ P"
"(0::nat) < (if P then 1 else 0) = P"
"(if P then 0 else 1) = (if ¬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 the Recursive Functions Sigma and Pi›
lemma setprod_atMost_Suc[simp]:
"(∏i ≤ Suc n. f i) = (∏i ≤ n. f i) * f(Suc n)"
by(simp add:atMost_Suc mult_ac)
lemma setprod_lessThan_Suc[simp]:
"(∏i < Suc n. f i) = (∏i < n. f i) * f n"
by (simp add:lessThan_Suc mult_ac)
lemma setsum_add_nat_ivl2: "n ≤ p ⟹
sum f {..<n} + sum f {n..p} = sum f {..p::nat}"
apply(subst sum.union_disjoint[symmetric])
apply(auto simp add: ivl_disj_un_one)
done
lemma setsum_eq_zero [simp]:
fixes f::"nat ⇒ nat"
shows "(∑i < n. f i) = 0 ⟷ (∀i < n. f i = 0)"
"(∑i ≤ n. f i) = 0 ⟷ (∀i ≤ n. f i = 0)"
by (auto)
lemma setprod_eq_zero [simp]:
fixes f::"nat ⇒ nat"
shows "(∏i < n. f i) = 0 ⟷ (∃i < n. f i = 0)"
"(∏i ≤ n. f i) = 0 ⟷ (∃i ≤ n. f i = 0)"
by (auto)
lemma setsum_one_less:
fixes n::nat
assumes "∀i < n. f i ≤ 1"
shows "(∑i < n. f i) ≤ n"
using assms
by (induct n) (auto)
lemma setsum_one_le:
fixes n::nat
assumes "∀i ≤ n. f i ≤ 1"
shows "(∑i ≤ n. f i) ≤ Suc n"
using assms
by (induct n) (auto)
lemma setsum_eq_one_le:
fixes n::nat
assumes "∀i ≤ n. f i = 1"
shows "(∑i ≤ n. f i) = Suc n"
using assms
by (induct n) (auto)
lemma setsum_least_eq:
fixes f::"nat ⇒ nat"
assumes h0: "p ≤ n"
assumes h1: "∀i ∈ {..<p}. f i = 1"
assumes h2: "∀i ∈ {p..n}. f i = 0"
shows "(∑i ≤ n. f i) = p"
proof -
have eq_p: "(∑i ∈ {..<p}. f i) = p"
using h1 by (induct p) (simp_all)
have eq_zero: "(∑i ∈ {p..n}. f i) = 0"
using h2 by auto
have "(∑i ≤ n. f i) = (∑i ∈ {..<p}. f i) + (∑i ∈ {p..n}. f i)"
using h0 by (simp add: setsum_add_nat_ivl2)
also have "... = (∑i ∈ {..<p}. f i)" using eq_zero by simp
finally show "(∑i ≤ n. f i) = p" using eq_p by simp
qed
lemma nat_mult_le_one:
fixes m n::nat
assumes "m ≤ 1" "n ≤ 1"
shows "m * n ≤ 1"
using assms by (induct n) (auto)
lemma setprod_one_le:
fixes f::"nat ⇒ nat"
assumes "∀i ≤ n. f i ≤ 1"
shows "(∏i ≤ n. f i) ≤ 1"
using assms
by (induct n) (auto intro: nat_mult_le_one)
lemma setprod_greater_zero:
fixes f::"nat ⇒ nat"
assumes "∀i ≤ n. f i ≥ 0"
shows "(∏i ≤ n. f i) ≥ 0"
using assms by (induct n) (auto)
lemma setprod_eq_one:
fixes f::"nat ⇒ nat"
assumes "∀i ≤ n. f i = Suc 0"
shows "(∏i ≤ n. f i) = Suc 0"
using assms by (induct n) (auto)
lemma setsum_cut_off_less:
fixes f::"nat ⇒ nat"
assumes h1: "m ≤ n"
and h2: "∀i ∈ {m..<n}. f i = 0"
shows "(∑i < n. f i) = (∑i < m. f i)"
proof -
have eq_zero: "(∑i ∈ {m..<n}. f i) = 0"
using h2 by auto
have "(∑i < n. f i) = (∑i ∈ {..<m}. f i) + (∑i ∈ {m..<n}. f i)"
using h1 by (metis atLeast0LessThan le0 sum.atLeastLessThan_concat)
also have "... = (∑i ∈ {..<m}. f i)" using eq_zero by simp
finally show "(∑i < n. f i) = (∑i < m. f i)" by simp
qed
lemma setsum_cut_off_le:
fixes f::"nat ⇒ nat"
assumes h1: "m ≤ n"
and h2: "∀i ∈ {m..n}. f i = 0"
shows "(∑i ≤ n. f i) = (∑i < m. f i)"
proof -
have eq_zero: "(∑i ∈ {m..n}. f i) = 0"
using h2 by auto
have "(∑i ≤ n. f i) = (∑i ∈ {..<m}. f i) + (∑i ∈ {m..n}. f i)"
using h1 by (simp add: setsum_add_nat_ivl2)
also have "... = (∑i ∈ {..<m}. f i)" using eq_zero by simp
finally show "(∑i ≤ n. f i) = (∑i < m. f i)" by simp
qed
lemma setprod_one [simp]:
fixes n::nat
shows "(∏i < n. Suc 0) = Suc 0"
"(∏i ≤ n. Suc 0) = Suc 0"
by (induct n) (simp_all)
section ‹Recursive Functions›