1(* ===================================================================== *) 2(* FILE : numLib.sml (Formerly num_lib.sml, num.sml) *) 3(* DESCRIPTION : Proof support for :num. Translated from hol88. *) 4(* *) 5(* AUTHORS : (c) Mike Gordon and *) 6(* Tom Melham, University of Cambridge *) 7(* DATE : 88.04.04 *) 8(* TRANSLATOR : Konrad Slind, University of Calgary *) 9(* UPDATE : October'94 bugfix to num_EQ_CONV (KLS;bugfix from tfm)*) 10(* UPDATE : January'99 fix to use "Norrish" numerals (MN) *) 11(* UPDATE : August'99 to incorporate num_CONV and INDUCT_TAC *) 12(* UPDATE : Nov'99 to incorporate main entrypoints from *) 13(* reduceLib and arithLib. Also, ADD_CONV and *) 14(* num_EQ_CONV are banished: use the stuff in reduceLib *) 15(* instead. *) 16(* ===================================================================== *) 17 18 19structure numLib :> numLib = 20struct 21 22local open numeralTheory in end; 23 24open HolKernel boolLib Num_conv Parse numSyntax; 25 26val ERR = mk_HOL_ERR "numLib"; 27 28(* Fix the grammar used by this file *) 29val ambient_grammars = Parse.current_grammars(); 30val _ = Parse.temp_set_grammars arithmeticTheory.arithmetic_grammars 31 32val N = numSyntax.num; 33 34(* --------------------------------------------------------------------- *) 35(* EXISTS_LEAST_CONV: applies the well-ordering property to non-empty *) 36(* sets of numbers specified by predicates. *) 37(* *) 38(* A call to EXISTS_LEAST_CONV `?n:num. P[n]` returns: *) 39(* *) 40(* |- (?n. P[n]) = ?n. P[n] /\ !n'. (n' < n) ==> ~P[n'] *) 41(* *) 42(* --------------------------------------------------------------------- *) 43 44local val wop = arithmeticTheory.WOP 45 val wth = CONV_RULE (ONCE_DEPTH_CONV ETA_CONV) wop 46 val check = assert (fn tm => type_of tm = N) 47 val acnv = RAND_CONV o ABS_CONV 48in 49fun EXISTS_LEAST_CONV tm = 50 let val (Bvar,P) = dest_exists tm 51 val n = check Bvar 52 val thm1 = UNDISCH (SPEC (rand tm) wth) 53 val thm2 = CONV_RULE (GEN_ALPHA_CONV n) thm1 54 val (c1,c2) = dest_comb (snd(dest_exists(concl thm2))) 55 val bth1 = RAND_CONV BETA_CONV c1 56 val bth2 = acnv (RAND_CONV (RAND_CONV BETA_CONV)) c2 57 val n' = variant (n :: free_vars tm) n 58 val abth2 = CONV_RULE (RAND_CONV (GEN_ALPHA_CONV n')) bth2 59 val thm3 = EXISTS_EQ n (MK_COMB(bth1,abth2)) 60 val imp1 = DISCH tm (EQ_MP thm3 thm2) 61 val eltm = rand(concl thm3) 62 val thm4 = CONJUNCT1 (ASSUME (snd(dest_exists eltm))) 63 val thm5 = CHOOSE (n,ASSUME eltm) (EXISTS (tm,n) thm4) 64 in 65 IMP_ANTISYM_RULE imp1 (DISCH eltm thm5) 66 end 67 handle HOL_ERR _ => raise ERR "EXISTS_LEAST_CONV" "" 68end; 69 70(*---------------------------------------------------------------------------*) 71(* EXISTS_GREATEST_CONV - Proves existence of greatest element satisfying P. *) 72(* *) 73(* EXISTS_GREATEST_CONV `(?x. P[x]) /\ (?y. !z. z > y ==> ~(P[z]))` = *) 74(* |- (?x. P[x]) /\ (?y. !z. z > y ==> ~(P[z])) = *) 75(* ?x. P[x] /\ !z. z > x ==> ~(P[z]) *) 76(* *) 77(* If the variables x and z are the same, the `z` instance will be primed. *) 78(* [JRH 91.07.17] *) 79(*---------------------------------------------------------------------------*) 80 81local val EXISTS_GREATEST = arithmeticTheory.EXISTS_GREATEST 82 val t = RATOR_CONV 83 and n = RAND_CONV 84 and b = ABS_CONV 85 val red1 = t o n o t o n o n o b 86 and red2 = t o n o n o n o b o n o b o n o n 87 and red3 = n o n o b o t o n 88 and red4 = n o n o b o n o n o b o n o n 89in 90fun EXISTS_GREATEST_CONV tm = 91 let val (lc,rc) = dest_conj tm 92 val pred = rand lc 93 val (xv,xb) = dest_exists lc 94 val (yv,yb) = dest_exists rc 95 val zv = fst (dest_forall yb) 96 val prealpha = CONV_RULE 97 (red1 BETA_CONV THENC red2 BETA_CONV THENC 98 red3 BETA_CONV THENC red4 BETA_CONV) (SPEC pred EXISTS_GREATEST) 99 val rqd = mk_eq (tm, mk_exists(xv,mk_conj(xb,subst[yv |-> xv] yb))) 100 in 101 Lib.S (Lib.C EQ_MP) (Lib.C ALPHA rqd o concl) prealpha 102 end 103 handle HOL_ERR _ => raise ERR "EXISTS_GREATEST_CONV" "" 104end; 105 106 107local fun SEC_ERR m = ERR "SUC_ELIM_CONV" m 108 fun assert f x = f x orelse raise SEC_ERR "assertion failed" 109in 110fun SUC_ELIM_CONV tm = 111 let val (v,bod) = dest_forall tm 112 val _ = assert (fn x => type_of x = N) v 113 val (sn,n) = (genvar N, genvar N) 114 val suck_suc = subst [numSyntax.mk_suc v |-> sn] bod 115 val suck_n = subst [v |-> n] suck_suc 116 val _ = assert (fn x => not (aconv x tm)) suck_n 117 val th1 = ISPEC (list_mk_abs ([sn,n],suck_n)) 118 arithmeticTheory.SUC_ELIM_THM 119 val BETA2_CONV = (RATOR_CONV BETA_CONV) THENC BETA_CONV 120 val th2 = CONV_RULE (LHS_CONV (QUANT_CONV BETA2_CONV)) th1 121 val th3 = CONV_RULE (RHS_CONV (QUANT_CONV 122 (FORK_CONV (ALL_CONV, BETA2_CONV)))) th2 123 in th3 124 end 125end; 126 127val num_CONV = Num_conv.num_CONV; 128 129(*--------------------------------------------------------------------------- 130 Forward rule for induction 131 ---------------------------------------------------------------------------*) 132 133local val v1 = genvar Type.bool 134 and v2 = genvar Type.bool 135in 136fun INDUCT (base,step) = 137 let val (Bvar,Body) = dest_forall(concl step) 138 val (ant,_) = dest_imp Body 139 val P = mk_abs(Bvar, ant) 140 val P0 = mk_comb(P, zero_tm) 141 val Pv = mk_comb(P,Bvar) 142 val PSUC = mk_comb(P, mk_suc Bvar) 143 val base' = EQ_MP (SYM(BETA_CONV P0)) base 144 and step' = SPEC Bvar step 145 and hypth = SYM(RIGHT_BETA(REFL Pv)) 146 and concth = SYM(RIGHT_BETA(REFL PSUC)) 147 and IND = SPEC P numTheory.INDUCTION 148 val template = mk_eq(concl step', mk_imp(v1, v2)) 149 val th1 = SUBST[v1 |-> hypth, v2|->concth] template (REFL (concl step')) 150 val th2 = GEN Bvar (EQ_MP th1 step') 151 val th3 = SPEC Bvar (MP IND (CONJ base' th2)) 152 in 153 GEN Bvar (EQ_MP (BETA_CONV(concl th3)) th3) 154 end 155 handle HOL_ERR _ => raise ERR "INDUCT" "" 156end; 157 158(* --------------------------------------------------------------------- *) 159(* [A] !n.t[n] *) 160(* ================================ *) 161(* [A] t[0] , [A,t[n]] t[SUC x] *) 162(* --------------------------------------------------------------------- *) 163 164fun INDUCT_TAC g = 165 INDUCT_THEN numTheory.INDUCTION ASSUME_TAC g 166 handle HOL_ERR _ => raise ERR "INDUCT_TAC" ""; 167 168 169fun completeInduct_on qtm g = 170 let open BasicProvers 171 val st = find_subterm qtm g 172 val ind_tac = Prim_rec.INDUCT_THEN 173 arithmeticTheory.COMPLETE_INDUCTION ASSUME_TAC 174 in 175 primInduct st ind_tac g 176 end 177 handle e => raise wrap_exn "numLib" "completeInduct_on" e 178 179 180(*--------------------------------------------------------------------------- 181 Invoked e.g. measureInduct_on `LENGTH L` or 182 measureInduct_on `(\(x,w). x+w) (M,N)` 183 ---------------------------------------------------------------------------*) 184 185local open relationTheory prim_recTheory 186 val mvar = mk_var("m", alpha --> numSyntax.num) 187 val measure_tm = prim_mk_const{Name="measure",Thy="prim_rec"} 188 val measure_m = mk_comb(measure_tm,mvar) 189 val ind_thm0 = GEN mvar 190 (BETA_RULE 191 (REWRITE_RULE[WF_measure,measure_def,inv_image_def] 192 (MATCH_MP (SPEC measure_m WF_INDUCTION_THM) 193 (SPEC_ALL WF_measure)))) 194in 195fun measureInduct_on q (g as (asl,w)) = 196 let val FVs = free_varsl (w::asl) 197 val tm = parse_in_context FVs q 198 val (meas, arg) = dest_comb tm 199 val (d,r) = dom_rng (type_of meas) (* r should be num *) 200 val st = BasicProvers.prim_find_subterm FVs arg g 201 val st_type = type_of (BasicProvers.dest_tmkind st) 202 val meas' = inst (match_type d st_type) meas 203 val ind_thm1 = INST_TYPE [Type.alpha |-> st_type] ind_thm0 204 val ind_thm2 = pairLib.GEN_BETA_RULE (SPEC meas' ind_thm1) 205 val ind_tac = Prim_rec.INDUCT_THEN ind_thm2 ASSUME_TAC 206 in 207 BasicProvers.primInduct st ind_tac g 208 end 209 handle e => raise wrap_exn "numLib" "measureInduct_on" e 210end 211 212val REDUCE_CONV = reduceLib.REDUCE_CONV 213val REDUCE_RULE = reduceLib.REDUCE_RULE 214val REDUCE_TAC = reduceLib.REDUCE_TAC 215 216val ARITH_CONV = Arith.ARITH_CONV 217val ARITH_PROVE = Drule.EQT_ELIM o ARITH_CONV 218val ARITH_TAC = CONV_TAC ARITH_CONV; 219 220 221(*---------------------------------------------------------------------------*) 222(* If "c" is a number constant, *) 223(* *) 224(* BOUNDED_FORALL_CONV cnv ``!n. n < c ==> P n`` *) 225(* *) 226(* generates "P (c-1) /\ !n. n < (c-1) ==> P n" and applies cnv to the first *) 227(* conjunct "P (c-1)". With NTAC or REPEATC, this can be used to prove *) 228(* bounded quantifications. *) 229(*---------------------------------------------------------------------------*) 230 231fun BOUNDED_FORALL_CONV cnv M = 232 let open reduceLib arithmeticTheory 233 val c = snd(dest_less(fst(dest_imp(snd(dest_forall M))))) 234 val thm = MP (SPEC c BOUNDED_FORALL_THM) 235 (EQT_ELIM(REDUCE_CONV (mk_less(zero_tm,c)))) 236 in 237 (HO_REWR_CONV thm THENC LAND_CONV cnv THENC REDUCE_CONV) M 238 end 239 handle e => raise wrap_exn "numLib" "BOUNDED_FORALL_CONV" e; 240 241 242(*---------------------------------------------------------------------------*) 243(* If "c" is a number constant, *) 244(* *) 245(* BOUNDED_EXISTS_CONV cnv `?n. n < c /\ P n` *) 246(* *) 247(* generates "P (c-1) \/ ?n. n < (c-1) /\ P n" and applies cnv to the first *) 248(* conjunct "P (c-1)". With NTAC or REPEATC, this can be used to prove *) 249(* bounded quantifications. *) 250(*---------------------------------------------------------------------------*) 251 252fun BOUNDED_EXISTS_CONV cnv M = 253 let open reduceLib arithmeticTheory 254 val c = snd(dest_less(fst(dest_conj(snd(dest_exists M))))) 255 val thm = MP (SPEC c BOUNDED_EXISTS_THM) 256 (EQT_ELIM(REDUCE_CONV (mk_less(zero_tm,c)))) 257 in 258 (HO_REWR_CONV thm THENC LAND_CONV cnv THENC REDUCE_CONV) M 259 end 260 handle e => raise wrap_exn "numLib" "BOUNDED_EXISTS_CONV" e; 261 262(* ---------------------------------------------------------------------- 263 LEAST_ELIM_TAC : tactic 264 265 Turns 266 267 A ?- Q ($LEAST P) 268 269 (where P is free) into 270 271 A ?- (?n. P n) /\ (!n. (!m. m < n ==> ~P m) /\ P n ==> Q n) 272 273 Picks an arbitrary LEAST-subterm if there are multiple such. 274 ---------------------------------------------------------------------- *) 275 276val LEAST_ELIM_TAC = DEEP_INTRO_TAC whileTheory.LEAST_ELIM 277 278(*--------------------------------------------------------------------------- 279 Simplification set for numbers (and booleans). 280 ---------------------------------------------------------------------------*) 281 282local open simpLib infix ++ 283in 284val std_ss = 285 (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++ 286 numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ combinSimps.COMBIN_ss ++ 287 numSimps.ARITH_RWTS_ss) 288 289val arith_ss = std_ss ++ numSimps.ARITH_DP_ss 290end; 291 292(*---------------------------------------------------------------------------*) 293(* Arith. decision proc packaged up. *) 294(*---------------------------------------------------------------------------*) 295 296fun DECIDE tm = 297 ARITH_PROVE tm handle HOL_ERR _ => tautLib.TAUT_PROVE tm 298 handle HOL_ERR _ => raise ERR "DECIDE" ""; 299 300 301fun DECIDE_TAC (g as (asl,_)) = 302((MAP_EVERY UNDISCH_TAC (filter numSimps.is_arith_asm asl) 303 THEN ARITH_TAC) 304 ORELSE tautLib.TAUT_TAC ORELSE NO_TAC) g; 305 306(*---------------------------------------------------------------------------*) 307(* Moving SUC out of patterns on lhs *) 308(*---------------------------------------------------------------------------*) 309 310val SUC_TO_NUMERAL_DEFN_CONV = let 311 fun UBLIST [] = ALL_CONV 312 | UBLIST (h::t) = UNBETA_CONV h THENC RATOR_CONV (UBLIST t) 313 fun basic_elim t = let 314 (* t of form !n. ..SUC n.. = .. n .. SUC n .. *) 315 val (v, body) = dest_forall t 316 val sv = numSyntax.mk_suc v 317 in 318 BINDER_CONV (LAND_CONV (UNBETA_CONV sv) THENC 319 RAND_CONV (UBLIST [sv, v])) THENC 320 REWR_CONV arithmeticTheory.SUC_ELIM_NUMERALS THENC 321 BINOP_CONV (BINDER_CONV (BINOP_CONV LIST_BETA_CONV) THENC 322 RAND_CONV (ALPHA_CONV v)) 323 end t 324 325 fun push_down t = 326 if is_forall (#2 (dest_forall t)) then 327 (SWAP_VARS_CONV THENC BINDER_CONV push_down) t 328 else ALL_CONV t 329 fun push_nth_down n t = 330 if n > 0 then BINDER_CONV (push_nth_down (n - 1)) t 331 else push_down t 332 fun pull_up t = 333 if is_forall (#2 (dest_forall t)) then 334 (BINDER_CONV pull_up THENC SWAP_VARS_CONV) t 335 else ALL_CONV t 336 fun pull_upto_nth n t = 337 if n > 0 then BINDER_CONV (pull_upto_nth (n - 1)) t 338 else pull_up t 339 fun push_over_conjs t = 340 if is_forall t then 341 (BINDER_CONV push_over_conjs THENC FORALL_AND_CONV) t 342 else ALL_CONV t 343 344 fun unsuc_conjn c = let 345 val (vs, body) = strip_forall c 346 val (l, r) = dest_eq body 347 val suc_terms = find_terms numSyntax.is_suc l 348 fun elim_one_suc st t = let 349 val v = numSyntax.dest_suc st 350 in 351 if is_var v then 352 case Lib.total (index (aconv v)) vs of 353 NONE => ALL_CONV t 354 | SOME i => (push_nth_down i THENC 355 LAST_FORALL_CONV basic_elim THENC 356 push_over_conjs THENC 357 BINOP_CONV (pull_upto_nth i)) t 358 else 359 ALL_CONV t 360 end 361 in 362 EVERY_CONV (map (EVERY_CONJ_CONV o elim_one_suc) suc_terms) c 363 end 364 fun reassociate_toplevel_conjns t = 365 if is_conj t then 366 ((REWR_CONV (GSYM CONJ_ASSOC) THENC 367 reassociate_toplevel_conjns) ORELSEC 368 RAND_CONV reassociate_toplevel_conjns) t 369 else ALL_CONV t 370in 371 EVERY_CONJ_CONV unsuc_conjn THENC reassociate_toplevel_conjns 372end 373 374val _ = Defn.SUC_TO_NUMERAL_DEFN_CONV_hook := SUC_TO_NUMERAL_DEFN_CONV; 375 376val SUC_RULE = Conv.CONV_RULE SUC_TO_NUMERAL_DEFN_CONV; 377 378(* ---------------------------------------------------------------------- 379 Parsing adjustments 380 ---------------------------------------------------------------------- *) 381 382val magic_injn = prim_mk_const {Thy = "arithmetic", 383 Name = GrammarSpecials.nat_elim_term}; 384val operators = [("+", ``$+``), 385 ("-", ``$-``), 386 ("*", ``$*``), 387 ("<", ``$<``), 388 ("<=", ``$<=``), 389 (">", ``$>``), 390 (">=", ``$>=``), 391 (GrammarSpecials.fromNum_str, magic_injn)]; 392 393fun deprecate_num () = let 394 fun losety {Name,Thy,Ty} = {Name = Name, Thy = Thy} 395 fun doit (s, t) = Parse.temp_remove_ovl_mapping s (losety (dest_thy_const t)) 396in 397 app (ignore o doit) operators 398end 399 400fun prefer_num () = app temp_overload_on operators 401 402val _ = Parse.temp_set_grammars ambient_grammars; 403 404end (* numLib *) 405