Re: [isabelle] Finite_Set comp_fun_commute



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.