Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Subject: Alternative inductive definitions package
Date: Mon, 13 Jun 94 13:18:18 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:187840:940613121851"@cl.cam.ac.uk>


An alternative package for inductive definitions is now available. It
can be found in the directory "ind-defs" in the Cambridge contrib directory
(hvg/contrib/ind-defs/* at ftp.cl.cam.ac.uk; see also
 hvg/contrib/00-Tarfiles/ind-defs.tar.gz for a tarred version).

This contribution provides broadly similar facilities to Tom Melham's
`ind_defs' library, but it allows much more general forms for the
hypotheses of rules.

Any monotone function in the relation being defined is permitted as a
hypothesis, and monotonicity is proved automatically for a wide range of
operations including (possibly paired) universal and existential
quantifiers, and list conjunction (ALL_EL). Users may augment the stock
of monotonicity rules with those for particular operations they may
require.

At present mutual induction is not supported. I have an experimental
implementation but it needs more work to simplify the cases theorem
cleanly, which I don't currently have time for. (Basically it uses the
idea Klaus recently suggested here for mutual recursion, viz. defining a
single relation with an extra "discriminating" parameter.) Other possible
extensions include coinduction, and implementing recursive types in a
similar fashion (this has been done in a unified way by Larry Paulson
in Isabelle).

The underlying implementation is essentially the same as the Tarski
contribution by Flemming Andersen & Kim Dam Petersen (actually Tarski's
theorem is proved on each call for a curried n-place relation, rather
than being stored as a theorem for a 1-place relation and modified). It
is intended to be easier to use, so the monotonicity proofs are automated
to some extent, and "clausal" definitions as in Tom's library are fully
supported.

The detailed structure is a little different from Tom's library, but it
would be quite easy to build a compatible interface on top. The main
function is "new_inductive_definition" which takes a term representing a
clausal definition, and returns a triple of rule, induction and cases
theorems. This is probably best illustrated by a few examples:

  #new_inductive_definition false `EVEN`
  #  "EVEN_NUM(0) /\
  #   (!n. EVEN_NUM(n) ==> EVEN_NUM(n + 2))";;
  (|- EVEN_NUM 0 /\ (!n. EVEN_NUM n ==> EVEN_NUM(n + 2)),
   |- !EVEN_NUM'.
       EVEN_NUM' 0 /\ (!n. EVEN_NUM' n ==> EVEN_NUM'(n + 2)) ==>
       (!a1. EVEN_NUM a1 ==> EVEN_NUM' a1),
   |- !a1. EVEN_NUM a1 = (a1 = 0) \/ (?n. EVEN_NUM n /\ (a1 = n + 2)))
  : (thm # thm # thm)
  Run time: 0.9s
  Intermediate theorems generated: 239

  #new_inductive_definition false `RSTC`
  #  "(!x y. R x y ==> RSTC R x y) /\
  #   (!x:*. RSTC R x x) /\
  #   (!x y. RSTC R x y ==> RSTC R y x) /\
  #   (!x y z. RSTC R x y /\ RSTC R y z ==> RSTC R x z)";;
  (|- !R.
       (!x y. R x y ==> RSTC R x y) /\
       (!x. RSTC R x x) /\
       (!x y. RSTC R x y ==> RSTC R y x) /\
       (!x y z. RSTC R x y /\ RSTC R y z ==> RSTC R x z),
   |- !R RSTC'.
       (!x y. R x y ==> RSTC' x y) /\
       (!x. RSTC' x x) /\
       (!x y. RSTC' x y ==> RSTC' y x) /\
       (!x y z. RSTC' x y /\ RSTC' y z ==> RSTC' x z) ==>
       (!a1 a2. RSTC R a1 a2 ==> RSTC' a1 a2),
   |- !R a1 a2.
       RSTC R a1 a2 =
       R a1 a2 \/
       (a2 = a1) \/
       RSTC R a2 a1 \/
       (?y. RSTC R a1 y /\ RSTC R y a2))
  : (thm # thm # thm)
  Run time: 1.6s
  Intermediate theorems generated: 410

  #let STUPID = "STUPID:num->num->num->bool" in
  #new_inductive_definition false `STUPID`
  #  "(!a b c. ^STUPID a (a + b) (a + b + c)) /\
  #   (!l. ALL_EL (\x. STUPID x (SUC x) x) l ==> ^STUPID (HD l) 1 1) /\
  #   ((!l n. (?x. n = EL x l) ==> ^STUPID n (HD l) n) ==> ^STUPID 1 1 1)";;
  (|- (!a b c. STUPID a(a + b)(a + (b + c))) /\
      (!l. ALL_EL(\x. STUPID x(SUC x)x)l ==> STUPID(HD l)1 1) /\
      ((!l n. (?x. n = EL x l) ==> STUPID n(HD l)n) ==> STUPID 1 1 1),
   |- !STUPID'.
       (!a b c. STUPID' a(a + b)(a + (b + c))) /\
       (!l. ALL_EL(\x. STUPID' x(SUC x)x)l ==> STUPID'(HD l)1 1) /\
       ((!l n. (?x. n = EL x l) ==> STUPID' n(HD l)n) ==> STUPID' 1 1 1) ==>
       (!a1 a2 a3. STUPID a1 a2 a3 ==> STUPID' a1 a2 a3),
   |- !a1 a2 a3.
       STUPID a1 a2 a3 =
       (?b c. T /\ (a2 = a1 + b) /\ (a3 = a1 + (b + c))) \/
       (?l.
         ALL_EL(\x. STUPID x(SUC x)x)l /\
         (a1 = HD l) /\
         (a2 = 1) /\
         (a3 = 1)) \/
       (!l n. (?x. n = EL x l) ==> STUPID n(HD l)n) /\
       (a1 = 1) /\
       (a2 = 1) /\
       (a3 = 1))
  : (thm # thm # thm)
  Run time: 1.9s
  Garbage collection time: 1.0s
  Intermediate theorems generated: 442

There is no documentation except the comments in the source file and what I
have just written. But I hope people will find it useful, and tell me of any
bugs. I plan to port it to hol90 when I finish the mutual extension and
incorporate any corrections, but if anyone wants to have a go themselves,
they are more than welcome.

John.