Update from HH
[hl193./.git] / RichterHilbertAxiomGeometry / readable.ml
1 (* ========================================================================= *)
2 (*        Miz3 interface for readable HOL Light tactics formal proofs        *)
3 (*                                                                           *)
4 (*                (c) Copyright, Bill Richter 2013                           *)
5 (*          Distributed under the same license as HOL Light                  *)
6 (*                                                                           *)
7 (* The primary meaning of readability is explained in the HOL Light tutorial *)
8 (* on page 81 after the proof of NSQRT_2 (ported below),                     *)
9 (* "We would like to claim that this proof can be read in isolation, without *)
10 (* running it in HOL.  For each step, every fact we used is clearly labelled *)
11 (* somewhere else in the proof, and every assumption is given explicitly."   *)
12 (* However readability is often improved by using tactics constructs like    *)
13 (* SIMP_TAC and MATCH_MP_TAC, which allow facts and assumptions to not be    *)
14 (* given explicitly, so as to not lose sight of the proof.  Readability is   *)
15 (* improved by a miz3 interface with few type annotations, back-quotes or    *)
16 (* double-quotes, and allowing HOL4/Isabelle math characters, e.g.           *)
17 (* ⇒ ⇔ ∧ ∨ ¬ ∀ ∃ ∈ ∉ α β γ λ θ μ ⊂ ∩ ∪ ∅ ━ ≡ ≅ ∡ ∥ ∏ ∘ →  ╪ .                *)
18 (* We use ideas for readable formal proofs due to John Harrison ("Towards    *)
19 (* more readable proofs" of the tutorial and Examples/mizar.ml), Freek       *)
20 (* Wiedijk (Mizarlight/miz2a.ml, miz3/miz3.ml and arxiv.org/pdf/1201.3601    *)
21 (* "A Synthesis of Procedural and Declarative Styles of Interactive          *)
22 (* Theorem Proving"), Marco Maggesi (author of tactic constructs             *)
23 (* INTRO_TAC, DESTRUCT_TAC & HYP), Petros Papapanagiotou (coauthor of        *)
24 (* Isabelle Light), Vincent Aravantinos (author of the Q-module              *)
25 (* https://github.com/aravantv/HOL-Light-Q) and Mark Adams (author of HOL    *)
26 (* Zero and Tactician).  These readability ideas yield the miz3-type         *)
27 (* declarative constructs assume, consider and case_split.  The semantics of *)
28 (* readable.ml is clear from an obvious translation to HOL Light proofs.  An *)
29 (* interactive mode is useful in writing, debugging and displaying proofs.   *)
30 (*                                                                           *)
31 (* The construct "case_split" reducing the goal to various cases given by    *)
32 (* "suppose" clauses.  The construct "proof" [...] "qed" allows arbitrarily  *)
33 (* long proofs, which can be arbitrarily nested with other case_split and    *)
34 (* proof/qed constructs.  THENL is only implemented implicitly in case_split *)
35 (* (also eq_tac and conj_tac), and this requires adjustments, such as using  *)
36 (* MATCH_MP_TAC num_INDUCTION instead of INDUCT_TAC.                         *)
37 (* ========================================================================= *)
38
39 (* The Str library defines regexp functions needed to process strings.       *)
40
41 #load "str.cma";;
42
43 (* parse_qproof uses system.ml quotexpander feature designed for miz3.ml to  *)
44 (* turn backquoted expression `;[...]` into a string with no newline or      *)
45 (* backslash problems.  Note that miz3.ml defines parse_qproof differently.  *)
46
47 let parse_qproof s = (String.sub s 1 (String.length s - 1));;
48
49 (* Allows HOL4 and Isabelle style math characters.                           *)
50
51 let CleanMathFontsForHOL_Light s =
52   let rec clean s loStringPairs =
53     match loStringPairs with
54     | [] -> s
55     | hd :: tl ->
56       let s = Str.global_replace (Str.regexp (fst hd)) (snd hd) s in
57       clean s tl in
58       clean s ["⇒","==>"; "⇔","<=>"; "∧","/\\ "; "∨","\\/"; "¬","~";
59       "∀","!"; "∃","?"; "∈","IN"; "∉","NOTIN";
60       "α","alpha"; "β","beta"; "γ","gamma"; "λ","\\ "; "θ","theta"; "μ","mu";
61       "⊂","SUBSET"; "∩","INTER"; "∪","UNION"; "∅","{}"; "━","DIFF";
62       "≡","==="; "≅","cong"; "∡","angle"; "∥","parallel";
63       "∏","prod"; "∘","_o_"; "→","--->"; "╪","INSERT"];;
64
65 (* printReadExn prints uncluttered error messages via Readable_fail.  This   *)
66 (* is due to Mark Adams, who also explained Roland Zumkeller's exec below.   *)
67
68 exception Readable_fail of string;;
69
70 let printReadExn e =
71   match e with
72   | Readable_fail s
73        -> print_string s
74   | _  -> print_string (Printexc.to_string e);;
75
76 #install_printer printReadExn;;
77
78 (* From update_database.ml: Execute any OCaml expression given as a string.  *)
79
80 let exec = ignore o Toploop.execute_phrase false Format.std_formatter
81   o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
82
83 (* Following miz3.ml, exec_thm returns the theorem representing a string, so *)
84 (* exec_thm "FORALL_PAIR_THM";; returns                                      *)
85 (* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2))                   *)
86 (* Extra error-checking is done to rule out the possibility of the theorem   *)
87 (* string ending with a semicolon.                                           *)
88
89 let thm_ref = ref TRUTH;;
90 let tactic_ref = ref ALL_TAC;;
91 let thmtactic_ref = ref MATCH_MP_TAC;;
92 let thmlist_tactic_ref = ref REWRITE_TAC;;
93 let termlist_thm_thm_ref = ref SPECL;;
94 let thm_thm_ref = ref GSYM;;
95 let term_thm_ref = ref ARITH_RULE;;
96 let thmlist_term_thm_ref = ref MESON;;
97
98 let exec_thm s =
99   if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse
100   else
101     try exec ("thm_ref := (("^ s ^"): thm);;");
102       !thm_ref
103     with _ -> raise Noparse;;
104
105 let exec_tactic s =
106   try exec ("tactic_ref := (("^ s ^"): tactic);;"); !tactic_ref
107   with _ -> raise Noparse;;
108
109 let exec_thmlist_tactic s =
110   try
111     exec ("thmlist_tactic_ref := (("^ s ^"): thm list -> tactic);;");
112     !thmlist_tactic_ref
113   with _ -> raise Noparse;;
114
115 let exec_thmtactic s =
116   try exec ("thmtactic_ref := (("^ s ^"): thm -> tactic);;"); !thmtactic_ref
117   with _ -> raise Noparse;;
118
119 let exec_termlist_thm_thm s =
120   try exec ("termlist_thm_thm_ref := (("^ s ^"): (term list -> thm -> thm));;");
121     !termlist_thm_thm_ref
122   with _ -> raise Noparse;;
123
124 let exec_thm_thm s =
125   try exec ("thm_thm_ref := (("^ s ^"): (thm -> thm));;");
126     !thm_thm_ref
127   with _ -> raise Noparse;;
128
129 let exec_term_thm s =
130   try exec ("term_thm_ref := (("^ s ^"): (term -> thm));;");
131     !term_thm_ref
132   with _ -> raise Noparse;;
133
134 let exec_thmlist_term_thm s =
135   try exec ("thmlist_term_thm_ref := (("^ s ^"): (thm list ->term -> thm));;");
136     !thmlist_term_thm_ref
137   with _ -> raise Noparse;;
138
139 (* make_env and parse_env_string (following parse_term from parser.ml,       *)
140 (* Mizarlight/miz2a.ml and https://github.com/aravantv/HOL-Light-Q) turn a   *)
141 (* string into a term with types inferred by the goal and assumption list.   *)
142
143 let (make_env: goal -> (string * pretype) list) =
144   fun (asl, w) -> map ((fun (s, ty) -> (s, pretype_of_type ty)) o dest_var)
145                    (freesl (w::(map (concl o snd) asl)));;
146
147 let parse_env_string env s =
148   let (ptm, l) = (parse_preterm o lex o explode) s in
149   if l = [] then (term_of_preterm o retypecheck env) ptm
150   else raise (Readable_fail
151     ("Unparsed input  at the end of the term\n" ^ s));;
152
153 (* versions of new_constant, parse_as_infix, new_definition and new_axiom    *)
154
155 let NewConstant (x, y) = new_constant(CleanMathFontsForHOL_Light x, y);;
156
157 let ParseAsInfix (x, y) = parse_as_infix (CleanMathFontsForHOL_Light x, y);;
158
159 let NewDefinition s =
160   new_definition (parse_env_string [] (CleanMathFontsForHOL_Light s));;
161
162 let NewAxiom s =
163   new_axiom (parse_env_string [] (CleanMathFontsForHOL_Light s));;
164
165 (* String versions without type annotations of SUBGOAL_THEN, SUBGOAL_TAC,    *)
166 (* intro_TAC, EXISTS_TAC, X_GEN_TAC, and EXISTS_TAC, and also new miz3-type  *)
167 (* tactic constructs assume, consider and case_split.                        *)
168
169 (* subgoal_THEN stm ttac gl = (SUBGOAL_THEN t ttac) gl,                      *)
170 (* where stm is a string that turned into a statement t by make_env and      *)
171 (* parse_env_string, using the goal gl.  We call stm a string statement.     *)
172 (* ttac is often the thm_tactic (LABEL_TAC string) or (DESTRUCT_TAC string). *)
173
174 let subgoal_THEN stm ttac gl =
175   SUBGOAL_THEN (parse_env_string (make_env gl) stm) ttac gl;;
176
177 (* subgoal_TAC stm lab tac gl = (SUBGOAL_TAC lab t [tac]) gl,                *)
178 (* exists_TAC stm gl = (EXISTS_TAC t) gl, and                                *)
179 (* X_gen_TAC svar gl = (X_GEN_TAC v) gl, where                               *)
180 (* stm is a string statement which is turned into a statement t by make_env, *)
181 (* parse_env_string and the goal gl. Similarly string svar is turned into a  *)
182 (* variable v.                                                               *)
183 (* X_genl_TAC combines X_gen_TAC and GENL.  Since below in StepToTactic the  *)
184 (* string-term list uses whitespace as the delimiter and no braces, there is *)
185 (* no reason in readable.ml proofs to use X_gen_TAC instead X_genl_TAC.      *)
186 (* intro_TAC is INTRO_TAC with the delimiter ";" replaced with",".           *)
187 (* eq_tac string tac                                                         *)
188 (* requires the goal to be an iff statement of the form x ⇔ y and then       *)
189 (* performs an EQ_TAC.  If string = "Right", then the tactic tac proves the  *)
190 (* implication y ⇒ x, and the goal becomes the other implication x ⇒ y.      *)
191 (* If string = "Left", then tac proves x ⇒ y and the goal becomes y ⇒ x.     *)
192 (* conj_tac string tac                                                       *)
193 (* requires the goal to be a conjunction statement x ∧ y and then performs a *)
194 (* CONJ_TAC.  If string = "Left" then the tactic tac proves x, and the goal  *)
195 (* becomes y.  If string = "Right", tac proves y and the new goal is x.      *)
196 (* consider svars stm lab tac                                                *)
197 (* defines new variables given by the string svars = "v1 v2 ... vn" and the  *)
198 (* string statement stm, which subgoal_THEN turns into statement t, labeled  *)
199 (* by lab.  The tactic tac proves the existential statement ?v1 ... vn. t.   *)
200 (* case_split sDestruct tac listofDisj listofTac                             *)
201 (* reduces the goal to n cases which are solved separately.  listofDisj is a *)
202 (* list of strings [st_1;...; st_n] whose disjunction st_1 \/...\/ st_n is a *)
203 (* string statement proved by tactic tac.  listofTac is a list of tactics    *)
204 (* [tac_1;...; tac_n] which prove the statements st_1,..., st_n.  The string *)
205 (* sDestruct must have the form "lab_1 |...| lab_n", and lab_i is a label    *)
206 (* used by tac_i to prove st_i.  Each lab_i must be a nonempty string.       *)
207 (* assume                                                                    *)
208 (* is a version of ASM_CASES_TAC, and performs proofs by contradiction and   *)
209 (* binary case_splits where one of the forks has a short proof.  In general, *)
210 (* assume statement lab tac                                                  *)
211 (* turns the string statement into a term t, with the tactic tac a proof of  *)
212 (* ¬t ⇒ w, where w is the goal. There is a new assumption t labeled lab, and *)
213 (* the new goal is the result of applying the tactic SIMP_TAC [t] to w.      *)
214 (* It's recommended to only use assume with a short proof tac.  Three uses   *)
215 (* of assume arise when t = ¬w or t = ¬α, with w = α ∨ β or w = β ∨ α.       *)
216 (* In all three cases write                                                  *)
217 (*      assume statement     [lab] by fol;                                   *)
218 (* and the new goal will be F (false) or β respectively, as a result of the  *)
219 (* SIMP_TAC [t].  So do not use assume if SIMP_TAC [t] is disadvantageous.   *)
220
221 let subgoal_TAC stm lab tac gl =
222   SUBGOAL_TAC lab (parse_env_string (make_env gl) stm) [tac] gl;;
223
224 let exists_TAC stm gl =
225   EXISTS_TAC (parse_env_string (make_env gl) stm) gl;;
226
227 let X_gen_TAC svar (asl, w as gl) =
228   let vartype = (snd o dest_var o fst o dest_forall) w in
229   X_GEN_TAC (mk_var (svar, vartype)) gl;;
230
231 let X_genl_TAC svarlist = MAP_EVERY X_gen_TAC svarlist;;
232
233 let intro_TAC s = INTRO_TAC (Str.global_replace (Str.regexp ",") ";" s);;
234
235 let assume statement lab tac (asl, w as gl) =
236   let t = parse_env_string (make_env gl) statement in
237   (DISJ_CASES_THEN (LABEL_TAC lab) (SPEC t EXCLUDED_MIDDLE) THENL
238   [ALL_TAC; FIRST_ASSUM MP_TAC THEN tac] THEN HYP SIMP_TAC lab []) gl;;
239
240 let eq_tac string tac =
241   if string = "Right" then CONV_TAC SYM_CONV THEN EQ_TAC THENL [tac; ALL_TAC]
242   else if string = "Left" then EQ_TAC THENL [tac; ALL_TAC]
243   else raise (Readable_fail
244     ("eq_tac requires " ^  string ^" to be either Left or Right"));;
245
246 let conj_tac string tac =
247   if string = "Right" then ONCE_REWRITE_TAC [CONJ_SYM] THEN
248     CONJ_TAC THENL [tac; ALL_TAC]
249   else if string = "Left" then CONJ_TAC THENL [tac; ALL_TAC]
250   else raise (Readable_fail
251     ("conj_tac requires " ^  string ^" to be either Left or Right"));;
252
253 let consider svars stm lab tac =
254   subgoal_THEN ("?"^ svars ^ ". "^ stm)
255     (DESTRUCT_TAC ("@"^ svars ^ "."^ lab)) THENL [tac; ALL_TAC];;
256
257 let case_split sDestruct tac listofDisj listofTac =
258   let disjunction = itlist
259     (fun s t -> if t = "" then "("^ s ^")" else "("^ s ^") \\/ "^ t)
260     listofDisj "" in
261   subgoal_TAC disjunction "" tac THEN
262   FIRST_X_ASSUM (DESTRUCT_TAC sDestruct) THENL listofTac;;
263
264 (* Following the HOL Light tutorial section "Towards more readable proofs."  *)
265
266 let fol = MESON_TAC;;
267 let rewrite = REWRITE_TAC;;
268 let simplify = SIMP_TAC;;
269 let set = SET_TAC;;
270 let rewriteR = GEN_REWRITE_TAC (RAND_CONV);;
271 let rewriteL = GEN_REWRITE_TAC (LAND_CONV);;
272 let rewriteI = GEN_REWRITE_TAC I;;
273 let rewriteRLDepth = GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o DEPTH_CONV);;
274 let TACtoThmTactic tac = fun  ths -> MAP_EVERY MP_TAC ths THEN tac;;
275 let arithmetic = TACtoThmTactic ARITH_TAC;;
276 let real_arithmetic = TACtoThmTactic REAL_ARITH_TAC;;
277 let num_ring = TACtoThmTactic (CONV_TAC NUM_RING);;
278 let real_ring = TACtoThmTactic (CONV_TAC REAL_RING);;
279
280 let ws = "[ \t\n]+";;
281 let ws0 = "[ \t\n]*";;
282
283 let StringRegexpEqual r s = Str.string_match r s 0 &&
284   s = Str.matched_string s;;
285
286 (* FindMatch sleft sright s                                                  *)
287 (* turns strings sleft and sright into regexps, recursively searches string  *)
288 (* s for matched pairs of substrings matching sleft and sright, and returns  *)
289 (* the position after the first substring matched by sright which is not     *)
290 (* paired with an sleft-matching substring.  Often here sleft ends with      *)
291 (* whitespace (ws) while sright begins with ws.  The "degenerate" case of    *)
292 (* X^ws^Y where X^ws matches sleft and ws^Y matches sright is handled by     *)
293 (* backing up a character after an sleft match if the last character is ws.  *)
294
295 let FindMatch sleft sright s =
296   let test = Str.regexp ("\("^ sleft ^"\|"^ sright ^"\)")
297   and left = Str.regexp sleft in
298   let rec FindMatchPosition s count =
299     if count = 1 then 0
300     else
301       try
302         ignore(Str.search_forward test s 0);
303         let TestMatch = Str.matched_group 1 s
304         and AfterTest = Str.match_end() in
305         let LastChar = Str.last_chars (Str.string_before s AfterTest) 1 in
306         let endpos =
307           if Str.string_match (Str.regexp ws) LastChar 0
308           then AfterTest - 1 else AfterTest in
309         let rest = Str.string_after s endpos
310         and increment =
311           if StringRegexpEqual left TestMatch then -1 else 1 in
312         endpos + (FindMatchPosition rest (count + increment))
313       with Not_found -> raise (Readable_fail
314         ("No matching right bracket operator "^ sright ^
315         " to left bracket operator "^ sleft ^" in "^ s)) in
316   FindMatchPosition s 0;;
317
318 (* FindSemicolon uses FindMatch to find the position before the next         *)
319 (* semicolon which is not a delimiter of a list.                             *)
320
321 let rec FindSemicolon s =
322   try
323     let rec FindMatchPosition s pos =
324       let start = Str.search_forward (Str.regexp ";\|\[") s pos  in
325       if Str.matched_string s = ";" then start
326       else
327         let rest = Str.string_after s (start + 1) in
328         let MatchingSquareBrace = FindMatch "\[" "\]" rest in
329         let newpos = start + 1 + MatchingSquareBrace in
330         FindMatchPosition s newpos in
331     FindMatchPosition s 0
332   with Not_found -> raise (Readable_fail ("No final semicolon in "^ s));;
333
334 (* FindCases uses FindMatch to take a string                                 *)
335 (* "suppose" proof_1 "end;" ... "suppose" proof_n "end;"                     *)
336 (* and return the list [proof_1; proof_2; ... ; proof_n].                    *)
337
338 let rec FindCases s =
339   let sleftCase, srightCase = ws^ "suppose"^ws, ws^ "end" ^ws0^ ";" in
340   if Str.string_match (Str.regexp sleftCase) s 0 then
341     let CaseEndRest = Str.string_after s (Str.match_end()) in
342     let PosAfterEnd = FindMatch sleftCase srightCase CaseEndRest in
343     let pos = Str.search_backward (Str.regexp srightCase)
344       CaseEndRest PosAfterEnd in
345     let case = Str.string_before CaseEndRest pos
346     and rest = Str.string_after CaseEndRest PosAfterEnd in
347     case :: (FindCases rest)
348   else [];;
349
350 (* StringToList uses FindSemicolon to turns a string into the list of        *)
351 (* substrings delimited by the semicolons which are not captured in lists.   *)
352
353 let rec StringToList s =
354   if StringRegexpEqual (Str.regexp ws0) s then [] else
355   if Str.string_match (Str.regexp "[^;]*;") s 0 then
356     let pos = FindSemicolon s in
357     let head = Str.string_before s pos in
358     head :: (StringToList (Str.string_after s (pos + 1)))
359   else [s];;
360
361 (* ExtractWsStringList string = (["l1"; "l2"; ...; "ln"], rest),             *)
362 (* if string = ws ^ "[l1; l2; ...; ln]" ^ rest.  Raises Not_found otherwise. *)
363
364 let ExtractWsStringList string =
365   if Str.string_match (Str.regexp (ws^ "\[")) string 0 then
366     let listRest = Str.string_after string (Str.match_end()) in
367     let RightBrace = FindMatch "\[" "\]" listRest in
368     let rest = Str.string_after listRest RightBrace
369     and list = Str.string_before listRest (RightBrace - 1) in
370     (StringToList list, rest)
371   else raise Not_found;;
372
373 (* theoremify string goal returns a pair  (thm, rest),                       *)
374 (* where thm is the first theorem found on string, using goal if needed, and *)
375 (* rest is the remainder of string.  Theoremify uses 3 helping functions:    *)
376 (* 1) CombTermThm_Term, which produces a combination of a term->thm          *)
377 (*      (e.g. ARITH_RULE) with a term,                                       *)
378 (* 2) CombThmlistTermThm_Thmlist_Term, which combines a thmlist->term->thm   *)
379 (*      (e.g. MESON) with a thmlist and a term, and                          *)
380 (* 3) CombTermlistThmThm_Termlist, which combines a termlist->thm->thm       *)
381 (*      (e.g. SPECL) with a termlist and a thm produced by theoremify.       *)
382 (* Similar functions CombThmtactic_Thm and CombThmlisttactic_Thmlist are     *)
383 (* used below, along with theoremify, by StringToTactic.                     *)
384
385 let CombTermThm_Term word rest gl =
386   let TermThm = exec_term_thm word in
387   try
388     let (stermlist, wsRest) = ExtractWsStringList rest in
389     if length stermlist = 1 then
390       let term = (parse_env_string (make_env gl)) (hd stermlist) in
391       (TermThm term,  wsRest)
392     else raise (Readable_fail ("term->thm "^ word
393     ^" not followed by length 1 term list, but instead the list \n["^
394     String.concat ";" stermlist ^"]"))
395   with Not_found -> raise (Readable_fail ("term->thm "^ word
396   ^" not followed by term list, but instead \n"^ rest));;
397
398 let rec theoremify string gl =
399   if Str.string_match (Str.regexp (ws^ "\([^][ \t\n]+\)")) string 0 then
400     let word = Str.matched_group 1 string
401     and rest = Str.string_after string (Str.match_end()) in
402     if word = "-" then (snd (hd (fst gl)), rest) else
403     try (exec_thm word, rest)
404     with _ ->
405     try (assoc word (fst gl), rest)
406     with _ ->
407     try firstPairMult (exec_thm_thm word) (theoremify rest gl)
408     with _ ->
409     try CombTermThm_Term word rest gl
410     with Noparse ->
411     try CombThmlistTermThm_Thmlist_Term word rest gl
412     with Noparse ->
413     try CombTermlistThmThm_Termlist word rest gl
414     with Noparse -> raise (Readable_fail ("Not a theorem:\n"^ string))
415   else raise (Readable_fail ("Empty theorem:\n"^ string))
416 and
417 firstPairMult f (a, b) = (f a, b)
418 and
419 CombTermlistThmThm_Termlist word rest gl =
420   let TermlistThmThm = exec_termlist_thm_thm word in
421   try
422     let (stermlist, WsThm) = ExtractWsStringList rest in
423     let termlist = map (parse_env_string (make_env gl)) stermlist in
424     firstPairMult (TermlistThmThm termlist) (theoremify WsThm gl)
425   with Not_found -> raise (Readable_fail ("termlist->thm->thm "^ word
426   ^"\n not followed by term list in\n"^ rest))
427 and
428 CombThmlistTermThm_Thmlist_Term word rest gl =
429   let thm_create sthm =
430     let (thm, rest) = theoremify (" "^ sthm) gl in
431     if rest = "" then thm
432     else raise (Readable_fail ("an argument of thmlist->term->thm "^ word ^
433     "\n is not a theorem, but instead \n"^ sthm)) in
434   let ThmlistTermThm = exec_thmlist_term_thm word in
435   try
436     let (stermlist, wsTermRest) = ExtractWsStringList rest in
437     let thmlist = map thm_create stermlist in
438     if Str.string_match (Str.regexp (ws^ "\[")) wsTermRest 0 then
439       let termRest = Str.string_after wsTermRest (Str.match_end()) in
440       let RightBrace = FindMatch "\[" "\]" termRest in
441       let rest = Str.string_after termRest RightBrace
442       and sterm = Str.string_before termRest (RightBrace - 1) in
443       let term = parse_env_string (make_env gl) sterm in
444       (ThmlistTermThm thmlist term, rest)
445     else raise (Readable_fail ("thmlist->term->thm "^ word
446       ^" followed by list of theorems ["^ String.concat ";" stermlist ^"]
447       not followed by term in\n"^ wsTermRest))
448   with Not_found -> raise (Readable_fail ("thmlist->term->thm "^ word
449   ^" not followed by thm list in\n"^ rest));;
450
451 let CombThmtactic_Thm step =
452   if Str.string_match (Str.regexp (ws^ "\([a-zA-Z0-9_]+\)")) step 0 then
453     let sthm_tactic = Str.matched_group 1 step
454     and sthm = Str.string_after step (Str.match_end()) in
455     let thm_tactic = exec_thmtactic sthm_tactic in
456     fun gl ->
457       let (thm, rest) = theoremify sthm gl in
458       if rest = "" then thm_tactic thm gl
459       else raise (Readable_fail ("thm_tactic "^ sthm_tactic
460       ^" not followed by a theorem, but instead\n"^ sthm))
461   else raise Not_found;;
462
463 let CombThmlisttactic_Thmlist step =
464   let rec makeThmListAccum string list gl =
465     if StringRegexpEqual (Str.regexp ws0) string then list else
466     let (thm, rest) = theoremify string gl in
467     makeThmListAccum rest (thm :: list) gl in
468   if Str.string_match (Str.regexp (ws^ "\([a-zA-Z0-9_]+\)")) step 0 then
469     let ttac = exec_thmlist_tactic (Str.matched_group 1 step)
470     and LabThmString = Str.string_after step (Str.match_end()) in
471     fun gl ->
472       let LabThmList =  List.rev (makeThmListAccum LabThmString [] gl) in
473       ttac LabThmList gl
474   else raise Not_found;;
475
476 (* StringToTactic uses regexp functions from the Str library to transform a  *)
477 (* string into a tactic.  The allowable tactics are written in BNF form as   *)
478 (*                                                                           *)
479 (* Tactic := ALL_TAC | Tactic THEN Tactic | thm->tactic Thm |                *)
480 (*   one-word-tactic (e.g. ARITH_TAC) | thmlist->tactic Thm-list |           *)
481 (*   intro_TAC string | exists_TAC term | X_genl_TAC term-list |             *)
482 (*   case_split string Tactic statement-list Tactic-list |                   *)
483 (*   consider variable-list statement label Tactic |                         *)
484 (*   eq_tac (Right | Left) Tactic | conj_tac (Right | Left) Tactic |         *)
485 (*   (assume | subgoal_TAC) statement label Tactic                           *)
486 (*                                                                           *)
487 (* Thm := theorem-name | label | - [i.e. last assumption] | thm->thm Thm |   *)
488 (*   term->thm term | thmlist->term->thm Thm-list term |                     *)
489 (*   termlist->thm->thm term-list Thm                                        *)
490 (*                                                                           *)
491 (* The string proofs allowed by StringToTactic are written in BNF form as    *)
492 (*                                                                           *)
493 (* Proof := Proof THEN Proof | case_split destruct_string ByProofQed         *)
494 (*   suppose statement; Proof end; ... suppose statement; Proof end; |       *)
495 (*   OneStepProof; | consider variable-list statement [label] ByProofQed |   *)
496 (*   eq_tac [Right|Left] ByProofQed | conj_tac [Right|Left] ByProofQed |     *)
497 (*   (assume | ) statement [label] ByProofQed                                *)
498 (*                                                                           *)
499 (* OneStepProof := one-word-tactic | thm->tactic Thm | intro_TAC string |    *)
500 (*   exists_TAC term-string | X_genl_TAC variable-string-list |              *)
501 (*   thmlist->tactic Thm-list                                                *)
502 (*                                                                           *)
503 (* ByProofQed := by OneStepProof; | proof Proof Proof ...  Proof qed;        *)
504 (*                                                                           *)
505 (* theorem is a version of prove based on the miz3.ml thm, with argument     *)
506 (* statement ByProofQed                                                      *)
507
508 let rec StringToTactic s =
509   if StringRegexpEqual (Str.regexp ws0) s then ALL_TAC
510   else
511     try makeCaseSplit s
512     with _ ->
513     let pos = FindSemicolon s in
514     let step, rest = Str.string_before s pos, Str.string_after s (pos + 1) in
515     try
516       let tactic = StepToTactic step in
517       tactic THEN StringToTactic rest
518     with Not_found ->
519     let (tactic, rest) = BigStepToTactic s step in
520     tactic THEN StringToTactic rest
521 and
522 GetProof ByProof s =
523   if ByProof = "by" then
524     let pos = FindSemicolon s in
525     let step, rest = Str.string_before s pos, Str.string_after s (pos + 1) in
526     (StepToTactic step, rest)
527   else
528     let pos_after_qed = FindMatch (ws^"proof"^ws) (ws^"qed"^ws0^";") s in
529     let pos = Str.search_backward (Str.regexp "qed") s pos_after_qed in
530     let proof = StringToTactic (Str.string_before s pos) in
531     (proof, Str.string_after s pos_after_qed)
532 and
533 makeCaseSplit s =
534   if Str.string_match (Str.regexp (ws^ "case_split" ^ws^ "\([^;]+\)" ^ws^
535     "\(by\|proof\)" ^ws)) s 0 then
536     let sDestruct = Str.matched_group 1 s
537     and (proof, rest) = GetProof (Str.matched_group 2 s)
538       (Str.string_after s (Str.group_end 2))
539     and SplitAtSemicolon case =
540       let pos = FindSemicolon case in
541       [Str.string_before case pos; Str.string_after case (pos + 1)] in
542     let list2Case = map SplitAtSemicolon (FindCases rest) in
543     let listofDisj = map hd list2Case
544     and listofTac = map (StringToTactic o hd o tl) list2Case in
545     case_split sDestruct proof listofDisj listofTac
546   else raise Not_found
547 and
548 StepToTactic step =
549   try
550     if StringRegexpEqual (Str.regexp (ws^ "\([^ \t\n]+\)" ^ws0)) step then
551       exec_tactic (Str.matched_group 1 step)
552     else raise Not_found
553   with _ ->
554   try CombThmtactic_Thm step
555   with _ ->
556   try CombThmlisttactic_Thmlist step
557   with _ ->
558   if Str.string_match (Str.regexp (ws^ "intro_TAC" ^ws)) step 0 then
559     let intro_string = Str.string_after step (Str.match_end()) in
560     intro_TAC intro_string
561   else if Str.string_match (Str.regexp (ws^ "exists_TAC" ^ws)) step 0 then
562     let exists_string = Str.string_after step (Str.match_end()) in
563     exists_TAC exists_string
564   else if Str.string_match (Str.regexp (ws^ "X_genl_TAC" ^ws)) step 0 then
565     let genl_string = Str.string_after step (Str.match_end()) in
566     let svarlist = Str.split (Str.regexp ws) genl_string in
567     X_genl_TAC svarlist
568   else raise Not_found
569 and
570 BigStepToTactic s step =
571   if Str.string_match (Str.regexp (ws^ "consider" ^ws^ "\(\(.\|\n\)+\)" ^ws^
572     "such" ^ws^ "that" ^ws^ "\(\(.\|\n\)+\)" ^ws^ "\[\(\(.\|\n\)*\)\]" ^ws^
573     "\(by\|proof\)" ^ws)) step 0 then
574     let vars, t = Str.matched_group 1 step, Str.matched_group 3 step
575     and lab = Str.matched_group 5 step
576     and KeyWord, endKeyWord = Str.matched_group 7 step, (Str.group_end 7) in
577     let (proof, rest) = GetProof KeyWord (Str.string_after s endKeyWord) in
578     (consider vars t lab proof, rest)
579   else
580     try
581       let start = Str.search_forward (Str.regexp
582         (ws^ "\[\([^]]*\)\]" ^ws^ "\(by\|proof\)" ^ws)) step 0 in
583       let statement = Str.string_before step start
584       and lab = Str.matched_group 1 step
585       and KeyWord = Str.matched_group 2 step
586       and AfterWord = Str.string_after s (Str.group_end 2) in
587       let (proof, rest) = GetProof KeyWord AfterWord in
588       if StringRegexpEqual (Str.regexp (ws^ "eq_tac")) statement
589       then (eq_tac lab proof, rest)
590       else if StringRegexpEqual (Str.regexp (ws^ "conj_tac")) statement
591       then (conj_tac lab proof, rest)
592       else if
593         Str.string_match (Str.regexp (ws^ "\(assume\)" ^ws)) statement 0
594       then
595         let statement = Str.string_after statement (Str.match_end()) in
596         (assume statement lab proof, rest)
597       else (subgoal_TAC statement lab proof, rest)
598     with Not_found -> raise (Readable_fail
599     ("Can't parse as a Proof:\n"^ step));;
600
601 let theorem s =
602   let s = CleanMathFontsForHOL_Light s in
603   try
604     let start = Str.search_forward (Str.regexp
605       (ws^ "proof\(" ^ws^ "\(.\|\n\)*\)" ^ws ^ "qed" ^ws0^ ";" ^ws0)) s 0 in
606     let thm = Str.string_before s start
607     and proof = Str.matched_group 1 s
608     and rest = Str.string_after s (Str.match_end()) in
609     if rest = "" then prove (parse_env_string [] thm, StringToTactic proof)
610     else raise (Readable_fail
611       ("Trailing garbage after the proof...qed:\n" ^ rest))
612   with Not_found ->
613   try
614     let start = Str.search_forward (Str.regexp (ws^ "by")) s 0 in
615     let thm = Str.string_before s start
616     and proof = Str.string_after s (Str.match_end()) in
617     try
618       prove (parse_env_string [] thm, StepToTactic proof)
619     with Not_found -> raise (Readable_fail ("Not a proof:\n" ^ proof))
620   with Not_found -> raise (Readable_fail
621     ("Missing initial \"proof\", \"by\", or final \"qed;\" in\n" ^ s));;
622
623 let interactive_goal s =
624   let thm = CleanMathFontsForHOL_Light s in
625   g (parse_env_string [] thm);;
626
627 let interactive_proof s =
628   let proof = CleanMathFontsForHOL_Light s in
629   e (StringToTactic proof);;
630
631 (* Two examples illustrating intro_TAC, eq_tac, exists_TAC MP_TAC and SPECL, *)
632 (* then a port of the HOL Light tutorial proof that sqrt 2 is irrational.    *)
633
634 let SKOLEM_THM_GEN = theorem `;
635   ∀P R. (∀x. P x ⇒ ∃y. R x y)  ⇔  ∃f. ∀x. P x ⇒ R x (f x)
636
637   proof
638     intro_TAC ∀P R;
639     eq_tac     [Right] by fol;
640     intro_TAC H1;
641     exists_TAC λx. @y. R x y;
642     fol H1;
643   qed;
644 `;;
645
646 let MOD_MOD_REFL = theorem `;
647   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
648
649   proof
650     intro_TAC !m n, H1;
651     MP_TAC SPECL [m; n; 1] MOD_MOD;
652     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
653   qed;
654 `;;
655
656 let NSQRT_2 = theorem `;
657   ∀p q. p * p = 2 * q * q  ⇒  q = 0
658
659   proof
660     MATCH_MP_TAC num_WF;
661     intro_TAC ∀p, A, ∀q, B;
662     EVEN(p * p) ⇔ EVEN(2 * q * q)     [] by fol B;
663     EVEN(p)     [] by fol - EVEN_DOUBLE EVEN_MULT;
664     consider m such that p = 2 * m     [C] by fol - EVEN_EXISTS;
665     case_split qp | pq by arithmetic;
666     suppose q < p;
667       q * q = 2 * m * m ⇒ m = 0     [] by fol qp A;
668       num_ring - B C;
669     end;
670     suppose p <= q;
671       p * p <= q * q     [] by fol - LE_MULT2;
672       q * q = 0     [] by arithmetic - B;
673     num_ring -;
674     end;
675   qed;
676 `;;
677
678 (* The following interactive version of the above proof shows a feature of   *)
679 (* proof/qed and case_split/suppose.  You can evaluate an incomplete proof   *)
680 (* of a statement in an interactive_proof and complete the proof afterward,  *)
681 (* as indicated below.  The "suppose" clauses of a case_split can also be    *)
682 (* incomplete.  Do not include code below the incomplete proof or case_split *)
683 (* in an interactive_proof body, for the usual THEN vs THENL reason.         *)
684
685 interactive_goal `;∀p q. p * p = 2 * q * q  ⇒  q = 0
686 `;;
687 interactive_proof `;
688     MATCH_MP_TAC num_WF;
689     intro_TAC ∀p, A, ∀q, B;
690     EVEN(p * p) ⇔ EVEN(2 * q * q)     [] proof  qed;
691 `;;
692 interactive_proof `;
693       fol B;
694 `;;
695 interactive_proof `;
696     EVEN(p)     [] by fol - EVEN_DOUBLE EVEN_MULT;
697     consider m such that p = 2 * m     [C] proof fol - EVEN_EXISTS; qed;
698 `;;
699 interactive_proof `;
700     case_split qp | pq by arithmetic;
701     suppose q < p;
702     end;
703     suppose p <= q;
704     end;
705 `;;
706 interactive_proof `;
707       q * q = 2 * m * m ⇒ m = 0     [] by fol qp A;
708       num_ring - B C;
709 `;;
710 interactive_proof `;
711       p * p <= q * q     [] by fol - LE_MULT2;
712       q * q = 0     [] by arithmetic - B;
713       num_ring -;
714 `;;
715 let NSQRT_2 = top_thm();;
716
717 (* An port from arith.ml uses by instead of proof...qed; in a short proof:   *)
718
719 let EXP_2 = theorem `;
720   ∀n:num. n EXP 2 = n * n
721   by rewrite BIT0_THM BIT1_THM EXP EXP_ADD MULT_CLAUSES ADD_CLAUSES`;;
722
723 (* An example using GSYM, ARITH_RULE, MESON and GEN_REWRITE_TAC, reproving   *)
724 (* the binomial theorem from sec 13.1--2 of the HOL Light tutorial.          *)
725
726 let binom = define
727  `(!n. binom(n,0) = 1) /\
728   (!k. binom(0,SUC(k)) = 0) /\
729   (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
730
731 let BINOM_LT = theorem `;
732   ∀n k. n < k  ⇒  binom(n,k) = 0
733
734   proof
735     INDUCT_TAC; INDUCT_TAC;
736     rewrite binom ARITH LT_SUC LT;
737     ASM_SIMP_TAC ARITH_RULE [n < k ==> n < SUC(k)] ARITH;
738   qed;
739 `;;
740
741 let BINOMIAL_THEOREM = theorem `;
742   ∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
743
744   proof
745     ∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i))     [Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
746     MATCH_MP_TAC num_INDUCTION;
747     simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
748     intro_TAC ∀n, nThm;
749     rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL ADD_ASSOC;
750     rewriteR ADD_SYM;
751     rewriteRLDepth SUB_SUC EXP;
752     rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] [1 = binom(n, 0)] GSYM Nsum0SUC;
753     simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n  ∧  0 <= SUC n] LT BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
754     simplify ARITH_RULE [k <= n  ⇒  SUC n - k = SUC(n - k)] EXP MULT_AC;
755   qed;
756 `;;