*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Ad-hoc-proving attributes*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 04 Nov 2014 17:44:14 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

(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.

diff -r 447972249785 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Nov 03 15:08:15 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Nov 04 17:36:43 2014 +0100 @@ -991,7 +991,7 @@ val name = full_name ctxt b; val facts = Global_Theory.name_thmss false name raw_facts; fun app (ths, atts) = - fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; + apfst flat o fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; val (res, ctxt') = fold_map app facts ctxt; val thms = Global_Theory.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; diff -r 447972249785 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Mon Nov 03 15:08:15 2014 +0100 +++ b/src/Pure/global_theory.ML Tue Nov 04 17:36:43 2014 +0100 @@ -146,7 +146,7 @@ (* add_thms(s) *) fun add_thms_atts pre_name ((b, thms), atts) = - enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms); + enter_thms pre_name (name_thms false true) (apfst flat oo fold_map (Thm.theory_attributes atts)) (b, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -175,7 +175,7 @@ let val name = Sign.full_name thy b; fun app (ths, atts) = - fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; + apfst flat o fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; val (thms, thy') = enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app) (b, facts) thy; diff -r 447972249785 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Mon Nov 03 15:08:15 2014 +0100 +++ b/src/Pure/more_thm.ML Tue Nov 04 17:36:43 2014 +0100 @@ -12,7 +12,7 @@ structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool - type attribute = Context.generic * thm -> Context.generic option * thm option + type attribute = Context.generic * thm -> Context.generic option * thm list option end; signature THM = @@ -72,16 +72,16 @@ val add_axiom_global: binding * term -> theory -> (string * thm) * theory val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory - type attribute = Context.generic * thm -> Context.generic option * thm option + type attribute = Context.generic * thm -> Context.generic option * thm list option type binding = binding * attribute list val empty_binding: binding val rule_attribute: (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute - val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic + val apply_attribute: attribute -> thm -> Context.generic -> thm list * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic - val theory_attributes: attribute list -> thm -> theory -> thm * theory - val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context + val theory_attributes: attribute list -> thm -> theory -> thm list * theory + val proof_attributes: attribute list -> thm -> Proof.context -> thm list * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag_rule: string * string -> thm -> thm @@ -443,25 +443,27 @@ (** attributes **) (*attributes subsume any kind of rules or context modifiers*) -type attribute = Context.generic * thm -> Context.generic option * thm option; +type attribute = Context.generic * thm -> Context.generic option * thm list option; type binding = binding * attribute list; val empty_binding: binding = (Binding.empty, []); -fun rule_attribute f (x, th) = (NONE, SOME (f x th)); +fun rule_attribute f (x, th) = (NONE, SOME [f x th]); fun declaration_attribute f (x, th) = (SOME (f th x), NONE); -fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; +fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME [th']) end; fun apply_attribute (att: attribute) th x = - let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th)) - in (the_default th th', the_default x x') end; + let val (x', ths') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th)) + in (the_default [th] ths', the_default x x') end; fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let - fun app [] th x = (th, x) - | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; + fun app [] th x = ([th], x) + | app (att :: atts) th x = + let val (ths', x') = apply_attribute att th (mk x) ||> dest + in fold_map (app atts) ths' x' |>> flat end in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory;

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

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

**Re: [isabelle] Ad-hoc-proving attributes***From:*Peter Lammich

- Previous by Date: [isabelle] New Z3 dependency
- Next by Date: Re: [isabelle] Trouble with the Int Theory
- Previous by Thread: Re: [isabelle] Porting the Isabelle/HOL to a newer version
- 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