[isabelle-dev] NEWS: oracle/thm dependencies for class instantiations

[Makarius]

*** 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
-------------- next part --------------
theory Test
  imports FOL
begin

ML \<open>Proofterm.proofs := 1\<close>  (*adhoc change at run-time (!) to record oracle propositions below*)

lemma any: "PROP any" sorry

class unit = "term" +
  fixes U :: 'a
  assumes U_eq: "x = U"

typedecl u1
instance u1 :: unit sorry

typedecl u2
instance u2 :: unit by (rule any)

lemma eq1: "x = y" for x y :: u1
  by (simp add: U_eq [of x] U_eq [of y])

lemma eq2: "x = y" for x y :: u2
  by (simp add: U_eq [of x] U_eq [of y])

thm_oracles eq1
thm_oracles eq2
thm_oracles eq1 eq2

end