# Re: [isabelle] Annotations in Simpl

```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"
```
```[...]
```
```(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:

fun eqsubst_inst_tac ctxt occL insts thm =
Subgoal.FOCUS (fn {context=ctxt,...} => let
val thm' = thm |> Rule_Insts.read_instantiate ctxt insts
in EqSubst.eqsubst_tac ctxt occL [thm'] 1 end) ctxt

fun subst_method inst_tac tac =
Args.goal_spec --
Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
Scan.optional (Scan.lift
```
(Parse.and_list1 (Args.var -- (Args.\$\$\$ "=" |-- Parse.!!! Args.name_source)) --|
```        Args.\$\$\$ "in")) [] --
Attrib.thms >>
(fn (((quant, occL), insts), thms) => fn ctxt => METHOD (fn facts =>
```
if null insts then quant (Method.insert_tac facts THEN' tac ctxt occL thms)
```      else
(case thms of
```
[thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt occL insts thm)
```        | _ => error "Cannot have instantiations with multiple rules")));

val eqsubst_inst_meth = subst_method
eqsubst_inst_tac EqSubst.eqsubst_tac

So now I can do:

lemma (in mult3_impl) mult3:
"∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult3(´m, ´n) ⦃´r = m * n⦄"
apply vcg_step
apply (subst_tac I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n  ⦄" in
annotate_named_loop[where name="''mult3_loop''"])

```

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