Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9210110435.AA01684@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Tuple arguments on the LHS in new_recursive_definition
Date: Sat, 10 Oct 92 21:35:13 PDT
From: chou@edu.ucla.cs

Want to be able to use tuple arguments on the LHS of a definition
in new_recursive_definition?  The following ML code allows you to
do that.  It's a quick-and-dirty fix and I have tested it on only
a few examples, so I won't guarantee it would work on your example.
But if you find any problem, I'd be happy to know (but may not be
able to fix!).  The following is a little example:

#new_theory `test` ;;
() : void

#let btree_AX = define_type `btree`
#`
#  btree = LEAF * | NODE btree btree
#` ;;
btree_AX = 
|- !f0 f1.
    ?! fn.
     (!x. fn(LEAF x) = f0 x) /\
     (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)

#let th1 = prove_tuple_rec_fn_exists btree_AX
#"
#  ( TEST (i,j,k) (LEAF (x:*)) (f,a) = i + (f x) + j + a + k ) /\
#  ( TEST (l,m,n) (NODE t1 t2) (f,a) = l + (TEST (l,m,n) t1 (f,a)) + m +
#                                          (TEST (l,m,n) t2 (f,a)) + n )
#" ;;
th1 = 
|- ?TEST.
    (!i j k x f a.
      TEST(i,j,k)(LEAF x)(f,a) = i + ((f x) + (j + (a + k)))) /\
    (!l m n t1 t2 f a.
      TEST(l,m,n)(NODE t1 t2)(f,a) =
      l + ((TEST(l,m,n)t1(f,a)) + (m + ((TEST(l,m,n)t2(f,a)) + n))))

Incidentally, the conversion FORALL_TUPLE_CONV below may be of some
independent interest.

Enjoy!
- Ching Tsun

==========================================================================

%-----------------------------------------------------------------------------
  mk_FST_SND_list "p" n =
  ["FST p"; "FST(SND p)"; "FST(SND(SND p))"; ...; "SND(SND(...(SND p)))"]
-----------------------------------------------------------------------------%

letrec mk_FST_SND_list (p : term) (n : int) =
  if (n = 1) then [p]
  if (n > 1) then ("FST ^p" . (mk_FST_SND_list "SND ^p" (n - 1)))
  else failwith `mk_FST_SND_list`
;;

%-----------------------------------------------------------------------------
  FORALL_TUPLE_CONV "(x1, ..., xn)" "(! p . t)" =
  |- (! p . t) = (! x1 ... xn . t[(x1, ..., xn)/p])
-----------------------------------------------------------------------------%

let FORALL_TUPLE_CONV (xt : term) (lhs : term) =
  let xl = (strip_pair xt) in
  let LR = (DISCH lhs (GENL xl (SPEC xt (ASSUME lhs)))) in
  let rhs = (rand (concl LR)) in
  let (tv,tm) = (dest_forall lhs) in
  let yl = (mk_FST_SND_list tv (length xl)) in
  let EQ = (DEPTH_CONV (REWRITE_CONV PAIR)) (list_mk_pair yl) in
  let RL = (DISCH rhs (GEN tv (SUBST [(EQ, tv)] tm
             (rev_itlist SPEC yl (ASSUME rhs))))) in
  ( IMP_ANTISYM_RULE LR RL )
;;

%-----------------------------------------------------------------------------
  prove_tuple_rec_fn_exists is a generalization of prove_rec_fn_exists
  in which tuple arguments in the LHS of a definition are allowed.
-----------------------------------------------------------------------------%

let prove_tuple_rec_fn_exists =
  let mk_subs (t : term) =
    if (is_pair t) then (genvar (type_of t), t) else (t, t)
  in
  let mk_canon_eq (eq : term) =
    let (lhs, rhs) = dest_eq eq in
    let (rator, randl) = strip_comb lhs in
    let subsl = map mk_subs randl in
    let lhs' = list_mk_comb (rator, map fst subsl) in
    let subsl' = filter (\(v, p). not (v = p)) subsl in
    let rhs' = (rev_itlist (C (curry mk_let) o fst) subsl'
                  o itlist (   curry mk_pabs o snd) subsl') rhs in
    ( mk_eq (lhs', rhs'), subsl')
  in
  let mk_canon_eqs =
    (list_mk_conj # I) o split o
    map (mk_canon_eq o snd o strip_forall) o conjuncts
  in
  letrec eq_CONV (subsl : (term # term) list) (eq : term) =
    ( if (is_forall eq) then
        ( let bv = bndvar (rand eq) in
          ( let tup = snd (assoc bv subsl) in
              (FORALL_TUPLE_CONV tup) THENC (eq_CONV subsl)
          ) ? (RAND_CONV o ABS_CONV) (eq_CONV subsl) )
      else
        ( (TRY_CONV o RAND_CONV) let_CONV )
    ) eq
  in
  letrec eqs_CONV =
    fun [subsl]        . (eq_CONV subsl)
      | (subsl.subsll) . (RATOR_CONV o RAND_CONV) (eq_CONV subsl)
                         THENC (RAND_CONV) (eqs_CONV subsll)
  in
  \ (rec_thm : thm) (eqs : term) .
    let (canon, subsll) = mk_canon_eqs eqs in
    let exists_thm = prove_rec_fn_exists rec_thm canon in
    ( ((CONV_RULE o RAND_CONV o ABS_CONV) (eqs_CONV subsll)) exists_thm )
;;

let new_rec_definition (rec_thm) (label, eqs) =
  let exists_thm = prove_tuple_rec_fn_exists rec_thm eqs in
  let name = (fst o dest_var o fst o dest_exists o concl) exists_thm in
  ( new_specification label [(`constant`, name)] exists_thm )
;;

let new_infix_rec_definition (rec_thm) (label, eqs) =
  let exists_thm = prove_tuple_rec_fn_exists rec_thm eqs in
  let name = (fst o dest_var o fst o dest_exists o concl) exists_thm in
  ( new_specification label [(`infix`, name)] exists_thm )
;;