*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 1 Nov 2012 12:03:54 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <5091CE53.6020006@cs.bham.ac.uk>*References*: <50916DB3.4030707@cs.bham.ac.uk> <B342CF2B-EEC3-4932-A98D-193702F57A14@cam.ac.uk> <5091CE53.6020006@cs.bham.ac.uk>

You should look at the documentation on the induct/induction proof methods. They achieve the effect of performing induction on a formula such as "\<forall>i::nat . P i \<longrightarrow> Q i" while completely hiding the tedious manipulations of these logical connectives that would normally be required. Larry Paulson On 1 Nov 2012, at 01:20, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote: > 2012-10-31 20:09 Lawrence Paulson: >> On 31 Oct 2012, at 18:28, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote: >>> * In statements such as "!x. p x --> q x" it is tedious (and always the same) to break their structure down to a level where the actually interesting work starts. >> >> It is almost never necessary or helpful to state a theorem in that format. > > Thanks for your advice! However simply changing my statements to … > >> I suggest >> >> lemma "p x ==> q x" >> >> for a straightforward proof, or >> >> lemma assumes "p x" shows "q x" >> >> for a more complicated structured proof. > > … such a structure doesn't always work; I think the proofs will also need some adaptation. > > The following lemma (reduced to the structural outline) has a (anti-)pattern that is typical for my formalisation: > > lemma skip_index_keeps_non_negativity : > fixes n::nat and v::real_vector > assumes non_empty: "n > 0" > and non_negative: "non_negative_real_vector n v" > shows "\<forall>i::nat . in_range n i \<longrightarrow> non_negative_real_vector (n-(1::nat)) (skip_index v i)" > proof > fix i::nat > show "in_range n i \<longrightarrow> non_negative_real_vector (n-(1::nat)) (skip_index v i)" > proof > assume "in_range n i" > ... > show "non_negative_real_vector (n-(1::nat)) (skip_index v i)" sorry > qed > qed > > How would I have to adapt the proof when rephrasing the statement as shows "in_range n i \<Longrightarrow> ..." ? > > (I'll be happy to accept "RTFM" as an answer, if you could give me a pointer.) > > Cheers, and thanks, > > Christoph > > -- > Christoph Lange, School of Computer Science, University of Birmingham > http://cs.bham.ac.uk/~langec, Skype duke4701 > > → Enabling Domain Experts to use Formalised Reasoning @ AISB 2013 > 2–5 April 2013, Exeter, UK. Deadlines 10 Dec (stage 1), 14 Jan (st. 2) > http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] attribute: rule_format
- Next by Date: [isabelle] Type restrictions; document preparation [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Previous by Thread: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Thread: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Cl-isabelle-users November 2012 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