Email Gateway (Aug 18 2022 at 09:36): Email Gateway (Aug 18 2022 at 09:36):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
I proved to use the examples about the integration between Isabelle and
Mucke.
I have installed Isabelle 2005 and Mucke 0.4.4.
Isabelle analyse theory MuckeExample1 (in HOL/Modelcheck) but when it
reaches lemma "reach_ex1" and in particular the application of the second
tactic it stops with the follow error:
*** exception THM raised: instantiate: type conflict
*** ?a::bool × bool × bool => bool :: bool × bool × bool => bool
*** ?a1::?'a :: ?'a
*** At command "apply".
While when it reaches the second lemma "reach_ex" it stops with the error:
*** Inner lexical error at: "INIT == % x . ¬ fst (x::bool × bool × bool) AND
¬ fst (snd x) AND ¬ snd (snd x)"
*** The error(s) above occurred for "INIT == % x . ¬ fst (x::bool × bool ×
bool) AND ¬ fst (snd x) AND ¬ snd (snd x)"
*** At command "by".
Can anyone help me?
Thanks in advance for the collaboration.
Gabriele
Email Gateway (Aug 18 2022 at 09:36):From: Makarius <makarius@sketis.net>
Unfortunately, the Mucke interface has not been used for a long time.
These files are essentially the leftover of some experiments with Mucke
0.3.5 -- according to the README. Both Isabelle and Mucke may well have
changed to make this kind of oracle code break down.
Makarius
Last updated: May 03 2024 at 04:19 UTC