Stream: Beginner Questions

Topic: ML in an Isabelle theory

Sana I. (Mar 21 2025 at 04:08):

I want to define a large set of structured values in my theory file. The size of the set can be quite large (in the thousands), so I would like to avoid copying or writing all of them directly into the .thy file to keep it clean and readable. I am trying to get these values automatically generated in a separate .ML file. The values themselves are nested sets of tagged elements, something like: { {⟪label1, value1⟫, ⟪label2, value2⟫, ...}, {...}, ... }

Ideally, I want to define something like:

definition generatorSet :: ___ where
  "generatorSet = ..."  (* value generated by ML *)

I'm currently generating the values programmatically in an .ML file and including it in the theory using:
ML_file "generate_set.ML"

I am not sure if this is the correct approach.

Is it possible to define the value of generatorSet entirely within the ML file, and have it behave like a regular constant that I can use throughout the theory later that can be used in proofs and other definitions?

Or is the recommended approach to pre-generate a portion of the .thy file using ML before loading the theory?

Any advice or code examples on how to bridge the ML and logic layers in Isabelle when working with large, structured, automatically-generated values would be great. Thank you.

Last updated: Apr 18 2025 at 20:21 UTC