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



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.