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



Hi Brian,

I am not sure whether this will help to establish your
theorem, but here is something to get you started. "Descending"
can only guess what the theorem should look like on
the raw type. From what I have seen it might guess wrong 
in case of higher-order theorems (or in case where you are
trying to lift constants of type ('a list) list to 
('a fset) fset). 

One way to get around this is to already provide the
lemma from which you want to lift. Like so

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

lemma map_concat_rev:
  "concat (map (map f) xss) = map f (concat xss)"
by (rule map_concat[symmetric])

lemma 
  "concat_fset (map_fset (map_fset f) xss) = map_fset f (concat_fset xss)"
apply(lifting map_concat_rev)


Hope this helps,
Christian



Brian Huffman writes:
 > 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.