Email Gateway (Aug 18 2022 at 18:13): Email Gateway (Aug 18 2022 at 18:13):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Consider the following (HOL/Main, Isabelle 2011)
locale preordX2 = le: preorder le lt + le': preorder le' lt'
for le::"'a => 'a => bool" and lt::"'a => 'a => bool"
and le'::"'b => 'b => bool" and lt'::"'b => 'b => bool"
+
fixes preordX2_opn:: "'a => 'b => 'a"
begin
This locale is abstracted over two preorders. I have an operation
"preordX2_opn" on objects of both preorders, so I need explicit type
variables 'a, 'b, for the constituent preorders in order to correctly
specify this operation.
Now consider the trivial lemma:
lemma
fixes a::'a
shows "~ (lt a a)"
using less_irrefl . --"less_irrefl from typeclass preorder"
This proof FAILS:
*** Failed to finish proof
*** At command "."
I suppose the failure is due to typing:
thm less_irrefl
\<not> (lt'\<Colon>'b \<Rightarrow> 'b \<Rightarrow> bool) (?x\<Colon>'b) ?x
It seems that type variable 'b is incorrect here; less_irrefl should
have a generalized type.
Indeed, the following proof succeeds:
lemma
fixes b::'b
shows "~ (lt' b b)"
using less_irrefl .
Randy
Email Gateway (Aug 18 2022 at 18:13):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Aug 23, 2011 at 12:41 PM, Randy Pollack <rpollack@inf.ed.ac.uk> wrote:
Consider the following (HOL/Main, Isabelle 2011)
locale preordX2 = le: preorder le lt + le': preorder le' lt'
for le::"'a => 'a => bool" and lt::"'a => 'a => bool"
and le'::"'b => 'b => bool" and lt'::"'b => 'b => bool"
+
fixes preordX2_opn:: "'a => 'b => 'a"
begin
Within this locale, you have these two lemmas in scope:
le.less_irrefl: "~ lt x x"
le'.less_irrefl: "~ lt' x x"
Now consider the trivial lemma:
lemma
fixes a::'a
shows "~ (lt a a)"
using less_irrefl . --"less_irrefl from typeclass preorder"
The unqualified lemma name "less_irrefl" is ambiguous here. Isabelle
resolves the ambiguity by picking the most-recently-introduced name
that matches, which happens to be "le'.less_irrefl". If you explicitly
say "using le.less_irrefl" the proof will work.
Last updated: Apr 20 2024 at 12:26 UTC