*To*: Lars Hupel <hupel at in.tum.de>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Ad-hoc-proving attributes*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 5 Nov 2014 08:06:31 +0100*In-reply-to*: <5459025E.1030208@in.tum.de>*References*: <5459025E.1030208@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

Hi Lars,

Andreas On 04/11/14 17:44, Lars Hupel wrote:

(My apologies for the somewhat mysterious subject line.) I was wondering whether it'd make sense to unify the mechanisms behind "inductive_cases", "inductive_simps", "fun_cases" etc.; namely, commands which prove some theorems on the spot, but apart from binding them to a name, have no further side effects on the theory. My main motivation for this is that, sometimes, I need "ad hoc" elimination rules, and since "inductive_cases" doesn't work in proof blocks, I end up with the rather awkward pattern of declaring them outside the proof and hiding them afterwards again. My initial thought was to make a variant of the command which works in a proof block (c.f. "lemmas" vs "note", "interpretation" vs "interpret"), but if Isabelle/HOL doesn't need more of one things, it's keywords. So, here's my proposal: Instead of an "inductive_cases" command, have an "inductive_cases" attribute. It could be used like this: lemmas fooE[elim] = [[inductive_cases "R (T x) (T y)"]] or this: then have "R a b" using [[inductive_cases "R (T x) (T y)"]] This would already work out of the box by declaring a "rule_attribute" which ignores its incoming "thm" argument. Is that something people would be interested in? (NB: What follows are some technical details which would probably belong to [isabelle-dev], but I don't want to split this thread.) Cheers Lars ---------------------------------------------------------------------- Making my case for "inductive_cases" is easy, because I could implement it with the existing tools, because it always proves a single theorem. If we want to be fully general though, it gets more complicated, because the current "attribute" mechanism doesn't allow to return more than one theorem. Looking at how attributes are implemented, I found this: type attribute = Context.generic * thm -> Context.generic option * thm option Modifying this to return a "thm list option" would certainly allow multiple theorems. To make it easy to use, one could create a new "smart constructor" for that type, e.g. val ad_hoc_proof_attribute: (Context.generic -> thm list) -> attribute which leaves the incoming context untouched and ignores the incoming theorem. I couldn't predict what more needed to be changed, so I decided to "apply some pressure and see what starts wobbling". I changed the type in "more_thm.ML". Then, the tricky bit is "apply_attributes", which is in some way a glorified fold left over a list of attributes. There, I ran into a problem: suppose we have thm _[inductive_cases "...", simp] In this case, the first part of the attribute sequence might produce more than theorem, which means that the second part needs to be applied to all of them. Peter pointed out to me that we already have precendent for that: thm foo.intros[simp] ... works in exactly the same way: "simp" is applied to all theorems in "foo.intros" (this is handled in "Isar/attrib.ML"). However, so far the full "attribute pipeline" only transformed one pair of theorem and context into another pair of theorem and context, and now it would need to deal with potentially multiple and traverse them in some manner (Depth first? Breadth first? That choice matters for non-commutative attributes, e.g. [simp, simplified]). I have attached a patch which _only_ attempts to change the definition in "more_thm.ML" and fix what breaks in "global_theory.ML" and "Isar/proof_context.ML" (in both files only minor changes were needed). A bit more thought is required for "Isar/attrib.ML", where I aborted my exploration.

**Follow-Ups**:**Re: [isabelle] Ad-hoc-proving attributes***From:*Lars Hupel

**References**:**[isabelle] Ad-hoc-proving attributes***From:*Lars Hupel

- Previous by Date: Re: [isabelle] reusable proofs
- Next by Date: Re: [isabelle] Disproof methods with Word.thy and AutoCorres
- Previous by Thread: [isabelle] Ad-hoc-proving attributes
- Next by Thread: Re: [isabelle] Ad-hoc-proving attributes
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list