Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] quotient package: descending method raises typ...

view this post on Zulip Email Gateway (Aug 18 2022 at 18:49):

From: Brian Huffman <huffman@in.tum.de>
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.

view this post on Zulip Email Gateway (Aug 18 2022 at 18:49):

From: Brian Huffman <huffman@in.tum.de>
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.

view this post on Zulip Email Gateway (Aug 18 2022 at 18:49):

From: Brian Huffman <huffman@in.tum.de>
On Sun, Dec 18, 2011 at 10:41 AM, Christian Urban <urbanc@in.tum.de> wrote:

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)

Yes, I also tried this. I understand that the "lifting" method
typically should discharge the current goal, but in this case it
leaves me with two new subgoals:

goal (2 subgoals):

  1. ⋀fa x y.
    ⟦Quot_True map_fset; (list_all2 list_eq OOO list_eq) x y⟧
    ⟹ ((list_eq ===> list_eq) ===>
    list_all2 list_eq OOO list_eq ===> list_all2 list_eq OOO list_eq)
    map map

  2. (∀f xss.
    concat_fset
    (((abs_fset ---> rep_fset) --->
    (map rep_fset ∘ rep_fset) ---> abs_fset ∘ map abs_fset)
    map (map_fset f) xss) =
    map_fset f (concat_fset xss)) =
    (∀f xss.
    concat_fset (map_fset (map_fset f) xss) =
    map_fset f (concat_fset xss))

I'm not sure what I should do at this point. Is there some additional
setup I can do that will allow "lifting" to discharge these
automatically, or are users expected to try to discharge these
manually?

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

--

view this post on Zulip Email Gateway (Aug 18 2022 at 18:49):

From: Christian Urban <urbanc@in.tum.de>
Hi Brian,

Lifting (and descending) cannot always be done completely
automatically. This is already a feature of the original
work of Homeier. This means the tactic just return what
they cannot solve automatically.

If I remember correctly, Cezary and I encountered similar
problems with lifting properties about concat such as

"concat [] = []"
"concat (x # xs) = x @ concat xs"

This required us to do some contortions like proving the
property concat_rsp in FSet.thy.

Best wishes,
Christian

Brian Huffman writes:

On Sun, Dec 18, 2011 at 10:41 AM, Christian Urban <urbanc@in.tum.de> wrote:

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)

Yes, I also tried this. I understand that the "lifting" method
typically should discharge the current goal, but in this case it
leaves me with two new subgoals:

goal (2 subgoals):
1. ⋀fa x y.
⟦Quot_True map_fset; (list_all2 list_eq OOO list_eq) x y⟧
⟹ ((list_eq ===> list_eq) ===>
list_all2 list_eq OOO list_eq ===> list_all2 list_eq OOO list_eq)
map map
2. (∀f xss.
concat_fset
(((abs_fset ---> rep_fset) --->
(map rep_fset ∘ rep_fset) ---> abs_fset ∘ map abs_fset)
map (map_fset f) xss) =
map_fset f (concat_fset xss)) =
(∀f xss.
concat_fset (map_fset (map_fset f) xss) =
map_fset f (concat_fset xss))

I'm not sure what I should do at this point. Is there some additional
setup I can do that will allow "lifting" to discharge these
automatically, or are users expected to try to discharge these
manually?

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

--

view this post on Zulip Email Gateway (Aug 18 2022 at 19:09):

From: Brian Huffman <huffman@in.tum.de>
[Note to isabelle-users members: This a continuation of an old thread
from Dec. 18.]

On Fri, Feb 3, 2012 at 4:35 PM, Cezary Kaliszyk
<cezarykaliszyk@gmail.com> wrote:

Hi Brian,

It is very late to answer your email, but I added the compositional
respectfulness and preservation theorems for 'map', which means
that the theorem you mentioned (map_concat) now lifts automatically.

Hi Cezary,

Thanks for adding the new respectfulness and preservation theorems for
map. Unfortunately the descending method still produces the same error
message, but the proof does indeed work with the lifting method now:

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

lemma "map_fset f (concat_fset xss) = concat_fset (map_fset (map_fset f) xss)"
by (lifting map_concat)

I also tried my other example again:

lemma concat_map_single: "concat (map (\<lambda>x. [x]) xs) = xs"
by (induct xs, simp_all)

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

Here the lifting method leaves a couple of subgoals, but by following
your example I was able to state and prove the necessary
respectfulness and preservation theorems:

lemma map_rsp3 [quot_respect]:
"((op = ===> list_eq) ===> list_eq ===> list_all2 list_eq OOO
list_eq) map map"

lemma map_prs3 [quot_preserve]:
"((id ---> rep_fset) ---> rep_fset ---> (abs_fset o map abs_fset))
map = map_fset"

So it seems that the quotient package needs a separate respectfulness
theorem for each of these type instances of map:

map_rsp, for map :: ('a => 'b) => 'a list => 'b list
map_rsp2, for map :: ('a list => 'b list) => 'a list list => 'b list list
map_rsp3, for map :: ('a => 'b list) => 'a list => 'b list list

I suppose I would need another theorem map_rsp4 in order to use map at
type ('a list => 'b) => 'a list list => 'b list, for example.

Moving on, I also tried lifting another monad law, which gave me a
completely new error message.

lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)"
by (induct xsss, simp_all)

lemma "concat_fset (map_fset concat_fset xsss) = concat_fset (concat_fset xsss)"
apply (lifting concat_map_concat)

*** Solve_quotient_assm failed. Possibly a quotient theorem is missing.

Perhaps you could help me determine what quotient theorem I need here?
I suspect that this error has something to do the variable xsss :: 'a
list list list, with the 3-deep nesting of the list type.

