Email Gateway (Aug 19 2022 at 16:10): Email Gateway (Aug 19 2022 at 16:10):From: Slawomir Kolodynski <skokodyn@yahoo.com>
When I was updating the IsarMathLib project for Isabelle 2014 I got the following:
*** exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
*** dest_Trueprop
*** !!f A B. ALL a b. f : Pi(A, B) --> <a, b> : f <-> a : A & f ` a = b
*** At command "by" (line 605 of "~/Projects/IsarMathLib/isarmathlib-1.9.1/IsarMathLib/func1.thy")
*** exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
*** dest_Trueprop
*** !!a A B. a : Sigma(A, B) --> <fst(a), snd(a)> = a
*** At command "by" (line 296 of "~/Projects/IsarMathLib/isarmathlib-1.9.1/IsarMathLib/Topology_ZF_10.thy")
I was able to work around this by rewriting the proofs slightly. I understand that the TERM exceptions are not just failures to check a proof but some internal errors (?), so I just wanted to report this for consideration for the next release.
The exception can be replicated by checking the following theory (in ZF logic)
theory Scratch imports func
begin
lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X"
shows "f(A) = {f`(x). x \<in> A}"
proof
from A1 show "f(A) \<subseteq> {f(x). x \<in> A}"
using image_iff apply_iff by auto
show "{f(x). x \<in> A} \<subseteq> f(A)"
proof
fix y assume "y \<in> {f`(x). x \<in> A}"
then obtain x where "x\<in>A \<and> y = f`(x)"
by auto
with A1 A2 show "y \<in> f(A)"
using apply_iff image_iff by auto
qed
qed
end
Regards,,Slawomir Kolodynski http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Email Gateway (Aug 19 2022 at 16:11):From: Makarius <makarius@sketis.net>
A TERM exception is indeed an internal breakdown. With some fiddling, I
managed to get an exception trace as follows (via Poly/ML 5.3.0):
List.map(2)
List.map(2)
List.map(2)
List.map(2)
Hypsubst().blast_hyp_subst_tac(1)(2)
Tactical.CSUBGOAL(3)
Tactical.CSUBGOAL(3)
Tactical.CSUBGOAL(3)
Tactical.EVY(1)(1)
Blast().raw_blast(4)cont(3)
Blast().prove(4)prv(4)closeF(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)closeF(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)closeF(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)
Blast().prove(4)
Blast().raw_blast(4)
This indicates that it is related to the following change from NEWS:
So your proof works again like this:
using [[hypsubst_thin = true]] by auto
Although that can only be a temporary workaround.
Thomas Sewell who made the hypsubst change should be able to say more
about this situation.
Makarius
http://stop-ttip.org 743,200 people so far
Email Gateway (Aug 22 2022 at 09:31):From: Makarius <makarius@sketis.net>
Trying that -- according to the included ch-test -- it leads to
non-termination of "blast" in the above example, but "auto" works.
My impression is that blast.ML is a bit non-canonical in many respects,
not just superficially due to the use of camel case in the source. Its
use of strip_Trueprop looses information about presence or absence of
Trueprop. Later use of Data.hyp_subst_tac may stumble on that.
Makarius
ch-test
Email Gateway (Aug 22 2022 at 09:31):From: Larry Paulson <lp15@cam.ac.uk>
Blast was never intended to do anything intelligent in the presence of meta-level connectives, which are much more common now, so some adjustments may be necessary.
Larry
Email Gateway (Aug 22 2022 at 09:41):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Perhaps a simple fix to the issue would be to avoid blast every seeing
meta-operators by atomizing them into their HOL/FOL counterparts first.
I'm not sure if this solution necessarily "plays nice" with every rule
that blast might be given, though. Perhaps rules that would introduce or
eliminate meta-operators would have to be normalized as well.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:53):From: Larry Paulson <lp15@cam.ac.uk>
It would have to be tested. Such formulas would necessarily be complex, with the danger of increasing runtimes significantly. The alternative is to filter them out.
Larry
Email Gateway (Aug 22 2022 at 12:17):From: Slawomir Kolodynski via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Back in October 2014 I reported an error that I encountered when updating IsarMathLib to Isabelle 2014.The error is still there in Isabelle2016-RC1. This can be replicated by checking the following theory (in Isabelle/ZF logic):
theory Scratch imports func
begin
lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X"
shows "f(A) = {f`(x). x \<in> A}"
proof
from A1 show "f(A) \<subseteq> {f(x). x \<in> A}"
using image_iff apply_iff by auto
show "{f(x). x \<in> A} \<subseteq> f(A)"
proof
fix y assume "y \<in> {f`(x). x \<in> A}"
then obtain x where "x\<in>A \<and> y = f`(x)"
by auto
with A1 A2 show "y \<in> f(A)"
using apply_iff image_iff by auto
qed
qed
end
which gives
exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
dest_Trueprop
⋀f A B.
∀a b. f ∈ Pi(A, B) ⟶
⟨a, b⟩ ∈ f ⟷ a ∈ A ∧ f ` a = b
in Isabelle/jEdit tooltip at the last auto keyword.
This is not a very important problem for me as I can work around it, but maybe it's good to know that it is still there.
Slawomir Kolodynski
Email Gateway (Aug 22 2022 at 12:17):From: Makarius <makarius@sketis.net>
On Sat, 23 Jan 2016, Slawomir Kolodynski via Cl-isabelle-users wrote:
Back in October 2014 I reported an error that I encountered when
updating IsarMathLib to Isabelle 2014. The error is still there in
Isabelle2016-RC1.
Yes, for the historical record the thread started here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00116.html
That was after the Isabelle2014 release. For the release process of
Isabelle2015, it was discussed again here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-April/msg00303.html
The conclusion: no conclusion yet. It not easy to change the situation
without revisiting the "blast" implementation, and it was not done in the
meantime. So it won't happen for Isabelle2016.
This is not a very important problem for me as I can work around it, but
maybe it's good to know that it is still there.
For the record on this mailing list: in October 2014 the workaround was
like this:
using [[hypsubst_thin]] by auto
Of course you can also do this more globally via "declare
[[hypsubst_thin]]", although you loose the potential benefit of the
hypsubst change behind this (see NEWS of Isabelle2014).
Makarius
Last updated: Apr 24 2024 at 16:18 UTC