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 pred_setTheory pairTheory listTheory arithmeticTheory integerTheory; 28open relationTheory; 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 "Lambek"; 46 47(******************************************************************************) 48(* *) 49(* Module: Form *) 50(* *) 51(******************************************************************************) 52 53val _ = Datatype `Form = At 'a | Slash Form Form | Backslash Form Form | Dot Form Form`; 54 55val _ = overload_on ("*", ``Dot``); (* \HOLTokenProd *) 56val _ = overload_on ("/", ``Slash``); 57val _ = overload_on ("\\\\", ``Backslash``); 58val _ = set_fixity "\\\\" (Infixr 1500); 59val _ = TeX_notation { hol = "\\\\", TeX = ("\\HOLTokenBackslash", 1) }; 60 61val Form_induction = TypeBase.induction_of ``:'a Form``; 62val Form_nchotomy = TypeBase.nchotomy_of ``:'a Form``; 63val Form_distinct = TypeBase.distinct_of ``:'a Form``; 64val Form_distinct' = save_thm ("Form_distinct'", GSYM Form_distinct); 65val Form_11 = TypeBase.one_one_of ``:'a Form``; 66 67val _ = type_abbrev ("arrow_extension", ``:'a Form -> 'a Form -> bool``); 68 69(* Rules of Lambek's "Syntactic Calculus" (non-associative + extension) *) 70val (arrow_rules, arrow_ind, arrow_cases) = Hol_reln ` 71 (!X A. arrow X A A) /\ (* one *) 72 (!X A B C. arrow X (Dot A B) C ==> arrow X A (Slash C B)) /\ (* beta *) 73 (!X A B C. arrow X A (Slash C B) ==> arrow X (Dot A B) C) /\ (* beta' *) 74 (!X A B C. arrow X (Dot A B) C ==> arrow X B (Backslash A C)) /\ (* gamma *) 75 (!X A B C. arrow X B (Backslash A C) ==> arrow X (Dot A B) C) /\ (* gamma' *) 76 (!X A B C. arrow X A B /\ arrow X B C ==> arrow X A C) /\ (* comp *) 77 (!(X :'a arrow_extension) A B. X A B ==> arrow X A B) `; (* arrow_plus *) 78 79val [one, beta, beta', gamma, gamma', comp, arrow_plus] = 80 map save_thm 81 (combine (["one", "beta", "beta'", "gamma", "gamma'", "comp", "arrow_plus"], 82 CONJUNCTS arrow_rules)); 83 84val beta_EQ = store_thm ("beta_EQ", 85 ``!X A B C. arrow X A (Slash C B) = arrow X (Dot A B) C``, 86 REPEAT STRIP_TAC 87 >> EQ_TAC 88 >| [ REWRITE_TAC [beta'], 89 REWRITE_TAC [beta] ]); 90 91val gamma_EQ = store_thm ("gamma_EQ", 92 ``!X A B C. arrow X B (Backslash A C) = arrow X (Dot A B) C``, 93 REPEAT STRIP_TAC 94 >> EQ_TAC 95 >| [ REWRITE_TAC [gamma'], 96 REWRITE_TAC [gamma] ]); 97 98val arrow_transitive = store_thm ( 99 "arrow_transitive", ``!X. transitive (arrow X)``, 100 REWRITE_TAC [transitive_def, comp]); 101 102val arrow_reflexive = store_thm ( 103 "arrow_reflexive", ``!X. reflexive (arrow X)``, 104 REWRITE_TAC [reflexive_def, one]); 105 106(** The arrow relationship and its extensions (like associativity, commutativity etc.) **) 107 108val _ = overload_on("add_extension", ``relation$RUNION``); 109(* X extends (to) X', or X is extended to X' *) 110val _ = overload_on("extends", ``relation$RSUBSET``); 111 112val no_extend = store_thm ("no_extend", ``!X. extends X X``, 113 RW_TAC bool_ss [RSUBSET]); 114 115val add_extend_l = store_thm ("add_extend_l", ``!X X'. extends X (add_extension X X')``, 116 RW_TAC bool_ss [RSUBSET, RUNION]); 117 118val add_extend_r = store_thm ("add_extend_r", ``!X X'. extends X' (add_extension X X')``, 119 RW_TAC bool_ss [RSUBSET, RUNION]); 120 121val extends_trans = store_thm ("extends_trans", 122 ``!X Y Z. extends X Y /\ extends Y Z ==> extends X Z``, 123 RW_TAC bool_ss [RSUBSET]); 124 125val extends_transitive = store_thm ( 126 "extends_transitive", ``transitive extends``, 127 REWRITE_TAC [transitive_def, extends_trans]); 128 129(** most popular extensions **) 130 131val NL_def = Define `(NL :'a arrow_extension) = EMPTY_REL`; 132 133(* L is defined by two rules, and it's reflexitive *) 134val (L_rules, L_ind, L_cases) = Hol_reln ` 135 (!A B C. L (Dot A (Dot B C)) (Dot (Dot A B) C)) /\ 136 (!A B C. L (Dot (Dot A B) C) (Dot A (Dot B C)))`; 137 138val [L_rule_rl, L_rule_lr] = 139 map save_thm (combine (["L_rule_rl", "L_rule_lr"], CONJUNCTS L_rules)); 140 141(* NLP is defined by only one rule, it's reflexitive too. *) 142val (NLP_rules, NLP_ind, NLP_cases) = Hol_reln ` 143 (!A B. NLP (Dot A B) (Dot B A))`; 144 145val LP_def = Define `LP = add_extension NLP L`; 146 147val NLextendsAll = store_thm ( 148 "NLextendsAll", ``!X. extends NL X``, 149 RW_TAC bool_ss [NL_def, EMPTY_REL_DEF, RSUBSET]); 150 151val NLPextendsLP = store_thm ("NLPextendsLP", ``extends NLP LP``, 152 REWRITE_TAC [LP_def, add_extend_l]); 153 154val LextendsLP = store_thm ("LextendsLP", ``extends L LP``, 155 REWRITE_TAC [LP_def, add_extend_r]); 156 157(* Some derived rules for arrow. 158 Note: all theorems here can be simply proved by PROVE_TAC [arrow_rules]. *) 159 160val Dot_mono_right = store_thm ("Dot_mono_right", 161 ``!X A B B'. arrow X B' B ==> arrow X (Dot A B') (Dot A B)``, 162 REPEAT STRIP_TAC 163 >> MATCH_MP_TAC gamma' 164 >> MATCH_MP_TAC comp 165 >> Q.EXISTS_TAC `B` 166 >> CONJ_TAC 167 >- ASM_REWRITE_TAC [] 168 >> MATCH_MP_TAC gamma 169 >> RW_TAC bool_ss [one]); 170 171val Dot_mono_left = store_thm ("Dot_mono_left", 172 ``!X A B A'. arrow X A' A ==> arrow X (Dot A' B) (Dot A B)``, 173 REPEAT STRIP_TAC 174 >> MATCH_MP_TAC beta' 175 >> MATCH_MP_TAC comp 176 >> Q.EXISTS_TAC `A` 177 >> CONJ_TAC 178 >- ASM_REWRITE_TAC [] 179 >> MATCH_MP_TAC beta 180 >> RW_TAC bool_ss [one]); 181 182val Dot_mono = store_thm ("Dot_mono", 183 ``!X A B C D. arrow X A C /\ arrow X B D ==> arrow X (Dot A B) (Dot C D)``, 184 REPEAT STRIP_TAC 185 >> MATCH_MP_TAC comp 186 >> EXISTS_TAC ``(Dot C B)`` 187 >> CONJ_TAC 188 >| [ MATCH_MP_TAC Dot_mono_left >> RW_TAC bool_ss [], 189 MATCH_MP_TAC Dot_mono_right >> RW_TAC bool_ss [] ]); 190 191val Slash_mono_left = store_thm ("Slash_mono_left", 192 ``!X C B C'. arrow X C' C ==> arrow X (Slash C' B) (Slash C B)``, 193 REPEAT STRIP_TAC 194 >> MATCH_MP_TAC beta 195 >> MATCH_MP_TAC comp 196 >> Q.EXISTS_TAC `C'` 197 >> CONJ_TAC 198 >| [ MATCH_MP_TAC beta' >> RW_TAC bool_ss [one], 199 RW_TAC bool_ss [] ]); 200 201val Slash_antimono_right = store_thm ("Slash_antimono_right", 202 ``!X C B B'. arrow X B' B ==> arrow X (Slash C B) (Slash C B')``, 203 REPEAT STRIP_TAC 204 >> MATCH_MP_TAC beta 205 >> MATCH_MP_TAC gamma' 206 >> MATCH_MP_TAC comp 207 >> Q.EXISTS_TAC `B` 208 >> CONJ_TAC 209 >- ASM_REWRITE_TAC [] 210 >> MATCH_MP_TAC gamma 211 >> MATCH_MP_TAC beta' 212 >> RW_TAC bool_ss [one]); 213 214val Backslash_antimono_left = store_thm ("Backslash_antimono_left", 215 ``!X A C A'. arrow X A A' ==> arrow X (Backslash A' C) (Backslash A C)``, 216 REPEAT STRIP_TAC 217 >> MATCH_MP_TAC gamma 218 >> MATCH_MP_TAC beta' 219 >> MATCH_MP_TAC comp 220 >> Q.EXISTS_TAC `A'` 221 >> CONJ_TAC 222 >- ASM_REWRITE_TAC [] 223 >> MATCH_MP_TAC beta 224 >> MATCH_MP_TAC gamma' 225 >> RW_TAC bool_ss [one]); 226 227val Backslash_mono_right = store_thm ("Backslash_mono_right", 228 ``!X A C C'. arrow X C' C ==> arrow X (Backslash A C') (Backslash A C)``, 229 REPEAT STRIP_TAC 230 >> MATCH_MP_TAC gamma 231 >> MATCH_MP_TAC comp 232 >> Q.EXISTS_TAC `C'` 233 >> CONJ_TAC 234 >| [ MATCH_MP_TAC beta' \\ 235 MATCH_MP_TAC beta \\ 236 MATCH_MP_TAC gamma' \\ 237 RW_TAC bool_ss [one], 238 ASM_REWRITE_TAC [] ]); 239 240val mono_X = store_thm ("mono_X", 241 ``!X' X A B. arrow X A B ==> extends X X' ==> arrow X' A B``, 242 GEN_TAC 243 >> Induct_on `arrow` 244 >> REPEAT STRIP_TAC (* 7 sub-goals here *) 245 >- REWRITE_TAC [one] 246 >- RW_TAC bool_ss [beta] 247 >- RW_TAC bool_ss [beta'] 248 >- RW_TAC bool_ss [gamma] 249 >- RW_TAC bool_ss [gamma'] 250 >- PROVE_TAC [comp] 251 >> PROVE_TAC [arrow_plus, RSUBSET]); 252 253val pi = store_thm ("pi", 254 ``!X. extends NLP X ==> !A B. arrow X (Dot A B) (Dot B A)``, 255 REPEAT STRIP_TAC 256 >> `NLP (Dot A B) (Dot B A)` by REWRITE_TAC [NLP_rules] 257 >> `arrow NLP (Dot A B) (Dot B A)` by RW_TAC bool_ss [arrow_plus] 258 >> PROVE_TAC [mono_X]); 259 260val pi_NLP = store_thm ("pi_NLP", ``!A B. arrow NLP (Dot A B) (Dot B A)``, 261 MATCH_MP_TAC pi 262 >> REWRITE_TAC [no_extend]); 263 264val pi_LP = store_thm ("pi_LP", ``!A B. arrow LP (Dot A B) (Dot B A)``, 265 MATCH_MP_TAC pi 266 >> REWRITE_TAC [NLPextendsLP]); 267 268val alfa = store_thm ("alfa", 269 ``!X. extends L X ==> !A B C. arrow X (Dot A (Dot B C)) (Dot (Dot A B) C)``, 270 REPEAT STRIP_TAC 271 >> `L (Dot A (Dot B C)) (Dot (Dot A B) C)` 272 by REWRITE_TAC [L_rule_rl] 273 >> `arrow L (Dot A (Dot B C)) (Dot (Dot A B) C)` 274 by RW_TAC bool_ss [arrow_plus] 275 >> PROVE_TAC [mono_X]); 276 277val alfa_L = store_thm ("alfa_L", 278 ``!A B C. arrow L (Dot A (Dot B C)) (Dot (Dot A B) C)``, 279 MATCH_MP_TAC alfa 280 >> REWRITE_TAC [no_extend]); 281 282val alfa_LP = store_thm ("alfa_LP", 283 ``!A B C. arrow LP (Dot A (Dot B C)) (Dot (Dot A B) C)``, 284 MATCH_MP_TAC alfa 285 >> REWRITE_TAC [LextendsLP]); 286 287val alfa' = store_thm ("alfa'", 288 ``!X. extends L X ==> !A B C. arrow X (Dot (Dot A B) C) (Dot A (Dot B C))``, 289 REPEAT STRIP_TAC 290 >> `L (Dot (Dot A B) C) (Dot A (Dot B C))` by REWRITE_TAC [L_rule_lr] 291 >> `arrow L (Dot (Dot A B) C) (Dot A (Dot B C))` by RW_TAC bool_ss [arrow_plus] 292 >> PROVE_TAC [mono_X]); 293 294val alfa'_L = store_thm ("alfa'_L", 295 ``!A B C. arrow L (Dot (Dot A B) C) (Dot A (Dot B C))``, 296 MATCH_MP_TAC alfa' 297 >> REWRITE_TAC [no_extend]); 298 299val alfa'_LP = store_thm ("alfa'_LP", 300 ``!A B C. arrow LP (Dot (Dot A B) C) (Dot A (Dot B C))``, 301 MATCH_MP_TAC alfa' 302 >> REWRITE_TAC [LextendsLP]); 303 304(******************************************************************************) 305(* *) 306(* L rules *) 307(* *) 308(******************************************************************************) 309 310val L_a = store_thm ("L_a", ``!x. arrow L x x``, REWRITE_TAC [one]); 311val L_b = store_thm ("L_b", ``!x y z. arrow L (Dot (Dot x y) z) (Dot x (Dot y z))``, 312 REWRITE_TAC [alfa'_L]); 313val L_b' = store_thm ("L_b'", ``!x y z. arrow L (Dot x (Dot y z)) (Dot (Dot x y) z)``, 314 REWRITE_TAC [alfa_L, alfa'_L]); 315val L_c = store_thm ("L_c", ``!x y z. arrow L (Dot x y) z ==> arrow L x (Slash z y)``, 316 REWRITE_TAC [beta]); 317val L_c' = store_thm ("L_c'", ``!x y z. arrow L (Dot x y) z ==> arrow L y (Backslash x z)``, 318 REWRITE_TAC [gamma]); 319val L_d = store_thm ("L_d", ``!x y z. arrow L x (Slash z y) ==> arrow L (Dot x y) z``, 320 REWRITE_TAC [beta']); 321val L_d' = store_thm ("L_d'", ``!x y z. arrow L y (Backslash x z) ==> arrow L (Dot x y) z``, 322 REWRITE_TAC [gamma']); 323val L_e = store_thm ("L_e", ``!x y z. arrow L x y /\ arrow L y z ==> arrow L x z``, 324 REWRITE_TAC [comp]); 325 326val L_arrow_rules = save_thm ( 327 "L_arrow_rules", LIST_CONJ [L_a, L_b, L_b', L_c, L_c', L_d, L_d', L_e]); 328 329local 330 val t = PROVE_TAC [L_arrow_rules] 331in 332 val L_f = store_thm ("L_f", ``!x y. arrow L x (Slash (Dot x y) y)``, t) 333 and L_g = store_thm ("L_g", ``!y z. arrow L (Dot (Slash z y) y) z``, t) 334 and L_h = store_thm ("L_h", ``!y z. arrow L y (Backslash (Slash z y) z)``, t) 335 and L_i = store_thm ("L_i", ``!x y z. arrow L (Dot (Slash z y) (Slash y x)) (Slash z x)``, t) 336 and L_j = store_thm ("L_j", ``!x y z. arrow L (Slash z y) (Slash (Slash z x) (Slash y x))``, t) 337 338 and L_k = store_thm ("L_k", ``!x y z. arrow L (Slash (Backslash x y) z) 339 (Backslash x (Slash y z))``, t) 340 341 and L_k' = store_thm ("L_k'", ``!x y z. arrow L (Backslash x (Slash y z)) 342 (Slash (Backslash x y) z)``, t) 343 344 and L_l = store_thm ("L_l", ``!x y z. arrow L (Slash (Slash x y) z) (Slash x (Dot z y))``, t) 345 and L_l' = store_thm ("L_l'", ``!x y z. arrow L (Slash x (Dot z y)) (Slash (Slash x y) z)``, t) 346 and L_m = store_thm ("L_m", ``!x x' y y'. arrow L x x' /\ arrow L y y' 347 ==> arrow L (Dot x y) (Dot x' y')``, t) 348 and L_n = store_thm ("L_n", ``!x x' y y'. arrow L x x' /\ arrow L y y' 349 ==> arrow L (Slash x y') (Slash x' y)``, t); 350 351 val L_arrow_rules_ex = save_thm ( 352 "L_arrow_rules_ex", LIST_CONJ [L_f, L_g, L_h, L_i, L_j, L_k, L_k', L_l, L_l', L_m, L_n]) 353end; 354 355local 356 val t = PROVE_TAC [L_a, L_c, L_c', L_d, L_d', L_e] (* L_b and L_b' are not used *) 357in 358 val L_dot_mono_r = store_thm ("L_dot_mono_r", 359 ``!A B B'. arrow L B B' ==> arrow L (Dot A B) (Dot A B')``, t) 360 and L_dot_mono_l = store_thm ("L_dot_mono_l", 361 ``!A B A'. arrow L A A' ==> arrow L (Dot A B) (Dot A' B)``, t) 362 and L_slash_mono_l = store_thm ("L_slash_mono_l", 363 ``!C B C'. arrow L C C' ==> arrow L (Slash C B) (Slash C' B)``, t) 364 and L_slash_antimono_r = store_thm ("L_slash_antimono_r", 365 ``!C B B'. arrow L B B' ==> arrow L (Slash C B') (Slash C B)``, t) 366 and L_backslash_antimono_l = store_thm ("L_backslash_antimono_l", 367 ``!A C A'. arrow L A A' ==> arrow L (Backslash A' C) (Backslash A C)``, t) 368 and L_backslash_mono_r = store_thm ("L_backslash_mono_r", 369 ``!A C'. arrow L C C' ==> arrow L (Backslash A C) (Backslash A C')``, t); 370 371 val L_arrow_rules_mono = save_thm ( 372 "L_arrow_rules_mono", 373 LIST_CONJ [L_dot_mono_r, L_dot_mono_l, 374 L_slash_mono_l, L_slash_antimono_r, 375 L_backslash_antimono_l, L_backslash_mono_r]) 376end; 377 378(******************************************************************************) 379(* *) 380(* Module: Terms *) 381(* *) 382(******************************************************************************) 383 384val _ = Datatype `Term = OneForm ('a Form) | Comma Term Term`; 385 386val Term_induction = TypeBase.induction_of ``:'a Term``; 387val Term_nchotomy = TypeBase.nchotomy_of ``:'a Term``; 388val Term_distinct = TypeBase.distinct_of ``:'a Term``; 389val Term_distinct' = save_thm ("Term_distinct'", GSYM Term_distinct); 390val Term_11 = TypeBase.one_one_of ``:'a Term``; 391 392val _ = type_abbrev ("gentzen_extension", ``:'a Term -> 'a Term -> bool``); 393 394(* Definition of the recursive function that translates Terms to Forms *) 395val deltaTranslation_def = Define ` 396 (deltaTranslation (OneForm f) = f) /\ 397 (deltaTranslation (Comma t1 t2) = Dot (deltaTranslation t1) (deltaTranslation t2))`; 398 399val deltaTranslationOneForm = store_thm ( 400 "deltaTranslationOneForm[simp]", 401 ``deltaTranslation (OneForm f) = f``, RW_TAC std_ss [deltaTranslation_def]); 402 403val deltaTranslationComma = store_thm ( 404 "deltaTranslationComma[simp]", 405 ``deltaTranslation (Comma t1 t2) = Dot (deltaTranslation t1) (deltaTranslation t2)``, 406 RW_TAC std_ss [deltaTranslation_def]); 407 408(* Non-associative extension, an empty relation actually *) 409val NL_Sequent_def = Define ` 410 (NL_Sequent :'a gentzen_extension) = EMPTY_REL`; 411 412(* NLP Sequent extension *) 413val (NLP_Sequent_rules, NLP_Sequent_ind, NLP_Sequent_cases) = Hol_reln ` 414 (!A B. NLP_Sequent (Comma A B) (Comma B A))`; 415 416val NLP_Intro = save_thm ("NLP_Intro", NLP_Sequent_rules); 417 418(* L Sequent extension, the Full Lambek Sequent Calculus extension *) 419val (L_Sequent_rules, L_Sequent_ind, L_Sequent_cases) = Hol_reln ` 420 (!A B C. L_Sequent (Comma A (Comma B C)) (Comma (Comma A B) C)) /\ 421 (!A B C. L_Sequent (Comma (Comma A B) C) (Comma A (Comma B C)))`; 422 423val [L_Intro_lr, L_Intro_rl] = 424 map save_thm (combine (["L_Intro_lr", "L_Intro_rl"], CONJUNCTS L_Sequent_rules)); 425 426val LP_Sequent_def = Define ` 427 LP_Sequent = add_extension NLP_Sequent L_Sequent`; 428 429val NLP_Sequent_LP_Sequent = store_thm ( 430 "NLP_Sequent_LP_Sequent", ``extends NLP_Sequent LP_Sequent``, 431 REWRITE_TAC [LP_Sequent_def, add_extend_l]); 432 433val L_Sequent_LP_Sequent = store_thm ( 434 "L_Sequent_LP_Sequent", ``extends L_Sequent LP_Sequent``, 435 REWRITE_TAC [LP_Sequent_def, add_extend_r]); 436 437val LPextendsL = store_thm ("LPextendsL", 438 ``!E. extends LP_Sequent E ==> extends L_Sequent E``, 439 RW_TAC bool_ss [LP_Sequent_def, RSUBSET, RUNION]); 440 441val LPextendsNLP = store_thm ("LPextendsNLP", 442 ``!E. extends LP_Sequent E ==> extends NLP_Sequent E``, 443 RW_TAC bool_ss [LP_Sequent_def, RSUBSET, RUNION]); 444 445(******************************************************************************) 446(* *) 447(* Module: ReplaceProp *) 448(* *) 449(******************************************************************************) 450 451(* The `replace` operator has the type ('a ReplaceProp) *) 452val _ = type_abbrev ("ReplaceProp", ``:'a Term -> 'a Term -> 'a Term -> 'a Term -> bool``); 453 454(* Inductive definition of `replace` such that when ``replace Gamma Gamma' Delta Delta'`` 455 then Gamma' results from replacing a distinguished occurrence of the subterm Delta in 456 the term Gamma by Delta' *) 457 458val (replace_rules, replace_ind, replace_cases) = Hol_reln ` 459 (!F1 F2. replace F1 F2 F1 F2) /\ (* replaceRoot *) 460 (!Gamma1 Gamma2 Delta F1 F2. 461 replace Gamma1 Gamma2 F1 F2 ==> 462 replace (Comma Gamma1 Delta) (Comma Gamma2 Delta) F1 F2) /\ (* replaceLeft *) 463 (!Gamma1 Gamma2 Delta F1 F2. 464 replace Gamma1 Gamma2 F1 F2 ==> 465 replace (Comma Delta Gamma1) (Comma Delta Gamma2) F1 F2)`; (* replaceRight *) 466 467local 468 val list = CONJUNCTS replace_rules 469in 470 val replaceRoot = save_thm ("replaceRoot[simp]", List.nth (list, 0)) 471 and replaceLeft = save_thm ("replaceLeft", List.nth (list, 1)) 472 and replaceRight = save_thm ("replaceRight", List.nth (list, 2)) 473end; 474 475(* Definition of `replaceCommaDot` such that when ``replaceCommaDot Gamma Gamma'`` 476 then Gamma' is the result of replacing a number of commas in Gamma by the connector dot. 477 478 Example: ``!A B. replaceCommaDot (A , (A , B)) (A , (A . B)))`` where in this case only 479 one occurrence of comma is replaced by a dot. *) 480 481val (replaceCommaDot1_rules, replaceCommaDot1_ind, replaceCommaDot1_cases) = Hol_reln ` 482 (!T1 T2 A B. replace T1 T2 (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) 483 ==> replaceCommaDot1 T1 T2)`; 484 485val replaceCommaDot_def = Define `replaceCommaDot = RTC replaceCommaDot1`; 486 487val replaceCommaDot_rule = store_thm ("replaceCommaDot_rule", 488 ``!T1 T2 A B. replace T1 T2 (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) 489 ==> replaceCommaDot T1 T2``, 490 PROVE_TAC [replaceCommaDot_def, replaceCommaDot1_rules, RTC_SINGLE]); 491 492val replaceTransitive = store_thm ("replaceTransitive", ``transitive replaceCommaDot``, 493 REWRITE_TAC [replaceCommaDot_def, RTC_TRANSITIVE]); 494 495(* a more practical version *) 496val replaceTransitive' = store_thm ("replaceTransitive'", 497 ``!T1 T2 T3. replaceCommaDot T1 T2 /\ replaceCommaDot T2 T3 ==> replaceCommaDot T1 T3``, 498 PROVE_TAC [replaceTransitive, transitive_def]); 499 500val noReplace = store_thm ("noReplace[simp]", ``!T. replaceCommaDot T T``, 501 PROVE_TAC [replaceCommaDot_def, RTC_REFLEXIVE, reflexive_def]); 502 503local 504 val t = PROVE_TAC [replaceCommaDot1_rules, replaceCommaDot_def, replaceTransitive, 505 transitive_def, RTC_SINGLE] 506in 507 val replaceOneComma = store_thm ("replaceOneComma", 508 ``!T1 T2 T3 A B. replaceCommaDot T1 T2 /\ 509 replace T2 T3 (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) 510 ==> replaceCommaDot T1 T3``, t) 511 512 and replaceOneComma' = store_thm ("replaceOneComma'", 513 ``!T1 T2 T3 A B. replace T1 T2 (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) /\ 514 replaceCommaDot T2 T3 515 ==> replaceCommaDot T1 T3``, t); 516 517 val replaceCommaDot_rules = save_thm ( 518 "replaceCommaDot_rules", LIST_CONJ [noReplace, replaceCommaDot_rule, 519 replaceOneComma, replaceOneComma']) 520end; 521 522(* An induction theorem for RTC replaceCommaDot1, similar to those generated by Hol_reln *) 523val replaceCommaDot_ind = store_thm ("replaceCommaDot_ind", 524 ``!(P:'a gentzen_extension). 525 (!x. P x x) /\ 526 (!x y z A B. replace x y (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) /\ P y z ==> P x z) 527 ==> (!x y. replaceCommaDot x y ==> P x y)``, 528 (* The idea is to use RTC_INDUCT thm to prove induct theorems for RTCs *) 529 REWRITE_TAC [replaceCommaDot_def] 530 >> GEN_TAC (* remove outer !P *) 531 >> STRIP_TAC (* prepare for higher order matching *) 532 >> HO_MATCH_MP_TAC (ISPEC ``replaceCommaDot1:'a gentzen_extension`` RTC_INDUCT) 533 >> PROVE_TAC [replaceCommaDot1_cases]); 534 535local 536 val t = GEN_TAC \\ (* prepare for higher order matching and induction *) 537 HO_MATCH_MP_TAC replaceCommaDot_ind \\ 538 PROVE_TAC [replace_rules, replaceCommaDot_rules] 539in 540 val replaceMonoRight = store_thm ("replaceMonoRight", 541 ``!T3 T1 T2. replaceCommaDot T1 T2 542 ==> replaceCommaDot (Comma T1 T3) (Comma T2 T3)``, t) 543 and replaceMonoLeft = store_thm ("replaceMonoLeft", 544 ``!T3 T1 T2. replaceCommaDot T1 T2 545 ==> replaceCommaDot (Comma T3 T1) (Comma T3 T2)``, t) 546end; 547 548val replaceMono = store_thm ("replaceMono", 549 ``!T1 T2 T3 T4. replaceCommaDot T1 T2 /\ replaceCommaDot T3 T4 550 ==> replaceCommaDot (Comma T1 T3) (Comma T2 T4)``, 551 REPEAT STRIP_TAC 552 >> MATCH_MP_TAC replaceTransitive' 553 >> EXISTS_TAC ``Comma T2 T3`` 554 >> PROVE_TAC [replaceMonoLeft, replaceMonoRight]); 555 556val replaceTranslation = store_thm ("replaceTranslation", 557 ``!T. replaceCommaDot T (OneForm (deltaTranslation T))``, 558 Induct 559 >- PROVE_TAC [deltaTranslation_def, noReplace] (* base case *) 560 >> REWRITE_TAC [deltaTranslation_def] (* induct case *) 561 >> MATCH_MP_TAC replaceTransitive' 562 >> EXISTS_TAC ``Comma (OneForm (deltaTranslation T')) (OneForm (deltaTranslation T''))`` 563 >> PROVE_TAC [replaceOneComma, noReplace, replaceRoot, replaceMono]); 564 565val replace_inv1 = store_thm ("replace_inv1", 566 ``!Gamma' Delta X C. 567 replace (OneForm C) Gamma' (OneForm X) Delta ==> (Gamma' = Delta) /\ (X = C)``, 568 REPEAT GEN_TAC 569 >> ONCE_REWRITE_TAC [replace_cases] \\ 570 REPEAT STRIP_TAC 571 >- ASM_REWRITE_TAC [] 572 >- PROVE_TAC [Term_11] 573 >> PROVE_TAC [Term_distinct]); 574 575val replace_inv2 = store_thm ("replace_inv2", 576 ``!Gamma1 Gamma2 Gamma' Delta X. 577 replace (Comma Gamma1 Gamma2) Gamma' (OneForm X) Delta ==> 578 (?G. (Gamma' = Comma G Gamma2) /\ replace Gamma1 G (OneForm X) Delta) \/ 579 (?G. (Gamma' = Comma Gamma1 G) /\ replace Gamma2 G (OneForm X) Delta)``, 580 REPEAT STRIP_TAC 581 >> POP_ASSUM (MP_TAC o (ONCE_REWRITE_RULE [replace_cases])) 582 >> REPEAT STRIP_TAC 583 >- PROVE_TAC [Term_distinct] 584 >| [ `(Gamma1 = Gamma1') /\ (Gamma2 = Delta')` by PROVE_TAC [Term_11] \\ 585 ASM_REWRITE_TAC [] \\ 586 MATCH_MP_TAC OR_INTRO_THM1 \\ 587 Q.EXISTS_TAC `Gamma2'` \\ 588 ASM_REWRITE_TAC [] , 589 `(Gamma1 = Delta') /\ (Gamma2 = Gamma1')` by PROVE_TAC [Term_11] \\ 590 ASM_REWRITE_TAC [] \\ 591 MATCH_MP_TAC OR_INTRO_THM2 \\ 592 Q.EXISTS_TAC `Gamma2'` \\ 593 ASM_REWRITE_TAC [] ]); 594 595val doubleReplace = store_thm ("doubleReplace", 596 ``!Gamma Gamma' T1 T2. 597 replace Gamma Gamma' T1 T2 ==> 598 !Gamma2 A T3. replace Gamma' Gamma2 (OneForm A) T3 ==> 599 (?G. replace Gamma G (OneForm A) T3 /\ replace G Gamma2 T1 T2) \/ 600 (?G. replace T2 G (OneForm A) T3 /\ replace Gamma Gamma2 T1 G)``, 601 Induct_on `replace` 602 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 603 >| [ (* goal 1 (of 3) *) 604 DISJ2_TAC \\ 605 Q.EXISTS_TAC `Gamma2` \\ 606 ASM_REWRITE_TAC [replaceRoot], 607 (* goal 2 (of 3) *) 608 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 609 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 610 [ (* goal 2.1 (of 2) *) 611 ASM_REWRITE_TAC [] >> RES_TAC >| (* 2 sub-goals here *) 612 [ (* goal 2.1.1 (of 2) *) 613 DISJ1_TAC \\ 614 EXISTS_TAC ``(Comma G' Delta)`` \\ 615 CONJ_TAC >| (* 2 sub-goals here *) 616 [ (* goal 2.1.1.1 (of 2) *) 617 MATCH_MP_TAC replaceLeft >> ASM_REWRITE_TAC [], 618 (* goal 2.1.1.2 (of 2) *) 619 MATCH_MP_TAC replaceLeft >> ASM_REWRITE_TAC [] ], 620 (* goal 2.1.2 (of 2) *) 621 DISJ2_TAC \\ 622 Q.EXISTS_TAC `G'` \\ 623 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 624 MATCH_MP_TAC replaceLeft >> ASM_REWRITE_TAC [] ], 625 (* goal 2.2 (of 2) *) 626 ASM_REWRITE_TAC [] \\ 627 DISJ1_TAC \\ 628 EXISTS_TAC ``(Comma Gamma G)`` \\ 629 CONJ_TAC >| (* 2 sub-goals here *) 630 [ (* goal 2.2.1 (of 2) *) 631 MATCH_MP_TAC replaceRight >> ASM_REWRITE_TAC [], 632 (* goal 2.2.2 (of 2) *) 633 MATCH_MP_TAC replaceLeft >> ASM_REWRITE_TAC [] ] ], 634 (* goal 3 (of 3) *) 635 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 636 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 637 [ (* goal 3.1 (of 2) *) 638 ASM_REWRITE_TAC [] \\ 639 DISJ1_TAC \\ 640 EXISTS_TAC ``(Comma G Gamma)`` \\ 641 CONJ_TAC >| (* 2 sub-goals here *) 642 [ (* goal 3.1.1 (of 2) *) 643 MATCH_MP_TAC replaceLeft >> ASM_REWRITE_TAC [], 644 (* goal 3.1.2 (of 2) *) 645 MATCH_MP_TAC replaceRight >> ASM_REWRITE_TAC [] ], 646 (* goal 3.2 (of 2) *) 647 ASM_REWRITE_TAC [] >> RES_TAC >| (* 2 sub-goals here *) 648 [ (* goal 3.2.1 (of 2) *) 649 DISJ1_TAC \\ 650 EXISTS_TAC ``(Comma Delta G')`` \\ 651 CONJ_TAC >| (* 2 sub-goals here *) 652 [ (* goal 3.2.1.1 (of 2) *) 653 MATCH_MP_TAC replaceRight >> ASM_REWRITE_TAC [], 654 (* goal 3.2.1.2 (of 2) *) 655 MATCH_MP_TAC replaceRight >> ASM_REWRITE_TAC [] ], 656 (* goal 3.2.2 (of 2) *) 657 DISJ2_TAC \\ 658 Q.EXISTS_TAC `G'` \\ 659 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 660 MATCH_MP_TAC replaceRight >> ASM_REWRITE_TAC [] ] ] ]); 661 662val replaceSameP = store_thm ("replaceSameP", 663 ``!T1 T2 T3 T4. replace T1 T2 T3 T4 ==> 664 !G. ?G'. replace T1 G' T3 G /\ replace G' T2 G T4``, 665 Induct_on `replace` 666 >> REPEAT STRIP_TAC 667 >| [ Q.EXISTS_TAC `G` >> REWRITE_TAC [replaceRoot], 668 POP_ASSUM (ASSUME_TAC o (Q.SPEC `G`)) 669 >> POP_ASSUM CHOOSE_TAC 670 >> EXISTS_TAC ``(Comma G' Delta)`` 671 >> RW_TAC bool_ss [replaceLeft], 672 POP_ASSUM (ASSUME_TAC o (Q.SPEC `G`)) 673 >> POP_ASSUM CHOOSE_TAC 674 >> EXISTS_TAC ``(Comma Delta G')`` 675 >> RW_TAC bool_ss [replaceRight] ]); 676 677val replaceTrans = store_thm ("replaceTrans", 678 ``!T5 T6 T1 T2 T3 T4. 679 replace T1 T2 T3 T4 ==> replace T3 T4 T5 T6 ==> replace T1 T2 T5 T6``, 680 NTAC 2 GEN_TAC 681 >> Induct_on `replace` 682 >> REPEAT STRIP_TAC 683 >| [ PROVE_TAC [replaceLeft], 684 PROVE_TAC [replaceRight] ]); 685 686(* easier for MATCH_MP_TAC *) 687val replaceTrans' = store_thm ("replaceTrans'", 688 ``!T5 T6 T1 T2 T3 T4. 689 replace T1 T2 T3 T4 /\ replace T3 T4 T5 T6 ==> replace T1 T2 T5 T6``, 690 PROVE_TAC [replaceTrans]); 691 692(******************************************************************************) 693(* *) 694(* Module: NaturalDeduction *) 695(* *) 696(******************************************************************************) 697 698val (natDed_rules, natDed_ind, natDed_cases) = Hol_reln ` 699 (!(E:'a gentzen_extension) A. (* NatAxiom *) 700 natDed E (OneForm A) A) /\ 701 (!E Gamma A B. (* SlashIntro *) 702 natDed E (Comma Gamma (OneForm B)) A ==> 703 natDed E Gamma (Slash A B)) /\ 704 (!E Gamma A B. (* BackslashIntro *) 705 natDed E (Comma (OneForm B) Gamma) A ==> 706 natDed E Gamma (Backslash B A)) /\ 707 (!E Gamma Delta A B. (* DotIntro *) 708 natDed E Gamma A /\ natDed E Delta B ==> 709 natDed E (Comma Gamma Delta) (Dot A B)) /\ 710 (!E Gamma Delta A B. (* SlashElim *) 711 natDed E Gamma (Slash A B) /\ natDed E Delta B ==> 712 natDed E (Comma Gamma Delta) A) /\ 713 (!E Gamma Delta A B. (* BackslashElim *) 714 natDed E Gamma B /\ natDed E Delta (Backslash B A) ==> 715 natDed E (Comma Gamma Delta) A) /\ 716 (!E Gamma Gamma' Delta A B C. (* DotElim *) 717 replace Gamma Gamma' (Comma (OneForm A) (OneForm B)) Delta /\ 718 natDed E Delta (Dot A B) /\ natDed E Gamma C ==> 719 natDed E Gamma' C) /\ 720 (!(E:'a gentzen_extension) C Gamma Gamma' Delta Delta'. (* NatExt *) 721 replace Gamma Gamma' Delta Delta' /\ E Delta Delta' /\ 722 natDed E Gamma C ==> natDed E Gamma' C)`; 723 724val [NatAxiom, SlashIntro, BackslashIntro, DotIntro, SlashElim, BackslashElim, DotElim, NatExt] = 725 map save_thm 726 (combine (["NatAxiom[simp]", "SlashIntro", "BackslashIntro", "DotIntro", "SlashElim", 727 "BackslashElim", "DotElim", "NatExt"], CONJUNCTS natDed_rules)); 728 729val NatAxiomGeneralized = store_thm ("NatAxiomGeneralized[simp]", 730 ``!E Gamma. natDed E Gamma (deltaTranslation Gamma)``, 731 Induct_on `Gamma:'a Term` 732 >- PROVE_TAC [deltaTranslation_def, NatAxiom] 733 >> REWRITE_TAC [deltaTranslation_def] 734 >> PROVE_TAC [DotIntro]); 735 736val DotElimGeneralized = store_thm ("DotElimGeneralized", 737 ``!E C Gamma Gamma'. replaceCommaDot Gamma Gamma' 738 ==> natDed E Gamma C ==> natDed E Gamma' C``, 739 NTAC 2 GEN_TAC 740 >> HO_MATCH_MP_TAC replaceCommaDot_ind 741 >> REPEAT STRIP_TAC 742 >> `natDed E (OneForm (Dot A B)) (Dot A B)` by PROVE_TAC [NatAxiomGeneralized, deltaTranslation_def] 743 >> `natDed E Gamma' C` by PROVE_TAC [DotElim] 744 >> RW_TAC bool_ss []); 745 746val NatTermToForm = store_thm ("NatTermToForm", 747 ``!E Gamma C. natDed E Gamma C ==> natDed E (OneForm (deltaTranslation Gamma)) C``, 748 REPEAT STRIP_TAC 749 >> PROVE_TAC [DotElimGeneralized, replaceTranslation]); 750 751val NatExtSimpl = store_thm ( 752 "NatExtSimpl", ``!E Gamma Gamma' C. E Gamma Gamma' /\ natDed E Gamma C ==> natDed E Gamma' C``, 753 REPEAT STRIP_TAC 754 >> `replace Gamma Gamma' Gamma Gamma'` by REWRITE_TAC [replaceRoot] 755 >> IMP_RES_TAC NatExt); 756 757(******************************************************************************) 758(* *) 759(* Module: Sequent Calculus *) 760(* *) 761(******************************************************************************) 762 763(* gentzen presentation using sequents. *) 764val (gentzenSequent_rules, gentzenSequent_ind, gentzenSequent_cases) = Hol_reln ` 765 (!(E:'a gentzen_extension) A. (* SeqAxiom = NatAxiom *) 766 gentzenSequent E (OneForm A) A) /\ 767 (!E Gamma A B. (* RightSlash = SlashIntro *) 768 gentzenSequent E (Comma Gamma (OneForm B)) A ==> 769 gentzenSequent E Gamma (Slash A B)) /\ 770 (!E Gamma A B. (* RightBackslash = BackslashIntro *) 771 gentzenSequent E (Comma (OneForm B) Gamma) A ==> 772 gentzenSequent E Gamma (Backslash B A)) /\ 773 (!E Gamma Delta A B. (* RightDot = DotIntro *) 774 gentzenSequent E Gamma A /\ gentzenSequent E Delta B ==> 775 gentzenSequent E (Comma Gamma Delta) (Dot A B)) /\ 776 777 (* Delta |- B /\ Gamma[A] |- C ==> Gamma[A / B, Delta] |- C *) 778 (!E Gamma Gamma' Delta A B C. (* LeftSlash *) 779 replace Gamma Gamma' (OneForm A) (Comma (OneForm (Slash A B)) Delta) /\ 780 gentzenSequent E Delta B /\ gentzenSequent E Gamma C ==> 781 gentzenSequent E Gamma' C) /\ 782 783 (* Delta |- B /\ Gamma[A] |- C ==> Gamma[Delta, B \ A] |- C *) 784 (!E Gamma Gamma' Delta A B C. (* LeftBackslash *) 785 replace Gamma Gamma' (OneForm A) (Comma Delta (OneForm (Backslash B A))) /\ 786 gentzenSequent E Delta B /\ gentzenSequent E Gamma C ==> 787 gentzenSequent E Gamma' C) /\ 788 789 (* Gamma[A, B] |- C ==> Gamma[A * B] |- C *) 790 (!E Gamma Gamma' A B C. (* LeftDot *) 791 replace Gamma Gamma' (Comma (OneForm A) (OneForm B)) (OneForm (Dot A B)) /\ 792 gentzenSequent E Gamma C ==> 793 gentzenSequent E Gamma' C) /\ 794 795 (* Delta |- A /\ Gamma[A] |- C ==> Gamma[Delta] |- C *) 796 (!E Delta Gamma Gamma' A C. (* CutRule *) 797 replace Gamma Gamma' (OneForm A) Delta /\ 798 gentzenSequent E Delta A /\ gentzenSequent E Gamma C ==> 799 gentzenSequent E Gamma' C) /\ 800 801 (* E Delta Delta' /\ Gamma[Delta] |- C ==> Gamma[Delta'] |- C *) 802 (!(E:'a gentzen_extension) Gamma Gamma' Delta Delta' C. (* SeqExt = NatExt *) 803 replace Gamma Gamma' Delta Delta' /\ E Delta Delta' /\ 804 gentzenSequent E Gamma C ==> gentzenSequent E Gamma' C)`; 805 806val [SeqAxiom, RightSlash, RightBackslash, RightDot, LeftSlash, LeftBackslash, LeftDot, 807 CutRule, SeqExt] = 808 map save_thm 809 (combine (["SeqAxiom[simp]", "RightSlash", "RightBackslash", "RightDot", 810 "LeftSlash", "LeftBackslash", "LeftDot", "CutRule", "SeqExt"], 811 CONJUNCTS gentzenSequent_rules)); 812 813(* old name: axiomeGeneralisation *) 814val SeqAxiomGeneralized = store_thm ("SeqAxiomGeneralized[simp]", 815 ``!E Gamma. gentzenSequent E Gamma (deltaTranslation Gamma)``, 816 Induct_on `Gamma:'a Term` 817 >| [ PROVE_TAC [deltaTranslation_def, SeqAxiom], (* base case *) 818 REWRITE_TAC [deltaTranslation_def] \\ (* induct case *) 819 PROVE_TAC [RightDot] ]); 820 821(* Some derived properties concerning gentzenSequent *) 822 823val LeftDotSimpl = store_thm ("LeftDotSimpl", 824 ``!E A B C. gentzenSequent E (Comma (OneForm A) (OneForm B)) C ==> 825 gentzenSequent E (OneForm (Dot A B)) C``, 826 REPEAT STRIP_TAC 827 >> MATCH_MP_TAC LeftDot 828 >> EXISTS_TAC ``(Comma (OneForm A) (OneForm B))`` 829 >> Q.EXISTS_TAC `A` 830 >> Q.EXISTS_TAC `B` 831 >> PROVE_TAC [replaceRoot]); 832 833val LeftDotGeneralized = store_thm ("LeftDotGeneralized", 834 ``!E C T1 T2. replaceCommaDot T1 T2 ==> gentzenSequent E T1 C ==> gentzenSequent E T2 C``, 835 NTAC 2 GEN_TAC 836 >> HO_MATCH_MP_TAC replaceCommaDot_ind 837 >> REPEAT STRIP_TAC 838 >> PROVE_TAC [LeftDot]); 839 840val SeqTermToForm = store_thm ("SeqTermToForm", 841 ``!E Gamma C. gentzenSequent E Gamma C 842 ==> gentzenSequent E (OneForm (deltaTranslation Gamma)) C``, 843 REPEAT GEN_TAC 844 >> MATCH_MP_TAC LeftDotGeneralized 845 >> RW_TAC bool_ss [replaceTranslation]); 846 847val LeftSlashSimpl = store_thm ("LeftSlashSimpl", 848 ``!E Gamma A B C. gentzenSequent E Gamma B /\ gentzenSequent E (OneForm A) C 849 ==> gentzenSequent E (Comma (OneForm (Slash A B)) Gamma) C``, 850 PROVE_TAC [replace_rules, replaceCommaDot_rules, LeftSlash]); 851 852val LeftBackslashSimpl = store_thm ("LeftBackslashSimpl", 853 ``!E Gamma A B C. gentzenSequent E Gamma B /\ gentzenSequent E (OneForm A) C 854 ==> gentzenSequent E (Comma Gamma (OneForm (Backslash B A))) C``, 855 PROVE_TAC [replace_rules, replaceCommaDot_rules, LeftBackslash]); 856 857val CutRuleSimpl = store_thm ("CutRuleSimpl", 858 ``!E Gamma A C. gentzenSequent E Gamma A /\ gentzenSequent E (OneForm A) C 859 ==> gentzenSequent E Gamma C``, 860 PROVE_TAC [replace_rules, replaceCommaDot_rules, CutRule]); 861 862val DotRightSlash' = store_thm ("DotRightSlash'", 863 ``!E A B C. gentzenSequent E (OneForm A) (Slash C B) 864 ==> gentzenSequent E (OneForm (Dot A B)) C``, 865 PROVE_TAC [replace_rules, replaceCommaDot_rules, gentzenSequent_rules]); 866 867val DotRightBackslash' = store_thm ("DotRightBackslash'", 868 ``!E A B C. gentzenSequent E (OneForm B) (Backslash A C) 869 ==> gentzenSequent E (OneForm (Dot A B)) C``, 870 PROVE_TAC [replace_rules, replaceCommaDot_rules, gentzenSequent_rules]); 871 872val SeqExtSimpl = store_thm ( 873 "SeqExtSimpl", ``!E Gamma Gamma' C. E Gamma Gamma' /\ gentzenSequent E Gamma C 874 ==> gentzenSequent E Gamma' C``, 875 REPEAT STRIP_TAC 876 >> `replace Gamma Gamma' Gamma Gamma'` by REWRITE_TAC [replaceRoot] 877 >> IMP_RES_TAC SeqExt); 878 879(* some definitions concerning extensions *) 880 881val LextensionSimpl = store_thm ("LextensionSimpl", 882 ``!E T1 T2 T3 C. extends L_Sequent E /\ 883 gentzenSequent E (Comma T1 (Comma T2 T3)) C 884 ==> gentzenSequent E (Comma (Comma T1 T2) T3) C``, 885 REPEAT STRIP_TAC 886 >> MATCH_MP_TAC SeqExt 887 >> EXISTS_TAC ``(Comma T1 (Comma T2 T3))`` (* Gamma *) 888 >> EXISTS_TAC ``(Comma T1 (Comma T2 T3))`` (* Delta *) 889 >> EXISTS_TAC ``(Comma (Comma T1 T2) T3)`` (* Delta' *) 890 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 891 >- REWRITE_TAC [replaceRoot] 892 >- PROVE_TAC [RSUBSET, L_Intro_lr] 893 >> ASM_REWRITE_TAC []); 894 895val LextensionSimpl' = store_thm ("LextensionSimpl'", (* dual theorem of above *) 896 ``!E T1 T2 T3 C. extends L_Sequent E /\ 897 gentzenSequent E (Comma (Comma T1 T2) T3) C 898 ==> gentzenSequent E (Comma T1 (Comma T2 T3)) C``, 899 REPEAT STRIP_TAC 900 >> MATCH_MP_TAC SeqExt 901 >> EXISTS_TAC ``(Comma (Comma T1 T2) T3)`` (* Gamma *) 902 >> EXISTS_TAC ``(Comma (Comma T1 T2) T3)`` (* Delta *) 903 >> EXISTS_TAC ``(Comma T1 (Comma T2 T3))`` (* Delta' *) 904 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 905 >- REWRITE_TAC [replaceRoot] 906 >- PROVE_TAC [RSUBSET, L_Intro_rl] 907 >> ASM_REWRITE_TAC []); 908 909val LextensionSimplDot = store_thm ("LextensionSimplDot", 910 ``!E A B C D. extends L_Sequent E /\ 911 gentzenSequent E (OneForm (Dot A (Dot B C))) D 912 ==> gentzenSequent E (OneForm (Dot (Dot A B) C)) D``, 913 REPEAT STRIP_TAC 914 >> MATCH_MP_TAC LeftDotSimpl 915 >> MATCH_MP_TAC LeftDot 916 >> EXISTS_TAC ``(Comma (Comma (OneForm A) (OneForm B)) (OneForm C))`` 917 >> Q.EXISTS_TAC `A` 918 >> Q.EXISTS_TAC `B` 919 >> STRIP_TAC 920 >- RW_TAC bool_ss [replaceLeft, replaceRoot] 921 >> MATCH_MP_TAC LextensionSimpl 922 >> STRIP_TAC 923 >- ASM_REWRITE_TAC [] 924 >> MATCH_MP_TAC CutRuleSimpl 925 >> EXISTS_TAC ``(deltaTranslation (Comma (OneForm A) (Comma (OneForm B) (OneForm C))))`` 926 >> RW_TAC bool_ss [SeqAxiomGeneralized, deltaTranslation_def]); 927 928val LextensionSimplDot' = store_thm ("LextensionSimplDot'", (* dual theorem of above *) 929 ``!E A B C D. extends L_Sequent E /\ 930 gentzenSequent E (OneForm (Dot (Dot A B) C)) D 931 ==> gentzenSequent E (OneForm (Dot A (Dot B C))) D``, 932 REPEAT STRIP_TAC 933 >> MATCH_MP_TAC LeftDotSimpl 934 >> MATCH_MP_TAC LeftDot 935 >> EXISTS_TAC ``(Comma (OneForm A) (Comma (OneForm B) (OneForm C)))`` 936 >> Q.EXISTS_TAC `B` 937 >> Q.EXISTS_TAC `C` 938 >> STRIP_TAC 939 >- RW_TAC bool_ss [replaceRight, replaceRoot] 940 >> MATCH_MP_TAC LextensionSimpl' 941 >> STRIP_TAC 942 >- ASM_REWRITE_TAC [] 943 >> MATCH_MP_TAC CutRuleSimpl 944 >> EXISTS_TAC ``(deltaTranslation (Comma (Comma (OneForm A) (OneForm B)) (OneForm C)))`` 945 >> RW_TAC bool_ss [SeqAxiomGeneralized, deltaTranslation_def]); 946 947val NLPextensionSimpl = store_thm ("NLPextensionSimpl", 948 ``!E T1 T2 C. extends NLP_Sequent E /\ 949 gentzenSequent E (Comma T1 T2) C 950 ==> gentzenSequent E (Comma T2 T1) C``, 951 REPEAT STRIP_TAC 952 >> MATCH_MP_TAC SeqExt 953 >> EXISTS_TAC ``(Comma T1 T2)`` 954 >> EXISTS_TAC ``(Comma T1 T2)`` 955 >> EXISTS_TAC ``(Comma T2 T1)`` 956 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 957 >- REWRITE_TAC [replaceRoot] 958 >- PROVE_TAC [RSUBSET, NLP_Intro] 959 >> ASM_REWRITE_TAC []); 960 961val NLPextensionSimplDot = store_thm ("NLPextensionSimplDot", 962 ``!E A B C. extends NLP_Sequent E /\ 963 gentzenSequent E (OneForm (Dot A B)) C 964 ==> gentzenSequent E (OneForm (Dot B A)) C``, 965 REPEAT STRIP_TAC 966 >> MATCH_MP_TAC LeftDotSimpl 967 >> MATCH_MP_TAC NLPextensionSimpl 968 >> STRIP_TAC 969 >- ASM_REWRITE_TAC [] 970 >> MATCH_MP_TAC CutRuleSimpl 971 >> EXISTS_TAC ``(deltaTranslation (Comma (OneForm A) (OneForm B)))`` 972 >> RW_TAC bool_ss [SeqAxiomGeneralized, deltaTranslation_def]); 973 974(* original name: gentzenExtends, see also mono_X *) 975val mono_E = store_thm ("mono_E", 976 ``!E' E Gamma A. gentzenSequent E Gamma A 977 ==> extends E E' 978 ==> gentzenSequent E' Gamma A``, 979 GEN_TAC 980 >> HO_MATCH_MP_TAC gentzenSequent_ind 981 >> REPEAT STRIP_TAC (* 9 goals here *) 982 >- REWRITE_TAC [SeqAxiom] 983 >- RW_TAC bool_ss [RightSlash] 984 >- RW_TAC bool_ss [RightBackslash] 985 >- RW_TAC bool_ss [RightDot] 986 >- PROVE_TAC [LeftSlash] 987 >- PROVE_TAC [LeftBackslash] 988 >- PROVE_TAC [LeftDot] 989 >- PROVE_TAC [CutRule] 990 >> `E' Delta Delta'` by PROVE_TAC [RSUBSET] 991 >> `gentzenSequent E' Gamma A` by RW_TAC bool_ss [] 992 >> PROVE_TAC [SeqExt]); 993 994(* Some theorems and derived properties 995 These definitions can be applied for all gentzen extensions, 996 we can see how CutRuleSimpl gets used in most of time. *) 997 998val application = store_thm ("application", 999 ``!E A B. gentzenSequent E (OneForm (Dot (Slash A B) B)) A``, 1000 REPEAT STRIP_TAC 1001 >> MATCH_MP_TAC LeftDotSimpl 1002 >> MATCH_MP_TAC LeftSlashSimpl 1003 >> REWRITE_TAC [SeqAxiom]); 1004 1005val application' = store_thm ("application'", 1006 ``!E A B. gentzenSequent E (OneForm (Dot B (Backslash B A))) A``, 1007 REPEAT STRIP_TAC 1008 >> MATCH_MP_TAC LeftDotSimpl 1009 >> MATCH_MP_TAC LeftBackslashSimpl 1010 >> REWRITE_TAC [SeqAxiom]); 1011 1012val RightSlashDot = store_thm ("RightSlashDot", 1013 ``!E A B C. gentzenSequent E (OneForm (Dot A C)) B 1014 ==> gentzenSequent E (OneForm A) (Slash B C)``, 1015 REPEAT STRIP_TAC 1016 >> MATCH_MP_TAC RightSlash 1017 >> MATCH_MP_TAC CutRuleSimpl 1018 >> EXISTS_TAC ``(deltaTranslation (Comma (OneForm A) (OneForm C)))`` 1019 >> RW_TAC bool_ss [SeqAxiomGeneralized, deltaTranslation_def]); 1020 1021val RightBackslashDot = store_thm ("RightBackslashDot", 1022 ``!E A B C. gentzenSequent E (OneForm (Dot B A)) C 1023 ==> gentzenSequent E (OneForm A) (Backslash B C)``, 1024 REPEAT STRIP_TAC 1025 >> MATCH_MP_TAC RightBackslash 1026 >> MATCH_MP_TAC CutRuleSimpl 1027 >> EXISTS_TAC ``(deltaTranslation (Comma (OneForm B) (OneForm A)))`` 1028 >> RW_TAC bool_ss [SeqAxiomGeneralized, deltaTranslation_def]); 1029 1030val coApplication = store_thm ("coApplication", 1031 ``!E A B. gentzenSequent E (OneForm A) (Slash (Dot A B) B)``, 1032 PROVE_TAC [RightSlash, RightDot, SeqAxiom]); 1033 1034val coApplication' = store_thm ("coApplication'", 1035 ``!E A B. gentzenSequent E (OneForm A) (Backslash B (Dot B A))``, 1036 PROVE_TAC [RightBackslash, RightDot, SeqAxiom]); 1037 1038val monotonicity = store_thm ("monotonicity", 1039 ``!E A B C D. gentzenSequent E (OneForm A) B /\ 1040 gentzenSequent E (OneForm C) D 1041 ==> gentzenSequent E (OneForm (Dot A C)) (Dot B D)``, 1042 PROVE_TAC [LeftDotSimpl, RightDot]); 1043 1044val isotonicity = store_thm ("isotonicity", 1045 ``!E A B C. gentzenSequent E (OneForm A) B 1046 ==> gentzenSequent E (OneForm (Slash A C)) (Slash B C)``, 1047 REPEAT STRIP_TAC 1048 >> MATCH_MP_TAC RightSlash 1049 >> MATCH_MP_TAC CutRuleSimpl 1050 >> Q.EXISTS_TAC `A` 1051 >> PROVE_TAC [LeftSlashSimpl, SeqAxiom]); 1052 1053val isotonicity' = store_thm ("isotonicity'", 1054 ``!E A B C. gentzenSequent E (OneForm A) B 1055 ==> gentzenSequent E (OneForm (Backslash C A)) (Backslash C B)``, 1056 REPEAT STRIP_TAC 1057 >> MATCH_MP_TAC RightBackslash 1058 >> MATCH_MP_TAC CutRuleSimpl 1059 >> Q.EXISTS_TAC `A` 1060 >> PROVE_TAC [LeftBackslashSimpl, SeqAxiom]); 1061 1062val antitonicity = store_thm ("antitonicity", 1063 ``!E A B C. gentzenSequent E (OneForm A) B 1064 ==> gentzenSequent E (OneForm (Slash C B)) (Slash C A)``, 1065 REPEAT STRIP_TAC 1066 >> MATCH_MP_TAC RightSlash 1067 >> MATCH_MP_TAC CutRuleSimpl 1068 >> EXISTS_TAC ``(Dot (Slash C B) B)`` 1069 >> STRIP_TAC 1070 >- PROVE_TAC [RightDot, SeqAxiom] 1071 >> REWRITE_TAC [application]); 1072 1073val antitonicity' = store_thm ("antitonicity'", 1074 ``!E A B C. gentzenSequent E (OneForm A) B 1075 ==> gentzenSequent E (OneForm (Backslash B C)) (Backslash A C)``, 1076 REPEAT STRIP_TAC 1077 >> MATCH_MP_TAC RightBackslash 1078 >> MATCH_MP_TAC CutRuleSimpl 1079 >> EXISTS_TAC ``(Dot B (Backslash B C))`` 1080 >> STRIP_TAC 1081 >- PROVE_TAC [RightDot, SeqAxiom] 1082 >> REWRITE_TAC [application']); 1083 1084val lifting = store_thm ("lifting", 1085 ``!E A B C. gentzenSequent E (OneForm A) (Slash B (Backslash A B))``, 1086 REPEAT GEN_TAC 1087 >> MATCH_MP_TAC RightSlash 1088 >> MATCH_MP_TAC CutRuleSimpl 1089 >> EXISTS_TAC ``(Dot A (Backslash A B))`` 1090 >> STRIP_TAC 1091 >- PROVE_TAC [RightDot, SeqAxiom] 1092 >> REWRITE_TAC [application']); 1093 1094val lifting' = store_thm ("lifting'", 1095 ``!E A B C. gentzenSequent E (OneForm A) (Backslash (Slash B A) B)``, 1096 REPEAT GEN_TAC 1097 >> MATCH_MP_TAC RightBackslash 1098 >> MATCH_MP_TAC CutRuleSimpl 1099 >> EXISTS_TAC ``(Dot (Slash B A) A)`` 1100 >> STRIP_TAC 1101 >- PROVE_TAC [RightDot, SeqAxiom] 1102 >> REWRITE_TAC [application]); 1103 1104(* These definitions can be applied iff associativity is supported by our logical system *) 1105 1106val mainGeach = store_thm ("mainGeach", 1107 ``!E A B C. extends L_Sequent E 1108 ==> gentzenSequent E (OneForm (Slash A B)) 1109 (Slash (Slash A C) (Slash B C))``, 1110 REPEAT STRIP_TAC 1111 >> NTAC 2 (MATCH_MP_TAC RightSlash) 1112 >> MATCH_MP_TAC LextensionSimpl 1113 >> CONJ_TAC 1114 >- POP_ASSUM ACCEPT_TAC 1115 >> MATCH_MP_TAC CutRuleSimpl 1116 >> EXISTS_TAC ``(Dot (Slash A B) B)`` 1117 >> CONJ_TAC 1118 >| [ MATCH_MP_TAC RightDot \\ 1119 CONJ_TAC >| 1120 [ REWRITE_TAC [SeqAxiom], 1121 MATCH_MP_TAC LeftSlashSimpl \\ 1122 STRIP_TAC \\ 1123 REWRITE_TAC [SeqAxiom] ], 1124 REWRITE_TAC [application] ]); 1125 1126val mainGeach' = store_thm ("mainGeach'", 1127 ``!E A B C. extends L_Sequent E 1128 ==> gentzenSequent E (OneForm (Backslash B A)) 1129 (Backslash (Backslash C B) (Backslash C A))``, 1130 REPEAT STRIP_TAC 1131 >> NTAC 2 (MATCH_MP_TAC RightBackslash) 1132 >> MATCH_MP_TAC LextensionSimpl' 1133 >> CONJ_TAC 1134 >- POP_ASSUM ACCEPT_TAC 1135 >> MATCH_MP_TAC CutRuleSimpl 1136 >> EXISTS_TAC ``(Dot B (Backslash B A))`` 1137 >> CONJ_TAC 1138 >| [ MATCH_MP_TAC RightDot \\ 1139 CONJ_TAC >| 1140 [ MATCH_MP_TAC LeftBackslashSimpl \\ 1141 STRIP_TAC \\ 1142 REWRITE_TAC [SeqAxiom], 1143 REWRITE_TAC [SeqAxiom] ] , 1144 REWRITE_TAC [application'] ]); 1145 1146val secondaryGeach = store_thm ("secondaryGeach", 1147 ``!E A B C. extends L_Sequent E 1148 ==> gentzenSequent E (OneForm (Slash B C)) 1149 (Backslash (Slash A B) (Slash A C))``, 1150 REPEAT STRIP_TAC 1151 >> MATCH_MP_TAC RightBackslash 1152 >> MATCH_MP_TAC RightSlash 1153 >> MATCH_MP_TAC LextensionSimpl 1154 >> CONJ_TAC >- (POP_ASSUM ACCEPT_TAC) 1155 >> MATCH_MP_TAC CutRuleSimpl 1156 >> EXISTS_TAC ``(Dot (Slash A B) B)`` 1157 >> CONJ_TAC 1158 >| [ MATCH_MP_TAC RightDot \\ 1159 CONJ_TAC >| 1160 [ REWRITE_TAC [SeqAxiom], 1161 MATCH_MP_TAC LeftSlashSimpl \\ 1162 STRIP_TAC \\ 1163 REWRITE_TAC [SeqAxiom] ], 1164 REWRITE_TAC [application] ]); 1165 1166val secondaryGeach' = store_thm ("secondaryGeach'", 1167``!E A B C. extends L_Sequent E 1168 ==> gentzenSequent E (OneForm (Backslash C B)) 1169 (Slash (Backslash C A) (Backslash B A))``, 1170 REPEAT STRIP_TAC 1171 >> MATCH_MP_TAC RightSlash 1172 >> MATCH_MP_TAC RightBackslash 1173 >> MATCH_MP_TAC LextensionSimpl' 1174 >> CONJ_TAC 1175 >- POP_ASSUM ACCEPT_TAC 1176 >> MATCH_MP_TAC CutRuleSimpl 1177 >> EXISTS_TAC ``(Dot B (Backslash B A))`` 1178 >> CONJ_TAC 1179 >| [ MATCH_MP_TAC RightDot \\ 1180 STRIP_TAC >| 1181 [ MATCH_MP_TAC LeftBackslashSimpl \\ 1182 STRIP_TAC \\ 1183 REWRITE_TAC [SeqAxiom], 1184 REWRITE_TAC [SeqAxiom] ] , 1185 REWRITE_TAC [application'] ]); 1186 1187val composition = store_thm ("composition", 1188 ``!E A B C. extends L_Sequent E 1189 ==> gentzenSequent E (OneForm (Dot (Slash A B) (Slash B C))) 1190 (Slash A C)``, 1191 REPEAT STRIP_TAC 1192 >> MATCH_MP_TAC CutRuleSimpl 1193 >> EXISTS_TAC ``(Dot (Slash (Slash A C) (Slash B C)) (Slash B C))`` 1194 >> CONJ_TAC 1195 >| [ MATCH_MP_TAC monotonicity \\ 1196 CONJ_TAC >| 1197 [ RW_TAC bool_ss [mainGeach], REWRITE_TAC [SeqAxiom] ], 1198 REWRITE_TAC [application] ]); 1199 1200val composition' = store_thm ("composition'", 1201 ``!E A B C. extends L_Sequent E 1202 ==> gentzenSequent E (OneForm (Dot (Backslash C B) (Backslash B A))) 1203 (Backslash C A)``, 1204 REPEAT STRIP_TAC 1205 >> MATCH_MP_TAC CutRuleSimpl 1206 >> EXISTS_TAC ``(Dot (Slash (Backslash C A) (Backslash B A)) (Backslash B A))`` 1207 >> CONJ_TAC 1208 >| [ MATCH_MP_TAC monotonicity \\ 1209 CONJ_TAC >| 1210 [ RW_TAC bool_ss [secondaryGeach'], REWRITE_TAC [SeqAxiom] ], 1211 REWRITE_TAC [application] ]); 1212 1213val restructuring = store_thm ("restructuring", 1214 ``!E A B C. extends L_Sequent E 1215 ==> gentzenSequent E (OneForm (Slash (Backslash A B) C)) 1216 (Backslash A (Slash B C))``, 1217 REPEAT STRIP_TAC 1218 >> MATCH_MP_TAC RightBackslash 1219 >> MATCH_MP_TAC RightSlash 1220 >> MATCH_MP_TAC LextensionSimpl 1221 >> CONJ_TAC 1222 >- POP_ASSUM ACCEPT_TAC 1223 >> MATCH_MP_TAC CutRuleSimpl 1224 >> EXISTS_TAC ``(Dot A (Backslash A B))`` 1225 >> CONJ_TAC 1226 >| [ MATCH_MP_TAC RightDot \\ 1227 CONJ_TAC >| [ REWRITE_TAC [SeqAxiom], 1228 MATCH_MP_TAC LeftSlashSimpl \\ 1229 REWRITE_TAC [SeqAxiom] ], 1230 REWRITE_TAC [application'] ]); 1231 1232val restructuring' = store_thm ("restructuring'", 1233 ``!E A B C. extends L_Sequent E 1234 ==> gentzenSequent E (OneForm (Backslash A (Slash B C))) 1235 (Slash (Backslash A B) C)``, 1236 REPEAT STRIP_TAC 1237 >> MATCH_MP_TAC RightSlash 1238 >> MATCH_MP_TAC RightBackslash 1239 >> MATCH_MP_TAC LextensionSimpl' 1240 >> CONJ_TAC 1241 >- POP_ASSUM ACCEPT_TAC 1242 >> MATCH_MP_TAC CutRuleSimpl 1243 >> EXISTS_TAC ``(Dot (Slash B C) C)`` 1244 >> CONJ_TAC 1245 >| [ MATCH_MP_TAC RightDot \\ 1246 CONJ_TAC >| [ MATCH_MP_TAC LeftBackslashSimpl \\ 1247 REWRITE_TAC [SeqAxiom], 1248 REWRITE_TAC [SeqAxiom] ], 1249 REWRITE_TAC [application] ]); 1250 1251val currying = store_thm ("currying", 1252 ``!E A B C. extends L_Sequent E 1253 ==> gentzenSequent E (OneForm (Slash A (Dot B C))) 1254 (Slash (Slash A C) B)``, 1255 REPEAT STRIP_TAC 1256 >> NTAC 2 (MATCH_MP_TAC RightSlashDot) 1257 >> MATCH_MP_TAC LextensionSimplDot 1258 >> CONJ_TAC 1259 >- POP_ASSUM ACCEPT_TAC 1260 >> REWRITE_TAC [application]); 1261 1262val currying' = store_thm ("currying'", 1263 ``!E A B C. extends L_Sequent E 1264 ==> gentzenSequent E (OneForm (Slash (Slash A C) B)) 1265 (Slash A (Dot B C))``, 1266 REPEAT STRIP_TAC 1267 >> MATCH_MP_TAC RightSlashDot 1268 >> MATCH_MP_TAC LextensionSimplDot' 1269 >> CONJ_TAC 1270 >- POP_ASSUM ACCEPT_TAC 1271 >> MATCH_MP_TAC CutRuleSimpl 1272 >> EXISTS_TAC ``(Dot (Slash A C) C)`` 1273 >> CONJ_TAC 1274 >| [ MATCH_MP_TAC monotonicity 1275 >> CONJ_TAC 1276 >> REWRITE_TAC [application, SeqAxiom], 1277 REWRITE_TAC [application] ]); 1278 1279val decurrying = store_thm ("decurrying", 1280 ``!E A B C. extends L_Sequent E 1281 ==> gentzenSequent E (OneForm (Backslash (Dot A B) C)) 1282 (Backslash B (Backslash A C))``, 1283 REPEAT STRIP_TAC 1284 >> NTAC 2 (MATCH_MP_TAC RightBackslashDot) 1285 >> MATCH_MP_TAC LextensionSimplDot' 1286 >> CONJ_TAC 1287 >- POP_ASSUM ACCEPT_TAC 1288 >> REWRITE_TAC [application']); 1289 1290val decurrying' = store_thm ("decurrying'", 1291 ``!E A B C. extends L_Sequent E 1292 ==> gentzenSequent E (OneForm (Backslash B (Backslash A C))) 1293 (Backslash (Dot A B) C)``, 1294 REPEAT STRIP_TAC 1295 >> MATCH_MP_TAC RightBackslashDot 1296 >> MATCH_MP_TAC LextensionSimplDot 1297 >> CONJ_TAC 1298 >- POP_ASSUM ACCEPT_TAC 1299 >> MATCH_MP_TAC CutRuleSimpl 1300 >> EXISTS_TAC ``(Dot A (Backslash A C))`` 1301 >> CONJ_TAC 1302 >| [ MATCH_MP_TAC monotonicity \\ 1303 REWRITE_TAC [application', SeqAxiom], 1304 REWRITE_TAC [application'] ]); 1305 1306(* Theorem for systems that support commutativity: if its extension extends NLP_Sequent *) 1307 1308val permutation = store_thm ("permutation", 1309 ``!E A B C. extends NLP_Sequent E 1310 ==> gentzenSequent E (OneForm A) (Backslash B C) 1311 ==> gentzenSequent E (OneForm B) (Backslash A C)``, 1312 REPEAT STRIP_TAC 1313 >> MATCH_MP_TAC RightBackslashDot 1314 >> MATCH_MP_TAC NLPextensionSimplDot 1315 >> CONJ_TAC 1316 >- ASM_REWRITE_TAC [] 1317 >> MATCH_MP_TAC CutRuleSimpl 1318 >> EXISTS_TAC ``(Dot B (Backslash B C))`` 1319 >> CONJ_TAC 1320 >| [ MATCH_MP_TAC monotonicity >> ASM_REWRITE_TAC [SeqAxiom], 1321 REWRITE_TAC [application'] ]); 1322 1323val exchange = store_thm ("exchange", 1324 ``!E A B. extends NLP_Sequent E 1325 ==> gentzenSequent E (OneForm (Slash A B)) (Backslash B A)``, 1326 REPEAT STRIP_TAC 1327 >> MATCH_MP_TAC RightBackslashDot 1328 >> MATCH_MP_TAC NLPextensionSimplDot 1329 >> RW_TAC bool_ss [application]); 1330 1331val exchange' = store_thm ("exchange'", 1332 ``!E A B. extends NLP_Sequent E 1333 ==> gentzenSequent E (OneForm (Backslash B A)) (Slash A B)``, 1334 REPEAT STRIP_TAC 1335 >> MATCH_MP_TAC RightSlashDot 1336 >> MATCH_MP_TAC NLPextensionSimplDot 1337 >> RW_TAC bool_ss [application']); 1338 1339val preposing = store_thm ("preposing", 1340 ``!E A B. extends NLP_Sequent E 1341 ==> gentzenSequent E (OneForm A) (Slash B (Slash B A))``, 1342 REPEAT STRIP_TAC 1343 >> MATCH_MP_TAC RightSlashDot 1344 >> MATCH_MP_TAC NLPextensionSimplDot 1345 >> RW_TAC bool_ss [application]); 1346 1347val postposing = store_thm ("postposing", 1348 ``!E A B. extends NLP_Sequent E 1349 ==> gentzenSequent E (OneForm A) (Backslash (Backslash A B) B)``, 1350 REPEAT STRIP_TAC 1351 >> MATCH_MP_TAC RightBackslashDot 1352 >> MATCH_MP_TAC NLPextensionSimplDot 1353 >> RW_TAC bool_ss [application']); 1354 1355(* For systems that support both commutativity and associativity *) 1356 1357val mixedComposition = store_thm ("mixedComposition", 1358 ``!E A B C. extends LP_Sequent E 1359 ==> gentzenSequent E (OneForm (Dot (Slash A B) (Backslash C B))) (Backslash C A)``, 1360 REPEAT STRIP_TAC 1361 >> MATCH_MP_TAC NLPextensionSimplDot 1362 >> CONJ_TAC 1363 >- RW_TAC bool_ss [LPextendsNLP] 1364 >> MATCH_MP_TAC RightBackslashDot 1365 >> MATCH_MP_TAC LextensionSimplDot' 1366 >> CONJ_TAC 1367 >- RW_TAC bool_ss [LPextendsL] 1368 >> MATCH_MP_TAC CutRuleSimpl 1369 >> EXISTS_TAC ``(Dot B (Slash A B))`` 1370 >> CONJ_TAC 1371 >| [ MATCH_MP_TAC monotonicity \\ 1372 RW_TAC bool_ss [application', SeqAxiom], 1373 MATCH_MP_TAC NLPextensionSimplDot \\ 1374 RW_TAC bool_ss [application, LPextendsNLP] ]); 1375 1376val mixedComposition' = store_thm ("mixedComposition'", 1377 ``!E A B C. extends LP_Sequent E 1378 ==> gentzenSequent E (OneForm (Dot (Slash B C) (Backslash B A))) (Slash A C)``, 1379 REPEAT STRIP_TAC 1380 >> MATCH_MP_TAC NLPextensionSimplDot 1381 >> CONJ_TAC 1382 >- RW_TAC bool_ss [LPextendsNLP] 1383 >> MATCH_MP_TAC RightSlashDot 1384 >> MATCH_MP_TAC LextensionSimplDot 1385 >> CONJ_TAC 1386 >- RW_TAC bool_ss [LPextendsL] 1387 >> MATCH_MP_TAC CutRuleSimpl 1388 >> EXISTS_TAC ``(Dot (Backslash B A) B)`` 1389 >> CONJ_TAC 1390 >| [ MATCH_MP_TAC monotonicity \\ 1391 RW_TAC bool_ss [application, SeqAxiom], 1392 MATCH_MP_TAC NLPextensionSimplDot \\ 1393 RW_TAC bool_ss [application', LPextendsNLP] ]); 1394 1395(******************************************************************************) 1396(* *) 1397(* Module: ArrowGentzen *) 1398(* *) 1399(******************************************************************************) 1400 1401val replace_arrow = store_thm ("replace_arrow", 1402 ``!X Gamma Gamma' T1 T2. 1403 replace Gamma Gamma' T1 T2 ==> 1404 arrow X (deltaTranslation T2) (deltaTranslation T1) ==> 1405 arrow X (deltaTranslation Gamma') (deltaTranslation Gamma)``, 1406 GEN_TAC 1407 >> HO_MATCH_MP_TAC replace_ind 1408 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1409 >| [ REWRITE_TAC [deltaTranslation_def] \\ 1410 RES_TAC \\ 1411 POP_ASSUM (ASSUME_TAC o (MATCH_MP Dot_mono_left)) \\ 1412 ASM_REWRITE_TAC [], 1413 REWRITE_TAC [deltaTranslation_def] \\ 1414 RES_TAC \\ 1415 POP_ASSUM (ASSUME_TAC o (MATCH_MP Dot_mono_right)) \\ 1416 ASM_REWRITE_TAC [] ]); 1417 1418val replace_arrow' = store_thm ("replace_arrow'", 1419 ``!C X Gamma Gamma' T1 T2. 1420 replace Gamma Gamma' T1 T2 ==> 1421 arrow X (deltaTranslation T2) (deltaTranslation T1) ==> 1422 arrow X (deltaTranslation Gamma) C ==> 1423 arrow X (deltaTranslation Gamma') C``, 1424 REPEAT STRIP_TAC 1425 >> IMP_RES_TAC replace_arrow 1426 >> IMP_RES_TAC comp); 1427 1428(* from axiomatic presentation to sequent calculus *) 1429val arrowToGentzenExt_def = Define ` 1430 arrowToGentzenExt (X :'a arrow_extension) (E :'a gentzen_extension) = 1431 !A B. X A B ==> gentzenSequent E (OneForm A) B`; 1432 1433val NLToNL_Sequent = store_thm ( 1434 "NLToNL_Sequent", ``arrowToGentzenExt NL NL_Sequent``, 1435 REWRITE_TAC [arrowToGentzenExt_def] 1436 >> RW_TAC std_ss [NL_def, EMPTY_REL_DEF]); 1437 1438val NLPToNLP_Sequent = store_thm ( 1439 "NLPToNLP_Sequent", ``arrowToGentzenExt NLP NLP_Sequent``, 1440 REWRITE_TAC [arrowToGentzenExt_def] 1441 >> REWRITE_TAC [NLP_cases] 1442 >> REPEAT STRIP_TAC 1443 >> ASM_REWRITE_TAC [] 1444 >> ASSUME_TAC (ISPEC ``NLP_Sequent`` no_extend) 1445 >> MATCH_MP_TAC NLPextensionSimplDot 1446 >> ASM_REWRITE_TAC [] 1447 >> REWRITE_TAC [SeqAxiom]); 1448 1449val LToL_Sequent = store_thm ( 1450 "LToL_Sequent", ``arrowToGentzenExt L L_Sequent``, 1451 REWRITE_TAC [arrowToGentzenExt_def] 1452 >> REWRITE_TAC [L_cases] 1453 >> ASSUME_TAC (ISPEC ``L_Sequent`` no_extend) 1454 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1455 >> ASM_REWRITE_TAC [] 1456 >| [ MATCH_MP_TAC LextensionSimplDot' >> ASM_REWRITE_TAC [] \\ 1457 REWRITE_TAC [SeqAxiom], 1458 MATCH_MP_TAC LextensionSimplDot >> ASM_REWRITE_TAC [] \\ 1459 REWRITE_TAC [SeqAxiom] ]); 1460 1461val LPToLP_Sequent = store_thm ( 1462 "LPToLP_Sequent", ``arrowToGentzenExt LP LP_Sequent``, 1463 REWRITE_TAC [arrowToGentzenExt_def, LP_def, RUNION] 1464 >> REPEAT STRIP_TAC (* two sub-goals here *) 1465 >| [ (* goal 1 (of 2) *) 1466 MP_TAC NLP_Sequent_LP_Sequent \\ 1467 POP_ASSUM (MP_TAC o (MATCH_MP (REWRITE_RULE [arrowToGentzenExt_def] NLPToNLP_Sequent))) \\ 1468 REWRITE_TAC [mono_E], 1469 (* goal 2 (of 2) *) 1470 MP_TAC L_Sequent_LP_Sequent \\ 1471 POP_ASSUM (MP_TAC o (MATCH_MP (REWRITE_RULE [arrowToGentzenExt_def] LToL_Sequent))) \\ 1472 REWRITE_TAC [mono_E] ]); 1473 1474val arrowToGentzen = store_thm ( 1475 "arrowToGentzen", 1476 ``!E X A B. arrow X A B ==> arrowToGentzenExt X E ==> gentzenSequent E (OneForm A) B``, 1477 GEN_TAC 1478 >> HO_MATCH_MP_TAC arrow_ind 1479 >> REPEAT STRIP_TAC (* 7 goals here, first is easy *) 1480 >- REWRITE_TAC [SeqAxiom] (* rest 6 goals *) 1481 >| [ (* goal 1 (of 6) *) 1482 MATCH_MP_TAC RightSlashDot >> RES_TAC, 1483 (* goal 2 (of 6) *) 1484 MATCH_MP_TAC DotRightSlash' >> RES_TAC, 1485 (* goal 3 (of 6) *) 1486 MATCH_MP_TAC RightBackslashDot >> RES_TAC, 1487 (* goal 4 (of 6) *) 1488 MATCH_MP_TAC DotRightBackslash' >> RES_TAC, 1489 (* goal 5 (of 6) *) 1490 MATCH_MP_TAC CutRuleSimpl \\ 1491 Q.EXISTS_TAC `A'` \\ 1492 RES_TAC \\ 1493 ASM_REWRITE_TAC [], 1494 (* goal 6 (of 6) *) 1495 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [arrowToGentzenExt_def])) \\ 1496 RES_TAC ]); 1497 1498(* particular cases for NLP, L; LP and NL systems *) 1499val arrowToGentzenNL = store_thm ( 1500 "arrowToGentzenNL", 1501 ``!A B. arrow NL A B ==> gentzenSequent NL_Sequent (OneForm A) B``, 1502 REPEAT STRIP_TAC 1503 >> irule arrowToGentzen 1504 >> Q.EXISTS_TAC `NL` 1505 >> ASM_REWRITE_TAC [NLToNL_Sequent]); 1506 1507val arrowToGentzenNLP = store_thm ( 1508 "arrowToGentzenNLP", 1509 ``!A B. arrow NLP A B ==> gentzenSequent NLP_Sequent (OneForm A) B``, 1510 REPEAT STRIP_TAC 1511 >> irule arrowToGentzen 1512 >> Q.EXISTS_TAC `NLP` 1513 >> ASM_REWRITE_TAC [NLPToNLP_Sequent]); 1514 1515val arrowToGentzenL = store_thm ( 1516 "arrowToGentzenL", 1517 ``!A B. arrow L A B ==> gentzenSequent L_Sequent (OneForm A) B``, 1518 REPEAT STRIP_TAC 1519 >> irule arrowToGentzen 1520 >> Q.EXISTS_TAC `L` 1521 >> ASM_REWRITE_TAC [LToL_Sequent]); 1522 1523val arrowToGentzenLP = store_thm ( 1524 "arrowToGentzenLP", 1525 ``!A B. arrow LP A B ==> gentzenSequent LP_Sequent (OneForm A) B``, 1526 REPEAT STRIP_TAC 1527 >> irule arrowToGentzen 1528 >> Q.EXISTS_TAC `LP` 1529 >> ASM_REWRITE_TAC [LPToLP_Sequent]); 1530 1531(* from sequent calculus to axiomatic presentation. 1532 Notice the strange thing here: the order of T1 and T2 are changed from E to X. *) 1533val gentzenToArrowExt_def = Define 1534 `gentzenToArrowExt (E :'a gentzen_extension) (X :'a arrow_extension) = 1535 (!T1 T2. E T1 T2 ==> X (deltaTranslation T2) (deltaTranslation T1))`; 1536 1537(* Build arrow_extensions directly from gentzen_extensions *) 1538val ToArrowExt_def = Define ` 1539 ToArrowExt (E :'a gentzen_extension) = 1540 CURRY { (deltaTranslation y, deltaTranslation x) | (x,y) IN (UNCURRY E) }`; 1541 1542val ToArrowExt_thm = store_thm ( 1543 "ToArrowExt_thm", 1544 ``!E T1 T2. E T1 T2 ==> (ToArrowExt E) (deltaTranslation T2) (deltaTranslation T1)``, 1545 REPEAT STRIP_TAC 1546 >> REWRITE_TAC [ToArrowExt_def, CURRY_DEF] 1547 >> ONCE_REWRITE_TAC [GSYM SPECIFICATION] 1548 >> ONCE_REWRITE_TAC [GSPECIFICATION] 1549 >> Q.EXISTS_TAC `(T2, T1)` 1550 >> `(T1, T2) IN (UNCURRY E)` 1551 by PROVE_TAC [UNCURRY_DEF, SPECIFICATION] 1552 >> FULL_SIMP_TAC std_ss []); 1553 1554val gentzenToArrowExt_thm = store_thm ( 1555 "gentzenToArrowExt_thm", ``!E. gentzenToArrowExt E (ToArrowExt E)``, 1556 REWRITE_TAC [gentzenToArrowExt_def, ToArrowExt_thm]); 1557 1558val NL_SequentToNL = store_thm ( 1559 "NL_SequentToNL", ``gentzenToArrowExt NL_Sequent NL``, 1560 REWRITE_TAC [gentzenToArrowExt_def] 1561 >> RW_TAC std_ss [NL_Sequent_def, EMPTY_REL_DEF]); 1562 1563val NLP_SequentToNLP = store_thm ( 1564 "NLP_SequentToNLP", ``gentzenToArrowExt NLP_Sequent NLP``, 1565 REWRITE_TAC [gentzenToArrowExt_def] 1566 >> REWRITE_TAC [NLP_Sequent_cases] 1567 >> REPEAT STRIP_TAC 1568 >> ASM_REWRITE_TAC [deltaTranslation_def] 1569 >> REWRITE_TAC [NLP_rules]); 1570 1571val L_SequentToL = store_thm ( 1572 "L_SequentToL", ``gentzenToArrowExt L_Sequent L``, 1573 REWRITE_TAC [gentzenToArrowExt_def] 1574 >> REWRITE_TAC [L_Sequent_cases] 1575 >> REPEAT STRIP_TAC 1576 >> ASM_REWRITE_TAC [deltaTranslation_def] 1577 >| [ REWRITE_TAC [L_rule_lr], 1578 REWRITE_TAC [L_rule_rl] ]); 1579 1580val LP_SequentToLP = store_thm ( 1581 "LP_SequentToLP", ``gentzenToArrowExt LP_Sequent LP``, 1582 REWRITE_TAC [gentzenToArrowExt_def, LP_Sequent_def, RUNION] 1583 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1584 >| [ (* goal 1 (of 2) *) 1585 POP_ASSUM (MP_TAC o (MATCH_MP (REWRITE_RULE [gentzenToArrowExt_def] NLP_SequentToNLP))) \\ 1586 MP_TAC NLPextendsLP \\ 1587 RW_TAC std_ss [RSUBSET], 1588 (* goal 2 (of 2) *) 1589 POP_ASSUM (MP_TAC o (MATCH_MP (REWRITE_RULE [gentzenToArrowExt_def] L_SequentToL))) \\ 1590 MP_TAC LextendsLP \\ 1591 RW_TAC std_ss [RSUBSET] ]); 1592 1593val gentzenToArrow' = store_thm ( 1594 "gentzenToArrow'", 1595 ``!X E Gamma A. gentzenSequent E Gamma A ==> gentzenToArrowExt E X ==> 1596 arrow X (deltaTranslation Gamma) A``, 1597 GEN_TAC 1598 >> HO_MATCH_MP_TAC gentzenSequent_ind 1599 >> REPEAT STRIP_TAC (* 9 sub-goals here *) 1600 >| [ (* goal 1 *) 1601 REWRITE_TAC [deltaTranslation_def, one], 1602 (* goal 2 *) 1603 RES_TAC >> POP_ASSUM MP_TAC \\ 1604 REWRITE_TAC [deltaTranslation_def, beta], 1605 (* goal 3 *) 1606 RES_TAC >> POP_ASSUM MP_TAC \\ 1607 REWRITE_TAC [deltaTranslation_def, gamma], 1608 (* goal 4 *) 1609 RES_TAC >> POP_ASSUM MP_TAC >> POP_ASSUM MP_TAC \\ 1610 RW_TAC std_ss [deltaTranslation_def, Dot_mono], 1611 (* goal 5 *) 1612 RES_TAC \\ 1613 SUFF_TAC ``arrow X (deltaTranslation (Comma (OneForm (Slash A A')) Gamma'')) 1614 (deltaTranslation (OneForm A))`` >| (* 2 sub-goals here *) 1615 [ (* goal 5.1 (of 2) *) 1616 DISCH_TAC \\ 1617 `arrow X (deltaTranslation Gamma') (deltaTranslation Gamma)` 1618 by PROVE_TAC [replace_arrow] \\ 1619 IMP_RES_TAC comp, 1620 (* goal 5.2 (of 2) *) 1621 REWRITE_TAC [deltaTranslation_def] \\ 1622 MATCH_MP_TAC beta' \\ 1623 MATCH_MP_TAC Slash_antimono_right \\ 1624 POP_ASSUM ACCEPT_TAC ], 1625 (* goal 6 *) 1626 RES_TAC \\ 1627 SUFF_TAC ``arrow X (deltaTranslation (Comma Gamma'' (OneForm (Backslash A' A)))) 1628 (deltaTranslation (OneForm A))`` >| (* 2 sub-goals here *) 1629 [ (* goal 6.1 (of 2) *) 1630 DISCH_TAC \\ 1631 `arrow X (deltaTranslation Gamma') A''` by PROVE_TAC [replace_arrow'], 1632 (* goal 6.2 (of 2) *) 1633 REWRITE_TAC [deltaTranslation_def] \\ 1634 MATCH_MP_TAC gamma' \\ 1635 MATCH_MP_TAC Backslash_antimono_left \\ 1636 POP_ASSUM ACCEPT_TAC ], 1637 (* goal 7 *) 1638 RES_TAC \\ 1639 SUFF_TAC ``arrow X (deltaTranslation (OneForm (Dot A B))) 1640 (deltaTranslation (Comma (OneForm A) (OneForm B)))`` >| 1641 (* 2 sub-goals here *) 1642 [ (* goal 7.1 *) 1643 DISCH_TAC \\ 1644 `arrow X (deltaTranslation Gamma') A'` by PROVE_TAC [replace_arrow'], 1645 (* goal 7.2 *) 1646 REWRITE_TAC [deltaTranslation_def, one] ], 1647 (* goal 8 *) 1648 RES_TAC \\ 1649 `arrow X (deltaTranslation Gamma) (deltaTranslation (OneForm A))` 1650 by ASM_REWRITE_TAC [deltaTranslation_def] \\ 1651 `arrow X (deltaTranslation Gamma'') A'` by PROVE_TAC [replace_arrow'], 1652 (* goal 9 *) 1653 FULL_SIMP_TAC std_ss [gentzenToArrowExt_def] \\ 1654 RES_TAC \\ 1655 `arrow X (deltaTranslation Delta') (deltaTranslation Delta)` 1656 by PROVE_TAC [arrow_plus] \\ 1657 `arrow X (deltaTranslation Gamma') A` by PROVE_TAC [replace_arrow'] ]); 1658 1659val gentzenToArrow = store_thm ( 1660 "gentzenToArrow", 1661 ``!E X Gamma A. gentzenToArrowExt E X /\ gentzenSequent E Gamma A 1662 ==> arrow X (deltaTranslation Gamma) A``, 1663 REPEAT STRIP_TAC 1664 >> PAT_X_ASSUM ``gentzenToArrowExt E X`` MP_TAC 1665 >> POP_ASSUM MP_TAC 1666 >> REWRITE_TAC [gentzenToArrow']); 1667 1668val gentzenToArrow_E = store_thm ( 1669 "gentzenToArrow_E", 1670 ``!E Gamma A. gentzenSequent E Gamma A ==> arrow (ToArrowExt E) (deltaTranslation Gamma) A``, 1671 REPEAT STRIP_TAC 1672 >> ASSUME_TAC (Q.SPEC `E` gentzenToArrowExt_thm) 1673 >> NTAC 2 (POP_ASSUM MP_TAC) 1674 >> REWRITE_TAC [gentzenToArrow']); 1675 1676val NLGentzenToArrow = store_thm ( 1677 "NLGentzenToArrow", 1678 ``!Gamma A. gentzenSequent NL_Sequent Gamma A ==> arrow NL (deltaTranslation Gamma) A``, 1679 REPEAT STRIP_TAC 1680 >> MP_TAC NL_SequentToNL 1681 >> POP_ASSUM MP_TAC 1682 >> REWRITE_TAC [gentzenToArrow']); 1683 1684val NLPGentzenToArrow = store_thm ( 1685 "NLPGentzenToArrow", 1686 ``!Gamma A. gentzenSequent NLP_Sequent Gamma A ==> arrow NLP (deltaTranslation Gamma) A``, 1687 REPEAT STRIP_TAC 1688 >> MP_TAC NLP_SequentToNLP 1689 >> POP_ASSUM MP_TAC 1690 >> REWRITE_TAC [gentzenToArrow']); 1691 1692val LGentzenToArrow = store_thm ( 1693 "LGentzenToArrow", 1694 ``!Gamma A. gentzenSequent L_Sequent Gamma A ==> arrow L (deltaTranslation Gamma) A``, 1695 REPEAT STRIP_TAC 1696 >> MP_TAC L_SequentToL 1697 >> POP_ASSUM MP_TAC 1698 >> REWRITE_TAC [gentzenToArrow']); 1699 1700val LPGentzenToArrow = store_thm ( 1701 "LPGentzenToArrow", 1702 ``!Gamma A. gentzenSequent LP_Sequent Gamma A ==> arrow LP (deltaTranslation Gamma) A``, 1703 REPEAT STRIP_TAC 1704 >> MP_TAC LP_SequentToLP 1705 >> POP_ASSUM MP_TAC 1706 >> REWRITE_TAC [gentzenToArrow']); 1707 1708(******************************************************************************) 1709(* *) 1710(* Module: Gentzen's Sequent Calculus and Natural Deduction *) 1711(* *) 1712(******************************************************************************) 1713 1714val replaceGentzen = store_thm ("replaceGentzen", 1715 ``!E Gamma Gamma' Delta Delta'. 1716 replace Gamma Gamma' Delta Delta' ==> 1717 gentzenSequent E Delta' (deltaTranslation Delta) ==> 1718 gentzenSequent E Gamma' (deltaTranslation Gamma)``, 1719 X_GEN_TAC ``E :'a gentzen_extension`` 1720 >> Induct_on `replace` 1721 >> REPEAT STRIP_TAC 1722 >> `gentzenSequent E Delta (deltaTranslation Delta)` by PROVE_TAC [SeqAxiomGeneralized] 1723 >> `gentzenSequent E Gamma' (deltaTranslation Gamma)` by PROVE_TAC [] 1724 >> PROVE_TAC [RightDot, deltaTranslation_def]); 1725 1726val replaceGentzen' = store_thm ( 1727 "replaceGentzen'", 1728 ``!Gamma Gamma' Delta Delta' C E. 1729 replace Gamma Gamma' Delta Delta' /\ 1730 gentzenSequent E Delta' (deltaTranslation Delta) /\ 1731 gentzenSequent E Gamma C ==> 1732 gentzenSequent E Gamma' C``, 1733 REPEAT STRIP_TAC 1734 >> MATCH_MP_TAC CutRuleSimpl 1735 >> EXISTS_TAC ``(deltaTranslation Gamma)`` 1736 >> CONJ_TAC (* 2 sub-goals here *) 1737 >| [ (* goal 1 (of 2) *) 1738 IMP_RES_TAC replaceGentzen, 1739 (* goal 2 (of 2) *) 1740 MATCH_MP_TAC SeqTermToForm \\ 1741 ASM_REWRITE_TAC [] ]); 1742 1743val replaceNatDed = store_thm ("replaceNatDed", 1744 ``!E Gamma Gamma' Delta Delta'. 1745 replace Gamma Gamma' Delta Delta' ==> 1746 natDed E Delta' (deltaTranslation Delta) ==> 1747 natDed E Gamma' (deltaTranslation Gamma)``, 1748 GEN_TAC 1749 >> HO_MATCH_MP_TAC replace_ind 1750 >> CONJ_TAC 1751 >- RW_TAC bool_ss [] 1752 >> REWRITE_TAC [deltaTranslation_def] 1753 >> CONJ_TAC 1754 >> REPEAT STRIP_TAC 1755 >> MATCH_MP_TAC DotIntro 1756 >> RW_TAC bool_ss [NatAxiomGeneralized]); 1757 1758(* E T1[A] T2[A] ==> ?T1[Delta]. X T1[Delta] T2[Delta] *) 1759val condCutExt_def = Define ` 1760 condCutExt (E :'a gentzen_extension) = 1761 !Gamma T1 T2 A Delta. 1762 E T1 T2 ==> replace T2 Gamma (OneForm A) Delta 1763 ==> ?Gamma'. E Gamma' Gamma /\ replace T1 Gamma' (OneForm A) Delta`; 1764 1765val conditionOKNL = store_thm ("conditionOKNL", ``condCutExt NL_Sequent``, 1766 REWRITE_TAC [condCutExt_def] 1767 >> REPEAT GEN_TAC 1768 >> GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [NL_Sequent_def] 1769 >> RW_TAC std_ss [EMPTY_REL_DEF]); 1770 1771val conditionOKNLP = store_thm ("conditionOKNLP", ``condCutExt NLP_Sequent``, 1772 REWRITE_TAC [condCutExt_def] 1773 >> REPEAT GEN_TAC 1774 >> GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [NLP_Sequent_cases] 1775 >> REPEAT STRIP_TAC 1776 >> `replace (Comma B A') Gamma (OneForm A) Delta` by PROVE_TAC [] 1777 >> ASM_REWRITE_TAC [] 1778 >> POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) 1779 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1780 >| [ (* goal 1 (of 2) *) 1781 ASM_REWRITE_TAC [] \\ 1782 EXISTS_TAC ``(Comma A' G)`` \\ 1783 CONJ_TAC >| (* 2 sub-goals here *) 1784 [ REWRITE_TAC [NLP_Sequent_rules], 1785 MATCH_MP_TAC replaceRight >> ASM_REWRITE_TAC [] ], 1786 ASM_REWRITE_TAC [] \\ 1787 EXISTS_TAC ``(Comma G B)`` \\ 1788 CONJ_TAC >| (* 2 sub-goals here *) 1789 [ REWRITE_TAC [NLP_Sequent_rules], 1790 MATCH_MP_TAC replaceLeft >> ASM_REWRITE_TAC [] ] ]); 1791 1792val conditionOKL = store_thm ("conditionOKL", ``condCutExt L_Sequent``, 1793 REWRITE_TAC [condCutExt_def] 1794 >> REPEAT GEN_TAC 1795 >> GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [L_Sequent_cases] 1796 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1797 >| [ (* goal 1 *) 1798 ASM_REWRITE_TAC [] \\ 1799 `replace (Comma (Comma A' B) C) Gamma (OneForm A) Delta` 1800 by PROVE_TAC [] \\ 1801 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1802 REPEAT STRIP_TAC >| (* 2 sub sub-goals here *) 1803 [ (* goal 1.1 (of 2) *) 1804 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1805 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 1806 [ (* goal 1.1.1 (of 2) *) 1807 ASM_REWRITE_TAC [] \\ 1808 EXISTS_TAC ``(Comma G' (Comma B C))`` \\ 1809 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 1810 MATCH_MP_TAC replaceLeft \\ 1811 ASM_REWRITE_TAC [], 1812 (* goal 1.1.2 (of 2) *) 1813 ASM_REWRITE_TAC [] \\ 1814 EXISTS_TAC ``(Comma A' (Comma G' C))`` \\ 1815 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 1816 MATCH_MP_TAC replaceRight \\ 1817 MATCH_MP_TAC replaceLeft \\ 1818 ASM_REWRITE_TAC [] ], 1819 (* goal 1.2 (of 2) *) 1820 ASM_REWRITE_TAC [] \\ 1821 EXISTS_TAC ``(Comma A' (Comma B G))`` \\ 1822 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 1823 NTAC 2 (MATCH_MP_TAC replaceRight) \\ 1824 ASM_REWRITE_TAC [] ], 1825 (* goal 2 (of 2) *) 1826 ASM_REWRITE_TAC [] \\ 1827 `replace (Comma A' (Comma B C)) Gamma (OneForm A) Delta` 1828 by PROVE_TAC [] \\ 1829 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1830 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 1831 [ (* goal 2.1 (of 2) *) 1832 ASM_REWRITE_TAC [] \\ 1833 EXISTS_TAC ``(Comma (Comma G B) C)`` \\ 1834 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 1835 NTAC 2 (MATCH_MP_TAC replaceLeft) \\ 1836 ASM_REWRITE_TAC [], 1837 (* goal 2.2 (of 2) *) 1838 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1839 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 1840 [ (* goal 2.2.1 (of 2) *) 1841 ASM_REWRITE_TAC [] \\ 1842 EXISTS_TAC ``(Comma (Comma A' G') C)`` \\ 1843 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 1844 MATCH_MP_TAC replaceLeft \\ 1845 MATCH_MP_TAC replaceRight \\ 1846 ASM_REWRITE_TAC [], 1847 (* goal 2.2.2 (of 2) *) 1848 ASM_REWRITE_TAC [] \\ 1849 EXISTS_TAC ``(Comma (Comma A' B) G')`` \\ 1850 CONJ_TAC >- REWRITE_TAC [L_Sequent_rules] \\ 1851 MATCH_MP_TAC replaceRight \\ 1852 ASM_REWRITE_TAC [] ] ] ]); 1853 1854val condAddExt = store_thm ( 1855 "condAddExt", 1856 ``!E E'. condCutExt E /\ condCutExt E' ==> condCutExt (add_extension E E')``, 1857 REPEAT GEN_TAC 1858 >> REWRITE_TAC [condCutExt_def, RUNION] 1859 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1860 >| [ (* goal 1 (of 2) *) 1861 RES_TAC \\ 1862 Q.EXISTS_TAC `Gamma'` \\ 1863 ASM_REWRITE_TAC [], 1864 (* goal 2 (of 2) *) 1865 RES_TAC \\ 1866 Q.EXISTS_TAC `Gamma'` \\ 1867 ASM_REWRITE_TAC [] ]); 1868 1869val CutNatDed = store_thm ( 1870 "CutNatDed", 1871 ``!Delta A E Gamma C. natDed E Gamma C ==> condCutExt E ==> natDed E Delta A ==> 1872 !Gamma'. replace Gamma Gamma' (OneForm A) Delta ==> natDed E Gamma' C``, 1873 NTAC 2 GEN_TAC 1874 >> Induct_on `natDed` 1875 >> REPEAT CONJ_TAC (* 8 sub-goals here *) 1876 >| [ (* goal 1 (of 8) *) 1877 fix [`E`, `C`] >> rpt STRIP_TAC \\ 1878 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv1)) \\ 1879 RW_TAC std_ss [] \\ 1880 ASM_REWRITE_TAC [], 1881 (* goal 2 (of 8) *) 1882 fix [`E`, `Gamma`, `C`, `B`] >> rpt STRIP_TAC \\ 1883 MATCH_MP_TAC SlashIntro \\ 1884 IMP_RES_TAC replaceLeft \\ 1885 POP_ASSUM (ASSUME_TAC o (SPEC ``(OneForm B)``)) \\ 1886 RES_TAC, 1887 (* goal 3 (of 8) *) 1888 fix [`E`, `Gamma`, `C`, `B`] >> rpt STRIP_TAC \\ 1889 MATCH_MP_TAC BackslashIntro \\ 1890 IMP_RES_TAC replaceRight \\ 1891 POP_ASSUM (ASSUME_TAC o (SPEC ``(OneForm B)``)) \\ 1892 RES_TAC, 1893 (* goal 4 (of 8) *) 1894 fix [`E`, `Gamma`, `Gamma'`, `C`, `C'`] >> rpt STRIP_TAC \\ 1895 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1896 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 1897 [ (* goal 4.1 (of 2) *) 1898 ASM_REWRITE_TAC [] \\ 1899 MATCH_MP_TAC DotIntro \\ 1900 CONJ_TAC >- RES_TAC \\ 1901 ASM_REWRITE_TAC [], 1902 (* goal 4.2 (of 2) *) 1903 ASM_REWRITE_TAC [] \\ 1904 MATCH_MP_TAC DotIntro \\ 1905 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 1906 RES_TAC ], 1907 (* goal 5 (of 8) *) 1908 fix [`E`, `Gamma`, `Gamma'`, `C`, `C'`] >> rpt STRIP_TAC \\ 1909 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1910 REPEAT STRIP_TAC (* 2 sub-goals here, same tacticals *) \\ 1911 ASM_REWRITE_TAC [] \\ 1912 MATCH_MP_TAC SlashElim \\ 1913 Q.EXISTS_TAC `C'` \\ 1914 ASM_REWRITE_TAC [] >> RES_TAC, 1915 (* goal 6 (of 8) *) 1916 fix [`E`, `Gamma`, `Gamma'`, `C`, `C'`] >> rpt STRIP_TAC \\ 1917 POP_ASSUM (MP_TAC o (MATCH_MP replace_inv2)) \\ 1918 REPEAT STRIP_TAC (* 2 sub-goals here, same tacticals *) \\ 1919 ASM_REWRITE_TAC [] \\ 1920 MATCH_MP_TAC BackslashElim \\ 1921 Q.EXISTS_TAC `C'` \\ 1922 ASM_REWRITE_TAC [] >> RES_TAC, 1923 (* goal 7 (of 8) *) 1924 fix [`E`, `Gamma`, `Gamma'`, `Gamma''`, `A'`, `B`, `C'`] \\ 1925 REPEAT STRIP_TAC \\ 1926 PAT_X_ASSUM ``replace Gamma Gamma' (Comma (OneForm A') (OneForm B)) Gamma''`` 1927 (ASSUME_TAC o (MATCH_MP doubleReplace)) \\ 1928 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`Gamma'''`, `A`, `Delta`])) \\ 1929 RES_TAC (* 2 sub-goals here, same tactical *) \\ 1930 IMP_RES_TAC DotElim, 1931 (* goal 8 (of 8) *) 1932 fix [`E`, `C`, `Gamma`, `Gamma'`, `Delta'`, `Delta''`] \\ 1933 REPEAT STRIP_TAC \\ 1934 PAT_X_ASSUM ``condCutExt E ==> P`` 1935 (ASSUME_TAC o 1936 (fn thm => (MATCH_MP thm (ASSUME ``condCutExt E``)))) \\ 1937 PAT_X_ASSUM ``natDed E Delta A ==> P`` 1938 (ASSUME_TAC o 1939 (fn thm => (MATCH_MP thm (ASSUME ``natDed E Delta A``)))) \\ 1940 PAT_X_ASSUM ``condCutExt E`` 1941 (ASSUME_TAC o (REWRITE_RULE [condCutExt_def])) \\ 1942 PAT_X_ASSUM ``replace Gamma Gamma' Delta' Delta''`` 1943 (ASSUME_TAC o (MATCH_MP doubleReplace)) \\ 1944 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`Gamma''`, `A`, `Delta`])) \\ 1945 POP_ASSUM (MP_TAC o 1946 (fn thm => (MATCH_MP 1947 thm (ASSUME ``replace Gamma' Gamma'' (OneForm A) Delta``)))) \\ 1948 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 1949 [ (* goal 8.1 (of 2) *) 1950 MATCH_MP_TAC NatExt \\ 1951 Q.EXISTS_TAC `G` \\ 1952 Q.EXISTS_TAC `Delta'` \\ 1953 Q.EXISTS_TAC `Delta''` \\ 1954 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 1955 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 1956 PAT_X_ASSUM ``!Gamma'. replace Gamma Gamma' (OneForm A) Delta ==> P`` 1957 (ASSUME_TAC o (Q.SPEC `G`)) \\ 1958 RES_TAC, 1959 (* goal 8.2 (of 2) *) 1960 PAT_X_ASSUM ``!Gamma T1 T2 A Delta. E T1 T2 ==> P`` 1961 (ASSUME_TAC o 1962 (Q.SPECL [`G`, `Delta'`, `Delta''`, `A`, `Delta`])) \\ 1963 POP_ASSUM (ASSUME_TAC o 1964 (fn thm => (MP thm (ASSUME ``(E :'a gentzen_extension) Delta' Delta''``)))) \\ 1965 POP_ASSUM (ASSUME_TAC o 1966 (fn thm => (MP thm (ASSUME ``replace Delta'' G (OneForm A) Delta``)))) \\ 1967 POP_ASSUM MP_TAC >> STRIP_TAC \\ 1968 PAT_X_ASSUM ``replace Gamma Gamma'' Delta' G`` 1969 (ASSUME_TAC o (MATCH_MP replaceSameP)) \\ 1970 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Gamma'''`)) \\ 1971 POP_ASSUM (Q.X_CHOOSE_TAC `G'`) \\ 1972 POP_ASSUM MP_TAC >> STRIP_TAC \\ 1973 MATCH_MP_TAC NatExt \\ 1974 Q.EXISTS_TAC `G'` \\ 1975 Q.EXISTS_TAC `Gamma'''` \\ 1976 Q.EXISTS_TAC `G` \\ 1977 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 1978 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 1979 PAT_X_ASSUM ``!Gamma'. P`` MATCH_MP_TAC \\ 1980 MATCH_MP_TAC replaceTrans' \\ 1981 Q.EXISTS_TAC `Delta'` \\ 1982 Q.EXISTS_TAC `Gamma'''` \\ 1983 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 1984 ASM_REWRITE_TAC [] ] ] ); 1985 1986val natDedComposition = store_thm ( 1987 "natDedComposition", 1988 ``!E Gamma F1 F2. condCutExt E /\ natDed E Gamma F1 /\ natDed E (OneForm F1) F2 1989 ==> natDed E Gamma F2``, 1990 REPEAT STRIP_TAC 1991 >> irule CutNatDed 1992 >> ASM_REWRITE_TAC [] 1993 >> take [`F1`, `Gamma`, `OneForm F1`] 1994 >> RW_TAC std_ss [replaceRoot]); 1995 1996(* The easy direction, doesn't depend on new theorems in this section *) 1997val natDedToGentzen = store_thm ( 1998 "natDedToGentzen", 1999 ``!E Gamma C. natDed E Gamma C ==> gentzenSequent E Gamma C``, 2000 HO_MATCH_MP_TAC natDed_ind (* or: Induct_on `natDed` *) 2001 >> REPEAT STRIP_TAC (* 8 sub-goals here *) 2002 >| [ (* goal 1 (of 8) *) 2003 REWRITE_TAC [SeqAxiom], 2004 (* goal 2 (of 8) *) 2005 MATCH_MP_TAC RightSlash \\ 2006 ASM_REWRITE_TAC [], 2007 (* goal 3 (of 8) *) 2008 MATCH_MP_TAC RightBackslash \\ 2009 ASM_REWRITE_TAC [], 2010 (* goal 4 (of 8) *) 2011 MATCH_MP_TAC RightDot \\ 2012 ASM_REWRITE_TAC [], 2013 (* goal 5 (of 8) *) 2014 MATCH_MP_TAC CutRule \\ 2015 Q.EXISTS_TAC `Gamma` (* for Delta' *) \\ 2016 EXISTS_TAC ``(Comma (OneForm (Slash A B)) Delta)`` \\ 2017 EXISTS_TAC ``(Slash A B)`` \\ 2018 CONJ_TAC >| (* 2 sub-goals here *) 2019 [ (* goal 5.1 (of 2) *) 2020 MATCH_MP_TAC replaceLeft \\ 2021 REWRITE_TAC [replaceRoot], 2022 (* goal 5.2 (of 2) *) 2023 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2024 MATCH_MP_TAC LeftSlashSimpl \\ 2025 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2026 REWRITE_TAC [SeqAxiom] ], 2027 (* goal 6 (of 8) *) 2028 MATCH_MP_TAC CutRule \\ 2029 Q.EXISTS_TAC `Delta` \\ 2030 EXISTS_TAC ``(Comma Gamma (OneForm (Backslash B A)))`` \\ 2031 EXISTS_TAC ``(Backslash B A)`` \\ 2032 CONJ_TAC >| (* 2 sub-goals here *) 2033 [ (* goal 6.1 (of 2) *) 2034 MATCH_MP_TAC replaceRight \\ 2035 REWRITE_TAC [replaceRoot], 2036 (* goal 6.2 (of 2) *) 2037 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2038 MATCH_MP_TAC LeftBackslashSimpl \\ 2039 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2040 REWRITE_TAC [SeqAxiom] ], 2041 (* goal 7 (of 8) *) 2042 MATCH_MP_TAC replaceGentzen' \\ 2043 Q.EXISTS_TAC `Gamma` \\ 2044 EXISTS_TAC ``(Comma (OneForm A) (OneForm B))`` \\ 2045 Q.EXISTS_TAC `Delta` \\ 2046 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2047 REWRITE_TAC [deltaTranslation_def] \\ 2048 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2049 ASM_REWRITE_TAC [], 2050 (* goal 8 (of 8) *) 2051 MP_TAC (SPEC_ALL SeqExt) >> REPEAT STRIP_TAC \\ 2052 RES_TAC ]); 2053 2054(* The hard direction, heavily depends on theorems proved recently *) 2055val gentzenToNatDed = store_thm ( 2056 "gentzenToNatDed", 2057 ``!E Gamma C. gentzenSequent E Gamma C ==> condCutExt E ==> natDed E Gamma C``, 2058 HO_MATCH_MP_TAC gentzenSequent_ind (* or: Induct_on `gentzenSequent` *) 2059 >> REPEAT CONJ_TAC (* 9 sub-goals here *) 2060 >| [ (* goal 1 (of 9) *) 2061 fix [`E`, `C`] >> rpt STRIP_TAC \\ 2062 REWRITE_TAC [NatAxiom], 2063 (* goal 2 (of 9) *) 2064 fix [`E`, `Gamma`, `C`, `B`] >> rpt STRIP_TAC \\ 2065 RES_TAC \\ 2066 MATCH_MP_TAC SlashIntro >> ASM_REWRITE_TAC [], 2067 (* goal 3 (of 9) *) 2068 fix [`E`, `Gamma`, `C`, `B`] >> rpt STRIP_TAC \\ 2069 RES_TAC \\ 2070 MATCH_MP_TAC BackslashIntro >> ASM_REWRITE_TAC [], 2071 (* goal 4 (of 9) *) 2072 fix [`E`, `Gamma`, `Gamma'`, `C`, `C'`] >> rpt STRIP_TAC \\ 2073 RES_TAC \\ 2074 MATCH_MP_TAC DotIntro >> ASM_REWRITE_TAC [], 2075 (* goal 5 (of 9) *) 2076 fix [`E`, `Gamma`, `Gamma'`, `Gamma''`, `A`, `C`, `C'`] \\ 2077 REPEAT STRIP_TAC \\ 2078 MATCH_MP_TAC natDedComposition \\ 2079 EXISTS_TAC ``(deltaTranslation Gamma)`` \\ 2080 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2081 CONJ_TAC >| (* 2 sub-goals here *) 2082 [ (* goal 5.1 (of 2) *) 2083 irule replaceNatDed \\ 2084 EXISTS_TAC ``(OneForm A)`` \\ 2085 EXISTS_TAC ``(Comma (OneForm (Slash A C)) Gamma'')`` \\ 2086 CONJ_TAC >| (* 2 sub-goals here *) 2087 [ (* goal 5.1.1 (of 2) *) 2088 REWRITE_TAC [deltaTranslation_def] \\ 2089 MATCH_MP_TAC SlashElim \\ 2090 Q.EXISTS_TAC `C` \\ 2091 CONJ_TAC >- REWRITE_TAC [NatAxiom] >> RES_TAC, 2092 (* goal 5.1.2 (of 2) *) 2093 ASM_REWRITE_TAC [] ], 2094 (* goal 5.2 (of 2) *) 2095 MATCH_MP_TAC NatTermToForm >> RES_TAC ], 2096 (* goal 6 (of 9) *) 2097 fix [`E`, `Gamma`, `Gamma'`, `Gamma''`, `A`, `C`, `C'`] \\ 2098 REPEAT STRIP_TAC \\ 2099 MATCH_MP_TAC natDedComposition \\ 2100 EXISTS_TAC ``(deltaTranslation Gamma)`` \\ 2101 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2102 CONJ_TAC >| (* 2 sub-goals here *) 2103 [ (* goal 6.1 (of 2) *) 2104 irule replaceNatDed \\ 2105 EXISTS_TAC ``(OneForm A)`` \\ 2106 EXISTS_TAC ``(Comma Gamma'' (OneForm (Backslash C A)))`` \\ 2107 CONJ_TAC >| (* 2 sub-goals here *) 2108 [ (* goal 6.1.1 (of 2) *) 2109 REWRITE_TAC [deltaTranslation_def] \\ 2110 MATCH_MP_TAC BackslashElim \\ 2111 Q.EXISTS_TAC `C` \\ 2112 CONJ_TAC >- RES_TAC \\ 2113 REWRITE_TAC [NatAxiom], 2114 (* goal 6.1.2 (of 2) *) 2115 ASM_REWRITE_TAC [] ], 2116 (* goal 6.2 (of 2) *) 2117 MATCH_MP_TAC NatTermToForm >> RES_TAC ], 2118 (* goal 7 (of 9) *) 2119 fix [`E`, `Gamma`, `Gamma'`, `A`, `B`, `C`] >> rpt STRIP_TAC \\ 2120 MATCH_MP_TAC natDedComposition \\ 2121 EXISTS_TAC ``(deltaTranslation Gamma)`` \\ 2122 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2123 CONJ_TAC >| (* 2 sub-goals here *) 2124 [ (* goal 7.1 (of 2) *) 2125 irule replaceNatDed \\ 2126 EXISTS_TAC ``(Comma (OneForm A) (OneForm B))`` \\ 2127 EXISTS_TAC ``(OneForm (Dot A B))`` \\ 2128 CONJ_TAC >| (* 2 sub-goals here *) 2129 [ (* goal 7.1.1 (of 2) *) 2130 REWRITE_TAC [deltaTranslation_def] \\ 2131 REWRITE_TAC [NatAxiom], 2132 (* goal 7.1.2 (of 2) *) 2133 ASM_REWRITE_TAC [] ], 2134 (* goal 7.2 (of 2) *) 2135 MATCH_MP_TAC NatTermToForm >> RES_TAC ], 2136 (* goal 8 (of 9) *) 2137 fix [`E`, `Gamma`, `Gamma'`, `Gamma''`, `C`, `C'`] \\ 2138 REPEAT STRIP_TAC \\ 2139 MATCH_MP_TAC natDedComposition \\ 2140 EXISTS_TAC ``(deltaTranslation Gamma')`` \\ 2141 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2142 CONJ_TAC >| (* 2 sub-goals here *) 2143 [ (* goal 8.1 (of 2) *) 2144 irule replaceNatDed \\ 2145 EXISTS_TAC ``(OneForm C)`` \\ 2146 Q.EXISTS_TAC `Gamma` \\ 2147 CONJ_TAC >| (* 2 sub-goals here *) 2148 [ (* goal 8.1.1 (of 2) *) 2149 REWRITE_TAC [deltaTranslation_def] >> RES_TAC, 2150 (* goal 8.1.2 (of 2) *) 2151 ASM_REWRITE_TAC [] ], 2152 (* goal 8.2 (of 2) *) 2153 MATCH_MP_TAC NatTermToForm >> RES_TAC ], 2154 (* goal 9 (of 9) *) 2155 fix [`E`, `Gamma`, `Gamma'`, `Delta`, `Delta'`, `C`] \\ 2156 REPEAT STRIP_TAC \\ 2157 MATCH_MP_TAC NatExt \\ 2158 Q.EXISTS_TAC `Gamma` \\ 2159 Q.EXISTS_TAC `Delta` \\ 2160 Q.EXISTS_TAC `Delta'` \\ 2161 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2162 CONJ_TAC >- ASM_REWRITE_TAC [] \\ 2163 RES_TAC ]); 2164 2165val gentzenEqNatDed = store_thm ( 2166 "gentzenEqNatDed", 2167 ``!E Gamma C. condCutExt E ==> (gentzenSequent E Gamma C = natDed E Gamma C)``, 2168 REPEAT STRIP_TAC 2169 >> EQ_TAC (* 2 sub-goals here *) 2170 >| [ (* goal 1 (of 2) *) 2171 DISCH_TAC \\ 2172 irule gentzenToNatDed \\ (* 2 sub-goals sharing the same tactical *) 2173 ASM_REWRITE_TAC [], 2174 (* goal 2 (of 2) *) 2175 REWRITE_TAC [natDedToGentzen] ]); 2176 2177val NLgentzenEqNatDed = store_thm ( 2178 "NLgentzenEqNatDed", 2179 ``!Gamma C. gentzenSequent NL_Sequent Gamma C = natDed NL_Sequent Gamma C``, 2180 REPEAT STRIP_TAC 2181 >> MP_TAC conditionOKNL 2182 >> REWRITE_TAC [gentzenEqNatDed]); 2183 2184val LgentzenEqNatDed = store_thm ( 2185 "LgentzenEqNatDed", 2186 ``!Gamma C. gentzenSequent L_Sequent Gamma C = natDed L_Sequent Gamma C``, 2187 REPEAT STRIP_TAC 2188 >> MP_TAC conditionOKL 2189 >> REWRITE_TAC [gentzenEqNatDed]); 2190 2191val NLPgentzenEqNatDed = store_thm ( 2192 "NLPgentzenEqNatDed", 2193 ``!Gamma C. gentzenSequent NLP_Sequent Gamma C = natDed NLP_Sequent Gamma C``, 2194 REPEAT STRIP_TAC 2195 >> MP_TAC conditionOKNLP 2196 >> REWRITE_TAC [gentzenEqNatDed]); 2197 2198(******************************************************************************) 2199(* *) 2200(* Module: Arrow and Natural Deduction *) 2201(* *) 2202(******************************************************************************) 2203 2204val natDedToArrow = store_thm ( 2205 "natDedToArrow", 2206 ``!E X Gamma A. gentzenToArrowExt E X ==> 2207 natDed E Gamma A ==> arrow X (deltaTranslation Gamma) A``, 2208 REPEAT STRIP_TAC 2209 >> MATCH_MP_TAC gentzenToArrow 2210 >> Q.EXISTS_TAC `E` 2211 >> CONJ_TAC 2212 >- ASM_REWRITE_TAC [] 2213 >> MATCH_MP_TAC natDedToGentzen 2214 >> ASM_REWRITE_TAC []); 2215 2216val natDedToArrow_E = store_thm ( 2217 "natDedToArrow_E", 2218 ``!E Gamma A. natDed E Gamma A ==> arrow (ToArrowExt E) (deltaTranslation Gamma) A``, 2219 REPEAT GEN_TAC 2220 >> MP_TAC (Q.SPEC `E` gentzenToArrowExt_thm) 2221 >> REWRITE_TAC [natDedToArrow]); 2222 2223val arrowToNatDed = store_thm ( 2224 "arrowToNatDed", 2225 ``!E X A B. condCutExt E /\ arrowToGentzenExt X E /\ arrow X A B 2226 ==> natDed E (OneForm A) B``, 2227 REPEAT STRIP_TAC 2228 >> irule gentzenToNatDed 2229 >> ASM_REWRITE_TAC [] 2230 >> irule arrowToGentzen 2231 >> Q.EXISTS_TAC `X` 2232 >> ASM_REWRITE_TAC []); 2233 2234(******************************************************************************) 2235(* *) 2236(* Grammar support in HOL *) 2237(* *) 2238(******************************************************************************) 2239 2240fun enable_grammar () = let 2241in 2242 add_rule { term_name = "arrow", fixity = Infix (NONASSOC, 450), 2243 pp_elements = [ BreakSpace(1,0), TOK ":-", BreakSpace(1,0), TM, BreakSpace(1,0), TOK "-->", 2244 BreakSpace(1,0) ], 2245 paren_style = OnlyIfNecessary, 2246 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)) }; 2247 2248 add_rule { term_name = "natDed", fixity = Infix (NONASSOC, 450), 2249 pp_elements = [ BreakSpace(1,0), TOK ":-", BreakSpace(1,0), TM, BreakSpace(1,0), TOK "|-n", 2250 BreakSpace(1,0) ], 2251 paren_style = OnlyIfNecessary, 2252 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)) }; 2253 2254 add_rule { term_name = "gentzenSequent", fixity = Infix (NONASSOC, 450), 2255 pp_elements = [ BreakSpace(1,0), TOK ":-", BreakSpace(1,0), TM, BreakSpace(1,0), TOK "|-g", 2256 BreakSpace(1,0) ], 2257 paren_style = OnlyIfNecessary, 2258 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)) }; 2259 2260 add_rule { term_name = "Sequent", fixity = Infix (NONASSOC, 450), 2261 pp_elements = [ BreakSpace(1,0), TOK ":-", BreakSpace(1,0), TM, BreakSpace(1,0), TOK "|-", 2262 BreakSpace(1,0) ], 2263 paren_style = OnlyIfNecessary, 2264 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)) } 2265end; 2266 2267val _ = enable_grammar (); 2268 2269val _ = export_theory (); 2270val _ = html_theory "Lambek"; 2271 2272(* last updated: April 10, 2017 *) 2273