theorems.ml

   1 (* ========================================================================= *)
   2 (* Additional theorems, mainly about quantifiers, and additional tactics.    *)
   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 (*                 (c) Copyright, Marco Maggesi 2012                         *)
   9 (* ========================================================================= *)
  10
  11 needs "simp.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* More stuff about equality.                                                *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let EQ_REFL = prove
  18  (`!x:A. x = x`,
  19   GEN_TAC THEN REFL_TAC);;
  20
  21 let REFL_CLAUSE = prove
  22  (`!x:A. (x = x) <=> T`,
  23   GEN_TAC THEN MATCH_ACCEPT_TAC(EQT_INTRO(SPEC_ALL EQ_REFL)));;
  24
  25 let EQ_SYM = prove
  26  (`!(x:A) y. (x = y) ==> (y = x)`,
  27   REPEAT GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o SYM));;
  28
  29 let EQ_SYM_EQ = prove
  30  (`!(x:A) y. (x = y) <=> (y = x)`,
  31   REPEAT GEN_TAC THEN EQ_TAC THEN MATCH_ACCEPT_TAC EQ_SYM);;
  32
  33 let EQ_TRANS = prove
  34  (`!(x:A) y z. (x = y) /\ (y = z) ==> (x = z)`,
  35   REPEAT STRIP_TAC THEN PURE_ASM_REWRITE_TAC[] THEN REFL_TAC);;
  36
  37 (* ------------------------------------------------------------------------- *)
  38 (* The following is a common special case of ordered rewriting.              *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 let AC acsuite = EQT_ELIM o PURE_REWRITE_CONV[acsuite; REFL_CLAUSE];;
  42
  43 (* ------------------------------------------------------------------------- *)
  44 (* A couple of theorems about beta reduction.                                *)
  45 (* ------------------------------------------------------------------------- *)
  46
  47 let BETA_THM = prove
  48  (`!(f:A->B) y. (\x. (f:A->B) x) y = f y`,
  49   REPEAT GEN_TAC THEN BETA_TAC THEN REFL_TAC);;
  50
  51 let ABS_SIMP = prove
  52  (`!(t1:A) (t2:B). (\x. t1) t2 = t1`,
  53   REPEAT GEN_TAC THEN REWRITE_TAC[BETA_THM; REFL_CLAUSE]);;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* A few "big name" intuitionistic tautologies.                              *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 let CONJ_ASSOC = prove
  60  (`!t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3`,
  61   ITAUT_TAC);;
  62
  63 let CONJ_SYM = prove
  64  (`!t1 t2. t1 /\ t2 <=> t2 /\ t1`,
  65   ITAUT_TAC);;
  66
  67 let CONJ_ACI = prove
  68  (`(p /\ q <=> q /\ p) /\
  69    ((p /\ q) /\ r <=> p /\ (q /\ r)) /\
  70    (p /\ (q /\ r) <=> q /\ (p /\ r)) /\
  71    (p /\ p <=> p) /\
  72    (p /\ (p /\ q) <=> p /\ q)`,
  73   ITAUT_TAC);;
  74
  75 let DISJ_ASSOC = prove
  76  (`!t1 t2 t3. t1 \/ t2 \/ t3 <=> (t1 \/ t2) \/ t3`,
  77   ITAUT_TAC);;
  78
  79 let DISJ_SYM = prove
  80  (`!t1 t2. t1 \/ t2 <=> t2 \/ t1`,
  81   ITAUT_TAC);;
  82
  83 let DISJ_ACI = prove
  84  (`(p \/ q <=> q \/ p) /\
  85    ((p \/ q) \/ r <=> p \/ (q \/ r)) /\
  86    (p \/ (q \/ r) <=> q \/ (p \/ r)) /\
  87    (p \/ p <=> p) /\
  88    (p \/ (p \/ q) <=> p \/ q)`,
  89   ITAUT_TAC);;
  90
  91 let IMP_CONJ = prove
  92  (`p /\ q ==> r <=> p ==> q ==> r`,
  93   ITAUT_TAC);;
  94
  95 let IMP_IMP = GSYM IMP_CONJ;;
  96
  97 let IMP_CONJ_ALT = prove
  98  (`p /\ q ==> r <=> q ==> p ==> r`,
  99   ITAUT_TAC);;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* A couple of "distribution" tautologies are useful.                        *)
 103 (* ------------------------------------------------------------------------- *)
 104
 105 let LEFT_OR_DISTRIB = prove
 106  (`!p q r. p /\ (q \/ r) <=> p /\ q \/ p /\ r`,
 107   ITAUT_TAC);;
 108
 109 let RIGHT_OR_DISTRIB = prove
 110  (`!p q r. (p \/ q) /\ r <=> p /\ r \/ q /\ r`,
 111   ITAUT_TAC);;
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* Degenerate cases of quantifiers.                                          *)
 115 (* ------------------------------------------------------------------------- *)
 116
 117 let FORALL_SIMP = prove
 118  (`!t. (!x:A. t) = t`,
 119   ITAUT_TAC);;
 120
 121 let EXISTS_SIMP = prove
 122  (`!t. (?x:A. t) = t`,
 123   ITAUT_TAC);;
 124
 125 (* ------------------------------------------------------------------------- *)
 126 (* I also use this a lot (as a prelude to congruence reasoning).             *)
 127 (* ------------------------------------------------------------------------- *)
 128
 129 let EQ_IMP = ITAUT `(a <=> b) ==> a ==> b`;;
 130
 131 (* ------------------------------------------------------------------------- *)
 132 (* Start building up the basic rewrites; we add a few more later.            *)
 133 (* ------------------------------------------------------------------------- *)
 134
 135 let EQ_CLAUSES = prove
 136  (`!t. ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\
 137        ((F <=> t) <=> ~t) /\ ((t <=> F) <=> ~t)`,
 138   ITAUT_TAC);;
 139
 140 let NOT_CLAUSES_WEAK = prove
 141  (`(~T <=> F) /\ (~F <=> T)`,
 142   ITAUT_TAC);;
 143
 144 let AND_CLAUSES = prove
 145  (`!t. (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
 146        (t /\ F <=> F) /\ (t /\ t <=> t)`,
 147   ITAUT_TAC);;
 148
 149 let OR_CLAUSES = prove
 150  (`!t. (T \/ t <=> T) /\ (t \/ T <=> T) /\ (F \/ t <=> t) /\
 151        (t \/ F <=> t) /\ (t \/ t <=> t)`,
 152   ITAUT_TAC);;
 153
 154 let IMP_CLAUSES = prove
 155  (`!t. (T ==> t <=> t) /\ (t ==> T <=> T) /\ (F ==> t <=> T) /\
 156        (t ==> t <=> T) /\ (t ==> F <=> ~t)`,
 157   ITAUT_TAC);;
 158
 159 extend_basic_rewrites
 160   [REFL_CLAUSE;
 161    EQ_CLAUSES;
 162    NOT_CLAUSES_WEAK;
 163    AND_CLAUSES;
 164    OR_CLAUSES;
 165    IMP_CLAUSES;
 166    FORALL_SIMP;
 167    EXISTS_SIMP;
 168    BETA_THM;
 169    let IMP_EQ_CLAUSE = prove
 170     (`((x = x) ==> p) <=> p`,
 171      REWRITE_TAC[EQT_INTRO(SPEC_ALL EQ_REFL); IMP_CLAUSES]) in
 172    IMP_EQ_CLAUSE];;
 173
 174 extend_basic_congs
 175   [ITAUT `(p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')`];;
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* Rewrite rule for unique existence.                                        *)
 179 (* ------------------------------------------------------------------------- *)
 180
 181 let EXISTS_UNIQUE_THM = prove
 182  (`!P. (?!x:A. P x) <=> (?x. P x) /\ (!x x'. P x /\ P x' ==> (x = x'))`,
 183   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_DEF]);;
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* Trivial instances of existence.                                           *)
 187 (* ------------------------------------------------------------------------- *)
 188
 189 let EXISTS_REFL = prove
 190  (`!a:A. ?x. x = a`,
 191   GEN_TAC THEN EXISTS_TAC `a:A` THEN REFL_TAC);;
 192
 193 let EXISTS_UNIQUE_REFL = prove
 194  (`!a:A. ?!x. x = a`,
 195   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 196   REPEAT(EQ_TAC ORELSE STRIP_TAC) THENL
 197    [EXISTS_TAC `a:A`; ASM_REWRITE_TAC[]] THEN
 198   REFL_TAC);;
 199
 200 (* ------------------------------------------------------------------------- *)
 201 (* Unwinding.                                                                *)
 202 (* ------------------------------------------------------------------------- *)
 203
 204 let UNWIND_THM1 = prove
 205  (`!P (a:A). (?x. a = x /\ P x) <=> P a`,
 206   REPEAT GEN_TAC THEN EQ_TAC THENL
 207    [DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC ACCEPT_TAC));
 208     DISCH_TAC THEN EXISTS_TAC `a:A` THEN
 209     CONJ_TAC THEN TRY(FIRST_ASSUM MATCH_ACCEPT_TAC) THEN
 210     REFL_TAC]);;
 211
 212 let UNWIND_THM2 = prove
 213  (`!P (a:A). (?x. x = a /\ P x) <=> P a`,
 214   REPEAT GEN_TAC THEN CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
 215   MATCH_ACCEPT_TAC UNWIND_THM1);;
 216
 217 let FORALL_UNWIND_THM2 = prove
 218  (`!P (a:A). (!x. x = a ==> P x) <=> P a`,
 219   REPEAT GEN_TAC THEN EQ_TAC THENL
 220    [DISCH_THEN(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[];
 221     DISCH_TAC THEN GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
 222     ASM_REWRITE_TAC[]]);;
 223
 224 let FORALL_UNWIND_THM1 = prove
 225  (`!P a. (!x. a = x ==> P x) <=> P a`,
 226   REPEAT GEN_TAC THEN CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
 227   MATCH_ACCEPT_TAC FORALL_UNWIND_THM2);;
 228
 229 (* ------------------------------------------------------------------------- *)
 230 (* Permuting quantifiers.                                                    *)
 231 (* ------------------------------------------------------------------------- *)
 232
 233 let SWAP_FORALL_THM = prove
 234  (`!P:A->B->bool. (!x y. P x y) <=> (!y x. P x y)`,
 235   ITAUT_TAC);;
 236
 237 let SWAP_EXISTS_THM = prove
 238  (`!P:A->B->bool. (?x y. P x y) <=> (?y x. P x y)`,
 239   ITAUT_TAC);;
 240
 241 (* ------------------------------------------------------------------------- *)
 242 (* Universal quantifier and conjunction.                                     *)
 243 (* ------------------------------------------------------------------------- *)
 244
 245 let FORALL_AND_THM = prove
 246  (`!P Q. (!x:A. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x)`,
 247   ITAUT_TAC);;
 248
 249 let AND_FORALL_THM = prove
 250  (`!P Q. (!x. P x) /\ (!x. Q x) <=> (!x:A. P x /\ Q x)`,
 251   ITAUT_TAC);;
 252
 253 let LEFT_AND_FORALL_THM = prove
 254  (`!P Q. (!x:A. P x) /\ Q <=> (!x:A. P x /\ Q)`,
 255   ITAUT_TAC);;
 256
 257 let RIGHT_AND_FORALL_THM = prove
 258  (`!P Q. P /\ (!x:A. Q x) <=> (!x. P /\ Q x)`,
 259   ITAUT_TAC);;
 260
 261 (* ------------------------------------------------------------------------- *)
 262 (* Existential quantifier and disjunction.                                   *)
 263 (* ------------------------------------------------------------------------- *)
 264
 265 let EXISTS_OR_THM = prove
 266  (`!P Q. (?x:A. P x \/ Q x) <=> (?x. P x) \/ (?x. Q x)`,
 267   ITAUT_TAC);;
 268
 269 let OR_EXISTS_THM = prove
 270  (`!P Q. (?x. P x) \/ (?x. Q x) <=> (?x:A. P x \/ Q x)`,
 271   ITAUT_TAC);;
 272
 273 let LEFT_OR_EXISTS_THM = prove
 274  (`!P Q. (?x. P x) \/ Q <=> (?x:A. P x \/ Q)`,
 275   ITAUT_TAC);;
 276
 277 let RIGHT_OR_EXISTS_THM = prove
 278  (`!P Q. P \/ (?x. Q x) <=> (?x:A. P \/ Q x)`,
 279   ITAUT_TAC);;
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* Existential quantifier and conjunction.                                   *)
 283 (* ------------------------------------------------------------------------- *)
 284
 285 let LEFT_EXISTS_AND_THM = prove
 286  (`!P Q. (?x:A. P x /\ Q) <=> (?x:A. P x) /\ Q`,
 287   ITAUT_TAC);;
 288
 289 let RIGHT_EXISTS_AND_THM = prove
 290  (`!P Q. (?x:A. P /\ Q x) <=> P /\ (?x:A. Q x)`,
 291   ITAUT_TAC);;
 292
 293 let TRIV_EXISTS_AND_THM = prove
 294  (`!P Q. (?x:A. P /\ Q) <=> (?x:A. P) /\ (?x:A. Q)`,
 295   ITAUT_TAC);;
 296
 297 let LEFT_AND_EXISTS_THM = prove
 298  (`!P Q. (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)`,
 299   ITAUT_TAC);;
 300
 301 let RIGHT_AND_EXISTS_THM = prove
 302  (`!P Q. P /\ (?x:A. Q x) <=> (?x:A. P /\ Q x)`,
 303   ITAUT_TAC);;
 304
 305 let TRIV_AND_EXISTS_THM = prove
 306  (`!P Q. (?x:A. P) /\ (?x:A. Q) <=> (?x:A. P /\ Q)`,
 307   ITAUT_TAC);;
 308
 309 (* ------------------------------------------------------------------------- *)
 310 (* Only trivial instances of universal quantifier and disjunction.           *)
 311 (* ------------------------------------------------------------------------- *)
 312
 313 let TRIV_FORALL_OR_THM = prove
 314  (`!P Q. (!x:A. P \/ Q) <=> (!x:A. P) \/ (!x:A. Q)`,
 315   ITAUT_TAC);;
 316
 317 let TRIV_OR_FORALL_THM = prove
 318  (`!P Q. (!x:A. P) \/ (!x:A. Q) <=> (!x:A. P \/ Q)`,
 319   ITAUT_TAC);;
 320
 321 (* ------------------------------------------------------------------------- *)
 322 (* Implication and quantifiers.                                              *)
 323 (* ------------------------------------------------------------------------- *)
 324
 325 let RIGHT_IMP_FORALL_THM = prove
 326  (`!P Q. (P ==> !x:A. Q x) <=> (!x. P ==> Q x)`,
 327   ITAUT_TAC);;
 328
 329 let RIGHT_FORALL_IMP_THM = prove
 330  (`!P Q. (!x. P ==> Q x) <=> (P ==> !x:A. Q x)`,
 331   ITAUT_TAC);;
 332
 333 let LEFT_IMP_EXISTS_THM = prove
 334  (`!P Q. ((?x:A. P x) ==> Q) <=> (!x. P x ==> Q)`,
 335   ITAUT_TAC);;
 336
 337 let LEFT_FORALL_IMP_THM = prove
 338  (`!P Q. (!x. P x ==> Q) <=> ((?x:A. P x) ==> Q)`,
 339   ITAUT_TAC);;
 340
 341 let TRIV_FORALL_IMP_THM = prove
 342  (`!P Q. (!x:A. P ==> Q) <=> ((?x:A. P) ==> (!x:A. Q))`,
 343   ITAUT_TAC);;
 344
 345 let TRIV_EXISTS_IMP_THM = prove
 346  (`!P Q. (?x:A. P ==> Q) <=> ((!x:A. P) ==> (?x:A. Q))`,
 347   ITAUT_TAC);;
 348
 349 (* ------------------------------------------------------------------------- *)
 350 (* Alternative versions of unique existence.                                 *)
 351 (* ------------------------------------------------------------------------- *)
 352
 353 let EXISTS_UNIQUE_ALT = prove
 354  (`!P:A->bool. (?!x. P x) <=> (?x. !y. P y <=> (x = y))`,
 355   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN EQ_TAC THENL
 356    [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `x:A`) ASSUME_TAC) THEN
 357     EXISTS_TAC `x:A` THEN GEN_TAC THEN EQ_TAC THENL
 358      [DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 359       DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_ACCEPT_TAC];
 360     DISCH_THEN(X_CHOOSE_TAC `x:A`) THEN
 361     ASM_REWRITE_TAC[GSYM EXISTS_REFL] THEN REPEAT GEN_TAC THEN
 362     DISCH_THEN(CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN REFL_TAC]);;
 363
 364 let EXISTS_UNIQUE = prove
 365  (`!P:A->bool. (?!x. P x) <=> (?x. P x /\ !y. P y ==> (y = x))`,
 366   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT] THEN
 367   AP_TERM_TAC THEN ABS_TAC THEN
 368   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV)
 369    [ITAUT `(a <=> b) <=> (a ==> b) /\ (b ==> a)`] THEN
 370   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
 371   REWRITE_TAC[FORALL_AND_THM] THEN SIMP_TAC[] THEN
 372   REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
 373   REWRITE_TAC[CONJ_ACI]);;
 374
 375 (* ------------------------------------------------------------------------- *)
 376 (* DESTRUCT_TAC, FIX_TAC and INTRO_TAC, giving more brief and elegant ways   *)
 377 (* of naming introduced variables and assumptions (from Marco Maggesi).      *)
 378 (* ------------------------------------------------------------------------- *)
 379
 380 let DESTRUCT_TAC,FIX_TAC,INTRO_TAC =
 381   let NAME_GEN_TAC s gl =
 382     let ty = (snd o dest_var o fst o dest_forall o snd) gl  in
 383     X_GEN_TAC (mk_var(s,ty)) gl
 384   and OBTAIN_THEN v ttac th =
 385     let ty = (snd o dest_var o fst o dest_exists o concl) th in
 386     X_CHOOSE_THEN (mk_var(v,ty)) ttac th
 387   and CONJ_LIST_TAC = end_itlist (fun t1 t2 -> CONJ_TAC THENL [t1; t2])
 388   and NUM_DISJ_TAC n =
 389     if n <= 0 then failwith "NUM_DISJ_TAC" else
 390     REPLICATE_TAC (n-1) DISJ2_TAC THEN REPEAT DISJ1_TAC
 391   and NAME_PULL_FORALL_CONV =
 392     let SWAP_FORALL_CONV = REWR_CONV SWAP_FORALL_THM
 393     and AND_FORALL_CONV = GEN_REWRITE_CONV I [AND_FORALL_THM]
 394     and RIGHT_IMP_FORALL_CONV = GEN_REWRITE_CONV I [RIGHT_IMP_FORALL_THM] in
 395     fun s ->
 396       let rec PULL_FORALL tm =
 397           if is_forall tm then
 398             if name_of(fst(dest_forall tm)) = s then REFL tm else
 399               (BINDER_CONV PULL_FORALL THENC SWAP_FORALL_CONV) tm
 400           else if is_imp tm then
 401             (RAND_CONV PULL_FORALL THENC RIGHT_IMP_FORALL_CONV) tm
 402           else if is_conj tm then
 403             (BINOP_CONV PULL_FORALL THENC AND_FORALL_CONV) tm
 404           else
 405             fail () in
 406       PULL_FORALL in
 407   let parse_fix =
 408     let ident = function
 409         Ident s::rest when isalpha s -> s,rest
 410       | _ -> raise Noparse in
 411     let rename =
 412       let old_name = possibly (a(Ident "/") ++ ident >> snd) in
 413       (a(Resword "[") ++ ident >> snd) ++ old_name ++ a(Resword "]") >> fst in
 414     let mk_var v = CONV_TAC (NAME_PULL_FORALL_CONV v) THEN GEN_TAC
 415     and mk_rename =
 416       function u,[v] -> CONV_TAC (NAME_PULL_FORALL_CONV v) THEN NAME_GEN_TAC u
 417              | u,_   -> NAME_GEN_TAC u in
 418     let vars = many (rename >> mk_rename || ident >> mk_var) >> EVERY
 419     and star = possibly (a (Ident "*") >> K (REPEAT GEN_TAC)) in
 420     vars ++ star >> function tac,[] -> tac | tac,_ -> tac THEN REPEAT GEN_TAC
 421   and parse_destruct =
 422     let OBTAINL_THEN : string list -> thm_tactical =
 423       EVERY_TCL o map OBTAIN_THEN in
 424     let ident p = function
 425         Ident s::rest when p s -> s,rest
 426       | _ -> raise Noparse in
 427     let rec destruct inp = disj inp
 428     and disj inp =
 429       let DISJ_CASES_LIST = end_itlist DISJ_CASES_THEN2 in
 430       (listof conj (a(Resword "|")) "Disjunction" >> DISJ_CASES_LIST) inp
 431     and conj inp = (atleast 1 atom >> end_itlist CONJUNCTS_THEN2) inp
 432     and obtain inp =
 433       let obtain_prfx =
 434         let var_list = atleast 1 (ident isalpha) in
 435         (a(Ident "@") ++ var_list >> snd) ++ a(Resword ".") >> fst in
 436       (obtain_prfx ++ destruct >> uncurry OBTAINL_THEN) inp
 437     and atom inp =
 438       let label = ident isalnum >> LABEL_TAC in
 439       let paren =
 440        (a(Resword "(") ++ destruct >> snd) ++ a(Resword ")") >> fst in
 441       (label || obtain || paren) inp in
 442     destruct in
 443   let parse_intro =
 444     let number = function
 445         Ident s::rest ->
 446           (try
 447              let n = int_of_string s in
 448              if n < 1 then raise Noparse else n,rest
 449            with Failure _ -> raise Noparse)
 450       | _ -> raise Noparse
 451     and pa_fix = a(Ident "!") ++ parse_fix >> snd
 452     and pa_dest = parse_destruct >> DISCH_THEN in
 453     let pa_prefix =
 454       elistof (pa_fix || pa_dest) (a(Resword ";")) "Prefix intro pattern" in
 455     let rec pa_intro toks =
 456       (pa_prefix ++ possibly pa_postfix >> uncurry (@) >> EVERY) toks
 457     and pa_postfix toks = (pa_conj || pa_disj) toks
 458     and pa_conj toks =
 459       let conjs =
 460         listof pa_intro (a(Ident "&")) "Intro pattern" >> CONJ_LIST_TAC in
 461       ((a(Resword "{") ++ conjs >> snd) ++ a(Resword "}") >> fst) toks
 462     and pa_disj toks =
 463       let disj = number >> NUM_DISJ_TAC in
 464       ((a(Ident "#") ++ disj >> snd) ++ pa_intro >> uncurry (THEN)) toks in
 465     pa_intro in
 466   let DESTRUCT_TAC s =
 467     let tac,rest =
 468       (fix "Destruct pattern" parse_destruct o lex o explode) s in
 469     if rest=[] then tac else failwith "Garbage after destruct pattern"
 470   and INTRO_TAC s =
 471     let tac,rest =
 472       (fix "Introduction pattern" parse_intro o lex o explode) s in
 473     if rest=[] then tac else failwith "Garbage after intro pattern"
 474   and FIX_TAC s =
 475     let tac,rest = (parse_fix o lex o explode) s in
 476     if rest=[] then tac else failwith "FIX_TAC: invalid pattern" in
 477   DESTRUCT_TAC,FIX_TAC,INTRO_TAC;;