ind_types.ml

   1 (* ========================================================================= *)
   2 (* Inductive (or free recursive) types.                                      *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "grobner.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Abstract left inverses for binary injections (we could construct them...) *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let INJ_INVERSE2 = prove
  17  (`!P:A->B->C.
  18     (!x1 y1 x2 y2. (P x1 y1 = P x2 y2) <=> (x1 = x2) /\ (y1 = y2))
  19     ==> ?X Y. !x y. (X(P x y) = x) /\ (Y(P x y) = y)`,
  20   GEN_TAC THEN DISCH_TAC THEN
  21   EXISTS_TAC `\z:C. @x:A. ?y:B. P x y = z` THEN
  22   EXISTS_TAC `\z:C. @y:B. ?x:A. P x y = z` THEN
  23   REPEAT GEN_TAC THEN ASM_REWRITE_TAC[BETA_THM] THEN
  24   CONJ_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN GEN_TAC THEN BETA_TAC THEN
  25   EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  26   W(EXISTS_TAC o rand o snd o dest_exists o snd) THEN REFL_TAC);;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* Define an injective pairing function on ":num".                           *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let NUMPAIR = new_definition
  33   `NUMPAIR x y = (2 EXP x) * (2 * y + 1)`;;
  34
  35 let NUMPAIR_INJ_LEMMA = prove
  36  (`!x1 y1 x2 y2. (NUMPAIR x1 y1 = NUMPAIR x2 y2) ==> (x1 = x2)`,
  37   REWRITE_TAC[NUMPAIR] THEN REPEAT(INDUCT_TAC THEN GEN_TAC) THEN
  38   ASM_REWRITE_TAC[EXP; GSYM MULT_ASSOC; ARITH; EQ_MULT_LCANCEL;
  39     NOT_SUC; GSYM NOT_SUC; SUC_INJ] THEN
  40   DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
  41   REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH]);;
  42
  43 let NUMPAIR_INJ = prove
  44  (`!x1 y1 x2 y2. (NUMPAIR x1 y1 = NUMPAIR x2 y2) <=> (x1 = x2) /\ (y1 = y2)`,
  45   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  46   FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP NUMPAIR_INJ_LEMMA) THEN
  47   POP_ASSUM MP_TAC THEN REWRITE_TAC[NUMPAIR] THEN
  48   REWRITE_TAC[EQ_MULT_LCANCEL; EQ_ADD_RCANCEL; EXP_EQ_0; ARITH]);;
  49
  50 let NUMPAIR_DEST = new_specification
  51   ["NUMFST"; "NUMSND"]
  52   (MATCH_MP INJ_INVERSE2 NUMPAIR_INJ);;
  53
  54 (* ------------------------------------------------------------------------- *)
  55 (* Also, an injective map bool->num->num (even easier!)                      *)
  56 (* ------------------------------------------------------------------------- *)
  57
  58 let NUMSUM = new_definition
  59   `NUMSUM b x = if b then SUC(2 * x) else 2 * x`;;
  60
  61 let NUMSUM_INJ = prove
  62  (`!b1 x1 b2 x2. (NUMSUM b1 x1 = NUMSUM b2 x2) <=> (b1 = b2) /\ (x1 = x2)`,
  63   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  64   POP_ASSUM(MP_TAC o REWRITE_RULE[NUMSUM]) THEN
  65   DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(AP_TERM `EVEN` th)) THEN
  66   REPEAT COND_CASES_TAC THEN REWRITE_TAC[EVEN; EVEN_DOUBLE] THEN
  67   REWRITE_TAC[SUC_INJ; EQ_MULT_LCANCEL; ARITH]);;
  68
  69 let NUMSUM_DEST = new_specification
  70   ["NUMLEFT"; "NUMRIGHT"]
  71   (MATCH_MP INJ_INVERSE2 NUMSUM_INJ);;
  72
  73 (* ------------------------------------------------------------------------- *)
  74 (* Injection num->Z, where Z == num->A->bool.                                *)
  75 (* ------------------------------------------------------------------------- *)
  76
  77 let INJN = new_definition
  78  `INJN (m:num) = \(n:num) (a:A). n = m`;;
  79
  80 let INJN_INJ = prove
  81  (`!n1 n2. (INJN n1 :num->A->bool = INJN n2) <=> (n1 = n2)`,
  82   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  83   POP_ASSUM(MP_TAC o C AP_THM `n1:num` o REWRITE_RULE[INJN]) THEN
  84   DISCH_THEN(MP_TAC o C AP_THM `a:A`) THEN REWRITE_TAC[BETA_THM]);;
  85
  86 (* ------------------------------------------------------------------------- *)
  87 (* Injection A->Z, where Z == num->A->bool.                                  *)
  88 (* ------------------------------------------------------------------------- *)
  89
  90 let INJA = new_definition
  91  `INJA (a:A) = \(n:num) b. b = a`;;
  92
  93 let INJA_INJ = prove
  94  (`!a1 a2. (INJA a1 = INJA a2) <=> (a1:A = a2)`,
  95   REPEAT GEN_TAC THEN REWRITE_TAC[INJA; FUN_EQ_THM] THEN EQ_TAC THENL
  96    [DISCH_THEN(MP_TAC o SPEC `a1:A`) THEN REWRITE_TAC[];
  97     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[]]);;
  98
  99 (* ------------------------------------------------------------------------- *)
 100 (* Injection (num->Z)->Z, where Z == num->A->bool.                           *)
 101 (* ------------------------------------------------------------------------- *)
 102
 103 let INJF = new_definition
 104   `INJF (f:num->(num->A->bool)) = \n. f (NUMFST n) (NUMSND n)`;;
 105
 106 let INJF_INJ = prove
 107  (`!f1 f2. (INJF f1 :num->A->bool = INJF f2) <=> (f1 = f2)`,
 108   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 109   REWRITE_TAC[FUN_EQ_THM] THEN
 110   MAP_EVERY X_GEN_TAC [`n:num`; `m:num`; `a:A`] THEN
 111   POP_ASSUM(MP_TAC o REWRITE_RULE[INJF]) THEN
 112   DISCH_THEN(MP_TAC o C AP_THM `a:A` o C AP_THM `NUMPAIR n m`) THEN
 113   REWRITE_TAC[NUMPAIR_DEST]);;
 114
 115 (* ------------------------------------------------------------------------- *)
 116 (* Injection Z->Z->Z, where Z == num->A->bool.                               *)
 117 (* ------------------------------------------------------------------------- *)
 118
 119 let INJP = new_definition
 120   `INJP f1 f2:num->A->bool =
 121         \n a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a`;;
 122
 123 let INJP_INJ = prove
 124  (`!(f1:num->A->bool) f1' f2 f2'.
 125         (INJP f1 f2 = INJP f1' f2') <=> (f1 = f1') /\ (f2 = f2')`,
 126   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 127   ONCE_REWRITE_TAC[FUN_EQ_THM] THEN REWRITE_TAC[AND_FORALL_THM] THEN
 128   X_GEN_TAC `n:num` THEN POP_ASSUM(MP_TAC o REWRITE_RULE[INJP]) THEN
 129   DISCH_THEN(MP_TAC o GEN `b:bool` o C AP_THM `NUMSUM b n`) THEN
 130   DISCH_THEN(fun th -> MP_TAC(SPEC `T` th) THEN MP_TAC(SPEC `F` th)) THEN
 131   ASM_SIMP_TAC[NUMSUM_DEST; ETA_AX]);;
 132
 133 (* ------------------------------------------------------------------------- *)
 134 (* Now, set up "constructor" and "bottom" element.                           *)
 135 (* ------------------------------------------------------------------------- *)
 136
 137 let ZCONSTR = new_definition
 138   `ZCONSTR c i r :num->A->bool
 139      = INJP (INJN (SUC c)) (INJP (INJA i) (INJF r))`;;
 140
 141 let ZBOT = new_definition
 142   `ZBOT = INJP (INJN 0) (@z:num->A->bool. T)`;;
 143
 144 let ZCONSTR_ZBOT = prove
 145  (`!c i r. ~(ZCONSTR c i r :num->A->bool = ZBOT)`,
 146   REWRITE_TAC[ZCONSTR; ZBOT; INJP_INJ; INJN_INJ; NOT_SUC]);;
 147
 148 (* ------------------------------------------------------------------------- *)
 149 (* Carve out an inductively defined set.                                     *)
 150 (* ------------------------------------------------------------------------- *)
 151
 152 let ZRECSPACE_RULES,ZRECSPACE_INDUCT,ZRECSPACE_CASES =
 153   new_inductive_definition
 154    `ZRECSPACE (ZBOT:num->A->bool) /\
 155     (!c i r. (!n. ZRECSPACE (r n)) ==> ZRECSPACE (ZCONSTR c i r))`;;
 156
 157 let recspace_tydef =
 158   new_basic_type_definition "recspace" ("_mk_rec","_dest_rec")
 159   (CONJUNCT1 ZRECSPACE_RULES);;
 160
 161 (* ------------------------------------------------------------------------- *)
 162 (* Define lifted constructors.                                               *)
 163 (* ------------------------------------------------------------------------- *)
 164
 165 let BOTTOM = new_definition
 166   `BOTTOM = _mk_rec (ZBOT:num->A->bool)`;;
 167
 168 let CONSTR = new_definition
 169   `CONSTR c i r :(A)recspace
 170      = _mk_rec (ZCONSTR c i (\n. _dest_rec(r n)))`;;
 171
 172 (* ------------------------------------------------------------------------- *)
 173 (* Some lemmas.                                                              *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let MK_REC_INJ = prove
 177  (`!x y. (_mk_rec x :(A)recspace = _mk_rec y)
 178          ==> (ZRECSPACE x /\ ZRECSPACE y ==> (x = y))`,
 179   REPEAT GEN_TAC THEN DISCH_TAC THEN
 180   REWRITE_TAC[snd recspace_tydef] THEN
 181   DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN
 182   ASM_REWRITE_TAC[]);;
 183
 184 let DEST_REC_INJ = prove
 185  (`!x y. (_dest_rec x = _dest_rec y) <=> (x:(A)recspace = y)`,
 186   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 187   POP_ASSUM(MP_TAC o AP_TERM
 188     `_mk_rec:(num->A->bool)->(A)recspace`) THEN
 189   REWRITE_TAC[fst recspace_tydef]);;
 190
 191 (* ------------------------------------------------------------------------- *)
 192 (* Show that the set is freely inductively generated.                        *)
 193 (* ------------------------------------------------------------------------- *)
 194
 195 let CONSTR_BOT = prove
 196  (`!c i r. ~(CONSTR c i r :(A)recspace = BOTTOM)`,
 197   REPEAT GEN_TAC THEN REWRITE_TAC[CONSTR; BOTTOM] THEN
 198   DISCH_THEN(MP_TAC o MATCH_MP MK_REC_INJ) THEN
 199   REWRITE_TAC[ZCONSTR_ZBOT; ZRECSPACE_RULES] THEN
 200   MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN
 201   REWRITE_TAC[fst recspace_tydef; snd recspace_tydef]);;
 202
 203 let CONSTR_INJ = prove
 204  (`!c1 i1 r1 c2 i2 r2. (CONSTR c1 i1 r1 :(A)recspace = CONSTR c2 i2 r2) <=>
 205                        (c1 = c2) /\ (i1 = i2) /\ (r1 = r2)`,
 206   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 207   POP_ASSUM(MP_TAC o REWRITE_RULE[CONSTR]) THEN
 208   DISCH_THEN(MP_TAC o MATCH_MP MK_REC_INJ) THEN
 209   W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 lhand o snd) THENL
 210    [CONJ_TAC THEN MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN
 211     REWRITE_TAC[fst recspace_tydef; snd recspace_tydef];
 212     ASM_REWRITE_TAC[] THEN REWRITE_TAC[ZCONSTR] THEN
 213     REWRITE_TAC[INJP_INJ; INJN_INJ; INJF_INJ; INJA_INJ] THEN
 214     ONCE_REWRITE_TAC[FUN_EQ_THM] THEN BETA_TAC THEN
 215     REWRITE_TAC[SUC_INJ; DEST_REC_INJ]]);;
 216
 217 let CONSTR_IND = prove
 218  (`!P. P(BOTTOM) /\
 219        (!c i r. (!n. P(r n)) ==> P(CONSTR c i r))
 220        ==> !x:(A)recspace. P(x)`,
 221   REPEAT STRIP_TAC THEN
 222   MP_TAC(SPEC `\z:num->A->bool. ZRECSPACE(z) /\ P(_mk_rec z)`
 223          ZRECSPACE_INDUCT) THEN
 224   BETA_TAC THEN ASM_REWRITE_TAC[ZRECSPACE_RULES; GSYM BOTTOM] THEN
 225   W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 lhand o snd) THENL
 226    [REPEAT GEN_TAC THEN REWRITE_TAC[FORALL_AND_THM] THEN
 227     REPEAT STRIP_TAC THENL
 228      [MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN ASM_REWRITE_TAC[];
 229       FIRST_ASSUM(ANTE_RES_THEN MP_TAC) THEN
 230       REWRITE_TAC[CONSTR] THEN
 231       RULE_ASSUM_TAC(REWRITE_RULE[snd recspace_tydef]) THEN
 232       ASM_SIMP_TAC[ETA_AX]];
 233     ASM_REWRITE_TAC[] THEN
 234     DISCH_THEN(MP_TAC o SPEC `_dest_rec (x:(A)recspace)`) THEN
 235     REWRITE_TAC[fst recspace_tydef] THEN
 236     REWRITE_TAC[ITAUT `(a ==> a /\ b) <=> (a ==> b)`] THEN
 237     DISCH_THEN MATCH_MP_TAC THEN
 238     REWRITE_TAC[fst recspace_tydef; snd recspace_tydef]]);;
 239
 240 (* ------------------------------------------------------------------------- *)
 241 (* Now prove the recursion theorem (this subcase is all we need).            *)
 242 (* ------------------------------------------------------------------------- *)
 243
 244 let CONSTR_REC = prove
 245  (`!Fn:num->A->(num->(A)recspace)->(num->B)->B.
 246      ?f. (!c i r. f (CONSTR c i r) = Fn c i r (\n. f (r n)))`,
 247   REPEAT STRIP_TAC THEN (MP_TAC o prove_inductive_relations_exist)
 248     `(Z:(A)recspace->B->bool) BOTTOM b /\
 249      (!c i r y. (!n. Z (r n) (y n)) ==> Z (CONSTR c i r) (Fn c i r y))` THEN
 250   DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 251   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN
 252   SUBGOAL_THEN `!x. ?!y. (Z:(A)recspace->B->bool) x y` MP_TAC THENL
 253    [W(MP_TAC o PART_MATCH rand CONSTR_IND o snd) THEN
 254     DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THEN REPEAT GEN_TAC THENL
 255      [FIRST_ASSUM(fun t -> GEN_REWRITE_TAC BINDER_CONV [GSYM t]) THEN
 256       REWRITE_TAC[GSYM CONSTR_BOT; EXISTS_UNIQUE_REFL];
 257       DISCH_THEN(MP_TAC o REWRITE_RULE[EXISTS_UNIQUE_THM; FORALL_AND_THM]) THEN
 258       DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 259       DISCH_THEN(MP_TAC o REWRITE_RULE[SKOLEM_THM]) THEN
 260       DISCH_THEN(X_CHOOSE_THEN `y:num->B` ASSUME_TAC) THEN
 261       REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 262       FIRST_ASSUM(fun th -> CHANGED_TAC(ONCE_REWRITE_TAC[GSYM th])) THEN
 263       CONJ_TAC THENL
 264        [EXISTS_TAC `(Fn:num->A->(num->(A)recspace)->(num->B)->B) c i r y` THEN
 265         REWRITE_TAC[CONSTR_BOT; CONSTR_INJ; GSYM CONJ_ASSOC] THEN
 266         REWRITE_TAC[UNWIND_THM1; RIGHT_EXISTS_AND_THM] THEN
 267         EXISTS_TAC `y:num->B` THEN ASM_REWRITE_TAC[];
 268         REWRITE_TAC[CONSTR_BOT; CONSTR_INJ; GSYM CONJ_ASSOC] THEN
 269         REWRITE_TAC[UNWIND_THM1; RIGHT_EXISTS_AND_THM] THEN
 270         REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 271         REPEAT AP_TERM_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
 272         X_GEN_TAC `w:num` THEN FIRST_ASSUM MATCH_MP_TAC THEN
 273         EXISTS_TAC `w:num` THEN ASM_REWRITE_TAC[]]];
 274     REWRITE_TAC[UNIQUE_SKOLEM_ALT] THEN
 275     DISCH_THEN(X_CHOOSE_THEN `fn:(A)recspace->B` (ASSUME_TAC o GSYM)) THEN
 276     EXISTS_TAC `fn:(A)recspace->B` THEN ASM_REWRITE_TAC[] THEN
 277     REPEAT GEN_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
 278     FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
 279     REWRITE_TAC[BETA_THM]]);;
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* The following is useful for coding up functions casewise.                 *)
 283 (* ------------------------------------------------------------------------- *)
 284
 285 let FCONS = new_recursive_definition num_RECURSION
 286  `(!a f. FCONS (a:A) f 0 = a) /\
 287   (!a f n. FCONS (a:A) f (SUC n) = f n)`;;
 288
 289 let FCONS_UNDO = prove
 290  (`!f:num->A. f = FCONS (f 0) (f o SUC)`,
 291   GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
 292   INDUCT_TAC THEN REWRITE_TAC[FCONS; o_THM]);;
 293
 294 let FNIL = new_definition
 295   `FNIL (n:num) = @x:A. T`;;
 296
 297 (* ------------------------------------------------------------------------- *)
 298 (* The initial mutual type definition function, with a type-restricted       *)
 299 (* recursion theorem.                                                        *)
 300 (* ------------------------------------------------------------------------- *)
 301
 302 let define_type_raw =
 303
 304   (* ----------------------------------------------------------------------- *)
 305   (* Handy utility to produce "SUC o SUC o SUC ..." form of numeral.         *)
 306   (* ----------------------------------------------------------------------- *)
 307
 308   let sucivate =
 309     let zero = `0` and suc = `SUC` in
 310     fun n -> funpow n (curry mk_comb suc) zero in
 311
 312   (* ----------------------------------------------------------------------- *)
 313   (* Eliminate local "definitions" in hyps.                                  *)
 314   (* ----------------------------------------------------------------------- *)
 315
 316
 317   let SCRUB_EQUATION eq (th,insts) = (*HA*)
 318     let eq' = itlist subst (map (fun t -> [t]) insts) eq in
 319     let l,r = dest_eq eq' in
 320     (MP (INST [r,l] (DISCH eq' th)) (REFL r),(r,l)::insts) in
 321
 322   (* ----------------------------------------------------------------------- *)
 323   (* Proves existence of model (inductively); use pseudo-constructors.       *)
 324   (*                                                                         *)
 325   (* Returns suitable definitions of constructors in terms of CONSTR, and    *)
 326   (* the rule and induction theorems from the inductive relation package.    *)
 327   (* ----------------------------------------------------------------------- *)
 328
 329   let justify_inductive_type_model =
 330     let t_tm = `T` and n_tm = `n:num` and beps_tm = `@x:bool. T` in
 331     let rec munion s1 s2 =
 332       if s1 = [] then s2 else
 333       let h1 = hd s1
 334       and s1' = tl s1 in
 335       try let _,s2' = remove (fun h2 -> h2 = h1) s2 in h1::(munion s1' s2')
 336       with Failure _ -> h1::(munion s1' s2) in
 337     fun def ->
 338       let newtys,rights = unzip def in
 339       let tyargls = itlist ((@) o map snd) rights [] in
 340       let alltys = itlist (munion o C subtract newtys) tyargls [] in
 341       let epstms = map (fun ty -> mk_select(mk_var("v",ty),t_tm)) alltys in
 342       let pty =
 343         try end_itlist (fun ty1 ty2 -> mk_type("prod",[ty1;ty2])) alltys
 344         with Failure _ -> bool_ty in
 345       let recty = mk_type("recspace",[pty]) in
 346       let constr = mk_const("CONSTR",[pty,aty]) in
 347       let fcons = mk_const("FCONS",[recty,aty]) in
 348       let bot = mk_const("BOTTOM",[pty,aty]) in
 349       let bottail = mk_abs(n_tm,bot) in
 350       let mk_constructor n (cname,cargs) =
 351         let ttys = map (fun ty -> if mem ty newtys then recty else ty) cargs in
 352         let args = make_args "a" [] ttys in
 353         let rargs,iargs = partition (fun t -> type_of t = recty) args in
 354         let rec mk_injector epstms alltys iargs =
 355           if alltys = [] then [] else
 356           let ty = hd alltys in
 357           try let a,iargs' = remove (fun t -> type_of t = ty) iargs in
 358               a::(mk_injector (tl epstms) (tl alltys) iargs')
 359           with Failure _ ->
 360               (hd epstms)::(mk_injector (tl epstms) (tl alltys) iargs) in
 361         let iarg =
 362           try end_itlist (curry mk_pair) (mk_injector epstms alltys iargs)
 363           with Failure _ -> beps_tm in
 364         let rarg = itlist (mk_binop fcons) rargs bottail in
 365       let conty = itlist mk_fun_ty (map type_of args) recty in
 366       let condef = list_mk_comb(constr,[sucivate n; iarg; rarg]) in
 367       mk_eq(mk_var(cname,conty),list_mk_abs(args,condef)) in
 368     let rec mk_constructors n rights =
 369       if rights = [] then [] else
 370       (mk_constructor n (hd rights))::(mk_constructors (n + 1) (tl rights)) in
 371     let condefs = mk_constructors 0 (itlist (@) rights []) in
 372     let conths = map ASSUME condefs in
 373     let predty = mk_fun_ty recty bool_ty in
 374     let edefs = itlist (fun (x,l) acc -> map (fun t -> x,t) l @ acc) def [] in
 375     let idefs = map2 (fun (r,(_,atys)) def -> (r,atys),def) edefs condefs in
 376     let mk_rule ((r,a),condef) =
 377       let left,right = dest_eq condef in
 378       let args,bod = strip_abs right in
 379       let lapp = list_mk_comb(left,args) in
 380       let conds = itlist2
 381         (fun arg argty sofar ->
 382           if mem argty newtys then
 383             mk_comb(mk_var(dest_vartype argty,predty),arg)::sofar
 384           else sofar) args a [] in
 385       let conc = mk_comb(mk_var(dest_vartype r,predty),lapp) in
 386       let rule = if conds = [] then conc
 387                  else mk_imp(list_mk_conj conds,conc) in
 388       list_mk_forall(args,rule) in
 389     let rules = list_mk_conj (map mk_rule idefs) in
 390     let th0 = derive_nonschematic_inductive_relations rules in
 391     let th1 = prove_monotonicity_hyps th0 in
 392     let th2a,th2bc = CONJ_PAIR th1 in
 393     let th2b = CONJUNCT1 th2bc in
 394     conths,th2a,th2b in
 395
 396   (* ----------------------------------------------------------------------- *)
 397   (* Shows that the predicates defined by the rules are all nonempty.        *)
 398   (* (This could be done much more efficiently/cleverly, but it's OK.)       *)
 399   (* ----------------------------------------------------------------------- *)
 400
 401   let prove_model_inhabitation rth =
 402     let srules = map SPEC_ALL (CONJUNCTS rth) in
 403     let imps,bases = partition (is_imp o concl) srules in
 404     let concs = map concl bases @ map (rand o concl) imps in
 405     let preds = setify (map (repeat rator) concs) in
 406     let rec exhaust_inhabitations ths sofar =
 407       let dunnit = setify(map (fst o strip_comb o concl) sofar) in
 408       let useful = filter
 409         (fun th -> not (mem (fst(strip_comb(rand(concl th)))) dunnit)) ths in
 410       if useful = [] then sofar else
 411       let follow_horn thm =
 412         let preds = map (fst o strip_comb) (conjuncts(lhand(concl thm))) in
 413         let asms = map
 414           (fun p -> find (fun th -> fst(strip_comb(concl th)) = p) sofar)
 415           preds in
 416         MATCH_MP thm (end_itlist CONJ asms) in
 417       let newth = tryfind follow_horn useful in
 418       exhaust_inhabitations ths (newth::sofar) in
 419     let ithms = exhaust_inhabitations imps bases in
 420     let exths = map
 421       (fun p -> find (fun th -> fst(strip_comb(concl th)) = p) ithms) preds in
 422     exths in
 423
 424   (* ----------------------------------------------------------------------- *)
 425   (* Makes a type definition for one of the defined subsets.                 *)
 426   (* ----------------------------------------------------------------------- *)
 427
 428   let define_inductive_type cdefs exth =
 429     let extm = concl exth in
 430     let epred = fst(strip_comb extm) in
 431     let ename = fst(dest_var epred) in
 432     let th1 = ASSUME (find (fun eq -> lhand eq = epred) (hyp exth)) in
 433     let th2 = TRANS th1 (SUBS_CONV cdefs (rand(concl th1))) in
 434     let th3 = EQ_MP (AP_THM th2 (rand extm)) exth in
 435     let th4,_ = itlist SCRUB_EQUATION (hyp th3) (th3,[]) in
 436     let mkname = "_mk_"^ename and destname = "_dest_"^ename in
 437     let bij1,bij2 = new_basic_type_definition ename (mkname,destname) th4 in
 438     let bij2a = AP_THM th2 (rand(rand(concl bij2))) in
 439     let bij2b = TRANS bij2a bij2 in
 440     bij1,bij2b in
 441
 442   (* ----------------------------------------------------------------------- *)
 443   (* Defines a type constructor corresponding to current pseudo-constructor. *)
 444   (* ----------------------------------------------------------------------- *)
 445
 446   let define_inductive_type_constructor defs consindex th =
 447     let avs,bod = strip_forall(concl th) in
 448     let asms,conc =
 449       if is_imp bod then conjuncts(lhand bod),rand bod else [],bod in
 450     let asmlist = map dest_comb asms in
 451     let cpred,cterm = dest_comb conc in
 452     let oldcon,oldargs = strip_comb cterm in
 453     let modify_arg v =
 454       try let dest = snd(assoc (rev_assoc v asmlist) consindex) in
 455           let ty' = hd(snd(dest_type(type_of dest))) in
 456           let v' = mk_var(fst(dest_var v),ty') in
 457           mk_comb(dest,v'),v'
 458       with Failure _ -> v,v in
 459     let newrights,newargs = unzip(map modify_arg oldargs) in
 460     let retmk = fst(assoc cpred consindex) in
 461     let defbod = mk_comb(retmk,list_mk_comb(oldcon,newrights)) in
 462     let defrt = list_mk_abs(newargs,defbod) in
 463     let expth = find (fun th -> lhand(concl th) = oldcon) defs in
 464     let rexpth = SUBS_CONV [expth] defrt in
 465     let deflf = mk_var(fst(dest_var oldcon),type_of defrt) in
 466     let defth = new_definition(mk_eq(deflf,rand(concl rexpth))) in
 467     TRANS defth (SYM rexpth) in
 468
 469   (* ----------------------------------------------------------------------- *)
 470   (* Instantiate the induction theorem on the representatives to transfer    *)
 471   (* it to the new type(s). Uses "\x. rep-pred(x) /\ P(mk x)" for "P".       *)
 472   (* ----------------------------------------------------------------------- *)
 473
 474   let instantiate_induction_theorem consindex ith =
 475     let avs,bod = strip_forall(concl ith) in
 476     let corlist = map((repeat rator F_F repeat rator) o dest_imp o body o rand)
 477       (conjuncts(rand bod)) in
 478     let consindex' = map (fun v -> let w = rev_assoc v corlist in
 479                                    w,assoc w consindex) avs in
 480     let recty = (hd o snd o dest_type o type_of o fst o snd o hd) consindex in
 481     let newtys = map (hd o snd o dest_type o type_of o snd o snd) consindex' in
 482     let ptypes = map (C mk_fun_ty bool_ty) newtys in
 483     let preds = make_args "P" [] ptypes in
 484     let args = make_args "x" [] (map (K recty) preds) in
 485     let lambs = map2 (fun (r,(m,d)) (p,a) ->
 486                        mk_abs(a,mk_conj(mk_comb(r,a),mk_comb(p,mk_comb(m,a)))))
 487                      consindex' (zip preds args) in
 488     SPECL lambs ith in
 489
 490   (* ----------------------------------------------------------------------- *)
 491   (* Reduce a single clause of the postulated induction theorem (old_ver) ba *)
 492   (* to the kind wanted for the new type (new_ver); |- new_ver ==> old_ver   *)
 493   (* ----------------------------------------------------------------------- *)
 494
 495   let pullback_induction_clause tybijpairs conthms =
 496     let PRERULE = GEN_REWRITE_RULE (funpow 3 RAND_CONV) (map SYM conthms) in
 497     let IPRULE = SYM o GEN_REWRITE_RULE I (map snd tybijpairs) in
 498     fun rthm tm ->
 499       let avs,bimp = strip_forall tm in
 500       if is_imp bimp then
 501         let ant,con = dest_imp bimp in
 502         let ths = map (CONV_RULE BETA_CONV) (CONJUNCTS (ASSUME ant)) in
 503         let tths,pths = unzip (map CONJ_PAIR ths) in
 504         let tth = MATCH_MP (SPEC_ALL rthm) (end_itlist CONJ tths) in
 505         let mths = map IPRULE (tth::tths) in
 506         let conth1 = BETA_CONV con in
 507         let contm1 = rand(concl conth1) in
 508         let conth2 = TRANS conth1
 509           (AP_TERM (rator contm1) (SUBS_CONV (tl mths) (rand contm1))) in
 510         let conth3 = PRERULE conth2 in
 511         let lctms = map concl pths in
 512         let asmin = mk_imp(list_mk_conj lctms,rand(rand(concl conth3))) in
 513         let argsin = map rand (conjuncts(lhand asmin)) in
 514         let argsgen =
 515           map (fun tm -> mk_var(fst(dest_var(rand tm)),type_of tm)) argsin in
 516         let asmgen = subst (zip argsgen argsin) asmin in
 517         let asmquant =
 518           list_mk_forall(snd(strip_comb(rand(rand asmgen))),asmgen) in
 519         let th1 = INST (zip argsin argsgen) (SPEC_ALL (ASSUME asmquant)) in
 520         let th2 = MP th1 (end_itlist CONJ pths) in
 521         let th3 = EQ_MP (SYM conth3) (CONJ tth th2) in
 522         DISCH asmquant (GENL avs (DISCH ant th3))
 523       else
 524         let con = bimp in
 525         let conth2 = BETA_CONV con in
 526         let tth = PART_MATCH I rthm (lhand(rand(concl conth2))) in
 527         let conth3 = PRERULE conth2 in
 528         let asmgen = rand(rand(concl conth3)) in
 529         let asmquant = list_mk_forall(snd(strip_comb(rand asmgen)),asmgen) in
 530         let th2 = SPEC_ALL (ASSUME asmquant) in
 531         let th3 = EQ_MP (SYM conth3) (CONJ tth th2) in
 532         DISCH asmquant (GENL avs th3) in
 533
 534   (* ----------------------------------------------------------------------- *)
 535   (* Finish off a consequence of the induction theorem.                      *)
 536   (* ----------------------------------------------------------------------- *)
 537
 538   let finish_induction_conclusion consindex tybijpairs =
 539     let tybij1,tybij2 = unzip tybijpairs in
 540     let PRERULE =
 541       GEN_REWRITE_RULE (LAND_CONV o LAND_CONV o RAND_CONV) tybij1 o
 542       GEN_REWRITE_RULE LAND_CONV tybij2
 543     and FINRULE = GEN_REWRITE_RULE RAND_CONV tybij1 in
 544     fun th ->
 545       let av,bimp = dest_forall(concl th) in
 546       let pv = lhand(body(rator(rand bimp))) in
 547       let p,v = dest_comb pv in
 548       let mk,dest = assoc p consindex in
 549       let ty = hd(snd(dest_type(type_of dest))) in
 550       let v' = mk_var(fst(dest_var v),ty) in
 551       let dv = mk_comb(dest,v') in
 552       let th1 = PRERULE (SPEC dv th) in
 553       let th2 = MP th1 (REFL (rand(lhand(concl th1)))) in
 554       let th3 = CONV_RULE BETA_CONV th2 in
 555       GEN v' (FINRULE (CONJUNCT2 th3)) in
 556
 557   (* ----------------------------------------------------------------------- *)
 558   (* Derive the induction theorem.                                           *)
 559   (* ----------------------------------------------------------------------- *)
 560
 561   let derive_induction_theorem consindex tybijpairs conthms iith rth =
 562     let bths = map2
 563       (pullback_induction_clause tybijpairs conthms)
 564       (CONJUNCTS rth) (conjuncts(lhand(concl iith))) in
 565     let asm = list_mk_conj(map (lhand o concl) bths) in
 566     let ths = map2 MP bths (CONJUNCTS (ASSUME asm)) in
 567     let th1 = MP iith (end_itlist CONJ ths) in
 568     let th2 = end_itlist CONJ (map
 569       (finish_induction_conclusion consindex tybijpairs) (CONJUNCTS th1)) in
 570     let th3 = DISCH asm th2 in
 571     let preds = map (rator o body o rand) (conjuncts(rand(concl th3))) in
 572     let th4 = GENL preds th3 in
 573     let pasms = filter (C mem (map fst consindex) o lhand) (hyp th4) in
 574     let th5 = itlist DISCH pasms th4 in
 575     let th6,_ = itlist SCRUB_EQUATION (hyp th5) (th5,[]) in
 576     let th7 = UNDISCH_ALL th6 in
 577     fst (itlist SCRUB_EQUATION (hyp th7) (th7,[])) in
 578
 579   (* ----------------------------------------------------------------------- *)
 580   (* Create the recursive functions and eliminate pseudo-constructors.       *)
 581   (* (These are kept just long enough to derive the key property.)           *)
 582   (* ----------------------------------------------------------------------- *)
 583
 584   let create_recursive_functions tybijpairs consindex conthms rth =
 585     let domtys = map (hd o snd o dest_type o type_of o snd o snd) consindex in
 586     let recty = (hd o snd o dest_type o type_of o fst o snd o hd) consindex in
 587     let ranty = mk_vartype "Z" in
 588     let fn = mk_var("fn",mk_fun_ty recty ranty)
 589     and fns = make_args "fn" [] (map (C mk_fun_ty ranty) domtys) in
 590     let args = make_args "a" [] domtys in
 591     let rights = map2 (fun (_,(_,d)) a -> mk_abs(a,mk_comb(fn,mk_comb(d,a))))
 592       consindex args in
 593     let eqs = map2 (curry mk_eq) fns rights in
 594     let fdefs = map ASSUME eqs in
 595     let fxths1 = map (fun th1 -> tryfind (fun th2 -> MK_COMB(th2,th1)) fdefs)
 596       conthms in
 597     let fxths2 = map (fun th -> TRANS th (BETA_CONV (rand(concl th)))) fxths1 in
 598     let mk_tybijcons (th1,th2) =
 599       let th3 = INST [rand(lhand(concl th1)),rand(lhand(concl th2))] th2 in
 600       let th4 = AP_TERM (rator(lhand(rand(concl th2)))) th1 in
 601       EQ_MP (SYM th3) th4 in
 602     let SCONV = GEN_REWRITE_CONV I (map mk_tybijcons tybijpairs)
 603     and ERULE = GEN_REWRITE_RULE I (map snd tybijpairs) in
 604     let simplify_fxthm rthm fxth =
 605       let pat = funpow 4 rand (concl fxth) in
 606       if is_imp(repeat (snd o dest_forall) (concl rthm)) then
 607         let th1 = PART_MATCH (rand o rand) rthm pat in
 608         let tms1 = conjuncts(lhand(concl th1)) in
 609         let ths2 = map (fun t -> EQ_MP (SYM(SCONV t)) TRUTH) tms1 in
 610         ERULE (MP th1 (end_itlist CONJ ths2))
 611       else
 612         ERULE (PART_MATCH rand rthm pat) in
 613     let fxths3 = map2 simplify_fxthm (CONJUNCTS rth) fxths2 in
 614     let fxths4 = map2 (fun th1 -> TRANS th1 o AP_TERM fn) fxths2 fxths3 in
 615     let cleanup_fxthm cth fxth =
 616       let tms = snd(strip_comb(rand(rand(concl fxth)))) in
 617       let kth = RIGHT_BETAS tms (ASSUME (hd(hyp cth))) in
 618       TRANS fxth (AP_TERM fn kth) in
 619     let fxth5 = end_itlist CONJ (map2 cleanup_fxthm conthms fxths4) in
 620     let pasms = filter (C mem (map fst consindex) o lhand) (hyp fxth5) in
 621     let fxth6 = itlist DISCH pasms fxth5 in
 622     let fxth7,_ =
 623       itlist SCRUB_EQUATION (itlist (union o hyp) conthms []) (fxth6,[]) in
 624     let fxth8 = UNDISCH_ALL fxth7 in
 625     fst (itlist SCRUB_EQUATION (subtract (hyp fxth8) eqs) (fxth8,[])) in
 626
 627   (* ----------------------------------------------------------------------- *)
 628   (* Create a function for recursion clause.                                 *)
 629   (* ----------------------------------------------------------------------- *)
 630
 631   let create_recursion_iso_constructor =
 632     let s = `s:num->Z` in
 633     let zty = `:Z` in
 634     let numty = `:num` in
 635     let rec extract_arg tup v =
 636       if v = tup then REFL tup else
 637       let t1,t2 = dest_pair tup in
 638       let PAIR_th = ISPECL [t1;t2] (if free_in v t1 then FST else SND) in
 639       let tup' = rand(concl PAIR_th) in
 640       if tup' = v then PAIR_th else
 641       let th = extract_arg (rand(concl PAIR_th)) v in
 642       SUBS[SYM PAIR_th] th in
 643     fun consindex ->
 644       let recty = hd(snd(dest_type(type_of(fst(hd consindex))))) in
 645       let domty = hd(snd(dest_type recty)) in
 646       let i = mk_var("i",domty)
 647       and r = mk_var("r",mk_fun_ty numty recty) in
 648       let mks = map (fst o snd) consindex in
 649       let mkindex = map (fun t -> hd(tl(snd(dest_type(type_of t)))),t) mks in
 650       fun cth ->
 651         let artms = snd(strip_comb(rand(rand(concl cth)))) in
 652         let artys = mapfilter (type_of o rand) artms in
 653         let args,bod = strip_abs(rand(hd(hyp cth))) in
 654         let ccitm,rtm = dest_comb bod in
 655         let cctm,itm = dest_comb ccitm in
 656         let rargs,iargs = partition (C free_in rtm) args in
 657         let xths = map (extract_arg itm) iargs in
 658         let cargs' = map (subst [i,itm] o lhand o concl) xths in
 659         let indices = map sucivate (0--(length rargs - 1)) in
 660         let rindexed = map (curry mk_comb r) indices in
 661         let rargs' = map2 (fun a rx -> mk_comb(assoc a mkindex,rx))
 662             artys rindexed in
 663         let sargs' = map (curry mk_comb s) indices in
 664         let allargs = cargs'@ rargs' @ sargs' in
 665         let funty = itlist (mk_fun_ty o type_of) allargs zty in
 666         let funname = fst(dest_const(repeat rator (lhand(concl cth))))^"'" in
 667         let funarg = mk_var(funname,funty) in
 668         list_mk_abs([i;r;s],list_mk_comb(funarg,allargs)) in
 669
 670   (* ----------------------------------------------------------------------- *)
 671   (* Derive the recursion theorem.                                           *)
 672   (* ----------------------------------------------------------------------- *)
 673
 674   let derive_recursion_theorem =
 675     let CCONV = funpow 3 RATOR_CONV (REPEATC (GEN_REWRITE_CONV I [FCONS])) in
 676     fun tybijpairs consindex conthms rath ->
 677       let isocons = map (create_recursion_iso_constructor consindex) conthms in
 678       let ty = type_of(hd isocons) in
 679       let fcons = mk_const("FCONS",[ty,aty])
 680       and fnil = mk_const("FNIL",[ty,aty]) in
 681       let bigfun = itlist (mk_binop fcons) isocons fnil in
 682       let eth = ISPEC bigfun CONSTR_REC in
 683       let fn = rator(rand(hd(conjuncts(concl rath)))) in
 684       let betm = let v,bod = dest_abs(rand(concl eth)) in vsubst[fn,v] bod in
 685       let LCONV = REWR_CONV (ASSUME betm) in
 686       let fnths =
 687         map (fun t -> RIGHT_BETAS [bndvar(rand t)] (ASSUME t)) (hyp rath) in
 688       let SIMPER = PURE_REWRITE_RULE
 689         (map SYM fnths @ map fst tybijpairs @ [FST; SND; FCONS; BETA_THM]) in
 690       let hackdown_rath th =
 691         let ltm,rtm = dest_eq(concl th) in
 692         let wargs = snd(strip_comb(rand ltm)) in
 693         let th1 = TRANS th (LCONV rtm) in
 694         let th2 = TRANS th1 (CCONV (rand(concl th1))) in
 695         let th3 = TRANS th2 (funpow 2 RATOR_CONV BETA_CONV (rand(concl th2))) in
 696         let th4 = TRANS th3 (RATOR_CONV BETA_CONV (rand(concl th3))) in
 697         let th5 = TRANS th4 (BETA_CONV (rand(concl th4))) in
 698         GENL wargs (SIMPER th5) in
 699       let rthm = end_itlist CONJ (map hackdown_rath (CONJUNCTS rath)) in
 700       let seqs =
 701         let unseqs = filter is_eq (hyp rthm) in
 702         let tys = map (hd o snd o dest_type o type_of o snd o snd) consindex in
 703         map (fun ty -> find
 704           (fun t -> hd(snd(dest_type(type_of(lhand t)))) = ty) unseqs) tys in
 705       let rethm = itlist EXISTS_EQUATION seqs rthm in
 706       let fethm = CHOOSE(fn,eth) rethm in
 707       let pcons = map (repeat rator o rand o repeat (snd o dest_forall))
 708         (conjuncts(concl rthm)) in
 709       GENL pcons fethm in
 710
 711   (* ----------------------------------------------------------------------- *)
 712   (* Basic function: returns induction and recursion separately. No parser.  *)
 713   (* ----------------------------------------------------------------------- *)
 714
 715   fun def ->
 716     let defs,rth,ith = justify_inductive_type_model def in
 717     let neths = prove_model_inhabitation rth in
 718     let tybijpairs = map (define_inductive_type defs) neths in
 719     let preds = map (repeat rator o concl) neths in
 720     let mkdests = map
 721       (fun (th,_) -> let tm = lhand(concl th) in rator tm,rator(rand tm))
 722       tybijpairs in
 723     let consindex = zip preds mkdests in
 724     let condefs = map (define_inductive_type_constructor defs consindex)
 725                       (CONJUNCTS rth) in
 726     let conthms = map
 727       (fun th -> let args = fst(strip_abs(rand(concl th))) in
 728                  RIGHT_BETAS args th) condefs in
 729     let iith = instantiate_induction_theorem consindex ith in
 730     let fth = derive_induction_theorem consindex tybijpairs conthms iith rth in
 731     let rath = create_recursive_functions tybijpairs consindex conthms rth in
 732     let kth = derive_recursion_theorem tybijpairs consindex conthms rath in
 733     fth,kth;;
 734
 735 (* ------------------------------------------------------------------------- *)
 736 (* Parser to present a nice interface a la Melham.                           *)
 737 (* ------------------------------------------------------------------------- *)
 738
 739 let parse_inductive_type_specification =
 740   let parse_type_loc src =
 741     let pty,rst = parse_pretype src in
 742     type_of_pretype pty,rst in
 743   let parse_type_conapp src =
 744     let cn,sps =
 745      match src with (Ident cn)::sps -> cn,sps
 746                   | _ -> fail() in
 747     let tys,rst = many parse_type_loc sps in
 748     (cn,tys),rst in
 749   let parse_type_clause src =
 750     let tn,sps =
 751       match src with (Ident tn)::sps -> tn,sps
 752                    | _ -> fail() in
 753     let tys,rst = (a (Ident "=") ++ listof parse_type_conapp (a (Resword "|"))
 754                                    "type definition clauses"
 755                    >> snd) sps in
 756     (mk_vartype tn,tys),rst in
 757   let parse_type_definition =
 758     listof parse_type_clause (a (Resword ";")) "type definition" in
 759   fun s ->
 760     let spec,rst = (parse_type_definition o lex o explode) s in
 761     if rst = [] then spec
 762     else failwith "parse_inductive_type_specification: junk after def";;
 763
 764 (* ------------------------------------------------------------------------- *)
 765 (* Use this temporary version to define the sum type.                        *)
 766 (* ------------------------------------------------------------------------- *)
 767
 768 let sum_INDUCT,sum_RECURSION =
 769   define_type_raw (parse_inductive_type_specification "sum = INL A | INR B");;
 770
 771 let OUTL = new_recursive_definition sum_RECURSION
 772   `OUTL (INL x :A+B) = x`;;
 773
 774 let OUTR = new_recursive_definition sum_RECURSION
 775   `OUTR (INR y :A+B) = y`;;
 776
 777 (* ------------------------------------------------------------------------- *)
 778 (* Generalize the recursion theorem to multiple domain types.                *)
 779 (* (We needed to use a single type to justify it via a proforma theorem.)    *)
 780 (*                                                                           *)
 781 (* NB! Before this is called nontrivially (i.e. more than one new type)      *)
 782 (*     the type constructor ":sum", used internally, must have been defined. *)
 783 (* ------------------------------------------------------------------------- *)
 784
 785 let define_type_raw =
 786   let generalize_recursion_theorem =
 787     let ELIM_OUTCOMBS = GEN_REWRITE_RULE TOP_DEPTH_CONV [OUTL; OUTR] in
 788     let rec mk_sum tys =
 789       let k = length tys in
 790       if k = 1 then hd tys else
 791       let tys1,tys2 = chop_list (k / 2) tys in
 792       mk_type("sum",[mk_sum tys1; mk_sum tys2]) in
 793     let mk_inls =
 794       let rec mk_inls ty =
 795         if is_vartype ty then [mk_var("x",ty)] else
 796         let _,[ty1;ty2] = dest_type ty in
 797         let inls1 = mk_inls ty1
 798         and inls2 = mk_inls ty2 in
 799         let inl = mk_const("INL",[ty1,aty; ty2,bty])
 800         and inr = mk_const("INR",[ty1,aty; ty2,bty]) in
 801         map (curry mk_comb inl) inls1 @ map (curry mk_comb inr) inls2 in
 802       fun ty -> let bods = mk_inls ty in
 803                 map (fun t -> mk_abs(find_term is_var t,t)) bods in
 804     let mk_outls =
 805       let rec mk_inls sof ty =
 806         if is_vartype ty then [sof] else
 807         let _,[ty1;ty2] = dest_type ty in
 808         let outl = mk_const("OUTL",[ty1,aty; ty2,bty])
 809         and outr = mk_const("OUTR",[ty1,aty; ty2,bty]) in
 810         mk_inls (mk_comb(outl,sof)) ty1 @ mk_inls (mk_comb(outr,sof)) ty2 in
 811       fun ty -> let x = mk_var("x",ty) in
 812                 map (curry mk_abs x) (mk_inls x ty) in
 813     let mk_newfun fn outl =
 814       let s,ty = dest_var fn in
 815       let dty = hd(snd(dest_type ty)) in
 816       let x = mk_var("x",dty) in
 817       let y,bod = dest_abs outl in
 818       let r = mk_abs(x,vsubst[mk_comb(fn,x),y] bod) in
 819       let l = mk_var(s,type_of r) in
 820       let th1 = ASSUME (mk_eq(l,r)) in
 821       RIGHT_BETAS [x] th1 in
 822     fun th ->
 823       let avs,ebod = strip_forall(concl th) in
 824       let evs,bod = strip_exists ebod in
 825       let n = length evs in
 826       if n = 1 then th else
 827       let tys = map (fun i -> mk_vartype ("Z"^(string_of_int i)))
 828                     (0--(n - 1)) in
 829       let sty = mk_sum tys in
 830       let inls = mk_inls sty
 831       and outls = mk_outls sty in
 832       let zty = type_of(rand(snd(strip_forall(hd(conjuncts bod))))) in
 833       let ith = INST_TYPE [sty,zty] th in
 834       let avs,ebod = strip_forall(concl ith) in
 835       let evs,bod = strip_exists ebod in
 836       let fns' = map2 mk_newfun evs outls in
 837       let fnalist = zip evs (map (rator o lhs o concl) fns')
 838       and inlalist = zip evs inls
 839       and outlalist = zip evs outls in
 840       let hack_clause tm =
 841         let avs,bod = strip_forall tm in
 842         let l,r = dest_eq bod in
 843         let fn,args = strip_comb r in
 844         let pargs = map
 845           (fun a -> let g = genvar(type_of a) in
 846                     if is_var a then g,g else
 847                     let outl = assoc (rator a) outlalist in
 848                     mk_comb(outl,g),g) args in
 849         let args',args'' = unzip pargs in
 850         let inl = assoc (rator l) inlalist in
 851         let rty = hd(snd(dest_type(type_of inl))) in
 852         let nty = itlist (mk_fun_ty o type_of) args' rty in
 853         let fn' = mk_var(fst(dest_var fn),nty) in
 854         let r' = list_mk_abs(args'',mk_comb(inl,list_mk_comb(fn',args'))) in
 855         r',fn in
 856       let defs = map hack_clause (conjuncts bod) in
 857       let jth = BETA_RULE (SPECL (map fst defs) ith) in
 858       let bth = ASSUME (snd(strip_exists(concl jth))) in
 859       let finish_clause th =
 860         let avs,bod = strip_forall (concl th) in
 861         let outl = assoc (rator (lhand bod)) outlalist in
 862         GENL avs (BETA_RULE (AP_TERM outl (SPECL avs th))) in
 863       let cth = end_itlist CONJ (map finish_clause (CONJUNCTS bth)) in
 864       let dth = ELIM_OUTCOMBS cth in
 865       let eth = GEN_REWRITE_RULE ONCE_DEPTH_CONV (map SYM fns') dth in
 866       let fth = itlist SIMPLE_EXISTS (map snd fnalist) eth in
 867       let dtms = map (hd o hyp) fns' in
 868       let gth = itlist (fun e th -> let l,r = dest_eq e in
 869                         MP (INST [r,l] (DISCH e th)) (REFL r)) dtms fth in
 870       let hth = PROVE_HYP jth (itlist SIMPLE_CHOOSE evs gth) in
 871       let xvs = map (fst o strip_comb o rand o snd o strip_forall)
 872                     (conjuncts(concl eth)) in
 873       GENL xvs hth in
 874   fun def -> let ith,rth = define_type_raw def in
 875              ith,generalize_recursion_theorem rth;;
 876
 877 (* ------------------------------------------------------------------------- *)
 878 (* Set up options and lists.                                                 *)
 879 (* ------------------------------------------------------------------------- *)
 880
 881 let option_INDUCT,option_RECURSION =
 882   define_type_raw
 883    (parse_inductive_type_specification "option = NONE | SOME A");;
 884
 885 let list_INDUCT,list_RECURSION =
 886   define_type_raw
 887    (parse_inductive_type_specification "list = NIL | CONS A list");;
 888
 889 (* ------------------------------------------------------------------------- *)
 890 (* Tools for proving injectivity and distinctness of constructors.           *)
 891 (* ------------------------------------------------------------------------- *)
 892
 893 let prove_constructors_injective =
 894   let DEPAIR = GEN_REWRITE_RULE TOP_SWEEP_CONV [PAIR_EQ] in
 895   let prove_distinctness ax pat =
 896     let f,args = strip_comb pat in
 897     let rt = end_itlist (curry mk_pair) args in
 898     let ty = mk_fun_ty (type_of pat) (type_of rt) in
 899     let fn = genvar ty in
 900     let dtm = mk_eq(mk_comb(fn,pat),rt) in
 901     let eth = prove_recursive_functions_exist ax (list_mk_forall(args,dtm)) in
 902     let args' = variants args args in
 903     let atm = mk_eq(pat,list_mk_comb(f,args')) in
 904     let ath = ASSUME atm in
 905     let bth = AP_TERM fn ath in
 906     let cth1 = SPECL args (ASSUME(snd(dest_exists(concl eth)))) in
 907     let cth2 = INST (zip args' args) cth1 in
 908     let pth = TRANS (TRANS (SYM cth1) bth) cth2 in
 909     let qth = DEPAIR pth in
 910     let qtm = concl qth in
 911     let rth = rev_itlist (C(curry MK_COMB)) (CONJUNCTS(ASSUME qtm)) (REFL f) in
 912     let tth = IMP_ANTISYM_RULE (DISCH atm qth) (DISCH qtm rth) in
 913     let uth = GENL args (GENL args' tth) in
 914     PROVE_HYP eth (SIMPLE_CHOOSE fn uth) in
 915   fun ax ->
 916     let cls = conjuncts(snd(strip_exists(snd(strip_forall(concl ax))))) in
 917     let pats = map (rand o lhand o snd o strip_forall) cls in
 918     end_itlist CONJ (mapfilter (prove_distinctness ax) pats);;
 919
 920 let prove_constructors_distinct =
 921   let num_ty = `:num` in
 922   let rec allopairs f l m =
 923     if l = [] then [] else
 924     map (f (hd l)) (tl m) @ allopairs f (tl l) (tl m) in
 925   let NEGATE = GEN_ALL o CONV_RULE (REWR_CONV (TAUT `a ==> F <=> ~a`)) in
 926   let prove_distinct ax pat =
 927     let nums = map mk_small_numeral (0--(length pat - 1)) in
 928     let fn = genvar (mk_type("fun",[type_of(hd pat); num_ty])) in
 929     let ls = map (curry mk_comb fn) pat in
 930     let defs = map2 (fun l r -> list_mk_forall(frees (rand l),mk_eq(l,r)))
 931       ls nums in
 932     let eth = prove_recursive_functions_exist ax (list_mk_conj defs) in
 933     let ev,bod = dest_exists(concl eth) in
 934     let REWRITE = GEN_REWRITE_RULE ONCE_DEPTH_CONV (CONJUNCTS (ASSUME bod)) in
 935     let pat' = map
 936      (fun t -> let f,args = if is_numeral t then t,[] else strip_comb t in
 937                list_mk_comb(f,variants args args)) pat in
 938     let pairs = allopairs (curry mk_eq) pat pat' in
 939     let nths = map (REWRITE o AP_TERM fn o ASSUME) pairs in
 940     let fths = map2 (fun t th -> NEGATE (DISCH t (CONV_RULE NUM_EQ_CONV th)))
 941       pairs nths in
 942     CONJUNCTS(PROVE_HYP eth (SIMPLE_CHOOSE ev (end_itlist CONJ fths))) in
 943   fun ax ->
 944     let cls = conjuncts(snd(strip_exists(snd(strip_forall(concl ax))))) in
 945     let lefts = map (dest_comb o lhand o snd o strip_forall) cls in
 946     let fns = itlist (insert o fst) lefts [] in
 947     let pats = map (fun f -> map snd (filter ((=)f o fst) lefts)) fns in
 948     end_itlist CONJ
 949      (end_itlist (@) (mapfilter (prove_distinct ax) pats));;
 950
 951 (* ------------------------------------------------------------------------- *)
 952 (* Automatically prove the case analysis theorems.                           *)
 953 (* ------------------------------------------------------------------------- *)
 954
 955 let prove_cases_thm =
 956   let mk_exclauses x rpats =
 957     let xts = map (fun t -> list_mk_exists(frees t,mk_eq(x,t))) rpats in
 958     mk_abs(x,list_mk_disj xts) in
 959   let prove_triv tm =
 960     let evs,bod = strip_exists tm in
 961     let l,r = dest_eq bod in
 962     if l = r then REFL l else
 963     let lf,largs = strip_comb l
 964     and rf,rargs = strip_comb r in
 965     if lf = rf then
 966       let ths = map (ASSUME o mk_eq) (zip rargs largs) in
 967       let th1 = rev_itlist (C (curry MK_COMB)) ths (REFL lf) in
 968       itlist EXISTS_EQUATION (map concl ths) (SYM th1)
 969     else failwith "prove_triv" in
 970   let rec prove_disj tm =
 971     if is_disj tm then
 972       let l,r = dest_disj tm in
 973       try DISJ1 (prove_triv l) r
 974       with Failure _ -> DISJ2 l (prove_disj r)
 975     else
 976       prove_triv tm in
 977   let prove_eclause tm =
 978     let avs,bod = strip_forall tm in
 979     let ctm = if is_imp bod then rand bod else bod in
 980     let cth = prove_disj ctm in
 981     let dth = if is_imp bod then DISCH (lhand bod) cth else cth in
 982     GENL avs dth in
 983   fun th ->
 984     let avs,bod = strip_forall(concl th) in
 985     let cls = map (snd o strip_forall) (conjuncts(lhand bod)) in
 986     let pats = map (fun t -> if is_imp t then rand t else t) cls in
 987     let spats = map dest_comb pats in
 988     let preds = itlist (insert o fst) spats [] in
 989     let rpatlist = map
 990       (fun pr -> map snd (filter (fun (p,x) -> p = pr) spats)) preds in
 991     let xs = make_args "x" (freesl pats) (map (type_of o hd) rpatlist) in
 992     let xpreds = map2 mk_exclauses xs rpatlist in
 993     let ith = BETA_RULE (INST (zip xpreds preds) (SPEC_ALL th)) in
 994     let eclauses = conjuncts(fst(dest_imp(concl ith))) in
 995     MP ith (end_itlist CONJ (map prove_eclause eclauses));;
 996
 997 (* ------------------------------------------------------------------------- *)
 998 (* Now deal with nested recursion. Need a store of previous theorems.        *)
 999 (* ------------------------------------------------------------------------- *)
1000
1001 inductive_type_store :=
1002  ["list",(2,list_INDUCT,list_RECURSION);
1003   "option",(2,option_INDUCT,option_RECURSION);
1004   "sum",(2,sum_INDUCT,sum_RECURSION)] @
1005  (!inductive_type_store);;
1006
1007 (* ------------------------------------------------------------------------- *)
1008 (* Also add a cached rewrite of distinctness and injectivity theorems. Since *)
1009 (* there can be quadratically many distinctness clauses, it would really be  *)
1010 (* preferable to have a conversion, but this seems OK up 100 constructors.   *)
1011 (* ------------------------------------------------------------------------- *)
1012
1013 let basic_rectype_net = ref empty_net;;
1014 let distinctness_store = ref ["bool",TAUT `(T <=> F) <=> F`];;
1015 let injectivity_store = ref [];;
1016
1017 let extend_rectype_net (tyname,(_,_,rth)) =
1018   let ths1 = try [prove_constructors_distinct rth] with Failure _ -> []
1019   and ths2 = try [prove_constructors_injective rth] with Failure _ -> [] in
1020   let canon_thl = itlist (mk_rewrites false) (ths1 @ ths2) [] in
1021   distinctness_store := map (fun th -> tyname,th) ths1 @ (!distinctness_store);
1022   injectivity_store := map (fun th -> tyname,th) ths2 @ (!injectivity_store);
1023   basic_rectype_net :=
1024     itlist (net_of_thm true) canon_thl (!basic_rectype_net);;
1025
1026 do_list extend_rectype_net (!inductive_type_store);;
1027
1028 (* ------------------------------------------------------------------------- *)
1029 (* Return distinctness and injectivity for a type by simple lookup.          *)
1030 (* ------------------------------------------------------------------------- *)
1031
1032 let distinctness ty = assoc ty (!distinctness_store);;
1033
1034 let injectivity ty = assoc ty (!injectivity_store);;
1035
1036 let cases ty =
1037   if ty = "num" then num_CASES else
1038   let _,ith,_ = assoc ty (!inductive_type_store) in prove_cases_thm ith;;
1039
1040 (* ------------------------------------------------------------------------- *)
1041 (* Convenient definitions for type isomorphism.                              *)
1042 (* ------------------------------------------------------------------------- *)
1043
1044 let ISO = new_definition
1045   `ISO (f:A->B) (g:B->A) <=> (!x. f(g x) = x) /\ (!y. g(f y) = y)`;;
1046
1047 let ISO_REFL = prove
1048  (`ISO (\x:A. x) (\x. x)`,
1049   REWRITE_TAC[ISO]);;
1050
1051 let ISO_FUN = prove
1052  (`ISO (f:A->A') f' /\ ISO (g:B->B') g'
1053    ==> ISO (\h a'. g(h(f' a'))) (\h a. g'(h(f a)))`,
1054   REWRITE_TAC[ISO; FUN_EQ_THM] THEN MESON_TAC[]);;
1055
1056 let ISO_USAGE = prove
1057  (`ISO f g
1058    ==> (!P. (!x. P x) <=> (!x. P(g x))) /\
1059        (!P. (?x. P x) <=> (?x. P(g x))) /\
1060        (!a b. (a = g b) <=> (f a = b))`,
1061   REWRITE_TAC[ISO; FUN_EQ_THM] THEN MESON_TAC[]);;
1062
1063 (* ------------------------------------------------------------------------- *)
1064 (* Hence extend type definition to nested types.                             *)
1065 (* ------------------------------------------------------------------------- *)
1066
1067 let define_type_raw =
1068
1069   (* ----------------------------------------------------------------------- *)
1070   (* Dispose of trivial antecedent.                                          *)
1071   (* ----------------------------------------------------------------------- *)
1072
1073   let TRIV_ANTE_RULE =
1074     let TRIV_IMP_CONV tm =
1075       let avs,bod = strip_forall tm in
1076       let bth =
1077         if is_eq bod then REFL (rand bod) else
1078         let ant,con = dest_imp bod in
1079         let ith = SUBS_CONV (CONJUNCTS(ASSUME ant)) (lhs con) in
1080         DISCH ant ith in
1081       GENL avs bth in
1082     fun th ->
1083       let tm = concl th in
1084       if is_imp tm then
1085         let ant,con = dest_imp(concl th) in
1086         let cjs = conjuncts ant in
1087         let cths = map TRIV_IMP_CONV cjs in
1088         MP th (end_itlist CONJ cths)
1089       else th in
1090
1091   (* ----------------------------------------------------------------------- *)
1092   (* Lift type bijections to "arbitrary" (well, free rec or function) type.  *)
1093   (* ----------------------------------------------------------------------- *)
1094
1095   let ISO_EXPAND_CONV = PURE_ONCE_REWRITE_CONV[ISO] in
1096
1097   let rec lift_type_bijections iths cty =
1098     let itys = map (hd o snd o dest_type o type_of o lhand o concl) iths in
1099     try assoc cty (zip itys iths) with Failure _ ->
1100     if not (exists (C occurs_in cty) itys)
1101     then INST_TYPE [cty,aty] ISO_REFL else
1102     let tycon,isotys = dest_type cty in
1103     if tycon = "fun"
1104     then MATCH_MP ISO_FUN
1105            (end_itlist CONJ (map (lift_type_bijections iths) isotys))
1106     else failwith
1107             ("lift_type_bijections: Unexpected type operator \""^tycon^"\"") in
1108
1109   (* ----------------------------------------------------------------------- *)
1110   (* Prove isomorphism of nested types where former is the smaller.          *)
1111   (* ----------------------------------------------------------------------- *)
1112
1113   let DE_EXISTENTIALIZE_RULE =
1114     let pth = prove
1115      (`(?) P ==> (c = (@)P) ==> P c`,
1116       GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
1117       DISCH_TAC THEN DISCH_THEN SUBST1_TAC THEN
1118       MATCH_MP_TAC SELECT_AX THEN POP_ASSUM ACCEPT_TAC) in
1119     let USE_PTH = MATCH_MP pth in
1120     let rec DE_EXISTENTIALIZE_RULE th =
1121       if not (is_exists(concl th)) then [],th else
1122       let th1 = USE_PTH th in
1123       let v1 = rand(rand(concl th1)) in
1124       let gv = genvar(type_of v1) in
1125       let th2 = CONV_RULE BETA_CONV (UNDISCH (INST [gv,v1] th1)) in
1126       let vs,th3 = DE_EXISTENTIALIZE_RULE th2 in
1127       gv::vs,th3 in
1128     DE_EXISTENTIALIZE_RULE in
1129
1130   let grab_type = type_of o rand o lhand o snd o strip_forall in
1131
1132   let clause_corresponds cl0  =
1133     let f0,ctm0 = dest_comb (lhs cl0) in
1134     let c0 = fst(dest_const(fst(strip_comb ctm0))) in
1135     let dty0,rty0 = dest_fun_ty (type_of f0) in
1136     fun cl1 ->
1137       let f1,ctm1 = dest_comb (lhs cl1) in
1138       let c1 = fst(dest_const(fst(strip_comb ctm1))) in
1139       let dty1,rty1 = dest_fun_ty (type_of f1) in
1140       c0 = c1 & dty0 = rty1 & rty0 = dty1 in
1141
1142   let prove_inductive_types_isomorphic n k (ith0,rth0) (ith1,rth1) =
1143     let sth0 = SPEC_ALL rth0
1144     and sth1 = SPEC_ALL rth1
1145     and t_tm = concl TRUTH in
1146     let pevs0,pbod0 = strip_exists (concl sth0)
1147     and pevs1,pbod1 = strip_exists (concl sth1) in
1148     let pcjs0,qcjs0 = chop_list k (conjuncts pbod0)
1149     and pcjs1,qcjs1 = chop_list k (snd(chop_list n (conjuncts pbod1))) in
1150     let tyal0 = setify (zip (map grab_type pcjs1) (map grab_type pcjs0)) in
1151     let tyal1 = map (fun (a,b) -> (b,a)) tyal0 in
1152     let tyins0 = map
1153      (fun f -> let domty,ranty = dest_fun_ty (type_of f) in
1154                tysubst tyal0 domty,ranty) pevs0
1155     and tyins1 = map
1156      (fun f -> let domty,ranty = dest_fun_ty (type_of f) in
1157                tysubst tyal1 domty,ranty) pevs1 in
1158     let tth0 = INST_TYPE tyins0 sth0
1159     and tth1 = INST_TYPE tyins1 sth1 in
1160     let evs0,bod0 = strip_exists(concl tth0)
1161     and evs1,bod1 = strip_exists(concl tth1) in
1162     let lcjs0,rcjs0 = chop_list k (map (snd o strip_forall) (conjuncts bod0))
1163     and lcjs1,rcjsx = chop_list k (map (snd o strip_forall)
1164       (snd(chop_list n (conjuncts bod1)))) in
1165     let rcjs1 =  map (fun t -> find (clause_corresponds t) rcjsx) rcjs0 in
1166     let proc_clause tm0 tm1 =
1167       let l0,r0 = dest_eq tm0
1168       and l1,r1 = dest_eq tm1 in
1169       let vc0,wargs0 = strip_comb r0 in
1170       let con0,vargs0 = strip_comb(rand l0) in
1171       let gargs0 = map (genvar o type_of) wargs0 in
1172       let nestf0 = map (fun a -> can (find (fun t -> is_comb t & rand t = a))
1173         wargs0) vargs0 in
1174       let targs0 = map2 (fun a f ->
1175         if f then find (fun t -> is_comb t & rand t = a) wargs0 else a)
1176          vargs0 nestf0 in
1177       let gvlist0 = zip wargs0 gargs0 in
1178       let xargs = map (fun v -> assoc v gvlist0) targs0 in
1179       let inst0 =
1180         list_mk_abs(gargs0,list_mk_comb(fst(strip_comb(rand l1)),xargs)),vc0 in
1181       let vc1,wargs1 = strip_comb r1 in
1182       let con1,vargs1 = strip_comb(rand l1) in
1183       let gargs1 = map (genvar o type_of) wargs1 in
1184       let targs1 = map2
1185         (fun a f -> if f then
1186                     find (fun t -> is_comb t & rand t = a) wargs1
1187                     else a) vargs1 nestf0 in
1188       let gvlist1 = zip wargs1 gargs1 in
1189       let xargs = map (fun v -> assoc v gvlist1) targs1 in
1190       let inst1 =
1191         list_mk_abs(gargs1,list_mk_comb(fst(strip_comb(rand l0)),xargs)),vc1 in
1192       inst0,inst1 in
1193     let insts0,insts1 = unzip (map2 proc_clause (lcjs0@rcjs0) (lcjs1@rcjs1)) in
1194     let uth0 = BETA_RULE(INST insts0 tth0)
1195     and uth1 = BETA_RULE(INST insts1 tth1) in
1196     let efvs0,sth0 = DE_EXISTENTIALIZE_RULE uth0
1197     and efvs1,sth1 = DE_EXISTENTIALIZE_RULE uth1 in
1198     let efvs2 = map
1199      (fun t1 -> find (fun t2 -> hd(tl(snd(dest_type(type_of t1)))) =
1200                                 hd(snd(dest_type(type_of t2)))) efvs1) efvs0 in
1201     let isotms = map2 (fun ff gg -> list_mk_icomb "ISO" [ff;gg]) efvs0 efvs2 in
1202     let ctm = list_mk_conj isotms in
1203     let cth1 = ISO_EXPAND_CONV ctm in
1204     let ctm1 = rand(concl cth1) in
1205     let cjs = conjuncts ctm1 in
1206     let eee = map (fun n -> n mod 2 = 0) (0--(length cjs - 1)) in
1207     let cjs1,cjs2 = partition fst (zip eee cjs) in
1208     let ctm2 = mk_conj(list_mk_conj (map snd cjs1),
1209                        list_mk_conj (map snd cjs2)) in
1210     let DETRIV_RULE = TRIV_ANTE_RULE o REWRITE_RULE[sth0;sth1] in
1211     let jth0 =
1212       let itha = SPEC_ALL ith0 in
1213       let icjs = conjuncts(rand(concl itha)) in
1214       let cinsts = map
1215         (fun tm -> tryfind (fun vtm -> term_match [] vtm tm) icjs)
1216         (conjuncts (rand ctm2)) in
1217       let tvs = subtract (fst(strip_forall(concl ith0)))
1218                   (itlist (fun (_,x,_) -> union (map snd x)) cinsts []) in
1219       let ctvs =
1220         map (fun p -> let x = mk_var("x",hd(snd(dest_type(type_of p)))) in
1221                              mk_abs(x,t_tm),p) tvs in
1222       DETRIV_RULE (INST ctvs (itlist INSTANTIATE cinsts itha))
1223     and jth1 =
1224       let itha = SPEC_ALL ith1 in
1225       let icjs = conjuncts(rand(concl itha)) in
1226       let cinsts = map
1227         (fun tm -> tryfind (fun vtm -> term_match [] vtm tm) icjs)
1228         (conjuncts (lhand ctm2)) in
1229       let tvs = subtract (fst(strip_forall(concl ith1)))
1230                     (itlist (fun (_,x,_) -> union (map snd x)) cinsts []) in
1231       let ctvs =
1232         map (fun p -> let x = mk_var("x",hd(snd(dest_type(type_of p)))) in
1233                                mk_abs(x,t_tm),p) tvs in
1234       DETRIV_RULE (INST ctvs (itlist INSTANTIATE cinsts itha)) in
1235     let cths4 = map2 CONJ (CONJUNCTS jth0) (CONJUNCTS jth1) in
1236     let cths5 = map (PURE_ONCE_REWRITE_RULE[GSYM ISO]) cths4 in
1237     let cth6 = end_itlist CONJ cths5 in
1238     cth6,CONJ sth0 sth1 in
1239
1240   (* ----------------------------------------------------------------------- *)
1241   (* Define nested type by doing a 1-level unwinding.                        *)
1242   (* ----------------------------------------------------------------------- *)
1243
1244   let SCRUB_ASSUMPTION th =
1245     let hyps = hyp th in
1246     let eqn = find (fun t -> let x = lhs t in
1247                              forall (fun u -> not (free_in x (rand u))) hyps)
1248                    hyps in
1249     let l,r = dest_eq eqn in
1250     MP (INST [r,l] (DISCH eqn th)) (REFL r) in
1251
1252   let define_type_basecase def =
1253     let add_id s = fst(dest_var(genvar bool_ty)) in
1254     let def' = map (I F_F (map (add_id F_F I))) def in
1255     define_type_raw def' in
1256
1257   let SIMPLE_BETA_RULE = GSYM o PURE_REWRITE_RULE[BETA_THM; FUN_EQ_THM] in
1258   let ISO_USAGE_RULE = MATCH_MP ISO_USAGE in
1259   let SIMPLE_ISO_EXPAND_RULE = CONV_RULE(REWR_CONV ISO) in
1260
1261   let REWRITE_FUN_EQ_RULE =
1262     let ths = itlist (mk_rewrites false) [FUN_EQ_THM] [] in
1263     let net = itlist (net_of_thm false) ths (basic_net()) in
1264     CONV_RULE o GENERAL_REWRITE_CONV true TOP_DEPTH_CONV net in
1265
1266   let is_nested vs ty =
1267     not (is_vartype ty) & not (intersect (tyvars ty) vs = []) in
1268   let rec modify_type alist ty =
1269     try rev_assoc ty alist
1270     with Failure _ -> try
1271         let tycon,tyargs = dest_type ty in
1272         mk_type(tycon,map (modify_type alist) tyargs)
1273     with Failure _ -> ty in
1274   let modify_item alist (s,l) =
1275     s,map (modify_type alist) l in
1276   let modify_clause alist (l,lis) =
1277      l,map (modify_item alist) lis in
1278   let recover_clause id tm =
1279     let con,args = strip_comb tm in
1280     fst(dest_const con)^id,map type_of args in
1281   let rec create_auxiliary_clauses nty =
1282     let id = fst(dest_var(genvar bool_ty)) in
1283     let tycon,tyargs = dest_type nty in
1284     let k,ith,rth = try assoc tycon (!inductive_type_store) with Failure _ ->
1285       failwith ("Can't find definition for nested type: "^tycon) in
1286     let evs,bod = strip_exists(snd(strip_forall(concl rth))) in
1287     let cjs = map (lhand o snd o strip_forall) (conjuncts bod) in
1288     let rtys = map (hd o snd o dest_type o type_of) evs in
1289     let tyins = tryfind (fun vty -> type_match vty nty []) rtys in
1290     let cjs' = map (inst tyins o rand) (fst(chop_list k cjs)) in
1291     let mtys = itlist (insert o type_of) cjs' [] in
1292     let pcons = map (fun ty -> filter (fun t -> type_of t = ty) cjs') mtys in
1293     let cls' = zip mtys (map (map (recover_clause id)) pcons) in
1294     let tyal = map (fun ty -> mk_vartype(fst(dest_type ty)^id),ty) mtys in
1295     let cls'' = map (modify_type tyal F_F map (modify_item tyal)) cls' in
1296     k,tyal,cls'',INST_TYPE tyins ith,INST_TYPE tyins rth in
1297   let rec define_type_nested def =
1298     let n = length(itlist (@) (map (map fst o snd) def) []) in
1299     let newtys = map fst def in
1300     let utys = unions (itlist (union o map snd o snd) def []) in
1301     let rectys = filter (is_nested newtys) utys in
1302     if rectys = [] then
1303       let th1,th2 = define_type_basecase def in n,th1,th2 else
1304     let nty = hd (sort (fun t1 t2 -> occurs_in t2 t1) rectys) in
1305     let k,tyal,ncls,ith,rth = create_auxiliary_clauses nty in
1306     let cls = map (modify_clause tyal) def @ ncls in
1307     let _,ith1,rth1 = define_type_nested cls in
1308     let xnewtys = map (hd o snd o dest_type o type_of)
1309                       (fst(strip_exists(snd(strip_forall(concl rth1))))) in
1310     let xtyal = map (fun ty -> let s = dest_vartype ty in
1311                                find (fun t -> fst(dest_type t) = s) xnewtys,ty)
1312                     (map fst cls) in
1313     let ith0 = INST_TYPE xtyal ith
1314     and rth0 = INST_TYPE xtyal rth in
1315     let isoth,rclauses =
1316       prove_inductive_types_isomorphic n k (ith0,rth0) (ith1,rth1) in
1317     let irth3 = CONJ ith1 rth1 in
1318     let vtylist = itlist (insert o type_of) (variables(concl irth3)) [] in
1319     let isoths = CONJUNCTS isoth in
1320     let isotys = map (hd o snd o dest_type o type_of o lhand o concl) isoths in
1321     let ctylist = filter
1322       (fun ty -> exists (fun t -> occurs_in t ty) isotys) vtylist in
1323     let atylist = itlist
1324       (union o striplist dest_fun_ty) ctylist [] in
1325     let isoths' = map (lift_type_bijections isoths)
1326       (filter (fun ty -> exists (fun t -> occurs_in t ty) isotys) atylist) in
1327     let cisoths = map (BETA_RULE o lift_type_bijections isoths')
1328       ctylist in
1329     let uisoths = map ISO_USAGE_RULE cisoths in
1330     let visoths = map (ASSUME o concl) uisoths in
1331     let irth4 = itlist PROVE_HYP uisoths (REWRITE_FUN_EQ_RULE visoths irth3) in
1332     let irth5 = REWRITE_RULE
1333       (rclauses :: map SIMPLE_ISO_EXPAND_RULE isoths') irth4 in
1334     let irth6 = repeat SCRUB_ASSUMPTION irth5 in
1335     let ncjs = filter (fun t -> exists (fun v -> not(is_var v))
1336                              (snd(strip_comb(rand(lhs(snd(strip_forall t)))))))
1337                       (conjuncts(snd(strip_exists
1338                          (snd(strip_forall(rand(concl irth6))))))) in
1339     let mk_newcon tm =
1340       let vs,bod = strip_forall tm in
1341       let rdeb = rand(lhs bod) in
1342       let rdef = list_mk_abs(vs,rdeb) in
1343       let newname = fst(dest_var(genvar bool_ty)) in
1344       let def = mk_eq(mk_var(newname,type_of rdef),rdef) in
1345       let dth = new_definition def in
1346       SIMPLE_BETA_RULE dth in
1347     let dths = map mk_newcon ncjs in
1348     let ith6,rth6 = CONJ_PAIR(PURE_REWRITE_RULE dths irth6) in
1349     n,ith6,rth6 in
1350   fun def ->
1351     let newtys = map fst def in
1352     let truecons = itlist (@) (map (map fst o snd) def) [] in
1353     let (p,ith0,rth0) = define_type_nested def in
1354     let avs,etm = strip_forall(concl rth0) in
1355     let allcls = conjuncts(snd(strip_exists etm)) in
1356     let relcls = fst(chop_list (length truecons) allcls) in
1357     let gencons =
1358       map (repeat rator o rand o lhand o snd o strip_forall) relcls in
1359     let cdefs =
1360       map2 (fun s r -> SYM(new_definition (mk_eq(mk_var(s,type_of r),r))))
1361            truecons gencons in
1362     let tavs = make_args "f" [] (map type_of avs) in
1363     let ith1 = SUBS cdefs ith0
1364     and rth1 = GENL tavs (SUBS cdefs (SPECL tavs rth0)) in
1365     let retval = p,ith1,rth1 in
1366     let newentries = map (fun s -> dest_vartype s,retval) newtys in
1367     (inductive_type_store := newentries @ (!inductive_type_store);
1368      do_list extend_rectype_net newentries; ith1,rth1);;
1369
1370 (* ----------------------------------------------------------------------- *)
1371 (* The overall function, with rather crude string-based benignity.         *)
1372 (* ----------------------------------------------------------------------- *)
1373
1374 let the_inductive_types = ref
1375  ["list = NIL | CONS A list",(list_INDUCT,list_RECURSION);
1376   "option = NONE | SOME A",(option_INDUCT,option_RECURSION);
1377   "sum = INL A | INR B",(sum_INDUCT,sum_RECURSION)];;
1378
1379 let define_type s =
1380   try let retval = assoc s (!the_inductive_types) in
1381       (warn true "Benign redefinition of inductive type"; retval)
1382   with Failure _ ->
1383       let defspec = parse_inductive_type_specification s in
1384       let newtypes = map fst defspec
1385       and constructors = itlist ((@) o map fst) (map snd defspec) [] in
1386       if not(length(setify newtypes) = length newtypes)
1387       then failwith "define_type: multiple definitions of a type"
1388       else if not(length(setify constructors) = length constructors)
1389       then failwith "define_type: multiple instances of a constructor"
1390       else if exists (can get_type_arity o dest_vartype) newtypes
1391       then let t = find (can get_type_arity) (map dest_vartype newtypes) in
1392            failwith("define_type: type :"^t^" already defined")
1393       else if exists (can get_const_type) constructors
1394       then let t = find (can get_const_type) constructors in
1395            failwith("define_type: constant "^t^" already defined")
1396       else
1397         let retval = define_type_raw defspec in
1398         the_inductive_types := (s,retval)::(!the_inductive_types); retval;;
1399
1400 (* ------------------------------------------------------------------------- *)
1401 (* Unwinding, and application of patterns. Add easy cases to default net.    *)
1402 (* ------------------------------------------------------------------------- *)
1403
1404 let UNWIND_CONV,MATCH_CONV =
1405   let pth_0 = prove
1406    (`(if ?!x. x = a /\ p then @x. x = a /\ p else @x. F) =
1407      (if p then a else @x. F)`,
1408     BOOL_CASES_TAC `p:bool` THEN ASM_REWRITE_TAC[COND_ID] THEN
1409     MESON_TAC[])
1410   and pth_1 = prove
1411    (`_MATCH x (_SEQPATTERN r s) =
1412      (if ?y. r x y then _MATCH x r else _MATCH x s) /\
1413     _FUNCTION (_SEQPATTERN r s) x =
1414      (if ?y. r x y then _FUNCTION r x else _FUNCTION s x)`,
1415     REWRITE_TAC[_MATCH; _SEQPATTERN; _FUNCTION] THEN
1416     MESON_TAC[])
1417   and pth_2 = prove
1418    (`((?y. _UNGUARDED_PATTERN (GEQ s t) (GEQ u y)) <=> s = t) /\
1419      ((?y. _GUARDED_PATTERN (GEQ s t) p (GEQ u y)) <=> s = t /\ p)`,
1420     REWRITE_TAC[_UNGUARDED_PATTERN; _GUARDED_PATTERN; GEQ_DEF] THEN
1421     MESON_TAC[])
1422   and pth_3 = prove
1423    (`(_MATCH x (\y z. P y z) = if ?!z. P x z then @z. P x z else @x. F) /\
1424      (_FUNCTION (\y z. P y z) x = if ?!z. P x z then @z. P x z else @x. F)`,
1425     REWRITE_TAC[_MATCH; _FUNCTION])
1426   and pth_4 = prove
1427    (`(_UNGUARDED_PATTERN (GEQ s t) (GEQ u y) <=> y = u /\ s = t) /\
1428      (_GUARDED_PATTERN (GEQ s t) p (GEQ u y) <=> y = u /\ s = t /\ p)`,
1429     REWRITE_TAC[_UNGUARDED_PATTERN; _GUARDED_PATTERN; GEQ_DEF] THEN
1430     MESON_TAC[])
1431   and pth_5 = prove
1432    (`(if ?!z. z = k then @z. z = k else @x. F) = k`,
1433     MESON_TAC[]) in
1434   let rec INSIDE_EXISTS_CONV conv tm =
1435     if is_exists tm then BINDER_CONV (INSIDE_EXISTS_CONV conv) tm
1436     else conv tm in
1437   let PUSH_EXISTS_CONV =
1438     let econv = REWR_CONV SWAP_EXISTS_THM in
1439     let rec conv bc tm =
1440       try (econv THENC BINDER_CONV(conv bc)) tm
1441       with Failure _ -> bc tm in
1442     conv in
1443   let BREAK_CONS_CONV =
1444     let conv2 = GEN_REWRITE_CONV DEPTH_CONV [AND_CLAUSES; OR_CLAUSES] THENC
1445                 ASSOC_CONV CONJ_ASSOC in
1446     fun tm ->
1447       let conv0 = TOP_SWEEP_CONV(REWRITES_CONV(!basic_rectype_net)) in
1448       let conv1 = if is_conj tm then LAND_CONV conv0 else conv0 in
1449       (conv1 THENC conv2) tm in
1450   let UNWIND_CONV =
1451     let baseconv = GEN_REWRITE_CONV I
1452       [UNWIND_THM1; UNWIND_THM2;
1453        EQT_INTRO(SPEC_ALL EXISTS_REFL);
1454        EQT_INTRO(GSYM(SPEC_ALL EXISTS_REFL))] in
1455     let rec UNWIND_CONV tm =
1456       let evs,bod = strip_exists tm in
1457       let eqs = conjuncts bod in
1458       try let eq = find
1459            (fun tm -> is_eq tm &
1460                       let l,r = dest_eq tm in
1461                       (mem l evs & not (free_in l r)) or
1462                       (mem r evs & not (free_in r l))) eqs in
1463           let l,r = dest_eq eq in
1464           let v = if mem l evs & not (free_in l r) then l else r in
1465           let cjs' = eq::(subtract eqs [eq]) in
1466           let n = length evs - (1 + index v (rev evs)) in
1467           let th1 = CONJ_ACI_RULE(mk_eq(bod,list_mk_conj cjs')) in
1468           let th2 = itlist MK_EXISTS evs th1 in
1469           let th3 = funpow n BINDER_CONV (PUSH_EXISTS_CONV baseconv)
1470                       (rand(concl th2)) in
1471           CONV_RULE (RAND_CONV UNWIND_CONV) (TRANS th2 th3)
1472        with Failure _ -> REFL tm in
1473      UNWIND_CONV in
1474   let MATCH_SEQPATTERN_CONV =
1475     GEN_REWRITE_CONV I [pth_1] THENC
1476     RATOR_CONV(LAND_CONV
1477      (BINDER_CONV(RATOR_CONV BETA_CONV THENC BETA_CONV) THENC
1478       PUSH_EXISTS_CONV(GEN_REWRITE_CONV I [pth_2] THENC BREAK_CONS_CONV) THENC
1479       UNWIND_CONV THENC
1480       GEN_REWRITE_CONV DEPTH_CONV
1481        [EQT_INTRO(SPEC_ALL EQ_REFL); AND_CLAUSES] THENC
1482       GEN_REWRITE_CONV DEPTH_CONV [EXISTS_SIMP]))
1483   and MATCH_ONEPATTERN_CONV tm =
1484     let th1 = GEN_REWRITE_CONV I [pth_3] tm in
1485     let tm' = body(rand(lhand(rand(concl th1)))) in
1486     let th2 = (INSIDE_EXISTS_CONV
1487                 (GEN_REWRITE_CONV I [pth_4] THENC
1488                  RAND_CONV BREAK_CONS_CONV) THENC
1489                UNWIND_CONV THENC
1490                GEN_REWRITE_CONV DEPTH_CONV
1491                 [EQT_INTRO(SPEC_ALL EQ_REFL); AND_CLAUSES] THENC
1492                GEN_REWRITE_CONV DEPTH_CONV [EXISTS_SIMP])
1493               tm' in
1494     let conv tm = if tm = lhand(concl th2) then th2 else fail() in
1495     CONV_RULE
1496         (RAND_CONV (RATOR_CONV
1497           (COMB2_CONV (RAND_CONV (BINDER_CONV conv)) (BINDER_CONV conv))))
1498         th1 in
1499   let MATCH_SEQPATTERN_CONV_TRIV =
1500     MATCH_SEQPATTERN_CONV THENC
1501     GEN_REWRITE_CONV I [COND_CLAUSES]
1502   and MATCH_SEQPATTERN_CONV_GEN =
1503     MATCH_SEQPATTERN_CONV THENC
1504     GEN_REWRITE_CONV TRY_CONV [COND_CLAUSES]
1505   and MATCH_ONEPATTERN_CONV_TRIV =
1506     MATCH_ONEPATTERN_CONV THENC
1507     GEN_REWRITE_CONV I [pth_5]
1508   and MATCH_ONEPATTERN_CONV_GEN =
1509     MATCH_ONEPATTERN_CONV THENC
1510     GEN_REWRITE_CONV TRY_CONV [pth_0; pth_5] in
1511   do_list extend_basic_convs
1512    ["MATCH_SEQPATTERN_CONV",
1513     (`_MATCH x (_SEQPATTERN r s)`,MATCH_SEQPATTERN_CONV_TRIV);
1514     "FUN_SEQPATTERN_CONV",
1515     (`_FUNCTION (_SEQPATTERN r s) x`,MATCH_SEQPATTERN_CONV_TRIV);
1516     "MATCH_ONEPATTERN_CONV",
1517     (`_MATCH x (\y z. P y z)`,MATCH_ONEPATTERN_CONV_TRIV);
1518     "FUN_ONEPATTERN_CONV",
1519     (`_FUNCTION (\y z. P y z) x`,MATCH_ONEPATTERN_CONV_TRIV)];
1520   (CHANGED_CONV UNWIND_CONV,
1521    (MATCH_SEQPATTERN_CONV_GEN ORELSEC MATCH_ONEPATTERN_CONV_GEN));;
1522
1523 let FORALL_UNWIND_CONV =
1524   let PUSH_FORALL_CONV =
1525      let econv = REWR_CONV SWAP_FORALL_THM in
1526      let rec conv bc tm =
1527        try (econv THENC BINDER_CONV(conv bc)) tm
1528        with Failure _ -> bc tm in
1529      conv in
1530   let baseconv = GEN_REWRITE_CONV I
1531    [MESON[] `(!x. x = a /\ p x ==> q x) <=> (p a ==> q a)`;
1532     MESON[] `(!x. a = x /\ p x ==> q x) <=> (p a ==> q a)`;
1533     MESON[] `(!x. x = a ==> q x) <=> q a`;
1534     MESON[] `(!x. a = x ==> q x) <=> q a`] in
1535   let rec FORALL_UNWIND_CONV tm =
1536     try let avs,bod = strip_forall tm in
1537         let ant,con = dest_imp bod in
1538         let eqs = conjuncts ant in
1539         let eq = find (fun tm ->
1540           is_eq tm &
1541           let l,r = dest_eq tm in
1542           (mem l avs & not (free_in l r)) or
1543           (mem r avs & not (free_in r l))) eqs in
1544         let l,r = dest_eq eq in
1545         let v = if mem l avs & not (free_in l r) then l else r in
1546         let cjs' = eq::(subtract eqs [eq]) in
1547         let n = length avs - (1 + index v (rev avs)) in
1548         let th1 = CONJ_ACI_RULE(mk_eq(ant,list_mk_conj cjs')) in
1549         let th2 = AP_THM (AP_TERM (rator(rator bod)) th1) con in
1550         let th3 = itlist MK_FORALL avs th2 in
1551         let th4 = funpow n BINDER_CONV (PUSH_FORALL_CONV baseconv)
1552                     (rand(concl th3)) in
1553         CONV_RULE (RAND_CONV FORALL_UNWIND_CONV) (TRANS th3 th4)
1554     with Failure _ -> REFL tm in
1555   FORALL_UNWIND_CONV;;