나는 fun foo :: "nat ⇒ nat"
where "foo = Suc"
이사벨은 "함수는 인수가 없다"고 불만을 작성하려고합니다. 왜 이런거야? 인수가없는 fun의 문제점은 무엇입니까? fun을 abbreviation 또는 definition으로 변경할 수 있으며 모두 정상입니다. 그러나 모든 다른 정의가 fun으로 선언 된 나의 .thy 파일
에서 일반적인 정의 작업과 나는 보조 정리가 해결 definition func :: "real ⇒ real"
where "func x = x"
에 FUNC의 정의를 교체하면 나는 그러나 다음 definition func :: "real ⇒ real"
where "func = real"
lemma "(λh. (func (x+h))) -- 0 -->
나는이 용어를 염두에두고있다. 예를 들어 "foo 1 2 a b"이고, 이사벨이 나를 위해 그것을 단순화 할 수 있는지 알고 싶다. simplify "foo 1 2 a b"
과 같은 것을 쓰고 간단한 용어가 출력 버퍼에 인쇄되어 있습니다. 이것이 가능한가? 나의 현재 '해결 방법'입니다 : 잘 작동하지만 조금 해키 보인다 lemma "foo 1 2 a
일부 Isabelle 술어를 삭제하기 위해 HOL-Z의 수학 툴킷을 사용하고 있습니다. 특히 나는 부분적인 함수 정의를 사용하여 필자가 작성한 Z 사양에서 관계의 일부를 정의하고있다. 여기서는 간단한 HOL 술어를 생성 할 수 있도록 스키마를 명세서로 변환한다. I 쓸 때 조건부 내에 다음 type_synonym ('a,'b) lts = "('a*'b)
나는 "Concrete semantics with Isabelle/HOL"을 읽고 있으며 고차원 논리에 매우 흥미로워지고 있습니다. 나는 보통의 1 차 논리와 몇 가지 모달 논리를 알고 있지만, 고차원 논리와 그 메타 이론에 대한 이전의 노출은 거의 없다. 그래서 나는 그 격차를 메꾸기를 원한다. 나는 HOL이 본질적으로 교회의 단순한 유형의 이론이고 순수
난 그냥 이자벨에서 시작하고있어 Concrete Semantics의에서 운동 3.3을 통해 작업하는 동안 나는 형 통일 오류를 받고 있어요 : 는 대체 함수를 정의 subst :: vname ⇒ aexp ⇒ aexp ⇒ aexp
subst x a e은 x의 모든 어커런스를 a으로 바꿔 결과가 e입니다. 예를 들어 : theory Scratchpad
i
나는 정리를 증명하려고 노력하고 있지만 부차적 인 목표에 갇혀있다. (내가 건너 뛰고 나중에 증명하는 것을 선호한다.) 어떻게 내가 이것을 건너 뛰고 다른 사람들을 증명할 수 있을까요? 먼저, oops과 sorry을 시도했지만 둘 다 (부 목적이 아닌) 전체 증명을 중단합니다. 나는 또한 보조 목표를 더미 보조 정리 (sorry으로 증명 된 가정)에 넣으려
isar에 정수 지수에 대한 간단한 증거를 작성하려고합니다. 나는 코멘트 영역에서 만들고 싶은 논점을 썼다. 그러나 표현하는 방법을 생각해 내는데 어려움을 겪고있다. 나는 src/HOL/Int.thy을 공부했지만, 나는이 라인들을 따라 예제 증거를 찾지 못하거나 내가 아직보고있는 것을 이해하지 못한다. :) theory Exponents
imports M