[isabelle-dev] Metis vs. polymorphism

[Lawrence Paulson]

No doubt this is my responsibility, but this very complicated heap of code has been out of my consciousness for many years. Sorting it out would be a non-trivial project.

Larry

> On 30 Dec 2014, at 15:06, Makarius <makarius at sketis.net> wrote:
> 
> Metis proof reconstruction is already known to have occasional problems due to polymorphism.  E.g. a long-pending question is how to avoid the various workarounds for Thm.bicompose that can be seen in Brownian motion here:
> 
> changeset:   52225:568b2cd65d50
> user:        wenzelm
> date:        Wed May 29 18:55:37 2013 +0200
> files:       src/HOL/Tools/Metis/metis_reconstruct.ML
> description:
> resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
> 
> 
> A related or unrelated Metis breakdown happened after a slight reform to give it a proper proof context (115965966e15), such that internal tools may refer to configuration options from the context as expected.
> 
> A bad consequence of that were a handful of broken Metis proofs (one in main Isabelle, the rest in AFP).  E.g. see
> 
> changeset:   59166:4e43651235b2
> user:        wenzelm
> date:        Sun Dec 21 15:59:19 2014 +0100
> files:       src/HOL/Cardinals/Cardinal_Order_Relation.thy
> description:
> recovered metis proof after 115965966e15 (Odd clash of type variables!?);
> 
> 
> In all these situations there were (redundant) polymorphic "uses" in the proof state, that could somehow cause a clash with schematic type variables inside Metis.  Presumably, Metis does not observe the Isabelle proof context with its notion of locally used names -- but this is really just a guess from a big distance from the actual code.
> 
> I did not change anything there, but repaired these very few proofs manually, by omitting the unused polymorphic facts.
> 
> 
> There is probably no immediate need for further action, although someone who understands Metis proof reconstruction might want to clean up its internal treatment of locally generated types, to eliminate this potential of surprise.
> 
> 
> 	Makarius
> 
> ----------------------------------------------------------------------------
>                http://stop-ttip.org  1,235,909 Participants
> ----------------------------------------------------------------------------
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev