[isabelle-dev] Safe approach to hypothesis substitution

[Alexander Krauss]

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 
thread...

I have another small comment on the issue with "algebra": You were 
saying that the goals were solved in the presimplification phase 
together with clarify. Are you sure about this? I played a little with 
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 
answer...

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