Email Gateway (Aug 19 2022 at 17:05): Email Gateway (Aug 19 2022 at 17:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
The error message "Failed to refine any pending goal" usually comes from one of the
following mistakes:
a) Your show statement does not match a conclusion of a goal (often there is a typo).
b) The assumption that you have "assume"d do not match the assumption of the goal that you
are trying to show with "show".
In your case, it is mistake b). In the original lemma statement, the assumption "2 dvd
(x::int)*x" was part of the goal, so you have to assume it inside the block. When you
rewrite the statement to
lemma
fixes x :: int
assumes s: "2 dvd x*x"
shows "2 dvd x"
then the assumption is already part of the context and no longer of the goal. You can
observe this change also in the output buffer when you look at the raw goal state.
Nevertheless, you still have the (now superfluous) assume 1: "2 dvd x*x" in your Isar
proof. That is, you are making an assumption that is no longer part of the goal state, so
you get an error upon show. If you delete this assume and use the assumption from the
lemma statement instead, everything should work fine.
Andreas
Email Gateway (Aug 19 2022 at 17:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
The Isabelle/Isar reference manual (available from the documentation panel) explains the
general syntax of mixfix syntax annotations. They are normally enclosed in parenthesis and
go between the type declaration and the "where" clause of fun/definition/inductive, etc.
Alternatively, you can also use the command "notation" for functions that have already
been defined. Examples of \<^bsub> \<^esub> can be found in library in theory Map.thy for
the function restrict_map.
Best,
Andreas
Email Gateway (Aug 19 2022 at 17:18):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
On 21/02/15 02:21, W. Douglas Maurer wrote:
The Isabelle/Isar reference manual (available from the documentation panel) explains the
general syntax of mixfix syntax annotations. They are normally enclosed in parenthesis
and go between the type declaration and the "where" clause of fun/definition/inductive,
etc. Alternatively, you can also use the command "notation" for functions that have
already been defined. Examples of \<^bsub> \<^esub> can be found in library in theory
Map.thy for the function restrict_map.Thanks. I'm not sure that I will ever do this myself, but I am going to show my students
how to do it in case they would like to try it.
Meanwhile I'm putting together some proofs involving dvd and the even function, using
theory Parity. One of the lemmas in Parity is lemma even_iff_2_dvd [algebra]: even a <-->
2 dvd a by (simp add: even_def dvd_eq_mod_eq_0). So I substituted 38 for a, obtaining
"even((38::int)) <--> (2::int) dvd (38::int)". Then I used try0, and try0 said: Try this:
by auto (auto, presburger, force: 0 ms; simp: 1 ms; fastforce: 8 ms). But one of the
methods that try0 tried was algebra, and algebra is not on that list. So what does lemma
even_iff_2_dvd [algebra] mean, then? If it read [simp] instead of [algebra], that would
mean that this is a simprule, something that simp tries. So why doesn't [algebra] mean
that this is something that algebra tries? And does that apply to other rule names in
square brackets, like [presburger]? Thanks! -WDMaurer
The annotations in square brackets are called attributes and they have a variety of
purposes. In the case of [algebra] and [presburger], they indeed indicate that these rules
should be used by these proof methods. From what I know, these two methods reason
abstractly, not for concrete numbers like 38. Moreover, I am not familiar with the
internals of try or try0. If you want to see whether algebra can solve this, just write
"by algebra" and see whether this works, too.
Andreas
--
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875
Last updated: Apr 19 2024 at 01:05 UTC