Re: [isabelle] change proposal: eliminating overloading for factorials



Presumably for the Fibonacci numbers too? Currently

fun fib :: "nat \<Rightarrow> nat"
where
    fib0: "fib 0 = 0"
  | fib1: "fib (Suc 0) = 1"
  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"


Larry

> On 28 Feb 2015, at 08:18, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
>> What about defining fact semi-polymorphic? Like
>>  fact :: nat => 'a::semiring_1
> 
> The nice thing about this is that simple propositions involving numerals
> are provable out of the box:
> 
>> context semiring_1
>> begin
>> 
>> primrec factorial :: "nat â 'a"
>> where
>>  "factorial 0 = 1"
>> | "factorial (Suc n) = of_nat (Suc n) * factorial n"
>> 
>> lemma "factorial 3 = 6"
>>  by (simp add: eval_nat_numeral)
>> 
>> end
> 
> This is again one of the things where you ask yourself how it could have
> been different in the past after you got used to it.
> 
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.