1structure schneiderUtils :> schneiderUtils = 2struct 3 4open HolKernel Parse boolLib; 5 6structure Parse = 7struct 8 open Parse 9 val (Type,Term) = parse_from_grammars bool_grammars 10end 11 12(* ************************************************************ *) 13(* PROP_TAC : A tautology checker with prop. abstraction *) 14(* REW_PROP_TAC: Same as PROP_TAC, but rewrites first with asm. *) 15(* UNDISCH_HD_TAC: UNDISCH with the head of the assumptions *) 16(* UNDISCH_NO_TAC i: UNDISCH the ith assumption *) 17(* POP_NO_ASSUM i : Takes the ith assumption for a thm_tactic *) 18(* POP_NO_TAC i: Eliminates the ith Assumption *) 19(* ASM_TAC i: Same as POP_NO_ASSUM, but retains the assumption *) 20(* ASM_LIST_TAC il : Uses a sublist of the assumptions *) 21(* APPLY_ASM_TAC i tac: Applies tac on the ith assumption *) 22(* ************************************************************ *) 23 24 25fun elem 0 l = hd l | elem i l = elem (i-1) (tl l) 26fun delete i l = if i=0 then tl l 27 else (hd l)::(delete (i-1) (tl l)) 28 29val PROP_TAC = tautLib.TAUT_TAC; 30val REW_PROP_TAC = PURE_ASM_REWRITE_TAC[] THEN PROP_TAC 31fun UNDISCH_HD_TAC (asm,g) = (UNDISCH_TAC (hd asm))(asm,g) 32fun UNDISCH_ALL_TAC (asm,g) = (MAP_EVERY UNDISCH_TAC asm)(asm,g) 33fun UNDISCH_NO_TAC i (asm,g) = (UNDISCH_TAC (elem i asm))(asm,g) 34fun POP_NO_ASSUM i thfun (asl,w) = thfun (ASSUME (elem i asl)) ((delete i asl),w) 35fun POP_NO_TAC i = POP_NO_ASSUM i (fn x=> ALL_TAC) 36fun ASM_TAC i tac (asm,g) = (tac (ASSUME(elem i asm))) (asm,g) 37fun ASM_LIST_TAC il tac (asm,g) = (tac (map ASSUME(map (fn i=>elem i asm)il))) (asm,g) 38 39fun APPLY_ASM_TAC i tac = 40 (UNDISCH_NO_TAC i) THEN CONV_TAC CONTRAPOS_CONV 41 THEN DISCH_TAC THEN tac THEN UNDISCH_HD_TAC 42 THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] 43 THEN DISCH_TAC 44 45 46fun prove_thm (name,t,tac) = save_thm(name,TAC_PROOF( ([],t),tac)) 47fun REWRITE1_TAC t = REWRITE_TAC[t] 48 49 50(* ********************** COPY_ASM_NO i *********************** *) 51(* *) 52(* [a0,...,an] |- g *) 53(* ========================================== *) 54(* [ai,a0,...,ai-1,ai+1,...,an] |- ai ==> g *) 55(* ************************************************************ *) 56 57fun COPY_ASM_NO i (asm,g) = 58 let val lemma =TAC_PROOF( 59 ([],���!a b. (a==>b) = (a==>a==>b)���), 60 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 61 THEN REWRITE_TAC[]) 62 val a = elem i asm 63 in 64 (UNDISCH_NO_TAC i THEN SUBST1_TAC(SPECL[a,g]lemma) 65 THEN DISCH_TAC)(asm,g) 66 end 67 68 69 70 71(* ************************************************************ *) 72(* ************************************************************ *) 73fun FORALL_UNFREE_CONV t = 74 let val (x,f) = dest_forall t 75 val lemma = TAC_PROOF(([],���!P.(!x:'a.P) = P���), 76 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]) 77 val lemma' = INST_TYPE[alpha |-> type_of x] lemma 78 in 79 BETA_RULE(SPEC f lemma') 80 end 81 82 83fun FORALL_IN_CONV t = 84 if is_forall t then 85 let val (x,f) = dest_forall t 86 in if mem x (free_vars f) then 87 ((FORALL_AND_CONV t) handle HOL_ERR _=> REFL t) 88 else FORALL_UNFREE_CONV t 89 end else 90 if is_abs t then (ABS_CONV FORALL_IN_CONV) t else 91 if is_comb t then ((RAND_CONV FORALL_IN_CONV) THENC 92 (RATOR_CONV FORALL_IN_CONV)) t 93 else REFL t 94 95 96 97 98 99(* ********* LEFT_EXISTS_TAC & LEFT_FORALL_TAC **************** *) 100(* *) 101(* ?x.P[x],G|-phi !x.P[x],G|-phi *) 102(* ================ ================ t *) 103(* P[x'],G|-phi P[t],G|-phi *) 104(* ************************************************************ *) 105 106val LEFT_EXISTS_TAC = 107 UNDISCH_HD_TAC THEN CONV_TAC LEFT_IMP_EXISTS_CONV 108 THEN GEN_TAC THEN DISCH_TAC 109 110fun LEFT_FORALL_TAC t = 111 UNDISCH_HD_TAC THEN CONV_TAC LEFT_IMP_FORALL_CONV 112 THEN EXISTS_TAC t THEN DISCH_TAC 113 114 115 116(* ******* LEFT_NO_EXISTS_TAC & LEFT_NO_FORALL_TAC ************ *) 117(* These tactics do exactly the same as the tactics above, but *) 118(* the quantified formulae need not be the topmost assumption *) 119(* and are therefore specified by their number. Note that the *) 120(* topmost assumption has number 0, then comes 1,... *) 121(* ************************************************************ *) 122 123fun LEFT_NO_EXISTS_TAC i = 124 (UNDISCH_NO_TAC i) THEN CONV_TAC LEFT_IMP_EXISTS_CONV 125 THEN GEN_TAC THEN DISCH_TAC 126 127fun LEFT_NO_FORALL_TAC i t = 128 (UNDISCH_NO_TAC i) THEN CONV_TAC LEFT_IMP_FORALL_CONV 129 THEN EXISTS_TAC t THEN DISCH_TAC 130 131 132 133(* ********* LEFT_DISJ_TAC & RIGHT_DISJ_TAC ******************* *) 134(* *) 135(* G |- a\/b G |- a\/b *) 136(* =========== =========== *) 137(* G,~b |- a G,~a |- b *) 138(* ************************************************************ *) 139 140fun LEFT_DISJ_TAC (asm,g) = 141 let val lem = TAC_PROOF(([],���!a b. a\/b = ~b==>a���), 142 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 143 THEN REWRITE_TAC[]) 144 val (a,b) = dest_disj g 145 in (SUBST1_TAC(SPECL[a,b]lem) THEN DISCH_TAC) (asm,g) 146 end 147 148fun RIGHT_DISJ_TAC (asm,g) = 149 let val lem = TAC_PROOF(([],���!a b. a\/b = ~a==>b���), 150 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 151 THEN REWRITE_TAC[]) 152 val (a,b) = dest_disj g 153 in (SUBST1_TAC(SPECL[a,b]lem) THEN DISCH_TAC) (asm,g) 154 end 155 156 157(* ********* LEFT_CONJ_TAC & RIGHT_CONJ_TAC ******************* *) 158(* *) 159(* G |- a/\b G |- a/\b *) 160(* ================== ================= *) 161(* G |- a | G,a|- b G |- b | G,b|- a *) 162(* ************************************************************ *) 163 164val LEFT_CONJ_TAC = CONJ_ASM1_TAC 165val RIGHT_CONJ_TAC = CONJ_ASM2_TAC 166 167(* ********** LEFT_LEMMA_DISJ_CASES_TAC *********************** *) 168(* Given a theorem G|-a\/b, these tactics behave as follows: *) 169(* *) 170(* A|-phi A|-phi *) 171(* ============================ ============================ *) 172(* A,G,a|-phi A,G,~a,b|-phi A,G,a,~b|-phi A,G,b|-phi *) 173(* *) 174(* ************************************************************ *) 175 176fun LEFT_LEMMA_DISJ_CASES_TAC th = 177 let val (a,b) = dest_disj (concl th) 178 val absorb_lem = TAC_PROOF(([],���!a b. a\/b = a \/(~a/\b)���), 179 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 180 THEN REWRITE_TAC[]) 181 in DISJ_CASES_TAC (EQ_MP (SPECL[a,b]absorb_lem) th) THEN UNDISCH_HD_TAC 182 THEN STRIP_TAC 183 end 184 185 186fun RIGHT_LEMMA_DISJ_CASES_TAC th = 187 let val (a,b) = dest_disj (concl th) 188 val absorb_lem = TAC_PROOF(([],���!a b. a\/b = (a/\~b) \/ b���), 189 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���b:bool���) 190 THEN REWRITE_TAC[]) 191 in DISJ_CASES_TAC (EQ_MP (SPECL[a,b]absorb_lem) th) THEN UNDISCH_HD_TAC 192 THEN STRIP_TAC 193 end 194 195 196 197 198(* *********************** MP2_TAC **************************** *) 199(* A ?- t *) 200(* ============== MP2_TAC (A' |- s ==> t) *) 201(* A ?- s *) 202(* *) 203(* ************************************************************ *) 204 205fun MP2_TAC th ((asm,g):goal) = 206 let val (s,t) = dest_imp(concl th) 207 in ([(asm,s)],fn [t]=> MP th t | _ => raise Match) 208 end 209 210 211 212 213(* ********************* MY_MP_TAC **************************** *) 214(* A ?- t *) 215(* ======================= MP2_TAC s *) 216(* A ?- s | A ?- s ==> t *) 217(* *) 218(* ************************************************************ *) 219 220fun MY_MP_TAC t (asm,g) = 221 let val lemma = TAC_PROOF( 222 ([],���!b.(?a.a /\ (a==>b)) ==> b���), 223 GEN_TAC THEN STRIP_TAC THEN RES_TAC) 224 in 225 (MATCH_MP_TAC (SPEC g lemma) 226 THEN EXISTS_TAC t THEN CONJ_TAC) (asm,g) 227 end; 228 229 230(* ****************** TAC_CONV ******************************** *) 231(* TAC_CONV: takes a tactic and generates a conversion of it *) 232(* Caution: does not work properly so far *) 233(* ************************************************************ *) 234 235fun TAC_CONV (tac:tactic) t = 236 let val goal = ([],t) 237 val subgoals = fst (tac goal) 238 val terms = map (fn (asm,g) =>if null asm then g 239 else mk_imp(list_mk_conj asm, g)) subgoals 240 val term = list_mk_conj terms 241 val eq = mk_eq(t,term) 242 in 243 TAC_PROOF(([],eq),tac THEN REWRITE_TAC[]) 244 end 245 246 247 248 249 250(* ************************************************************ *) 251 252(* ************************************************************ *) 253 254(* 255val num_Axiom1 = TAC_PROOF( 256 ([],���!e:'a.!f. ?fn1. (fn1 t0 = e) /\ 257 (!t. fn1(SUC(t+t0)) = f (fn1 (t+t0)) (t))���), 258 let val lemma = EXISTENCE(SPEC_ALL num_Axiom) 259 in 260 REPEAT GEN_TAC THEN ASSUME_TAC lemma THEN LEFT_EXISTS_TAC 261 THEN EXISTS_TAC (���\t.fn1(t-t0):'a���) THEN BETA_TAC 262 THEN ASM_REWRITE_TAC[SUB_EQUAL_0] THEN GEN_TAC 263 THEN REWRITE_TAC[SYM(SPEC_ALL(CONJUNCT2 ADD)),ADD_SUB] 264 THEN ASM_REWRITE_TAC[] 265 end) 266 267 268val num_Axiom2 = TAC_PROOF( 269 ([],���!e:'a.!f. ?fn1. (fn1 t0 = e) /\ 270 (!t. fn1(SUC(t+t0)) = f (fn1 (t+t0)) (t+t0))���), 271 let val lemma = BETA_RULE(EXISTENCE(SPECL[(���e:'a���), 272 (���\n:'a.\m.(f n (m+t0)):'a���)] num_Axiom)) 273 in 274 REPEAT GEN_TAC THEN ASSUME_TAC lemma THEN LEFT_EXISTS_TAC 275 THEN EXISTS_TAC (���\t.fn1(t-t0):'a���) THEN BETA_TAC 276 THEN ASM_REWRITE_TAC[SUB_EQUAL_0] THEN GEN_TAC 277 THEN REWRITE_TAC[SYM(SPEC_ALL(CONJUNCT2 ADD)),ADD_SUB] 278 THEN ASM_REWRITE_TAC[] 279 end) 280 281*) 282 283 284 285(* ********************* BOOL_VAR_ELIM_TAC ******************** *) 286(* BOOL_VAR_ELIM_CONV v P[v:bool] proves the following theorem *) 287(* |- (!v.P[v]) = P[T] /\ P[F] *) 288(* The corresponding tactic looks as follows: *) 289(* *) 290(* G |- P[v:bool] *) 291(* ================= *) 292(* G |- P[T] /\ P[F] *) 293(* *) 294(* Note: This tactic is more useful than BOOL_CASES_TAC if the *) 295(* two formulae P[T] and P[F] are identical. Then the variable *) 296(* v is simply eliminated. *) 297(* ************************************************************ *) 298 299fun BOOL_VAR_ELIM_CONV v Pv = 300 let val lemma = TAC_PROOF( 301 ([],���!P.(!b.P b) =(P T) /\ (P F)���), 302 GEN_TAC THEN EQ_TAC THENL[ 303 DISCH_TAC, 304 STRIP_TAC THEN 305 GEN_TAC THEN BOOL_CASES_TAC (���b:bool���)] 306 THEN ASM_REWRITE_TAC[]) 307 in 308 BETA_RULE (SPEC (mk_abs(v,Pv)) lemma) 309 end 310 311 312fun BOOL_VAR_ELIM_TAC v (asm,g) = 313 let val x = genvar bool 314 val Pv = subst[v |-> x]g 315 val lemma = snd(EQ_IMP_RULE(BOOL_VAR_ELIM_CONV x Pv)) 316 in 317 (SPEC_TAC(v,x) THEN MATCH_MP_TAC lemma) (asm,g) 318 end 319 320 321 322(* ************************************************************ *) 323(* COND_FUN_EXT_CONV ((c=>f|g)x) --> *) 324(* |- ((c=>f|g)x) = (c => (f x) | (g x)) *) 325(* ************************************************************ *) 326 327fun COND_FUN_EXT_CONV condi = 328 let val (t,x) = dest_comb condi 329 val (c,f,g) = dest_cond t 330 val fx = mk_comb(f,x) 331 val gx = mk_comb(g,x) 332 val t' = mk_cond(c,fx,gx) 333 val gl = mk_eq(condi,t') 334 in 335 prove(gl,COND_CASES_TAC THEN REWRITE_TAC[]) 336 end 337 338val COND_FUN_EXT_TAC = CONV_TAC (TOP_DEPTH_CONV COND_FUN_EXT_CONV); 339 340 341(* ******************** COND_EQ_CONV ************************** *) 342(* Given a term of the form c=>(a=b)|(a=d) this conversion *) 343(* proves that |- [c=>(a=b)|(a=d)] = [a=(c=>b|d)]. This is *) 344(* quite useful for generation equations for rewriting. *) 345(* ************************************************************ *) 346 347fun COND_EQ_CONV t = 348 let val (c,l,r) = dest_cond t 349 val (a1,b) = dest_eq l 350 val (a2,d) = dest_eq r 351 val lemma = TAC_PROOF(([], 352 ���!a b c d. (c=>(a=b)|(a:'a=d)) = (a = (c=>b|d))���), 353 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���c:bool���) 354 THEN REWRITE_TAC[]) 355 val aty = type_of a1 356 val lemma' = INST_TYPE[alpha |-> aty]lemma 357 in 358 SPECL[a1,b,c,d]lemma' 359 end 360 361 362val COND_EQ_TAC = CONV_TAC (DEPTH_CONV(CHANGED_CONV COND_EQ_CONV)) 363 364 365(* ******************* SELECT_EXISTS_TAC ********************** *) 366(* *) 367(* G |- Q(@x.P x) *) 368(* ================================== *) 369(* G |- ?x.P x G |- !y.P y==> Q y *) 370(* *) 371(* The term @x.P x has to be given as argument. The tactic will *) 372(* then eliminate this term in Q and the subgoals above are *) 373(* obtained. This tactic only makes sense if G|-?x.P x holds. *) 374(* Otherwise the tactic below should be used. *) 375(* ************************************************************ *) 376 377fun SELECT_EXISTS_TAC t (asm,g) = 378 let val SELECT_ELIM_THM = TAC_PROOF( 379 ([],���!P Q. (?x:'a. P x) /\ (!y. P y ==> Q y) ==> Q(@x.P x)���), 380 REPEAT GEN_TAC 381 THEN SUBST1_TAC(SYM(SELECT_CONV(���P(@x:'a.P x)���))) 382 THEN STRIP_TAC THEN RES_TAC) 383 val (x,Px) = dest_select t 384 val P = mk_abs(x,Px) 385 val y = genvar(type_of x) 386 val Q = mk_abs (y, subst[t |-> y]g) 387 val lemma1 = INST_TYPE[alpha |-> type_of x] SELECT_ELIM_THM 388 val lemma2 = BETA_RULE(SPECL[P,Q]lemma1) 389 in 390 (MP2_TAC lemma2 THEN CONJ_TAC)(asm,g) 391 end 392 393 394 395(* *********************** SELECT_TAC ************************* *) 396(* *) 397(* G |- Q(@x.P x) *) 398(* ========================================== *) 399(* G |-(?x.P x) => !y. P y ==> Q y | !y.Q y *) 400(* *) 401(* ************************************************************ *) 402 403 404 405fun SELECT_TAC t (asm,g) = 406 let val SELECT_THM = TAC_PROOF(([], 407 ���!P Q. ((?x:'a.P x) => !y. P y ==> Q y | !y.Q y) ==> Q(@x.P x) ���), 408 REPEAT GEN_TAC 409 THEN DISJ_CASES_TAC(SPEC(���?x:'a.P x���)BOOL_CASES_AX) 410 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC 411 THENL[RULE_ASSUM_TAC 412 (REWRITE_RULE [SYM(SELECT_CONV (���P(@x:'a.P x)���))]) 413 THEN RES_TAC THEN ASM_REWRITE_TAC[], 414 ASM_REWRITE_TAC[]]) 415 val (x,Px) = dest_select t 416 val P = mk_abs(x,Px) 417 val y = genvar(type_of x) 418 val Q = mk_abs (y,subst[t |-> y]g) 419 val lemma1 = INST_TYPE[alpha |-> type_of x] SELECT_THM 420 val lemma2 = BETA_RULE(SPECL[P,Q]lemma1) 421 in 422 (MP2_TAC lemma2 THEN COND_CASES_TAC)(asm,g) 423 end 424 425 426(* **************** SELECT_UNIQUE_RULE *********************** *) 427(* *) 428(* "y" A1 |- Q[y] A2 |- !x y.(Q[x]/\Q[y]) ==> (x=y) *) 429(* =================================================== *) 430(* A1 U A2 |- (@x.Q[x]) = y *) 431(* *) 432(* Permits substitution for values specified by the Hilbert *) 433(* Choice operator with a specific value, if and only if unique *) 434(* existance of the specific value is proven. *) 435(* ************************************************************ *) 436 437 438val SELECT_UNIQUE_THM = TAC_PROOF(([], 439 ���!Q y. Q y /\ (!x y:'a.(Q x /\ Q y) ==> (x=y)) ==> ((@x.Q x) = y)���), 440 REPEAT STRIP_TAC THEN SELECT_EXISTS_TAC (���@x.(Q:'a->bool) x���) 441 THENL[EXISTS_TAC(���y:'a���) THEN ASM_REWRITE_TAC[], 442 GEN_TAC THEN DISCH_TAC THEN RES_TAC]) 443 444 445 446fun SELECT_UNIQUE_RULE y th1 th2 = 447 let val Q=(hd o strip_conj o fst o dest_imp o snd o strip_forall o concl) th2 448 val x = (hd o (filter(C mem(free_vars Q))) o fst o strip_forall o concl)th2 449 val Q' = mk_abs(x,Q) 450 val th1'=SUBST [(���b:bool���) |-> SYM (BETA_CONV (���^Q' ^y���))] 451 (���b:bool���) th1 452 in 453 (MP (SPECL [(���$@ ^Q'���), y] th2) 454 (CONJ (BETA_RULE (SELECT_INTRO th1')) th1)) 455 end 456 457 458fun SELECT_UNIQUE_TAC (asm,g) = 459 let val (Qx,y) = dest_eq g 460 val (x,Q) = dest_select Qx 461 val xty = type_of x 462 val Qy = mk_abs(x,Q) 463 val lemma1 = INST_TYPE[alpha |-> xty] SELECT_UNIQUE_THM 464 val lemma2 = BETA_RULE(SPECL[Qy,y] lemma1) 465 in 466 (MATCH_MP_TAC lemma2 THEN CONJ_TAC) (asm,g) 467 end 468 469 470fun COND_ELIM_CONV t = 471 let val lem = TAC_PROOF(([], 472 ���!a b c. (a=> b|c) = (a==>b) /\ (~a==> c)���), 473 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 474 THEN REWRITE_TAC[]) 475 val (a,b,c) = dest_cond t 476 in SPECL[a,b,c] lem 477 end 478 479val COND_ELIM_TAC = CONV_TAC(DEPTH_CONV COND_ELIM_CONV) 480 481 482end; 483