Re: [isabelle] Finite_Set comp_fun_commute



Mm, yes, my mistake. The domain of f should be "g ` A" rather than just "A". So the theorem should be:

> lemma fold_image_stronger:
> assumes "⋀x y. ⟦ x ∈ g ` A ; y ∈ g ` 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"

I think *this* one is true ... (but how to prove it?)

Thanks,
john

On 19 Feb 2013, at 18:01, Lawrence Paulson wrote:

> Is your desired theorem true?
> 
> I would find it easier to believe if it also assumed "x : A" and "g ` A <= A".
> 
> Larry Paulson
> 
> 
> On 19 Feb 2013, at 16:43, John Wickerson <jpw48 at cam.ac.uk> wrote:
> 
>> 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
>>> 
>>> 
>>> 
>> 
>> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.