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
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
