Stream: Isabelle/ML

Topic: Folding definitions


view this post on Zulip 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?

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC