ind_defs.ml

   1 (* ========================================================================= *)
   2 (* Mutually inductively defined relations.                                   *)
   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 "theorems.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Strip off exactly n arguments from combination.                           *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let strip_ncomb =
  17   let rec strip(n,tm,acc) =
  18     if n < 1 then tm,acc else
  19     let l,r = dest_comb tm in
  20     strip(n - 1,l,r::acc) in
  21   fun n tm -> strip(n,tm,[]);;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Expand lambda-term function definition with its arguments.                *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let RIGHT_BETAS =
  28   rev_itlist (fun a -> CONV_RULE (RAND_CONV BETA_CONV) o C AP_THM a);;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (*      A, x = t |- P[x]                                                     *)
  32 (*     ------------------ EXISTS_EQUATION                                    *)
  33 (*        A |- ?x. P[x]                                                      *)
  34 (* ------------------------------------------------------------------------- *)
  35
  36 let EXISTS_EQUATION =
  37   let pth = prove
  38    (`!P t. (!x:A. (x = t) ==> P x) ==> (?) P`,
  39     REWRITE_TAC[EXISTS_DEF] THEN BETA_TAC THEN
  40     REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
  41     EXISTS_TAC `t:A` THEN FIRST_ASSUM MATCH_MP_TAC THEN
  42     REFL_TAC) in
  43   fun tm th ->
  44     let l,r = dest_eq tm in
  45     let P = mk_abs(l,concl th) in
  46     let th1 = BETA_CONV(mk_comb(P,l)) in
  47     let th2 = ISPECL [P; r] pth in
  48     let th3 = EQ_MP (SYM th1) th in
  49     let th4 = GEN l (DISCH tm th3) in
  50     MP th2 th4;;
  51
  52 (* ========================================================================= *)
  53 (* Part 1: The main part of the inductive definitions package.               *)
  54 (* This proves that a certain definition yields the requires theorems.       *)
  55 (* ========================================================================= *)
  56
  57 let derive_nonschematic_inductive_relations =
  58   let getconcl tm =
  59     let bod = repeat (snd o dest_forall) tm in
  60     try snd(dest_imp bod) with Failure _ -> bod
  61   and CONJ_ACI_RULE = AC CONJ_ACI
  62   and SIMPLE_DISJ_PAIR th =
  63     let l,r = dest_disj(hd(hyp th)) in
  64     PROVE_HYP (DISJ1 (ASSUME l) r) th,PROVE_HYP (DISJ2 l (ASSUME r)) th
  65   and HALF_BETA_EXPAND args th = GENL args (RIGHT_BETAS args th) in
  66   let AND_IMPS_CONV tm =
  67     let ths = CONJUNCTS(ASSUME tm) in
  68     let avs = fst(strip_forall(concl(hd ths))) in
  69     let thl = map (DISCH tm o UNDISCH o SPEC_ALL) ths in
  70     let th1 = end_itlist SIMPLE_DISJ_CASES thl in
  71     let tm1 = hd(hyp th1) in
  72     let th2 = GENL avs (DISCH tm1 (UNDISCH th1)) in
  73     let tm2 = concl th2 in
  74     let th3 = DISCH tm2 (UNDISCH (SPEC_ALL (ASSUME tm2))) in
  75     let thts,tht =  nsplit SIMPLE_DISJ_PAIR (tl ths) th3 in
  76     let proc_fn th =
  77       let t = hd(hyp th) in GENL avs (DISCH t (UNDISCH th)) in
  78     let th4 = itlist (CONJ o proc_fn) thts (proc_fn tht) in
  79     IMP_ANTISYM_RULE (DISCH_ALL th2) (DISCH_ALL th4) in
  80   let t_tm = `T` in
  81   let calculate_simp_sequence =
  82     let rec getequs(avs,plis) =
  83       if plis = [] then [] else
  84       let h::t = plis in
  85       let r = snd h in
  86       if mem r avs then
  87         h::(getequs(avs,filter ((<>) r o snd) t))
  88       else
  89         getequs(avs,t) in
  90     fun avs plis ->
  91       let oks = getequs(avs,plis) in
  92       oks,subtract plis oks
  93   and FORALL_IMPS_CONV tm =
  94     let avs,bod = strip_forall tm in
  95     let th1 = DISCH tm (UNDISCH(SPEC_ALL(ASSUME tm))) in
  96     let th2 = itlist SIMPLE_CHOOSE avs th1 in
  97     let tm2 = hd(hyp th2) in
  98     let th3 = DISCH tm2 (UNDISCH th2) in
  99     let th4 = ASSUME (concl th3) in
 100     let ant = lhand bod in
 101     let th5 = itlist SIMPLE_EXISTS avs (ASSUME ant) in
 102     let th6 = GENL avs (DISCH ant (MP th4 th5)) in
 103     IMP_ANTISYM_RULE (DISCH_ALL th3) (DISCH_ALL th6) in
 104   let canonicalize_clause cls args =
 105     let avs,bimp = strip_forall cls in
 106     let ant,con = try dest_imp bimp with Failure _ -> t_tm,bimp in
 107     let rel,xargs = strip_comb con in
 108     let plis = zip args xargs in
 109     let yes,no = calculate_simp_sequence avs plis in
 110     let nvs = filter (not o C mem (map snd yes)) avs in
 111     let eth =
 112       if is_imp bimp then
 113         let atm = itlist (curry mk_conj o mk_eq) (yes@no) ant in
 114         let ths,tth = nsplit CONJ_PAIR plis (ASSUME atm) in
 115         let thl = map (fun t -> find (fun th -> lhs(concl th) = t) ths) args in
 116         let th0 = MP (SPECL avs (ASSUME cls)) tth in
 117         let th1 = rev_itlist (C (curry MK_COMB)) thl (REFL rel) in
 118         let th2 = EQ_MP (SYM th1) th0 in
 119         let th3 = INST yes (DISCH atm th2) in
 120         let tm4 = funpow (length yes) rand (lhand(concl th3)) in
 121         let th4 = itlist (CONJ o REFL o fst) yes (ASSUME tm4) in
 122         let th5 = GENL args (GENL nvs (DISCH tm4 (MP th3 th4))) in
 123         let th6 = SPECL nvs (SPECL (map snd plis) (ASSUME (concl th5))) in
 124         let th7 = itlist (CONJ o REFL o snd) no (ASSUME ant) in
 125         let th8 = GENL avs (DISCH ant (MP th6 th7)) in
 126         IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8)
 127       else
 128         let atm = list_mk_conj(map mk_eq (yes@no)) in
 129         let ths = CONJUNCTS (ASSUME atm) in
 130         let thl = map (fun t -> find (fun th -> lhs(concl th) = t) ths) args in
 131         let th0 = SPECL avs (ASSUME cls) in
 132         let th1 = rev_itlist (C (curry MK_COMB)) thl (REFL rel) in
 133         let th2 = EQ_MP (SYM th1) th0 in
 134         let th3 = INST yes (DISCH atm th2) in
 135         let tm4 = funpow (length yes) rand (lhand(concl th3)) in
 136         let th4 = itlist (CONJ o REFL o fst) yes (ASSUME tm4) in
 137         let th5 = GENL args (GENL nvs (DISCH tm4 (MP th3 th4))) in
 138         let th6 = SPECL nvs (SPECL (map snd plis) (ASSUME (concl th5))) in
 139         let th7 = end_itlist CONJ (map (REFL o snd) no) in
 140         let th8 = GENL avs (MP th6 th7) in
 141         IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th8) in
 142     let ftm = funpow (length args) (body o rand) (rand(concl eth)) in
 143     TRANS eth (itlist MK_FORALL args (FORALL_IMPS_CONV ftm)) in
 144   let canonicalize_clauses clauses =
 145     let concls = map getconcl clauses in
 146     let uncs = map strip_comb concls in
 147     let rels = itlist (insert o fst) uncs [] in
 148     let xargs = map (C assoc uncs) rels in
 149     let closed = list_mk_conj clauses in
 150     let avoids = variables closed in
 151     let flargs =
 152       make_args "a" avoids (map type_of (end_itlist (@) xargs)) in
 153     let zargs = zip rels (shareout xargs flargs) in
 154     let cargs = map (fun (r,a) -> assoc r zargs) uncs in
 155     let cthms = map2 canonicalize_clause clauses cargs in
 156     let pclauses = map (rand o concl) cthms in
 157     let collectclauses tm =
 158       mapfilter (fun t -> if fst t = tm then snd t else fail())
 159                 (zip (map fst uncs) pclauses) in
 160     let clausell = map collectclauses rels in
 161     let cclausel = map list_mk_conj clausell in
 162     let cclauses = list_mk_conj cclausel
 163     and oclauses = list_mk_conj pclauses in
 164     let eth = CONJ_ACI_RULE(mk_eq(oclauses,cclauses)) in
 165     let pth = TRANS (end_itlist MK_CONJ cthms) eth in
 166     TRANS pth (end_itlist MK_CONJ (map AND_IMPS_CONV cclausel))
 167   and derive_canon_inductive_relations clauses =
 168     let closed = list_mk_conj clauses in
 169     let clauses = conjuncts closed in
 170     let vargs,bodies = unzip(map strip_forall clauses) in
 171     let ants,concs = unzip(map dest_imp bodies) in
 172     let rels = map (repeat rator) concs in
 173     let avoids = variables closed in
 174     let rels' = variants avoids rels in
 175     let crels = zip rels' rels in
 176     let prime_fn = subst crels in
 177     let closed' = prime_fn closed in
 178     let mk_def arg con =
 179       mk_eq(repeat rator con,
 180         list_mk_abs(arg,list_mk_forall(rels',mk_imp(closed',prime_fn con)))) in
 181     let deftms = map2 mk_def vargs concs in
 182     let defthms = map2 HALF_BETA_EXPAND vargs (map ASSUME deftms) in
 183     let mk_ind args th =
 184       let th1 = fst(EQ_IMP_RULE(SPEC_ALL th)) in
 185       let ant = lhand(concl th1) in
 186       let th2 = SPECL rels' (UNDISCH th1) in
 187       GENL args (DISCH ant (UNDISCH th2)) in
 188     let indthms = map2 mk_ind vargs defthms in
 189     let indthmr = end_itlist CONJ indthms in
 190     let indthm = GENL rels' (DISCH closed' indthmr) in
 191     let mconcs = map2 (fun a t -> list_mk_forall(a,mk_imp(t,prime_fn t)))
 192       vargs ants in
 193     let monotm = mk_imp(concl indthmr,list_mk_conj mconcs) in
 194     let monothm = ASSUME(list_mk_forall(rels,list_mk_forall(rels',monotm))) in
 195     let closthm = ASSUME closed' in
 196     let monothms = CONJUNCTS
 197       (MP (SPEC_ALL monothm) (MP (SPECL rels' indthm) closthm)) in
 198     let closthms = CONJUNCTS closthm in
 199     let prove_rule mth (cth,dth) =
 200       let avs,bod = strip_forall(concl mth) in
 201       let th1 = IMP_TRANS (SPECL avs mth) (SPECL avs cth) in
 202       let th2 = GENL rels' (DISCH closed' (UNDISCH th1)) in
 203       let th3 = EQ_MP (SYM (SPECL avs dth)) th2 in
 204       GENL avs (DISCH (lhand bod) th3) in
 205     let rulethms = map2 prove_rule monothms (zip closthms defthms) in
 206     let rulethm = end_itlist CONJ rulethms in
 207     let dtms = map2 (curry list_mk_abs) vargs ants in
 208     let double_fn = subst (zip dtms rels) in
 209     let mk_unbetas tm dtm =
 210       let avs,bod = strip_forall tm in
 211       let il,r = dest_comb bod in
 212       let i,l = dest_comb il in
 213       let bth = RIGHT_BETAS avs (REFL dtm) in
 214       let munb = AP_THM (AP_TERM i bth) r in
 215       let iunb = AP_TERM (mk_comb(i,double_fn l)) bth in
 216       let junb = AP_TERM (mk_comb(i,r)) bth in
 217       let quantify = itlist MK_FORALL avs in
 218       (quantify munb,(quantify iunb,quantify junb)) in
 219     let unths = map2 mk_unbetas clauses dtms in
 220     let irthm = EQ_MP (SYM(end_itlist MK_CONJ (map fst unths))) rulethm in
 221     let mrthm = MP (SPECL rels (SPECL dtms monothm)) irthm in
 222     let imrth = EQ_MP (SYM(end_itlist MK_CONJ (map (fst o snd) unths))) mrthm in
 223     let ifthm = MP (SPECL dtms indthm) imrth in
 224     let fthm = EQ_MP (end_itlist MK_CONJ (map (snd o snd) unths)) ifthm in
 225     let mk_case th1 th2 =
 226       let avs = fst(strip_forall(concl th1)) in
 227       GENL avs (IMP_ANTISYM_RULE (SPEC_ALL th1) (SPEC_ALL th2)) in
 228     let casethm = end_itlist CONJ
 229       (map2 mk_case (CONJUNCTS fthm) (CONJUNCTS rulethm)) in
 230     CONJ rulethm (CONJ indthm casethm) in
 231   fun tm ->
 232     let clauses = conjuncts tm in
 233     let canonthm = canonicalize_clauses clauses in
 234     let canonthm' = SYM canonthm in
 235     let pclosed = rand(concl canonthm) in
 236     let pclauses = conjuncts pclosed in
 237     let rawthm = derive_canon_inductive_relations pclauses in
 238     let rulethm,otherthms = CONJ_PAIR rawthm in
 239     let indthm,casethm = CONJ_PAIR otherthms in
 240     let rulethm' = EQ_MP canonthm' rulethm
 241     and indthm' = CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV canonthm')) indthm in
 242     CONJ rulethm' (CONJ indthm' casethm);;
 243
 244 (* ========================================================================= *)
 245 (* Part 2: Tactic-integrated tools for proving monotonicity automatically.   *)
 246 (* ========================================================================= *)
 247
 248 let MONO_AND = ITAUT `(A ==> B) /\ (C ==> D) ==> (A /\ C ==> B /\ D)`;;
 249
 250 let MONO_OR = ITAUT `(A ==> B) /\ (C ==> D) ==> (A \/ C ==> B \/ D)`;;
 251
 252 let MONO_IMP = ITAUT `(B ==> A) /\ (C ==> D) ==> ((A ==> C) ==> (B ==> D))`;;
 253
 254 let MONO_NOT = ITAUT `(B ==> A) ==> (~A ==> ~B)`;;
 255
 256 let MONO_FORALL = prove
 257  (`(!x:A. P x ==> Q x) ==> ((!x. P x) ==> (!x. Q x))`,
 258   REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 259   ASM_REWRITE_TAC[]);;
 260
 261 let MONO_EXISTS = prove
 262  (`(!x:A. P x ==> Q x) ==> ((?x. P x) ==> (?x. Q x))`,
 263   DISCH_TAC THEN DISCH_THEN(X_CHOOSE_TAC `x:A`) THEN
 264   EXISTS_TAC `x:A` THEN FIRST_ASSUM MATCH_MP_TAC THEN
 265   ASM_REWRITE_TAC[]);;
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* Assignable list of monotonicity theorems, so users can add their own.     *)
 269 (* ------------------------------------------------------------------------- *)
 270
 271 let monotonicity_theorems = ref
 272  [MONO_AND; MONO_OR; MONO_IMP; MONO_NOT; MONO_EXISTS; MONO_FORALL];;
 273
 274 (* ------------------------------------------------------------------------- *)
 275 (* Attempt to backchain through the monotonicity theorems.                   *)
 276 (* ------------------------------------------------------------------------- *)
 277
 278 let MONO_TAC =
 279   let imp = `(==>)` and IMP_REFL = ITAUT `!p. p ==> p` in
 280   let BACKCHAIN_TAC th =
 281     let match_fn = PART_MATCH (snd o dest_imp) th in
 282     fun (asl,w) ->
 283       let th1 = match_fn w in
 284       let ant,con = dest_imp(concl th1) in
 285       null_meta,[asl,ant],fun i [t] -> MATCH_MP (INSTANTIATE i th1) t
 286   and MONO_ABS_TAC (asl,w) =
 287     let ant,con = dest_imp w in
 288     let vars = snd(strip_comb con) in
 289     let rnum = length vars - 1 in
 290     let hd1,args1 = strip_ncomb rnum ant
 291     and hd2,args2 = strip_ncomb rnum con in
 292     let th1 = rev_itlist (C AP_THM) args1 (BETA_CONV hd1)
 293     and th2 = rev_itlist (C AP_THM) args1 (BETA_CONV hd2) in
 294     let th3 = MK_COMB(AP_TERM imp th1,th2) in
 295     CONV_TAC(REWR_CONV th3) (asl,w)
 296   and APPLY_MONOTAC tacs (asl,w) =
 297     let a,c = dest_imp w in
 298     if aconv a c then ACCEPT_TAC (SPEC a IMP_REFL) (asl,w) else
 299     let cn = try fst(dest_const(repeat rator c)) with Failure _ -> "" in
 300     tryfind (fun (k,t) -> if k = cn then t (asl,w) else fail()) tacs in
 301   fun gl ->
 302     let tacs = itlist
 303       (fun th l -> let ft = repeat rator (funpow 2 rand (concl th)) in
 304                    let c = try fst(dest_const ft) with Failure _ -> "" in
 305                    (c,BACKCHAIN_TAC th THEN REPEAT CONJ_TAC)::l)
 306       (!monotonicity_theorems) ["",MONO_ABS_TAC] in
 307     let MONO_STEP_TAC = REPEAT GEN_TAC THEN APPLY_MONOTAC tacs in
 308     (REPEAT MONO_STEP_TAC THEN ASM_REWRITE_TAC[]) gl;;
 309
 310 (* ------------------------------------------------------------------------- *)
 311 (* Attempt to dispose of the non-equational assumption(s) of a theorem.      *)
 312 (* ------------------------------------------------------------------------- *)
 313
 314 let prove_monotonicity_hyps =
 315   let tac = REPEAT GEN_TAC THEN
 316     DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
 317     REPEAT CONJ_TAC THEN MONO_TAC in
 318   let prove_mth t = prove(t,tac) in
 319   fun th ->
 320     let mths = mapfilter prove_mth (filter (not o is_eq) (hyp th)) in
 321     itlist PROVE_HYP mths th;;
 322
 323 (* ========================================================================= *)
 324 (* Part 3: The final user wrapper, with schematic variables added.           *)
 325 (* ========================================================================= *)
 326
 327 let the_inductive_definitions = ref [];;
 328
 329 let prove_inductive_relations_exist,new_inductive_definition =
 330   let rec pare_comb qvs tm =
 331     if intersect (frees tm) qvs = [] & forall is_var (snd(strip_comb tm))
 332     then tm
 333     else pare_comb qvs (rator tm) in
 334   let generalize_schematic_variables gflag vs =
 335     let generalize_def tm th =
 336       let l,r = dest_eq tm in
 337       let lname,lty = dest_var l in
 338       let l' = mk_var(lname,itlist (mk_fun_ty o type_of) vs lty) in
 339       let r' = list_mk_abs(vs,r) in
 340       let tm' = mk_eq(l',r') in
 341       let th0 = RIGHT_BETAS vs (ASSUME tm') in
 342       let th1 = INST [lhs(concl th0),l] (DISCH tm th) in
 343       MP th1 th0 in
 344     fun th ->
 345       let defs,others = partition is_eq (hyp th) in
 346       let th1 = itlist generalize_def defs th in
 347       if gflag then
 348         let others' = map (fun t -> let fvs = frees t in
 349                                     SPECL fvs (ASSUME (list_mk_forall(fvs,t))))
 350                           others in
 351         GENL vs (itlist PROVE_HYP others' th1)
 352       else th1
 353   and derive_existence th =
 354     let defs = filter is_eq (hyp th) in
 355     itlist EXISTS_EQUATION defs th
 356   and make_definitions th =
 357     let defs = filter is_eq (hyp th) in
 358     let dths = map new_definition defs in
 359     let insts = zip (map (lhs o concl) dths) (map lhs defs) in
 360     rev_itlist (C MP) dths (INST insts (itlist DISCH defs th))
 361   and unschematize_clauses clauses =
 362     let schem = map (fun cls -> let avs,bod = strip_forall cls in
 363                   pare_comb avs (try snd(dest_imp bod) with Failure _ -> bod))
 364                             clauses in
 365       let schems = setify schem in
 366       if is_var(hd schem) then (clauses,[]) else
 367       if not (length(setify (map (snd o strip_comb) schems)) = 1)
 368       then failwith "Schematic variables not used consistently" else
 369       let avoids = variables (list_mk_conj clauses) in
 370       let hack_fn tm = mk_var(fst(dest_var(repeat rator tm)),type_of tm) in
 371       let grels = variants avoids (map hack_fn schems) in
 372       let crels = zip grels schems in
 373       let clauses' = map (subst crels) clauses in
 374       clauses',snd(strip_comb(hd schems)) in
 375   let find_redefinition tm (rth,ith,cth as trip) =
 376     if aconv tm (concl rth) then trip else failwith "find_redefinition" in
 377   let prove_inductive_properties tm =
 378     let clauses = conjuncts tm in
 379     let clauses',fvs = unschematize_clauses clauses in
 380     let th = derive_nonschematic_inductive_relations (list_mk_conj clauses') in
 381     fvs,prove_monotonicity_hyps th in
 382   let prove_inductive_relations_exist tm =
 383     let fvs,th1 = prove_inductive_properties tm in
 384     let th2 = generalize_schematic_variables true fvs th1 in
 385     derive_existence th2
 386   and new_inductive_definition tm =
 387     try let th = tryfind (find_redefinition tm) (!the_inductive_definitions) in
 388         warn true "Benign redefinition of inductive predicate"; th
 389     with Failure _ ->
 390     let fvs,th1 = prove_inductive_properties tm in
 391     let th2 = generalize_schematic_variables true fvs th1 in
 392     let th3 = make_definitions th2 in
 393     let avs = fst(strip_forall(concl th3)) in
 394     let r,ic = CONJ_PAIR(SPECL avs th3) in
 395     let i,c = CONJ_PAIR ic in
 396     let thtr = GENL avs r,GENL avs i,GENL avs c in
 397     the_inductive_definitions := thtr::(!the_inductive_definitions);
 398     thtr in
 399   prove_inductive_relations_exist,new_inductive_definition;;
 400
 401 (* ------------------------------------------------------------------------- *)
 402 (* Derivation of "strong induction".                                         *)
 403 (* ------------------------------------------------------------------------- *)
 404
 405 let derive_strong_induction =
 406   let dest_ibod tm =
 407     let avs,ibod = strip_forall tm in
 408     let n = length avs in
 409     let prator = funpow n rator in
 410     let ant,con = dest_imp ibod in
 411     n,(prator ant,prator con) in
 412   let rec prove_triv tm =
 413     if is_conj tm then CONJ (prove_triv(lhand tm)) (prove_triv(rand tm)) else
 414     let avs,bod = strip_forall tm in
 415     let a,c = dest_imp bod in
 416     let ths = CONJUNCTS(ASSUME a) in
 417     let th = find (aconv c o concl) ths in
 418     GENL avs (DISCH a th) in
 419   let rec weaken_triv th =
 420     if is_conj(concl th)
 421     then CONJ (weaken_triv(CONJUNCT1 th)) (weaken_triv(CONJUNCT2 th)) else
 422     let avs,bod = strip_forall(concl th) in
 423     let th1 = SPECL avs th in
 424     let a = fst(dest_imp(concl th1)) in
 425     GENL avs (DISCH a (CONJUNCT2 (UNDISCH th1))) in
 426   let MATCH_IMPS = MATCH_MP MONO_AND in
 427   fun (rth,ith) ->
 428     let ovs,ibod = strip_forall(concl ith) in
 429     let iant,icon = dest_imp ibod in
 430     let ns,prrs = unzip (map dest_ibod (conjuncts icon)) in
 431     let rs,ps = unzip prrs in
 432     let gs = variants (variables ibod) ps in
 433     let svs,tvs = chop_list (length ovs - length ns) ovs in
 434     let sth = SPECL svs rth and jth = SPECL svs ith in
 435     let gimps = subst (zip gs rs) icon in
 436     let prs = map2 (fun n (r,p) ->
 437       let tys,ty = nsplit dest_fun_ty (1--n) (type_of r) in
 438       let gvs = map genvar tys in
 439       list_mk_abs(gvs,mk_conj(list_mk_comb(r,gvs),list_mk_comb(p,gvs))))
 440      ns prrs in
 441     let modify_rule rcl itm =
 442       let avs,bod = strip_forall itm in
 443       if is_imp bod then
 444         let a,c = dest_imp bod in
 445         let mgoal = mk_imp(gimps,mk_imp(vsubst(zip gs ps) a,a)) in
 446         let mth = ASSUME(list_mk_forall(gs@ps@avs,mgoal)) in
 447         let ith_r = BETA_RULE(SPECL (prs @ rs @ avs) mth) in
 448         let jth_r = MP ith_r (prove_triv(lhand(concl ith_r))) in
 449         let t = lhand(concl jth_r) in
 450         let kth_r = UNDISCH jth_r in
 451         let ntm = list_mk_forall(avs,mk_imp(t,c)) in
 452         let lth_r = MP(SPECL avs rcl) kth_r
 453         and lth_p = UNDISCH(SPECL avs (ASSUME ntm)) in
 454         DISCH ntm (GENL avs (DISCH t (CONJ lth_r lth_p)))
 455       else
 456         DISCH itm (GENL avs (CONJ (SPECL avs rcl) (SPECL avs (ASSUME itm)))) in
 457     let mimps = map2 modify_rule (CONJUNCTS sth) (conjuncts iant) in
 458     let th1 = end_itlist (fun th th' -> MATCH_IMPS(CONJ th th')) mimps in
 459     let th2 = BETA_RULE(SPECL prs jth) in
 460     let th3 = IMP_TRANS th1 th2 in
 461     let nasm = lhand(concl th3) in
 462     let th4 = GENL ps (DISCH nasm (weaken_triv(UNDISCH th3))) in
 463     GENL svs (prove_monotonicity_hyps th4);;