locale 내에 실행 파일 inductive을 만들고 싶습니다. locale 모든 것이 잘 작동하지 않으면 : definition "P a b = True"
inductive test :: "'a ⇒ 'a ⇒ bool" where
"test a a" |
"test a b ⟹ P b c ⟹ test a c"
code_pred tes
해석없이 직접 locale 정의의 코드를 생성하고 싶습니다. 예 : (* A locale, from the code point of view, similar to a class *)
locale MyTest =
fixes L :: "string list"
assumes distinctL: "distinct L"
begin
는 다음 로케일 정의 고려 : 나는 f의 정의 나 보조 정리 f_pos 작업을하려고하면, ISAR에서 locale my_locale =
fixes a :: nat
assumes "a > 0"
begin
definition "f n ≡ a + n"
lemma f_pos: "f x > 0"
sorry
end
을, 로케일
최근에 how to drop an unwanted premise in an apply-style proof을 알게 된 지금 불필요한 변수을 삭제하는 방법에 대해 궁금합니다. 즉, y이 A, B 또는 C에 표시되지 않는 경우 내가 목표를 1. !!x y z. A ⟹ B ⟹ C
이 있다고 가정합니다. 어떻게 그것을 다음과 같이 변형 할 수 있습니까? 1.
('a × 'a) 유형의 쌍으로 작업하고 있고 패턴이 일치하는 fun을 정의한다고 가정 해 봅시다. 내가 증거 적용 스타일의 쌍을 표현 (a,b)로 교체 할 수있는 방법 fun test :: "('a × 'a) ⇒ 'a ⇒ bool" where "test (a,b) c = True"
지금 형 ('a × 'a)의 변수 a_b이있는 경우. 예를 들어, 다음
몫 유형 (natq)으로 옮기고 싶은 부분에 부분적으로 정의 된 연산자 (disj_union)가 있습니다. 도덕적으로,이 은이어야한다고 생각합니다. 동등한 클래스 에서 찾을 수 있기 때문에 연산자가 정의 된 대표자 인입니다. 그러나 disj_union은 부분적으로 만 정의 되었기 때문에 해제 된 정의가 동등성을 유지한다는 증거를 완성 할 수 없습니다. 아래
는 다음과 같은 바보 같은 예를 생각해 theory meta_all
imports Main
begin
lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A"
apply(blast)
done
lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)"
apply(blast)
코드 생성에 대한 매우 간단한 정의가 있다고 가정하면. 특정 경우에만 정의되며 달리 런타임 예외가 발생합니다. definition "blubb a = (if P a then True else undefined)"
이제 blubb을 표시하고 싶습니다. 예외가 발생하는 경우는 무시해야합니다 (내 관점에서 보면 수학적 관점이 아님). 그러나 임의의 값인 X이
이 질문은 Isabelle/HOL 정리 정리기를 사용한 코드 생성을 참조합니다. 나는 목록 export_code distinct in Scala file -
나는 다음과 같은 코드 def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match {
case (Nil, y) => fal
적용 스크립트에서 apply (rule)을 사용하면 일반적으로 적절한 규칙이 선택됩니다. 구조화 된 증명에서 proof에 대해서도 마찬가지입니다. 사용 된 규칙의 이름은 어디에서 배울 수 있습니까? Pure.intro/intro/iff (또는 ? 또는 ! 변종 중 하나)로 선언