임의의 용어에 단순화 자 적용하기

Question

나는이 용어를 염두에두고있다. 예를 들어 "foo 1 2 a b"이고, 이사벨이 나를 위해 그것을 단순화 할 수 있는지 알고 싶다.

simplify "foo 1 2 a b" 

과 같은 것을 쓰고 간단한 용어가 출력 버퍼에 인쇄되어 있습니다. 이것이 가능한가?

나의 현재 '해결 방법'입니다 : 잘 작동하지만 조금 해키 보인다

lemma "foo 1 2 a b = blah" 
apply simp 

. (내 경우) 작동하지 않습니다 무엇

은 다음과 같습니다

value "foo 1 2 a b" 

a 때문에 b은 언 바운드 변수, 내 foo는 코드 생성기가된다는 무한 집합 및 기타 멋진 물건을 수반하기 때문이다.

Answer 1

AFAIK는 내장 기능이 없지만이를 달성하는 데는 여러 가지 방법이 있습니다. 당신은 이미 그 중 하나를 발견했습니다, 즉 용어를 보조 정리로 서술 한 다음 단순화기를 호출하십시오. 단점은 모든 상황에서 사용할 수 없다는 것입니다 (예 : 적용 증명 스크립트 내부가 아닌 경우).

또는 [simplified] 속성을 통해 단순화를 호출 할 수 있습니다. 이것은 thm 명령을 통해 모든 컨텍스트에서 작동하며 출력 버퍼에 출력을 생성합니다. 먼저, 정리를 정리에 주입해야합니다. 그러면 simplify을 정리에 적용하고 thm과 함께 결과를 표시 할 수 있습니다. 여기에 잡동사니의 이론에 들어갈 수있는 준비물이 있습니다.

definition simp :: "'a ⇒ bool" where "simp _ = True" 
notation (output) simp ("_") 
lemma simp: "simp x" by(simp add: simp_def) 

그런 다음

thm simp[of "foo 1 2 a b", simplified] 

를 작성하고 출력 창에서 단순화 된 용어를 볼 수 있습니다.

평 가가 일반적으로 사용하는 simpset보다 다른 재 작성 규칙 세트 (코드 방정식)를 사용하기 때문에 평가 메커니즘이 원하는 것이 아닐 수 있습니다. 따라서 이것은 단순화기를 적용하는 것보다 다른 용어로 평가할 가능성이 높습니다. 차이를 확인하려면 lemma "foo 1 2 a b = blah"으로 simp 대신 code_simp을 적용하십시오. 증명 방법 code_simp은 value [simp]처럼 코드 방정식을 사용합니다.

Answer 2

value 명령을 사용하는 경우 인수 평가는 등록 된 평가자가 수행합니다 (Isabelle2013-2의 Reference Manual 참조).

value 명령에 추가 인수를 제공하여 이전 버전의 Isabelle (예 : Isabelle2013-2)에서 평가자를 명시 적으로 선택하는 것이 가능했습니다. 예

value [simp] "foo 1 2 a b" 

이 Isabelle2014이 파라미터가 삭제되었음을 보인다 Isabelle2014의 Reference Manual에있어서, 상기 전략은 이제 처음 사용 ML 부호 생성에 고정되고, 경우에이 평가에 의해, 정규화 실패.

Isabelle의 개발 버전 (e82c72f3b227)에있는 NEWS 파일에서이 매개 변수가 곧 출시 될 Isabelle 릴리스에서 다시 활성화되는 것처럼 보입니다.

UPDATE : 안드레아스 지적으로 value [simp]가 apply simp로 단순화 동일한 규칙을 사용하지 않습니다. 따라서 위에서 설명한 솔루션을 사용하더라도 원하는 결과를 얻지 못할 가능성이 높습니다.