Email Gateway (Aug 18 2022 at 14:51): Email Gateway (Aug 18 2022 at 14:51):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I have the following class definition:
class well_founded_transitive = ord +
assumes order_trans1: "x < y ==> y < z ==> y < z"
and less_eq_def: "x <= y =( x = y \/ x < y)"
and less_induct1 [case_names less]: "(!!x . (!!y . y < x ==> y) ==>
x) ==> a"
begin
definition
"Sup_less P w = SUPR {v . v < w} P";
end
and I have the following definition
definition
"Sup_less2 pair X (u::'a::well_founded_transitive) i = SUPR {v . pair
v i < u} (% v . X v i)";
However, what I am interested in is something like:
definition
"Sup_less2 X u i = SUPR {v . (v, i) < u} (% v . X v i)";
However, with the second definition I get the error message:
*** Type unification failed: No type arity * :: ord
*** Type error in application: Incompatible operand type
*** Operator: op < :: ??'a × ??'b => ??'a × ??'b => bool
*** Operand: (v, i) :: ??'a × ??'b
*** At command "definition".
Is there a way to achieve the second kind of definition for Sup_less2?
I need the order to be over pairs, however, I must have an un-instantiated
order relation.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 14:52):From: Brian Huffman <brianh@cs.pdx.edu>
The problem is that Isabelle doesn't know what you mean by "(v, i) <
u", since the comparison operators have not been defined for pairs.
(That's what "No type arity * :: ord" is supposed to tell you.)
There are two ways to solve this problem:
instantiation "*" :: (ord, ord) ord
begin
definition "a < b = fst a < fst b | (fst a = fst b & snd a < snd b)"
instance ..
end
The above definition is the lexicographic ordering, but other
definitions are certainly possible. You could also define less-than
pointwise:
instantiation "*" :: (ord, ord) ord
begin
definition "a < b = fst a < fst b & snd a < snd b"
instance ..
end
The drawback is that once you give a type class instance, you are
stuck with it: You must use the same definition of less-than for pairs
throughout the remainder of your theory.
definition
"Sup_less2 X u i = SUPR {v . v < fst u | (v = fst u & i < snd u)} (%
v . X v i)";
On the other hand, if you want a point-wise less-than ordering, you
would use this definition:
definition
"Sup_less2 X u i = SUPR {v . v < fst u & i < snd u} (% v . X v i)";
Hope this helps,
Email Gateway (Aug 18 2022 at 14:52):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian,
Thank you for your answer. Unfortunately both of the approaches
you suggested require defining the order in terms of possible orders on
the components, and this is something I don't want. I need to
have an un-interpreted order on pairs, and later I need to
instantiate it differently for different examples. The first definition
I used
Sup_less2 pair X u i = SUPR {v . pair v i < u} (% v . X v i)
could give me what I need. In examples I can instantiate both
the order and the function pair. However this approach,
using classes, does not bring any advantage because
everything becomes simpler if I use directly the order as a
parameter:
Sup_less2 lesspairs X u i = SUPR {v . lesspairs (v, i) u} (% v . X v i)
I have also tried to have the function pair defined by the class,
but then it was not possible to be of the type:
pair:: 'b * 'c => 'a.
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 14:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
something like
class pair_ord =
fixes pair_less_eq :: "'a * 'b => 'a * 'b => bool"
assumes ...
is indeed beyond the rather restricted Isabelle polymorphism.
Perhaps a possible solution is to formulate this order as locale and
develope your specfication relative to this:
locale pair_ord =
fixes pair_less_eq :: "'a * 'b => 'a * 'b => bool"
assumes ...
begin
definition ...
lemma ...
primrec ...
...
end
This could then be interpreted on different pair order predicates:
definition pair_less_eq_nat_int :: "nat * int => nat * int => bool"
where ...
definition pair_less_eq_list_unit :: 'a list * unit => 'a list * unit =>
bool" where ...
interpretation pair_ord_nat_int: pair_ord pair_less_eq_nat_int ...
interpretation pair_ord_list_unit: pair_ord pair_less_eq_list_unit ...
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:53):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Florian,
Thank you for your answer. In my development I need the order
on 'a types as well as on pairs 'a * 'b, and I have a general
result using a order on 'a which is instantiated later to a order on pairs.
I think that I have finally reached a conclusion which is flexible enough,
and also sound.
I will define the class of well founded and transitive relations
class well_founded_transitive = ord +
assumes order_trans1: "x < y /\ y < z ==> x < z"
...
begin...end
I will also declare an uninterpreted constant
consts
pair:: "'a => 'b => 'c::well_founded_transitive"
and I will prove all results based on these facts
Later for concrete examples I instantiate both the
class for pairs, as well as I define the pair
using an axiom:
instantiation "*":: (well_founded_transitive, well_founded_transitive)
well_founded_transitive
begin ...end
axioms pair_def: "pair a b = (a, b)";
I have tested this approach and it seems to work. I also
think that I am not introducing inconsistencies, because
I only introduce this axiom once after I instantiate
the class for pairs.
Viorel
Florian Haftmann wrote:
Email Gateway (Aug 18 2022 at 14:54):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
Yes, since your axiom is nothing else than a definition -- a copy of
Pair :: 'a => 'b => 'a * 'b, essentially. In that case you should use
the "overloading" target (see §5.7. of the Isabelle reference manual).
Hope this helps
Florian
signature.asc
Last updated: Apr 26 2024 at 04:17 UTC