伊莎貝爾簡單的雙功能

Question

伊莎貝爾的新品牌，以及一般的HOL編程。 教科書中的練習之一是：

定義一個遞歸函數double :: nat⇒nat並證明double m = add m m。

im仍然試圖定義它，但我無法弄清楚。， 這是我迄今爲止所做的。

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

我有一個函數add定義如下。

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

但我不認爲我打算在double的定義中使用add。 也是一個解釋與答案將不勝感激。 謝謝 陰雨

Answer 1

揣摩如何在double n和Suc來表達double (Suc n)。這將給你一個遞歸的定義。