Re: [isabelle] Annotations in Simpl


On 10.07.2012 03:27, Thomas Sewell wrote:
You may not necessarily need to single-step the vcg. Have a look at
whileAnno_def: "whileAnno b I V c == While b c". Since this is full
equality, you can add or remove annotations with fold/unfold if this is
definition "name_loop v = UNIV"
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="..."])

thank you both for your answers! This renaming indeed provides a less fiddly solution (somehow I did not think about using the simplifier on Simpl programs ...).

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.