Re: [isabelle] Annotations in Simpl



On 10.07.2012 09:49, Lars Noschinski wrote:
[...]
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 ...).

Actually, this fails if the invariant needs to meta-quantified variables -- I don't think we have a substitution variant of (rule_tac x=... in ...).

  -- Lars





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