CODEWITHSUNDEEP
isabelletheorem-proving
DianaPrince
DianaPrince

Reputation: 101

Isabelle Code Generation and Linear Order

I am trying to use the export_code tool for the following definition: 

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

This is not working due to missing code equations for Eps. Now I discovered that there is also a definition:

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

However, I am not capable of asserting that ('a ×'a) is a linear order (which would be fine for me, e.g. first comparing the first element and then the second). Can someone help me to either fix my own definition or using the existing one?

Upvotes: 1

Views: 158

Answers (1)

Peter Zeller
Peter Zeller

Reputation: 2286

To use sorted_list_of_set you can implement the type class linorder for product types:

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

You can also import "HOL-Library.Product_Lexorder" from the standard library, which includes a similar definition.

Then you can define set_to_list if you restrict the type parameter to implement linorder: 

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

Upvotes: 2

Related Questions