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

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

**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

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

- Previous by Date: Re: [isabelle] quotient package: descending method raises type unification error
- Next by Date: [isabelle] Simplification problem
- Previous by Thread: Re: [isabelle] quotient package: descending method raises type unification error
- Next by Thread: [isabelle] Simplification problem
- 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