*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Ad-hoc-proving attributes*From*: Peter Lammich <lammich at in.tum.de>*Date*: Wed, 05 Nov 2014 15:18:53 +0100*In-reply-to*: <5459025E.1030208@in.tum.de>*References*: <5459025E.1030208@in.tum.de>

I would appreciate an attribute [[inductive_cases <term>]] instead of the command. -- Peter On Di, 2014-11-04 at 17:44 +0100, 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.

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

- Previous by Date: Re: [isabelle] Ad-hoc-proving attributes
- Next by Date: Re: [isabelle] AFP submission and smt2
- Previous by Thread: Re: [isabelle] Ad-hoc-proving attributes
- Next by Thread: [isabelle] Disproof methods with Word.thy and AutoCorres
- 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