*To*: bnord <bnord01 at gmail.com>*Subject*: Re: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 31 Jul 2013 13:39:52 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <51F8E4E0.8090202@gmail.com>*References*: <51F8E4E0.8090202@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

Hi Benedikt,

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

**References**:

- Previous by Date: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule
- Next by Date: Re: [isabelle] Replacing COMP
- Previous by Thread: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list