[isabelle] Ad-hoc-proving attributes



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


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