Add `example` as an Isar synonym for `lemma`

Question

In my Isabelle/HOL theories, I like using unnamed lemmas as examples.

Here is an example how some of my theories look like.

definition foo_function :: "nat ⇒ nat" where "foo_function x = x+1"

text‹Example:›
lemma "foo_function 3 = 4" by eval

I feel the whole theory would read much nicer if I have an example keyword, which is basically equivalent to an unnamed lemma. Here is what I would like to write:

definition foo_function :: "nat ⇒ nat" where "foo_function x = x+1"

example "foo_function 3 = 4" by eval

Is there a super simple and stable way to set this up?

Answer 1

Control-click on lemma (besides proofs, this is the most important feature in Isabelle. Really. You can control-click on nearly everything to understand how it is defined) and copy-pasting the setup:

theory Scratch
  imports Main
  keywords "example" :: thy_goal_stmt
begin

ML ‹

local

val long_keyword =
  Parse_Spec.includes >> K "" ||
  Parse_Spec.long_statement_keyword;

val long_statement =
  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
  Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));

val short_statement =
  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
    >> (fn ((shows, assumes), fixes) =>
      (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
        Element.Shows shows));

fun theorem spec schematic descr =
  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
    ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
        long Thm.theoremK NONE (K I) binding includes elems concl)));
val _ = theorem \<^command_keyword>‹example› false "example";
in end
›
example True
  by eval
end