Re: [isabelle] Ad-hoc-proving attributes



Hi,

> 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?

I actually didn't know about that proof method, but it looks similar.
The difference is that I would actually need to spell out the rule I
want, and then continue to prove it with that method. With my proposal,
you just get the theorem generated on the spot, without having to spell
it out. It's very nice in proofs where you obtain variables. From my
current work:

obtain x1 x2
  where "x = x1 $ x2"
    and "rs, compile rs ⊢ x1 ≈ t1"
    and "rs, compile rs ⊢ x2 ≈ t2"
  by (auto elim: [[summon_ind_cases "rs, compile rs ⊢ x ≈ t1 $$ t2"]])

I could have expressed that equally well with

inductive_cases need_to_make_up_a_name: "rs, compile rs ..."

lemma ...
proof ...


  obtain ...
    by (auto elim: ...)

qed

hide_fact ...

The reason why I prefer an attribute over a command is that I don't need
to make up a name for something which only makes sense in the context of
a particular proof. Here, the "compile rs" is an artifact from the lemma
I'm proving. Another reason is that I think attributes are vastly
underrated – as opposed to commands, they can be used uniformly in a lot
of different situations.

I have attached a working example of that "summon_ind_cases" attribute.
(As an aside, I realize that my handling of variables is not canonical
here; presumably, I need to parse "for" fixes as well. Grepping the
sources for occurrences of "Parse.for_fixes" didn't reveal any canonical
use cases, though.)

Cheers
Lars
theory Summon
imports Main
begin

attribute_setup summon_ind_cases = \<open>Args.prop >>
  (fn t => Thm.rule_attribute (fn context => fn _ => Inductive.mk_cases (Context.proof_of context) t))
\<close> "Proves an ad-hoc instance of an elimination rule"

attribute_setup summon_fun_cases = \<open>Args.prop >>
  (fn t => Thm.rule_attribute (fn context => fn _ => Fun_Cases.mk_fun_cases (Context.proof_of context) t))
\<close> "Proves an ad-hoc instance of an elimination rule"

subsection "Examples"

thm [[summon_ind_cases "sorted (x # xs)"]]
thm [[summon_fun_cases "splice [] xs = []"]]

end


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