Bad context for command "definition" - using reuse state · Beginner Questions

function apply_divisor_module_list ::
  "'a::linorder Result × 'b set StructVotes × ('a::linorder, 'b set) Seats ⇒
   'b set list ⇒ 'a::linorder set ⇒ ('a::linorder, 'b set) Seats ⇒
   'b set StructVotes ⇒ 'b set StructVotes ⇒ nat list ⇒
   ('a::linorder Result × 'b set StructVotes × ('a::linorder, 'b set) Seats) list" where
"apply_divisor_module_list input (party # parties) indexes seats votes fract_votes ps =
    (if party = {} then []
     else let res = fst (input);
              (result, new_fractvotes, new_seats) =
                  divisor_module res party indexes seats votes fract_votes ps
          in (result, new_fractvotes, new_seats) #
        apply_divisor_module_list (result, new_fractvotes, new_seats) parties indexes seats votes fract_votes ps)"

(* example *)
definition x :: "nat" where
"x = 3"

but i get the error "bad context for command "definition" - using reuse state". I am almost sure it's about syntax but how can I solve?

Manuel Eberl (Dec 13 2023 at 14:28):

There is a difference between fun and function. When you declare a function with function, you have to prove a bunch of things, namely that the function definition equations are exhaustive and non-overlapping. Usually, a combination of pat_completness and auto does the trick. When you use fun, this is done automatically.

Unlike fun, the function command also does not prove termination automatically. You have to manually do this, e.g. in most cases a termination by lexicographic_order does the trick. See the tutorial on the function package: https://isabelle.in.tum.de/dist/Isabelle2023/doc/functions.pdf

So the problem here is that after calling function, you are still in ‘proof mode’ because there is something you have to prove. However, you cannot usedefinition in proof mode. Hence the error.

Lukas Stevens (Dec 13 2023 at 14:40):

Salvatore Francesco Rossetta (Dec 13 2023 at 16:47):

I was using function because I think I read it was more general than fun. Indeed when changing now I only had this warning:

Missing patterns in function definition:
⋀a c d e f g. apply_divisor_module_list a [] c d e f g = undefined

Wolfgang Jeltsch (Dec 13 2023 at 17:25):

Yes, it is more general but therefore also more difficult to use. I always use the simplest tool possible. In the order of complexity, the usual tools for defining functions are definition, primrec, fun, and function.

Yong Kiam (Dec 14 2023 at 04:53):

Mathias Fleury (Dec 14 2023 at 05:51):

primrec is like fun (recursive functions), but only for primitive recursion: the patterns must exactly the constructors of the datatype. For example this:

primrec fib where
‹fib 0 = 0› |
‹fib (Suc 1) = 1›

Mathias Fleury (Dec 14 2023 at 05:52):

primrec is simpler and does not generate a new inductive principle (because it is identical to the default one from the type)

Manuel Eberl (Dec 14 2023 at 08:40):

primrec also works better in places where you have to prove something about the function automatically, such as that it is measurable, or proving a transfer rule. Because you can simply once and for all prove measurability of the primitive recursion operator, or a transfer rule for the primitive recursion operator.

Stream: Beginner Questions

Topic: Bad context for command "definition" - using reuse state

Salvatore Francesco Rossetta (Dec 13 2023 at 14:12):