A relevant past message. Larry > Begin forwarded message: > > From: Makarius <makar...@sketis.net> > Subject: Re: [isabelle] TERM exception in fologic.ML > Date: 27 October 2014 at 20:22:02 GMT > To: Slawomir Kolodynski <skoko...@yahoo.com> > Cc: "cl-isabelle-us...@lists.cam.ac.uk" <cl-isabelle-us...@lists.cam.ac.uk> > > On Mon, 27 Oct 2014, Slawomir Kolodynski wrote: > >> 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 > > 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: > > * Standard tactics and proof methods such as "clarsimp", "auto" and > "safe" now preserve equality hypotheses "x = expr" where x is a free > variable. Locale assumptions and chained facts containing "x" > continue to be useful. The new method "hypsubst_thin" and the > configuration option "hypsubst_thin" (within the attribute name space) > restore the previous behavior. INCOMPATIBILITY, especially where > induction is done after these methods or when the names of free and > bound variables clash. As first approximation, old proofs may be > repaired by "using [[hypsubst_thin = true]]" in the critical spot. > > > 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 > ----------------------------------------------------------------------------
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev