James Hanson (Feb 07 2024 at 16:49): James Hanson (Feb 07 2024 at 16:49):I'm trying to formalize some basic results about Henkin-Tarski-Monk cylindric algebras in Isabelle/HOL for practice. When I try to run sledgehammer in this following context (with cvc4 verit z3 e spass vampire zipperposition as the list of provers), it says Unknown ATP: agsyhol. This is in Isabelle2023 on Linux.
theory Cylindric_Algebras
imports HOL.Nat HOL.Boolean_Algebras
begin
locale cylindric_algebra = boolean_algebra +
fixes cyl :: "nat ⇒ 'a ⇒ 'a" and
diag :: "nat ⇒ nat ⇒ 'a"
assumes Cyl_ax_0: "cyl b zero = zero" and
Cyl_ax_1: "x ≤ (cyl a x)" and
Cyl_ax_2: "cyl a (x ⊓ (cyl a y)) = (cyl a x) ⊓ (cyl a y)" and
Cyl_ax_3: "cyl a (cyl b x) = cyl b (cyl a x)" and
Cyl_ax_4: "diag a a = one" and
Cyl_ax_5: "a ≠ b ⟶ b ≠ c ⟶ diag a c = cyl b ((diag a b) ⊓ (diag b c))" and
Cyl_ax_6: "a ≠ b ⟶ (cyl a ((diag a b) ⊓ x)) ⊓ (cyl a ((diag a b) ⊓ (-x))) = zero"
begin
theorem thm_1_2_1: "cyl a x = zero ⟶ x = zero"
proof
I tried varying the list of provers and nothing changed. I'm guessing that somehow one of the imported libraries is making sledgehammer look for agsyhol, which seems to be no longer included with Isabelle, but what is actually going on?
Mathias Fleury (Feb 07 2024 at 16:52):In general: do not import anything starting with HOL.. Import Main instead
Mathias Fleury (Feb 07 2024 at 16:53):I think that this will solve your issue
James Hanson (Feb 07 2024 at 17:20):@Mathias Fleury Thank you. If it's appropriate I have a minor followup question. Why can't I use any of the defined notation from the Boolean algebras library? It's not accepting ⊓ for instance.
Christian Pardillo Laursen (Feb 07 2024 at 21:53):You probably need to be proving a lemma in the abstract_boolean_algebra context before you can get access to the notation it defines
Christian Pardillo Laursen (Feb 07 2024 at 21:57):Although if you're talking about ⊓ for lattices, then unbundle lattice_syntax should work
Last updated: Apr 28 2024 at 16:17 UTC