\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Group Theory - HOL Light

Table of Contents

1. Implementation

I'm just tracing out the implementation details. We find: 

let group_tybij =
  let eth = prove
   (`?s (z:A) n a.
          z IN s /\
          (!x. x IN s ==> n x IN s) /\
          (!x y. x IN s /\ y IN s ==> a x y IN s) /\
          (!x y z. x IN s /\ y IN s /\ z IN s
                   ==> a x (a y z) = a (a x y) z) /\
          (!x. x IN s ==> a z x = x /\ a x z = x) /\
          (!x. x IN s ==> a (n x) x = z /\ a x (n x) = z)`,
    MAP_EVERY EXISTS_TAC
     [`{ARB:A}`; `ARB:A`; `(\x. ARB):A->A`; `(\x y. ARB):A->A->A`] THEN
    REWRITE_TAC[IN_SING] THEN MESON_TAC[]) in
  new_type_definition "group" ("group","group_operations")
   (GEN_REWRITE_RULE DEPTH_CONV [EXISTS_UNPAIR_THM] eth);;

This defines "group" and "group_operations".

Let us analyze what-in-Heaven's-name is going on here. The proposition, if translated into logic, states \(\exists s\exists z{:}A\exists n\exists a.(\dots)\) where \(s\) is the set underlying the group, \(z{:}A\) is the identity element, \(n\) is the group inverse operator, and \(a\) is the law of composition. The axioms they satisfy are:

  1. \(z\in s\) (the identity element belongs to the underlying set)
  2. \(\forall x, x\in s\implies n(x)\in s\) (every element \(x\in s\) belonging to the underlying set also has its inverse element \(n x\) be a member of \(s\))
  3. \(\forall x\forall y, x\in s\land y\in s\implies a(x,y)\in s\) (the law of composition maps any \(x,y\in s\) to an element \(a(x,y)\in s\))
  4. \(\forall x\forall y\forall z, x\in s\land y\in s\land z\in s\implies a(x, a(y,z)) = a(a(x,y),z)\) (associativity of the law of composition)
  5. \(\forall x, x\in s\implies [a(z,x)=x\land a(x,z)=x]\) (the left and right unit laws for the identity element)
  6. \(\forall x, x\in s\implies [a(n(x),x)=z\land a(x,n(x))=z]\) (the inverse element satisfies the obvious property)

Also, the IN predicate is implemented as: 

let IN = new_definition
  `!P:A->bool. !x. x IN P <=> P x`;;

That is to say, a set is just a predicate, so membership IN a set amounts to satisfying the underlying predicate.

1.1. Where is new_type_definition defined?

In class.ml, we find the implementation of new_type_definition as: 

let the_type_definitions = ref ([]:((string*string*string)*(thm*thm))list);;

let new_type_definition tyname (absname,repname) th =
  try let th',tth' = assoc (tyname,absname,repname) (!the_type_definitions) in
      if concl th' <> concl th then failwith "" else
      (warn true "Benign redefinition of type"; tth')
  with Failure _ ->
    let th0 =
     CONV_RULE (RATOR_CONV (REWR_CONV EXISTS_THM) THENC BETA_CONV) th in
    let th1,th2 = new_basic_type_definition tyname (absname,repname) th0 in
    let tth = CONJ (GEN_ALL th1)
                   (GEN_ALL (CONV_RULE(LAND_CONV (TRY_CONV BETA_CONV)) th2)) in
    the_type_definitions := ((tyname,absname,repname),(th,tth))::
                            (!the_type_definitions);
    tth;;

See also: Rob Arthan's On Definitions of Constants and Types in HOL.

2. References

Last Updated 2022-02-04 Fri 09:11.