[isabelle-dev] Metis vs. polymorphism

[Makarius]

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