Stream: Beginner Questions

Topic: Do we have something like "simp once"/"unfolding once"?

Yiming Xu (Dec 14 2024 at 15:22):

For some iff thms generated from induction, it will obviously loop when we expend it, say:

height_le ?r ?Op ?R ?a1.0 ?a2.0 =
(?a1.0 = ?r ∧ ?a2.0 = 0 ∨
 (∃w n m vl v.
     ?a1.0 = v ∧ ?a2.0 = n + 1 ∧ height_le ?r ?Op ?R w n ∧ m ∈ ?Op ∧ ?R m (w # vl) ∧ v ∈ set vl))

Yiming Xu (Dec 14 2024 at 15:23):

But sometimes I would still want to expand it only once to see how the goal looks like. Is there anything that only apply the unfolding/rw only once?

Mathias Fleury (Dec 14 2024 at 15:57):

apply (subst ...) (possibly with position specification like subst (asm)(4)) or apply (rewrite ....)(possibly with rewrite at ... in ...)

Yiming Xu (Dec 14 2024 at 15:59):

Mathias Fleury said:

apply (subst ...) (possibly with position specification like subst (asm)(4)) or apply (rewrite ....)(possibly with rewrite at ... in ...)

subst works for me in the sense that

...
 then have hle_v_suc_n:"height_le r τ R v (n + 1)"
    apply (subst height_le.simps)

gives

 w ∈ generated_set τ R {r} ⟹
    v = r ∧ n + 1 = 0 ∨
    (∃w na m vl va.
        v = va ∧ n + 1 = na + 1 ∧ height_le r τ R w na ∧ m ∈ τ ∧ R m (w # vl) ∧ va ∈ set vl)

Yiming Xu (Dec 14 2024 at 16:00):

rewrite reports error

Undefined method: "rewrite"⌂

Yiming Xu (Dec 14 2024 at 16:00):

Oh maybe imports...

Mathias Fleury (Dec 14 2024 at 16:01):

yeah rewrite is somewhere

Mathias Fleury (Dec 14 2024 at 16:01):

https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL-ex/Rewrite_Examples.html

Yiming Xu (Dec 14 2024 at 16:01):

Great! Thanks!

Mathias Fleury (Dec 14 2024 at 16:02):

HOL-Library.Rewrite and the link is the tutorial

Yiming Xu (Dec 14 2024 at 16:03):

Nice to see it exists!

Last updated: Dec 21 2024 at 16:20 UTC