# [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.