*To*: Tjark Weber <webertj at in.tum.de>*Subject*: Re: [isabelle] Question about Contexts and Sorts*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 19 Jan 2011 10:08:52 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1295457974.5459.44.camel@weber>*References*: <1295457974.5459.44.camel@weber>*Sender*: huffman.brian.c at gmail.com

Hi Tjark, You can get an idea of what is going on by printing a few raw terms within the context of the proof. lemma (in B) "b = c" ML_val {* concl_of @{thm c_def} *} ML_val {* concl_of @{thm b_def} *} ML_val {* concl_of @{thm B_class.b_def} *} You will notice that in the "B" context, theorem c_def states "Scratch.C_class.c = Scratch.A_class.a", and is polymorphic, having a schematic type variable "?'a::Scratch.C". This is the same as its usual meaning in the top-level context. On the other hand, in the "B" context, theorem b_def is not the same polymorphic theorem that you would get at the top-level. It states that "Scratch.B.b a = a", where "a" is a free variable of type "'a::HOL.type". The variable "a" and type variable 'a are both fixed by the context. In the "B" context, the top-level polymorphic version of b_def must be referred to by its qualified name "B_class.b_def". Now let's look at the raw representation of what you are trying to prove: ML_val {* @{term "?thesis"} *} This reveals that you are trying to show "Scratch.B_class.b = Scratch.C_class.c". The theorem referred to by the name "b_def" in this context is not helpful here. The proof will succeed if you use "B_class.b_def", though. > lemma (in B) "b = c" by (simp only: B_class.b_def c_def) I guess the confusion comes from the fact that in context "B", the term "b" can have two completely different meanings, depending on its type. I wonder if there is a way to configure the pretty-printer so that it would be easier to distinguish the two? - Brian On Wed, Jan 19, 2011 at 9:26 AM, Tjark Weber <webertj at in.tum.de> wrote: > Hi, > > Could someone who understands Isabelle's contexts, classes and sorts > better than I do perhaps enlighten me why the second proof in the > example theory below fails? (I guess it fails because b_def is > expecting sort HOL.type, while the actual sort is {Scratch.B,Scratch.C}. > However, I don't quite understand the reason for this. Is it a bug? Is > there a workaround?) > > Many thanks in advance! > > Kind regards, > Tjark > > ========== 8< ========== > > theory Scratch imports Main > begin > > class A = > fixes a :: 'a > > class B = A > begin > definition "b = a" > end > > class C = A > begin > definition "c = a" > end > > lemma bc: "b = c" by (simp only: b_def c_def) > > lemma (in B) "b = c" by (simp only: b_def c_def) > -- {* fails because b_def is expecting sort HOL.type *} > > end > > > >

**Follow-Ups**:**Re: [isabelle] Question about Contexts and Sorts***From:*Tjark Weber

**References**:**[isabelle] Question about Contexts and Sorts***From:*Tjark Weber

- Previous by Date: [isabelle] Question about Contexts and Sorts
- Next by Date: Re: [isabelle] Question about Contexts and Sorts
- Previous by Thread: [isabelle] Question about Contexts and Sorts
- Next by Thread: Re: [isabelle] Question about Contexts and Sorts
- Cl-isabelle-users January 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list