Stream: New Members & Projects

Topic: automatic isabelle -> Isar conversion


view this post on Zulip Brando Miranda (Dec 16 2021 at 16:53):

I was curious to know if there was a way to automatically convert Isabelle tactic script to Isar declarative scripts (I know there is no dichotomy but just to phrase the question). Mainly, because I was curious to see if the procedure would teach me anything to do something similar for Coq (to generate IsarCoq lol but that's besides the point, I am genuinly curious about how generate nice Isar like scripts in general and apply it somewhere later). Ideally, it would be nice with a little machine learning if possible. If it does require machine learning then perhaps ideally not deep learning at first (to do such conversions).

Reference: https://www.reddit.com/r/isabelle/comments/rh0mh7/is_there_an_automatic_way_to_generate_isar/ and https://stackoverflow.com/questions/70352908/is-there-an-automatic-way-to-generate-isar-scripts-given-a-correct-isabelle-tact


Last updated: Jul 15 2022 at 23:21 UTC