如何在伊莎貝爾證明最大交換性質

Question

我對伊莎貝爾非常新，所以請有憐憫。如何用此功能證明最大交換屬性？

fun max :: "nat => nat => nat" where 
"max 0 0 = 0" | 
"max (Suc x) 0 = Suc x" | 
"max 0 (Suc x) = Suc x" | 
"max (Suc x) (Suc y) = Suc (max x y)" 

lemma "max x y = max y x" 
? ? ? 

我知道，它可以很容易地證明了

definition max :: "nat ⇒ nat ⇒ nat" where 
"max x y = (if x ≥ y then x else y)" 

lemma "max x y = max y x" 
apply(simp add:max_def) 
done 

這不是一個家庭作業。我真的很好奇，並希望儘可能多地瞭解伊莎貝爾和數學證明。謝謝你的時間。

Answer 1

證明遞歸定義函數的一些事實的典型方法是歸納法，其中歸納的結構遵循遞歸定義的結構。

在伊莎貝爾，你可以用induct方法進行歸納。如果您編寫induct n的自然數爲n，則會得到兩種情況：n = 0和n是某件事的繼承者的情況。

但是，在這種情況下，您應該使用函數包爲max提供的歸納規則，它被稱爲max.induct。所以，只要做你的目標apply (induction x y rule: max.induct)，然後看看你留下了什麼。這對於你想要證明的東西來說已經足夠了。

但是，您已經提到了替代定義if x ≥ y then x else y。根據該定義，一些證據（如max的結合性）可能更容易。在這種情況下，你可以簡單地證明這種替代定義

lemma max_altdef: "max x y = (if x ≥ y then x else y)" 

，然後使用的任何定義是爲您在各種情況下更方便。 max_altdef的證明也是一個簡單的歸納。