*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Generalized version of wf_map_prod_image*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 24 May 2018 09:20:09 +0200*In-reply-to*: <CADWNZtmthNAhmLkE_jaMMXGw8BZZ2dLF662tTExsZyfSiLpeBg@mail.gmail.com>*References*: <CADWNZtmthNAhmLkE_jaMMXGw8BZZ2dLF662tTExsZyfSiLpeBg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:52.0) Gecko/20100101 Thunderbird/52.8.0

A generalized version of the thm due to Andrei Popescu is in now: http://isabelle.in.tum.de/repos/isabelle/rev/80df7c90e315 Thanks to both of you. Tobias On 20/05/2018 12:12, Kasper F. Brandt wrote:

Hello list I wrote this generalization of wf_map_prod_image that only requires the mapping to be injective on the the subset present in the relation. lemma wf_map_prod_image': fixes r:: "('a × 'a) set" and f:: "'a ⇒ 'b" assumes wf_r: "wf r" and inj: "inj_on f (fst ` r ∪ snd ` r)" shows "wf (map_prod f f ` r)" unfolding wf_eq_minimal proof (clarify) fix Q::"'b set" and x::"'b" assume x_mem: "x ∈ Q" let "?Q'" = "{p. f p ∈ Q ∧ p ∈ (fst ` r ∪ snd ` r)}" show "∃z∈Q. ∀y. (y, z) ∈ map_prod f f ` r ⟶ y ∉ Q" proof (rule case_split) assume ex_fp_Q: "∃p. f p ∈ Q ∧ p ∈ (fst ` r ∪ snd ` r)" obtain z0 where z0_mem: "z0∈?Q'" and *: "∀y. (y, z0) ∈ r ⟶ y ∉ ?Q'" using ex_fp_Q wf_r[unfolded wf_eq_minimal, rule_format, of _ ?Q'] by blast have **: "⋀y z. (y,z) ∈ r ⟹ y ∈ (fst ` r ∪ snd ` r) ∧ z ∈ (fst ` r ∪ snd ` r) " by (metis Domain.intros Domain_fst Range.RangeI Range_snd Un_iff) have "∀y. (y, f z0) ∈ map_prod f f ` r ⟶ y ∉ Q" proof (intro allI impI) fix y assume "(y, f z0) ∈ map_prod f f ` r" then obtain y' and ya where y'_ya_def: "(y, f z0) = (f y', f ya)" and y'_ya_rel: "(y', ya) ∈ r" using prod_fun_imageE by blast have "f z0 ∈ Q ∧ z0 ∈ fst ` r ∪ snd ` r" using z0_mem by blast moreover have "f y' = y ∧ f ya = f z0" using y'_ya_def by fastforce ultimately have "ya = z0" using "**" y'_ya_rel inj inj_onD by metis then show "y ∉ Q" using "*" "**" Pair_inject y'_ya_def y'_ya_rel by blast qed then show "∃z∈Q. ∀y. (y, z) ∈ map_prod f f ` r ⟶ y ∉ Q" using z0_mem by blast next assume not_ex_fp_Q: "∄p. f p ∈ Q ∧ p ∈ (fst ` r ∪ snd ` r)" then have "⋀p . f p ∈ Q ⟹ p ∉ fst ` r ∧ p ∉ snd ` r" by blast then have "⋀z y. z ∈ Q ⟹ (y, z) ∉ map_prod f f ` r" by force then show ?thesis using x_mem by auto qed qed Would it make sense to add this to Wellfounded.thy, or replace the existing one? I'll note that this should follow from wf_map_prod_image by defining a type from the subset present in the relation, but I don't know Isabelle well enough to know how easy it is to prove this version from it. If nothing else this version is written in Isar style while wf_map_prod_image is currently in apply-script style (I haven't checked Isabelle 2018) - Kasper Fabæch Brandt

**Attachment:
smime.p7s**

**References**:**[isabelle] Generalized version of wf_map_prod_image***From:*Kasper F. Brandt

- Previous by Date: Re: [isabelle] isabelle doc - where to start?
- Next by Date: Re: [isabelle] code del and code drop
- Previous by Thread: Re: [isabelle] Generalized version of wf_map_prod_image
- Next by Thread: [isabelle] Formal Methods internship at Arm Research
- Cl-isabelle-users May 2018 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