나는 다소 큰 용어 foo
을 가지고 있습니다. 나는 값'값'에서 '보조 정리'로
value "foo"
다음 이사벨이 평가 foo
를 입력 할 때 foo_value
을 말한다. 이제 다음 보조 정리를 증명하고 싶습니다.
lemma "foo = foo_value"
어떤 증명 방법을 사용해야합니까? 나는 try
을 시도했지만 시간이 초과되었습니다. 나는 수동으로 foo
에서 발생하는 다양한 정의를 펼쳐서 진행할 수있을 것 같아요,하지만 확실하게 내가 value
명령이 사용하고있는 어떤 메커니즘을 사용할 수 있어야합니까?
감사합니다. Andreas, 매우 흥미롭고 도움이됩니다. 나는 궁금하다 : 처음 두 메소드가 커널을 우회한다면, 보조 정리가 적절하게 증명되었다고 말할 수 있을까? 예를 들어, 공식 평가서 보관소에 '평가판'이 포함 된 이론을 제출하는 것이 허용됩니까? –
첫 번째 두 가지 방법 중 하나를 사용하는 경우 코드 생성기 설정이 정상적이라고 신뢰할 수 있습니다. AFP에 '평가에 의해'증명 자료를 제출하는 것이 문제가되어서는 안되며, 이미 거기에 몇 가지가있다. 사실 모든 반사 증명 방법은 평가에 의존합니다. 한 예는 AFP 엔트리의 정규 세트와 표현 http://afp.sourceforge.net/entries/Regular-Sets.shtml에있는'regexp' 메소드입니다. –