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 `;;