*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Annotations in Simpl*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Tue, 10 Jul 2012 11:27:45 +1000*In-reply-to*: <A7D5435C-E30C-46E4-BA36-ABCF5C4B515D@nicta.com.au>*References*: <4FFB1C13.4090400@in.tum.de> <A7D5435C-E30C-46E4-BA36-ABCF5C4B515D@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1

Hi Lars.

definition "name_loop v = UNIV" (in proc defn): " WHILE ´n ≠ 0 INV name_loop ''foo'' DO ... OD " lemma annotate_named_loop: "whileAnno b (name_loop v) V c = whileAnno b I V c" by (simp add: whileAnno_def) (in unfolding) apply (simp add: annotate_named_loop[where name="''foo''" and I="..."]) Not a lot nicer, but maybe a bit less fiddly.

Yours, Thomas. On 10/07/12 09:09, Gerwin Klein wrote:

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 doneThis 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:*Lars Noschinski

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

**Re: [isabelle] Annotations in Simpl***From:*Gerwin Klein

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