Stream: Isabelle/ML

Topic: Folding definitions

Lukas Stevens (Mar 27 2023 at 11:28):

I am trying to fold some definitions with Local_Defs.fold. The problem is that the folding stops before a fixpoint is reached. Here is an example:

definition "C ≡ True"
definition "A ≡ False ∧ C"

ML ‹
  Thm.cterm_of @{context} @{term ‹False ∧ True›}
  |> Thm.reflexive
  |> Local_Defs.fold @{context} @{thms A_def C_def}
›

The resulting theorem is False ∧ C ≡ False ∧ C but it should be A ≡ A. Any ideas what I could do?

Lukas Stevens (Mar 27 2023 at 12:00):

My solution for now is to just apply Local_Defs.fold until a fixpoint is reached.

Last updated: Nov 16 2025 at 20:22 UTC