1 module Sections = struct
3 (* Basic commands for working with the goal stack *)
4 (* b() from tactics.ml *)
5 let revert_proof_step() =
6 let l = !current_goalstack in
7 if length l = 1 then failwith "Can't back up any more" else
8 current_goalstack := tl l;
12 (* A flag for fast proof loading (using mk_thm) *)
13 let fast_load_flag = ref false;;
15 (* Section variables, hypotheses (with labels), implicit types, and auxiliary lemmas *)
19 hyps : (string * term) list;
20 types : (string * hol_type) list;
21 lemmas : (string * thm) list;
25 let empty_section : section_info = {vars = []; hyps = []; types = []; lemmas = []};;
27 let section_stack = ref ([] : (string * section_info ref) list);;
30 (* Begins a new section *)
31 let begin_section name =
32 let sections = !section_stack in
33 if can (C assoc sections) name then
34 failwith ("Section " ^ name ^ " is already active")
36 let sections = (name, ref empty_section) :: sections in
37 section_stack := sections;;
40 (* Ends the active section *)
41 let end_section name =
42 let sections = !section_stack in
44 failwith "end_section: No open sections"
46 let last_name, _ = hd sections in
47 if Pervasives.compare last_name name <> 0 then
48 failwith ("The last open section is " ^ last_name)
50 section_stack := tl sections;;
53 (* Ends all sections *)
54 let end_all_sections () =
58 (* Returns all section variables in the current section *)
59 let current_section_vars () =
60 if !section_stack = [] then []
62 !((snd o hd) !section_stack).vars;;
65 (* Returns all hypotheses in the current section *)
66 let current_section_hyps () =
67 if !section_stack = [] then []
69 !((snd o hd) !section_stack).hyps;;
72 (* Returns all section variables from all sections *)
73 let section_vars () : term list =
74 let vars = map (fun (_, s) -> !s.vars) !section_stack in
78 (* Returns all implicit types from all sections *)
79 let section_types () : (string * hol_type) list =
80 let types = map (fun (_, s) -> !s.types) !section_stack in
84 (* Returns all hypotheses from all sections *)
85 let section_hyps () : (string * term) list =
86 let hyps = map (fun (_, s) -> !s.hyps) !section_stack in
90 (* Returns all lemmas from all sections *)
91 let section_lemmas () : (string * thm) list =
92 let lemmas = map (fun (_, s) -> !s.lemmas) !section_stack in
96 (* Returns names of all section lemmas and hypotheses *)
97 let section_labels () : string list =
98 let hyp_names = map fst (section_hyps()) and
99 lemma_names = map fst (section_lemmas()) in
100 hyp_names @ lemma_names;;
103 (* Instantiates types of section variables in the term *)
104 let inst_section_vars tm =
105 let s_vars = map dest_var (section_vars()) in
106 let find_var (name, ty) =
107 try (assoc name s_vars, ty)
108 with Failure _ -> (bool_ty, bool_ty) in
109 let inst_var (name, ty) tm =
110 let ty_dst, ty_src = find_var (name, ty) in
111 try (inst (type_match ty_src ty_dst []) tm)
113 failwith ("Section variable " ^ name ^
114 " has type " ^ string_of_type ty_dst) in
115 let f_vars = map dest_var (frees tm) in
116 itlist inst_var f_vars tm;;
119 (* Instantiates implicit types in the given term *)
120 (* (free variables and top generalized variables are considered in the term) *)
121 let inst_section_types tm =
122 let s_types = section_types() in
124 let name, ty = dest_var tm in
125 try (assoc name s_types, ty) with Failure _ -> (bool_ty, bool_ty) in
126 let f_vars = frees tm in
127 let g_vars, _ = strip_forall tm in
128 let ty_dst, ty_src = unzip (map find_type (g_vars @ f_vars)) in
129 let ty_inst = itlist2 type_match ty_src ty_dst [] in
133 (* Checks if the term contains any free variables
134 which are not section variables *)
135 let check_section_term tm =
136 let f_vars = frees tm in
137 if !section_stack = [] then
139 let str = String.concat ", " (map string_of_term f_vars) in
140 failwith ("Free variables: " ^ str)
143 let s_vars = section_vars() in
144 let vars = subtract f_vars s_vars in
146 let str = String.concat ", " (map string_of_term vars) in
147 failwith ("Free variables: " ^ str)
151 (* Adds the given variable to the active section *)
152 let add_section_var var =
153 let sections = !section_stack in
154 if sections = [] then
155 failwith "add_section_var: No open sections"
157 let s_var = section_vars() in
158 let var_name, _ = dest_var var in
159 if can (C assoc (map dest_var s_var)) var_name then
160 failwith ("A variable with the name "^var_name^" is already defined")
162 let section = (snd o hd) sections in
163 section := {!section with vars = var :: !section.vars};;
166 (* Adds the given implicit type to the active section *)
167 let add_section_type tm =
168 let sections = !section_stack in
169 if sections = [] then
170 failwith "add_section_type: No open sections"
172 let s_types = section_types() in
173 let var_name, ty = dest_var tm in
174 if can (C assoc s_types) var_name then
175 failwith ("An implicit type for the variable "^var_name^" is already defined")
177 let section = (snd o hd) sections in
178 section := {!section with types = (var_name, ty) :: !section.types};;
180 (* Adds the given lemma to the active section *)
181 let add_section_lemma name th =
182 let sections = !section_stack in
183 if sections = [] then
184 failwith "add_section_lemma: No open sections"
186 let labels = section_labels() in
187 if mem name labels then
188 failwith ("A lemma (or hypothesis) with the name " ^ name ^ " is already defined")
190 let section = (snd o hd) sections in
191 section := {!section with lemmas = (name, th) :: !section.lemmas};;
194 (* Adds the given hypothesis (term) to the active section *)
195 let add_section_hyp label hyp =
196 let sections = !section_stack in
197 if sections = [] then
198 failwith "add_section_hyp: No open sections"
200 let labels = section_labels() in
201 if mem label labels then
202 failwith ("A hypothesis (or lemma) with the label " ^ label ^ " is already defined")
204 let hyp0 = inst_section_vars hyp in
205 let hyp1 = inst_section_types hyp0 in
206 if type_of hyp1 <> bool_ty then
207 failwith "A boolean term is expected"
209 let section = (snd o hd) sections in
210 check_section_term hyp1;
211 section := {!section with hyps = (label, hyp1) :: !section.hyps};;
214 (* Removes the given variable from the active section *)
215 let remove_section_var var_name =
216 let sections = !section_stack in
217 if sections = [] then
218 failwith "remove_section_var: No open sections"
220 let section = (snd o hd) sections in
221 let new_vars = filter (fun var -> (fst o dest_var) var <> var_name) !section.vars in
222 section := {!section with vars = new_vars};;
225 (* Removes the given implicit type from the active section *)
226 let remove_section_type type_name =
227 let sections = !section_stack in
228 if sections = [] then
229 failwith "remove_section_type: No open sections"
231 let section = (snd o hd) sections in
232 let new_types = filter (fun name, _ -> name <> type_name) !section.types in
233 section := {!section with types = new_types};;
236 (* Removes the given lemma from the active section *)
237 let remove_section_lemma lemma_name =
238 let sections = !section_stack in
239 if sections = [] then
240 failwith "remove_section_lemma: No open sections"
242 let section = (snd o hd) sections in
243 let new_lemmas = filter (fun name, _ -> name <> lemma_name) !section.lemmas in
244 section := {!section with lemmas = new_lemmas};;
247 (* Removes the given assumption from the active section *)
248 let remove_section_hyp label =
249 let sections = !section_stack in
250 if sections = [] then
251 failwith "remove_section_hyp: No open sections"
253 let section = (snd o hd) sections in
254 let new_hyps = filter (fun name, _ -> name <> label) !section.hyps in
255 section := {!section with hyps = new_hyps};;
258 (* Prepares a goal term *)
259 let prepare_goal_term tm =
260 if !section_stack = [] then (check_section_term tm; tm)
262 let tm0 = inst_section_vars tm in
263 let tm1 = inst_section_types tm0 in
264 let s_hyps = map snd (section_hyps()) in
265 let r = itlist (curry mk_imp) s_hyps tm1 in
266 check_section_term r; r;;
269 (* Prepares a goal term and an initial tactic *)
270 let prepare_section_proof names tm =
271 let f_vars = map dest_var (frees tm) in
272 let find_type var_name =
273 try assoc var_name f_vars with Failure _ -> failwith ("Unused variable: " ^ var_name) in
274 let g_vars = map (fun name -> mk_var (name, find_type name)) names in
275 let g_tm = list_mk_forall (g_vars, tm) in
276 let tm0 = prepare_goal_term g_tm in
277 let hyp_names = map fst (section_hyps()) in
278 let lemmas = section_lemmas() in
279 let gen_tac = REPLICATE_TAC (length g_vars) GEN_TAC in
280 let disch_tac = itlist (fun name tac -> DISCH_THEN (LABEL_TAC name) THEN tac) hyp_names ALL_TAC in
281 let assume_tac = itlist (fun (name,lemma) tac -> LABEL_TAC name lemma THEN tac) lemmas ALL_TAC in
282 tm0, assume_tac THEN disch_tac THEN gen_tac;;
285 (* Starts a proof of the goal using section hypotheses *)
286 let start_section_proof names tm =
287 let tm0, tac0 = prepare_section_proof names tm in
288 let _ = set_goal([], tm0) in
289 refine (by (VALID tac0));;
292 (* Returns the final theorem *)
293 let end_section_proof () =
294 let th = top_thm() in
295 let hyps = section_hyps() in
296 itlist (fun _ th -> UNDISCH th) hyps th;;
299 (* Proves a lemma using section hypotheses and variables *)
300 let section_proof names tm tac_list =
301 let tm0, tac0 = prepare_section_proof names tm in
302 let gstate = mk_goalstate ([], tm0) in
304 if !fast_load_flag then
305 [fun g -> ACCEPT_TAC(mk_thm([], snd g)) g]
308 let _, sgs, just = rev_itlist by (tac0 :: tac_list1) gstate in
310 if sgs = [] then just null_inst []
311 else failwith "section_proof: unsolved goals" in
312 let hyps = section_hyps() in
313 itlist (fun _ th -> UNDISCH th) hyps th0;;
316 (* Discharges all assumptions and generalizes all section variables *)
317 let finalize_theorem th =
318 let hyps = map snd (current_section_hyps()) in
319 let th_hyps = hyp th in
320 let hyps0 = intersect hyps th_hyps in
321 let s_vars = current_section_vars() in
322 let th1 = rev_itlist (fun hyp th -> DISCH hyp th) hyps0 th in
323 let f_vars = frees (concl th1) in
324 let vars = intersect f_vars s_vars in
325 itlist (fun var th -> GEN var th) vars th1;;