Простая лемма в Изабель

Question

Я пытался научиться использовать Изабель и столкнулся с проблемой. Следующая лемма работает:

lemma sum_square: "(a+b)^2=a^2+(2::real)*a*b+b^2"
apply (simp add: power2_eq_square) 
output: (a + b) * (a + b) = a * a + 2 * a * b + b * b

однако следующая лемма не имеет:

lemma sum_sq: "(a+b)^2 = (a+b) * (a+b)"
apply (simp add: power2_eq_square)
output: Failed to apply proof method

Может кто-нибудь сказать мне, что я делаю не так?

Кроме того, может ли кто-нибудь направить меня к учебникам Изабель или простым доказательствам, через которые я могу работать, чтобы расширить свои знания об Изабель?

Answer 1

В Изабель несколько операторов, таких как умножение, сложение, возведение в степень и т. Д., Являются полиморфными и чисто синтаксическими. Т.е. в вашем заявлении (a+b)^2 = (a+b) * (a+b) тип a а также b может быть чем угодно, и не обязательно является числовым типом.

Вы можете обнаружить такие случаи с помощью Ctrl-click или Ctrl-hover по соответствующей лемме и переменным. Например, power2_eq_square определяется в контексте monoid_multтолько если a а также b имеют тип, который также является monoid_multТогда применима лемма. Тем не менее, тип a является 'a :: {numeral,power},

Что касается учебников, просто нажмите на Documentation в правой части окна Isabelle/jEdit, а затем два учебника prog-prove а также tutorial стать видимым