[isabelle] quotient package: descending method raises type unification error



Hello all,

I tried to test the higher-order lifting capabilities of the
Isabelle2011-1 quotient package recently. Here is my example theory:

theory Scratch
imports "~~/src/HOL/Quotient_Examples/FSet"
begin

lemma "concat_fset (map_fset (map_fset f) xss) = map_fset f (concat_fset xss)"
apply descending

*** Type unification failed: Clash of types "_ list" and "_ fset"
***
*** Type error in application: incompatible operand type
***
*** Operator:  map :: ('b fset \<Rightarrow> 'a fset) \<Rightarrow> 'b
fset list \<Rightarrow> 'a fset list
*** Operand:   map f :: 'b list \<Rightarrow> 'a list

A recent development version (4ecf63349466) yields exactly the same
error message.

To test whether the multiple occurrences of map_fset at different
types were causing the problem, I tried a simpler example:

lemma "concat_fset (map_fset (\<lambda>x. {|x|}) xs) = xs"
apply descending

*** Type unification failed: Clash of types "_ list" and "_ fset"
***
*** Type error in application: incompatible operand type
***
*** Operator:  map :: ('a \<Rightarrow> 'a fset) \<Rightarrow> 'a list
\<Rightarrow> 'a fset list
*** Operand:   \<lambda>x. [x] :: 'a \<Rightarrow> 'a list

Is there some additional configuration/setup I need to do to enable
lifting of higher-order theorems, or does this error indicate a bug in
the quotient package?

Also, can anyone suggest *any* examples of higher-order theorems upon
which the descending method actually works? I can't seem to find one.


- Brian





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