*To*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Annotations in Simpl*From*: Gerwin Klein <gerwin.klein at nicta.com.au>*Date*: Tue, 10 Jul 2012 09:09:03 +1000*In-reply-to*: <4FFB1C13.4090400@in.tum.de>*References*: <4FFB1C13.4090400@in.tum.de>

Hi Lars, On 10/07/2012, at 3:59 AM, Lars Noschinski wrote: > The only other solution I have found would be adding the invariants only in the proof: > > > procedures mult2 (n :: nat, m :: nat | r :: nat) > " > ´r :== (0 :: nat) ;; > WHILE ´n ≠ 0 > DO > ´r :== ´r + ´m ;; > ´n :== ´n - 1 > OD > " > > lemma (in mult2_impl) mult2: > "∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult2(´m, ´n) ⦃´r = m * n⦄" > apply vcg_step > apply (hoare_rule HoarePartial.Seq) > defer > apply (hoare_rule I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n ⦄" in > HoarePartial.reannotateWhileNoGuard) > apply vcg > apply (simp_all add: mult_Suc_right[symmetric]) > apply vcg > apply simp > done This is what we used for the kernel proof. It doesn't look nice and has the disadvantages you explain. It does have the advantage that you can pick different invariants/annotations for each proof about that function. Slight side rant: It's strange that Hoare logic insists that one would only ever prove one property about a function, have one invariant, and one annotation that fits them all. In theory this is all equivalent and there is a "complete specification", but in practise that is not how things are proved or should be proved. Just think about what we do for functional programs in Isabelle. Nothing is more cumbersome and useless than having to state one lemma that says everything about one function. From that point of view, I'm fairly convinced that annotations and invariants belong with the proof, not with the program (or everything belongs with the program). It would be nice to have a better notation for connecting them, though. Cheers, Gerwin

**Follow-Ups**:**Re: [isabelle] Annotations in Simpl***From:*Thomas Sewell

**Re: [isabelle] Annotations in Simpl***From:*John Wickerson

**Re: [isabelle] Annotations in Simpl***From:*Lukas Bulwahn

**References**:**[isabelle] Annotations in Simpl***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] HOLCF equality
- Next by Date: Re: [isabelle] I want to print axiomatization info
- Previous by Thread: [isabelle] Annotations in Simpl
- Next by Thread: Re: [isabelle] Annotations in Simpl
- Cl-isabelle-users July 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