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





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