define.ml

   1 (* ========================================================================= *)
   2 (* Automated support for general recursive definitions.                      *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2007                       *)
   5 (* ========================================================================= *)
   6
   7 needs "cart.ml";;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Constant supporting casewise definitions.                                 *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let CASEWISE_DEF = new_recursive_definition list_RECURSION
  14  `(CASEWISE [] f x = @y. T) /\
  15   (CASEWISE (CONS h t) f x =
  16         if ?y. FST h y = x then SND h f (@y. FST h y = x)
  17         else CASEWISE t f x)`;;
  18
  19 let CASEWISE = prove
  20  (`(CASEWISE [] f x = @y. T) /\
  21    (CASEWISE (CONS (s,t) clauses) f x =
  22         if ?y. s y = x then t f (@y. s y = x) else CASEWISE clauses f x)`,
  23   REWRITE_TAC[CASEWISE_DEF]);;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Conditions for all the clauses in a casewise definition to hold.          *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let CASEWISE_CASES = prove
  30  (`!clauses c x.
  31     (?s t a. MEM (s,t) clauses /\ (s a = x) /\
  32              (CASEWISE clauses c x = t c a)) \/
  33     ~(?s t a. MEM (s,t) clauses /\ (s a = x)) /\
  34     (CASEWISE clauses c x = @y. T)`,
  35   MATCH_MP_TAC list_INDUCT THEN
  36   REWRITE_TAC[MEM; CASEWISE; FORALL_PAIR_THM; PAIR_EQ] THEN
  37   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_MESON_TAC[]);;
  38
  39 let CASEWISE_WORKS = prove
  40  (`!clauses c:C.
  41      (!s t s' t' x y. MEM (s,t) clauses /\ MEM (s',t') clauses /\ (s x = s' y)
  42                       ==> (t c x = t' c y))
  43      ==> ALL (\(s:P->A,t). !x. CASEWISE clauses c (s x) :B = t c x) clauses`,
  44   REWRITE_TAC[GSYM ALL_MEM; FORALL_PAIR_THM] THEN
  45   MESON_TAC[CASEWISE_CASES]);;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* Various notions of admissibility, with tail recursion and preconditions.  *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 let admissible = new_definition
  52  `admissible(<<) p s t <=>
  53         !f g a. p f a /\ p g a /\ (!z. z << s(a) ==> (f z = g z))
  54                 ==> (t f a = t g a)`;;
  55
  56 let tailadmissible = new_definition
  57  `tailadmissible(<<) p s t <=>
  58         ?P G H. (!f a y. P f a /\ y << G f a ==> y << s a) /\
  59                 (!f g a. (!z. z << s(a) ==> (f z = g z))
  60                          ==> (P f a = P g a) /\
  61                              (G f a = G g a) /\ (H f a = H g a)) /\
  62                 (!f a:P. p f a ==> (t (f:A->B) a =
  63                                     if P f a then f(G f a) else H f a))`;;
  64
  65 let superadmissible = new_definition
  66  `superadmissible(<<) p s t <=>
  67         admissible(<<) (\f a. T) s p ==> tailadmissible(<<) p s t`;;
  68
  69 (* ------------------------------------------------------------------------- *)
  70 (* A lemma.                                                                  *)
  71 (* ------------------------------------------------------------------------- *)
  72
  73 let MATCH_SEQPATTERN = prove
  74  (`_MATCH x (_SEQPATTERN r s) =
  75    if ?y. r x y then _MATCH x r else _MATCH x s`,
  76   REWRITE_TAC[_MATCH; _SEQPATTERN] THEN MESON_TAC[]);;
  77
  78 (* ------------------------------------------------------------------------- *)
  79 (* Admissibility combinators.                                                *)
  80 (* ------------------------------------------------------------------------- *)
  81
  82 let ADMISSIBLE_CONST = prove
  83  (`!p s c. admissible(<<) p s (\f. c)`,
  84   REWRITE_TAC[admissible]);;
  85
  86 let ADMISSIBLE_BASE = prove
  87  (`!(<<) p s t.
  88         (!f a. p f a ==> t a << s a)
  89         ==> admissible((<<):A->A->bool) p s (\f:A->B x:P. f(t x))`,
  90   REWRITE_TAC[admissible] THEN MESON_TAC[]);;
  91
  92 let ADMISSIBLE_COMB = prove
  93  (`!(<<) p s:P->A g:(A->B)->P->C->D y:(A->B)->P->C.
  94         admissible(<<) p s g /\ admissible(<<) p s y
  95         ==> admissible(<<) p s (\f x. (g f x) (y f x))`,
  96   SIMP_TAC[admissible] THEN MESON_TAC[]);;
  97
  98 let ADMISSIBLE_RAND = prove
  99  (`!(<<) p s:P->A g:P->C->D y:(A->B)->P->C.
 100         admissible(<<) p s y
 101         ==> admissible(<<) p s (\f x. (g x) (y f x))`,
 102   SIMP_TAC[admissible] THEN MESON_TAC[]);;
 103
 104 let ADMISSIBLE_LAMBDA = prove
 105  (`!(<<) p s:P->A t:(A->B)->C->P->bool.
 106      admissible(<<) (\f (u,x). p f x) (\(u,x). s x) (\f (u,x). t f u x)
 107      ==> admissible(<<) p s (\f x. \u. t f u x)`,
 108   REWRITE_TAC[admissible; FUN_EQ_THM; FORALL_PAIR_THM] THEN MESON_TAC[]);;
 109
 110 let ADMISSIBLE_NEST = prove
 111  (`!(<<) p s t.
 112         admissible(<<) p s t /\
 113         (!f a. p f a ==> t f a << s a)
 114         ==> admissible((<<):A->A->bool) p s (\f:A->B x:P. f(t f x))`,
 115   REWRITE_TAC[admissible] THEN MESON_TAC[]);;
 116
 117 let ADMISSIBLE_COND = prove
 118  (`!(<<) p P s h k.
 119         admissible(<<) p s P /\
 120         admissible(<<) (\f x. p f x /\ P f x) s h /\
 121         admissible(<<) (\f x. p f x /\ ~P f x) s k
 122         ==> admissible(<<) p s (\f x:P. if P f x then h f x else k f x)`,
 123   REPEAT GEN_TAC THEN
 124   REWRITE_TAC[admissible; AND_FORALL_THM] THEN
 125   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 126   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 127   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
 128
 129 let ADMISSIBLE_MATCH = prove
 130  (`!(<<) p s e c.
 131         admissible(<<) p s e /\ admissible(<<) p s (\f x. c f x (e f x))
 132         ==> admissible(<<) p s (\f x:P. _MATCH (e f x) (c f x))`,
 133   REWRITE_TAC[admissible; _MATCH] THEN
 134   REPEAT STRIP_TAC THEN REPEAT COND_CASES_TAC THEN ASM_MESON_TAC[]);;
 135
 136 let ADMISSIBLE_SEQPATTERN = prove
 137  (`!(<<) p s c1 c2 e.
 138         admissible(<<) p s (\f x:P. ?y. c1 f x (e f x) y) /\
 139         admissible(<<) (\f x. p f x /\ ?y. c1 f x (e f x) y) s
 140                        (\f x. c1 f x (e f x)) /\
 141         admissible(<<) (\f x. p f x /\ ~(?y. c1 f x (e f x) y)) s
 142                        (\f x. c2 f x (e f x))
 143         ==> admissible(<<) p s (\f x. _SEQPATTERN (c1 f x) (c2 f x) (e f x))`,
 144   REWRITE_TAC[_SEQPATTERN; admissible] THEN MESON_TAC[]);;
 145
 146 let ADMISSIBLE_UNGUARDED_PATTERN = prove
 147  (`!(<<) p s pat e t y.
 148       admissible (<<) p s pat /\
 149       admissible (<<) p s e /\
 150       admissible (<<) (\f x. p f x /\ pat f x = e f x) s t /\
 151       admissible (<<) (\f x. p f x /\ pat f x = e f x) s y
 152         ==> admissible(<<) p s
 153              (\f x:P. _UNGUARDED_PATTERN (GEQ (pat f x) (e f x))
 154                                          (GEQ (t f x) (y f x)))`,
 155   REPEAT GEN_TAC THEN
 156   REWRITE_TAC[admissible; FORALL_PAIR_THM; _UNGUARDED_PATTERN] THEN
 157   REWRITE_TAC[GEQ_DEF] THEN REPEAT STRIP_TAC THEN
 158   MATCH_MP_TAC(TAUT `(a <=> a') /\ (a /\ a' ==> (b <=> b'))
 159                      ==> (a /\ b <=> a' /\ b')`) THEN
 160   ASM_MESON_TAC[]);;
 161
 162 let ADMISSIBLE_GUARDED_PATTERN = prove
 163  (`!(<<) p s pat q e t y.
 164       admissible (<<) p s pat /\
 165       admissible (<<) p s e /\
 166       admissible (<<) (\f x. p f x /\ pat f x = e f x /\ q f x) s t /\
 167       admissible (<<) (\f x. p f x /\ pat f x = e f x) s q /\
 168       admissible (<<) (\f x. p f x /\ pat f x = e f x /\ q f x) s y
 169         ==> admissible(<<) p s
 170              (\f x:P. _GUARDED_PATTERN (GEQ (pat f x) (e f x))
 171                                        (q f x)
 172                                        (GEQ (t f x) (y f x)))`,
 173   REPEAT GEN_TAC THEN
 174   REWRITE_TAC[admissible; FORALL_PAIR_THM; _GUARDED_PATTERN] THEN
 175   REWRITE_TAC[GEQ_DEF] THEN REPEAT STRIP_TAC THEN
 176   REPEAT(MATCH_MP_TAC(TAUT `(a <=> a') /\ (a /\ a' ==> (b <=> b'))
 177                             ==> (a /\ b <=> a' /\ b')`) THEN
 178          REPEAT STRIP_TAC) THEN
 179   TRY(MATCH_MP_TAC(MESON[] `x = x' /\ y = y' ==> (x = y <=> x' = y')`)) THEN
 180   ASM_MESON_TAC[]);;
 181
 182 let ADMISSIBLE_NSUM = prove
 183  (`!(<<) p:(B->C)->P->bool s:P->A h a b.
 184         admissible(<<) (\f (k,x). a(x) <= k /\ k <= b(x) /\ p f x)
 185                        (\(k,x). s x) (\f (k,x). h f x k)
 186    ==> admissible(<<) p s (\f x. nsum(a(x)..b(x)) (h f x))`,
 187   REWRITE_TAC[admissible; FORALL_PAIR_THM] THEN REPEAT STRIP_TAC THEN
 188   MATCH_MP_TAC NSUM_EQ_NUMSEG THEN ASM_MESON_TAC[]);;
 189
 190 let ADMISSIBLE_SUM = prove
 191  (`!(<<) p:(B->C)->P->bool s:P->A h a b.
 192         admissible(<<) (\f (k,x). a(x) <= k /\ k <= b(x) /\ p f x)
 193                        (\(k,x). s x) (\f (k,x). h f x k)
 194    ==> admissible(<<) p s (\f x. sum(a(x)..b(x)) (h f x))`,
 195   REWRITE_TAC[admissible; FORALL_PAIR_THM] THEN REPEAT STRIP_TAC THEN
 196   MATCH_MP_TAC SUM_EQ_NUMSEG THEN ASM_MESON_TAC[]);;
 197
 198 let ADMISSIBLE_MAP = prove
 199  (`!(<<) p s h l.
 200         admissible(<<) p s l /\
 201         admissible (<<) (\f (y,x). p f x /\ MEM y (l f x))
 202                         (\(y,x). s x) (\f (y,x). h f x y)
 203    ==> admissible (<<) p s (\f:A->B x:P. MAP (h f x) (l f x))`,
 204   REWRITE_TAC[admissible; FORALL_PAIR_THM] THEN REPEAT STRIP_TAC THEN
 205   MATCH_MP_TAC(MESON[] `x = y /\ MAP f x = MAP g x ==> MAP f x = MAP g y`) THEN
 206   CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 207   MATCH_MP_TAC MAP_EQ THEN REWRITE_TAC[GSYM ALL_MEM] THEN
 208   REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 209   ASM_REWRITE_TAC[FORALL_PAIR_THM] THEN ASM_MESON_TAC[]);;
 210
 211 let ADMISSIBLE_MATCH_SEQPATTERN = prove
 212  (`!(<<) p s c1 c2 e.
 213         admissible(<<) p s (\f x. ?y. c1 f x (e f x) y) /\
 214         admissible(<<) (\f x. p f x /\ ?y. c1 f x (e f x) y) s
 215                        (\f x. _MATCH (e f x) (c1 f x)) /\
 216         admissible(<<) (\f x. p f x /\ ~(?y. c1 f x (e f x) y)) s
 217                        (\f x. _MATCH (e f x) (c2 f x))
 218         ==> admissible(<<) p s
 219               (\f x:P. _MATCH (e f x) (_SEQPATTERN (c1 f x) (c2 f x)))`,
 220   REWRITE_TAC[MATCH_SEQPATTERN; ADMISSIBLE_COND]);;
 221
 222 (* ------------------------------------------------------------------------- *)
 223 (* Superadmissible generalizations where applicable.                         *)
 224 (*                                                                           *)
 225 (* Note that we can't take the "higher type" route in the simple theorem     *)
 226 (* ADMISSIBLE_MATCH because that isn't a context where tail recursion makes  *)
 227 (* sense. Instead, we use specific theorems for the two _MATCH instances.    *)
 228 (* Note that also, because of some delicacy over assessing welldefinedness   *)
 229 (* of patterns, a special well-formedness hypothesis crops up here. (We need *)
 230 (* to separate it from the function f or we lose the "tail" optimization.)   *)
 231 (* ------------------------------------------------------------------------- *)
 232
 233 let ADMISSIBLE_IMP_SUPERADMISSIBLE = prove
 234  (`!(<<) p s t:(A->B)->P->B.
 235       admissible(<<) p s t ==> superadmissible(<<) p s t`,
 236   REWRITE_TAC[admissible; superadmissible; tailadmissible] THEN
 237   REPEAT STRIP_TAC THEN
 238   MAP_EVERY EXISTS_TAC
 239    [`\f:A->B x:P. F`;
 240     `\f:A->B. (anything:P->A)`;
 241     `\f:A->B a:P. if p f a then t f a :B else fixed`] THEN
 242   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
 243
 244 let SUPERADMISSIBLE_CONST = prove
 245  (`!p s c. superadmissible(<<) p s (\f. c)`,
 246   REPEAT GEN_TAC THEN
 247   MATCH_MP_TAC ADMISSIBLE_IMP_SUPERADMISSIBLE THEN
 248   REWRITE_TAC[ADMISSIBLE_CONST]);;
 249
 250 let SUPERADMISSIBLE_TAIL = prove
 251  (`!(<<) p s t:(A->B)->P->A.
 252       admissible(<<) p s t /\
 253       (!f a. p f a ==> !y. y << t f a ==> y << s a)
 254       ==> superadmissible(<<) p s (\f x. f(t f x))`,
 255   REWRITE_TAC[admissible; superadmissible; tailadmissible] THEN
 256   REPEAT STRIP_TAC THEN MAP_EVERY EXISTS_TAC
 257    [`\f:A->B x:P. T`;
 258     `\f:A->B a:P. if p f a then t f a :A else s a`;
 259     `\f:A->B. anything:P->B`] THEN
 260   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
 261
 262 let SUPERADMISSIBLE_COND = prove
 263  (`!(<<) p P s h k:(A->B)->P->B.
 264         admissible(<<) p s P /\
 265         superadmissible(<<) (\f x. p f x /\ P f x) s h /\
 266         superadmissible(<<) (\f x. p f x /\ ~P f x) s k
 267         ==> superadmissible(<<) p s (\f x. if P f x then h f x else k f x)`,
 268   REWRITE_TAC[superadmissible; admissible] THEN REPEAT GEN_TAC THEN
 269   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 270   DISCH_THEN(fun th -> DISCH_TAC THEN CONJUNCTS_THEN MP_TAC th) THEN
 271   ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 272   DISCH_THEN(fun th -> ANTS_TAC THENL [ASM_MESON_TAC[]; MP_TAC th]) THEN
 273   REWRITE_TAC[tailadmissible] THEN
 274   REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_IMP_FORALL_THM] THEN
 275   MAP_EVERY X_GEN_TAC
 276    [`P1:(A->B)->P->bool`; `G1:(A->B)->P->A`; `H1:(A->B)->P->B`;
 277     `P2:(A->B)->P->bool`; `G2:(A->B)->P->A`; `H2:(A->B)->P->B`] THEN
 278   REWRITE_TAC[TAUT `(a1 /\ b1 /\ c1 ==> a2 /\ b2 /\ c2 ==> x) <=>
 279                     (a1 /\ a2) /\ (b1 /\ b2) /\ (c1 /\ c2) ==> x`] THEN
 280   DISCH_THEN(fun th ->
 281    MAP_EVERY EXISTS_TAC
 282    [`\f:A->B a:P. if p f a then if P f a then P2 f a else P1 f a else F`;
 283    `\f:A->B a:P. if p f a then if P f a then G2 f a else G1 f a else z:A`;
 284    `\f:A->B a:P. if p f a then if P f a then H2 f a else H1 f a else w:B`] THEN
 285    MP_TAC th) THEN
 286   REWRITE_TAC[] THEN REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THENL
 287    [ASM_MESON_TAC[];
 288     POP_ASSUM_LIST(MP_TAC o end_itlist CONJ);
 289     ALL_TAC] THEN
 290   REWRITE_TAC[IMP_IMP; AND_FORALL_THM] THEN
 291   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 292   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 293   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
 294
 295 let SUPERADMISSIBLE_MATCH_SEQPATTERN = prove
 296  (`!(<<) p s c1 c2 e.
 297         admissible(<<) p s (\f x. ?y. c1 f x (e f x) y) /\
 298         superadmissible(<<) (\f x. p f x /\ ?y. c1 f x (e f x) y) s
 299                             (\f x. _MATCH (e f x) (c1 f x)) /\
 300         superadmissible(<<) (\f x. p f x /\ ~(?y. c1 f x (e f x) y)) s
 301                             (\f x. _MATCH (e f x) (c2 f x))
 302         ==> superadmissible(<<) p s
 303               (\f x:P. _MATCH (e f x) (_SEQPATTERN (c1 f x) (c2 f x)))`,
 304   REWRITE_TAC[MATCH_SEQPATTERN; SUPERADMISSIBLE_COND]);;
 305
 306 let SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN = prove
 307  (`!(<<) p s e:P->D pat:Q->D arg.
 308       (!f a t u. p f a /\ pat t = e a /\ pat u = e a ==> arg a t = arg a u) /\
 309       (!f a t. p f a /\ pat t = e a ==> !y. y << arg a t ==> y << s a)
 310       ==> superadmissible(<<) p s
 311            (\f:A->B x. _MATCH (e x)
 312                     (\u v. ?t. _UNGUARDED_PATTERN (GEQ (pat t) u)
 313                                                   (GEQ (f(arg x t)) v)))`,
 314   REPEAT GEN_TAC THEN STRIP_TAC THEN
 315   REWRITE_TAC[superadmissible] THEN DISCH_TAC THEN
 316   REWRITE_TAC[_UNGUARDED_PATTERN; GEQ_DEF; _MATCH] THEN
 317   REWRITE_TAC[tailadmissible] THEN
 318   SUBGOAL_THEN
 319    `!f:A->B x:P.
 320      p f x ==> ((?!v. ?t:Q. pat t:D = e x /\ f(arg x t) = v) <=>
 321                 ?t. pat t = e x)`
 322    (fun th -> SIMP_TAC[th]) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 323   MAP_EVERY EXISTS_TAC
 324    [`\(f:A->B) x:P. p f x /\ ?t:Q. pat t:D = e x`;
 325     `\f:A->B x:P. arg x (@t. (pat:Q->D) t = e x):A`;
 326     `\(f:A->B) x:P. (@z:B. F)`] THEN
 327   RULE_ASSUM_TAC(REWRITE_RULE[admissible]) THEN SIMP_TAC[] THEN
 328   ASM_MESON_TAC[]);;
 329
 330 let SUPERADMISSIBLE_MATCH_GUARDED_PATTERN = prove
 331  (`!(<<) p s e:P->D pat:Q->D q arg.
 332       (!f a t u. p f a /\ pat t = e a /\ q a t /\ pat u = e a /\ q a u
 333                  ==> arg a t = arg a u) /\
 334       (!f a t. p f a /\ q a t /\ pat t = e a ==> !y. y << arg a t ==> y << s a)
 335       ==> superadmissible(<<) p s
 336            (\f:A->B x. _MATCH (e x)
 337                     (\u v. ?t. _GUARDED_PATTERN (GEQ (pat t) u)
 338                                                 (q x t)
 339                                                 (GEQ (f(arg x t)) v)))`,
 340   REPEAT GEN_TAC THEN STRIP_TAC THEN
 341   REWRITE_TAC[superadmissible] THEN DISCH_TAC THEN
 342   REWRITE_TAC[_GUARDED_PATTERN; GEQ_DEF; _MATCH] THEN
 343   REWRITE_TAC[tailadmissible] THEN
 344   SUBGOAL_THEN
 345    `!f:A->B x:P.
 346      p f x ==> ((?!v. ?t:Q. pat t:D = e x /\ q x t /\ f(arg x t) = v) <=>
 347                 ?t. pat t = e x /\ q x t)`
 348    (fun th -> SIMP_TAC[th]) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 349   MAP_EVERY EXISTS_TAC
 350    [`\(f:A->B) x:P. p f x /\ ?t:Q. pat t:D = e x /\ q x t`;
 351     `\f:A->B x:P. arg x (@t. (pat:Q->D) t = e x /\ q x t):A`;
 352     `\(f:A->B) x:P. (@z:B. F)`] THEN
 353   RULE_ASSUM_TAC(REWRITE_RULE[admissible]) THEN SIMP_TAC[] THEN
 354   ASM_MESON_TAC[]);;
 355
 356 (* ------------------------------------------------------------------------- *)
 357 (* Combine general WF/tail recursion theorem with casewise definitions.      *)
 358 (* ------------------------------------------------------------------------- *)
 359
 360 let WF_REC_TAIL_GENERAL' = prove
 361  (`!P G H H'.
 362          WF (<<) /\
 363          (!f g x. (!z. z << x ==> (f z = g z))
 364                   ==> (P f x <=> P g x) /\
 365                       (G f x = G g x) /\ (H' f x = H' g x)) /\
 366          (!f x y. P f x /\ y << G f x ==> y << x) /\
 367          (!f x. H f x = if P f x then f(G f x) else H' f x)
 368          ==> ?f. !x. f x = H f x`,
 369   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 370   MATCH_MP_TAC WF_REC_TAIL_GENERAL THEN ASM_MESON_TAC[]);;
 371
 372 let WF_REC_CASES = prove
 373  (`!(<<) clauses.
 374         WF((<<):A->A->bool) /\
 375         ALL (\(s,t). ?P G H.
 376                      (!f a y. P f a /\ y << G f a ==> y << s a) /\
 377                      (!f g a. (!z. z << s(a) ==> (f z = g z))
 378                               ==> (P f a = P g a) /\
 379                                   (G f a = G g a) /\ (H f a = H g a)) /\
 380                      (!f a:P. t f a = if P f a then f(G f a) else H f a))
 381             clauses
 382         ==> ?f:A->B. !x. f x = CASEWISE clauses f x`,
 383   REPEAT STRIP_TAC THEN MATCH_MP_TAC WF_REC_TAIL_GENERAL' THEN
 384   FIRST_X_ASSUM(MP_TAC o check(is_binary "ALL" o concl)) THEN
 385   SPEC_TAC(`clauses:((P->A)#((A->B)->P->B))list`,
 386            `clauses:((P->A)#((A->B)->P->B))list`) THEN
 387   ASM_REWRITE_TAC[] THEN POP_ASSUM(K ALL_TAC) THEN
 388   MATCH_MP_TAC list_INDUCT THEN
 389   REWRITE_TAC[ALL; CASEWISE; FORALL_PAIR_THM] THEN CONJ_TAC THENL
 390    [MAP_EVERY EXISTS_TAC
 391      [`\f:A->B x:A. F`; `\f:A->B. anything:A->A`; `\f:A->B x:A. @y:B. T`] THEN
 392     REWRITE_TAC[];
 393     ALL_TAC] THEN
 394   MAP_EVERY X_GEN_TAC
 395     [`s:P->A`; `t:(A->B)->P->B`; `clauses:((P->A)#((A->B)->P->B))list`] THEN
 396   DISCH_THEN(fun th -> DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 397                        MP_TAC th) THEN
 398   ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(K ALL_TAC) THEN
 399   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
 400   MAP_EVERY X_GEN_TAC
 401    [`P1:(A->B)->A->bool`; `G1:(A->B)->A->A`; `H1:(A->B)->A->B`;
 402     `P2:(A->B)->P->bool`; `G2:(A->B)->P->A`; `H2:(A->B)->P->B`] THEN
 403   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 404   EXISTS_TAC
 405    `\f:A->B x:A. if ?y:P. s y = x then P2 f (@y. s y = x) else P1 f x:bool` THEN
 406   EXISTS_TAC `\f:A->B x:A.
 407      if ?y:P. s y = x then G2 f (@y. s y = x) else G1 f x:A` THEN
 408   EXISTS_TAC `\f:A->B x:A. if ?y:P. s y = x
 409                            then H2 f (@y. s y = x) else H1 f x:B` THEN
 410   ASM_MESON_TAC[]);;
 411
 412 let WF_REC_CASES' = prove
 413  (`!(<<) clauses.
 414         WF((<<):A->A->bool) /\
 415         ALL (\(s,t). tailadmissible(<<) (\f a. T) s t) clauses
 416         ==> ?f:A->B. !x. f x = CASEWISE clauses f x`,
 417   REWRITE_TAC[WF_REC_CASES; tailadmissible]);;
 418
 419 let RECURSION_CASEWISE = prove
 420  (`!clauses.
 421    (?(<<). WF(<<) /\
 422            ALL (\(s:P->A,t). tailadmissible(<<) (\f a. T) s t) clauses) /\
 423    (!s t s' t' f x y. MEM (s,t) clauses /\ MEM (s',t') clauses
 424                       ==> (s x = s' y) ==> (t f x = t' f y))
 425    ==> ?f:A->B. ALL (\(s,t). !x. f (s x) = t f x) clauses`,
 426   REPEAT GEN_TAC THEN REWRITE_TAC[IMP_IMP; CONJ_ASSOC] THEN
 427   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 428   DISCH_THEN(CHOOSE_THEN (MP_TAC o MATCH_MP WF_REC_CASES')) THEN
 429   MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN
 430   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[CASEWISE_WORKS]);;
 431
 432 let RECURSION_CASEWISE_PAIRWISE = prove
 433  (`!clauses.
 434         (?(<<). WF (<<) /\
 435                 ALL (\(s,t). tailadmissible(<<) (\f a. T) s t) clauses) /\
 436         ALL (\(s,t). !f x y. (s x = s y) ==> (t f x = t f y)) clauses /\
 437         PAIRWISE (\(s,t) (s',t'). !f x y. (s x = s' y) ==> (t f x = t' f y))
 438                  clauses
 439         ==> (?f. ALL (\(s,t). !x. f (s x) = t f x) clauses)`,
 440   let lemma = prove
 441    (`!P. (!x y. P x y ==> P y x)
 442          ==> !l. (!x y. MEM x l /\ MEM y l ==> P x y) <=>
 443                  ALL (\x. P x x) l /\ PAIRWISE P l`,
 444     REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; GSYM ALL_MEM] THEN
 445     REPEAT GEN_TAC THEN DISCH_TAC THEN LIST_INDUCT_TAC THEN
 446     REWRITE_TAC[PAIRWISE; MEM; GSYM ALL_MEM] THEN ASM_MESON_TAC[])
 447   and paired_lambda = prove
 448    (`(\x. P x) = (\(a,b). P (a,b))`,
 449     REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]) in
 450   let pth = REWRITE_RULE[FORALL_PAIR_THM; paired_lambda] (ISPEC
 451     `\(s,t) (s',t'). !c x:A y:A. (s x = s' y) ==> (t c x = t' c y)` lemma) in
 452   let cth = prove(lhand(concl pth),MESON_TAC[]) in
 453   REWRITE_TAC[GSYM(MATCH_MP pth cth); RIGHT_IMP_FORALL_THM] THEN
 454   REWRITE_TAC[RECURSION_CASEWISE]);;
 455
 456 let SUPERADMISSIBLE_T = prove
 457  (`superadmissible(<<) (\f x. T) s t <=> tailadmissible(<<) (\f x. T) s t`,
 458   REWRITE_TAC[superadmissible; admissible]);;
 459
 460 let RECURSION_SUPERADMISSIBLE = REWRITE_RULE[GSYM SUPERADMISSIBLE_T]
 461         RECURSION_CASEWISE_PAIRWISE;;
 462
 463 (* ------------------------------------------------------------------------- *)
 464 (* The main suite of functions for justifying recursion.                     *)
 465 (* ------------------------------------------------------------------------- *)
 466
 467 let instantiate_casewise_recursion,
 468     pure_prove_recursive_function_exists,
 469     prove_general_recursive_function_exists =
 470
 471 (* ------------------------------------------------------------------------- *)
 472 (* Make some basic simplification of conjunction of welldefinedness clauses. *)
 473 (* ------------------------------------------------------------------------- *)
 474
 475   let SIMPLIFY_WELLDEFINEDNESS_CONV =
 476     let LSYM =
 477       GEN_ALL o CONV_RULE(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) o SPEC_ALL
 478     and evensimps = prove
 479      (`((2 * m + 2 = 2 * n + 1) <=> F) /\
 480        ((2 * m + 1 = 2 * n + 2) <=> F) /\
 481        ((2 * m = 2 * n + 1) <=> F) /\
 482        ((2 * m + 1 = 2 * n) <=> F) /\
 483        ((2 * m = SUC(2 * n)) <=> F) /\
 484        ((SUC(2 * m) = 2 * n) <=> F)`,
 485       REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN
 486       DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
 487       REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH; EVEN]) in
 488     let allsimps = itlist (mk_rewrites false)
 489      [EQ_ADD_RCANCEL; EQ_ADD_LCANCEL;
 490       EQ_ADD_RCANCEL_0; EQ_ADD_LCANCEL_0;
 491       LSYM EQ_ADD_RCANCEL_0; LSYM EQ_ADD_LCANCEL_0;
 492       EQ_MULT_RCANCEL; EQ_MULT_LCANCEL;
 493       EQT_INTRO(SPEC_ALL EQ_REFL);
 494       ADD_EQ_0; LSYM ADD_EQ_0;
 495       MULT_EQ_0; LSYM MULT_EQ_0;
 496       MULT_EQ_1; LSYM MULT_EQ_1;
 497       ARITH_RULE `(m + n = 1) <=> (m = 1) /\ (n = 0) \/ (m = 0) /\ (n = 1)`;
 498       ARITH_RULE `(1 = m + n) <=> (m = 1) /\ (n = 0) \/ (m = 0) /\ (n = 1)`;
 499       evensimps; ARITH_EQ] []
 500     and [simp1; simp2; simp3] = map MATCH_MP (CONJUNCTS
 501       (TAUT
 502        `((a <=> F) /\ (b <=> b) ==> ((a ==> b) <=> T)) /\
 503         ((a <=> a') /\ (a' ==> (b <=> T)) ==> ((a ==> b) <=> T)) /\
 504         ((a <=> a') /\ (a' ==> (b <=> b')) ==> ((a ==> b) <=> (a' ==> b')))`))
 505     and false_tm = `F` and and_tm = `(/\)`
 506     and eq_refl = EQT_INTRO(SPEC_ALL EQ_REFL) in
 507     fun tm ->
 508       let net = itlist (net_of_thm false) allsimps (!basic_rectype_net) in
 509       let RECTYPE_ARITH_EQ_CONV =
 510         TOP_SWEEP_CONV(REWRITES_CONV net) THENC
 511         GEN_REWRITE_CONV DEPTH_CONV [AND_CLAUSES; OR_CLAUSES] in
 512       let SIMPLIFY_CASE_DISTINCTNESS_CLAUSE tm =
 513         let avs,bod = strip_forall tm in
 514         let ant,cons = dest_imp bod in
 515         let ath = RECTYPE_ARITH_EQ_CONV ant in
 516         let atm = rand(concl ath) in
 517         let bth = CONJ ath
 518           (if atm = false_tm then REFL cons
 519                     else DISCH atm
 520                           (PURE_REWRITE_CONV[eq_refl; ASSUME atm] cons)) in
 521         let cth = try simp1 bth with Failure _ -> try simp2 bth
 522                   with Failure _ -> simp3 bth in
 523         itlist MK_FORALL avs cth in
 524       (DEPTH_BINOP_CONV and_tm SIMPLIFY_CASE_DISTINCTNESS_CLAUSE THENC
 525        GEN_REWRITE_CONV DEPTH_CONV [FORALL_SIMP; AND_CLAUSES]) tm in
 526
 527 (* ------------------------------------------------------------------------- *)
 528 (* Simplify an existential question about a pattern.                         *)
 529 (* ------------------------------------------------------------------------- *)
 530
 531   let EXISTS_PAT_CONV =
 532     let pth = prove
 533      (`((?y. _UNGUARDED_PATTERN (GEQ s t) (GEQ z y)) <=> s = t) /\
 534        ((?y. _GUARDED_PATTERN (GEQ s t) g (GEQ z y)) <=> g /\ s = t)`,
 535       REWRITE_TAC[_UNGUARDED_PATTERN; _GUARDED_PATTERN; GEQ_DEF] THEN
 536       MESON_TAC[]) in
 537     let basecnv = GEN_REWRITE_CONV I [pth]
 538     and pushcnv = GEN_REWRITE_CONV I [SWAP_EXISTS_THM] in
 539     let rec EXISTS_PAT_CONV tm =
 540      ((pushcnv THENC BINDER_CONV EXISTS_PAT_CONV) ORELSEC
 541       basecnv) tm in
 542     fun tm -> if is_exists tm then EXISTS_PAT_CONV tm
 543               else failwith "EXISTS_PAT_CONV" in
 544
 545 (* ------------------------------------------------------------------------- *)
 546 (* Hack a proforma to introduce new pairing or pattern variables.            *)
 547 (* ------------------------------------------------------------------------- *)
 548
 549   let HACK_PROFORMA,EACK_PROFORMA =
 550     let elemma0 = prove
 551      (`((!z. GEQ (f z) (g z)) <=> (!x y. GEQ (f(x,y)) (g(x,y)))) /\
 552        ((\p. P p) = (\(x,y). P(x,y)))`,
 553       REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM])
 554     and elemma1 = prove
 555      (`(!P. (!t:A->B->C#D->E. P t) <=> (!t. P (\a b (c,d). t a b d c))) /\
 556        (!P. (!t:B->C#D->E. P t) <=> (!t. P (\b (c,d). t b d c))) /\
 557        (!P. (!t:C#D->E. P t) <=> (!t. P (\(c,d). t d c)))`,
 558       REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN
 559       ASM_REWRITE_TAC[] THENL
 560        [FIRST_X_ASSUM(MP_TAC o SPEC `\a b d c. (t:A->B->C#D->E) a b (c,d)`);
 561         FIRST_X_ASSUM(MP_TAC o SPEC `\b d c. (t:B->C#D->E) b (c,d)`);
 562         FIRST_X_ASSUM(MP_TAC o SPEC `\d c. (t:C#D->E) (c,d)`)] THEN
 563       MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 564       REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]) in
 565     let HACK_PROFORMA n th =
 566       if n <= 1 then th else
 567       let mkname i = "_P"^string_of_int i in
 568       let ty = end_itlist (fun s t -> mk_type("prod",[s;t]))
 569                           (map (mk_vartype o mkname) (1--n)) in
 570       let conv i =
 571         let name = "x"^string_of_int i in
 572         let cnv = ALPHA_CONV (mk_var(name,mk_vartype(mkname i))) in
 573         fun tm -> if is_abs tm & name_of(bndvar tm) <> name
 574                   then cnv tm else failwith "conv" in
 575       let convs = FIRST_CONV (map conv (1--n)) in
 576       let th1 = INST_TYPE [ty,`:P`] th in
 577       let th2 = REWRITE_RULE[FORALL_PAIR_THM] th1 in
 578       let th3 = REWRITE_RULE[elemma0; elemma1] th2 in
 579       CONV_RULE(REDEPTH_CONV convs) th3
 580     and EACK_PROFORMA n th =
 581       if n <= 1 then th else
 582       let mkname i = "_Q"^string_of_int i in
 583       let ty = end_itlist (fun s t -> mk_type("prod",[s;t]))
 584                           (map (mk_vartype o mkname) (1--n)) in
 585       let conv i =
 586         let name = "t"^string_of_int i in
 587         let cnv = ALPHA_CONV (mk_var(name,mk_vartype(mkname i))) in
 588         fun tm -> if is_abs tm & name_of(bndvar tm) <> name
 589                   then cnv tm else failwith "conv" in
 590       let convs = FIRST_CONV (map conv (1--n)) in
 591       let th1 = INST_TYPE [ty,`:Q`] th in
 592       let th2 = REWRITE_RULE[EXISTS_PAIR_THM] th1 in
 593       let th3 = REWRITE_RULE[elemma1] th2 in
 594       let th4 = REWRITE_RULE[FORALL_PAIR_THM] th3 in
 595       CONV_RULE(REDEPTH_CONV convs) th4 in
 596     HACK_PROFORMA,EACK_PROFORMA in
 597
 598 (* ------------------------------------------------------------------------- *)
 599 (* Hack and apply.                                                           *)
 600 (* ------------------------------------------------------------------------- *)
 601
 602   let APPLY_PROFORMA_TAC th (asl,w as gl) =
 603     let vs = fst(dest_gabs(body(rand w))) in
 604     let n = 1 + length(fst(splitlist dest_pair vs)) in
 605     (MATCH_MP_TAC(HACK_PROFORMA n th) THEN BETA_TAC) gl in
 606
 607   let is_pattern p n tm =
 608     try let f,args = strip_comb(snd(strip_exists (body(body tm)))) in
 609         is_const f & name_of f = p & length args = n
 610     with Failure _ -> false in
 611
 612   let SIMPLIFY_MATCH_WELLDEFINED_TAC =
 613     let pth0 = MESON[]
 614      `(a /\ x = k ==> x = y ==> d) ==> (a /\ x = k /\ y = k ==> d)`
 615     and pth1 = MESON[]
 616      `(a /\ b /\ c /\ x = k ==> x = y ==> d)
 617       ==> (a /\ x = k /\ b /\ y = k /\ c ==> d)` in
 618     REPEAT GEN_TAC THEN
 619     (MATCH_MP_TAC pth1 ORELSE MATCH_MP_TAC pth0) THEN
 620     CONV_TAC(RAND_CONV SIMPLIFY_WELLDEFINEDNESS_CONV) THEN
 621     PURE_REWRITE_TAC
 622       [AND_CLAUSES; IMP_CLAUSES; OR_CLAUSES; EQ_CLAUSES; NOT_CLAUSES] in
 623
 624   let rec headonly f tm =
 625     match tm with
 626       Comb(s,t) -> headonly f s & headonly f t & not(t = f)
 627     | Abs(x,t) -> headonly f t
 628     | _ -> true in
 629
 630   let MAIN_ADMISS_TAC (asl,w as gl) =
 631     let had,args = strip_comb w in
 632     if not(is_const had) then failwith "ADMISS_TAC" else
 633     let f,fbod = dest_abs(last args) in
 634     let xtup,bod = dest_gabs fbod in
 635     let hop,args = strip_comb bod in
 636     match (name_of had,name_of hop) with
 637       "superadmissible","COND"
 638           -> APPLY_PROFORMA_TAC SUPERADMISSIBLE_COND gl
 639     | "superadmissible","_MATCH" when
 640           name_of(repeat rator (last args)) = "_SEQPATTERN"
 641           -> (APPLY_PROFORMA_TAC SUPERADMISSIBLE_MATCH_SEQPATTERN THEN
 642               CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
 643     | "superadmissible","_MATCH" when
 644          is_pattern "_UNGUARDED_PATTERN" 2 (last args)
 645           -> let n = length(fst(strip_exists(body(body(last args))))) in
 646              let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN in
 647              (APPLY_PROFORMA_TAC th THEN CONJ_TAC THENL
 648                [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
 649     | "superadmissible","_MATCH" when
 650          is_pattern "_GUARDED_PATTERN" 3 (last args)
 651           -> let n = length(fst(strip_exists(body(body(last args))))) in
 652              let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_GUARDED_PATTERN in
 653              (APPLY_PROFORMA_TAC th THEN CONJ_TAC THENL
 654                [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
 655     | "superadmissible",_ when is_comb bod & rator bod = f
 656           -> APPLY_PROFORMA_TAC SUPERADMISSIBLE_TAIL gl
 657     | "admissible","sum"
 658           -> APPLY_PROFORMA_TAC ADMISSIBLE_SUM gl
 659     | "admissible","nsum"
 660           -> APPLY_PROFORMA_TAC ADMISSIBLE_NSUM gl
 661     | "admissible","MAP"
 662           -> APPLY_PROFORMA_TAC ADMISSIBLE_MAP gl
 663     | "admissible","_MATCH" when
 664           name_of(repeat rator (last args)) = "_SEQPATTERN"
 665           -> (APPLY_PROFORMA_TAC ADMISSIBLE_MATCH_SEQPATTERN THEN
 666               CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
 667     | "admissible","_MATCH"
 668           -> APPLY_PROFORMA_TAC ADMISSIBLE_MATCH gl
 669     | "admissible","_UNGUARDED_PATTERN"
 670           -> APPLY_PROFORMA_TAC ADMISSIBLE_UNGUARDED_PATTERN gl
 671     | "admissible","_GUARDED_PATTERN"
 672           -> APPLY_PROFORMA_TAC ADMISSIBLE_GUARDED_PATTERN gl
 673     | "admissible",_ when is_abs bod
 674           -> APPLY_PROFORMA_TAC ADMISSIBLE_LAMBDA gl
 675     | "admissible",_ when is_comb bod & rator bod = f
 676           -> if free_in f (rand bod) then
 677                APPLY_PROFORMA_TAC ADMISSIBLE_NEST gl
 678              else
 679                APPLY_PROFORMA_TAC ADMISSIBLE_BASE gl
 680     | "admissible",_ when is_comb bod & headonly f bod
 681           -> APPLY_PROFORMA_TAC ADMISSIBLE_COMB gl
 682     | _ -> failwith "MAIN_ADMISS_TAC" in
 683
 684   let ADMISS_TAC =
 685     CONJ_TAC ORELSE
 686     MATCH_ACCEPT_TAC ADMISSIBLE_CONST ORELSE
 687     MATCH_ACCEPT_TAC SUPERADMISSIBLE_CONST ORELSE
 688     MAIN_ADMISS_TAC ORELSE
 689     MATCH_MP_TAC ADMISSIBLE_IMP_SUPERADMISSIBLE in
 690
 691 (* ------------------------------------------------------------------------- *)
 692 (* Instantiate the casewise recursion theorem for existential claim.         *)
 693 (* Also make a first attempt to simplify the distinctness clause. This may   *)
 694 (* yield a theorem with just the wellfoundedness "?(<<)" assumption, or it   *)
 695 (* may be that and an additional distinctness one.                           *)
 696 (* ------------------------------------------------------------------------- *)
 697
 698   let instantiate_casewise_recursion =
 699     let EXPAND_PAIRED_ALL_CONV =
 700       let pth0,pth1 = (CONJ_PAIR o prove)
 701        (`(ALL (\(s,t). P s t) [a,b] <=> P a b) /\
 702          (ALL (\(s,t). P s t) (CONS (a,b) l) <=>
 703           P a b /\ ALL (\(s,t). P s t) l)`,
 704         REWRITE_TAC[ALL]) in
 705       let conv0 = REWR_CONV pth0 and conv1 = REWR_CONV pth1 in
 706       let rec conv tm =
 707         try conv0 tm with Failure _ ->
 708         let th = conv1 tm in CONV_RULE (funpow 2 RAND_CONV conv) th in
 709       conv
 710     and LAMBDA_PAIR_CONV =
 711       let rewr1 =  GEN_REWRITE_RULE I [GSYM FORALL_PAIR_THM]
 712       and rewr2 = GEN_REWRITE_CONV I [FUN_EQ_THM] in
 713       fun parms tm ->
 714         let parm = end_itlist (curry mk_pair) parms in
 715         let x,bod = dest_abs tm in
 716         let tm' = mk_gabs(parm,vsubst[parm,x] bod) in
 717         let th1 = BETA_CONV(mk_comb(tm,parm))
 718         and th2 = GEN_BETA_CONV (mk_comb(tm',parm)) in
 719         let th3 = TRANS th1 (SYM th2) in
 720         let th4 = itlist (fun v th -> rewr1 (GEN v th))
 721                          (butlast parms) (GEN (last parms) th3) in
 722         EQ_MP (SYM(rewr2(mk_eq(tm,tm')))) th4
 723     and FORALL_PAIR_CONV =
 724       let rule = GEN_REWRITE_RULE RAND_CONV [GSYM FORALL_PAIR_THM] in
 725       let rec depair l t =
 726         match l with
 727           [v] -> REFL t
 728         | v::vs -> rule(BINDER_CONV (depair vs) t) in
 729       fun parm parms ->
 730         let p = mk_var("P",mk_fun_ty (type_of parm) bool_ty) in
 731         let tm = list_mk_forall(parms,mk_comb(p,parm)) in
 732         GEN p (SYM(depair parms tm)) in
 733     let ELIM_LISTOPS_CONV =
 734       PURE_REWRITE_CONV[PAIRWISE; ALL; GSYM CONJ_ASSOC; AND_CLAUSES] THENC
 735       TOP_DEPTH_CONV GEN_BETA_CONV in
 736     let tuple_function_existence tm =
 737       let f,def = dest_exists tm in
 738       let domtys0,ranty0 = splitlist dest_fun_ty (type_of f) in
 739       let nargs =
 740         itlist
 741          (max o length o snd o strip_comb o lhs o snd o strip_forall)
 742          (conjuncts(snd(strip_forall def))) 0 in
 743       let domtys,midtys = chop_list nargs domtys0 in
 744       let ranty = itlist mk_fun_ty midtys ranty0 in
 745       if length domtys <= 1 then ASSUME tm else
 746       let dty = end_itlist (fun ty1 ty2 -> mk_type("prod",[ty1;ty2])) domtys in
 747       let f' = variant (frees tm)
 748                        (mk_var(fst(dest_var f),mk_fun_ty dty ranty)) in
 749       let gvs = map genvar domtys in
 750       let f'' = list_mk_abs(gvs,mk_comb(f',end_itlist (curry mk_pair) gvs)) in
 751       let def' = subst [f'',f] def in
 752       let th1 = EXISTS (tm,f'') (ASSUME def')
 753       and bth = BETAS_CONV (list_mk_comb(f'',gvs)) in
 754       let th2 = GEN_REWRITE_CONV TOP_DEPTH_CONV [bth] (hd(hyp th1)) in
 755       SIMPLE_CHOOSE f' (PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th2))) th1) in
 756     let pinstantiate_casewise_recursion def =
 757       try PART_MATCH I EXISTS_REFL def with Failure _ ->
 758       let f,bod = dest_exists def in
 759       let cjs = conjuncts bod in
 760       let eqs = map (snd o strip_forall) cjs in
 761       let lefts,rights = unzip(map dest_eq eqs) in
 762       let arglists = map (snd o strip_comb) lefts in
 763       let parms0 = freesl(unions arglists) in
 764       let parms = if parms0 <> [] then parms0 else [genvar aty] in
 765       let parm = end_itlist (curry mk_pair) parms in
 766       let ss = map (fun a -> mk_gabs(parm,end_itlist (curry mk_pair) a))
 767                    arglists
 768       and ts = map (fun a -> mk_abs(f,mk_gabs(parm,a))) rights in
 769       let clauses = mk_flist(map2 (curry mk_pair) ss ts) in
 770       let pth = ISPEC clauses RECURSION_SUPERADMISSIBLE in
 771       let FIDDLE_CONV =
 772         (LAND_CONV o LAND_CONV o BINDER_CONV o RAND_CONV o LAND_CONV o
 773          GABS_CONV o RATOR_CONV o LAND_CONV o ABS_CONV) in
 774       let th0 = UNDISCH(CONV_RULE(FIDDLE_CONV(LAMBDA_PAIR_CONV parms)) pth) in
 775       let th1 = EQ_MP (GEN_ALPHA_CONV f (concl th0)) th0 in
 776       let rewr_forall_th = REWR_CONV(FORALL_PAIR_CONV parm parms) in
 777       let th2 = CONV_RULE (BINDER_CONV
 778                     (LAND_CONV(GABS_CONV rewr_forall_th) THENC
 779                      EXPAND_PAIRED_ALL_CONV)) th1 in
 780       let f2,bod2 = dest_exists(concl th2) in
 781       let ths3 = map
 782        (CONV_RULE (COMB2_CONV (funpow 2 RAND_CONV GEN_BETA_CONV)
 783                   (RATOR_CONV BETA_CONV THENC GEN_BETA_CONV)) o SPEC_ALL)
 784        (CONJUNCTS(ASSUME bod2)) in
 785       let ths4 = map2
 786        (fun th t -> let avs,tbod = strip_forall t in
 787                     itlist GEN avs (PART_MATCH I th tbod)) ths3 cjs in
 788       let th5 = SIMPLE_EXISTS f (end_itlist CONJ ths4) in
 789       let th6 = PROVE_HYP th2 (SIMPLE_CHOOSE f th5) in
 790       let th7 =
 791        (RAND_CONV(COMB2_CONV
 792             (RAND_CONV (LAND_CONV (GABS_CONV(BINDER_CONV
 793                      (BINDER_CONV(rewr_forall_th) THENC rewr_forall_th)))))
 794             (LAND_CONV (funpow 2 GABS_CONV(BINDER_CONV
 795                      (BINDER_CONV(rewr_forall_th) THENC
 796                       rewr_forall_th))))) THENC
 797         ELIM_LISTOPS_CONV) (hd(hyp th6)) in
 798       let th8 = PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th7))) th6 in
 799       let wfasm,cdasm = dest_conj(hd(hyp th8)) in
 800       let th9 = PROVE_HYP (CONJ (ASSUME wfasm) (ASSUME cdasm)) th8 in
 801       let th10 = SIMPLIFY_WELLDEFINEDNESS_CONV cdasm in
 802       let th11 = PROVE_HYP (UNDISCH(snd(EQ_IMP_RULE th10))) th9 in
 803       PROVE_HYP TRUTH th11 in
 804     fun etm ->
 805       let eth = tuple_function_existence etm in
 806       let dtm = hd(hyp eth) in
 807       let dth = pinstantiate_casewise_recursion dtm in
 808       PROVE_HYP dth eth in
 809
 810 (* ------------------------------------------------------------------------- *)
 811 (* Justify existence assertion and try to simplify/remove side-conditions.   *)
 812 (* ------------------------------------------------------------------------- *)
 813
 814   let pure_prove_recursive_function_exists =
 815     let break_down_admissibility th1 =
 816       if hyp th1 = [] then th1 else
 817       let def = concl th1 in
 818       let f,bod = dest_exists def in
 819       let cjs = conjuncts bod in
 820       let eqs = map (snd o strip_forall) cjs in
 821       let lefts,rights = unzip(map dest_eq eqs) in
 822       let arglists = map (snd o strip_comb) lefts in
 823       let parms0 = freesl(unions arglists) in
 824       let parms = if parms0 <> [] then parms0 else [genvar aty] in
 825       let wfasm = find is_exists (hyp th1) in
 826       let ord,bod = dest_exists wfasm in
 827       let SIMP_ADMISS_TAC =
 828         REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
 829         REPEAT ADMISS_TAC THEN
 830         TRY(W(fun (asl,w) -> let v = fst(dest_forall w) in
 831                 X_GEN_TAC v THEN
 832                 MAP_EVERY
 833                   (fun v -> TRY(GEN_REWRITE_TAC I [FORALL_PAIR_THM]) THEN
 834                             X_GEN_TAC v)
 835                   parms THEN
 836                 CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN
 837                 MAP_EVERY (fun v -> SPEC_TAC(v,v)) (rev parms @ [v]))) THEN
 838         PURE_REWRITE_TAC[FORALL_SIMP] THEN
 839         W(fun (asl,w) -> MAP_EVERY (fun t -> SPEC_TAC(t,t))
 840                                    (subtract (frees w) [ord])) THEN
 841         W(fun (asl,w) -> ACCEPT_TAC(ASSUME w)) in
 842       let th2 = prove(bod,SIMP_ADMISS_TAC) in
 843       let th3 = SIMPLE_EXISTS ord th2 in
 844       let allasms = hyp th3 and wfasm = lhand(concl th2) in
 845       let th4 = ASSUME(list_mk_conj(wfasm::subtract allasms [wfasm])) in
 846       let th5 = SIMPLE_CHOOSE ord (itlist PROVE_HYP (CONJUNCTS th4) th3) in
 847       PROVE_HYP th5 th1 in
 848     fun dtm ->
 849       let th =  break_down_admissibility(instantiate_casewise_recursion dtm) in
 850       if concl th = dtm then th
 851       else failwith "prove_general_recursive_function_exists: sanity" in
 852
 853 (* ------------------------------------------------------------------------- *)
 854 (* Same, but attempt to prove the wellfoundedness hyp by good guesses.       *)
 855 (* ------------------------------------------------------------------------- *)
 856
 857   let prove_general_recursive_function_exists =
 858     let prove_depth_measure_exists =
 859       let num_ty = `:num` in
 860       fun tyname ->
 861         let _,_,sth = assoc tyname (!inductive_type_store) in
 862         let ty,zty = dest_fun_ty
 863          (type_of(fst(dest_exists(snd(strip_forall(concl sth)))))) in
 864         let rth = INST_TYPE [num_ty,zty] sth in
 865         let avs,bod = strip_forall(concl rth) in
 866         let ev,cbod = dest_exists bod in
 867         let process_clause k t =
 868           let avs,eq = strip_forall t in
 869           let l,r = dest_eq eq in
 870           let fn,cargs = dest_comb l in
 871           let con,args = strip_comb cargs in
 872           let bargs = filter (fun t -> type_of t = ty) args in
 873           let r' = list_mk_binop `(+):num->num->num`
 874                     (mk_small_numeral k :: map (curry mk_comb fn) bargs) in
 875           list_mk_forall(avs,mk_eq(l,r')) in
 876         let cjs = conjuncts cbod in
 877         let def = map2 process_clause (1--length cjs) cjs in
 878         prove_recursive_functions_exist sth (list_mk_conj def) in
 879     let INDUCTIVE_MEASURE_THEN tac (asl,w) =
 880       let ev,bod = dest_exists w in
 881       let ty = fst(dest_type(fst(dest_fun_ty(type_of ev)))) in
 882       let th = prove_depth_measure_exists ty in
 883       let ev',bod' = dest_exists(concl th) in
 884       let th' = INST_TYPE(type_match (type_of ev') (type_of ev) []) th in
 885       (MP_TAC th' THEN MATCH_MP_TAC MONO_EXISTS THEN
 886        GEN_TAC THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN tac) (asl,w) in
 887     let CONSTANT_MEASURE_THEN =
 888       let one_tm = `1` in
 889       fun tac (asl,w) ->
 890         let ev,bod = dest_exists w in
 891         let ty = fst(dest_fun_ty(type_of ev)) in
 892         (EXISTS_TAC(mk_abs(genvar ty,one_tm)) THEN tac) (asl,w) in
 893     let GUESS_MEASURE_THEN tac =
 894       (EXISTS_TAC `\n. n + 1` THEN tac) ORELSE
 895       (INDUCTIVE_MEASURE_THEN tac) ORELSE
 896       CONSTANT_MEASURE_THEN tac in
 897     let pth_lexleft = prove
 898      (`(?r. WF(r) /\
 899             ?s. WF(s) /\
 900                 P(\(x1,y1) (x2,y2). r x1 x2 \/ (x1 = x2) /\ s y1 y2))
 901        ==> ?t:A#B->A#B->bool. WF(t) /\ P t`,
 902       REPEAT STRIP_TAC THEN EXISTS_TAC
 903        `\(x1:A,y1:B) (x2:A,y2:B). r x1 x2 \/ (x1 = x2) /\ s y1 y2` THEN
 904       ASM_SIMP_TAC[WF_LEX]) in
 905     let pth_lexright = prove
 906      (`(?r. WF(r) /\
 907             ?s. WF(s) /\
 908                 P(\(x1,y1) (x2,y2). r y1 y2 \/ (y1 = y2) /\ s x1 x2))
 909        ==> ?t:A#B->A#B->bool. WF(t) /\ P t`,
 910       REPEAT STRIP_TAC THEN
 911       EXISTS_TAC `\u:A#B v:A#B.
 912                     (\(x1:B,y1:A) (x2:B,y2:A). r x1 x2 \/ (x1 = x2) /\ s y1 y2)
 913                      ((\(a,b). b,a) u) ((\(a,b). b,a) v)` THEN
 914       ASM_SIMP_TAC[ISPEC `\(a,b). b,a` WF_MEASURE_GEN; WF_LEX; ETA_AX] THEN
 915       FIRST_X_ASSUM(fun th -> MP_TAC th THEN
 916                               MATCH_MP_TAC EQ_IMP THEN
 917                               AP_TERM_TAC) THEN
 918       REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]) in
 919     let pth_measure = prove
 920      (`(?m:A->num. P(MEASURE m)) ==> ?r:A->A->bool. WF(r) /\ P r`,
 921       MESON_TAC[WF_MEASURE]) in
 922     let rec GUESS_WF_THEN tac (asl,w) =
 923      ((MATCH_MP_TAC pth_lexleft THEN GUESS_WF_THEN (GUESS_WF_THEN tac)) ORELSE
 924       (MATCH_MP_TAC pth_lexright THEN GUESS_WF_THEN (GUESS_WF_THEN tac)) ORELSE
 925       (MATCH_MP_TAC pth_measure THEN
 926        REWRITE_TAC[MEASURE; MEASURE_LE] THEN
 927        REWRITE_TAC[FORALL_PAIR_THM] THEN
 928        GUESS_MEASURE_THEN tac)) (asl,w) in
 929     let PRE_GUESS_TAC =
 930       CONV_TAC(BINDER_CONV(DEPTH_BINOP_CONV `(/\)`
 931        (TRY_CONV SIMPLIFY_WELLDEFINEDNESS_CONV THENC
 932         TRY_CONV FORALL_UNWIND_CONV))) in
 933     let GUESS_ORDERING_TAC =
 934       let false_tm = `\x:A y:A. F` in
 935       W(fun (asl,w) ->
 936             let ty = fst(dest_fun_ty(type_of(fst(dest_exists w)))) in
 937             EXISTS_TAC(inst [ty,aty] false_tm) THEN
 938             REWRITE_TAC[WF_FALSE] THEN NO_TAC) ORELSE
 939       GUESS_WF_THEN
 940        (REWRITE_TAC[FORALL_PAIR_THM] THEN ARITH_TAC) in
 941     fun etm ->
 942       let th = pure_prove_recursive_function_exists etm in
 943       try let wtm = find is_exists (hyp th) in
 944           let wth = prove(wtm,PRE_GUESS_TAC THEN GUESS_ORDERING_TAC) in
 945           PROVE_HYP wth th
 946       with Failure _ -> th in
 947
 948   instantiate_casewise_recursion,
 949   pure_prove_recursive_function_exists,
 950   prove_general_recursive_function_exists;;
 951
 952 (* ------------------------------------------------------------------------- *)
 953 (* Simple "define" function.                                                 *)
 954 (* ------------------------------------------------------------------------- *)
 955
 956 let define =
 957   let close_definition_clauses tm =
 958     let avs,bod = strip_forall tm in
 959     let cjs = conjuncts bod in
 960     let fs =
 961       try map (repeat rator o lhs o snd o strip_forall) cjs
 962       with Failure _ -> failwith "close_definition_clauses: non-equation" in
 963     if length (setify fs) <> 1
 964     then failwith "close_definition_clauses: defining multiple functions" else
 965     let f = hd fs in
 966     if mem f avs then failwith "close_definition_clauses: fn quantified" else
 967     let do_clause t =
 968       let lvs,bod = strip_forall t in
 969       let fvs = subtract (frees(lhs bod)) (f::lvs) in
 970       SPECL fvs (ASSUME(list_mk_forall(fvs,t))) in
 971     let ths = map do_clause cjs in
 972     let ajs = map (hd o hyp) ths in
 973     let th = ASSUME(list_mk_conj ajs) in
 974     f,itlist GEN avs (itlist PROVE_HYP (CONJUNCTS th) (end_itlist CONJ ths)) in
 975   fun tm ->
 976     let tm' = snd(strip_forall tm) in
 977     try let th,th' = tryfind (fun th -> th,PART_MATCH I th tm')
 978                              (!the_definitions) in
 979         if can (PART_MATCH I th') (concl th) then
 980          (warn true "Benign redefinition"; th')
 981         else failwith ""
 982     with Failure _ ->
 983       let f,th = close_definition_clauses tm in
 984       let etm = mk_exists(f,hd(hyp th)) in
 985       let th1 = prove_general_recursive_function_exists etm in
 986       let th2 = new_specification[fst(dest_var f)] th1 in
 987       let g = mk_mconst(dest_var f) in
 988       let th3 = PROVE_HYP th2 (INST [g,f] th) in
 989       the_definitions := th3::(!the_definitions); th3;;