I waited for this change.
Peter
-------- Original Message --------
Subject: [isabelle-dev] NEWS: oracle/thm dependencies for class instantiations
From: Makarius <[email protected]>
To: isabelle-dev <[email protected]>
CC:
*** General ***
* Internal derivations record dependencies on oracles and other theorems
accurately, including the implicit type-class reasoning wrt. proven
class relations and type arities. In particular, the formal tagging with
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
propagated properly to theorems depending on such type instances.
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
actual proposition that is assumed in the goal and proof context. This
requires at least Proofterm.proofs = 1 to show up in theorem
dependencies.
* Command 'thm_oracles' prints all oracles used in given theorems,
covering the full graph of transitive dependencies.
This refers to Isabelle/86692888c313 (and further changes leading up to
it). The command 'thm_oracles' is documented in isar-ref as usual. Some
examples are in the included Test.thy
This finishes pending implementations that go back to 1994 (type class
inferences by Wenzel), 1996 (oracles by Paulson), 2001 (proofterms by
Berghofer). So after 2 decades we can now officially claim that oracles
are tracked by the inference kernel.
Luckily the performance impact is only 2% .. 10% -- this is rather
small, since every inference that could instantiate type variables needs
to track sort constraints that are solved eventually by a pro-forma
proof (Thm.solve_constraints).
This is only an intermediate result from further improvements of the
internal derivation management (eventually with full export of
dependencies, as well as proofterms -- at least for "small" sessions
like HOL-Analysis; right now even Main HOL still causes problems).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
