How to Beweisen Commutative Eigenschaft des Maximums in Isabelle

Question

Ich bin extrem neu zu Isabelle, also bitte erbarme dich. Wie kann ich mit dieser Funktion die kommutative Eigenschaft des Maximums nachweisen?

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" 
? ? ? 

Ich weiß, dass es leicht für

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 

nachgewiesen werden diese Zuordnung keine Hausaufgaben. Ich bin wirklich neugierig und würde gerne so viel wie möglich über Isabelle und mathematische Beweise verstehen. Vielen Dank für Ihre Zeit.

Answer 1

Der typische Weg, eine Tatsache über eine rekursiv definierte Funktion zu beweisen, ist die Induktion, bei der die Struktur der Induktion der Struktur der rekursiven Definition folgt.

In Isabelle können Sie Induktion mit der induct Methode tun. Wenn Sie induct n für eine natürliche Zahl n schreiben, werden Sie zwei Fälle erhalten: der Fall, in dem n = 0 und der Fall n der Nachfolger von etwas ist.

In diesem Fall sollten Sie jedoch die für max vorgesehene Induktionsregel durch das Funktionspaket verwenden, das max.induct heißt. Also, tun Sie einfach apply (induction x y rule: max.induct) auf Ihr Ziel und sehen Sie, was Sie hinterher übrig haben. Dies ist ausreichend für das, was Sie beweisen möchten.

Sie haben jedoch bereits die alternative Definition if x ≥ y then x else y erwähnt. Einige Beweise (wie die Assoziativität von max) sind wahrscheinlich leichter mit dieser Definition. In solchen Fällen können Sie diese alternative Definition einfach als

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

prüfen und dann die für Sie in jeder Situation geeignetere Definition verwenden. Der Beweis von max_altdef ist auch eine einfache Induktion.