Inductive predicate with type parameters in Isabelle

Question

I started learning Isabelle and wanted to try defining a monoid in Isabelle but don't know how.

In Coq, I would do something like this:

Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop :=
| axioms: (forall (e: τ), op e i = e) ->
          (forall (e: τ), op i e = e) ->
          monoid τ op i.

I am not sure how to do the same thing in Isabelle. Conceptually I thought of something like this:

inductive 'a monoid "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦f e i = e; f i e = e⟧ ⇒ monoid f i"

But, that is not valid in Isabelle.

How do I define inductive predicates with typed parameters in Isabelle ?

Answer 1

I don't know much about Coq, but Isabelle's type system is very different. Isabelle values do not take ‘type parameters’, and Isabelle types do not take ‘value parameters’.

In Isabelle, your example is a simple polymorphic definition which can be done like this:

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦f e i = e; f i e = e⟧ ⟹ monoid f i"

I must point out that this means that if there exists even one e for which this holds, you have a monoid. What you probably meant to write is

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦⋀e. f e i = e; ⋀e. f i e = e⟧ ⟹ monoid f i"

Here, the e is universally quantified in the assumptions, meaning the laws must hold for all e in order to constitute a monoid.

Doing this as an inductive definition is possible and has the advantage of automatically generating appropriate introduction/elimination rules (and the ability to generate more with inductive_cases) There are, however, other ways.

Using a Definition

However, you could also write this as a simple definition:

definition monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" where
  "monoid f i = ((∀e. f e i = e) ∧ (∀e. f i e = e))"

This gives you the definition of monoid as the lemma monoid_def. If you want introduction/elimination rules, you have to derive them yourself.

Using a locale

The third, and probably most suitable solution is that of locales. A locale is a way of keeping certain fixed variables and assumptions in a context and reason within this context. The following example demonstrates how to define a monoid as a locale, derive lemmas in that locale, and then interpret the locale for a concrete example monoid (namely lists) and use the lemmas we proved in the locale for them.

locale monoid =
  fixes i :: 'a and f :: "'a ⇒ 'a ⇒ 'a"
  assumes left_neutral:  "f i e = e"
      and right_neutral: "f e i = e"
begin
  lemma neutral_unique_left:
    assumes "⋀e. f i' e = e"
    shows   "i' = i"
  proof-
    from right_neutral have "i' = f i' i" by simp
    also from assms have "f i' i = i" by simp
    finally show "i' = i" .
  qed
end

thm monoid.neutral_unique_left
(* Output: monoid i f ⟹ (⋀e. f i' e = e) ⟹ i' = i *)

(* Let's interpret our monoid for the type "'a list", with [] 
   as neutral element and concatenation (_ @ _) as the operation. *)
interpretation list_monoid: monoid "[]" "λxs ys. xs @ ys"
  by default simp_all

thm list_monoid.neutral_unique_left
(* Output: (⋀e. i' @ e = e) ⟹ i' = [] *)

Using a type class

A fourth possibility which is similar to locales it that of type classes. Isabelle supports type classes (like those in Haskell, albeit more restrictive), and you could create a monoid type class and then instantiate it for concrete types like nat, int, 'a list, etc.

More information

For more information on inductive predicates, locales, and type classes, see the documentation of these tools: http://isabelle.in.tum.de/documentation.html