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