[isabelle] locale expressions?
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"
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:
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:
\<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:
shows "~ (lt' b b)"
using less_irrefl .
This archive was generated by a fusion of
Pipermail (Mailman edition) and