如何證明加倍函數的逆轉等於Isabelle中的逆轉函數的加倍？

Question

我有形式

double [x1, x2, ...] = [x1, x1, x2, x2, ...] 

即

fun double :: " 'a list ⇒ 'a list" 
where 
    "double [] = []" | 
    "double (x#xs) = x # x # double xs" 

和反轉列表中的元素與另一個功能snoc，增加的幫助功能雙打列表的元素的功能一個元素列表的右側：

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" 
where 
    "snoc [] x = [x]" | 
    "snoc (y # ys) x = y # (snoc ys x)" 


fun reverse :: "'a list ⇒ 'a list" 
where 
    "reverse [] = []" | 
    "reverse (x # xs) = snoc (reverse xs) x" 

現在我要證明

lemma rev_double: "rev (double xs) = double (rev xs)" 

爲真。

我試圖上xs

lemma rev_double: "rev (double xs) = double (rev xs)" 
by (induction xs) 

應用誘導和我寫輔助引理double_snoc，其確保倍增列表是相同的它的第一元件和列表的其餘部分（其使用函數倍增snocleft其以列表的左端插入的元件）

fun snocleft::"'a list ⇒ 'a ⇒ 'a list " 
where 
    "snocleft [] x = [x]" | 
    "snocleft (y # ys) x = x # (y # ys)" 


lemma double_snoc: "double (snocleft xs y) = y # y # double xs" 
by (induction xs) auto 

我還沒有作出證明引理任何進展。你有什麼解決方案或提示如何設置證明？

Answer 1

您將函數定義爲reverse，但是在所有引理中，都使用rev，指的是預定義的列表反轉函數rev。

你是什麼意思大概是這樣的：

lemma reverse_double: "reverse (double xs) = double (reverse xs)" 

如果試圖通過感應（與apply (induction xs)）來證明這一點，你會卡在感應的情況下與以下目標：

snoc (snoc (double (reverse xs)) a) a = 
    double (snoc (reverse xs) a) 

這應該是直觀的顯而易見的：如果你第一次snoc然後加倍，那麼它與第一次加倍然後再次兩次相同。因此，讓我們證明這一點作爲輔助引理：

lemma double_snoc: "double (snoc xs x) = snoc (snoc (double xs) x) x" 
    by (induction xs) auto 

現在的reverse_double證明經過自動：

lemma reverse_double: "reverse (double xs) = double (reverse xs)" 
    by (induction xs) (auto simp: double_snoc)