Re: [isabelle] Generalized version of wf_map_prod_image

Thanks for the input. It looks helpful and I will take care of it.


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
     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
     then show "∃z∈Q. ∀y. (y, z) ∈ map_prod f f ` r ⟶ y ∉ Q"
       using z0_mem by blast
     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

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
Description: S/MIME Cryptographic Signature

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