isabelle

0열

1답변

Programming and Proving in Isabelle/HOL에는 'datatype exp'로 표현되는 간단한 산술 표현식에서 'algebra_simps'를 사용하는 것이 제안 된 연습 문제 2.4가 있습니다. algebra_simps를 사용하여 그러한 표현식의 몇 가지 간단한 속성을 입증 할 수있는 예를 제시 할 수 있습니까? 예를 들어 'Mul

1열

1답변

이사벨 구문 번역 : Force eta-expansion?

이자벨의 목록 이론 filter에 대한 구문 번역을 설정 한 : syntax -- {* Special syntax for filter *} "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])") translations "[x<-xs . P]"== "CONST fi

1열

1답변

Isabelle/JEdit에서 xsymbols가 사용됩니까? <a href="http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf" rel="nofollow">Isabelle/HOL tutorial</a>의 섹션 4.1.2에서

우리는 증명 일반의 X-기호 모드 또는 LaTeX의 출력이 활성화 될 때마다 이 규칙에 따라 "xsymbols"의 모드가 활성화되어 찾을 수 있습니다. 이제 일반 사무 총장의 퇴색과 관련하여 xsymbols와 관련이 있습니까?

0열

1답변

구문 "F;"를 번역하고 싶습니다. "참 참 참 참"으로하고, "부울 목록"에서 사용하는

이 내가 원하는 것을 나타내지 만 이는 작동하지 않습니다이 syntax "_F_hex" :: "any => any" ("F;") translations "F;" => "True,True,True,True" 이 같은 F;을 사용합니다 : [F;,F;] == [True,True,True,True,True,True,True,True]

0열

2답변

Lueng의 RegExp 라이브러리가 Isabelle/ML에서 작동합니까? Isabelle/ML에 사용할 regex lib devs가 있습니까?

1 : 누구나 알고 있습니까? Lueng's RegExp library은 Isabelle/ML과 함께 작동합니까? Q2 : 개발자가 Isabelle/ML 용으로 사용하는 표준 정규식 라이브러리가 있습니까? 필자는 스칼라를 배우기위한 큰 계획을 가지고 있었는데, 나의 주요 응용 프로그램은 TEX 파일을 생성하기 위해 THY를 처리하려고했다. 나는 스칼라에 대

1열

1답변

내부 구문 주석 내부의 큰 따옴표

" 문자는 큰 따옴표로 묶인 Isabelle의 내부 구문에 주석 안에 넣을 때 예상대로 동작하지 않습니다. 명확히하기 위해 : 다음 함수 정의에서, 나는 the "at" sign이 주석으로 해석 될 것으로 기대한다. 실제로 Isabelle은 주석의 첫 번째 " 문자를 해당 라인의 시작 부분 인 "과 일치 시키므로 구문 오류가 발생합니다. fun revers

2열

1답변

평등 이사벨 사이의 용어는 일부

좀 놀랐어요 그 value "let x = SOME n. n ∈ {1::int,2} in x = x" 반환 True. 베타 확장 및 α 이름 바꾸기 이후 해당 용어는 다음과 동일합니다. value "(SOME na. na ∈ {1::int,2}) = (SOME nb. nb ∈ {1::int,2})" 이 동등성을 유지해야하는 이유가 없습니다. na의

1열

1답변

Isabelle은 종결 증명없이 내 재귀 함수 코드를 생성하지 않습니다

외래 재귀 함수 (fun이 아닌 function을 사용)를 작성하면 코드 생성기가 종료 증명을 제공하지 않으면 내 함수 실행을 거부합니다 - 심지어 sorry- 방패로 충분합니다. theory Misc imports Main "~~/src/HOL/Library/Code_Target_Numeral" begin function foo :

1열

2답변

'값'에서 '보조 정리'로

나는 다소 큰 용어 foo을 가지고 있습니다. 나는 값 value "foo" 다음 이사벨이 평가 foo를 입력 할 때 foo_value을 말한다. 이제 다음 보조 정리를 증명하고 싶습니다. lemma "foo = foo_value" 어떤 증명 방법을 사용해야합니까? 나는 try을 시도했지만 시간이 초과되었습니다. 나는 수동으로 foo에서 발생하는 다

1열

1답변

inductive_set의 모노 속성 사용

나는 inductive_set이 필요한 단조 로움 요구 사항을 만족 시킨다는 것을 증명하기 위해 고심하고 있습니다. 누군가 제가 여기서 잘못하고 있다고 조언 할 수 있습니까? 이처럼 조성을 보조 정리를 명시하는 경우 theory Scratch imports Main begin consts foo :: "'a set ⇒ 'a set" lemma foo