isabelle

1열

1답변

이사벨 (Isabelle)의 ML 프로그래밍 : 내장 함수 및 전술 중 일부를 찾을 수 없음

이사벨 (Isabelle)에 ML 코드를 작성하기 위해 "이사벨 요리 책"을 연구 중입니다. 불행히도 내장 함수를 찾을 수 없으므로 (이름이 변경되었거나 경로 structure.fct를 지정해야하기 때문에) 많은 예제가 작동하지 않습니다. 예를 들어 etac, rtac 및 atac을 사용하는 예제는 더 이상 작동하지 않습니다. 새로운 이름은 무엇이며 어떻게

0열

2답변

Isabelle/jEdit에서 세트 이론의 기호를 입력하는 방법은 무엇입니까?

Isabelle/jEdit에 어떻게 ∈, ⊆, ∪, ∩ 같은 기호를 입력 할 수 있습니까? Isabelle/HOL 자습서에 "", "< =", "Un"및 "Int"를 입력해야한다고 나와 있습니다. 그러나 "< ="은 ≤을 제공하고 다른 기호는 전혀 기호로 변환되지 않습니다. "\ <에 >"또는 그 접두어를 입력하고 마우스로 원하는 기호를 선택하는 것만 볼

1열

2답변

AFP의 'find_theorems`

find_theorems 메커니즘을 사용하여 정식 교정 자료 (AFP) 전체 보관소를 검색하려면 어떻게해야합니까? 내 컴퓨터에 보관 파일을 다운로드했으며 여기에서 이론을 가져올 수 있습니다. 예를 들어, 내가 imports Kleene_Algebra.Kleene_Algebra_Models이라고 쓰면 그 이론의 모든 정리가 성공적으로 나에게 제공된다. 하지만

0열

1답변

이사벨에서 규칙 유도와 변수 일반화를 어떻게 결합 할 수 있습니까?

이사벨 (Isabelle)에서는 arbitrary 키워드를 사용하여 유도 증명에 변수를 일반화 할 수 있습니다. 이것은 보통 유도를 위해 확실히 작동합니다 (예 : apply (induction n arbitrary: m)). apply (induction rule: R.induct)에서와 같이 규칙 유도를 사용할 수도 있습니다. 그러나 규칙 유도를 사용할

0열

1답변

Isabelle/Isar에 여러 변수가있는 실존 적 명제를 효과적으로 증명하려면 어떻게해야합니까?

Isabelle/Isar에 보조제 ∃ n m k . [n, m, k] = [2, 3, 5]을 증명하고 싶다고 말합니다. 45 페이지의 이자벨/HOL 튜토리얼에 제안 내가 가서 경우 다음과 같이 내 증거는 같습니다 물론 lemma "∃ n m k . [n, m, k] = [2, 3, 5]" proof show "∃ m k . [2, m, k] =

0열

1답변

"4.6 Isabelle/HOL에서의 프로그래밍과 증명"의 연습 4.6에있는 보조 정리를 증명하려면 어떻게해야합니까?

저는 "4.6 Isabelle/HOL에서의 프로그래밍과 증명"에서 Exercise 4.6을 풀려고합니다. 목록을 집합으로 변환하고 보조 정리 "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"을 증명하는 함수 elems :: "'a list ⇒ 'a set"을 정의 할 것을 요구합니다. 지금까지, 나는

0열

1답변

이사벨 유형 오류

저는 이사벨에게 신입생이며 대학 운동을하고 있습니다. 이사벨의 역기능을 증명할 필요가있어. 하스켈에서 함수는 다음과 같을 것이다 : 지금 이자벨에서이 기능을 "회전"을 정의하는 tryed rev [] = [] rev (x:xs) = rev xs ++ [x] . Type unification failed: Clash of types "_ ⇒

0열

1답변

이사벨에서 임의의 기호의 음수 버전을 사용할 수 있습니까?

이사벨 (Isabelle)은 특정 다른 기호의 부정 버전 인 기호를 사용할 수있게합니다. 예 : ≠ 및 ∉입니다. LaTeX의 \not 매크로와 같은 임의의 기호의 부정 버전을 가져 오는 메커니즘이 있습니까?

1열

2답변

이자벨에서 유도 적으로 정의 된 관계의 비 반사성을 어떻게 증명할 수 있습니까?

이자벨에서 예를 들어 자연수의 불평등의 다음과 같은 정의를 생각해 inductive unequal :: "nat ⇒ nat ⇒ bool" where zero_suc: "unequal 0 (Suc _)" | suc_zero: "unequal (Suc _) 0" | suc_suc: "unequal n m ⟹ unequal (Suc n

2열

1답변

이사벨 simplifier는 경우 문에 대한 경우의 차이를 소개합니다 (왜 때?)는 내가 만약 표현을 포함하는 목표에 바보-방법을 적용하는 경우

는 simplifier 자동 사례 구별 소개 : lemma "undefined (if x then True else False)" apply simp 이를 목표를 준다 : (x ⟶ undefined True) ∧ (¬ x ⟶ undefined False) 내 질문은 : 단순화자가 어떻게 이것을 지시 했습니까? 나는 이것이 단순한 규칙을 발견