*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Finite_Set comp_fun_commute*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Tue, 19 Feb 2013 17:43:02 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1361288296.2373.95.camel@lapbroy33>*References*: <ACB40174-AB28-4980-85BB-DC77A6D13891@cam.ac.uk> <1361288296.2373.95.camel@lapbroy33>

Hi Peter, thanks very much for this. Forgive me if I'm mistaken, but I don't understand how either of these approaches would help. I think I would still need to reason about terms like > fold f s (insert a A) in order to complete the induction, and I can't reason about such terms without knowing that f satisfies the "comp_fun_commute" property. Let me state my problem more concretely... Finite_Set provides the following lemma (the first assumption comes from the context "comp_fun_commute"): > lemma fold_image: > assumes "⋀x y. f x ∘ f y = f y ∘ f x" > assumes "finite A" and "inj_on g A" > shows "fold f x (g ` A) = fold (f ∘ g) x A" But I want the following lemma: > lemma fold_image_stronger: > assumes "⋀x y. ⟦ x ∈ A ; y ∈ A ⟧ ⟹ f x ∘ f y = f y ∘ f x" > assumes "finite A" and "inj_on g A" > shows "fold f x (g ` A) = fold (f ∘ g) x A" How might I prove it? It's tricky because all the other lemmas about Finite_Set.fold are in the "comp_fun_commute" context where > ⋀x y. f x ∘ f y = f y ∘ f x holds, whereas I only have the weaker property > ⋀x y. ⟦ x ∈ A ; y ∈ A ⟧ ⟹ f x ∘ f y = f y ∘ f x available to me. Thanks very much, john On 19 Feb 2013, at 16:38, Peter Lammich wrote: > Hi. > > An alternative is to use an invariant rule, i.e., something like: > > > I s a0 !!x s a. [| I s a; x\in s |] ==> I (s-{x}) (f x a) > ------------------------------------------------------------ if finite s > I {} (fold f s a0) > > > or, alternatively, show that your proposition holds for folding over any > distinct list representing the set: > > > !!l. [| distinct l; set l = s |] ==> P (foldl f l a0) > -------------------------------------------------------- if finite s > P (fold f s a0) > > > Both rules (modulo my typos) should be provable by induction over the > finite set s. > > -- > Peter > > > > On Di, 2013-02-19 at 16:01 +0100, John Wickerson wrote: >> Dear Isabelle, >> >> This question is directed at anybody familiar with the Finite_Set theory... >> >> http://isabelle.in.tum.de/library/HOL/Finite_Set.html >> >> ... in particular, the Finite_Set.fold functional. Consider the term >> >> Finite_Set.fold f s A >> >> Various lemmas (e.g. Finite_Set.comp_fun_commute.fold_image) require me to show that f satisfies the "comp_fun_commute" property, i.e. >> >> (1) f x o f y = f y o f x >> >> for all x and y. This is too strong a requirement for me. I can show that (1) holds for all x and y in A, but not for all x and y in general. Morally, I *should* only have to show that f commutes when given inputs drawn from A. >> >> It would be quite a bit of hassle for me to convert these lemmas to stronger versions. So I was wondering if anybody has come across this problem before, or knows how to easily strengthen these lemmas, or has any other advice on this topic? >> >> Thanks, >> john > > >

**Follow-Ups**:**Re: [isabelle] Finite_Set comp_fun_commute***From:*Lawrence Paulson

**References**:**[isabelle] Finite_Set comp_fun_commute***From:*John Wickerson

**Re: [isabelle] Finite_Set comp_fun_commute***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Finite_Set comp_fun_commute
- Next by Date: Re: [isabelle] Finite_Set comp_fun_commute
- Previous by Thread: Re: [isabelle] Finite_Set comp_fun_commute
- Next by Thread: Re: [isabelle] Finite_Set comp_fun_commute
- Cl-isabelle-users February 2013 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