Re: [isabelle] theory_of_thm @{thm xxx}



Thanks Thomas.

In my particular case, I have implemented an attribute that also uses
theorems fetched from record types. The problem is, that the theory that
declares the record type does not import the theory that declares the
attribute.

For now, I solved the problem by fetching the theorems in their original
context, and then transferring them to HOL/Main, assuming that all
theorems that my attribute sees depend on a super-theory of Main, which
is realistic in my case.

Peter

On Mi, 2012-08-22 at 15:31 +1000, 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.
> 
> Yours,
>      Thomas.
> 
> On 22/08/12 02:47, Peter Lammich wrote:
> > Hi all,
> >
> > consider the following toy example:
> >
> > theory Scratch
> > imports Pure
> > begin
> >
> > ML_val {*
> >    theory_of_thm @{thm meta_mp}
> > *}
> >
> > Output: val it = {Pure, Scratch:1}: theory
> >
> >
> > Why is Scratch contained in here? The theorem is defined in Pure, not in
> > Scratch.
> > Is there a way to reference to the theorem by name such that its theory
> > is the one it was defined in, and not the one the antiquotation occurs
> > in?
> > In my real application (using HOL instead of Pure), I get odd
> > "non-trivial theory-merge" exceptions, because "theory_of_thm @{thm
> > xxx}" contains too much.
> >
> >
> > Regards and thanks in advance for any help,
> >    Peter
> >
> >
> >
> 







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