Re: [isabelle] theory_of_thm @{thm xxx}



On Wed, 22 Aug 2012, Thomas Sewell wrote:

In principle, having @{thm meta_mp} live only in @{theory Pure} would make perfect sense.

In practice, this would create a problem if you tried, say:

theory Scratch
imports A B
begin

ML_val {*
Thm.transitive @{thm A.eq1} @{thm B.eq2}
*}

How does Thm.transitive figure out an appropriate context for a rule derived from A.eq1 and B.eq2?

To avoid this problem, A.eq1 and B.eq2 are "pulled" up into theory Scratch when they are fetched, thus allowing derivation operations to proceed without doing any interesting work.

There are other ways in ML to fetch these theorems in their original context, at which point if you attempt resolution or similar you will see the error "Attempt to perform non-trivial merge of theories" from Pure/context.ML.

The proper technical term for "pulled" is "transfer" in Isabelle terminology. What you mention in a certain context needs to be understood in the sense of that context. Formal entities with a back-reference to a context certificate (theory stamp) need to be transferred explicitly, unlike terms who might get re-checked implicitly. (Such system operations are carefully implemented to be monotonic wrt. the theory context.)

The Isar source language alreadys transfers formal entities mentioned in the text: notably 'thm' and @{thm} etc. so one never has to worry about it.


In really ancient times we did not understand this important principle yet, and there were many oddities coming from theorems with incomparable theory stamps, or comparable theory stamps that were just too little for the current context, say to perform an instantiation.

These problems are long forgotten, because the transfer principle is the established way for such a long time already. (This is in disagreement with the very first sentence above.)


	Makarius






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