Re: [isabelle] "using [[...]]" with Isabelle/Eisbach or Isabelle/ML



Hi Christian,

The match method can be slightly abused to get the desired effect:

method my_simproc_env methods m =
  (match termI in H[simproc del: bad_simproc]:_ â âmâ)

Here the match against the âtermIâ fact only produces one result, which we name and then use as a handle for making our âsimproc del:â declaration.

We can then use this as a usual higher-order method:

apply (my_simproc_env âsimpâ)

However, it is relatively straightforward to write a method in ML that will accomplish this a bit more generically.

method_setup noting =
 âScan.lift (Parse.and_list1 Parse.xthms1  --| Args.$$$ "in") --  Method_Closure.method_text >> (fn (args, m) => fn ctxt =>
   let
     fun no_binding args = map (pair (Binding.empty, [])) args;

     val ctxt' = ctxt
       |> Proof_Context.note_thmss ""
        (Attrib.map_facts_refs (map (Attrib.attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) (no_binding args))
       |> snd

   in Method_Closure.method_evaluate m ctxt' end)
â

Which then looks a bit like the ânoteâ command:

   apply (noting [[simproc del: bad_simproc]]
            in âsimpâ)

Regards,
Dan



> On 23 Mar 2016, at 12:39 AM, Christian Sternagel <c.sternagel at gmail.com> wrote:
>
> Dear all,
>
> what is the equivalent to e.g.
>
> lemma "..."
>  ...
>  using [[simproc del: s]]
>  ...
>
> in Eisbach methods (or if that doesn't work with Isabelle/ML).
>
> cheers
>
> chris
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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