Yiming Xu (Dec 10 2024 at 19:37): Yiming Xu (Dec 10 2024 at 19:37):I encounter something massive like this
x ∈ (λ(v, f, w). w) `
({w |w. nth_world M r s cwl n w} ×
s ×
⋃ (set `
uncurry cwl `
(s ×
{w |w. nth_world M r s cwl n w})))
My aim is to convert this to a predicate on x. What would mature users' attack on this?
Yiming Xu (Dec 10 2024 at 19:40):My way to do it in HOL4 would be simplifying with the definition of Image, uncurrying and products. I naively tried some unfolding, and got this:
x ∈ (λ(v, f, w). w) `
({w |w. nth_world M r s cwl n w} ×
s ×
⋃ (set `
(λpair.
cwl (fst pair) (snd pair)) `
(s ×
{w |w. nth_world M r s cwl n w})))
Note the \lambda pair. .... Is there something to do to tell Isabelle to split the pair?
Mathias Fleury (Dec 10 2024 at 19:46):apply (auto simp: image_iff)
Yiming Xu (Dec 10 2024 at 19:53):Thanks! It works perfectly, and my proof now look like this:
...
then show "x ∈ (λ(v, f, w). w) `
({w |w. nth_world M r s cwl n w} ×
s ×
⋃ (set `
uncurry cwl `
(s ×
{w |w.
nth_world M r s cwl n w})))"
unfolding
mem_Sigma_iff mem_Collect_eq uncurry_def
Bex_def bex_triv UN_iff image_iff
apply (auto simp: image_iff )
using xw by blast
I am a bit overwhelmed how to turn it into Isar. I will try a bit...
Mathias Fleury (Dec 10 2024 at 19:54):my intuition says that show ... using xw by (fastforce simp: image_iff) should work (or maybe force), making it possible to write all that in one line
Yiming Xu (Dec 10 2024 at 19:56):So what do you know about "fastforce" and "force" that helps you to make this conjecture?
Mathias Fleury (Dec 10 2024 at 19:56):fastforce and force try harder than auto
Mathias Fleury (Dec 10 2024 at 19:57):so usually auto + blast can be combined in one step of fastforce or force
Yiming Xu (Dec 10 2024 at 19:57):sledgehammer(add: mem_Sigma_iff mem_Collect_eq uncurry_def
Bex_def bex_triv UN_iff image_iff xw) fails.
Mathias Fleury (Dec 10 2024 at 19:57):Yeah but rewriting using the simplifier is not exactly sledgehammer strength.
Yiming Xu (Dec 10 2024 at 19:58):Mathias Fleury said:
so usually auto + blast can be combined in one step of fastforce or force
Thanks! That is good to know.
FYI this time both of them does not work this time.
Mathias Fleury (Dec 10 2024 at 19:58):Sad :frown:
Mathias Fleury (Dec 10 2024 at 19:58):but happens
Yiming Xu (Dec 10 2024 at 19:59):Mathias Fleury said:
Yeah but rewriting using the simplifier is not exactly sledgehammer strength.
I am in the era that sledgehammer is already there, so I hardly know anything about apply style yet. That is why I do not even know what to try.
Yiming Xu (Dec 10 2024 at 19:59):I will try to chop the goal into smaller pieces...
Last updated: Dec 21 2024 at 16:20 UTC