Re: [isabelle] TERM exception in fologic.ML



On Fri, 12 Dec 2014, Thomas Sewell wrote:

The problem can be traced to the way blast_hyp_subst_tac works, and can
be triggered like this (in HOL):

theory Scratch imports main begin

lemma
  "x = y ==> (!!x. True) ==> x : T ==> S <= T ==> T <= R ==> S <= R"
  apply blast

This will happen when blast is called on any goal, in HOL or in ZF,
where the goal must be nontrivial, provable by blast's internal
strategy, contain a substitutable equality hypothesis, and contain some
non-atomic hypothesis (a meta-forall, meta-implication or meta-equality).

This has always been the case. What has changed is that auto no longer
removes the equality hypothesis itself before calling blast.

The problem is that blast_hyp_subst_tac just won't work if the
hypotheses aren't all atomic. The TERM exception comes from the "map
dest_Trueprop", but in any case the implementation won't work with
meta-operators either.

The trivial fix is to extend the "handle THM _ => no_tac | EQ_VAR => no_tac" in blast_hyp_subst_tac to also handle TERM exceptions. This will completely solve the current problem. I recommend somebody commit this in time for the next release, at which point [[hypsubst_thin = true]] will no longer be needed for this auto.

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
# HG changeset patch
# User wenzelm
# Date 1430229197 -7200
#      Tue Apr 28 15:53:17 2015 +0200
# Node ID 7d523eefe09f67418506d84b9fd2faa0e17dfae1
# Parent  18267ceb10b5d55806af77f89a88ade687e0b10b
test;

diff -r 18267ceb10b5 -r 7d523eefe09f src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Tue Apr 28 11:48:44 2015 +0200
+++ b/src/Provers/hypsubst.ML	Tue Apr 28 15:53:17 2015 +0200
@@ -286,7 +286,7 @@
               inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
               all_imp_intr_tac ctxt hyps i])
   end
-  handle THM _ => no_tac | EQ_VAR => no_tac);
+  handle TERM _ => no_tac | THM _ => no_tac | EQ_VAR => no_tac);
 
 (*apply an equality or definition ONCE;
   fails unless the substitution has an effect*)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.