Email Gateway (Aug 19 2022 at 11:21): Email Gateway (Aug 19 2022 at 11:21):From: David Sanán <sananbad@scss.tcd.ie>
Dear Andreas and Florian,
Thanks for your valuables comment. I will follow your suggestions.
Code generation is not an actual concern. However combining the use of Tobia's index and Florian suggestion
assumes "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! ordinal x) = x"
would release the needed to prove manually the instantiation "ordinal dat0 = 0" "ordinal dat1 = 1" "ordinal dat2 = 2" ... am I right?
Before reading your last posts I had already tried to prove "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! ordinal x) = x" in a general function (not within an instantiation), but I could not (I need more experience!). I will try with instantiations then.
Thanks again and best regards,
David.
Email Gateway (Aug 19 2022 at 11:22):From: David Sanán <sananbad@scss.tcd.ie>
I reply to myself,
Just defining the class and with the assumption "ordinal = index enum_class.enum" datatype instantiations are straightforward using definitions.
Thanks and best regards,
David.
Email Gateway (Aug 19 2022 at 11:32):From: David Sanan <sananbad@scss.tcd.ie>
Dear all,
I am starting with Isabelle and I am trying something I consider a
basic thing but I can't see how to do it.
From a datatype which I have instantiated to enum, I want to get the
ordinal of an element as defined in the Enum.enum list.
So if I define
datatype my_data = dat0|
dat1|
dat2
lemma user_my_data_induct: "P dat0 <--> P dat1 ==> P dat2 ==> P x"
by (cases x) auto
lemma UNIV_my_data [no_atp]: "UNIV = { dat0, dat1, dat2}"
apply (safe)
apply (case_tac x)
apply (auto intro:user_my_data_induct)
done
instantiation my_data :: enum begin
definition "enum_my_data= [dat0, dat1, dat2]"
definition "enum_all_my_data P <--> P dat0 /\ P dat1 /\ P dat2"
definition "enum_ex_my_data P <--> P dat0 \/ P dat1 \/ P dat2"
instance proof
qed (simp_all only: enum_my_data_def enum_all_my_data_def
enum_ex_my_data_def UNIV_my_data, simp_all)
end
I want to map dat0 to 0, dat1 to 1 ...
Is there define any function for that? I have looking but I could not
find anything.
I can always create it, of course but I would like to know whether
there is something for this or not.
Thanks and best regards,
David.
Email Gateway (Aug 19 2022 at 11:32):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi David,
From what you write, I guess that you want to have an operation ordinal :: 'a :: enum =>
nat such that "ordinal x" returns the position of x in the enumeration list enum_class.enum.
I am not aware of any pre-defined setup for this use case in the Isabelle/HOL library. You
can of course define
"ordinal x =
(THE i. i < length (enum_class.enum :: 'a list) & enum_class.enum !! i = x)"
but that won't be fun to work with. The entry List_Index in the Archive of Formal Proofs
(http://afp.sourceforge.net/entries/List-Index.shtml), however, defines a function index
such that "ordinal = index enum_class.enum". That should fit your purpose.
You still have to prove the assignment manually for your instantiation, i.e.,
"ordinal dat0 = 0" "ordinal dat1 = 1" "ordinal dat2 = 2"
but this will be automatic with index.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 11:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
An alternative could be:
class index = enum +
fixes ordinal :: "'a => nat"
assumes "n < length (Enum.enum :: 'a list) ==> ordinal
(Enum.enum ! n :: 'a) = n"
assumes "n < length (Enum.enum :: 'a list) ==> (Enum.enum !
ordinal x) = x" -- {* disclaimer: not checked in Isabelle yet *}
I.e. the THE-definition of ordinal is absorbed into a constructive type
class. This leaves you still to provided reasonable instance
definitions for ordinal for each instance type, but this might turn out
simple if you have a look at the corresponding Enum.enum instances.
Practice shows which approach is more appropriate.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:33):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian and David,
If code generation is a concern, Florian is right: a separate type class with the index
operation is preferable, because then, you can tailor the code equations for ordinal to
every datatype you are using. If you use large datatypes, I expect that this will improve
the run-time considerably. However, I did not see from the original post that code
generation was intended (although the enum class mainly serves for code generation).
However, even then, I suggest to build on Tobias' AFP entry as follows:
class index = enum +
fixes ordinal :: "'a => nat"
assumes ordinal_conv_index: "ordinal = index enum_class.enum"
As ordinal is fully specified, the assumption of the type class can directly be
definitional. (You can even start working with "index enum_class.enum" directly and later
on introduce such a type class for code generation, but that leads too far here.
Best,
Andreas
Email Gateway (Aug 19 2022 at 11:44):From: David Sanán <sananbad@scss.tcd.ie>
Hi Again,
After successfully includes an "ordinal" operation for datatypes instantiating enum, I have included the reverse operation "data", which gives a datatype from an natural in case the given natural is within the datatype range. So I have extended the index class adding the new data operation fixes data :: "nat ⇒ 'a option" and the following assumption type_conv_ordinal: "data (ordinal (x)) = Some x".
The problem comes when I am instantiating some datatype to index. When proving the assumption, which apparently can be done well "by auto", well using "by (simp_all add: ordinal_conv_index data_my_data_def enum_UNIV)". For this instantiation
instantiation my_data:: index
begin
definition
"index_class.ordinal (a::my_data) ≡ index enum_class.enum a"
definition
"index_class.data (n::nat) ≡
if n < size (enum_class.enum::(my_data list))
then Some (nth enum_class.enum n)::(my_data option)
else None::(my_data option)"
instance proof
fix m::my_data
show "index_class.ordinal m = index enum_class.enum m" by (simp_all add: ordinal_my_data_def)
show "data (ordinal (m)) = Some m" by (simp_all add: ordinal_conv_index data_my_data_def enum_UNIV)
qed
end
Although the proof finishes well, the second "show" is marked with a forbid symbol and "by (simp_all add: ordinal_conv_index data_my_data_def enum_UNIV)" is red highlighted and the output shows the following:
show data (ordinal m) = Some m
Successful attempt to solve goal by exported rule:
data (ordinal ?m2) = Some ?m2
proof (state): step 6
this:
data (ordinal m) = Some m
goal:
No subgoals!
Failed to finish proof:
goal (1 subgoal):
data (ordinal m) = Some m
why is this happening?
The whole index class and the instantiation are below.
Thanks and best regards,
David.
class index = enum +
fixes ordinal :: "'a ⇒ nat"
fixes data :: "nat ⇒ 'a option"
assumes ordinal_conv_index: "ordinal m = index enum_class.enum m"
and type_conv_ordinal: "data (ordinal (x)) = Some x"
end
datatype my_data = dat0
|dat1
|dat2
lemma my_data_induct: "P dat0 ⟹ P dat1 ⟹ P dat2 ⟹ P x"
by (cases x) auto
lemma UNIV_my_data [no_atp]: "UNIV = { dat0,dat1,dat2}"
apply (safe)
apply (case_tac x)
apply (auto intro:my_data_induct)
done
instantiation my_data :: enum begin
definition "enum_my_data = [dat0,dat1,dat2]"
definition "enum_all_my_data P ⟷ P dat0 ∧ P dat1 ∧ P dat2"
definition "enum_ex_my_data P ⟷ P dat0 ∨ P dat1 ∨ P dat2 "
instance proof
qed (simp_all only: enum_my_data_def enum_all_my_data_def enum_ex_my_data_def UNIV_my_data, simp_all)
end
instantiation my_data:: index
begin
definition
"index_class.ordinal (a::my_data) ≡ index enum_class.enum a"
definition
"index_class.data (n::nat) ≡
if n < size (enum_class.enum::(my_data list))
then Some (nth enum_class.enum n)::(my_data option)
else None::(my_data option)"
instance proof
fix m::my_data
show "index_class.ordinal m = index enum_class.enum m" by (simp_all add: ordinal_my_data_def)
show "data (ordinal (m)) = Some m" by auto
qed
end
Email Gateway (Aug 19 2022 at 11:44):From: David Sanán <sananbad@scss.tcd.ie>
I partially answer myself...
The proof was not already done (or was it?)although it said there was not any subgoals left and there was no error in the end of the instance proof... Instead of using "by" I have used "apply" and now the proof steps look clearer to me.
Finally I have solved it just adding another definition to the simplification method and the final proof is:
instance proof
fix m::my_data
show "index_class.ordinal m = index enum_class.enum m" by (simp_all add: ordinal_my_data_def)
show "data (ordinal (m)) = Some m" by (simp_all add: data_my_data_def ordinal_my_data_def enum_UNIV)
qed
end
However, shouldn't the whole instance proof be marked as incomplete (that is the end of the proof should not be clear) in my first attempt?
Also If I remove the definition "data_my_data_def" from the simplification I have:
Successful attempt to solve goal by exported rule:
data (ordinal ?m2) = Some ?m2
Failed to finish proof:
goal (1 subgoal):
data (ordinal m) = Some m
this:
data (ordinal m) = Some m
goal:
No subgoals!
Does it means that the proof is done??? It seems so to me, but when I try to build the model I have:
Failed to finish proof (line 210 of "List-Index/List_Index.thy"):
*** goal (1 subgoal):
*** data (ordinal m) = Some m
*** 1. data (index enum_class.enum m) = Some m
*** At command "by" (line 210 of "List-Index/List_Index.thy")
Thanks and regards,
David.
Last updated: Apr 24 2024 at 20:16 UTC