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

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

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

**Re: [isabelle] Ad-hoc-proving attributes***From:*Andreas Lochbihler

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