Re: [isabelle] Annotations in Simpl



On 14/07/2012, at 1:41 AM, Lars Noschinski wrote:

> 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.

That does indeed look quite nice. Would you be happy to include your tactic in the AFP Simpl entry?

Gerwin




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