Isabelle simple double function

0
votes

Im brand new to Isabelle, and HOL programming in general. One of the exercises in a text book is to:

Define a recursive function double :: nat ⇒ nat and prove double m = add m m.

Im Still trying to define it but i can't figure it out., Here is what i have done so far.

fun double :: "nat => nat"  where
"double 0 = 0" |  //my base case
"double (n) =  //I don't know what to do here

I have a function add defined as follows.

fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

but i don't think I'm meant to use add in the definition of double. Also an explanation with the answer would be greatly appreciated. Thank you, Rainy

1
recursionlogicisabelle

1 Answers

1
votes

Try to figure out how to express double (Suc n) in terms of double n and Suc. That willl give you a recursive definition.