3 val CONTEXT_TAC : ((string * pretype) list -> tactic) -> tactic
4 val PARSE_IN_CONTEXT : (term -> tactic) -> (string -> tactic)
5 val EXISTS_TAC : string -> tactic
6 val SUBGOAL_THEN : string -> thm_tactic -> tactic
7 val SUBGOAL_TAC : string -> string -> tactic list -> tactic
8 val ASM_CASES_TAC : string -> tactic
9 val BOOL_CASES_TAC : string -> tactic
10 val SPEC_TAC : string * string -> tactic
11 val SPEC : string -> thm -> thm
12 val SPECL : string list -> thm -> thm
13 val GEN : string -> thm -> thm
14 val GENL : string list -> thm -> thm
15 val X_GEN_TAC : string -> tactic
16 val REAL_ARITH : string -> thm
17 val REAL_FIELD : string -> thm
18 val REAL_RING : string -> thm
19 val ARITH_RULE : string -> thm
20 val NUM_RING : string -> thm
21 val INT_ARITH : string -> thm
22 val call_with_interface : (unit -> 'a) -> (term -> 'b) -> string -> 'b
26 let parse_preterm = fst o parse_preterm o lex o explode
28 let CONTEXT_TAC ttac (asms,c as g) =
29 let vs = frees c @ freesl (map (concl o snd) asms) in
30 ttac (map (fun x -> name_of x,pretype_of_type(type_of x)) vs) g
32 let PARSE_IN_CONTEXT ttac s =
33 CONTEXT_TAC (fun env ->
34 ttac (term_of_preterm (retypecheck env (parse_preterm s))))
36 let type_of_forall = type_of o fst o dest_forall
38 let force_type ?(env=[]) s ty =
39 let pty = pretype_of_type ty in
40 term_of_preterm (retypecheck env (Typing(parse_preterm s,pty)))
42 let BOOL_CONTEXT_TAC ttac s =
43 CONTEXT_TAC (fun env -> ttac (force_type ~env s bool_ty))
45 let SUBGOAL_THEN s ttac = BOOL_CONTEXT_TAC (C SUBGOAL_THEN ttac) s
46 let SUBGOAL_TAC l s tacs = BOOL_CONTEXT_TAC (C (SUBGOAL_TAC l) tacs) s
48 let ASM_CASES_TAC = BOOL_CONTEXT_TAC ASM_CASES_TAC
49 let BOOL_CASES_TAC = BOOL_CONTEXT_TAC BOOL_CASES_TAC
51 let EXISTS_TAC s (_,c as g) =
52 CONTEXT_TAC (fun env ->
53 EXISTS_TAC (force_type ~env s (type_of (fst (dest_exists c))))) g
56 PARSE_IN_CONTEXT (fun u' -> SPEC_TAC (u',force_type x (type_of u'))) u
58 let SPEC s th = SPEC (force_type s (type_of_forall (concl th))) th
61 try rev_itlist SPEC tms th with Failure _ -> failwith "SPECL"
64 GEN (try find ((=) s o name_of) (frees (concl th)) with _ -> parse_term s)
69 let X_GEN_TAC s (_,c as g) = X_GEN_TAC (force_type s (type_of_forall c)) g
71 let call_with_interface p f s =
72 let i = !the_interface in
74 let res = f (parse_term s) in
78 let [REAL_ARITH;REAL_FIELD;REAL_RING] =
79 map (call_with_interface prioritize_real) [REAL_ARITH;REAL_FIELD;REAL_RING]
80 let [ARITH_RULE;NUM_RING] =
81 map (call_with_interface prioritize_num) [ARITH_RULE;NUM_RING]
82 let INT_ARITH = call_with_interface prioritize_int INT_ARITH
88 let COMPLEX_FIELD = call_with_interface prioritize_complex COMPLEX_FIELD;;
89 let SIMPLE_COMPLEX_ARITH =
90 call_with_interface prioritize_complex SIMPLE_COMPLEX_ARITH;
93 let MP_REWRITE_TAC th (_,c as g) =
94 let [th] = mk_rewrites true th [] in
95 let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
97 ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
98 (SUBGOAL_THEN (lhand (concl !th)) (fun x ->
99 REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;
101 let CASES_REWRITE_TAC th (_,c as g) =
102 let [th] = mk_rewrites true th [] in
103 let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
104 let th = ref TRUTH in
105 ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
106 (ASM_CASES_TAC (lhand (concl !th)) THENL [
107 POP_ASSUM (fun x -> REWRITE_TAC[MP !th x] THEN ASSUME_TAC x);
108 POP_ASSUM (ASSUME_TAC o REWRITE_RULE[NOT_CLAUSES])]) g;;
110 let wrap f x = f [x];;
112 let CONJS xs = end_itlist CONJ xs;;
114 let rec simp_horn_conv =
115 let is_atomic (x,y) = if x = [] then y else failwith "" in
116 let rec tl = function [] -> [] | _::xs -> xs in
118 let fixpoint = ref true in
120 rev_itlist (fun (hs,cs) (dones,todos) ->
121 let atomics = flat (mapfilter is_atomic (dones@todos)) in
122 let f = filter (not o C mem atomics) in
123 let hs' = f hs and cs' = f cs in
124 if not (hs' = hs) or not (cs' = cs) then fixpoint := false;
125 if (cs' = [] && cs <> [])
126 then (dones,tl todos)
127 else ((hs',cs')::dones),tl todos)
130 if !fixpoint then l else simp_horn_conv (fst l');;
133 let strip_conj = binops `(/\)` in
134 fun t -> map (fun t ->
136 let h,c = dest_imp t in
137 strip_conj h,strip_conj c
138 with _ -> [],[t]) (strip_conj t);;
141 let term_of_horn = function
142 |[],cs -> list_mk_conj cs
143 |_,[] -> (print_endline "ici";`T`)
144 |hs,cs -> mk_imp (list_mk_conj hs,list_mk_conj cs)
146 list_mk_conj o map term_of_horn;;
148 let SIMP_HORN_CONV t =
149 TAUT (mk_eq (t,((term_of_horns o simp_horn_conv o horns_of_term) t)));;
153 THEN CONV_TAC (TOP_DEPTH_CONV (CHANGED_CONV SIMP_HORN_CONV));;
155 let HINT_EXISTS_TAC =
156 let strip_conj = binops `/\` in
159 let hs = map snd hs in
160 let vars = flat (map thm_frees hs) in
161 let vs,c' = strip_exists c in
162 let cs = strip_conj c' in
163 let hyp_match c h = term_match (subtract vars vs) c (concl h), h in
164 let (_,fosubs,_),h = tryfind (fun c -> tryfind (hyp_match c) hs) cs in
165 let ts,vs' = unzip fosubs in
166 let vs'' = subtract vs vs' in
167 let th = MESON[] (mk_eq(list_mk_exists(vs,P),list_mk_exists(vs'@vs'',P))) in
168 (REWRITE_TAC [th] THEN MAP_EVERY EXISTS_TAC ts THEN REWRITE_TAC [h]) g;;
170 let rec fixpoint f x =
172 if y = x then y else fixpoint f y;;
175 GEN_ALL o REWRITE_RULE[IMP_IMP;GSYM CONJ_ASSOC] o DISCH_ALL o fixpoint
176 (UNDISCH_ALL o SPEC_ALL);;