On Sun, Dec 18, 2011 at 11:46 AM, Christian Urban <urbanc@in.tum.de> wrote:

Hi Brian,

Lifting (and descending) cannot always be done completely
automatically. This is already a feature of the original
work of Homeier. This means the tactic just return what
they cannot solve automatically.

If I remember correctly, Cezary and I encountered similar
problems with lifting properties about concat such as

"concat [] = []"
  "concat (x # xs) = x @ concat xs"

This required us to do some contortions like proving the
property concat_rsp in FSet.thy.

Best wishes,
Christian

Brian Huffman writes:

On Sun, Dec 18, 2011 at 10:41 AM, Christian Urban <urbanc@in.tum.de> wrote:
 > >
 > > 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)
 >
 > Yes, I also tried this. I understand that the "lifting" method
 > typically should discharge the current goal, but in this case it
 > leaves me with two new subgoals:
 >
 > goal (2 subgoals):
 >  1. ⋀fa x y.
 >        ⟦Quot_True map_fset; (list_all2 list_eq OOO list_eq) x y⟧
 >        ⟹ ((list_eq ===> list_eq) ===>
 >            list_all2 list_eq OOO list_eq ===> list_all2 list_eq OOO list_eq)
 >            map map
 >  2. (∀f xss.
 >         concat_fset
 >          (((abs_fset ---> rep_fset) --->
 >            (map rep_fset ∘ rep_fset) ---> abs_fset ∘ map abs_fset)
 >            map (map_fset f) xss) =
 >         map_fset f (concat_fset xss)) =
 >     (∀f xss.
 >         concat_fset (map_fset (map_fset f) xss) =
 >         map_fset f (concat_fset xss))
 >
 > I'm not sure what I should do at this point. Is there some additional
 > setup I can do that will allow "lifting" to discharge these
 > automatically, or are users expected to try to discharge these
 > manually?
 >
 > - Brian
 >
 > > 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
 > >
 > > --

--

--
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/~cek/

view this post on Zulip Email Gateway (Aug 18 2022 at 19:11):

From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Hi Brian,

On Sat, Feb 04, 2012 at 10:05:00AM +0100, Brian Huffman wrote:

It is very late to answer your email, but I added the compositional
respectfulness and preservation theorems for 'map', which means
that the theorem you mentioned (map_concat) now lifts automatically.
Thanks for adding the new respectfulness and preservation theorems for
map. Unfortunately the descending method still produces the same error
message [...]

Should be fixed now. As mentioned before in this thread the procedure
for guessing which theorem one wants to lift (and the procedure for
guessing the lifted theorem) is a heuristic. The idea for the
heuristic is to be greedy as this is what the user wants in most
cases, however the implementation was not greedy enough.

Moving on, I also tried lifting another monad law, which gave me a
completely new error message.

lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)"
by (induct xsss, simp_all)

lemma "concat_fset (map_fset concat_fset xsss) = concat_fset (concat_fset xsss)"
apply (lifting concat_map_concat)

*** Solve_quotient_assm failed. Possibly a quotient theorem is missing.

Perhaps you could help me determine what quotient theorem I need here?
I suspect that this error has something to do the variable xsss :: 'a
list list list, with the 3-deep nesting of the list type.

If instead of lifting you use lifting_setup and manually apply
regularize and injection, you can see the missing quotient theorem,
namely:

Quotient (list_all2 (list_all2 op \<approx> OOO op \<approx>) OOO op \<approx>)
(abs_fset \<circ> map (abs_fset \<circ> map abs_fset))
(map (map rep_fset \<circ> rep_fset) \<circ> rep_fset)

Since this involves a composition of 3 relations I imagine it to be
very tedious to prove; but if you declare it with the [quot_thm]
attribute, the lifting will only leave the usual respectfulness and
preservation obligations.

Regards,

Cezary

On Sun, Dec 18, 2011 at 11:46 AM, Christian Urban <urbanc@in.tum.de> wrote:

Hi Brian,

Lifting (and descending) cannot always be done completely
automatically. This is already a feature of the original
work of Homeier. This means the tactic just return what
they cannot solve automatically.

If I remember correctly, Cezary and I encountered similar
problems with lifting properties about concat such as

"concat [] = []"
  "concat (x # xs) = x @ concat xs"

This required us to do some contortions like proving the
property concat_rsp in FSet.thy.

Best wishes,
Christian

Brian Huffman writes:

On Sun, Dec 18, 2011 at 10:41 AM, Christian Urban <urbanc@in.tum.de> wrote:
 > >
 > > 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)
 >
 > Yes, I also tried this. I understand that the "lifting" method
 > typically should discharge the current goal, but in this case it
 > leaves me with two new subgoals:
 >
 > goal (2 subgoals):
 >  1. ⋀fa x y.
 >        ⟦Quot_True map_fset; (list_all2 list_eq OOO list_eq) x y⟧
 >        ⟹ ((list_eq ===> list_eq) ===>
 >            list_all2 list_eq OOO list_eq ===> list_all2 list_eq OOO list_eq)
 >            map map
 >  2. (∀f xss.
 >         concat_fset
 >          (((abs_fset ---> rep_fset) --->
 >            (map rep_fset ∘ rep_fset) ---> abs_fset ∘ map abs_fset)
 >            map (map_fset f) xss) =
 >         map_fset f (concat_fset xss)) =
 >     (∀f xss.
 >         concat_fset (map_fset (map_fset f) xss) =
 >         map_fset f (concat_fset xss))
 >
 > I'm not sure what I should do at this point. Is there some additional
 > setup I can do that will allow "lifting" to discharge these
 > automatically, or are users expected to try to discharge these
 > manually?
 >
 > - Brian
 >
 > > 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
 > >
 > > --

--

Last updated: Nov 21 2024 at 12:39 UTC