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