1(* 2 * Formalized Lambek Calculus in Higher Order Logic (HOL4) 3 * 4 * (based on https://github.com/coq-contribs/lambek) 5 * 6 * Copyright 2016-2017 University of Bologna, Italy (Author: Chun Tian) 7 *) 8 9(* This program is free software; you can redistribute it and/or *) 10(* modify it under the terms of the GNU Lesser General Public License *) 11(* as published by the Free Software Foundation; either version 2.1 *) 12(* of the License, or (at your option) any later version. *) 13(* *) 14(* This program is distributed in the hope that it will be useful, *) 15(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) 16(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) 17(* GNU General Public License for more details. *) 18(* *) 19(* You should have received a copy of the GNU Lesser General Public *) 20(* License along with this program; if not, write to the Free *) 21(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) 22(* 02110-1301 USA *) 23 24open HolKernel Parse boolLib bossLib; 25 26open pred_setTheory relationTheory pairTheory listTheory prim_recTheory arithmeticTheory 27open stringTheory integerTheory LambekTheory CutFreeTheory; 28 29local 30 val PAT_X_ASSUM = PAT_ASSUM; 31 val qpat_x_assum = Q.PAT_ASSUM; 32 open Tactical 33in 34 (* Backward compatibility with Kananaskis 11 *) 35 val PAT_X_ASSUM = PAT_X_ASSUM; 36 val qpat_x_assum = qpat_x_assum; 37 38 (* Tacticals for better expressivity *) 39 fun fix ts = MAP_EVERY Q.X_GEN_TAC ts; (* from HOL Light *) 40 fun set ts = MAP_EVERY Q.ABBREV_TAC ts; (* from HOL mizar mode *) 41 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) 42end; 43 44val _ = new_theory "Example"; 45 46(* check if a given sentence has category s *) 47val sentence_def = Define ` 48 sentence words = arrow NL words (At "S")`; 49 50(******************************************************************************) 51(* *) 52(* Example 1: check simple sentences in (arrow NL) *) 53(* *) 54(******************************************************************************) 55 56(* in most simple cases, we have one-one mapping between words and their syntactic categories *) 57val John = ``At "np"``; 58val works = ``Backslash (At "np") (At "S")``; 59 60val John_works = ``(Dot ^John ^works)``; 61 62(* "John works" is a sentence, manual proof *) 63val John_works_thm = store_thm ( 64 "John_works_thm", ``sentence ^John_works``, 65 REWRITE_TAC [sentence_def] 66 >> MATCH_MP_TAC gamma' 67 >> REWRITE_TAC [one]); 68 69(* same proof, done automatically *) 70val John_works_thm2 = store_thm ( 71 "John_works_thm2", ``sentence ^John_works``, 72 REWRITE_TAC [sentence_def] 73 >> PROVE_TAC [arrow_rules]); 74 75local 76 val before_tac = REWRITE_TAC [sentence_def] 77 and after_tac = PROVE_TAC [arrow_rules] 78in 79 fun check_arrow tm = 80 prove (tm, before_tac >> after_tac) 81end; 82 83val John_works_thm3 = save_thm ( 84 "John_works_thm3", check_arrow ``sentence ^John_works``); 85 86(******************************************************************************) 87(* *) 88(* Example 2: check complex sentences in Natural Deduction *) 89(* *) 90(******************************************************************************) 91 92val Ex1 = store_thm ("Ex1", (* sn/n . n |- sn *) 93 ``natDed NL_Sequent (OneForm (Dot (Slash (At "sn") (At "n")) (At "n"))) (At "sn")``, 94 MATCH_MP_TAC DotElim 95 >> ONCE_REWRITE_TAC [replace_cases] 96 >> RW_TAC std_ss [Term_11, Term_distinct] 97 >> EXISTS_TAC ``Slash (At "sn") (At "n")`` 98 >> EXISTS_TAC ``At "n"`` 99 >> RW_TAC std_ss [NatAxiom] 100 >> MATCH_MP_TAC SlashElim 101 >> EXISTS_TAC ``At "n"`` 102 >> RW_TAC std_ss [NatAxiom]); 103 104val Ex2 = store_thm ("Ex2", (* sn . (((sn \ n) / S) . S)) |- n *) 105 ``natDed NL_Sequent 106 (OneForm (Dot (At "sn") (Dot (Slash (Backslash (At "sn") (At "n")) (At "S")) (At "S")))) 107 (At "n")``, 108 MATCH_MP_TAC DotElim 109 >> ONCE_REWRITE_TAC [replace_cases] 110 >> RW_TAC std_ss [Term_11, Term_distinct] 111 >> EXISTS_TAC ``At "sn"`` 112 >> EXISTS_TAC ``Dot (Slash (Backslash (At "sn") (At "n")) (At "S")) (At "S")`` 113 >> RW_TAC std_ss [NatAxiom] 114 >> MATCH_MP_TAC BackslashElim 115 >> EXISTS_TAC ``At "sn"`` 116 >> RW_TAC std_ss [NatAxiom] 117 >> MATCH_MP_TAC DotElim 118 >> ONCE_REWRITE_TAC [replace_cases] 119 >> RW_TAC std_ss [Term_11, Term_distinct] 120 >> EXISTS_TAC ``Slash (Backslash (At "sn") (At "n")) (At "S")`` 121 >> EXISTS_TAC ``At "S"`` 122 >> RW_TAC std_ss [NatAxiom] 123 >> MATCH_MP_TAC SlashElim 124 >> EXISTS_TAC ``At "S"`` 125 >> RW_TAC std_ss [NatAxiom]); 126 127(******************************************************************************) 128(* *) 129(* Example 3: check complex sentences in Natural Deduction *) 130(* *) 131(******************************************************************************) 132 133val Kevin = ``At "np"``; 134val talks = ``Slash (Backslash (At "np") (At "S")) (At "pp")``; (* (np \ s) / pp *) 135 136val to = ``Slash (At "pp") (At "np")``; 137 138val himself = (* ((np \ s) / np) \ (np \ s) *) 139 ``Backslash (Slash (Backslash (At "np") (At "S")) (At "np")) 140 (Backslash (At "np") (At "S"))``; 141 142(* (Kevin, ((talks, to), himself)) *) 143val Kevin_talks_to_himself = ``Dot ^Kevin (Dot (Dot ^talks ^to) ^himself)``; 144 145(* this time automatic proof search by arrow doesn't work: 146 147> check_arrow ``sentence ^Kevin_talks_to_himself``; 148Meson search level: ................Exception- Interrupt raised 149 *) 150 151(* 152val Kevin_talks_to_himself_thm = store_thm ( 153 "Kevin_talks_to_himself_thm", ``arrow NL ^Kevin_talks_to_himself (At "S")``, 154 >> ); 155*) 156 157(******************************************************************************) 158(* *) 159(* Example 4: "cosa guarda passare" in bot natDed and gentzenSequent *) 160(* *) 161(******************************************************************************) 162 163(* a basic category type, but how to use it? *) 164(* val _ = Datatype `Lexicon = <| word : string ; category : 'a Form |>`; *) 165 166val cosa = ``(At "S") / ((At "S") / (At "np"))``; 167val guarda = ``(At "S") / (At "inf")``; 168val passare = ``(At "inf") / (At "np")``; 169val il = ``(At "np") / (At "n")``; 170val treno = ``At "n"``; 171 172(* 173S/(S/np) * (S/inf * inf/np) --> S 174S/(S/np) --> S / (S/inf * inf/np) 1751. S/inf * inf/np --> S/np 176S/(S/np) * S/np --> S 177S/(S/np) --> S/(S/np) 178val cosa_guarda_passare_arrow = store_thm ( 179 "cosa_guarda_passare_arrow", 180 ``arrow L (Dot ^cosa (Dot ^guarda ^passare)) (At "S")``, 181); 182 *) 183 184(* Natural Deduction for Lambek Calculus: 185 186 inf/np |- inf/np np |- np 187 ----------------------------- /e 188 S/inf |- S/inf inf/np, np |- inf 189 ----------------------------------- /e 190 S/inf, (inf/np, np) |- S 191 -------------------------- L_Sequent 192 (S/inf, inf/np), np |- S 193 -------------------------- /i 194 S/(S/np) |- S/(S/np) S/inf, inf/np |- S/np 195------------------------------------------------ /e 196 S/(S/np), (S/inf, inf/np) |- S 197------------------------------------ Lex 198("cosa", ("guarda", "passare")) |- S 199 200 *) 201val cosa_guarda_passare_natDed = store_thm ( 202 "cosa_guarda_passare_natDed", 203 ``natDed L_Sequent (Comma (OneForm ^cosa) (Comma (OneForm ^guarda) (OneForm ^passare))) 204 (At "S")``, 205 MATCH_MP_TAC SlashElim 206 >> EXISTS_TAC ``(At "S") / (At "np")`` (* guess 1 *) 207 >> CONJ_TAC (* 2 sub-goals here *) 208 >| [ (* goal 1 *) 209 REWRITE_TAC [NatAxiom], 210 (* goal 2 *) 211 MATCH_MP_TAC SlashIntro \\ 212 MATCH_MP_TAC NatExtSimpl \\ 213 EXISTS_TAC ``(Comma (OneForm (At "S" / At "inf")) 214 (Comma (OneForm (At "inf" / At "np")) (OneForm (At "np"))))`` \\ 215 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 216 MATCH_MP_TAC SlashElim \\ 217 EXISTS_TAC ``At "inf"`` \\ (* guess 2 *) 218 CONJ_TAC >| (* 2 sub-goals here *) 219 [ (* goal 2.1 *) 220 REWRITE_TAC [NatAxiom], 221 (* goal 2.2 *) 222 MATCH_MP_TAC SlashElim \\ 223 EXISTS_TAC ``At "np"`` \\ (* guess 3 *) 224 REWRITE_TAC [NatAxiom] ] ]); 225 226(* Lambek's Sequent Calculus: 227 228 S |- S inf |- inf 229 --------------------- /L 230 S/inf, inf |- S np |- np 231 -------------------------------- /L 232 S/inf, (inf/np, np) |- S 233 -------------------------- L_Sequent 234 (S/inf, inf/np), np |- S 235 ----------------------------- /R 236 S |- S S/inf, inf/np |- S/np 237-------------------------------------- /L 238 S/(S/np), (S/inf, inf/np) |- S 239------------------------------------ Lex 240("cosa", ("guarda", "passare")) |- S 241 242 *) 243val cosa_guarda_passare_gentzenSequent = store_thm ( 244 "cosa_guarda_passare_gentzenSequent", 245 ``gentzenSequent L_Sequent (Comma (OneForm ^cosa) (Comma (OneForm ^guarda) (OneForm ^passare))) 246 (At "S")``, 247 MATCH_MP_TAC LeftSlashSimpl 248 >> CONJ_TAC (* 2 sub-goals here *) 249 >| [ (* goal 1 *) 250 MATCH_MP_TAC RightSlash \\ 251 MATCH_MP_TAC SeqExtSimpl \\ 252 EXISTS_TAC ``(Comma (OneForm (At "S" / At "inf")) 253 (Comma (OneForm (At "inf" / At "np")) (OneForm (At "np"))))`` \\ 254 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 255 MATCH_MP_TAC LeftSlashSimpl \\ 256 CONJ_TAC >| (* 2 sub-goals here *) 257 [ (* goal 1.1 *) 258 MATCH_MP_TAC LeftSlashSimpl \\ 259 REWRITE_TAC [SeqAxiom], 260 (* goal 1.2 *) 261 REWRITE_TAC [SeqAxiom] ], 262 (* goal 2 *) 263 REWRITE_TAC [SeqAxiom] ]); 264 265val r0 = 266 ``(Unf (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 267 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 268 (At "S")))``; 269 270val r1 = 271 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 272 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 273 (At "S")) 274 LeftSlash 275 [ (Unf (Sequent L_Sequent (OneForm (At "S")) (At "S"))) ; 276 (Unf (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 277 (At "S" / At "np"))) ])``; 278 279val r0_to_r1 = store_thm ( 280 "r0_to_r1", ``derivOne ^r0 ^r1``, 281 MATCH_MP_TAC derivLeftSlash 282 >> EXISTS_TAC ``At "S"`` 283 >> REWRITE_TAC [replaceRoot]); 284 285val r0_to_r1' = store_thm ( 286 "r0_to_r1'", ``deriv ^r0 ^r1``, 287 MATCH_MP_TAC derivDerivOne 288 >> REWRITE_TAC [r0_to_r1]); 289 290val r0_to_r1'' = store_thm ( 291 "r0_to_r1''", ``Deriv ^r0 ^r1``, 292 REWRITE_TAC [Deriv_def] 293 >> MATCH_MP_TAC RTC_SINGLE 294 >> REWRITE_TAC [r0_to_r1']); 295 296val r2 = 297 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 298 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 299 (At "S")) 300 LeftSlash 301 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) 302 SeqAxiom []) ; 303 (Unf (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 304 (At "S" / At "np"))) ])``; 305 306val r1_to_r2 = store_thm ( 307 "r1_to_r2", ``deriv ^r1 ^r2``, 308 MATCH_MP_TAC derivLeft 309 >> MATCH_MP_TAC derivDerivOne 310 >> REWRITE_TAC [derivSeqAxiom]); 311 312val r3 = 313 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 314 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 315 (At "S")) 316 LeftSlash 317 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) 318 SeqAxiom []) ; 319 (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 320 (At "S" / At "np")) 321 RightSlash 322 [ (Unf (Sequent L_Sequent (Comma (Comma (OneForm (At "S" / At "inf")) 323 (OneForm (At "inf" / At "np"))) 324 (OneForm (At "np"))) 325 (At "S"))) ]) ])``; 326 327val r2_to_r3 = store_thm ( 328 "r2_to_r3", ``deriv ^r2 ^r3``, 329 MATCH_MP_TAC derivRight 330 >> MATCH_MP_TAC derivDerivOne 331 >> REWRITE_TAC [derivRightSlash]); 332 333val r4 = 334 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 335 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 336 (At "S")) 337 LeftSlash 338 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) 339 SeqAxiom []) ; 340 (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 341 (At "S" / At "np")) 342 RightSlash 343 [ (Der (Sequent L_Sequent (Comma (Comma (OneForm (At "S" / At "inf")) 344 (OneForm (At "inf" / At "np"))) 345 (OneForm (At "np"))) 346 (At "S")) 347 SeqExt 348 [ (Unf (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 349 (Comma (OneForm (At "inf" / At "np")) 350 (OneForm (At "np")))) 351 (At "S"))) ]) ]) ])``; 352 353val r3_to_r4 = store_thm ( 354 "r3_to_r4", ``deriv ^r3 ^r4``, 355 MATCH_MP_TAC derivRight 356 >> MATCH_MP_TAC derivOne 357 >> MATCH_MP_TAC derivDerivOne 358 >> MATCH_MP_TAC derivSeqExt 359 >> EXISTS_TAC ``(Comma (OneForm (At "S" / At "inf")) 360 (Comma (OneForm (At "inf" / At "np")) (OneForm (At "np"))))`` 361 >> EXISTS_TAC ``(Comma (Comma (OneForm (At "S" / At "inf")) 362 (OneForm (At "inf" / At "np"))) 363 (OneForm (At "np")))`` 364 >> REWRITE_TAC [replaceRoot, L_Sequent_rules]); 365 366val r5 = 367 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 368 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 369 (At "S")) 370 LeftSlash 371 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) 372 SeqAxiom []) ; 373 (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 374 (At "S" / At "np")) 375 RightSlash 376 [ (Der (Sequent L_Sequent (Comma (Comma (OneForm (At "S" / At "inf")) 377 (OneForm (At "inf" / At "np"))) 378 (OneForm (At "np"))) 379 (At "S")) 380 SeqExt 381 [ (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 382 (Comma (OneForm (At "inf" / At "np")) 383 (OneForm (At "np")))) 384 (At "S")) 385 LeftSlash 386 [ (Unf (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 387 (OneForm (At "inf"))) 388 (At "S"))) ; 389 (Unf (Sequent L_Sequent (OneForm (At "np")) (At "np"))) ]) ]) ]) ])``; 390 391val r4_to_r5 = store_thm ( 392 "r4_to_r5", ``deriv ^r4 ^r5``, 393 MATCH_MP_TAC derivRight 394 >> MATCH_MP_TAC derivOne 395 >> MATCH_MP_TAC derivOne 396 >> MATCH_MP_TAC derivDerivOne 397 >> MATCH_MP_TAC derivLeftSlash 398 >> EXISTS_TAC ``At "inf"`` 399 >> MATCH_MP_TAC replaceRight 400 >> REWRITE_TAC [replaceRoot]); 401 402val r6 = 403 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 404 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 405 (At "S")) 406 LeftSlash 407 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) 408 SeqAxiom []) ; 409 (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 410 (At "S" / At "np")) 411 RightSlash 412 [ (Der (Sequent L_Sequent (Comma (Comma (OneForm (At "S" / At "inf")) 413 (OneForm (At "inf" / At "np"))) 414 (OneForm (At "np"))) 415 (At "S")) 416 SeqExt 417 [ (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 418 (Comma (OneForm (At "inf" / At "np")) 419 (OneForm (At "np")))) 420 (At "S")) 421 LeftSlash 422 [ (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 423 (OneForm (At "inf"))) 424 (At "S")) 425 LeftSlash 426 [ (Unf (Sequent L_Sequent (OneForm (At "S")) (At "S"))) ; 427 (Unf (Sequent L_Sequent (OneForm (At "inf")) (At "inf"))) ]) ; 428 (Unf (Sequent L_Sequent (OneForm (At "np")) (At "np"))) ]) ]) ]) ])``; 429 430val r5_to_r6 = store_thm ( 431 "r5_to_r6", ``deriv ^r5 ^r6``, 432 MATCH_MP_TAC derivRight 433 >> MATCH_MP_TAC derivOne 434 >> MATCH_MP_TAC derivOne 435 >> MATCH_MP_TAC derivLeft 436 >> MATCH_MP_TAC derivDerivOne 437 >> MATCH_MP_TAC derivLeftSlash 438 >> EXISTS_TAC ``At "S"`` 439 >> REWRITE_TAC [replaceRoot]); 440 441val r_final = 442 ``(Der (Sequent L_Sequent (Comma (OneForm (At "S" / (At "S" / At "np"))) 443 (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np")))) 444 (At "S")) 445 LeftSlash 446 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) 447 SeqAxiom []) ; 448 (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) (OneForm (At "inf" / At "np"))) 449 (At "S" / At "np")) 450 RightSlash 451 [ (Der (Sequent L_Sequent (Comma (Comma (OneForm (At "S" / At "inf")) 452 (OneForm (At "inf" / At "np"))) 453 (OneForm (At "np"))) 454 (At "S")) 455 SeqExt 456 [ (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 457 (Comma (OneForm (At "inf" / At "np")) 458 (OneForm (At "np")))) 459 (At "S")) 460 LeftSlash 461 [ (Der (Sequent L_Sequent (Comma (OneForm (At "S" / At "inf")) 462 (OneForm (At "inf"))) 463 (At "S")) 464 LeftSlash 465 [ (Der (Sequent L_Sequent (OneForm (At "S")) (At "S")) SeqAxiom []) ; 466 (Der (Sequent L_Sequent (OneForm (At "inf")) (At "inf")) SeqAxiom []) ]) ; 467 (Der (Sequent L_Sequent (OneForm (At "np")) (At "np")) SeqAxiom []) ]) ]) ]) ])``; 468 469val r_finished = store_thm ( 470 "r_finished", ``Proof ^r_final``, 471 PROVE_TAC [Proof_rules]); 472 473val r_degree_zero = store_thm ( 474 "r_degree_zero", ``degreeProof ^r_final = 0``, 475 REWRITE_TAC [degreeProof_def] 476 >> rw [MAX_EQ_0]); 477 478val r6_to_final = store_thm ( 479 "r6_to_final", ``deriv ^r6 ^r_final``, 480 MATCH_MP_TAC derivRight 481 >> MATCH_MP_TAC derivOne 482 >> MATCH_MP_TAC derivOne 483 >> MATCH_MP_TAC derivBoth 484 >> CONJ_TAC 485 >| [ MATCH_MP_TAC derivBoth \\ 486 CONJ_TAC \\ (* 2 sub-goals, same tacticals *) 487 MATCH_MP_TAC derivDerivOne >> REWRITE_TAC [derivSeqAxiom], 488 MATCH_MP_TAC derivDerivOne >> REWRITE_TAC [derivSeqAxiom] ]); 489 490fun derivToDeriv thm = 491 REWRITE_RULE [SYM Deriv_def] (MATCH_MP RTC_SINGLE thm); 492 493val r0_to_final = store_thm ( 494 "r0_to_final", ``Deriv ^r0 ^r_final``, 495 ASSUME_TAC r0_to_r1'' 496 >> ASSUME_TAC (derivToDeriv r1_to_r2) 497 >> ASSUME_TAC (derivToDeriv r2_to_r3) 498 >> ASSUME_TAC (derivToDeriv r3_to_r4) 499 >> ASSUME_TAC (derivToDeriv r4_to_r5) 500 >> ASSUME_TAC (derivToDeriv r5_to_r6) 501 >> ASSUME_TAC (derivToDeriv r6_to_final) 502 >> REPEAT (IMP_RES_TAC Deriv_trans)); 503 504val _ = export_theory (); 505val _ = html_theory "Example"; 506 507(* Emit theory books in TeX *) 508(* 509if (OS.FileSys.isDir "../papers" handle e => false) then 510 let in 511 OS.FileSys.remove "../papers/references.tex" handle e => {}; 512 OS.FileSys.remove "../papers/HOLLambek.tex" handle e => {}; 513 OS.FileSys.remove "../papers/HOLCutFree.tex" handle e => {}; 514 OS.FileSys.remove "../papers/HOLExample.tex" handle e => {}; 515 516 EmitTeX.print_theories_as_tex_doc 517 ["Lambek", "CutFree", "Example"] "../papers/references" 518 end 519else 520 {}; 521 *) 522 523(* last updated: April 9, 2017 *) 524