이사벨 (Isabelle) 상수 간의 함수 정의

Question

저는 수학자이자 이사벨에게 익숙해지기 시작했습니다. 믿을 수 없을 정도로 단순해야만하는 것은 실망 스럽습니다. 어떻게 두 개의 상수 사이에 함수를 정의합니까? 함수 f : {1,2,3} \에서 {1,2,4}로 1에서 1, 2에서 4, 3에서 2로 매핑 하시겠습니까?

은 내가 사고없이 상수 T1과 T2로 세트를 정의하는 관리 가정,하지만 난이 있어야합니다 생각

definition f ::"t1 => t2" where 
"f 1 = 1" | 
"f 2 = 4" | 
"f 3 = 2" 

뭔가를 시도 할 수 없다 (그렇지 않은 데이터 유형을 것 때문에 그런 것 같아요) 이 어려움 뒤에 근본적인 오해, 그래서 어떤지도를 주셔서 감사합니다.

Answer 1

귀하의 질문에 여러 측면이 있습니다.

는

첫째, 신속하게 작업 뭔가를 얻을 수,과 같이, 대신 definition의 fun 키워드를 사용

fun test :: "nat ⇒ nat" where 
    "test (Suc 0) = 1" | 
    "test (Suc (Suc 0)) = 4" | 
    "test (Suc (Suc (Suc 0))) = 2" | 
    "test _ = undefined" 

할 수 있습니다 직접 definition 키워드를 사용하여 정의의 머리에 인수에없는 패턴 일치 반면, 당신은 fun으로 할 수 있습니다. 또한 패턴 일치에서 nat 데이터 유형 (0 및 Suc)의 생성자로 오버로드 된 숫자 리터럴 (1, 2, 3 등)을 대체했습니다.

대안과 같이, definition을 고수하지만, case 문을 사용하여 정의의 몸 내부 함수의 인수의 사례 분석을 밀어하는 것입니다 : test2 같이있는 정의

definition test2 :: "nat ⇒ nat" where 
    "test2 x ≡ 
    case x of 
     (Suc 0) ⇒ 1 
    | (Suc (Suc 0)) ⇒ 4 
    | (Suc (Suc (Suc 0))) ⇒ 2 
    | _ ⇒ undefined" 

참고가되지 않습니다 단순화 자에 의해 기본적으로 펼쳐지기 때문에 교정본에 test2의 발생을 확장하려면 간단계의 simpset에 정리 인 test2_def을 수동으로 추가해야합니다.

typedef과 함께 두 개의 3 요소 세트에 해당하는 새로운 유형을 정의 할 수도 있지만 (개인적으로는 유형을 집합으로 사용할 수 없습니다.) 직접 nat을 사용합니다.

편집 :

이

typedef t1 = "{x::nat. x = 1 ∨ x = 2 ∨ x = 3}" 
    by auto 

definition test :: "t1 ⇒ t1" where 
    "test x ≡ 
    case (Rep_t1 x) of 
    | Suc 0 ⇒ Abs_t1 1 
    | Suc (Suc 0) ⇒ Abs_t1 4 
    | Suc (Suc (Suc 0)) ⇒ Abs_t1 2" 

비록, 정말 지금까지 자신을 typedef를 사용하지 않는, 그래서이되지 않을 수도를 사용하는 가장 좋은 방법은 다른 사람이 가능하게 제안 할 수 있습니다 : 그런 짓을, typedef를 사용하는 다른 방법. typedef이하는 일은 새로운 유형에 대해 비어 있지 않은 주민 집합을 식별하여 기존 유형에서 새로운 유형을 개척합니다. auto으로 끝나는 증거 의무는 새로운 유형에 대한 정의 집합이 실제로 비어 있지 않음을 증명하기위한 것이며,이 경우에는 3 요소 집합의 새 원을 t1이라는 새로운 유형으로 조각하고 있습니다. 그래서 증명은 매우 사소합니다. Abs_t1과 Rep_t1이라는 두 개의 새로운 상수가 생성되어 내추럴과 새 유형간에 앞뒤로 이동할 수 있습니다. typedef 명령 뒤에 print_theorems을 입력하면 Isabelle이 자동으로 생성 한 t1에 대한 몇 가지 새로운 정리가 표시됩니다.