1(* ===================================================================== *) 2(* FILE : Mutual.sml *) 3(* DESCRIPTION : Tools associated with datatypes defined by mutual *) 4(* recursion. We provide an induction tactic, adapted *) 5(* from the standard INDUCT_THEN operator, which was *) 6(* translated from the HOL 88 version. *) 7(* *) 8(* AUTHOR : (c) Tom Melham, University of Cambridge *) 9(* DATE : 87.08.23 *) 10(* REVISED : 90.06.02 *) 11(* TRANSLATOR : Konrad Slind, University of Calgary *) 12(* ADAPTOR : Peter Vincent Homeier, University of Pennsylvania *) 13(* DATE : March 27, 1998 *) 14(* ===================================================================== *) 15 16structure Mutual :> Mutual = 17struct 18 19open HolKernel Parse boolLib; 20 21val ERR = mk_HOL_ERR "Mutual"; 22 23val AND = conjunction; 24 25(* ---------------------------------------------------------------------*) 26(* Internal function: *) 27(* *) 28(* MOVEQS tys : returns a conversion that, when applied to a term with *) 29(* universal quantifications, moves the quantifications *) 30(* of variables of types in tys outward, and the others *) 31(* inward towards the body; otherwise, order is preserved. *) 32(* *) 33(* ---------------------------------------------------------------------*) 34 35fun MOVEQS tys tm = 36 if not (is_forall tm) then raise ERR "MOVEQS" "not a forall" 37 else 38 let val (Bvars,Body) = strip_forall tm 39(* 40 val _ = print_string "MOVEQS\n" 41 val _ = print_term tm 42 val _ = print_newline() 43*) 44 val (vars1,vars2) = partition (fn v => mem (type_of v) tys) Bvars 45 val tm1 = list_mk_forall (vars1 @ vars2, Body) 46 val eq_thm = 47 Tactical.prove (mk_eq(tm, tm1), 48 EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]) 49 in 50 itlist (fn v => 51 CONV_RULE (RAND_CONV (ONCE_DEPTH_CONV FORALL_IMP_CONV))) 52 vars2 eq_thm 53 end; 54 55(* Test case: 56val tys = [==`:num`==]; 57val tm = (--`!n b m a. b ==> (a /\ n+m < m)`--); 58MOVEQS tys tm; 59*) 60 61 62(* ---------------------------------------------------------------------*) 63(* Internal function: *) 64(* *) 65(* REPAIR th : returns an induction theorem by repairing th, using *) 66(* MOVEQS on the hypotheses of the antecedent. *) 67(* *) 68(* ---------------------------------------------------------------------*) 69 70fun REPAIR th = 71 let val (Bvars,Body) = strip_forall(concl th) 72 val (hy,cns) = dest_imp Body 73 val tys = map (type_of o fst o dest_forall) (strip_conj cns) 74 in 75 CONV_RULE (((itlist (fn v => RAND_CONV o ABS_CONV) Bvars) o 76 RATOR_CONV o RAND_CONV o 77 ONCE_DEPTH_CONV) (MOVEQS tys)) 78 (REWRITE_RULE[AND_IMP_INTRO,GSYM CONJ_ASSOC] th) 79 end; 80 81(* Test case: 82REPAIR avexp_induction handle e => (print_HOL_ERR e; raise e); 83*) 84 85 86(* ---------------------------------------------------------------------*) 87(* Internal function: *) 88(* *) 89(* BETAS "f" tm : returns a conversion that, when applied to a term with*) 90(* the same structure as the input term tm, will do a *) 91(* beta reduction at all top-level subterms of tm which *) 92(* are of the form "f <arg>", for some argument <arg>. *) 93(* *) 94(* ---------------------------------------------------------------------*) 95 96fun BETAS fnns body = 97 if ((is_var body) orelse (is_const body)) 98 then REFL 99 else if (is_abs body) 100 then ABS_CONV (BETAS fnns (snd(dest_abs body))) 101 else let val (Rator,Rand) = dest_comb body 102 in 103 if op_mem aconv Rator fnns then BETA_CONV 104 else let val cnv1 = BETAS fnns Rator 105 and cnv2 = BETAS fnns Rand 106 fun f (Rator,Rand) = (cnv1 Rator, cnv2 Rand) 107 in 108 (MK_COMB o (f o dest_comb)) 109 end 110 end; 111 112(* ---------------------------------------------------------------------*) 113(* Internal function: GTAC *) 114(* *) 115(* !x. tm[x] *) 116(* ------------ GTAC "y" (primes the "y" if necessary). *) 117(* tm[y] *) 118(* *) 119(* NB: the x is always a genvar, so optimized for this case. *) 120(* ---------------------------------------------------------------------*) 121 122fun GTAC y (A,g) = 123 let val (Bvar,Body) = dest_forall g 124 and y' = variant (free_varsl (g::A)) y 125 in 126 ([(A,subst[Bvar |-> y'] Body)], 127 fn [th] => GEN Bvar (INST [y' |-> Bvar] th) 128 | _ => raise Match) 129 end; 130 131(* ---------------------------------------------------------------------*) 132(* Internal function: TACF *) 133(* *) 134(* TACF is used to generate the subgoals for each case in an inductive *) 135(* proof. The argument tm is formula which states one generalized *) 136(* case in the induction. For example, the induction theorem for num is:*) 137(* *) 138(* |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n *) 139(* *) 140(* In this case, the argument tm will be one of: *) 141(* *) 142(* 1: "P 0" or 2: !n. P n ==> P(SUC n) *) 143(* *) 144(* TACF applied to each these terms to construct a parameterized tactic *) 145(* which will be used to further break these terms into subgoals. The *) 146(* resulting tactic takes a variable name x and a user supplied theorem *) 147(* continuation ttac. For a base case, like case 1 above, the resulting*) 148(* tactic just throws these parameters away and passes the goal on *) 149(* unchanged (i.e. \x ttac. ALL_TAC). For a step case, like case 2, the*) 150(* tactic applies GTAC x as many times as required. It then strips off *) 151(* the induction hypotheses and applies ttac to each one. For example, *) 152(* if tac is the tactic generated by: *) 153(* *) 154(* TACF "!n. P n ==> P(SUC n)" "x:num" ASSUME_TAC *) 155(* *) 156(* then applying tac to the goal A,"!n. P[n] ==> P[SUC n] has the same *) 157(* effect as applying: *) 158(* *) 159(* GTAC "x:num" THEN DISCH_THEN ASSUME_TAC *) 160(* *) 161(* TACF is a strictly local function, used only to define TACS, below. *) 162(* ---------------------------------------------------------------------*) 163local 164fun ctacs tm = 165 if (is_conj tm) 166 then let val tac2 = ctacs (snd(dest_conj tm)) 167 in fn ttac => CONJUNCTS_THEN2 ttac (tac2 ttac) 168 end 169 else fn ttac => ttac 170val find = Lib.first; 171fun findx bvars v = find (fn x => type_of x = type_of v) bvars 172in 173fun TACF tm = 174 let val (vs,body) = strip_forall tm 175 in 176 if is_imp body 177 then let val TTAC = ctacs (fst(dest_imp body)) 178 in 179 fn xs => fn ttac => 180(* 181 let val _ = print_string "TACF: xs = " 182 val _ = print_terms xs 183 val _ = print_newline() 184 val _ = print_string "vs = " 185 val _ = print_terms vs 186 val _ = print_newline() 187 val _ = print_string "map (findx xs) vs = " 188 val _ = print_terms (map (findx xs) vs) 189 val _ = print_newline() 190 in 191*) 192 MAP_EVERY (GTAC o (findx xs)) vs THEN 193 (* MAP_EVERY (GTAC o (Lib.K x)) vs THEN *) 194 DISCH_THEN (TTAC ttac) 195(* 196 end 197*) 198 end 199 else 200 fn xs => fn ttac => Tactical.ALL_TAC 201 end 202end; 203 204(* ---------------------------------------------------------------------*) 205(* Internal function: TACS *) 206(* *) 207(* TACS uses TACF to generate a parameterized list of tactics, one for *) 208(* each conjunct in the hypothesis of an induction theorem. *) 209(* *) 210(* For example, if tm is the hypothesis of the induction thoerem for the*) 211(* natural numbers---i.e. if: *) 212(* *) 213(* tm = "P 0 /\ (!n. P n ==> P(SUC n))" *) 214(* *) 215(* then TACS tm yields the paremterized list of tactics: *) 216(* *) 217(* \x ttac. [TACF "P 0" x ttac; TACF "!n. P n ==> P(SUC n)" x ttac] *) 218(* *) 219(* TACS is a strictly local function, used only in MUTUAL_INDUCT_THEN. *) 220(* ---------------------------------------------------------------------*) 221 222fun f (conj1,conj2) = (TACF conj1, TACS conj2) 223and 224 TACS tm = 225 let val (cf,csf) = f(dest_conj tm) 226 handle HOL_ERR _ => (TACF tm, Lib.K(Lib.K[])) 227 in 228 fn xs => fn ttac => (cf xs ttac)::(csf xs ttac) 229 end; 230 231(* ---------------------------------------------------------------------*) 232(* Internal function: GOALS *) 233(* *) 234(* GOALS generates the subgoals (and proof functions) for all the cases *) 235(* in an induction. The argument A is the common assumption list for all*) 236(* the goals, and tacs is a list of tactics used to generate subgoals *) 237(* from these goals. *) 238(* *) 239(* GOALS is a strictly local function, used only in MUTUAL_INDUCT_THEN. *) 240(* ---------------------------------------------------------------------*) 241fun GOALS A [] tm = raise ERR "GOALS" "empty lsit" 242 | GOALS A [t] tm = 243 let val (sg,pf) = t (A,tm) in ([sg],[pf]) end 244 | GOALS A (h::t) tm = 245 let val (conj1,conj2) = dest_conj tm 246 val (sgs,pfs) = GOALS A t conj2 247 val (sg,pf) = h (A,conj1) 248 in 249 ((sg::sgs),(pf::pfs)) 250 end; 251 252(* --------------------------------------------------------------------- *) 253(* Internal function: GALPH *) 254(* *) 255(* GALPH "!x1 ... xn. A ==> B": alpha-converts the x's to genvars. *) 256(* --------------------------------------------------------------------- *) 257local 258fun rule v = 259 let val gv = genvar(type_of v) 260 in 261 fn eq => let val th = FORALL_EQ v eq 262 in TRANS th (GEN_ALPHA_CONV gv (rhs(concl th))) 263 end 264 end 265in 266fun GALPH tm = 267 let val (vs,hy) = strip_forall tm 268 in if (is_imp hy) then Lib.itlist rule vs (REFL hy) else REFL tm 269 end 270end; 271 272(* --------------------------------------------------------------------- *) 273(* Internal function: GALPHA *) 274(* *) 275(* Applies the conversion GALPH to each conjunct in a sequence. *) 276(* --------------------------------------------------------------------- *) 277 278 279fun f (conj1,conj2) = (GALPH conj1, GALPHA conj2) 280and GALPHA tm = 281 let val (c,cs) = f(dest_conj tm) 282 in 283 MK_COMB(AP_TERM AND c, cs) 284 end 285 handle HOL_ERR _ => GALPH tm; 286 287 288(* --------------------------------------------------------------------- *) 289(* MUTUAL_INDUCT_THEN : general induction tactic for mutuallly recursive *) 290(* datatypes. *) 291(* --------------------------------------------------------------------- *) 292local val bool = genvar (Type.bool) 293 294fun MUTUAL_INDUCT_THEN1 th = 295 let val th' = REPAIR th 296(* 297 val _ = print_string "Repaired induction theorem:\n" 298 val _ = print_theorem th' 299 val _ = print_string "\n" 300*) 301 val (Bvars,Body) = strip_forall(concl th') 302 val (hy,_) = dest_imp Body 303 val bconv = BETAS Bvars hy 304 and tacsf = TACS hy 305 val vs = map (fn Bvar => genvar (type_of Bvar)) Bvars 306 val eta_th = LIST_CONJ (map (CONV_RULE(RAND_CONV ETA_CONV)) 307 (CONJUNCTS(UNDISCH(SPECL vs th')))) 308(* 309 val _ = print_string "eta_th:\n" 310 val _ = print_theorem eta_th 311 val _ = print_string "\n" 312*) 313 val (asm,con) = case dest_thm eta_th 314 of ([asm],con) => (asm,con) 315 | _ => raise ERR "MUTUAL_INDUCT_THEN1" "" 316 val dis = DISCH asm eta_th 317 val ind = GENL vs (SUBST [bool |-> GALPHA asm] (mk_imp(bool, con)) dis) 318(* 319 val _ = print_string "ind:\n" 320 val _ = print_theorem ind 321 val _ = print_string "\n" 322*) 323 val find = Lib.first; 324 fun findt ts v = 325 find (fn x => type_of (snd(dest_comb x)) = type_of v) ts 326 handle _ => let val ty = type_of v 327 val ty' = hd(snd(dest_type ty)) 328 val (Tyop',Args') = dest_type ty' 329 val nm = implode [hd (explode Tyop')] 330 val v' = mk_var(nm, ty') 331 in 332 mk_forall(v', T) 333 end 334 val CHECK_TAC :tactic = fn (asl,gl) => ACCEPT_TAC (ASSUME gl) (asl,gl) 335 336 in 337 fn ttac => fn (A,t) => (* t is the current goal *) 338 let val ts = strip_conj t 339 val lams = map (snd o dest_comb) ts 340 val ts' = map (findt ts) vs 341 val ts_thm = Tactical.prove 342 (mk_eq(list_mk_conj ts',list_mk_conj ts), 343 REWRITE_TAC[] THEN 344 EQ_TAC THEN STRIP_TAC THEN 345 REPEAT CONJ_TAC THEN 346 CHECK_TAC) 347(* 348 val _ = print_string "ts_thm:\n" 349 val _ = print_theorem ts_thm 350 val _ = print_string "\n" 351*) 352 val lams' = map (snd o dest_comb) ts' 353 val spec = SPECL lams' (itlist2 (fn v => fn lam => 354 INST_TYPE (Lib.snd(Term.match_term v lam)) 355 handle HOL_ERR _ => Lib.I 356 ) vs lams' ind) 357(* 358 val _ = print_string "spec:\n" 359 val _ = print_theorem spec 360 val _ = print_string "\n" 361*) 362 val (ant,conseq) = dest_imp(concl spec) 363 val beta = SUBST [bool |-> bconv ant] (mk_imp(bool,conseq)) spec 364(* 365 val _ = print_string "beta:\n" 366 val _ = print_theorem beta 367 val _ = print_string "\n" 368*) 369 val bvars = map (fst o dest_abs) lams' 370 val tacs = tacsf bvars ttac 371 val (gll,pl) = GOALS A tacs (fst(dest_imp(concl beta))) 372 val pf = ((EQ_MP ts_thm) o (MP beta) o LIST_CONJ) 373 o mapshape(map length gll)pl 374 in 375 (Lib.flatten gll, pf) 376 end 377 handle HOL_ERR _ 378 => raise ERR "MUTUAL_INDUCT_THEN" "tactic application error" 379 end 380 handle (e as HOL_ERR 381 {origin_structure = "Mutual", 382 origin_function = "MUTUAL_INDUCT_THEN",...}) => raise e 383 | _ => raise ERR "MUTUAL_INDUCT_THEN" "ill-formed induction theorem" 384 385in 386 387fun MUTUAL_INDUCT_THEN th ttac = 388 MUTUAL_INDUCT_THEN1 th ttac 389 THEN REWRITE_TAC[] 390 THEN TRY (UNDISCH_TAC (concl TRUTH) THEN DISCH_THEN (fn th => ALL_TAC)) 391 392end; 393 394 395fun MUTUAL_INDUCT_TAC ind = MUTUAL_INDUCT_THEN ind ASSUME_TAC; 396 397end (* Mutual *) 398