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"
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:

  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.