Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: recursive data types.
Date: Sat, 09 Nov 91 20:51:35 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.356:09.10.91.20.51.40"@cl.cam.ac.uk>


Non-automatic recursive data types.
-----------------------------------

In a recent message Jeff asked for a data type something like:

       data = INT | CHAR | RECORD (data)list

and I just thought I'd see how much work it is to define such a
type "by hand", given the already existing type (*)ltree.  The
attached HOL source is the result of this investigation.  The
bottom line is a data type :data with the property that


     |- !e1 e2 f.
         ?!fn:data->*.
          (fn INT = e1) /\
          (fn CHAR = e2) /\
          (!ds. fn(RECORD ds) = f(MAP fn ds)ds)

The proof went through pretty along the same lines as one might
have an automated tool to do it, though of course it's WAY too slow
as it stands (e.g. it uses rewriting, REDEPTH_CONV, etc).   As you
can see, the proof itself is pretty easy.

Sorry about the lack of documentation and the somewhat hacked
proof style, but I hope interested users will be able to follow
the proof anyway.

Tom

==========================================================================
new_theory `data`;;

let IS_DATA =
     "\v:one+one+one.
       \tl:((one+one+one)ltree)list.
           ((v = (INL one)) /\ (tl = [])) \/
           ((v = (INR (INL one))) /\ (tl = [])) \/
           (v = (INR (INR one)))" ;;

let ethm =
    TAC_PROOF
    (([], "?x. TRP ^IS_DATA x"),
     MATCH_MP_TAC exists_TRP THEN
     EXISTS_TAC "INL one:(one+one+one)" THEN
     BETA_TAC THEN REWRITE_TAC []);;

let data_TY_DEF =
    new_type_definition(`data`,"TRP ^IS_DATA",ethm);;

let data_ISO_DEF =
     define_new_type_bijections `data_ISO_DEF` `ABS` `REP` data_TY_DEF;;

let INT_DEF =
    new_definition
    (`INT_DEF`,
     "INT = ABS(Node(INL one)[])");;

let CHAR_DEF =
    new_definition
    (`CHAR_DEF`,
     "CHAR = ABS(Node(INR (INL one))[])");;

let RECORD_DEF =
    new_definition
    (`RECORD_DEF`,
     "RECORD xs = ABS(Node(INR (INR one)) (MAP REP xs))");;

let lemma1 =
    prove
    ("!l. (MAP (f:*->**) l = []) = (l = [])",
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [NOT_CONS_NIL;MAP]);;

let lemma2 =
    prove
    ("!P Q R. ((P \/ Q) ==> R) =  ((P ==> R) /\ (Q ==> R))",
     REPEAT GEN_TAC THEN
     MAP_EVERY ASM_CASES_TAC ["P:bool";"Q:bool"] THEN
     ASM_REWRITE_TAC []);;

let AD_HOC_CONV tm =
    let v,eq,P = (I # dest_imp) (dest_forall tm) in
    let l,r = dest_eq eq in
    let imp1 = DISCH tm (MP (SPEC r (ASSUME tm)) (REFL r)) in
    let asm = rand(concl imp1) in
    let th1 = SUBST [SYM(ASSUME eq),v] P (ASSUME asm) in
    let imp2 = DISCH asm (GEN v (DISCH eq th1)) in
        IMP_ANTISYM_RULE imp1 imp2;;

let theorem1 =
    let thm1 = BETA_RULE (MATCH_MP TY_DEF_THM data_ISO_DEF) in
    let thm2 = PURE_REWRITE_RULE [lemma1;lemma2] thm1 in
    let thm3 = CONV_RULE (REDEPTH_CONV FORALL_AND_CONV) thm2 in
    let thm4 = CONV_RULE (TOP_DEPTH_CONV ANTE_CONJ_CONV) thm3 in
    let thm5 = CONV_RULE (DEPTH_CONV FORALL_IMP_CONV) thm4 in
    let thm6 = CONV_RULE (DEPTH_CONV AD_HOC_CONV) thm5 in
    let thm7 = REWRITE_RULE [MAP] thm6 in
    let ths = [SYM INT_DEF; SYM CHAR_DEF; SYM(SPEC_ALL RECORD_DEF)] in
        REWRITE_RULE ths thm7;;

let data_Axiom =
    let tm =
     "\l:(*)list.\v:one + (one + one). \d:(data)list.
      (ISL v => e1 | (ISL(OUTR v) => e2 |  f l d)):*" in
    let thm1 = BETA_RULE (ISPEC tm theorem1) in
    let thm2 = REWRITE_RULE [ISL;OUTR] thm1 in
    let cleanup = ONCE_DEPTH_CONV (ALPHA_CONV "ds:(data)list") in
    let thm3 =  CONV_RULE cleanup thm2 in
        GEN_ALL thm3;;