Re: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule



Hi Benedikt,

"case splitting" is a too general term here, because only tuples of fixed variables are expanded to their components. You can achieve the same effect by unfolding with split_paired_all:

lemma "P (while b c (x,y))"
proof(rule while_rule, unfold split_paired_all)

Hope this helps,
Andreas

On 31/07/13 12:20, bnord wrote:
Hi there,

when one has a polymorphic proof rule what is the preferred way to do 'case splitting' on
the concrete type when using it for an Isar proof?

Example with while_rule from HOL/Library/While_Combinator:

lemma "P (while b c (x,y))" proof(rule while_rule)   yields
goal (5 subgoals):
1. ?P (x, y)
2. ⋀s. ?P s ⟹ b s ⟹ ?P (c s)
3. ⋀s. ?P s ⟹ ¬ b s ⟹ P s
4. wf ?r
5. ⋀s. ?P s ⟹ b s ⟹ (c s, s) ∈ ?r

Which requires one to do unwrap and wrap 's' four times.

lemma "P (while b c (x,y))" proof(rule while_rule,safe)   yields the /more desirable/
goal (5 subgoals):
1. ?P (x, y)
2. ⋀a ba. ?P (a, ba) ⟹ b (a, ba) ⟹ ?P (c (a, ba))
3. ⋀a ba. ?P (a, ba) ⟹ ¬ b (a, ba) ⟹ P (a, ba)
4. wf ?r
5. ⋀a ba. ?P (a, ba) ⟹ b (a, ba) ⟹ (c (a, ba), a, ba) ∈ ?r

But I feel bad about starting an Isar proof with an automatic method.

What is the best way to achieve something similar? Is it necessary to write a new proof rule?

Best
Benedikt





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