Re: [isabelle] theory_of_thm @{thm xxx}



On Wed, 22 Aug 2012, Thomas Sewell wrote:

For instance, a system like Isabelle could have theorems depend on lists of theories, or equivalently construct meet/join objects in the theory lattice. It would probably be inefficient and sometimes surprising, but it could be done. I'm not saying that this is a good approach, I'm saying that the vagueness of principle encompasses it.

Until 1997 there was indeed an explicit join (merge) constructed for incomparable theory stamps. This was a bit inefficient, and sometimes occurred in surprising situations, so we discontinued it.

Nonetheless, the join (least upper bound of given theory stamps) is sometimes not sufficient to do the job, it might be still too small for the current context where you are working. Say you want to instantiate a theorem with variables that have type class constraints, but the merge of theories does not give you the required instance yet. (Such incidents did happen in practical situations in the past and motivated the rethinking of the concepts.)

The claim of the current Isabelle scheme of trivial merges of already related theories + transfer to the context where you are working is that it addresses all practical situations. I am ready to see counter examples for that claim, if they exist.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.