와 문제를합니까 : 어떻게 그것을 예라면 setprod f (UNIV :: 'n∷finite set) = setprod (λx. x) (f ` (UNIV :: 'n∷finite set))
, 증명할 수 있습니까? (* tested with Isabelle2013-2 *)
theory Notepad
imports
Main
"~~/sr
에서 ==> B ==> C ==> B를 증명 나는 이자벨에 A ==> B ==> C ==> B
증명에 대해 의아해입니다. 분명히 당신은 할 수있다 apply simp
그러나 나는 이것을 규칙을 사용하여 어떻게 증명할 수 있었느냐? 또는 규칙을 덤프하는 방법이 있습니까 simp? 감사.
에 대해서 *과 **의 차이점은 무엇이며 A * 1 and A ** mat 1`은 무엇입니까? 예 :가 이사벨에 lemma myexample:
fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
shows "(A * 1 = A) ∧ (A ** (mat 1) = A)"
by (metis comm_se
인증 된 프로그램을 설계하는 데 Coq를 사용하는 방법에 대해 이야기하는 여러 연구 그룹과 적어도 한 권의 책을 봅니다. 인증 프로그램의 정의에 대한 합의가 있습니까? 제가 말할 수있는 것에서는, 그것이 의미하는 바는 모두 프로그램이 합법적이고 정확한 타입임을 증명했습니다. 이제 프로그램의 유형은 비어 있고, 정렬되어 있고,> 5와 같은 요소가 포함되어 있
simp 메소드가 튜플을 그 구성 요소로 분할하는 것을 어떻게 멈출 수 있는가? 예. 내가 fun foo where "foo z = blah z"
lemma "∃z :: nat × nat × nat × nat × nat. foo z"
를 작성하는 경우 증거 상태 ∃z. foo z입니다. 그런 다음 쓸 경우 apply (simp)
증명 상태는 ∃a
내 목표 상태 인 경우 foo ==> bar --> qux의 반대, 내가 목표 상태 foo ==> bar ==> qux를 산출하기 위해 문 apply (intro impI)
를 사용할 수 있다는 것을 알고. 다른 방향은 어떨까요? 어떤 명령이 나를 목표 상태 foo ==> bar --> qux으로 보내겠습니까? 내가 지금까지 함께 온 가장 좋은는 app
대 시도를 실행할 때 내가 (이이 제목에 언급되지 않음) 슬레지 해머 결과에서 는 의 출력이 실행하는 동안 종종 쇠망 에서 다양한 결과를 제공하려고 만 보면 이유는 완전히 다른 결과를 얻을 수 있습니까 슬레지 해머가 직접 제로 (!) 결과를줍니다. 이제 슬레지 해머의 디자인 목표는 결정론이 아닙니다. as stated by Lawrence Paulson.
instance+[ ]nat 및 instantiation+[ ]nat과 함께 src/HOL 폴더에 grep을 작성했는데 nat에 대해 인스턴스화 된 모든 유형 클래스를 찾을 수 있습니다. 내가 또한 int, rat 및 real 인스턴스화 한 방법을 살펴 것이 중요하기 때문에 유형 클래스에 대한 종속성을 표시합니다 print_dependencies처럼 그 일
이 질문은 related to my last question입니다. 제 질문에 대한 대답은 "입니다. 일반적으로 작업을 위해 리포지토리 버전을 사용하는 것은 좋지 않습니다." ". 그렇다면 내 질문은입니다. mecurial 저장소의 개발 버전을 사용하는 가장 큰 단점은 무엇입니까? 내 경험 Isabelle2013-2 단순히 완전히 사용할 수 없게 점이다 :
랩탑에서 Isabelle/jEdit으로 작업하고 있습니다. 노트북에는 4 개의 코어 즉 4 개의 CPU가 있습니다. 그러나 나는 또한 다음 방에 서버 컴퓨터를 가지고있다. 서버에는 20 개 이상의 CPU가 있습니다. 일반적으로 시도 결과가 sledgehammer 자체가 실패한 슬레지 해머 결과를 제공하기 때문에 sledgehammer과 try을 병렬로 실행