Re: [isabelle] Ad-hoc-proving attributes



Hi Lars,

I understand that your proposal is more general than the proof method ind_cases, but could you comment on how they relate to each other?

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.





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