Email Gateway (Mar 02 2025 at 10:36): Email Gateway (Mar 02 2025 at 10:36):From: Oleksandr Gavenko <gavenkoa@gmail.com>
I'm translating Prover9 proof into Isabelle and I find it difficult to
work with gigantic nesting expressions.
To troubleshoot I'd like to have debugging tools:
=======
Substitution printing is partially archivable via syntax:
thm THM[where a=...]
thm THM[of _ a _ "(b+c)"]
But I'd like to write just something simple as:
thm "a~e=e~a"[of "x+1" "z-1"]
to see the result of substitution.
I can define a temporary failed thm as a workaround:
lemma x: "(((A ~ B) ~ C ~ B) ~ C ~ A)"
sorry
thm x[of "A~A" _ "(B~A)~A"]
I tried something less invasive:
notepad begin
have x: "(((A ~ B) ~ C ~ B) ~ C ~ A)"
sorry
thm x
end
but variables of the fact are not "placeholders", so substitution
results in an error:
thm x[of a]
More instantiations than variables in theorem
===============
I defined some syntax in a theory and want Isabelle to find MGU for an
expression to match against the existing theorem.
For:
op(520, infix_right, "~").
formulas(assumptions).
% Rule Detachment.
prop(P) & prop(P~Q) -> prop(Q) #label(detachment).
% Axioms
prop((X~Y) ~ (Y~Z) ~ (X~Z)) #label(tran).
prop((X~Y) ~ (Y~X)) #label(sym).
end_of_list.
formulas(goals).
prop(X~(X~Y)~Y).
end_of_list.
Prover9 tells me:
1 prop(A) & prop(A ~ B) -> prop(B) # label(detachment) #
label(non_clause). [assumption].
2 prop(A ~ (A ~ B) ~ B) # label(non_clause) # label(goal). [goal].
3 -prop(A) | -prop(A ~ B) | prop(B) # label(detachment). [clausify(1)].
4 prop((A ~ B) ~ (B ~ C) ~ A ~ C) # label(tran). [assumption].
5 prop((A ~ B) ~ B ~ A) # label(sym). [assumption].
6 -prop(c1 ~ (c1 ~ c2) ~ c2). [deny(2)].
8 prop(((A ~ B) ~ C ~ B) ~ C ~ A). [hyper(3,a,4,a,b,5,a)].
15 prop(A ~ (A ~ B) ~ B). [hyper(3,a,8,a,b,8,a)].
16 $F. [resolve(15,a,6,a)].
and I have a hard time understanding how hyperresolution happened at
line 15 (rule 3 applied on some instances of 8 2 times).
hyperresolution is like Modus Ponens with unification and I'd like
to debug unifications of some expressions against some facts.
I have no problems dealing with inline ML code, but Isabelle Cookbook
is gibberish for my level of knowledge of Isabelle - I cant find
functions I can call for printing substitution & unification.
Last updated: Mar 09 2025 at 12:28 UTC