2014-04-03 1 views
1

나는 다소 큰 용어 foo을 가지고 있습니다. 나는 값'값'에서 '보조 정리'로

value "foo" 

다음 이사벨이 평가 foo를 입력 할 때 foo_value을 말한다. 이제 다음 보조 정리를 증명하고 싶습니다.

lemma "foo = foo_value" 

어떤 증명 방법을 사용해야합니까? 나는 try을 시도했지만 시간이 초과되었습니다. 나는 수동으로 foo에서 발생하는 다양한 정의를 펼쳐서 진행할 수있을 것 같아요,하지만 확실하게 내가 value 명령이 사용하고있는 어떤 메커니즘을 사용할 수 있어야합니까?

답변

4

value의 다른 평가 매커니즘에 대응하는 세 증거 방법이있다 :

  • eval 코드 발생기가 사용; value [code]에 해당합니다. 생성 된 ML 코드가 True으로 평가되면 증명이 성공합니다.
  • normalization은 ML의 기호 정규화 엔진에 문을 컴파일합니다. 그것은 value [nbe]을 모방합니다.
  • code_simp은 평가판으로 Isabelle 's simplifier를 사용합니다. value [simp]에 해당합니다.

tutorial on code generation은 이러한 증명 방법을보다 자세히 설명합니다. evalnormalization은 oracles처럼 행동합니다. 즉, 그들은 code_simp의 모든 평가 단계가 커널을 통과하는 반면 Isabelle의 커널을 우회합니다. 일반적으로 evalnormalization보다 빠르며 normalizationcode_simp보다 빠릅니다.

+0

감사합니다. Andreas, 매우 흥미롭고 도움이됩니다. 나는 궁금하다 : 처음 두 메소드가 커널을 우회한다면, 보조 정리가 적절하게 증명되었다고 말할 수 있을까? 예를 들어, 공식 평가서 보관소에 '평가판'이 포함 된 이론을 제출하는 것이 허용됩니까? –

+1

첫 번째 두 가지 방법 중 하나를 사용하는 경우 코드 생성기 설정이 정상적이라고 신뢰할 수 있습니다. AFP에 '평가에 의해'증명 자료를 제출하는 것이 문제가되어서는 안되며, 이미 거기에 몇 가지가있다. 사실 모든 반사 증명 방법은 평가에 의존합니다. 한 예는 AFP 엔트리의 정규 세트와 표현 http://afp.sourceforge.net/entries/Regular-Sets.shtml에있는'regexp' 메소드입니다. –

1

나는 모든 경우에 작동하는지 잘 모르겠지만, 당신은 시도 할 수 : 많은 경우에

lemma "foo = foo_value" 
    by eval 

는, by simp도 작업을해야하고 나는 그런 의미에서 (eval는 오라클의 종류 것 같다 커널에 의해 완벽하게 검증되지 않았기 때문에 내가 잘못하면 누구든지 나를 바로 잡으십시오.)