theory common
imports Nat Hilbert_Choice
begin
section {* induct_def *}
lemma induct_def_n:
fixes N :: nat
shows "\ F. F 0 = base \ (\ n < N. F(n + 1) = f n (F n))"
proof (induct N)
case 0
show "\ F. F 0 = base \ (\ n < 0. F(n + 1) = f n (F n))" by auto
next
case Suc
fix N :: nat
assume "\ F. F 0 = base \ (\ n < N. F(n + 1) = f n (F n))"
then obtain F where "F 0 = base" and IH: "\ n < N. F(n + 1) = f n (F n)" by auto
def new_F \ "\ n. if n = N + 1 then f N (F N) else F n"
have "new_F 0 = base" using `F 0 = base` and new_F_def by auto
moreover {
fix n
assume "n < Suc N"
{
assume "n = N"
hence "new_F(n + 1) = f n (new_F n)" using new_F_def by auto
}
moreover {
assume "n \ N"
hence "n < N" using `n < Suc N` and new_F_def by auto
hence "new_F(n + 1) = f n (new_F n)" using IH and new_F_def by auto
}
ultimately have "new_F(n + 1) = f n (new_F n)" by auto
}
hence "\ n < Suc N. new_F(n + 1) = f n (new_F n)" by auto
ultimately have "new_F 0 = base \ (\ n < Suc N. new_F(n + 1) = f n (new_F n))" by auto
thus "\ F. F 0 = base \ (\ n < Suc N. F(n + 1) = f n (F n))" by auto
qed
lemma induct_def_inf:
"\ F. F 0 = base \ (\ n :: nat. F(n + 1) = f n (F n))"
proof -
{
fix N :: nat
have "\ F. F 0 = base \ (\ n < N. F(n + 1) = f n (F n))" by (rule induct_def_n)
}
hence SuDDydQn: "\ N. \ F. F 0 = base \ (\ n < N. F(n + 1) = f n (F n))" by auto
def property \ "\ N F. F 0 = base \ (\ n < N. F(n + 1) = f n (F n))"
{
fix N and M and F and G
assume "property N F" and "property M G"
fix n
assume "n \ N" and "n \ M"
hence "F n = G n" proof (induct n)
case 0
thus ?case using `property N F` and `property M G` and property_def by auto
next
case Suc
thus ?case using `property N F` and `property M G` and property_def by auto
qed
}
hence uniq: "\ N M F G. property N F \ property M G \ (\ n. n \ N \ n \ M \ F n = G n)" by auto
have "\ N. \ F. property N F" using SuDDydQn and property_def by auto
hence "\ nth_fun. \ N. property N (nth_fun N)" using choice by auto
then obtain nth_fun where "\ N. property N (nth_fun N)" by auto
def F \ "\ n. nth_fun n n"
have "F 0 = base" using F_def and `\ N. property N (nth_fun N)` and property_def by auto
moreover {
fix n
have "F(n + 1) = nth_fun (n + 1) (n + 1)" using F_def by auto
also have "property (n + 1) (nth_fun (n + 1))" using `\ N. property N (nth_fun N)` by auto
hence e7tBKBNi: "\ m < n + 1. nth_fun (n + 1) (m + 1) = f m (nth_fun (n + 1) m)"
using property_def by auto
hence "nth_fun (n + 1) (n + 1) = f n (nth_fun (n + 1) n)" by auto
also {
have "property (n + 1) (nth_fun (n + 1))" and "property n (nth_fun n)" using `\ N. property N (nth_fun N)` by auto
hence "nth_fun (n + 1) n = nth_fun n n" using uniq by auto
also have "... = F n" using F_def by auto
finally have "nth_fun (n + 1) n = F n" by auto
}
hence "f n (nth_fun (n + 1) n) = f n (F n)" by auto
finally have "F(n + 1) = f n (F n)" by auto
}
hence "\ n. F(n + 1) = f n (F n)" by auto
ultimately have "F 0 = base \ (\ n. F(n + 1) = f n (F n))" by auto
thus "\ F. F 0 = base \ (\ n. F(n + 1) = f n (F n))" by auto
qed
end