monotonicity_theorems : thm list ref

SYNOPSIS

List of monotonicity theorems for inductive definitions package.

DESCRIPTION

The various tools for making inductive definitions, such as new_inductive_definition, need to prove certain `monotonicity' side-conditions. They attempt to do so automatically by using various pre-proved theorems asserting the monotonicity of certain operators. Normally, all this happens smoothly without user intervention, but if the inductive definition involves new operators, you may need to augment this list with corresponding monotonicity theorems.

FAILURE CONDITIONS

Not applicable.

EXAMPLE

Suppose we define a `lexical order' construct:

  # let LEX = define
     `(LEX(<<) [] l <=> F) /\
      (LEX(<<) l [] <=> F) /\
      (LEX(<<) (CONS h1 t1) (CONS h2 t2) <=>
            if h1 << h2 then LENGTH t1 = LENGTH t2
            else (h1 = h2) /\ LEX(<<) t1 t2)`;;

If we want to make an inductive definition that uses this --- for example a lexicographic path order on a representation of first-order terms --- we need to add a theorem asserting that this operation is monotonic. To prove it, we first establish a lemma:

  # let LEX_LENGTH = prove
     (`!l1 l2 R. LEX(R) l1 l2 ==> (LENGTH l1 = LENGTH l2)`,
      REPEAT(LIST_INDUCT_TAC THEN SIMP_TAC[LEX]) THEN ASM_MESON_TAC[LENGTH]);;

and hence derive monotonicity:

  # let MONO_LEX = prove
     (`(!x:A y:A. R x y ==> S x y) ==> LEX R x y ==> LEX S x y`,
      DISCH_TAC THEN
      MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`x:A list`; `y:A list`] THEN
      REPEAT(LIST_INDUCT_TAC THEN REWRITE_TAC[LEX]) THEN
      ASM_MESON_TAC[LEX_LENGTH]);;

We can now make the inductive definitions package aware of it by:

  # monotonicity_theorems := MONO_LEX::(!monotonicity_theorems);;

SEE ALSO

new_inductive_definition.