I'm very new to Isabelle and am trying to implement a datatype such as
datatype fruit = Apple | Banana| Cantaloupe
(word choices are inane here to not confuse it with trying to do anything else)
However, its important to note that Apple ≤ Banana ≤ Cantaloupe.
What would be the best way to implement in Isabelle? Would a datatype be appropriate?
Bonus question: How could you instantiate a variable to be one of those 3 options?
About your main question.
I'm assuming that you want to specify an ordering by hand, i.e., you want to spell out all cases. If you're happy with standard lexicographic order, there's an AFP entry which is capable of doing that automatically.
Yes, the proper way of implementing what you want is by starting with a datatype. Then, you will need to define the ≤ operator. For that, you need to instantiate a class. The first two sections on in the documentation of type classes will give you an idea how that works. For your example, it'd look something like this:
instantiation fruit :: linorder begin
fun less_fruit where
"Apple < Apple ⟷ False" |
"Apple < _ ⟷ True" |
"Banana < Apple ⟷ False" |
"Banana < Banana ⟷ False" |
"Banana < _ ⟷ True" |
"Cantaloupe < _ ⟷ False"
definition less_eq_fruit :: "fruit ⇒ fruit ⇒ bool" where
[simp]: "less_eq_fruit x y ⟷ x = y ∨ x < y"
instance sorry
end
Finally, you will have to carry out the instance proof, that is: you need to show that the operators you defined indeed form a linear order. In the above example I cheated using the sorry command.
The way to do it properly directly leads to your bonus question.
You can instantiate the variables by using the cases tactic. See it in action for the instance proof:
instance proof
fix x y :: fruit
show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
by (cases x; cases y; simp)
next
(* more stuff to prove here *)
qed
The cases method takes a variable name and will split the current goal into multiple cases (here: three). The ; (sequential composition) operator will apply the first method and apply the second method on all new subgoals. Finally, everything can be solved with simp.