<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">

<html>

<head>

  <meta content="text/html; charset=ISO-8859-1"

 http-equiv="Content-Type">

  <title></title>

</head>

<body text="#000000" bgcolor="#ffffff">

On 08/25/2010 07:57 AM, Thomas Sewell wrote:

<blockquote

 cite="mid:2EB36A07AAE8C44BBB1986425E7A22D01287FF3F33@atp-mbx1.in.nicta.com.au"

 type="cite">

  <pre wrap="">It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines.</pre>

</blockquote>

<br>

Sorry for that. ^^<br>

<br>

<blockquote

 cite="mid:2EB36A07AAE8C44BBB1986425E7A22D01287FF3F33@atp-mbx1.in.nicta.com.au"

 type="cite">

  <pre wrap="">I'm trying to steer clear of contexts - it would seem more elegant to me if there was a purely tactical solution to this problem.

  </pre>

</blockquote>

<br>

Well as you said<br>

<blockquote>

  <pre wrap="">There's no truly safe way to delete an equality on a Free variable without inspecting the whole context.

  </pre>

</blockquote>

<br>

<blockquote

 cite="mid:2EB36A07AAE8C44BBB1986425E7A22D01287FF3F33@atp-mbx1.in.nicta.com.au"

 type="cite">

  <pre wrap="">

To answer Andreas' question about blast_hyp_subst_tac:

I made some attempts, but it seemed that making blast_hyp_subst_tac share behaviour or even code with the other versions led to incompatibilities I didn't really understand. The patch I sent keeps blast_hyp_subst_tac strictly in compatibility mode with previous behaviour.</pre>

</blockquote>

<br>

Ahh, ok.<br>

<br>

<blockquote

 cite="mid:2EB36A07AAE8C44BBB1986425E7A22D01287FF3F33@atp-mbx1.in.nicta.com.au"

 type="cite">

  <pre wrap="">I think you've outlined why there was a problem - blast is guessing incorrectly what the tactic will do. Perhaps in the future the Hypsubst ML structure could export its eq_var and triv_asm term inspection functions so blast would have a better idea what it would do (assuming blast can construct accurately what the subgoal passed would be).

  </pre>

</blockquote>

<br>

Blast has a different term structure with Skolems replacing

Goal-Parameters etc. In the current architecture<br>

there seems to be no easy way to get a subgoal of the search back as an

isabelle subgoal.<br>

<br>

</body>

</html>