Isabelle을 사용한 삽입 정렬 알고리즘 증명

Question

Isabelle/HOL에서 코드 생성 (ML, Python 등)을위한 삽입 정렬 알고리즘을 구현했습니다. 나는 해당 함수가 잘 작동한다고 확신하지만, 그것을 증명하고 그것을 작동 시키려면 몇 가지 정리를 만들어야한다. 내 기능은 다음과 같습니다.

(* The following functions are used to prove the algorithm works fine *) 
fun menor_igual :: "nat ⇒ nat list ⇒ bool" where 
"menor_igual n [] = True" | 
"menor_igual n (x # xs) = (n ≤ x ∧ menor_igual n xs)" 

fun ordenado :: "nat list ⇒ bool" where 
"ordenado [] = True" | 
"ordenado (x # xs) = (menor_igual x xs ∧ ordenado xs)" 

fun cuantos :: "nat list ⇒ nat ⇒ nat" where 
"cuantos [] num = 0" | 
"cuantos (x # xs) num = (if x = num then Suc (cuantos xs num) else cuantos xs num)" 


(* These functions make the algorithm itself *) 
fun insertar:: "nat ⇒ nat list ⇒ nat list" where 
"insertar num [] = [num]" | 
"insertar num (x # xs) = (if (num ≤ x) then (num # x # xs) else x # insertar num xs)" 

fun asc :: "nat list ⇒ nat list" where 
"asc [] = []" | 
"asc (x # xs) = insertar x (asc xs)" 

문제는 정확하게 정리를 만드는 법을 모르겠습니다. 순서가 지정된 목록의 길이가 원본 목록과 동일하고 두 목록의 요소 이름이 같아야한다는 것을 증명해야합니다.

첫 번째 정리 목록이 올바르게 정렬되어 있음을 증명하려고

theorem "ordenado (asc xs)" 
apply (induction xs rule: asc.induct) 
apply auto 

theorem "cuantos (asc xs) x = cuantos xs x" 
apply (induction xs rule: asc.induct) 
apply auto 

, 두 번째는 두 목록이 동일한 길이를 가지고 있음을 증명하려고 : 나의 첫 번째 정리는이 있습니다.

유도 및 자동 적용시 0 정리를 얻으려는 경우 정리가 올바르며 알고리즘이 제대로 작동하지만 이후 소계를 제거하는 방법을 알지 못한다는 것을 알지 못합니다. 간단한 규칙 (lemma [simp]: "")을 수행하는 방법, 당신의 도움에 감사드립니다. asc xs가 당신은 insertar x (asc xs) 정렬되어 있음을 증명해야, 정렬 가정,

1. ⋀x xs. 
     ordenado (asc xs) ⟹ 
     ordenado (insertar x (asc xs)) 

입니다 :

Answer 1

theorem "ordenado (asc xs)" 
apply (induction xs rule: asc.induct) 
apply auto 

후 당신은 여전히 ​​다음과 같은 subgoal을 증명해야합니다. 이것은 제 경우에만 xs이 이미 정렬 된 경우 insertar x xs가 정렬한다고하는

lemma ordenado_insertar [simp]: 
    "ordenado (insertar x xs) = ordenado xs" 
... 

insertar 사이 ordenado를 상호 작용에 대한 보조 보조 정리를 증명하기 위해 제안합니다. 이 보조 정리를 증명하기 위해서는 보조 보조 정리가 다시 필요합니다. 이번에는 약 menor_igual이고 상호 작용은 menor_igual과 insertar 사이입니다.

lemma le_menor_igual [simp]: 
    "y ≤ x ⟹ menor_igual x xs ⟹ menor_igual y xs" 
    ... 

lemma menor_igual_insertar [simp]: 
    "menor_igual y (insertar x xs) ⟷ y ≤ x ∧ menor_igual y xs" 
    ... 

첫번째 후 y은 ... 등 작은 동등한 xs 모든 원소 y가 작아지는 같으면 x 및 x가 xs 작은 동등한 모든 요소 중임

나는 운동으로 증명을 남겨둔다;).

두 번째 정리에 대해서는 동일한 처방을 따르는 것이 좋습니다. 먼저 induct을 입력하고 auto을 입력 한 다음 (이미했듯이) 아직 누락 된 속성을 찾아서 보조 정리로 증명하고 교정본을 완성하십시오.