0

I know this might be rather out there question but I was curious if it was possible to automatically generate an Isar script given an Isabelle script. My guess is that it should be possible but the problem would be ill-posed as there might be many possible Isar scripts given a tactic script.

My guess of an approach would be something like this:

  1. execute the Isabelle tactic script (to reveal many intermediate statements)
  2. select with some heuristic H (maybe based on human proofs) of which sub-trees of the proof tree to close with have lemma_sub_tree_i using L1, L2, L3, ..., Ln by SomeProof (perhaps the by ... has more Isar scripts we automatically generated, so this function is recursive)
  3. Verify the new Isar script is valid i.e. output the new Isar script if the statement is the same as the original Isabelle tactic proof and the proof goes through/type checks/validates.

Is this possible? At the very least - is it possible in principle with some (hopefully sensible heuristic H. (Of course I know that step 2 is rather important and hoping there is a heuristic that I could truly use in practice to make an actual implementation of this).

Related:

4

0 回答 0