Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with auto (at ML level)

Email Gateway (Aug 18 2022 at 14:03):

From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,

I found a somewhat strange difference in the behaviour of auto_tac
between an ISAR-level execution and an ML-level execution:

lemma aux :
"triangle ?X3X79 ?X2X77 ?X1X75 \<and> ?X3X79 ~= ?X2X77 \<and> ?X2X77
~= ?X1X75 \<and> ?X3X79 ~= ?X1X75"
apply(auto intro: abs_cases )
done

does the trick: searching between several intro-rules one possible
solution that instantiates
the meta-variables conveniently.

In contrast:
ML{* fun auto_solver thms {prems: Thm.thm list, context:
Proof.context} =
auto_tac ((local_claset_of context) addIs thms,
local_simpset_of context)*}

lemma aux :
"triangle ?X3X79 ?X2X77 ?X1X75 \<and> ?X3X79 ~= ?X2X77 \<and> ?X2X77
~= ?X1X75 \<and> ?X3X79 ~= ?X1X75"
apply(tactic "(auto_solver (thms\"abs_cases\")){prems=[], context=
@{context}}")

looks as if "auto intro!: abs_cases" has been fired; backtracking is
reduced to just choosing
the first match and getting stuck.

The full example is in the appendix.

Can anybody point me out where I oversimplified Isar's way to control
auto_tac ?

Best regards,

bu
Trian.thy

Email Gateway (Aug 18 2022 at 14:03):

From: Makarius <makarius@sketis.net>
The problem here is that the old operators addIs (and simular) prefer
rules from right to left, while Isar declarations work in textual order
from left to right. Thus the internal priorities of the rules come out
differently.

Your example works, if auto_solver is defined like this:

ML {*
fun auto_solver thms {prems: Thm.thm list, context: Proof.context} =
auto_tac (local_claset_of context addIs (rev thms),
local_simpset_of context)
*}

Here (rev thms) does the trick.

Makarius

Last updated: Apr 24 2024 at 20:16 UTC