*To*: Ian Lynagh <igloo at earth.li>*Subject*: Re: [isabelle] stuck on proof*From*: Makarius <makarius at sketis.net>*Date*: Fri, 20 Aug 2010 15:10:30 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20100819151351.GA11077@matrix.chaos.earth.li>*References*: <20100816161640.GB16241@matrix.chaos.earth.li> <4C6A4359.3090608@in.tum.de> <20100819151351.GA11077@matrix.chaos.earth.li>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Thu, 19 Aug 2010, Ian Lynagh wrote:

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 IfThenElseconstruct, then the proof now leaves me with an unsolved goal:

In the attached Simple.thy there are 3 Isar proofs of increasing detail.

lemma "principalType e = Some t ==> STyping e t" by (induct e arbitrary: t) (auto simp: STyping.intros split: option.splits SType.splits)

lemma "principalType e = Some t ==> STyping e t" proof (induct e arbitrary: t) case (EBool b) then show ?case by (simp add: STyping.intros) next case (EInt n) then show ?case by (simp add: STyping.intros) next case (EGreaterThan lhs rhs) then show ?case by (auto simp: STyping.intros split: option.splits SType.splits) qed The last version expands on the induction cases a little: lemma "principalType e = Some t ==> STyping e t" proof (induct e arbitrary: t) case (EBool b) then have "t = TBool" by simp also have "STyping (EBool b) TBool" .. finally show "STyping (EBool b) t" . next case (EInt n) then have "t = TInt" by simp also have "STyping (EInt n) TInt" .. finally show "STyping (EInt n) t" . next case (EGreaterThan lhs rhs) have *: "principalType (EGreaterThan lhs rhs) = Some t" by fact show "STyping (EGreaterThan lhs rhs) t" proof (cases t) case TBool have "STyping lhs TInt" proof (rule EGreaterThan.hyps) from TBool and * show "principalType lhs = Some TInt" by (simp split: option.splits SType.splits) qed moreover have "STyping rhs TInt" proof (rule EGreaterThan.hyps) from TBool and * show "principalType rhs = Some TInt" by (simp split: option.splits SType.splits) qed ultimately have "STyping (EGreaterThan lhs rhs) TBool" .. then show ?thesis by (simp only: TBool) next case TInt with * have False by (simp split: option.splits SType.splits) then show ?thesis .. qed qed

thm r1 [OF t2] or experiment with the effect of simplification, e.g. from my_facts have XXX apply simp

from my_facts have my_prop by simp

My understanding was that Isar is more like coq's C-zar (or moreaccurately, I guess, C-zar is like Isar). With C-zar I am optimisticthat readable, and not /too/ verbose, proofs would be possible.Unfortunately, due to C-zar bugs, writing the proofs is not currentlypossible, and C-zar seems to be largely dead, ...

Makarius

(* :encoding=utf-8: *) theory Simple imports Main begin datatype SExpr = EBool bool | EInt int | EGreaterThan SExpr SExpr datatype SType = TBool | TInt inductive STyping :: "SExpr => SType => bool" where STypingBool: "STyping (EBool b) TBool" | STypingInt: "STyping (EInt n) TInt" | STypingGreaterThan: "STyping lhs TInt \<Longrightarrow> STyping rhs TInt \<Longrightarrow> STyping (EGreaterThan lhs rhs) TBool" fun principalType :: "SExpr => SType option" where "principalType (EBool b) = Some TBool" | "principalType (EInt n) = Some TInt" | "principalType (EGreaterThan lhs rhs) = (case (principalType lhs, principalType rhs) of (Some TInt, Some TInt) => Some TBool | _ => None)" lemma "principalType e = Some t ==> STyping e t" by (induct e arbitrary: t) (auto simp: STyping.intros split: option.splits SType.splits) lemma "principalType e = Some t ==> STyping e t" proof (induct e arbitrary: t) case (EBool b) then show ?case by (simp add: STyping.intros) next case (EInt n) then show ?case by (simp add: STyping.intros) next case (EGreaterThan lhs rhs) then show ?case by (auto simp: STyping.intros split: option.splits SType.splits) qed lemma "principalType e = Some t ==> STyping e t" proof (induct e arbitrary: t) case (EBool b) then have "t = TBool" by simp also have "STyping (EBool b) TBool" .. finally show "STyping (EBool b) t" . next case (EInt n) then have "t = TInt" by simp also have "STyping (EInt n) TInt" .. finally show "STyping (EInt n) t" . next case (EGreaterThan lhs rhs) have *: "principalType (EGreaterThan lhs rhs) = Some t" by fact show "STyping (EGreaterThan lhs rhs) t" proof (cases t) case TBool have "STyping lhs TInt" proof (rule EGreaterThan.hyps) from TBool and * show "principalType lhs = Some TInt" by (simp split: option.splits SType.splits) qed moreover have "STyping rhs TInt" proof (rule EGreaterThan.hyps) from TBool and * show "principalType rhs = Some TInt" by (simp split: option.splits SType.splits) qed ultimately have "STyping (EGreaterThan lhs rhs) TBool" .. then show ?thesis by (simp only: TBool) next case TInt with * have False by (simp split: option.splits SType.splits) then show ?thesis .. qed qed end

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

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

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

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

- Previous by Date: Re: [isabelle] How to use setsum for set addition?
- Next by Date: [isabelle] obtains forgets consumes and case_names in locales
- 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