1(* 2 * Formalized Lambek Calculus in Higher Order Logic (HOL4) 3 * 4 * (based on https://github.com/coq-contribs/lambek) 5 * 6 * Copyright 2002-2003 Houda ANOUN and Pierre Casteran, LaBRI/INRIA. 7 * Copyright 2016-2017 University of Bologna, Italy (Author: Chun Tian) 8 *) 9 10(* This program is free software; you can redistribute it and/or *) 11(* modify it under the terms of the GNU Lesser General Public License *) 12(* as published by the Free Software Foundation; either version 2.1 *) 13(* of the License, or (at your option) any later version. *) 14(* *) 15(* This program is distributed in the hope that it will be useful, *) 16(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) 17(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) 18(* GNU General Public License for more details. *) 19(* *) 20(* You should have received a copy of the GNU Lesser General Public *) 21(* License along with this program; if not, write to the Free *) 22(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) 23(* 02110-1301 USA *) 24 25open HolKernel Parse boolLib bossLib; 26 27open relationTheory prim_recTheory arithmeticTheory listTheory; 28open LambekTheory; 29 30local 31 val PAT_X_ASSUM = PAT_ASSUM; 32 val qpat_x_assum = Q.PAT_ASSUM; 33 open Tactical 34in 35 (* Backward compatibility with Kananaskis 11 *) 36 val PAT_X_ASSUM = PAT_X_ASSUM; 37 val qpat_x_assum = qpat_x_assum; 38 39 (* Tacticals for better expressivity *) 40 fun fix ts = MAP_EVERY Q.X_GEN_TAC ts; (* from HOL Light *) 41 fun set ts = MAP_EVERY Q.ABBREV_TAC ts; (* from HOL mizar mode *) 42 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) 43end; 44 45val _ = new_theory "CutFree"; 46 47hide "S"; 48 49(*** Module: CutSequent ***) 50 51(* this theorem was not in HOL kananaskis-11 final release, it's new in K-12 *) 52val MAX_EQ_0 = store_thm ( 53 "MAX_EQ_0", 54 ``(MAX m n = 0) <=> (m = 0) /\ (n = 0)``, 55 SRW_TAC [] [MAX_DEF, EQ_IMP_THM] 56 >> FULL_SIMP_TAC (srw_ss()) [NOT_LESS_0, NOT_LESS]); 57 58val maxNatL = store_thm ("maxNatL", 59 ``(MAX n m = 0) ==> (n = 0)``, RW_TAC std_ss [MAX_EQ_0]); 60val maxNatR = store_thm ("maxNatR", 61 ``(MAX n m = 0) ==> (m = 0)``, RW_TAC std_ss [MAX_EQ_0]); 62 63val degreeFormula_def = Define ` 64 (degreeFormula (At C) = 1) /\ 65 (degreeFormula (Slash F1 F2) = SUC (MAX (degreeFormula F1) (degreeFormula F2))) /\ 66 (degreeFormula (Backslash F1 F2) = SUC (MAX (degreeFormula F1) (degreeFormula F2))) /\ 67 (degreeFormula (Dot F1 F2) = SUC (MAX (degreeFormula F1) (degreeFormula F2)))`; 68 69val degreeForm_0 = store_thm ("degreeForm_0", ``!F0. 1 <= (degreeFormula F0)``, 70 Induct >> rw [degreeFormula_def]); 71 72(* Deep Embeddings for Lambek's Sequent Calculus *) 73val _ = Datatype `Sequent = Sequent ('a gentzen_extension) ('a Term) ('a Form)`; 74 75val _ = Datatype `Rule = SeqAxiom 76 | RightSlash | RightBackslash | RightDot 77 | LeftSlash | LeftBackslash | LeftDot 78 | CutRule | SeqExt`; 79 80val all_rules_def = Define ` 81 all_rules = 82 { SeqAxiom; RightSlash; RightBackslash; RightDot; 83 LeftSlash; LeftBackslash; LeftDot; SeqExt; CutRule }`; 84 85(* Note: (Dertree list) never has more than 2 elements in Lambek's Sequent Calculus *) 86val _ = Datatype `Dertree = Der ('a Sequent) Rule (Dertree list) 87 | Unf ('a Sequent)`; 88 89val Dertree_induction = TypeBase.induction_of ``:'a Dertree``; 90val Dertree_nchotomy = TypeBase.nchotomy_of ``:'a Dertree``; 91val Dertree_distinct = TypeBase.distinct_of ``:'a Dertree``; 92val Dertree_distinct' = save_thm ("Dertree_distinct'", GSYM Dertree_distinct); 93val Dertree_11 = TypeBase.one_one_of ``:'a Dertree``; 94 95(* not used *) 96val Is_Unfinished_def = Define ` 97 (Is_Unfinished (Der _ _ []) = F) /\ 98 (Is_Unfinished (Der _ _ [D]) = Is_Unfinished D) /\ 99 (Is_Unfinished (Der _ _ [D1; D2]) = (Is_Unfinished D1 /\ Is_Unfinished D2)) /\ 100 (Is_Unfinished (Unf _) = T)`; 101 102(* not used *) 103val Is_Finished_def = Define ` 104 (Is_Finished (Der _ _ []) = T) /\ 105 (Is_Finished (Der _ _ [D]) = Is_Finished D) /\ 106 (Is_Finished (Der _ _ [D1; D2]) = (Is_Finished D1 /\ Is_Finished D2)) /\ 107 (Is_Finished (Unf _) = F)`; 108 109(* structure accessors *) 110val head_def = Define ` 111 (head (Der seq _ _) = seq) /\ 112 (head (Unf seq) = seq)`; 113 114val concl_def = Define ` 115 (concl (Unf (Sequent E Delta A)) = A) /\ 116 (concl (Der (Sequent E Delta A) _ _) = A)`; 117 118val prems_def = Define ` 119 (prems (Unf (Sequent E Delta A)) = Delta) /\ 120 (prems (Der (Sequent E Delta A) _ _) = Delta)`; 121 122val exten_def = Define ` 123 (exten (Unf (Sequent E Delta A)) = E) /\ 124 (exten (Der (Sequent E Delta A) _ _) = E)`; 125 126val degreeRule_def = Define ` 127 (degreeRule (Der S SeqAxiom []) = 0) /\ 128 (degreeRule (Der S RightSlash [H]) = 0) /\ 129 (degreeRule (Der S RightBackslash [H]) = 0) /\ 130 (degreeRule (Der S RightDot [H1; H2]) = 0) /\ 131 (degreeRule (Der S LeftSlash [H1; H2]) = 0) /\ 132 (degreeRule (Der S LeftBackslash [H1; H2]) = 0) /\ 133 (degreeRule (Der S LeftDot [H]) = 0) /\ 134 (degreeRule (Der S SeqExt [H]) = 0) /\ 135 (* The degree of a cut is the degree of the cut formula which disappears after 136 application of the rule. *) 137 (degreeRule (Der S CutRule [H1; H2]) = degreeFormula (concl H1))`; 138 139(* degreeProof, one way to check if CutRule gets used *) 140val degreeProof_def = Define ` 141 (degreeProof (Der S SeqAxiom []) = 0) /\ 142 (degreeProof (Der S RightSlash [H]) = degreeProof H) /\ 143 (degreeProof (Der S RightBackslash [H]) = degreeProof H) /\ 144 (degreeProof (Der S RightDot [H1; H2]) = MAX (degreeProof H1) (degreeProof H2)) /\ 145 (degreeProof (Der S LeftSlash [H1; H2]) = MAX (degreeProof H1) (degreeProof H2)) /\ 146 (degreeProof (Der S LeftBackslash [H1; H2]) = MAX (degreeProof H1) (degreeProof H2)) /\ 147 (degreeProof (Der S LeftDot [H]) = degreeProof H) /\ 148 (degreeProof (Der S SeqExt [H]) = degreeProof H) /\ 149 (* CutRule is special *) 150 (degreeProof (Der S CutRule [H1; H2]) = 151 MAX (degreeFormula (concl H1)) 152 (MAX (degreeProof H1) (degreeProof H2)))`; 153 154(* subFormula and their theorems *) 155val (subFormula_rules, subFormula_ind, subFormula_cases) = Hol_reln ` 156 (!(A:'a Form). subFormula A A) /\ (* equalForm *) 157 (!A B C. subFormula A B ==> subFormula A (Slash B C)) /\ (* slashL *) 158 (!A B C. subFormula A B ==> subFormula A (Slash C B)) /\ (* slashR *) 159 (!A B C. subFormula A B ==> subFormula A (Backslash B C)) /\ (* backslashL *) 160 (!A B C. subFormula A B ==> subFormula A (Backslash C B)) /\ (* backslashR *) 161 (!A B C. subFormula A B ==> subFormula A (Dot B C)) /\ (* dotL *) 162 (!A B C. subFormula A B ==> subFormula A (Dot C B))`; (* dotR *) 163 164val [equalForm, slashL, slashR, backslashL, backslashR, dotL, dotR] = 165 map save_thm 166 (combine (["equalForm", "slashL", "slashR", "backslashL", "backslashR", "dotL", "dotR"], 167 CONJUNCTS subFormula_rules)); 168 169(* The simp set related to Form *) 170val Form_ss = DatatypeSimps.type_rewrites_ss [``:'a Form``]; 171 172val subAt = store_thm ("subAt", ``!A a. subFormula A (At a) ==> (A = At a)``, 173 ONCE_REWRITE_TAC [subFormula_cases] 174 >> SIMP_TAC bool_ss [Form_distinct]); (* or: SIMP_TAC (bool_ss ++ Form_ss) [] *) 175 176val subSlash = store_thm ("subSlash", 177 ``!A B C. subFormula A (Slash B C) ==> (A = Slash B C) \/ subFormula A B \/ subFormula A C``, 178 REPEAT GEN_TAC 179 >> ONCE_REWRITE_TAC [Q.SPECL [`A`, `(Slash B C)`] subFormula_cases] 180 >> SIMP_TAC (bool_ss ++ Form_ss) [EQ_SYM_EQ]); 181 182val subBackslash = store_thm ("subBackslash", 183 ``!A B C. subFormula A (Backslash B C) ==> (A = Backslash B C) \/ subFormula A B \/ subFormula A C``, 184 REPEAT GEN_TAC 185 >> ONCE_REWRITE_TAC [Q.SPECL [`A`, `(Backslash B C)`] subFormula_cases] 186 >> SIMP_TAC (bool_ss ++ Form_ss) [EQ_SYM_EQ]); 187 188val subDot = store_thm ("subDot", 189 ``!A B C. subFormula A (Dot B C) ==> (A = Dot B C) \/ subFormula A B \/ subFormula A C``, 190 REPEAT GEN_TAC 191 >> ONCE_REWRITE_TAC [Q.SPECL [`A`, `(Dot B C)`] subFormula_cases] 192 >> SIMP_TAC (bool_ss ++ Form_ss) [EQ_SYM_EQ]); 193 194(* all previous theorems and rules were used in this proof ... *) 195val subFormulaTrans = store_thm ( 196 "subFormulaTrans", 197 ``!A B C. subFormula A B ==> subFormula B C ==> subFormula A C``, 198 Induct_on `C` 199 >| [ (* case 1 *) 200 PROVE_TAC [subAt], 201 (* case 2, can be proved by PROVE_TAC [subSlash, slashL, slashR] *) 202 REPEAT STRIP_TAC \\ 203 POP_ASSUM (STRIP_ASSUME_TAC o MATCH_MP subSlash) >| 204 [ PROVE_TAC [], 205 PROVE_TAC [slashL], 206 PROVE_TAC [slashR] ], 207 (* case 3 *) 208 PROVE_TAC [subBackslash, backslashL, backslashR], 209 (* case 4 *) 210 PROVE_TAC [subDot, dotL, dotR] ]); 211 212val subFormulaTrans' = store_thm ( 213 "subFormulaTrans'", ``transitive subFormula``, 214 PROVE_TAC [subFormulaTrans, transitive_def]); 215 216(* subFormTerm *) 217val (subFormTerm_rules, subFormTerm_ind, subFormTerm_cases) = Hol_reln ` 218 (!A B. subFormula A B ==> subFormTerm A (OneForm B)) /\ (* eqFT *) 219 (!A T1 T2. subFormTerm A T1 ==> subFormTerm A (Comma T1 T2)) /\ (* comL *) 220 (!A T1 T2. subFormTerm A T1 ==> subFormTerm A (Comma T2 T1))`; (* comR *) 221 222val [eqFT, comL, comR] = 223 map save_thm (combine (["eqFT", "comL", "comR"], CONJUNCTS subFormTerm_rules)); 224 225val Term_11 = TypeBase.one_one_of ``:'a Term``; 226val Term_distinct = TypeBase.distinct_of ``:'a Term``; 227 228val oneFormSub = store_thm ( 229 "oneFormSub", ``!A B. subFormTerm A (OneForm B) ==> subFormula A B``, 230 ONCE_REWRITE_TAC [subFormTerm_cases] 231 >> REPEAT STRIP_TAC 232 >| [ PROVE_TAC [Term_11], 233 PROVE_TAC [Term_distinct], 234 PROVE_TAC [Term_distinct] ]); 235 236val oneFormSubEQ = store_thm ( 237 "oneFormSubEQ[simp]", ``!A B. subFormTerm A (OneForm B) = subFormula A B``, 238 REPEAT GEN_TAC 239 >> EQ_TAC (* 2 sub-goals here *) 240 >| [ REWRITE_TAC [oneFormSub], 241 REWRITE_TAC [eqFT] ]); 242 243val comSub = store_thm ("comSub", 244 ``!f T1 T2. subFormTerm f (Comma T1 T2) ==> subFormTerm f T1 \/ subFormTerm f T2``, 245 REPEAT GEN_TAC 246 >> GEN_REWRITE_TAC LAND_CONV empty_rewrites [Once subFormTerm_cases] 247 >> REPEAT STRIP_TAC 248 >| [ PROVE_TAC [Term_distinct], 249 PROVE_TAC [Term_11], 250 PROVE_TAC [Term_11] ]); 251 252val subReplace1 = store_thm ("subReplace1", 253 ``!f T1 T2 T3 T4. replace T1 T2 T3 T4 ==> subFormTerm f T3 ==> subFormTerm f T1``, 254 GEN_TAC 255 >> HO_MATCH_MP_TAC replace_ind 256 >> REPEAT STRIP_TAC 257 >- PROVE_TAC [comL] 258 >> PROVE_TAC [comR]); 259 260val subReplace2 = store_thm ("subReplace2", 261 ``!f T1 T2 T3 T4. replace T1 T2 T3 T4 ==> subFormTerm f T4 ==> subFormTerm f T2``, 262 GEN_TAC 263 >> HO_MATCH_MP_TAC replace_ind 264 >> REPEAT STRIP_TAC 265 >- PROVE_TAC [comL] 266 >> PROVE_TAC [comR]); 267 268val subReplace3 = store_thm ("subReplace3", 269 ``!X T1 T2 T3 T4. replace T1 T2 T3 T4 ==> subFormTerm X T1 270 ==> subFormTerm X T2 \/ subFormTerm X T3``, 271 GEN_TAC 272 >> HO_MATCH_MP_TAC replace_ind 273 >> REPEAT STRIP_TAC 274 >- ASM_REWRITE_TAC [] 275 >| [ (* case 2 *) 276 `subFormTerm X T1 \/ subFormTerm X Delta` by PROVE_TAC [comSub] >| 277 [ `subFormTerm X T2 \/ subFormTerm X T3` by PROVE_TAC [] \\ 278 PROVE_TAC [comL], 279 PROVE_TAC [comR] ], 280 (* case 3 *) 281 `subFormTerm X Delta \/ subFormTerm X T1` by PROVE_TAC [comSub] >| 282 [ PROVE_TAC [comL], 283 `subFormTerm X T2 \/ subFormTerm X T3` by PROVE_TAC [] \\ 284 PROVE_TAC [comR] ] ]); 285 286val CutFreeProof_def = Define ` 287 CutFreeProof p = (degreeProof p = 0)`; 288 289val notCutFree = store_thm ("notCutFree", 290 ``!E T1 T2 D A C p p1 p2. 291 replace T1 T2 (OneForm A) D /\ 292 (p1 = Sequent E D A) /\ (p2 = Sequent E T1 C) ==> 293 ~CutFreeProof (Der _ CutRule [Der p1 _ _; Der p2 _ _])``, 294 REPEAT GEN_TAC 295 >> STRIP_TAC 296 >> REWRITE_TAC [CutFreeProof_def] 297 >> RW_TAC std_ss [degreeProof_def, concl_def] 298 >> STRIP_TAC 299 >> `1 <= degreeFormula A` by REWRITE_TAC [degreeForm_0] 300 >> `degreeFormula A = 0` by PROVE_TAC [MAX_EQ_0] 301 >> RW_TAC arith_ss []); 302 303val (subProofOne_rules, subProofOne_ind, subProofOne_cases) = Hol_reln ` 304 (!p0 p E Gamma A B R D. 305 (p0 = Sequent E Gamma (Slash A B)) /\ 306 (p = Der (Sequent E (Comma Gamma (OneForm B)) A) R D) 307 ==> subProofOne p (Der p0 RightSlash [p])) /\ (* 1. rs *) 308 309 (!p0 p E Gamma A B R D. 310 (p0 = Sequent E Gamma (Backslash B A)) /\ 311 (p = Der (Sequent E (Comma (OneForm B) Gamma) A) R D) 312 ==> subProofOne p (Der p0 RightBackslash [p])) /\ (* 2. rbs *) 313 314 (!p0 p1 p2 E Gamma Delta A B R D. 315 (p0 = Sequent E (Comma Gamma Delta) (Dot A B)) /\ 316 (p1 = Der (Sequent E Gamma A) R D) /\ 317 (p2 = Der (Sequent E Delta B) R D) 318 ==> subProofOne p1 (Der p0 RightDot [p1; p2])) /\ (* 3. rd1 *) 319 320 (!p0 p1 p2 E Gamma Delta A B R D. 321 (p0 = Sequent E (Comma Gamma Delta) (Dot A B)) /\ 322 (p1 = Der (Sequent E Gamma A) R D) /\ 323 (p2 = Der (Sequent E Delta B) R D) 324 ==> subProofOne p2 (Der p0 RightDot [p1; p2])) /\ (* 4. rd2 *) 325 326 (!p0 p1 p2 E Gamma Gamma' Delta A B C R D. 327 (p0 = Sequent E Gamma' C) /\ 328 (p1 = Der (Sequent E Delta B) R D) /\ 329 (p2 = Der (Sequent E Gamma C) R D) /\ 330 (replace Gamma Gamma' (OneForm A) (Comma (OneForm (Slash A B)) Delta)) 331 ==> subProofOne p1 (Der p0 LeftSlash [p1; p2])) /\ (* 5. ls1 *) 332 333 (!p0 p1 p2 E Gamma Gamma' Delta A B C R D. 334 (p0 = Sequent E Gamma' C) /\ 335 (p1 = Der (Sequent E Delta B) R D) /\ 336 (p2 = Der (Sequent E Gamma C) R D) /\ 337 replace Gamma Gamma' (OneForm A) (Comma (OneForm (Slash A B)) Delta) 338 ==> subProofOne p2 (Der p0 LeftSlash [p1; p2])) /\ (* 6. ls2 *) 339 340 (!p0 p1 p2 E Gamma Gamma' Delta A B C R D. 341 (p0 = Sequent E Gamma' C) /\ 342 (p1 = Der (Sequent E Delta B) R D) /\ 343 (p2 = Der (Sequent E Gamma C) R D) /\ 344 replace Gamma Gamma' (OneForm A) (Comma Delta (OneForm (Backslash B A))) 345 ==> subProofOne p1 (Der p0 LeftBackslash [p1; p2])) /\ (* 7. lbs1 *) 346 347 (!p0 p1 p2 E Gamma Gamma' Delta A B C R D. 348 (p0 = Sequent E Gamma' C) /\ 349 (p1 = Der (Sequent E Delta B) R D) /\ 350 (p2 = Der (Sequent E Gamma C) R D) /\ 351 replace Gamma Gamma' (OneForm A) (Comma Delta (OneForm (Backslash B A))) 352 ==> subProofOne p2 (Der p0 LeftBackslash [p1; p2])) /\ (* 8. lbs2 *) 353 354 (!p0 p E Gamma Gamma' A B C R D. 355 (p0 = Sequent E Gamma' C) /\ 356 (p = Der (Sequent E Gamma C) R D) /\ 357 replace Gamma Gamma' (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) 358 ==> subProofOne p (Der p0 LeftDot [p])) /\ (* 9. ld *) 359 360 (!p0 p1 p2 E Gamma Gamma' Delta A C R D. 361 (p0 = Sequent E Gamma' C) /\ 362 (p1 = Der (Sequent E Delta A) R D) /\ 363 (p2 = Der (Sequent E Gamma C) R D) /\ 364 replace Gamma Gamma' (OneForm A) Delta 365 ==> subProofOne p1 (Der p0 CutRule [p1; p2])) /\ (* 10. cr1 *) 366 367 (!p0 p1 p2 E Gamma Gamma' Delta A C R D. 368 (p0 = Sequent E Gamma' C) /\ 369 (p1 = Der (Sequent E Delta A) R D) /\ 370 (p2 = Der (Sequent E Gamma C) R D) /\ 371 replace Gamma Gamma' (OneForm A) Delta 372 ==> subProofOne p2 (Der p0 CutRule [p1; p2])) /\ (* 11. cr2 *) 373 374 (!p0 p E Gamma Gamma' T1 T2 C R D. 375 (p0 = Sequent E Gamma' C) /\ 376 (p = Der (Sequent E Gamma C) R D) /\ 377 (E :'a gentzen_extension) T1 T2 /\ 378 replace Gamma Gamma' T1 T2 379 ==> subProofOne p (Der p0 SeqExt [p])) `; (* se *) 380 381val [rs, rbs, rd1, rd2, ls1, ls2, lbs1, lbs2, ld, cr1, cr2, se] = 382 map save_thm 383 (combine (["rs", "rbs", "rd1", "rd2", "ls1", "ls2", "lbs1", "lbs2", 384 "ld", "cr1", "cr2", "se"], 385 CONJUNCTS subProofOne_rules)); 386 387(* (subProof :'a Dertree -> 'a Dertree -> bool) *) 388val subProof_def = Define `subProof = RTC subProofOne`; 389 390val sameProof = store_thm ( 391 "sameProof", ``!p. subProof p p``, 392 REWRITE_TAC [subProof_def, RTC_REFL]); 393 394val subProof1 = store_thm ( 395 "subProof1", ``!p1 p2 p3. subProofOne p1 p2 /\ subProof p2 p3 ==> subProof p1 p3``, 396 REWRITE_TAC [subProof_def, RTC_RULES]); 397 398val subProof_rules = save_thm ( 399 "subProof_rules", LIST_CONJ [sameProof, subProof1]); 400 401(* 402 |- ���P. 403 (���x. P x x) ��� 404 (���x y z. subProofOne x y ��� P y z ��� P x z) ��� 405 ���x y. subProof x y ��� P x y 406 *) 407val subProof_ind = save_thm ( 408 "subProof_ind", 409 REWRITE_RULE [GSYM subProof_def] (Q.ISPEC `subProofOne` RTC_INDUCT)); 410 411(* 412 |- ���P. 413 (���x. P x x) ��� 414 (���x y z. subProofOne x y ��� subProof y z ��� P y z ��� P x z) ��� 415 ���x y. subProof x y ��� P x y: 416 *) 417val subProof_strongind = save_thm ( 418 "subProof_strongind", 419 REWRITE_RULE [GSYM subProof_def] (Q.ISPEC `subProofOne` RTC_STRONG_INDUCT)); 420 421(* 422 |- ���x y. subProof x y ��� (x = y) ��� ���u. subProofOne x u ��� subProof u y 423 *) 424val subProof_cases = save_thm ( 425 "subProof_cases", 426 REWRITE_RULE [GSYM subProof_def] (Q.ISPEC `subProofOne` RTC_CASES1)); 427 428(* 429 |- ���x y. subProof x y ��� (x = y) ��� ���u. subProof x u ��� subProofOne u y 430 *) 431val subProof_cases' = save_thm ( 432 "subProof_cases'", 433 REWRITE_RULE [GSYM subProof_def] (Q.ISPEC `subProofOne` RTC_CASES2)); 434 435(* original code: 436val (subProof'_rules, subProof'_ind, subProof'_cases) = Hol_reln ` 437 (!(p :'a Dertree). subProof' p p) /\ 438 (!p1 p2 p3. subProof' p2 p1 /\ subProofOne p3 p2 ==> subProof' p3 p1)`; 439 *) 440 441val CutFreeSubProofOne = store_thm ("CutFreeSubProofOne", 442 ``!q p. subProofOne q p ==> CutFreeProof p ==> CutFreeProof q``, 443 Induct_on `subProofOne` 444 >> REWRITE_TAC [CutFreeProof_def, degreeProof_def] 445 >> PROVE_TAC [MAX_EQ_0]); 446 447val CutFreeSubProof = store_thm ("CutFreeSubProof", 448 ``!q p. subProof q p ==> CutFreeProof p ==> CutFreeProof q``, 449 REWRITE_TAC [subProof_def] 450 >> HO_MATCH_MP_TAC RTC_INDUCT 451 >> PROVE_TAC [CutFreeSubProofOne]); 452 453val extensionSub_def = Define ` 454 extensionSub E = !Form T1 T2. E T1 T2 ==> subFormTerm Form T1 ==> subFormTerm Form T2`; 455 456val subProofOne_extension = store_thm ( 457 "subProofOne_extension", 458 ``!q p. subProofOne q p ==> 459 extensionSub (exten p) ==> extensionSub (exten q)``, 460 REPEAT GEN_TAC 461 >> ONCE_REWRITE_TAC [subProofOne_cases] 462 >> REPEAT STRIP_TAC (* 12 subgoals, all sharing the same tacticals *) 463 >> `extensionSub E` by METIS_TAC [exten_def] 464 >> ASM_REWRITE_TAC [exten_def]); 465 466val subProof_extension = store_thm ( 467 "subProof_extension", 468 ``!q p. subProof q p ==> 469 extensionSub (exten p) ==> extensionSub (exten q)``, 470 HO_MATCH_MP_TAC subProof_strongind 471 >> REPEAT STRIP_TAC 472 >> RES_TAC 473 >> IMP_RES_TAC subProofOne_extension); 474 475(* one-step derivation (of proofs): Dertree -> Dertree -> bool *) 476val (derivOne_rules, derivOne_ind, derivOne_cases) = Hol_reln ` 477 (!E A. 478 derivOne (Unf (Sequent E (OneForm A) A)) 479 (Der (Sequent E (OneForm A) A) SeqAxiom [])) /\ 480 (!E Gamma A B. 481 derivOne (Unf (Sequent E Gamma (Slash A B))) 482 (Der (Sequent E Gamma (Slash A B)) RightSlash 483 [ Unf (Sequent E (Comma Gamma (OneForm B)) A) ])) /\ 484 (!E Gamma A B. 485 derivOne (Unf (Sequent E Gamma (Backslash B A))) 486 (Der (Sequent E Gamma (Backslash B A)) RightBackslash 487 [ Unf (Sequent E (Comma (OneForm B) Gamma) A) ])) /\ 488 (!E Gamma Delta A B. 489 derivOne (Unf (Sequent E (Comma Gamma Delta) (Dot A B))) 490 (Der (Sequent E (Comma Gamma Delta) (Dot A B)) RightDot 491 [ Unf (Sequent E Gamma A); Unf (Sequent E Delta B) ])) /\ 492 (!E Gamma Gamma' Delta A B C. 493 replace Gamma Gamma' (OneForm A) (Comma (OneForm (Slash A B)) Delta) ==> 494 derivOne (Unf (Sequent E Gamma' C)) 495 (Der (Sequent E Gamma' C) LeftSlash 496 [ Unf (Sequent E Gamma C); Unf (Sequent E Delta B) ])) /\ 497 (!E Gamma Gamma' Delta A B C. 498 replace Gamma Gamma' (OneForm A) (Comma Delta (OneForm (Backslash B A))) ==> 499 derivOne (Unf (Sequent E Gamma' C)) 500 (Der (Sequent E Gamma' C) LeftBackslash 501 [ Unf (Sequent E Gamma C); Unf (Sequent E Delta B) ])) /\ 502 (!E Gamma Gamma' A B C. 503 replace Gamma Gamma' (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) ==> 504 derivOne (Unf (Sequent E Gamma' C)) 505 (Der (Sequent E Gamma' C) LeftDot 506 [ Unf (Sequent E Gamma C) ])) /\ 507 (!E Delta Gamma Gamma' A C. 508 replace Gamma Gamma' (OneForm A) Delta ==> 509 derivOne (Unf (Sequent E Gamma' C)) 510 (Der (Sequent E Gamma' C) CutRule 511 [ Unf (Sequent E Gamma C); Unf (Sequent E Delta A) ])) /\ 512 (!E Gamma Gamma' Delta Delta' C. 513 replace Gamma Gamma' Delta Delta' /\ E Delta Delta' ==> 514 derivOne (Unf (Sequent E Gamma' C)) 515 (Der (Sequent E Gamma' C) SeqExt 516 [ Unf (Sequent E Gamma C) ]))`; 517 518val [derivSeqAxiom, derivRightSlash, derivRightBackslash, derivRightDot, 519 derivLeftSlash, derivLeftBackslash, derivLeftDot, derivCutRule, derivSeqExt] = 520 map save_thm 521 (combine (["derivSeqAxiom", "derivRightSlash", "derivRightBackslash", 522 "derivRightDot", "derivLeftSlash", "derivLeftBackslash", 523 "derivLeftDot", "derivCutRule", "derivSeqExt"], 524 CONJUNCTS derivOne_rules)); 525 526(* structure rules *) 527val (deriv_rules, deriv_ind, deriv_cases) = Hol_reln ` 528 (!D1 D2. derivOne D1 D2 ==> deriv D1 D2) /\ 529 (!S R D1 D1'. deriv D1 D1' ==> deriv (Der S R [D1]) (Der S R [D1'])) /\ 530 (!S R D1 D1' D. deriv D1 D1' ==> deriv (Der S R [D1; D]) (Der S R [D1'; D])) /\ 531 (!S R D2 D2' D. deriv D2 D2' ==> deriv (Der S R [D; D2]) (Der S R [D; D2'])) /\ 532 (!S R D1 D1' D2 D2'. deriv D1 D1' /\ deriv D2 D2' 533 ==> deriv (Der S R [D1; D2]) (Der S R [D1'; D2']))`; 534 535val [derivDerivOne, derivOne, derivLeft, derivRight, derivBoth] = 536 map save_thm 537 (combine (["derivDerivOne", "derivOne", "derivLeft", "derivRight", "derivBoth"], 538 CONJUNCTS deriv_rules)); 539 540(* closure rules, in this way we can finish a proof *) 541val Deriv_def = Define `Deriv = RTC deriv`; 542 543(* |- ���x. Deriv x x *) 544val Deriv_refl = save_thm ( 545 "Deriv_refl", 546 REWRITE_RULE [SYM Deriv_def] 547 (((Q.ISPEC `deriv`) o (Q.GEN `R`) o (Q.GEN `x`)) RTC_REFL)); 548 549(* |- ���x y z. Deriv x y ��� Deriv y z ��� Deriv x z *) 550val Deriv_trans = save_thm ( 551 "Deriv_trans", 552 REWRITE_RULE [SYM Deriv_def] 553 (Q.ISPEC `deriv` (REWRITE_RULE [transitive_def] RTC_TRANSITIVE))); 554 555fun derivToDeriv thm = 556 REWRITE_RULE [SYM Deriv_def] (MATCH_MP RTC_SINGLE thm); 557 558fun derivOneToDeriv thm = 559 REWRITE_RULE [GSYM Deriv_def] 560 (MATCH_MP (Q.ISPEC `deriv` RTC_SINGLE) 561 (MATCH_MP derivDerivOne (SPEC_ALL thm))); 562 563(* derivation rules expressed in relation `Deriv`, for convinence *) 564 565(* |- ���E A. 566 Deriv (Unf (E:- OneForm A |- A)) 567 (Der (E:- OneForm A |- A) SeqAxiom []) 568 *) 569val DerivSeqAxiom = save_thm ( 570 "DerivSeqAxiom", 571 ((Q.GEN `E`) o (Q.GEN `A`) o derivOneToDeriv) derivSeqAxiom); 572 573val DerivRightSlash = save_thm ( 574 "DerivRightSlash", 575 ((Q.GEN `E`) o (Q.GEN `Gamma`) o (Q.GEN `A`) o (Q.GEN `B`) o 576 derivOneToDeriv) derivRightSlash); 577 578val DerivRightBackslash = save_thm ( 579 "DerivRightBackslash", 580 ((Q.GEN `E`) o (Q.GEN `Gamma`) o (Q.GEN `A`) o (Q.GEN `B`) o 581 derivOneToDeriv) derivRightBackslash); 582 583val DerivRightDot = save_thm ( 584 "DerivRightDot", 585 ((Q.GEN `E`) o (Q.GEN `Gamma`) o (Q.GEN `Delta`) o (Q.GEN `A`) o (Q.GEN `B`) o 586 derivOneToDeriv) derivRightDot); 587 588val DerivLeftSlash = store_thm ( 589 "DerivLeftSlash", 590 ``!E Gamma Gamma' Delta A B C. 591 replace Gamma Gamma' (OneForm A) (Comma (OneForm (Slash A B)) Delta) ==> 592 Deriv (Unf (Sequent E Gamma' C)) 593 (Der (Sequent E Gamma' C) LeftSlash 594 [ Unf (Sequent E Gamma C); Unf (Sequent E Delta B) ])``, 595 REPEAT STRIP_TAC 596 >> REWRITE_TAC [Deriv_def] 597 >> MATCH_MP_TAC (Q.ISPEC `deriv` RTC_SINGLE) 598 >> MATCH_MP_TAC derivDerivOne 599 >> POP_ASSUM MP_TAC 600 >> REWRITE_TAC [derivLeftSlash]); 601 602val DerivLeftBackslash = store_thm ( 603 "DerivLeftBackslash", 604 ``!E Gamma Gamma' Delta A B C. 605 replace Gamma Gamma' (OneForm A) (Comma Delta (OneForm (Backslash B A))) ==> 606 Deriv (Unf (Sequent E Gamma' C)) 607 (Der (Sequent E Gamma' C) LeftBackslash 608 [ Unf (Sequent E Gamma C); Unf (Sequent E Delta B) ])``, 609 REPEAT STRIP_TAC 610 >> REWRITE_TAC [Deriv_def] 611 >> MATCH_MP_TAC (Q.ISPEC `deriv` RTC_SINGLE) 612 >> MATCH_MP_TAC derivDerivOne 613 >> POP_ASSUM MP_TAC 614 >> REWRITE_TAC [derivLeftBackslash]); 615 616val DerivLeftDot = store_thm ( 617 "DerivLeftDot", 618 ``!E Gamma Gamma' A B C. 619 replace Gamma Gamma' (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) ==> 620 Deriv (Unf (Sequent E Gamma' C)) 621 (Der (Sequent E Gamma' C) LeftDot 622 [ Unf (Sequent E Gamma C) ])``, 623 REPEAT STRIP_TAC 624 >> REWRITE_TAC [Deriv_def] 625 >> MATCH_MP_TAC (Q.ISPEC `deriv` RTC_SINGLE) 626 >> MATCH_MP_TAC derivDerivOne 627 >> POP_ASSUM MP_TAC 628 >> REWRITE_TAC [derivLeftDot]); 629 630val DerivCutRule = store_thm ( 631 "DerivCutRule", 632 ``!E Delta Gamma Gamma' A C. 633 replace Gamma Gamma' (OneForm A) Delta ==> 634 Deriv (Unf (Sequent E Gamma' C)) 635 (Der (Sequent E Gamma' C) CutRule 636 [ Unf (Sequent E Gamma C); Unf (Sequent E Delta A) ])``, 637 REPEAT STRIP_TAC 638 >> REWRITE_TAC [Deriv_def] 639 >> MATCH_MP_TAC (Q.ISPEC `deriv` RTC_SINGLE) 640 >> MATCH_MP_TAC derivDerivOne 641 >> POP_ASSUM MP_TAC 642 >> REWRITE_TAC [derivCutRule]); 643 644val DerivSeqExt = store_thm ( 645 "DerivSeqExt", 646 ``!E Gamma Gamma' Delta Delta' C. 647 replace Gamma Gamma' Delta Delta' /\ E Delta Delta' ==> 648 Deriv (Unf (Sequent E Gamma' C)) 649 (Der (Sequent E Gamma' C) SeqExt 650 [ Unf (Sequent E Gamma C) ])``, 651 REPEAT STRIP_TAC 652 >> REWRITE_TAC [Deriv_def] 653 >> MATCH_MP_TAC (Q.ISPEC `deriv` RTC_SINGLE) 654 >> MATCH_MP_TAC derivDerivOne 655 >> PROVE_TAC [derivSeqExt]); 656 657val DerivOne = store_thm ("DerivOne", 658 ``!S R D1 D1'. Deriv D1 D1' ==> Deriv (Der S R [D1]) (Der S R [D1'])``, 659 NTAC 2 GEN_TAC 660 >> REWRITE_TAC [Deriv_def] 661 >> HO_MATCH_MP_TAC RTC_INDUCT 662 >> REPEAT STRIP_TAC (* 2 sub-goals here, first one is easy *) 663 >- REWRITE_TAC [RTC_REFL] 664 >> PAT_X_ASSUM ``deriv D1 D1'`` (ASSUME_TAC o (MATCH_MP derivOne)) 665 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP (Q.ISPEC `deriv` RTC_SINGLE)) 666 o (SPECL [``S :'a Sequent``, ``R :Rule``])) 667 >> IMP_RES_TAC (Q.ISPEC `deriv` (REWRITE_RULE [transitive_def] RTC_TRANSITIVE))); 668 669val DerivLeft = store_thm ("DerivLeft", 670 ``!S R D D1 D1'. Deriv D1 D1' ==> Deriv (Der S R [D1; D]) (Der S R [D1'; D])``, 671 NTAC 3 GEN_TAC 672 >> REWRITE_TAC [Deriv_def] 673 >> HO_MATCH_MP_TAC RTC_INDUCT 674 >> REPEAT STRIP_TAC (* 2 sub-goals here, first one is easy *) 675 >- REWRITE_TAC [RTC_REFL] 676 >> PAT_X_ASSUM ``deriv D1 D1'`` (ASSUME_TAC o (MATCH_MP derivLeft)) 677 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP (Q.ISPEC `deriv` RTC_SINGLE)) o (Q.SPECL [`S`, `R`, `D`])) 678 >> IMP_RES_TAC (Q.ISPEC `deriv` (REWRITE_RULE [transitive_def] RTC_TRANSITIVE))); 679 680val DerivRight = store_thm ("DerivRight", 681 ``!S R D D2 D2'. Deriv D2 D2' ==> Deriv (Der S R [D; D2]) (Der S R [D; D2'])``, 682 NTAC 3 GEN_TAC 683 >> REWRITE_TAC [Deriv_def] 684 >> HO_MATCH_MP_TAC RTC_INDUCT 685 >> REPEAT STRIP_TAC (* 2 sub-goals here, first one is easy *) 686 >- REWRITE_TAC [RTC_REFL] 687 >> PAT_X_ASSUM ``deriv D1 D1'`` (ASSUME_TAC o (MATCH_MP derivRight)) 688 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP (Q.ISPEC `deriv` RTC_SINGLE)) o (Q.SPECL [`S`, `R`, `D`])) 689 >> IMP_RES_TAC (Q.ISPEC `deriv` (REWRITE_RULE [transitive_def] RTC_TRANSITIVE))); 690 691val DerivBoth = store_thm ("DerivBoth", 692 ``!S R D2 D2' D1 D1'. Deriv D1 D1' ==> Deriv D2 D2' 693 ==> Deriv (Der S R [D1; D2]) (Der S R [D1'; D2'])``, 694 NTAC 4 GEN_TAC 695 >> REWRITE_TAC [Deriv_def] 696 >> HO_MATCH_MP_TAC RTC_INDUCT 697 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 698 >| [ (* goal 1 (of 2) *) 699 POP_ASSUM MP_TAC \\ 700 Q.SPEC_TAC (`D2'`, `D2'`) \\ 701 Q.SPEC_TAC (`D2`, `D2`) \\ 702 HO_MATCH_MP_TAC RTC_INDUCT \\ 703 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 704 [ (* goal 1.1 (of 2) *) 705 REWRITE_TAC [RTC_REFL], 706 (* goal 1.2 (of 2) *) 707 PAT_X_ASSUM ``deriv D2 D2'`` (ASSUME_TAC o (MATCH_MP derivRight)) \\ 708 POP_ASSUM (ASSUME_TAC o (MATCH_MP (Q.ISPEC `deriv` RTC_SINGLE)) 709 o (Q.SPECL [`S`, `R`, `D1`])) \\ 710 IMP_RES_TAC (Q.ISPEC `deriv` (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)) ], 711 (* goal 2 (of 2) *) 712 RES_TAC \\ 713 PAT_X_ASSUM ``deriv D1 D1'`` (ASSUME_TAC o (MATCH_MP derivLeft)) \\ 714 POP_ASSUM (ASSUME_TAC o (MATCH_MP (Q.ISPEC `deriv` RTC_SINGLE)) 715 o (Q.SPECL [`S`, `R`, `D2`])) \\ 716 IMP_RES_TAC (Q.ISPEC `deriv` (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)) ]); 717 718(* All Deriv rules *) 719val Deriv_rules = save_thm ("Deriv_rules", 720 LIST_CONJ [ DerivSeqAxiom, DerivRightSlash, DerivRightBackslash, DerivRightDot, 721 DerivLeftSlash, DerivLeftBackslash, DerivLeftDot, 722 DerivCutRule, DerivSeqExt, 723 DerivOne, DerivLeft, DerivRight, DerivBoth, 724 Deriv_refl, Deriv_trans ]); 725 726(* Inductively define a "finished" proof *) 727val (Proof_rules, Proof_ind, Proof_cases) = Hol_reln ` 728 (!S R. Proof (Der S R [])) /\ 729 (!S R D. Proof D ==> Proof (Der S R [D])) /\ 730 (!S R D1 D2. Proof D1 /\ Proof D2 ==> Proof (Der S R [D1; D2]))`; 731 732val [ProofZero, ProofOne, ProofTwo] = 733 map save_thm 734 (combine (["ProofZero", "ProofOne", "ProofTwo"], CONJUNCTS Proof_rules)); 735 736(* Derivations starting from "Unf" are not finished! *) 737val notProofUnf = store_thm ( 738 "notProofUnf", 739 ``!S. ~Proof (Unf S)``, 740 GEN_TAC 741 >> ONCE_REWRITE_TAC [Proof_cases] 742 >> rw []); 743 744(* Now we make a connection between our derivation proofs and gentzenSequent relation *) 745 746(* the easy direction (completeness) *) 747val gentzenToDeriv = store_thm ( 748 "gentzenToDeriv", 749 ``!E Gamma A. gentzenSequent E Gamma A 750 ==> (?D. Deriv (Unf (Sequent E Gamma A)) D /\ Proof D)``, 751 Induct_on `gentzenSequent` 752 >> REPEAT STRIP_TAC (* 9 sub-goals here *) 753 >| [ (* goal 1 (of 9) *) 754 EXISTS_TAC ``(Der (Sequent E (OneForm A) A) SeqAxiom [])`` \\ 755 REWRITE_TAC [DerivSeqAxiom, Proof_rules], 756 (* goal 2 (of 9) *) 757 EXISTS_TAC ``(Der (Sequent E Gamma (Slash A B)) RightSlash [D])`` \\ 758 CONJ_TAC >| (* 2 sub-goals here *) 759 [ (* goal 2.1 (of 2) *) 760 ASSUME_TAC (SPEC_ALL DerivRightSlash) \\ 761 PAT_X_ASSUM ``Deriv (Unf (Sequent E (Comma Gamma (OneForm B)) A)) D`` 762 (ASSUME_TAC o (MATCH_MP DerivOne)) \\ 763 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`Sequent E Gamma (Slash A B)`, `RightSlash`])) \\ 764 IMP_RES_TAC Deriv_trans, 765 (* goal 2.2 (of 2) *) 766 POP_ASSUM MP_TAC \\ 767 REWRITE_TAC [ProofOne] ], 768 (* goal 3 (of 9) *) 769 EXISTS_TAC ``(Der (Sequent E Gamma (Backslash B A)) RightBackslash [D])`` \\ 770 CONJ_TAC >| (* 2 sub-goals here *) 771 [ (* goal 3.1 (of 2) *) 772 ASSUME_TAC (SPEC_ALL DerivRightBackslash) \\ 773 PAT_X_ASSUM ``Deriv (Unf (Sequent E (Comma (OneForm B) Gamma) A)) D`` 774 (ASSUME_TAC o (MATCH_MP DerivOne)) \\ 775 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`Sequent E Gamma (Backslash B A)`, `RightBackslash`])) \\ 776 IMP_RES_TAC Deriv_trans, 777 (* goal 3.2 (of 2) *) 778 POP_ASSUM MP_TAC \\ 779 REWRITE_TAC [ProofOne] ], 780 (* goal 4 (of 9) *) 781 EXISTS_TAC ``(Der (Sequent E (Comma Gamma Gamma') (Dot A A')) RightDot [D; D'])`` \\ 782 CONJ_TAC >| (* 2 sub-goals here *) 783 [ (* goal 4.1 (of 2) *) 784 `Deriv (Der (Sequent E (Comma Gamma Gamma') (Dot A A')) RightDot 785 [ (Unf (Sequent E Gamma A)); (Unf (Sequent E Gamma' A')) ]) 786 (Der (Sequent E (Comma Gamma Gamma') (Dot A A')) RightDot [D; D'])` 787 by PROVE_TAC [DerivBoth] \\ 788 ASSUME_TAC (Q.SPECL [`E`, `Gamma`, `Gamma'`, `A`, `A'`] DerivRightDot) \\ 789 IMP_RES_TAC Deriv_trans, 790 (* goal 4.2 (of 2) *) 791 MATCH_MP_TAC ProofTwo >> ASM_REWRITE_TAC [] ], 792 (* goal 5 (of 9) *) 793 EXISTS_TAC ``(Der (Sequent E Gamma' A'') LeftSlash [D'; D])`` \\ 794 CONJ_TAC >| (* 2 sub-goals here *) 795 [ (* goal 5.1 (of 2) *) 796 `Deriv (Der (Sequent E Gamma' A'') LeftSlash 797 [ (Unf (Sequent E Gamma A'')); (Unf (Sequent E Gamma'' A')) ]) 798 (Der (Sequent E Gamma' A'') LeftSlash [D'; D])` 799 by PROVE_TAC [DerivBoth] \\ 800 ASSUME_TAC (Q.SPECL [`E`, `Gamma`, `Gamma'`, `Gamma''`, `A`, `A'`, `A''`] 801 DerivLeftSlash) \\ 802 RES_TAC >> IMP_RES_TAC Deriv_trans, 803 (* goal 5.2 (of 2) *) 804 MATCH_MP_TAC ProofTwo >> ASM_REWRITE_TAC [] ], 805 (* goal 6 (of 9) *) 806 EXISTS_TAC ``(Der (Sequent E Gamma' A'') LeftBackslash [D'; D])`` \\ 807 CONJ_TAC >| (* 2 sub-goals here *) 808 [ (* goal 6.1 (of 2) *) 809 `Deriv (Der (Sequent E Gamma' A'') LeftBackslash 810 [ (Unf (Sequent E Gamma A'')); (Unf (Sequent E Gamma'' A')) ]) 811 (Der (Sequent E Gamma' A'') LeftBackslash [D'; D])` 812 by PROVE_TAC [DerivBoth] \\ 813 ASSUME_TAC (Q.SPECL [`E`, `Gamma`, `Gamma'`, `Gamma''`, `A`, `A'`, `A''`] 814 DerivLeftBackslash) \\ 815 RES_TAC >> IMP_RES_TAC Deriv_trans, 816 (* goal 6.2 (of 2) *) 817 MATCH_MP_TAC ProofTwo >> ASM_REWRITE_TAC [] ], 818 (* goal 7 (of 9) *) 819 EXISTS_TAC ``(Der (Sequent E Gamma' A') LeftDot [D])`` \\ 820 CONJ_TAC >| (* 2 sub-goals here *) 821 [ (* goal 7.1 (of 2) *) 822 IMP_RES_TAC DerivLeftDot \\ 823 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`E`, `A'`])) \\ 824 PAT_X_ASSUM ``Deriv (Unf (Sequent E Gamma A')) D`` 825 (ASSUME_TAC o (MATCH_MP DerivOne)) \\ 826 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`Sequent E Gamma' A'`, `LeftDot`])) \\ 827 IMP_RES_TAC Deriv_trans, 828 (* goal 7.2 (of 2) *) 829 POP_ASSUM MP_TAC \\ 830 REWRITE_TAC [ProofOne] ], 831 (* goal 8 (of 9) *) 832 EXISTS_TAC ``(Der (Sequent E Gamma'' A') CutRule [D'; D])`` \\ 833 CONJ_TAC >| (* 2 sub-goals here *) 834 [ (* goal 8.1 (of 2) *) 835 IMP_RES_TAC DerivCutRule \\ 836 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`E`, `A'`])) \\ 837 `Deriv (Der (Sequent E Gamma'' A') CutRule 838 [ (Unf (Sequent E Gamma' A')); (Unf (Sequent E Gamma A)) ]) 839 (Der (Sequent E Gamma'' A') CutRule [D'; D])` 840 by PROVE_TAC [DerivBoth] \\ 841 IMP_RES_TAC Deriv_trans, 842 (* goal 8.2 (of 2) *) 843 MATCH_MP_TAC ProofTwo >> ASM_REWRITE_TAC [] ], 844 (* goal 9 (of 9) *) 845 EXISTS_TAC ``(Der (Sequent E Gamma' A) SeqExt [D])`` \\ 846 CONJ_TAC >| (* 2 sub-goals here *) 847 [ (* goal 9.1 (of 2) *) 848 IMP_RES_TAC DerivOne \\ 849 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`(Sequent E Gamma' A)`, `SeqExt`])) \\ 850 `Deriv (Unf (Sequent E Gamma' A)) 851 (Der (Sequent E Gamma' A) SeqExt [Unf (Sequent E Gamma A)])` 852 by PROVE_TAC [DerivSeqExt] \\ 853 IMP_RES_TAC Deriv_trans, 854 (* goal 9.2 (of 2) *) 855 POP_ASSUM MP_TAC \\ 856 REWRITE_TAC [ProofOne] ] ]); 857 858(******************************************************************************) 859(* *) 860(* Sub-formula properties in cut-free proofs *) 861(* *) 862(******************************************************************************) 863 864val subFormulaPropertyOne = store_thm ( 865 "subFormulaPropertyOne", 866 ``!q p. subProofOne q p ==> 867 extensionSub (exten p) ==> 868 CutFreeProof p ==> 869 !x. (subFormTerm x (prems q) \/ subFormula x (concl q)) ==> 870 (subFormTerm x (prems p) \/ subFormula x (concl p))``, 871 REPEAT GEN_TAC 872 >> NTAC 3 DISCH_TAC 873 >> GEN_TAC 874 >> DISCH_TAC 875 >> PAT_X_ASSUM ``subProofOne q p`` MP_TAC 876 >> ONCE_REWRITE_TAC [subProofOne_cases] 877 >> STRIP_TAC (* 12 sub-goals here *) 878 >| [ (* goal 1 (of 12) *) 879 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 880 ASM_REWRITE_TAC [prems_def, concl_def] \\ 881 STRIP_TAC >| (* 2 sub-goals here *) 882 [ (* goal 1.1 (of 2) *) 883 POP_ASSUM (MP_TAC o (MATCH_MP comSub)) >> rw [] >| (* 2 sub-goals here *) 884 [ (* goal 1.1.1 (of 2) *) 885 DISJ1_TAC >> ASM_REWRITE_TAC [], 886 (* goal 1.1.2 (of 2) *) 887 (* Removed due to oneFormSubEQ[simp]: 888 POP_ASSUM (ASSUME_TAC o (MATCH_MP oneFormSub)) \\ *) 889 POP_ASSUM (ASSUME_TAC o (Q.SPEC `A`) o (MATCH_MP slashR)) \\ 890 ASM_REWRITE_TAC [] ], 891 (* goal 1.2 (of 2) *) 892 DISJ2_TAC \\ 893 POP_ASSUM (ASSUME_TAC o (Q.SPEC `B`) o (MATCH_MP slashL)) \\ 894 ASM_REWRITE_TAC [] ], 895 (* goal 2 (of 12) *) 896 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 897 ASM_REWRITE_TAC [prems_def, concl_def] \\ 898 STRIP_TAC >| (* 2 sub-goals here *) 899 [ (* goal 2.1 (of 2) *) 900 POP_ASSUM (MP_TAC o (MATCH_MP comSub)) >> rw [] >| (* 2 sub-goals here *) 901 [ (* goal 2.1.1 (of 2) *) 902 (* Removed due to oneFormSubEQ[simp]: 903 POP_ASSUM (ASSUME_TAC o (MATCH_MP oneFormSub)) \\ *) 904 POP_ASSUM (ASSUME_TAC o (Q.SPEC `A`) o (MATCH_MP backslashL)) \\ 905 ASM_REWRITE_TAC [], 906 (* goal 2.1.2 (of 2) *) 907 DISJ1_TAC >> ASM_REWRITE_TAC [] ], 908 (* goal 2.2 (of 2) *) 909 DISJ2_TAC \\ 910 POP_ASSUM (ASSUME_TAC o (Q.SPEC `B`) o (MATCH_MP backslashR)) \\ 911 ASM_REWRITE_TAC [] ], 912 (* goal 3 (of 12) *) 913 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 914 ASM_REWRITE_TAC [prems_def, concl_def] \\ 915 STRIP_TAC >| (* 2 sub-goals here *) 916 [ (* goal 3.1 (of 2) *) 917 DISJ1_TAC \\ 918 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Delta`) o (MATCH_MP comL)) \\ 919 ASM_REWRITE_TAC [], 920 (* goal 3.2 (of 2) *) 921 DISJ2_TAC \\ 922 POP_ASSUM (ASSUME_TAC o (Q.SPEC `B`) o (MATCH_MP dotL)) \\ 923 ASM_REWRITE_TAC [] ], 924 (* goal 4 (of 12) *) 925 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 926 ASM_REWRITE_TAC [prems_def, concl_def] \\ 927 STRIP_TAC >| (* 2 sub-goals here *) 928 [ (* goal 4.1 (of 2) *) 929 DISJ1_TAC \\ 930 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Gamma`) o (MATCH_MP comR)) \\ 931 ASM_REWRITE_TAC [], 932 (* goal 4.2 (of 2) *) 933 DISJ2_TAC \\ 934 POP_ASSUM (ASSUME_TAC o (Q.SPEC `A`) o (MATCH_MP dotR)) \\ 935 ASM_REWRITE_TAC [] ], 936 (* goal 5 (of 12) *) 937 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 938 ASM_REWRITE_TAC [prems_def, concl_def] \\ 939 STRIP_TAC >| (* 2 sub-goals here *) 940 [ (* goal 5.1 (of 2) *) 941 DISJ1_TAC \\ 942 IMP_RES_TAC subReplace2 \\ 943 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 944 POP_ASSUM (ASSUME_TAC o (SPEC ``(OneForm (Slash A B))``) o (MATCH_MP comR)) \\ 945 DISCH_TAC >> RES_TAC, 946 (* goal 5.2 (of 2) *) 947 DISJ1_TAC \\ 948 IMP_RES_TAC subReplace2 \\ 949 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 950 POP_ASSUM (ASSUME_TAC o (Q.SPEC `A`) o (MATCH_MP slashR)) \\ 951 POP_ASSUM (ASSUME_TAC o (MATCH_MP eqFT)) \\ 952 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Delta`) o (MATCH_MP comL)) \\ 953 DISCH_TAC >> RES_TAC ], 954 (* goal 6 (of 12) *) 955 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 956 ASM_REWRITE_TAC [prems_def, concl_def] \\ 957 STRIP_TAC >| (* 2 sub-goals here *) 958 [ (* goal 6.1 (of 2) *) 959 IMP_RES_TAC subReplace3 >| (* 2 sub-goals here *) 960 [ (* goal 6.1.1 (of 2) *) 961 ASM_REWRITE_TAC [], 962 (* goal 6.1.2 (of 2) *) 963 IMP_RES_TAC subReplace2 \\ 964 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 965 POP_ASSUM (ASSUME_TAC o (MATCH_MP oneFormSub)) \\ 966 POP_ASSUM (ASSUME_TAC o (Q.SPEC `B`) o (MATCH_MP slashL)) \\ 967 POP_ASSUM (ASSUME_TAC o (MATCH_MP eqFT)) \\ 968 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Delta`) o (MATCH_MP comL)) \\ 969 DISCH_TAC >> RES_TAC >> ASM_REWRITE_TAC [] ], 970 (* goal 6.2 (of 2) *) 971 DISJ2_TAC >> ASM_REWRITE_TAC [] ], 972 (* goal 7 (of 12) *) 973 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 974 ASM_REWRITE_TAC [prems_def, concl_def] \\ 975 STRIP_TAC >| (* 2 sub-goals here *) 976 [ (* goal 7.1 (of 2) *) 977 DISJ1_TAC \\ 978 IMP_RES_TAC subReplace2 \\ 979 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 980 POP_ASSUM (ASSUME_TAC o (SPEC ``(OneForm (Backslash B A))``) o (MATCH_MP comL)) \\ 981 DISCH_TAC >> RES_TAC, 982 (* goal 7.2 (of 2) *) 983 DISJ1_TAC \\ 984 IMP_RES_TAC subReplace2 \\ 985 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 986 POP_ASSUM (ASSUME_TAC o (Q.SPEC `A`) o (MATCH_MP backslashL)) \\ 987 POP_ASSUM (ASSUME_TAC o (MATCH_MP eqFT)) \\ 988 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Delta`) o (MATCH_MP comR)) \\ 989 DISCH_TAC >> RES_TAC ], 990 (* goal 8 (of 12) *) 991 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 992 ASM_REWRITE_TAC [prems_def, concl_def] \\ 993 STRIP_TAC >| (* 2 sub-goals here *) 994 [ (* goal 8.1 (of 2) *) 995 IMP_RES_TAC subReplace3 >| (* 2 sub-goals here *) 996 [ (* goal 8.1.1 (of 2) *) 997 ASM_REWRITE_TAC [], 998 (* goal 8.1.2 (of 2) *) 999 IMP_RES_TAC subReplace2 \\ 1000 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 1001 POP_ASSUM (ASSUME_TAC o (MATCH_MP oneFormSub)) \\ 1002 POP_ASSUM (ASSUME_TAC o (Q.SPEC `B`) o (MATCH_MP backslashR)) \\ 1003 POP_ASSUM (ASSUME_TAC o (MATCH_MP eqFT)) \\ 1004 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Delta`) o (MATCH_MP comR)) \\ 1005 DISCH_TAC >> RES_TAC >> ASM_REWRITE_TAC [] ], 1006 (* goal 8.2 (of 2) *) 1007 DISJ2_TAC >> ASM_REWRITE_TAC [] ], 1008 (* goal 9 (of 12) *) 1009 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 1010 ASM_REWRITE_TAC [prems_def, concl_def] \\ 1011 STRIP_TAC >| (* 2 sub-goals here *) 1012 [ (* goal 9.1 (of 2) *) 1013 IMP_RES_TAC subReplace3 >| (* 2 sub-goals here *) 1014 [ (* goal 9.1.1 (of 2) *) 1015 ASM_REWRITE_TAC [], 1016 (* goal 9.1.2 (of 2) *) 1017 IMP_RES_TAC subReplace2 \\ 1018 POP_ASSUM (MP_TAC o (Q.SPEC `x`)) \\ 1019 POP_ASSUM (MP_TAC o (MATCH_MP comSub)) \\ 1020 STRIP_TAC >| (* 2 sub-goals here *) 1021 [ (* goal 9.1.2.1 (of 2) *) 1022 POP_ASSUM (ASSUME_TAC o (MATCH_MP oneFormSub)) \\ 1023 POP_ASSUM (ASSUME_TAC o (Q.SPEC `B`) o (MATCH_MP dotL)) \\ 1024 POP_ASSUM (ASSUME_TAC o (MATCH_MP eqFT)) \\ 1025 DISCH_TAC >> RES_TAC >> ASM_REWRITE_TAC [], 1026 (* goal 9.1.2.2 (of 2) *) 1027 POP_ASSUM (ASSUME_TAC o (MATCH_MP oneFormSub)) \\ 1028 POP_ASSUM (ASSUME_TAC o (Q.SPEC `A`) o (MATCH_MP dotR)) \\ 1029 POP_ASSUM (ASSUME_TAC o (MATCH_MP eqFT)) \\ 1030 DISCH_TAC >> RES_TAC \\ 1031 ASM_REWRITE_TAC [] ] ], 1032 (* goal 9.2 (of 2) *) 1033 DISJ2_TAC >> ASM_REWRITE_TAC [] ], 1034 (* goal 10 (of 12) *) 1035 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 1036 ASM_REWRITE_TAC [prems_def, concl_def] \\ 1037 STRIP_TAC \\ (* 2 sub-goals here, sharing the same tactical *) 1038 METIS_TAC [notCutFree], 1039 (* goal 11 (of 12) *) 1040 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 1041 ASM_REWRITE_TAC [prems_def, concl_def] \\ 1042 STRIP_TAC \\ (* 2 sub-goals here, sharing the same tactical *) 1043 METIS_TAC [notCutFree], 1044 (* goal 12 (of 12) *) 1045 PAT_X_ASSUM ``subFormTerm x (prems q) \/ subFormula x (concl q)`` MP_TAC \\ 1046 ASM_REWRITE_TAC [prems_def, concl_def] \\ 1047 STRIP_TAC >| (* 2 sub-goals here, sharing the same tactical *) 1048 [ (* goal 12.1 (of 2) *) 1049 IMP_RES_TAC subReplace3 >- ASM_REWRITE_TAC [] \\ 1050 DISJ1_TAC >> IMP_RES_TAC subReplace2 \\ 1051 POP_ASSUM (ASSUME_TAC o (Q.SPEC `x`)) \\ 1052 `extensionSub E` by METIS_TAC [exten_def] \\ 1053 IMP_RES_TAC extensionSub_def >> RES_TAC, 1054 (* goal 12.2 (of 2) *) 1055 DISJ2_TAC >> ASM_REWRITE_TAC [] ] ]); 1056 1057(* original statements in the Coq version *) 1058val subFormulaPropertyOne' = store_thm ( 1059 "subFormulaPropertyOne'", 1060 ``!Gamma1 Gamma2 B C x E p q. 1061 (p = Der (Sequent E Gamma1 B) _ _) ==> 1062 (q = Der (Sequent E Gamma2 C) _ _) ==> 1063 extensionSub E ==> 1064 subProofOne q p ==> 1065 CutFreeProof p ==> 1066 (subFormTerm x Gamma2 \/ subFormula x C) ==> 1067 (subFormTerm x Gamma1 \/ subFormula x B)``, 1068 REPEAT GEN_TAC 1069 >> NTAC 5 STRIP_TAC 1070 >> `Gamma1 = prems p` by PROVE_TAC [prems_def] 1071 >> `Gamma2 = prems q` by PROVE_TAC [prems_def] 1072 >> `B = concl p` by PROVE_TAC [concl_def] 1073 >> `C = concl q` by PROVE_TAC [concl_def] 1074 >> `E = exten p` by PROVE_TAC [exten_def] 1075 >> `extensionSub (exten p)` by PROVE_TAC [] 1076 >> ONCE_ASM_REWRITE_TAC [] 1077 >> METIS_TAC [subFormulaPropertyOne]); 1078 1079val subFormulaProperty = store_thm ( 1080 "subFormulaProperty", 1081 ``!q p. subProof q p ==> 1082 extensionSub (exten p) ==> 1083 CutFreeProof p ==> 1084 !x. (subFormTerm x (prems q) \/ subFormula x (concl q)) ==> 1085 (subFormTerm x (prems p) \/ subFormula x (concl p))``, 1086 HO_MATCH_MP_TAC subProof_strongind 1087 >> STRIP_TAC >- rw [] 1088 >> fix [`p3`, `p2`, `p1`] 1089 >> set [`T1 = prems p1`, `T2 = prems p2`, `T3 = prems p3`, 1090 `A1 = concl p1`, `A2 = concl p2`, `A3 = concl p3`, 1091 `E = exten p1`] 1092 >> PURE_ONCE_REWRITE_TAC [] 1093 >> NTAC 4 STRIP_TAC >> DISCH_TAC 1094 >> `subFormTerm x T2 \/ subFormula x A2 ==> 1095 subFormTerm x T1 \/ subFormula x A1` by METIS_TAC [] 1096 >> `CutFreeProof p2` by METIS_TAC [CutFreeSubProof] 1097 >> `extensionSub (exten p2)` by METIS_TAC [subProof_extension] 1098 >> `subFormTerm x T2 \/ subFormula x A2` 1099 by METIS_TAC [subFormulaPropertyOne] 1100 >> METIS_TAC []); 1101 1102(* original statements in the Coq version *) 1103val subFormulaProperty' = store_thm ( 1104 "subFormulaProperty'", 1105 ``!Gamma1 Gamma2 B C x E p q. 1106 (p = Der (Sequent E Gamma1 B) _ _) ==> 1107 (q = Der (Sequent E Gamma2 C) _ _) ==> 1108 extensionSub E ==> 1109 subProof q p ==> 1110 CutFreeProof p ==> 1111 (subFormTerm x Gamma2 \/ subFormula x C) ==> 1112 (subFormTerm x Gamma1 \/ subFormula x B)``, 1113 REPEAT GEN_TAC 1114 >> NTAC 5 STRIP_TAC 1115 >> `Gamma1 = prems p` by PROVE_TAC [prems_def] 1116 >> `Gamma2 = prems q` by PROVE_TAC [prems_def] 1117 >> `B = concl p` by PROVE_TAC [concl_def] 1118 >> `C = concl q` by PROVE_TAC [concl_def] 1119 >> `E = exten p` by PROVE_TAC [exten_def] 1120 >> `extensionSub (exten p)` by PROVE_TAC [] 1121 >> ONCE_ASM_REWRITE_TAC [] 1122 >> METIS_TAC [subFormulaProperty]); 1123 1124val _ = export_theory (); 1125val _ = html_theory "CutFree"; 1126 1127(* last updated: April 25, 2017 *) 1128