Re: [isabelle] Question about Contexts and Sorts



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
>
>
>
>





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