Programming and Proving in Isabelle/HOL에는 'datatype exp'로 표현되는 간단한 산술 표현식에서 'algebra_simps'를 사용하는 것이 제안 된 연습 문제 2.4가 있습니다. algebra_simps를 사용하여 그러한 표현식의 몇 가지 간단한 속성을 입증 할 수있는 예를 제시 할 수 있습니까? 예를 들어 'Mult a b = Mult b a'입니까?algebra_simps를 사용한 산술 표현식의 동등성
일반적으로 유사한 형식으로 표현 된 간단한 산술 표현식의 동등성을 입증하려고합니다 (제한된 연산자 집합 만 사용).
lemma Mult_comm: "eval (Mult a b) x = eval (Mult b a) x"
by simp
algebra_simps
당신이 eval 기능을 적절하게 정의한 경우, 당신은 당신이이처럼 예에 준 재산을 증명할 수 정수,이 경우). 그들은이 특별한 예와 아무런 관련이 없습니다. 포함 된 보조 정리를 보면 thm algebra_simps을 입력 할 수 있습니다.
정수 곱셈의 변환 성은 이미 기본 단순화 규칙이므로 어쨌든 algebra_simps이 실제로 필요하지 않습니다.
그래서, 당신은 실제로 그들을 필요로 할 경우, algebra_simps를 사용하는 예를 고려하는 방법을 보여 셈의 올바른 분배 법칙 : 당신은 그냥이에 apply simp을 시도 할 경우
lemma Mult_distrib_right: "eval (Mult (Add a b) c) x = eval (Add (Mult a c) (Mult b c)) x"
것은, 당신이 목표로 붙이게됩니다
(eval a x + eval b x) * eval c x =
eval a x * eval c x + eval b x * eval c x
다행히 규칙 algebra_simps(4) 그냥 말한다 규칙은 다음과 같습니다 thm algebra_simps(4)이 규칙은 (?a + ?b) * ?c = ?a * ?c + ?b * ?c 중임을 보여줍니다. 당신은, 그것은 algebra_simps 규칙을 사용하는 말한다면 이자벨의 simplifier 수행하여 자동으로 적용됩니다
apply (simp add: algebra_simps)
대신
apply simp