Re: [isabelle] Ad-hoc-proving attributes



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.






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