Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error in simproc

Email Gateway (Aug 18 2022 at 10:15):

From: Tom Ridge <tjr22@cam.ac.uk>
Dear All,

I keep getting errors resembling the following when trying to invoke simp.

*** Error in simproc "let_simp":
*** Error in simproc "split_beta":
*** Proof failed.
*** (l(turn', trys').
*** let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts,
Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
*** ((turn', trys'), bool_case :084 pc'))
*** (Rsharedf (:081, :082)) =
*** (let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts,
Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
*** (Rsharedf (:081, :082), bool_case :084 pc'))
*** 1. (l(turn', trys').
*** let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts,
Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
*** ((turn', trys'), bool_case :084 pc'))
*** (Rsharedf (:081, :082)) =
*** (let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts,
Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
*** (Rsharedf (:081, :082), bool_case :084 pc'))
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** (l(turn', trys').
*** let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts,
Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
*** ((turn', trys'), bool_case :084 pc'))
*** (Rsharedf (:081, :082)) =
*** (let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts,
Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
*** (Rsharedf (:081, :082), bool_case :084 pc'))
*** At command "apply".

Does anyone know what is going on?

Thanks

Tom

Email Gateway (Aug 18 2022 at 10:16):

From: Norbert Schirmer <schirmer@informatik.tu-muenchen.de>
Hi Tom,

to find out if the error really stems from the simplification-
procedure for let you
can disable the let-simproc by:

ML "use_let_simproc := false"

If the let-simproc is to blame, it would be nice if you could send me
an example that causes the problem, so that
I can track it down.

Norbert

Last updated: May 03 2024 at 08:18 UTC