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

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule
*From*: bnord <bnord01 at gmail.com>
*Date*: Wed, 31 Jul 2013 12:20:16 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:17.0) Gecko/20130620 Thunderbird/17.0.7

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.*