1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Lemma: General Tactics *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
9 module Tactics = struct
11 (* ASSUMPTION LISTS *)
14 FIRST[FIRST_X_ASSUM CHOOSE_TAC;
15 FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC);
18 let FIRST_RULE_ASSUM rule ttc = FIRST_ASSUM (ttc o rule );;
20 let FIRST_RULE_X_ASSUM rule ttc = FIRST_X_ASSUM (ttc o rule );;
24 let INDUCT_SPEC_TAC vn =
25 let v = mk_var (vn,`:nat`) in
26 SPEC_TAC (v,v) THEN INDUCT_TAC;;
29 (* ------------------------------------------------------------------ *)
30 (* SELECT ELIMINATION.
31 SELECT_TAC should work whenever there is a single predicate selected.
32 Something more sophisticated might be needed when there
35 Useful for proving statements such as `1 + (@x. (x=3)) = 4` *)
36 (* ------------------------------------------------------------------ *)
38 (* spec form of SELECT_AX *)
39 let select_thm select_fn select_exist =
40 BETA_RULE (ISPECL [select_fn;select_exist]
45 `\m. (X:num->bool) m /\ (!n. X n ==> m <= n)` `n:num`;;
47 let SELECT_EXIST = prove_by_refinement(
48 `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
53 ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX);
59 let SELECT_THM = MESON[SELECT_EXIST]
60 `!(P:A->bool) Q. (((?y. P y) ==> (!t. (P t ==> Q t))) /\ ((~(?y. P y)) ==>
61 (!t. Q t))) ==> Q ((@) P)`;;
65 `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,MESON_TAC[]) in
66 let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in
67 unbeta_tac THEN (MATCH_MP_TAC SELECT_THM) THEN BETA_TAC THEN
72 let (PAT_MATCH:term list -> (string*thm) -> bool) = fun pat sth ->
73 not(search_thml (term_match[]) pat [sth] = []);;
75 let (PAT_TAC2:tactic -> tactic -> term list -> (string * thm) -> tactic) = fun tac1 tac2 pat sth -> if PAT_MATCH pat sth then tac1 else tac2;;
77 let (PAT_TAC:term list -> (string * thm) -> tactic) =
78 PAT_TAC2 ALL_TAC NO_TAC;;
80 let (FIRST_PAT_ASSUM: term list -> thm_tactic -> tactic) =
81 fun pat ttac gl -> tryfind (fun sth -> (PAT_TAC pat sth THEN ttac (snd sth)) gl) (goal_asms gl);;
83 let (FIRST_PAT_X_ASSUM:term list -> thm_tactic -> tactic) =
85 FIRST_PAT_ASSUM pat (fun th -> UNDISCH_THEN (concl th) ttac);;
87 let (EVERY_PAT_ASSUM:term list -> thm_tactic -> tactic) =
89 let rl = map snd (filter (PAT_MATCH pat) (goal_asms gl)) in
90 let tacl = map ttac rl in
93 (* Well defined functions *)
95 (* Harrison's lemma *)
96 let WELLDEFINED_FUNCTION_1 = prove
97 (`(?f:B->C. !x:A. f(s x) = t x) <=> (!x x'. s x = s x' ==> t x = t x')`,
98 MATCH_MP_TAC EQ_TRANS THEN
99 EXISTS_TAC `?f:B->C. !y. !x:A. s x = y ==> f y = t x` THEN
101 [MESON_TAC[]; REWRITE_TAC[GSYM SKOLEM_THM] THEN
105 let WELLDEFINED_FUNCTION_2b = prove_by_refinement(
106 `(?f:C->D. (!x:A y:B. P x y ==> f(s x y) = t x y)) <=>
107 (!x x' y y'. (P x y /\ P x' y' /\ (s x y = s x' y')) ==> t x y = t x' y')`,
109 MATCH_MP_TAC EQ_TRANS ;
110 EXISTS_TAC `?f:C->D. !z. !x:A y:B. ((P x y) /\ (s x y = z)) ==> f z = t x y`;
113 REWRITE_TAC[GSYM SKOLEM_THM];