S
Есть тут кто Isabelle/HOL тыкал?
theory Mul
imports Main
begin
fun mul :: "nat ⇒ nat ⇒ nat"
where
"mul n 0 = 0" |
"mul n (Suc(m)) = n + mul n m"
lemma[simp]: "mul 0 m = 0"
apply (induction m)
apply auto
done
lemma[simp]: "mul (Suc n) m = m + n * m"
apply (induction m)
apply auto
done
lemma "mul n m = n * m"
apply (induction n)
apply auto
done
end
