Email Gateway (Aug 18 2022 at 16:48): Email Gateway (Aug 18 2022 at 16:48):From: Tjark Weber <webertj@in.tum.de>
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
Email Gateway (Aug 18 2022 at 16:48):From: Brian Huffman <brianh@cs.pdx.edu>
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?
Email Gateway (Aug 18 2022 at 16:48):From: Tjark Weber <webertj@in.tum.de>
Brian,
Indeed. Try
lemma (in B) "b = c"
apply (cut_tac b_def)
(with Long Names switched on for greater effect). No wonder I was
confused.
Thanks for your quick reply!
Kind regards,
Tjark
Last updated: Apr 25 2024 at 01:08 UTC