Email Gateway (Aug 19 2022 at 12:55): Email Gateway (Aug 19 2022 at 12:55):From: Yannick <yannick_duchene@yahoo.fr>
On Mon, 09 Dec 2013 10:44:27 +0100, Andreas Lochbihler
<andreas.lochbihler@inf.ethz.ch> wrote:
Hi Yannik,
What is a destructor? Isn't it pattern matching?
A destructor (or more precisely, a selector) is a function that returns
one of the arguments of a constructor. For example, hd and tl are the
selectors for list, they return the arguments of a Cons.The new datatype package (keyword datatype_new) generates such
discriminators and selectors, the old one (keyword datatype) does not.
In Isabelle2013-1, the datatypes in HOL are generated by the old
datatype package. To use the new datatype package, you must import
~~/src/HOL/BNF/BNF. But of course, you can always define your own
discriminators and selectors.
So I will try this one.
lemma "isα t ⟹ t = α a" sorry -- No way too
This is not provable, you probably want to have "isα t ⟹ EX a. t = α a".
Try by(cases t)(auto simp add: isα_def)
Yes, that was the intent. I though this was the same as to say there exist
an “a” such that “t = α a”. Or else, this just mean nothing, unless “a” is
fixed and in which case this is indeed not provable. Is “a” implicitly
fixed in the proposition I tested? If so, I didn't suspected it, and will
be aware of it since now.
Thanks for the precious comments :)
Email Gateway (Aug 19 2022 at 12:55):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Yannik,
Yes, fresh variables in theorem statements are implicitly fixed. You can also specify
variables that you can instantiate later, as in
schematic_lemma "isα t ==> t = α ?a"
but this does not work well with Isar proofs, parallelisation of proof checking, and (in
this case) proof automation. So it's better to explicitly use an existential quantifier here.
Best,
Andreas
Email Gateway (Aug 19 2022 at 12:55):From: Yannick <yannick_duchene@yahoo.fr>
I missed it (as it was not my first time in “datatypes.pdf”, I missed this
change in the introduction). Also HOL-BNF can be selected as the default
image in jEdit.
Now there are theorems “t.discI(n)” which indeed do what's needed. The
functions “t.is_Cn” do the same as explicitly defined functions (in a
prior message).
Is it OK to use HOL-BNF or is it still subject to big change? What would
you recommend between “datatype” and “datatype_new”?
Email Gateway (Aug 19 2022 at 12:56):From: Yannick <yannick_duchene@yahoo.fr>
I forget to comment on this: “thm isα_def” just says “isα ≡ isα_sumC”, and
“isα_sumC” is just a constant of type “t => bool”, so it was not usable
(HOL-BNF has a really usable “is_Atom_def”).
Email Gateway (Aug 19 2022 at 12:56):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
This is what you get with the function package. In that case, isα.simps is what you need.
With definition, the theorem is usually names <constant name>_def. In your example above,
however, you renamed the definition theorem to isα, so apply(simp add: isα) should work.
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:16):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I was seeking for something like constructor predicates, I mean something
which says whether or not an instance of that data‑type is from a
particular constructor of a that data‑type.
In “datatypes.pdf”, in “2.3 Generated Constants” there is the mention of
discriminators of the form “t.is_Cn” where “Cn” is the name of a
constructor of the type “t”.
I could not find anything like this in the theory context, so searched the
web for “Isabelle HOL is_Cons is_Nil” with the hope this could pop up some
examples on the topic. I could just find this, which did not help to
understand:
http://isabelle.in.tum.de/repos/isabelle/file/3d520eec2746/src/HOL/Codatatype/Tools/bnf_wrap.ML
For the practical issue, I encountered a case where I needed but failed to
prove this: “a ≠ ω b ⟹ a ≠ ω (c # d)”. I can't prove it, as “a” is not
produced by “ω” there is no “b” and no way to compare the latter to “(c #
d)”. The case seemed a bit paradoxical to me, when I started to think I
finally need something to say “a” is not produced by the constructor “ω”.
Also I noticed “datatypes.pdf” talks about “datatype_new” and some others,
which seems not to be recognized. Is this an error or something old or
something new to come?
Email Gateway (Aug 19 2022 at 13:17):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I fell back to this:
datatype "term" =
Any ("ε")
| Atom atom ("α")
| Variable variable ("υ")
| Compound "term list" ("ω")
;
primrec isυ :: "term ⇒ bool" where
"isυ ε = False"
| "isυ (α _) = False"
| "isυ (υ _) = True"
| "isυ (ω _) = False"
(* And so on for the other three constructors… *)
“isυ” is what is supposed to be “term.is_Variable” after “datatypes.pdf”,
but which does not seems to be there.
The simplifier seems to be able to deal with this in proof.
I noticed something I don't understand. Isabelle/jEdit tells me in the
output pan and about the primrec: “No function definition for datatype
"List.list"”.
Email Gateway (Aug 19 2022 at 13:17):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s actually quite rare to need destructor or discriminator functions in datatypes. You should use pattern-matching instead, or the built-in case expression. With the latter, you can also get the simplifier to perform rewriting with case-splitting automatically.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:17):From: Yannick <yannick_duchene@yahoo.fr>
On Sun, 08 Dec 2013 15:24:49 +0100, Lawrence Paulson <lp15@cam.ac.uk>
wrote:
It’s actually quite rare to need destructor or discriminator functions
in datatypes.
What is a destructor? Isn't it pattern matching?
I guess too it may be perhaps quite rare, but it's unavoidable for my
actual practical case. Using pattern matching in propositions is not
always OK, as it can lead to paradoxical cases where its needed to prove a
relation between things which don't exist. That's why I need a predicates
which really says “t is as this” or “t is not as this”.
You should use pattern-matching instead, or the built-in case
expression. With the latter, you can also get the simplifier to perform
rewriting with case-splitting automatically.
I tried with a definition and a function:
definition isα: "isα t ≡ (case t of α a ⇒ True | _ ⇒ False)"
lemma "t = α a ⟹ isα t" sorry -- No way, and unfolding does not help
lemma "isα t ⟹ t = α a" sorry -- No way too
Or:
fun isα where "isα t = (case t of α a ⇒ True | _ ⇒ False)"
lemma "t = α a ⟹ isα t" sorry -- OK
lemma "isα t ⟹ t = α a" by simp -- But no way with this one
None seems to work as expectable and even “try” fails to find a solution.
Email Gateway (Aug 19 2022 at 13:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Yannik,
What is a destructor? Isn't it pattern matching?
A destructor (or more precisely, a selector) is a function that returns one of the
arguments of a constructor. For example, hd and tl are the selectors for list, they return
the arguments of a Cons.
The new datatype package (keyword datatype_new) generates such discriminators and
selectors, the old one (keyword datatype) does not. In Isabelle2013-1, the datatypes in
HOL are generated by the old datatype package. To use the new datatype package, you must
import ~~/src/HOL/BNF/BNF. But of course, you can always define your own discriminators
and selectors.
I tried with a definition and a function:
definition isα: "isα t ≡ (case t of α a ⇒ True | _ ⇒ False)"
lemma "t = α a ⟹ isα t" sorry -- No way, and unfolding does not help
Have you tried apply(simp add: isα_def)? It should do the job.
lemma "isα t ⟹ t = α a" sorry -- No way too
This is not provable, you probably want to have "isα t ⟹ EX a. t = α a".
Try by(cases t)(auto simp add: isα_def)
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 13:17):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Yannick,
Also I noticed “datatypes.pdf” talks about “datatype_new” and some others, which seems not to be recognized. Is this an error or something old or something new to come?
The answer is in the introduction of that document (p. 4):
To use the package, it is necessary to import the BNF theory, which can be precompiled into the HOL-BNF image. The following commands show how to launch jEdit/PIDE with the image loaded and how to build the image without launching jEdit:
isabelle jedit -l HOL-BNF
isabelle build -b HOL-BNF
Regards,
Jasmin
Last updated: Apr 19 2024 at 08:19 UTC