[isabelle-dev] Safe approach to hypothesis substitution

[Alexander Krauss]

Hi Thomas,

Thomas Sewell wrote:
> I should clear up some confusion that may have been caused by my
> mail. I was trying to avoid repeating all that had been said on this
> issue, and it seems I left out some that hadn't been said as well.
> 
> This approach avoids ever deleting an equality on a Free variable
> during a 'safe' reasoning step. It will substitute with that equality
> but keep it in place.

Thanks for the clarification. I think I understand better now.

> Note that with this
> change terminal tactics operating in 'unsafe' mode - fast, best, etc
> - will call thin_triv_tac via Context_Rules and behave similarly to
> before.

similarly? :-)))

What different behaviour could occur?

> 2. Yes, count vars is a bit strange, as it will consider "(%f. f)
> (%x. x)" to contain two copies of Bound -1. The point is to count
> loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp,
> which it gets right.

So it's probably just the name that confused me...

Best,
Alex