Email Gateway (Aug 18 2022 at 20:27): Email Gateway (Aug 18 2022 at 20:27):From: li yongjian <lyj238@gmail.com>
Dear all:
I'm trying your tutorial material on SAT solver (page 196).
I meet a type error that I cannot solve. Could you please do me
a hand?
see line 64 in the attachment.
The error says that Isabelle cannot unify the same type .
regards!
machineLearning.thy
Email Gateway (Aug 18 2022 at 20:27):From: Christian Urban <christian.urban@kcl.ac.uk>
Hi Yongjian,
Although the reference is vague, I assume this is also about
the programming cookbook and the code in question is:
ML{*
val (pform, table) =
Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty;
SatSolver.invoke_solver "dpll" pform
*}
Note that the code in your theory differs from the above by
first including the file prop_logic.ML.
ML{*
use "/usr/local/Isabelle2011/src/HOL/Tools/prop_logic.ML";
val (pform, table) =
(Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty);
pform;
SatSolver.invoke_solver "dpll" pform;
*}
If you remove this line, your code works. I guess the problem has
something to do with redefining types in ML, which would explain
the puzzling error message.
BTW, a more robust way to reference files would be
use "~~/src/HOL/Tools/prop_logic.ML"
Hope this helps,
Christian
Last updated: May 01 2024 at 20:18 UTC