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 x IN FVs 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 140local 141val lem = TAC_PROOF(([],���!a b. a\/b <=> ~b==>a���), 142 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 143 THEN REWRITE_TAC[]) 144in 145fun LEFT_DISJ_TAC (asm,g) = 146 let 147 val (a,b) = dest_disj g 148 in (SUBST1_TAC(SPECL[a,b]lem) THEN DISCH_TAC) (asm,g) 149 end 150end 151 152local 153val lem = TAC_PROOF(([],���!a b. a\/b <=> ~a==>b���), 154 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 155 THEN REWRITE_TAC[]) 156in 157fun RIGHT_DISJ_TAC (asm,g) = 158 let val (a,b) = dest_disj g 159 in (SUBST1_TAC(SPECL[a,b]lem) THEN DISCH_TAC) (asm,g) 160 end 161end 162 163 164(* ********* LEFT_CONJ_TAC & RIGHT_CONJ_TAC ******************* *) 165(* *) 166(* G |- a/\b G |- a/\b *) 167(* ================== ================= *) 168(* G |- a | G,a|- b G |- b | G,b|- a *) 169(* ************************************************************ *) 170 171val LEFT_CONJ_TAC = CONJ_ASM1_TAC 172val RIGHT_CONJ_TAC = CONJ_ASM2_TAC 173 174(* ********** LEFT_LEMMA_DISJ_CASES_TAC *********************** *) 175(* Given a theorem G|-a\/b, these tactics behave as follows: *) 176(* *) 177(* A|-phi A|-phi *) 178(* ============================ ============================ *) 179(* A,G,a|-phi A,G,~a,b|-phi A,G,a,~b|-phi A,G,b|-phi *) 180(* *) 181(* ************************************************************ *) 182 183local 184 val absorb_lem = prove(���!a b. a\/b <=> a \/(~a/\b)���, 185 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���a:bool���) 186 THEN REWRITE_TAC[]) 187in 188fun LEFT_LEMMA_DISJ_CASES_TAC th = 189 let val (a,b) = dest_disj (concl th) 190 in DISJ_CASES_TAC (EQ_MP (SPECL[a,b]absorb_lem) th) THEN UNDISCH_HD_TAC 191 THEN STRIP_TAC 192 end 193end 194 195local 196 val absorb_lem = prove(���!a b. a\/b <=> (a/\~b) \/ b���, 197 REPEAT GEN_TAC THEN BOOL_CASES_TAC (���b:bool���) 198 THEN REWRITE_TAC[]) 199in 200fun RIGHT_LEMMA_DISJ_CASES_TAC th = 201 let val (a,b) = dest_disj (concl th) 202 in DISJ_CASES_TAC (EQ_MP (SPECL[a,b]absorb_lem) th) THEN UNDISCH_HD_TAC 203 THEN STRIP_TAC 204 end 205end 206 207 208 209 210(* *********************** MP2_TAC **************************** *) 211(* A ?- t *) 212(* ============== MP2_TAC (A' |- s ==> t) *) 213(* A ?- s *) 214(* *) 215(* ************************************************************ *) 216 217fun MP2_TAC th ((asm,g):goal) = 218 let val (s,t) = dest_imp(concl th) 219 in ([(asm,s)],fn [t]=> MP th t | _ => raise Match) 220 end 221 222 223 224 225(* ********************* MY_MP_TAC **************************** *) 226(* A ?- t *) 227(* ======================= MP2_TAC s *) 228(* A ?- s | A ?- s ==> t *) 229(* *) 230(* ************************************************************ *) 231 232local 233val lemma = TAC_PROOF( 234 ([],���!b.(?a.a /\ (a==>b)) ==> b���), 235 GEN_TAC THEN STRIP_TAC THEN RES_TAC) 236in 237fun MY_MP_TAC t (asm,g) = 238 (MATCH_MP_TAC (SPEC g lemma) THEN EXISTS_TAC t THEN CONJ_TAC) (asm,g) 239end 240 241 242(* ****************** TAC_CONV ******************************** *) 243(* TAC_CONV: takes a tactic and generates a conversion of it *) 244(* Caution: does not work properly so far *) 245(* ************************************************************ *) 246 247fun TAC_CONV (tac:tactic) t = 248 let val goal = ([],t) 249 val subgoals = fst (tac goal) 250 val terms = map (fn (asm,g) =>if null asm then g 251 else mk_imp(list_mk_conj asm, g)) subgoals 252 val term = list_mk_conj terms 253 val eq = mk_eq(t,term) 254 in 255 TAC_PROOF(([],eq),tac THEN REWRITE_TAC[]) 256 end 257 258 259 260 261 262(* ************************************************************ *) 263 264(* ************************************************************ *) 265 266(* 267val num_Axiom1 = TAC_PROOF( 268 ([],���!e:'a.!f. ?fn1. (fn1 t0 = e) /\ 269 (!t. fn1(SUC(t+t0)) = f (fn1 (t+t0)) (t))���), 270 let val lemma = EXISTENCE(SPEC_ALL num_Axiom) 271 in 272 REPEAT GEN_TAC THEN ASSUME_TAC lemma THEN LEFT_EXISTS_TAC 273 THEN EXISTS_TAC (���\t.fn1(t-t0):'a���) THEN BETA_TAC 274 THEN ASM_REWRITE_TAC[SUB_EQUAL_0] THEN GEN_TAC 275 THEN REWRITE_TAC[SYM(SPEC_ALL(CONJUNCT2 ADD)),ADD_SUB] 276 THEN ASM_REWRITE_TAC[] 277 end) 278 279 280val num_Axiom2 = TAC_PROOF( 281 ([],���!e:'a.!f. ?fn1. (fn1 t0 = e) /\ 282 (!t. fn1(SUC(t+t0)) = f (fn1 (t+t0)) (t+t0))���), 283 let val lemma = BETA_RULE(EXISTENCE(SPECL[(���e:'a���), 284 (���\n:'a.\m.(f n (m+t0)):'a���)] num_Axiom)) 285 in 286 REPEAT GEN_TAC THEN ASSUME_TAC lemma THEN LEFT_EXISTS_TAC 287 THEN EXISTS_TAC (���\t.fn1(t-t0):'a���) THEN BETA_TAC 288 THEN ASM_REWRITE_TAC[SUB_EQUAL_0] THEN GEN_TAC 289 THEN REWRITE_TAC[SYM(SPEC_ALL(CONJUNCT2 ADD)),ADD_SUB] 290 THEN ASM_REWRITE_TAC[] 291 end) 292 293*) 294 295 296 297(* ********************* BOOL_VAR_ELIM_TAC ******************** *) 298(* BOOL_VAR_ELIM_CONV v P[v:bool] proves the following theorem *) 299(* |- (!v.P[v]) = P[T] /\ P[F] *) 300(* The corresponding tactic looks as follows: *) 301(* *) 302(* G |- P[v:bool] *) 303(* ================= *) 304(* G |- P[T] /\ P[F] *) 305(* *) 306(* Note: This tactic is more useful than BOOL_CASES_TAC if the *) 307(* two formulae P[T] and P[F] are identical. Then the variable *) 308(* v is simply eliminated. *) 309(* ************************************************************ *) 310 311local 312 val lemma = prove(���!P.(!b.P b) <=> (P T) /\ (P F)���, 313 GEN_TAC THEN EQ_TAC THENL[ 314 DISCH_TAC, 315 STRIP_TAC THEN 316 GEN_TAC THEN BOOL_CASES_TAC (���b:bool���)] 317 THEN ASM_REWRITE_TAC[]) 318in 319fun BOOL_VAR_ELIM_CONV v Pv = 320 BETA_RULE (SPEC (mk_abs(v,Pv)) lemma) 321end 322 323 324fun BOOL_VAR_ELIM_TAC v (asm,g) = 325 let val x = genvar bool 326 val Pv = subst[v |-> x]g 327 val lemma = snd(EQ_IMP_RULE(BOOL_VAR_ELIM_CONV x Pv)) 328 in 329 (SPEC_TAC(v,x) THEN MATCH_MP_TAC lemma) (asm,g) 330 end 331 332 333 334(* ************************************************************ *) 335(* COND_FUN_EXT_CONV ((c=>f|g)x) --> *) 336(* |- ((c=>f|g)x) = (c => (f x) | (g x)) *) 337(* ************************************************************ *) 338 339fun COND_FUN_EXT_CONV condi = 340 let val (t,x) = dest_comb condi 341 val (c,f,g) = dest_cond t 342 val fx = mk_comb(f,x) 343 val gx = mk_comb(g,x) 344 val t' = mk_cond(c,fx,gx) 345 val gl = mk_eq(condi,t') 346 in 347 prove(gl,COND_CASES_TAC THEN REWRITE_TAC[]) 348 end 349 350val COND_FUN_EXT_TAC = CONV_TAC (TOP_DEPTH_CONV COND_FUN_EXT_CONV); 351 352 353(* ******************* SELECT_EXISTS_TAC ********************** *) 354(* *) 355(* G |- Q(@x.P x) *) 356(* ================================== *) 357(* G |- ?x.P x G |- !y.P y==> Q y *) 358(* *) 359(* The term @x.P x has to be given as argument. The tactic will *) 360(* then eliminate this term in Q and the subgoals above are *) 361(* obtained. This tactic only makes sense if G|-?x.P x holds. *) 362(* Otherwise the tactic below should be used. *) 363(* ************************************************************ *) 364 365fun SELECT_EXISTS_TAC t (asm,g) = 366 let val SELECT_ELIM_THM = TAC_PROOF( 367 ([],���!P Q. (?x:'a. P x) /\ (!y. P y ==> Q y) ==> Q(@x.P x)���), 368 REPEAT GEN_TAC 369 THEN SUBST1_TAC(SYM(SELECT_CONV(���P(@x:'a.P x)���))) 370 THEN STRIP_TAC THEN RES_TAC) 371 val (x,Px) = dest_select t 372 val P = mk_abs(x,Px) 373 val y = genvar(type_of x) 374 val Q = mk_abs (y, subst[t |-> y]g) 375 val lemma1 = INST_TYPE[alpha |-> type_of x] SELECT_ELIM_THM 376 val lemma2 = BETA_RULE(SPECL[P,Q]lemma1) 377 in 378 (MP2_TAC lemma2 THEN CONJ_TAC)(asm,g) 379 end 380 381(* **************** SELECT_UNIQUE_RULE *********************** *) 382(* *) 383(* "y" A1 |- Q[y] A2 |- !x y.(Q[x]/\Q[y]) ==> (x=y) *) 384(* =================================================== *) 385(* A1 U A2 |- (@x.Q[x]) = y *) 386(* *) 387(* Permits substitution for values specified by the Hilbert *) 388(* Choice operator with a specific value, if and only if unique *) 389(* existance of the specific value is proven. *) 390(* ************************************************************ *) 391 392 393val SELECT_UNIQUE_THM = TAC_PROOF(([], 394 ���!Q y. Q y /\ (!x y:'a.(Q x /\ Q y) ==> (x=y)) ==> ((@x.Q x) = y)���), 395 REPEAT STRIP_TAC THEN SELECT_EXISTS_TAC (���@x.(Q:'a->bool) x���) 396 THENL[EXISTS_TAC(���y:'a���) THEN ASM_REWRITE_TAC[], 397 GEN_TAC THEN DISCH_TAC THEN RES_TAC]) 398 399 400 401fun SELECT_UNIQUE_RULE y th1 th2 = 402 let val Q=(hd o strip_conj o fst o dest_imp o snd o strip_forall o concl) th2 403 val x = (hd o (filter(C tmem(free_vars Q))) o fst o strip_forall o concl)th2 404 val Q' = mk_abs(x,Q) 405 val th1'=SUBST [(���b:bool���) |-> SYM (BETA_CONV (���^Q' ^y���))] 406 (���b:bool���) th1 407 in 408 (MP (SPECL [(���$@ ^Q'���), y] th2) 409 (CONJ (BETA_RULE (SELECT_INTRO th1')) th1)) 410 end 411 412 413fun SELECT_UNIQUE_TAC (asm,g) = 414 let val (Qx,y) = dest_eq g 415 val (x,Q) = dest_select Qx 416 val xty = type_of x 417 val Qy = mk_abs(x,Q) 418 val lemma1 = INST_TYPE[alpha |-> xty] SELECT_UNIQUE_THM 419 val lemma2 = BETA_RULE(SPECL[Qy,y] lemma1) 420 in 421 (MATCH_MP_TAC lemma2 THEN CONJ_TAC) (asm,g) 422 end 423 424 425end; 426