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.
Email Gateway (Mar 13 2025 at 09:34):From: Lukas Bartl <lukas.bartl@uni-a.de>
Hi Oleksandr,
but variables of the fact are not "placeholders"
If you add "for A B C" after the proposition, they become placeholders
(called "schematic variables" in Isabelle).
An easy way to do substitution printing might be to use "let":
notepad
begin
let ?a = "x+1"
let ?e = "z-1"
term "?a ~ ?e"
end
It can also do higher-order matching (but not full unification):
notepad
begin
let "(+) ?a ?b" = "0 + 1"
term ?a
term ?b
end
If this is not enough, the Isabelle Cookbook is indeed the place to
start. Both substitution and unification are explained in Chapter 3
(Isabelle Essentials).
Best,
Lukas
Am 27.02.25 um 23:57 schrieb Oleksandr Gavenko:
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:
- printing of substitution in expression
- finding MGU for a given expression and existing theorem
=======
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
endbut 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: Apr 18 2025 at 01:39 UTC