new_inductive_set : term -> thm * thm * thm

SYNOPSIS

Define a set or family of sets inductively.

DESCRIPTION

The function new_inductive_set is applied to a conjunction of ``rules'', each of the form !x1...xn. Pi ==> ti IN Sk. This conjunction is interpreted as an inductive definition of a family of sets Sk (however many appear in the consequents of the rules). That is, the sets are defined to be the smallest ones closed under the rules. The function new_inductive_set will convert this into explicit definitions, define a new constant for each Sk, and return a triple of theorems. The first one will be the ``rule'' theorem, which essentially matches the input clauses except that the Si are now the new constants; this simply says that the new sets are indeed closed under the rules. The second theorem is an induction theorem, asserting that the sets are the least ones closed under the rules. Finally, the cases theorem gives a case analysis theorem showing how each set of values satisfying the set may be composed.

FAILURE CONDITIONS

Fails if the clauses are malformed, if the constants are already in use, or if there are unproven monotonicity hypotheses. See new_inductive_definition for more detailed discussion in the similar case of indunctive relations.

EXAMPLE

A classic example where we have mutual induction is the set of even and odd numbers:

  # let EO_RULES, EO_INDUCT, EO_CASES = new_inductive_set
    `0 IN even_numbers /\
     (!n. n IN even_numbers ==> SUC n IN odd_numbers) /\
     1 IN odd_numbers /\
     (!n. n IN odd_numbers ==> SUC n IN even_numbers)`;;
  val EO_RULES : thm =
    |- 0 IN even_numbers /\
       (!n. n IN even_numbers ==> SUC n IN odd_numbers) /\
       1 IN odd_numbers /\
       (!n. n IN odd_numbers ==> SUC n IN even_numbers)
  val EO_INDUCT : thm =
    |- !odd_numbers' even_numbers'.
           even_numbers' 0 /\
           (!n. even_numbers' n ==> odd_numbers' (SUC n)) /\
           odd_numbers' 1 /\
           (!n. odd_numbers' n ==> even_numbers' (SUC n))
           ==> (!a0. a0 IN odd_numbers ==> odd_numbers' a0) /\
               (!a1. a1 IN even_numbers ==> even_numbers' a1)
  val EO_CASES : thm =
    |- (!a0. a0 IN odd_numbers <=>
             (?n. a0 = SUC n /\ n IN even_numbers) \/ a0 = 1) /\
       (!a1. a1 IN even_numbers <=>
             a1 = 0 \/ (?n. a1 = SUC n /\ n IN odd_numbers))

Note that the `rules' theorem corresponds exactly to the input, and says that indeed the sets do satisfy the rules. The `induction' theorem says that the sets are the minimal ones satisfying the rules. You can use this to prove properties by induction, e.g. the relationship with the pre-defined concepts of odd and even:

  # g `(!n. n IN odd_numbers ==> ODD(n)) /\
       (!n. n IN even_numbers ==> EVEN(n))`;;

applying the induction theorem:

  # e(MATCH_MP_TAC EO_INDUCT);;
  val it : goalstack = 1 subgoal (1 total)

  `EVEN 0 /\
   (!n. EVEN n ==> ODD (SUC n)) /\
   ODD 1 /\
   (!n. ODD n ==> EVEN (SUC n))`

This is easily finished off by, for example:

  # e(REWRITE_TAC[GSYM NOT_EVEN; EVEN; ARITH]);;
  val it : goalstack = No subgoals

This function uses new_inductive_relation internally, and the documentation for that function gives additional information and other relevant examples.