Jason Hu (Aug 29 2022 at 19:13): Jason Hu (Aug 29 2022 at 19:13):Hi, I noticed that the Isabelle tutorial is a bit out of date. There are examples stop working with the latest Isabelle version. For example, it seems the book heavily relies on typ_pat and term_pat, but it no longer compiles. Is that possible to update the book? Also, given how useful typ_pat and term_pat seem to be, is that possible just provide them in Isabelle?
Kevin Kappelmann (Aug 30 2022 at 06:12):HI Jason, I assume you are referring to Christian Urban's cookbook. As written on its website, there's a repository and you are invited to contribute. You may write Christian an email and ask him whether he likes your suggestions and how you should send him your proposed changeset.
Kevin Kappelmann (Aug 30 2022 at 06:18):About the pattern antiquotations: I think this has been proposed multiple times but Makarius (the main kernel maintainer) does not seem quite keen to include them. See, for example, this mail thread: https://isabelle.zulipchat.com/#narrow/stream/247542-Mirror.3A-Isabelle-Development-Mailing-List/topic/.5Bisabelle-dev.5D.20NEWS.3A.20ML.20antiquotations.20for.20type.20construct.2E.2E.2E
Jason Hu (Aug 30 2022 at 13:56):thx. I am reading the book and I am not able to follow the examples because essentially the book itself is a library on its own. is there a modern and recommended way to look into how to write isabelle/ML programs?
Kevin Kappelmann (Aug 30 2022 at 14:26):I think the cookbook + the implementation manual are the best sources available.
I do not understand what you mean with "the book itself is a library on its own"...?
Jason Hu (Aug 30 2022 at 15:26):because the cookbook implements a bunch of functions and anti-quotes that are not available as they are in the latest isabelle, nor do they run after copy and paste into the Isabelle buffer. I open up the source code of the book and they still won't run. as a result, the later sections cannot be understood at all if code in the earlier sections breaks for some reason. for example, the unification section depends on @typ_pat and @term_pat but I have no idea how to make those things work.
Jan van Brügge (Aug 30 2022 at 18:11):Yeah, the implementation manual is probably your best starting point and then you can ask questions here. In the next year I will write a tutorial paper about Isabelle/ML to do axiomatizations, tactics and so on.
Kevin Kappelmann (Aug 31 2022 at 05:52):Jason Hu said:
because the cookbook implements a bunch of functions and anti-quotes that are not available as they are in the latest isabelle, nor do they run after copy and paste into the Isabelle buffer. I open up the source code of the book and they still won't run. as a result, the later sections cannot be understood at all if code in the earlier sections breaks for some reason. for example, the unification section depends on
@typ_patand@term_patbut I have no idea how to make those things work.
I suggest that you simply download the latest version compatible with the cookbook and study it this way. Currently, this is Isabelle 2019, available here: https://isabelle.in.tum.de/download_past.html
Though some internal function names and signatures may have changed, the overall philosophy and approach when developing Isabelle/ML code stayed the same.
Jason Hu (Sep 01 2022 at 20:03):maybe I should be more specific about what I am trying to do: is there any (simple) example for looping assumptions and named theorems and then manipulating the goal?
Jan van Brügge (Sep 01 2022 at 21:34):what do you mean with looping assumption? changing their order?
Jason Hu (Sep 02 2022 at 01:27):looking through the assumptions and do something with it, like fold maybe?
Jan van Brügge (Sep 02 2022 at 08:33):You can use Subgoal.FOCUS (fn {context=ctxt, prems, ...} => (* code here *)) @{context}. Then you get all assumptions in prems. Again without some concrete goal it is hard what would be best
Last updated: Apr 23 2024 at 12:29 UTC