Recursion.thy (:brush=isabelle:) theory Recursion imports Main begin
text ‹Define the factorial› fun f :: ‹nat => nat› where
‹f 0 = 1› | ‹f (Suc n) = (Suc n) * f n›
text ‹Some checks› value ‹f 0› value ‹f 1› value ‹f 5›
text ‹Define the functor whose fixed point is the factorial› definition Fact :: ‹(nat => nat) => (nat => nat)› where
‹Fact u ≡ (λn. (case n of
0 ⇒ 1
| Suc m ⇒ n * (u m)
)
)›
text ‹
Check what happens with successive applications of the functor to the null function. ^^ is the composition power: f^^n = f ∘ f ∘ ... ∘ f n times
› text ‹A function that always returns the special Isabelle/HOL constant 'undefined'› abbreviation ‹undef ≡ (λn. undefined)›
value ‹Fact undef› value ‹(Fact undef) 0› value ‹(Fact (Fact undef)) 1› value ‹((Fact^^2) undef) 1› value ‹((Fact^^3) undef) 2› value ‹((Fact^^3) undef) 3› value ‹((Fact^^4) undef) 3› value ‹((Fact^^5) undef) 4› value ‹((Fact^^6) undef) 5›
text ‹Show that f is a fixed point of Fact› thm ext lemma ‹Fact f = f› proof -
have ‹⋀n. Fact f n = f n› unfolding Fact_def by (simp split: nat.split) thus ?thesis by (rule ext)
qed
text ‹Another proof› lemma ‹Fact f = f› proof (rule ext)
{ fix n
have ‹Fact f n = f n›
proof (cases n)
case 0
then show ?thesis unfolding Fact_def by simp
next
case (Suc nat)
then show ?thesis unfolding Fact_def by simp
qed
} thus ‹⋀n. Fact f n = f n› by simp
qed
text ‹Non constructive definition of the factorial› function g ::‹nat ⇒ nat› where
‹g 0 = 1›
| ‹g (Suc n) = (g (Suc (Suc n))) div (Suc n)›
using not0_implies_Suc by auto
termination sorry
value ‹g 0› ⌦‹value ‹g 1››
text ‹Define the matching functor› definition G :: ‹(nat => nat) => (nat => nat)› where
‹G u ≡ λn. (case n of
0 ⇒ 1
| Suc m ⇒ (u (Suc n)) div (Suc n)
)
›
text ‹
Check what happens with successive applications of the functor to the null function.
› value ‹(G undef) 0› value ‹((G^^10) undef) 1› (* Cannot build g *)
text ‹
The factorial f is also a fixed point of G, but we cannot use G^^i to approximate it.
› lemma ‹G f = f› proof -
{ fix n
have ‹G f n = f n›
proof (cases n)
case 0
then show ?thesis unfolding G_def by simp
next
case (Suc m)
hence ‹G f n = (f (Suc n)) div (Suc n)› unfolding G_def by simp
also have ‹... = ((Suc n) * (f n)) div (Suc n)› by simp
also have ‹... = f n› using nonzero_mult_div_cancel_left by blast
finally show ?thesis .
qed
} thus ?thesis by (rule ext)
qed
text ‹Conjecture de Syracuse› function h :: ‹nat ⇒ nat› where
‹h n = (if n < 2 then 1
else
if (n mod 2) = 0 then
h (n div 2)
else
h (3*n+1)
)
›
by auto
termination sorry
text ‹Some checks...› value ‹h 0› value ‹h 2› value ‹h (1+1)› value ‹h 3›
text ‹Definition of the matching functor› definition Syr :: ‹(nat => nat) => (nat => nat)› where
‹Syr u ≡ (λn. (if n < 2 then 1
else
if (n mod 2) = 0 then
u (n div 2)
else
u (3*n+1)
)
)
›
text ‹Find the right power P to be able to terminate each call› value ‹Syr undef 0› value ‹Syr undef 1› value ‹(Syr^^P) undef 2› value ‹(Syr^^P) undef 3› value ‹(Syr^^P) undef 4› value ‹(Syr^^P) undef 5› value ‹(Syr^^P) undef 6›
text ‹Show that λn. 1 a fixed point of Syr› lemma ‹Syr (λn. 1) = (λn. 1)›
unfolding Syr_def by presburger
end (:endbrush:)
Fac.thy (:brush=isabelle:) theory Fac
imports Main
begin section ‹Fixed point semantics›
text ‹
In this theory, we consider functions as relations, which are sets of pairs
of elements: a ℛ b is the same as (a, b) ∈ {(x, y). x ℛ y}.
› text ‹
Fac is a functor, which takes a partial function int ⇒ int
and yields a more defined partial function.
Starting from the function defined nowhere (the empty set {}), it
yields (0,1) which is a partial function that gives the factorial of 0.
Given a partial function interpreted as a set of (n, n!) pairs, it yields
a partial function defining the (n+1, (n+1)!) pairs using:
n! = n (n-1)!, which leads to: (n+1)! = (n+1)n!
› text ‹ ▪ {} ▪ Fac {} = (0,1) ▪ Fac (Fac {}) = Fac (0,1) = (0,1), (1, 1*1) ▪ Fac (Fac (Fac {})) = Fac (0,1), (1, 1) = (0,1), (1, 1*1), (2, 2*1) ▪ Fac (Fac (Fac (Fac {}))) = Fac (0,1), (1, 1), (2, 2) = (0,1), (1, 1*1), (2, 2*1), (3, 3*2) ›
definition Fac:: ‹int rel ⇒ int rel› where
‹Fac f ≡ (0,1) ∪ image (λ(n, fac_n). (n+1, (n+1)*fac_n)) f›
text ‹
Applying Fac ten times to the empty set yields a partial function which gives the factorial of 0 .. 9 *)
› value ‹(Fac ^^ 1) {}› value ‹(Fac ^^ 2) {}› value ‹(Fac ^^ 3) {}› value ‹(Fac ^^ 4) {}› value ‹(Fac ^^ 5) {}›
value ‹(Fac ^^ 10){}›
text ‹Definition of the factorial as the least fixed point of Fac› definition fac:: ‹int rel› where
‹fac ≡ lfp Fac›
text ‹
In order to use this definition, we have to prove that Fac is monotone, i.e. that it always adds information
› lemma mono_Fac: ‹mono Fac› (* unfolding mono_def Fac_def by blast *) proof -
{
fix x::‹int rel› fix y::‹int rel› assume ‹x ⊆ y›
hence ‹Fac x ⊆ Fac y› unfolding Fac_def by blast
}
thus ?thesis unfolding mono_def by simp
qed
lemma ‹(Fac ^^ n) {} ⊆ (Fac ^^ (Suc n)) {}›
by (metis funpow_decreasing le_SucI le_refl mono_Fac)
thm funpow_simps_right text ‹
Each time we apply Fac to an approximation of fac, we get a better approximation. Show that we can compute 3! using the 4th approximation of the factorial
› lemma Fac_3 : ‹(3, 6) ∈ (Fac ^^ Suc(Suc(Suc(Suc 0)))){}›
unfolding Fac_def using funpow_simps_right by simp
lemma Four_suc:‹4 = (Suc (Suc (Suc (Suc 0))))› by simp
lemma Fac_3' : ‹(3, 6) ∈ (Fac^^4){}›
unfolding Fac_def using funpow_simps_right by (simp add: Four_suc)
text ‹Show that any iteration of Fac on the empty set is an approximation of fac› lemma fac_approx : ‹(Fac ^^ (n::nat)){} ⊆ fac› proof(induction n)
case 0 then show ?case by simp
next
case (Suc n)
then show ?case
unfolding fac_def
using lfp_unfold[OF mono_Fac]
Kleene_iter_lpfp[OF mono_Fac] by blast
qed
thm Set.subsetD thm Set.subsetD[OF fac_approx] thm Set.subsetD[OF fac_approx, of _ 4]
text ‹Show that 6 is 3!› lemma fac_3 : ‹(3, 6) ∈ fac›
using Fac_3 fac_approx by blast
end (:endbrush:)