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?
My solution for now is to just apply Local_Defs.fold
until a fixpoint is reached.
Last updated: Dec 30 2024 at 16:22 UTC