*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Finite_Set comp_fun_commute*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 20 Feb 2013 12:58:34 +0100*In-reply-to*: <17A819D4-0C30-4CA9-BB83-B2D673469A5D@cam.ac.uk>*References*: <ACB40174-AB28-4980-85BB-DC77A6D13891@cam.ac.uk> <1361288296.2373.95.camel@lapbroy33> <E1C14B0C-0621-40AF-82E5-6F4BC51F1608@cam.ac.uk> <DB0F6D65-766E-42F2-AB00-56F676C009D4@cam.ac.uk> <F685D69A-6C4C-4198-97D4-379229A677A1@cam.ac.uk> <1361320203.2658.9.camel@lapbroy33> <867C4AB2-C21C-44A6-99D3-D4867974587B@cam.ac.uk> <17A819D4-0C30-4CA9-BB83-B2D673469A5D@cam.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130216 Thunderbird/17.0.3

I have that on my radar. Tobias Am 20/02/2013 12:40, schrieb John Wickerson: > Just a thought: since "fold_image_even_stronger" needs only a subset of the assumptions needed by "Finite_Set.fold_image", perhaps your new theorem should replace the one in the HOL library? > > john > > On 20 Feb 2013, at 09:10, John Wickerson wrote: > >> Awesome! Thanks so much Peter, that's really kind of you. >> >> John >> >> >> On 20 Feb 2013, at 01:30, Peter Lammich wrote: >> >>> Hi John. >>> >>> Sorry for the confusion with the invariant rules. They hold (if the >>> property P admits only one result) but are probably not very useful to >>> prove your stronger fold_image rule. >>> >>> To prove that (even a stronger one) you can exploit the fact that the >>> definition of fold does not depend on this strange locale with too >>> strong assumptions, but on an inductively defined predicate fold_graph, >>> that contains the results of all possible fold orderings. >>> >>> Here is the proof of your fold_image_stronger, but you do not need the >>> first two assumptions at all! >>> Please excuse the aux-lemmas and the not very elaborated proofs: >>> >>> theorem fold_image_even_stronger: >>> assumes I: "inj_on g A" >>> shows "Finite_Set.fold f x (g`A) = Finite_Set.fold (f o g) x A" >>> oops (*Proof comes below, first need to show some aux-lemmas *) >>> >>> >>> lemma inj_img_insertE: >>> assumes I: "inj_on f s" >>> assumes N: "x\<notin>r" >>> assumes E: "insert x r = f`s" >>> obtains x' s' where "s=insert x' s'" and "x'\<notin>s'" >>> and "x = f x'" and "r = f`s'" >>> proof - >>> from E have "x\<in>f`s" by auto >>> then obtain x' where "x'\<in>s" and "x = f x'" by auto >>> hence "s = insert x' (s - {x'})" by auto >>> have "r = f`(s - {x'})" apply auto >>> apply (metis (no_types) Diff_insert_absorb E I N >>> `s = insert x' (s - {x'})` `x = f x'` image_insert inj_on_insert >>> insertI1 insert_Diff1) >>> by (metis E I `x = f x'` `x' \<in> s` imageI inj_on_contraD insertE) >>> show ?thesis >>> apply rule >>> apply fact >>> apply simp >>> apply fact+ >>> done >>> qed >>> >>> lemma fold_graph_image: >>> "inj_on g s \<Longrightarrow> fold_graph f a (g`s) r >>> \<longleftrightarrow> fold_graph (f o g) a s r" >>> proof >>> case goal1 >>> from goal1(2,1) show ?case >>> proof (induct "g`s" r arbitrary: s rule: fold_graph.induct) >>> case emptyI thus ?case by (auto intro: fold_graph.emptyI) >>> next >>> case (insertI x A r s) >>> with inj_img_insertE obtain x' A' where >>> "x'\<notin>A'" and [simp]: "s = insert x' A'" "x = g x'" "A=g`A'" >>> by metis >>> with insertI.hyps(3)[of A'] insertI.prems >>> have FG: "fold_graph (f o g) a A' r" >>> by auto >>> from fold_graph.insertI[OF `x'\<notin>A'` FG] >>> show ?case by simp >>> qed >>> next >>> case goal2 >>> from goal2(2,1) show ?case >>> proof (induct rule: fold_graph.induct) >>> case emptyI thus ?case by (auto intro: fold_graph.emptyI) >>> next >>> case (insertI x A r) >>> hence FG: "fold_graph f a (g`A) r" by simp >>> from `x\<notin>A` insertI.prems have N: "g x \<notin> g`A" by auto >>> from fold_graph.insertI[OF N FG] show ?case by simp >>> qed >>> qed >>> >>> lemma fold_graph_image': >>> "inj_on g s \<Longrightarrow> fold_graph f a (g`s) = fold_graph (f o >>> g) a s" >>> by (rule ext) (rule fold_graph_image) >>> >>> theorem fold_image_even_stronger: >>> assumes I: "inj_on g A" >>> shows "Finite_Set.fold f x (g`A) = Finite_Set.fold (f o g) x A" >>> unfolding Finite_Set.fold_def >>> by (simp add: fold_graph_image'[OF I, of f x]) >>> >>> >>> Best, >>> Peter >>> >>> >>> On Di, 2013-02-19 at 19:34 +0100, John Wickerson wrote: >>>> 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 >>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> >>>>> >>>> >>> >>> >>> >> >> >

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

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

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

**Re: [isabelle] Finite_Set comp_fun_commute***From:*Lawrence Paulson

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

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

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

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

- Previous by Date: Re: [isabelle] Propositions: value vs lemma
- Next by Date: Re: [isabelle] Propositions: value vs lemma
- Previous by Thread: Re: [isabelle] Finite_Set comp_fun_commute
- Next by Thread: [isabelle] Participate: Enabling Domain Experts to use Formalised Reasoning (AISB 2013, Exeter, UK, 3-5 Apr 2013). Tutorials on Matching, Auctions, Finance.
- 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