Генерация кода Изабель и линейный порядок - PullRequest
Новая
       57

Генерация кода Изабель и линейный порядок

1 голос
/ 04 марта 2020

Я пытаюсь использовать инструмент export_code для следующего определения: 

definition set_to_list :: "('a×'a) set ⇒ ('a×'a) list"
  where "set_to_list A = (SOME L. set L = A)"

Это не работает из-за отсутствия кодовых уравнений для Eps. Теперь я обнаружил, что есть также определение: 

definition sorted_list_of_set :: "'a set ⇒ 'a list" where
  "sorted_list_of_set = folding.F insort []"

Однако я не могу утверждать, что ('a ×' a) является линейным порядком (что было бы хорошо для меня, например, первое сравнение первый элемент, а затем второй). Может ли кто-нибудь помочь мне исправить собственное определение или использовать существующее?

1 Ответ

2 голосов
/ 04 марта 2020

Чтобы использовать sorted_list_of_set, вы можете реализовать класс типов linorder для типов продуктов: 

instantiation prod :: (linorder,linorder) linorder begin
definition "less_eq_prod ≡ λ(x1,x2) (y1,y2). x1<y1 ∨ x1=y1 ∧ x2≤y2"
definition "less_prod ≡ λ(x1,x2) (y1,y2). x1<y1 ∨ x1=y1 ∧ x2<y2"
instance by standard (auto simp add: less_eq_prod_def less_prod_def) 
end

Вы также можете импортировать "HOL-Library.Product_Lexorder" из стандартной библиотеки, которая включает аналогичное определение.

Тогда вы можете определить set_to_list, если вы ограничите параметр типа для реализации linorder: 

definition set_to_list :: "('a::linorder×'a) set ⇒ ('a×'a) list"
  where "set_to_list A = sorted_list_of_set A"
...