*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] stuck on proof*From*: Ian Lynagh <igloo at earth.li>*Date*: Thu, 19 Aug 2010 16:13:51 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4C6A4359.3090608@in.tum.de>*Mail-followup-to*: Tobias Nipkow <nipkow at in.tum.de>, isabelle-users at cl.cam.ac.uk*References*: <20100816161640.GB16241@matrix.chaos.earth.li> <4C6A4359.3090608@in.tum.de>*User-agent*: Mutt/1.5.18 (2008-05-17)

On Tue, Aug 17, 2010 at 10:07:53AM +0200, Tobias Nipkow wrote: > lemma "(principalType e = Some t) ==> (STyping e t)" > apply (induct e arbitrary: t) > apply (auto simp: STyping.intros split:option.splits SType.splits) > done > > split: ... instructs auto (or simp) to split case expressions for > certain types automatically. Thanks, but this isn't the sort of proof I'm hoping to end up with. My hope is to have a proof that a Haskell programmer can read, understand and ideally even adapt; i.e. I want a machine-checked proof, rather than a machine proof. For example, if I add an IfThenElse construct, then the proof now leaves me with an unsolved goal: goal (1 subgoal): 1. !!e1 e2 e3 t aa ab. [| !!t. TBool = t ==> STyping e1 TBool; !!t. aa = t ==> STyping e2 t; !!t. ab = t ==> STyping e3 t; principalType e1 = Some TBool; principalType e2 = Some aa; principalType e3 = Some ab; (if aa = ab then Some aa else None) = Some t |] ==> STyping (EIfThenElse e1 e2 e3) t for which the solution is not clear, because the proof is opaque to non-Isabellers. My understanding was that Isar is more like coq's C-zar (or more accurately, I guess, C-zar is like Isar). With C-zar I am optimistic that readable, and not /too/ verbose, proofs would be possible. Unfortunately, due to C-zar bugs, writing the proofs is not currently possible, and C-zar seems to be largely dead, but the beginning of a proof looks like this: Lemma typingIsPrincipalType : forall (e : SExpr) (t : SType) (typing : STyping e t), principalType e = Some t. proof. let e, t be such that typing : (STyping e t). per induction on typing. suppose it is (STypingBool b). hence thesis by principalType. suppose it is (STypingInt n). hence thesis by principalType. Thanks Ian

**Follow-Ups**:**Re: [isabelle] stuck on proof***From:*Makarius

**References**:**[isabelle] stuck on proof***From:*Ian Lynagh

**Re: [isabelle] stuck on proof***From:*Tobias Nipkow

- Previous by Date: [isabelle] Proving consistency
- Next by Date: Re: [isabelle] Proving consistency
- Previous by Thread: Re: [isabelle] stuck on proof
- Next by Thread: Re: [isabelle] stuck on proof
- Cl-isabelle-users August 2010 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