# [isabelle-dev] Safe approach to hypothesis substitution

Alexander Krauss krauss at in.tum.de
Wed Aug 25 12:10:15 CEST 2010

```Hi Thomas,

Thomas Sewell wrote:
> It's interesting that my innocent thread on hypothesis substitution
> has been hijacked into a discussion about context-aware coding
> guidelines.

There is still hope if we move the unrelated discussions to another

I have another small comment on the issue with "algebra": You were
saying that the goals were solved in the presimplification phase
the theory, and it seemed to me that it is only solved using the fact
"dvd_mult2", which is not used in the presimplification rules. Thus,
clarify leaves behind an assumption which somehow confuses the following
code. I am not sure what assumptions are made by the following code, but
maybe it should be able to ignore additional assumptions...? Maybe Amine
Chaieb can comment on this further, but it may take a while to get an

As you say, terminal methods that break with the patch are problematic,
so we should try to understand this, even if we decide in the end that
it is a problem of the algebra method.

One more small thing:

> @@ -115,27 +116,55 @@
>       | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
>                         then raise Match
>                         else false               (*eliminates u*)
> -     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
> +     | (Free f, _) =>  if bnd orelse Logic.occs(Free f,u) orelse
>                            novars andalso has_vars u
>                         then raise Match
>                         else true                (*eliminates t*)
> -     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
> +     | (_, Free f) =>  if bnd orelse Logic.occs(Free f,t) orelse
>                            novars andalso has_vars t
>                         then raise Match
>                         else false               (*eliminates u*)
>       | _ => raise Match;

How is this change related to the rest? It seems to me that the only
difference between (Free f) and t/u is only the possible eta
contraction... So my question should rather be: Why was this correct before?

Alex

```