Recursion.thy
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
Fac.thy
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