Re: [isabelle] Annotations in Simpl



On 10.07.2012 13:24, Lars Noschinski wrote:
On 10.07.2012 10:06, Lars Noschinski wrote:
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
...).

It turns out that this is fairly easy to implement:
[...]

I've refined this now to a specialized tactic, so I can just write

  apply (anno_loop_tac my_named_loop="{...}").

Now this aspect feels quite natural.

  -- Lars





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