*To*: christian.urban at kcl.ac.uk*Subject*: Re: [isabelle] quotient package: descending method raises type unification error*From*: Brian Huffman <huffman at in.tum.de>*Date*: Sun, 18 Dec 2011 10:58:29 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20111218094214.6EE39116E001@talisker.in.tum.de>*References*: <CAAMXsiY_tz7zCcT3mBonewVgxmZ_TX98aNc=b+rOAtJdPkc7AQ@mail.gmail.com> <20111218094214.6EE39116E001@talisker.in.tum.de>

On Sun, Dec 18, 2011 at 10:41 AM, Christian Urban <urbanc at 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 > > --

**Follow-Ups**:**Re: [isabelle] quotient package: descending method raises type unification error***From:*Christian Urban

**References**:**[isabelle] quotient package: descending method raises type unification error***From:*Brian Huffman

**[isabelle] quotient package: descending method raises type unification error***From:*Christian Urban

- Previous by Date: [isabelle] quotient package: descending method raises type unification error
- Next by Date: Re: [isabelle] quotient package: descending method raises type unification error
- Previous by Thread: [isabelle] quotient package: descending method raises type unification error
- Next by Thread: Re: [isabelle] quotient package: descending method raises type unification error
- Cl-isabelle-users December 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list