如何生成反向排序代码

Question

生成排序算法的代码的最简单方法是什么？在现有的List.sort之上构建排序算法时，它的排序顺序是相反的？

我想出了两个解决方案，下面显示在我的答案。但他们都不是很满意。

任何其他的想法如何做到这一点？

Answer 1

我想出了两种可能的解决方案。但都有（严重的）缺点。 （我希望几乎可以自动获得结果。）

1. 引入Haskell样式的newtype。例如，如果我们想的nat S，列出的东西像

   datatype 'a new = New (old : 'a) 
   
   instantiation new :: (linorder) linorder 
   begin 
   
   definition "less_eq_new x y ⟷ old x ≥ old y" 
   definition "less_new x y ⟷ old x > old y" 
   
   instance by (default, case_tac [!] x) (auto simp: less_eq_new_def less_new_def) 
   
   end 
   

   排序此时

   value [code] "sort_key New [0::nat, 1, 0, 0, 1, 2]" 
   

   产生期望的反向排序。虽然这相对比较容易，但它并不像我希望解决方案那样自动化，并且运行时间很小（因为Isabelle没有Haskell的newtype）。

2. 通过线性顺序对偶的语言环境。首先，我们或多或少地复制现有的插入排序代码（但不是依赖于一个类型类型，而是使显式比较的参数）。

   fun insort_by_key :: "('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'a list ⇒ 'a list" 
   where 
       "insort_by_key P f x [] = [x]" 
   | "insort_by_key P f x (y # ys) = 
       (if P (f x) (f y) then x # y # ys else y # insort_by_key P f x ys)" 
   
   definition "revsort_key f xs = foldr (insort_by_key (op ≥) f) xs []" 
   

   此时我们的代码为revsort_key。

   value [code] "revsort_key id [0::nat, 1, 0, 0, 1, 2]" 
   

   但我们也希望所有已经在linorder场所证明了很好的结果（从linorder类派生）。为此，我们引入线性顺序的对偶，并使用“mixin”（不确定是否使用了正确的命名）来替换所有出现的linorder.sort_key（不允许代码生成）我们新的“代码常数“revsort_key。

   interpretation dual_linorder!: linorder "op ≥ :: 'a::linorder ⇒ 'a ⇒ bool" "op >" 
   where 
       "linorder.sort_key (op ≥ :: 'a ⇒ 'a ⇒ bool) f xs = revsort_key f xs" 
   proof - 
       show "class.linorder (op ≥ :: 'a ⇒ 'a ⇒ bool) (op >)" by (rule dual_linorder) 
       then interpret rev_order: linorder "op ≥ :: 'a ⇒ 'a ⇒ bool" "op >" . 
       have "rev_order.insort_key f = insort_by_key (op ≥) f" 
       by (intro ext) (induct_tac xa; simp) 
       then show "rev_order.sort_key f xs = revsort_key f xs" 
       by (simp add: rev_order.sort_key_def revsort_key_def) 
   qed 
   

   虽然这个解决方案，我们没有任何运行时间延长，这是迄今为止对我的口味和太冗长不容易适应标准代码设置的变化（例如，如果我们想用对于我们所有的分类操作，从Archive of Formal Proofs合并排序实施）。