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

Question

외래 재귀 함수 (fun이 아닌 function을 사용)를 작성하면 코드 생성기가 종료 증명을 제공하지 않으면 내 함수 실행을 거부합니다 - 심지어 sorry- 방패로 충분합니다.

theory Misc imports 
    Main 
    "~~/src/HOL/Library/Code_Target_Numeral" 
begin 

function foo :: "nat list ⇒ nat list list" 
where 
    "foo G = (
    if G = [] then 
    map concat [[G]] 
    else 
    concat (map foo (map (λx. [Suc x]) (tl G))) 
)" 
by auto 
termination sorry 

value "foo [1,2,3]" 

end 

현재 value 명령이 올바른 결과 "[]"를 반환 여기 내 최소한의 작업 예입니다합니다 (foo 기능의 내용에 대해 걱정하지 마십시오, 그것은 증거가 아닌 사소한 종단 그냥 무작위 기능이다). 그러나 라인 termination sorry을 제거하면 value 명령은 "foo [1, 2, 3]"을 반환합니다.

sorry과 이론 파일을 망칠 필요없이 코드 생성기를 foo으로 실행할 수있는 방법이 있습니까? 나는 실제적으로 을하고 싶지 않다.은 정말 어려운 증거이기 때문에 해지 증명을해야한다.

Answer 1

Chris의 의견은 귀하의 질문에 대한 답변이지만, 필자는 예제를 제공 할 것이라고 생각했습니다.

비 종결 기능에는 심장 마비를 일으킬 수있는 능력이있어 종단 증명이 필요합니다 (또는 적어도 sorry 이상). 다음 함수 정의와 예를 들어

:

function f :: "nat ⇒ nat" where "f n = f n + 1" 
    by auto 

termination 
    sorry 

우리는 다음 False을 증명하기 위해 갈 수

lemma "False" 
    by (metis a.f.elims add_eq_self_zero if_1_0_0) 

unsoundness 제공을 함수의 비 종단에서.

구체적인 예를 들면, 종료 증명은 그리 어렵지 않습니다. 목록 G의 길이가 항상 감소한다는 것을 알 수 있습니다. 다음과 같이 측정 함수를 사용하면 값이 감소 함을 알 수 있습니다.

termination 
    (* Give Isabelle a termination relation. We say that the length 
    * of the parameter is strictly decreasing to 0. *) 
    apply (relation "measure length", simp) 

    (* simplify *) 
    apply clarsimp 

    (* Sledgehammer can now solve this goal, but by hand is a bit neater. *) 
    apply (drule length_pos_if_in_set, clarsimp) 
    done