1 2(* ========================================================================== *) 3(* Equivalence of Sequent Calculus and Natural Deduction *) 4(* Working from Troelstra and Schwichtenburg - Basic Proof Theory 2nd Edition *) 5(* Written by Alexander Cox, ANU, u6060697@anu.edu.au *) 6(* Supervised by Michael Norrish, ANU; Data61 *) 7(* ========================================================================== *) 8 9open HolKernel boolLib Parse bossLib 10open bagTheory 11open pred_setTheory 12 13val _ = new_theory "IntuitionisticProof"; 14 15 16val _ = set_fixity "Imp" (Infixr 460); 17val _ = set_fixity "BiImp" (Infix (NONASSOC, 455) ); 18val _ = set_fixity "And" (Infixr 490); 19val _ = set_fixity "Or" (Infixr 490); 20val _ = set_fixity "Not" (Prefix 510); 21 22val _ = Datatype `formula = 23 Var 'a 24 | Or formula formula 25 | And formula formula 26 | Imp formula formula 27 | Bot`; 28 29 30val Not_def = Define `Not A = A Imp Bot`; 31val BiImp_def = Define `A BiImp B = (A Imp B) And (B Imp A)`; 32val Top_def = Define `Top = Bot Imp Bot`; 33 34(* Natural Deduction for intuitionistic logic *) 35(* N is the 'deduciblility' relation for this system *) 36(* A, B and C are used to represent formulae *) 37(* D, D1, D2, D3 are used to represent the set of open assumptions *) 38(* I'm representing the deductions simply with unlabeled sets of *) 39(* open assumptions, as in T&S 2.1.8-2.1.9 (p.41--44) *) 40 41val (N_rules, N_ind, N_cases) = Hol_reln ` 42 (��� (A :'a formula). N {A} A) (* Base case *) 43��� (���A B D1 D2. (N D1 A) ��� (N D2 B) 44 ==> (N (D1 UNION D2) (A And B))) (* And Intro *) 45��� (���A B D. (N D (A And B)) ==> N D A) (* And Elimination Left Conjunct *) 46��� (���A B D. (N D (A And B)) ==> N D B) (* And Elim Right Conjunct *) 47��� (���A B D. (N (A INSERT D) B) ==> N D (A Imp B)) (* Imp Intro *) 48��� (���A B D1 D2. (N D1 (A Imp B)) ��� (N D2 A) 49 ==> N (D1 UNION D2) B) (* Imp Elim *) 50��� (���A B D. N D A ==> N D (A Or B)) (* Or Intro right *) 51��� (���A B D. N D B ==> N D (A Or B)) (* Or Intro left *) 52��� (���A B C D D1 D2. (N D (A Or B)) ��� (* Or Elim *) 53(N (A INSERT D1) C) ��� (N (B INSERT D2) C) ==> N (D ��� D1 ��� D2) C) 54��� (���A D. (N D Bot) ==> (N D A))`; (* Intuitionistic Absurdity Rule *) 55 56val [N_ax, N_andi, N_andel, N_ander, 57 N_impi, N_impe, N_orir, N_oril, N_ore, N_bot] = CONJUNCTS N_rules; 58 59Theorem N_FINITE: 60 ���D A. N D A ==> FINITE D 61Proof Induct_on `N` >> rw[] 62QED 63 64val (Nd_rules, Nd_ind, Nd_cases) = Hol_reln ` 65 (��� (A :'a formula). Nd {A} A) (* Base case *) 66��� (���A B D1 D2. (Nd D1 A) ��� (Nd D2 B) 67 ==> (Nd (D1 UNION D2) (A And B))) (* And Intro *) 68��� (���A B D. (Nd D (A And B)) ==> Nd D A) (* And Elimination Left Conjunct *) 69��� (���A B D. (Nd D (A And B)) ==> Nd D B) (* And Elim Right Conjunct *) 70��� (���A B D. (Nd D B) ==> Nd (D DELETE A) (A Imp B)) (* Imp Intro *) 71��� (���A B D1 D2. (Nd D1 (A Imp B)) ��� (Nd D2 A) 72 ==> Nd (D1 UNION D2) B) (* Imp Elim *) 73��� (���A B D. Nd D A ==> Nd D (A Or B)) (* Or Intro right *) 74��� (���A B D. Nd D B ==> Nd D (A Or B)) (* Or Intro left *) 75��� (���A B C D D1 D2. (Nd D (A Or B)) ��� (Nd D1 C) ��� (Nd D2 C) 76 ==> Nd (D ��� (D1 DELETE A) ��� (D2 DELETE B)) C) (* Or Elim *) 77��� (���A D. (Nd D Bot) ==> (Nd D A))`; (* Intuitionistic Absurdity Rule *) 78 79val [Nd_ax, Nd_andi, Nd_andel, Nd_ander, 80 Nd_impi, Nd_impe, Nd_orir, Nd_oril, Nd_ore, Nd_bot] = CONJUNCTS Nd_rules; 81 82Theorem N_lw: 83 ���D A. N D A ==> ���B. N (B INSERT D) A 84Proof 85 rw[] >> 86 `N {B} B` by metis_tac[N_ax] >> 87 `N ({B} ��� D) (B And A)` by metis_tac[N_andi] >> 88 `N ({B} ��� D) A` by metis_tac[N_ander] >> 89 metis_tac[INSERT_SING_UNION] 90QED 91 92Theorem Nd_lw: 93���D A. Nd D A ==> ���B. Nd (B INSERT D) A 94Proof 95 rw[] >> 96 `Nd {B} B` by metis_tac[Nd_ax] >> 97 `Nd ({B} ��� D) (B And A)` by metis_tac[Nd_andi] >> 98 `Nd ({B} ��� D) A` by metis_tac[Nd_ander] >> 99 metis_tac[INSERT_SING_UNION] 100QED 101 102Theorem N_lw_SUBSET: 103 ���D'. FINITE D' ==> ���D A. N D A ��� D ��� D' ==> N D' A 104Proof 105 GEN_TAC >> 106 Induct_on `CARD D'` 107 >- (rw[] >> 108 metis_tac[CARD_EQ_0,SUBSET_EMPTY]) 109 >- (rw[] >> 110 Cases_on `D=D'` 111 >- metis_tac[] 112 >- (`���D��� e. (D' = e INSERT D���) ��� D ��� D��� ��� e NOTIN D���` 113 by (`���e. e ��� D' ��� e NOTIN D` 114 by metis_tac[PSUBSET_DEF,PSUBSET_MEMBER] >> 115 qexists_tac `D' DELETE e` >> 116 qexists_tac `e` >> 117 simp[] >> 118 fs[SUBSET_DEF]) >> 119 rw[] >> 120 fs[] >> 121 metis_tac[N_lw])) 122QED 123 124Theorem Nd_lw_SUBSET: 125���D'. FINITE D' ==> ���D A. Nd D A ��� D ��� D' ==> Nd D' A 126Proof 127 GEN_TAC >> 128 Induct_on `CARD D'` 129 >- (rw[] >> metis_tac[CARD_EQ_0,SUBSET_EMPTY]) 130 >- (rw[] >> Cases_on `D=D'` >- metis_tac[] >> 131 `���D��� e. (D' = e INSERT D���) ��� D ��� D��� ��� e NOTIN D���` 132 by (`���e. e ��� D' ��� e NOTIN D` 133 by metis_tac[PSUBSET_DEF,PSUBSET_MEMBER] >> 134 qexists_tac `D' DELETE e` >> 135 qexists_tac `e` >> 136 simp[] >> 137 fs[SUBSET_DEF]) >> 138 rw[] >> 139 fs[] >> 140 metis_tac[Nd_lw]) 141QED 142 143Theorem N_impi_DELETE: 144 ���D A B. N D A ==> N (D DELETE B) (B Imp A) 145Proof 146 rw[] >> 147 `N (B INSERT D) A` by metis_tac[N_lw] >> 148 Cases_on `B ��� D` 149 >- (`���D'. (D = B INSERT D') ��� B NOTIN D'` 150 by metis_tac[DECOMPOSITION] >> 151 fs[] >> 152 `(B INSERT D') DELETE B = D'` 153 by (dsimp[EXTENSION] >> 154 metis_tac[]) >> 155 simp[N_impi]) 156 >- simp[DELETE_NON_ELEMENT_RWT,N_impi] 157QED 158 159Theorem N_Nd: 160 ���D A. N D A <=> Nd D A 161Proof 162 `(���D A:'a formula. N D A ==> Nd D A) ��� 163 (���D A:'a formula. Nd D A ==> N D A)` 164 suffices_by metis_tac[] >> 165 conj_tac 166 >- (Induct_on `N` >> 167 rw[Nd_rules] 168 >- metis_tac[Nd_andel] 169 >- metis_tac[Nd_ander] 170 >- (`Nd ((A INSERT D) DELETE A) (A Imp B)` 171 by metis_tac[Nd_impi] >> 172 fs[DELETE_DEF] >> 173 irule Nd_lw_SUBSET >> 174 conj_tac >- metis_tac[N_FINITE,FINITE_INSERT] >> 175 qexists_tac `D DIFF {A}` >> 176 simp[]) 177 >- metis_tac[Nd_impe] 178 >- (`Nd (D ��� ((A INSERT D1) DELETE A) ��� ((B INSERT D2) DELETE B)) C` 179 by metis_tac[Nd_ore] >> 180 fs[DELETE_DEF] >> 181 irule Nd_lw_SUBSET >> 182 conj_tac >- metis_tac[N_FINITE,FINITE_UNION,FINITE_INSERT] >> 183 qexists_tac `D ��� (D1 DIFF {A}) ��� (D2 DIFF {B})` >> 184 rw[SUBSET_DEF])) 185 >- (Induct_on `Nd` >> 186 rw[N_rules] 187 >- metis_tac[N_andel] 188 >- metis_tac[N_ander] 189 >- metis_tac[N_impi_DELETE] 190 >- metis_tac[N_impe] 191 >- (`N (A INSERT (D1 DELETE A)) C` 192 by (irule N_lw_SUBSET >> 193 rw[] >- metis_tac[N_FINITE] >> 194 qexists_tac `D1` >> 195 rw[DELETE_DEF,SUBSET_DEF]) >> 196 `N (B INSERT (D2 DELETE B)) C` 197 by (irule N_lw_SUBSET >> 198 rw[] >- metis_tac[N_FINITE] >> 199 qexists_tac `D2` >> 200 rw[DELETE_DEF,SUBSET_DEF]) >> 201 metis_tac[N_ore])) 202QED 203 204val NThm = Define `NThm A = N EMPTY A`; 205 206(* Example deductions *) 207val N_example = Q.prove(`NThm (A Imp (B Imp A))`, 208`N {A} A` by rw[N_ax] >> 209`N {B} B` by rw[N_ax] >> 210`{A} UNION {B} = {A;B}` by simp[UNION_DEF,INSERT_DEF] >> 211`N {A;B} (A And B)` by metis_tac[N_andi] >> 212`N {A;B} (A)` by metis_tac[N_andel] >> 213`N {A} (B Imp A)` by (irule N_impi >> simp[INSERT_COMM]) >> 214`N {} (A Imp (B Imp A))` by metis_tac[N_impi] >> 215 rw[NThm]); 216 217val N_example = Q.prove(`NThm (Bot Imp A)`, 218 `N {Bot} Bot` by rw[N_rules] >> 219 `N {Bot} A` by rw[N_rules] >> 220 `{} = ({Bot} DIFF {Bot})` by rw[DIFF_DEF] >> 221 `N EMPTY (Bot Imp A)` by metis_tac[N_rules] >> 222 rw[NThm]); 223 224 225(* Sequent Calculus (Gentzen System) for intuitionistic logic *) 226(* G is the 'deduciblility' relation for this system *) 227(* A, B and C are used to represent formulae *) 228(* �� is used to represent the multiset of the antecedents *) 229(* The consequent is always a single formula in intuitionistic logic *) 230 231val (G_rules, G_ind, G_cases) = Hol_reln ` 232 (���(A:'a formula) ��. (A <: ��) ��� FINITE_BAG �� ==> G �� A) (* Ax *) 233��� (��� A ��. (Bot <: ��) ��� FINITE_BAG �� ==> G �� A) (* LBot *) 234��� (���A �� C. (G ({|A;A|} ��� ��) C) 235 ==> G ({|A|} ��� ��) C) (* Left Contraction *) 236��� (���A B �� C. (G (BAG_INSERT A ��) C) 237 ==> (G (BAG_INSERT (A And B) ��) C)) (* Left And 1 *) 238��� (���A B �� C. (G (BAG_INSERT B ��) C) 239 ==> (G (BAG_INSERT (A And B) ��) C)) (* Left And 2 *) 240��� (���A B ��. (G �� A) ��� (G �� B) 241 ==> (G �� (A And B))) (* Right And *) 242��� (���A B �� C. (G (BAG_INSERT A ��) C) 243 ��� (G (BAG_INSERT B ��) C) 244 ==> (G (BAG_INSERT (A Or B) ��) C)) (* Left Or *) 245��� (���A B ��. (G �� A) 246 ==> (G �� (A Or B))) (* Right Or 1 *) 247��� (���A B ��. (G �� B) 248 ==> (G �� (A Or B))) (* Right Or 2 *) 249��� (���A B �� C. (G �� A) ��� (G (BAG_INSERT B ��) C) 250 ==> (G (BAG_INSERT (A Imp B) ��) C)) (* Left Imp *) 251��� (���A B ��. (G (BAG_INSERT A ��) B) 252 ==> (G �� (A Imp B))) (* Right Imp *) 253��� (���A B �� ��. (G �� A) ��� (G (BAG_INSERT A ��) B) ==> G (�� ��� ��) B)` (* Cut *) 254 255val [G_ax, G_bot, G_lc, G_landl, G_landr, G_rand, 256 G_lor, G_rorl, G_rorr, G_limp, G_rimp, G_cut] = CONJUNCTS G_rules; 257 258val GThm = Define `GThm A = G EMPTY_BAG A`; 259 260val G_example1 = 261 Q.prove(`GThm ((A And B) Imp (B And A))`, rw[GThm,G_rules]); 262 263val G_example2 = Q.prove (`GThm ((A Imp (A Imp B)) Imp (A Imp B))`, 264rw[GThm] >> 265`G {|(A Imp A Imp B)|} (A Imp B)` suffices_by metis_tac[G_rules] >> 266`G {|A;(A Imp A Imp B)|} (B)` suffices_by metis_tac[G_rules] >> 267`G {|A|} (A)` by metis_tac[G_ax,BAG_IN_BAG_INSERT,FINITE_BAG] >> 268`G {|B;A|} (B)` by metis_tac[G_ax,BAG_IN_BAG_INSERT,FINITE_BAG] >> 269(* `G {|A;B|} (B)` by simp[G_lw] >> *) 270(* `G {|B;A|} (B)` by simp[BAG_INSERT_commutes] >> *) 271`G {|(A Imp B);A|} (B)` by metis_tac[G_rules] >> 272`G {|(A Imp A Imp B);A|} (B)` suffices_by metis_tac[BAG_INSERT_commutes] >> 273metis_tac[G_rules]); 274 275val G_land_commutes = Q.prove(`G {| A And B |} �� ==> G {| B And A |} ��`, 276rw[] >> 277`G {|B|} B` by metis_tac[G_ax,BAG_IN_BAG_INSERT,FINITE_BAG] >> 278`G {|B And A|} B` by metis_tac[G_landl] >> 279`G {|A|} A` by metis_tac[G_ax,BAG_IN_BAG_INSERT,FINITE_BAG] >> 280`G {|B And A|} A` by metis_tac[G_landr] >> 281`G {|B And A|} (A And B)` by metis_tac[G_rand] >> 282`G ({|B And A|} ��� {||}) ��` by metis_tac[G_cut] >> 283metis_tac[BAG_UNION_EMPTY]); 284 285Theorem G_FINITE: 286 ����� A. G �� A ==> FINITE_BAG �� 287Proof Induct_on `G` >> rw[] 288QED 289 290(* Thanks for your help with this theorem Michael *) 291Theorem G_lw: 292 ����� A. G �� A ��� �����'. �� ��� ��' ��� FINITE_BAG ��' ��� G ��' A 293Proof 294 Induct_on `G` >> rw[] 295 >- (irule G_ax >> fs[SUB_BAG, BAG_IN]) 296 >- (irule G_bot >> fs[SUB_BAG,BAG_IN]) 297 >- (�����������. ��' = {|A|} ��� �������� 298 by (qexists_tac �����' - {|A|}��� >> irule SUB_BAG_DIFF_EQ >> 299 metis_tac[SUB_BAG_UNION_down]) >> 300 rw[] >> irule G_lc >> first_x_assum irule >> simp[] >> fs[]) 301 >- (�����������. ��' = BAG_INSERT (A And B) �������� 302 by (qexists_tac �����' - {|A And B|}��� >> fs[BAG_INSERT_UNION] >> 303 irule SUB_BAG_DIFF_EQ >> metis_tac[SUB_BAG_UNION_down]) >> 304 rw[] >> irule G_landl >> first_x_assum irule >> fs[SUB_BAG_INSERT]) 305 >- (�����������. ��' = BAG_INSERT (A And B) �������� 306 by (qexists_tac �����' - {|A And B|}��� >> fs[BAG_INSERT_UNION] >> 307 irule SUB_BAG_DIFF_EQ >> metis_tac[SUB_BAG_UNION_down]) >> 308 rw[] >> irule G_landr >> first_x_assum irule >> fs[SUB_BAG_INSERT]) 309 >- (irule G_rand >> simp[]) 310 >- (�����������. ��' = BAG_INSERT (A Or B) �������� 311 by (qexists_tac �����' - {|A Or B|}��� >> fs[BAG_INSERT_UNION] >> 312 irule SUB_BAG_DIFF_EQ >> metis_tac[SUB_BAG_UNION_down]) >> 313 rw[] >> fs[SUB_BAG_INSERT] >> irule G_lor >> conj_tac >> 314 first_x_assum (fn th => irule th >> fs[SUB_BAG_INSERT] >> NO_TAC)) 315 >- simp[G_rorl] 316 >- simp[G_rorr] 317 >- (�����������. ��' = BAG_INSERT (A Imp B) �������� 318 by (qexists_tac �����' - {|A Imp B|}��� >> fs[BAG_INSERT_UNION] >> 319 irule SUB_BAG_DIFF_EQ >> metis_tac[SUB_BAG_UNION_down]) >> 320 rw[] >> irule G_limp >> fs[SUB_BAG_INSERT]) 321 >- simp[SUB_BAG_INSERT, G_rimp] 322 >- (rename [�������� ��� ����� ��� ��������] >> 323 �����������. ����� = ����� ��� ����� ��� �������� 324 by metis_tac[SUB_BAG_EXISTS, COMM_BAG_UNION, ASSOC_BAG_UNION] >> 325 rw[] >> irule G_cut >> 326 rename [���G (BAG_INSERT A _) B���] >> qexists_tac ���A��� >> 327 conj_tac >> first_x_assum irule >> fs[SUB_BAG_INSERT]) 328QED 329 330Theorem G_lw_BAG_MERGE: 331 ����� A. G �� A ==> �����'. FINITE_BAG ��' ==> G (BAG_MERGE ��' ��) A 332Proof 333 rw[] >> 334 irule G_lw >> 335 `FINITE_BAG ��` by metis_tac[G_FINITE] >> 336 simp[FINITE_BAG_MERGE] >> 337 qexists_tac `��` >> 338 simp[SUB_BAG,BAG_INN_BAG_MERGE] 339QED 340 341Theorem G_lw_BAG_UNION: 342 ����� A. G �� A ==> �����'. FINITE_BAG ��' ==> G (�� ��� ��') A 343Proof 344 rw[] >> 345 irule G_lw >> 346 `FINITE_BAG ��` by metis_tac[G_FINITE] >> 347 simp[FINITE_BAG_UNION] >> 348 qexists_tac `��` >> 349 simp[] 350QED 351 352Theorem G_lw_BAG_INSERT: 353 ����� A. G �� A ==> ���B ��'. G (BAG_INSERT B ��) A 354Proof 355 rw[] >> 356 irule G_lw >> 357 `FINITE_BAG ��` by metis_tac[G_FINITE] >> 358 simp[FINITE_BAG_THM] >> 359 qexists_tac `��` >> 360 simp[SUB_BAG_INSERT_I] 361QED 362 363val G_lc_AeA = 364 Q.prove(`���A e ��'. G (BAG_INSERT A (BAG_INSERT e (BAG_INSERT A ��'))) B 365 ==> G (BAG_INSERT e (BAG_INSERT A ��')) B`, 366 rw[] >> 367 `G ({|A;A|} ��� ({|e|} ��� ��')) B` 368 by (fs[BAG_UNION_INSERT,ASSOC_BAG_UNION,BAG_INSERT_UNION] >> 369 simp[COMM_BAG_UNION] >> 370 fs[EL_BAG,BAG_UNION]) >> 371 `G ({|A|} ��� ({|e|} ��� ��')) B` 372 by metis_tac[G_lc] >> 373 `G (({|A|} ��� {|e|}) ��� ��') B` 374 by fs[ASSOC_BAG_UNION] >> 375 `G (({|e|} ��� {|A|}) ��� ��') B` 376 by fs[COMM_BAG_UNION] >> 377 fs[BAG_INSERT_UNION] >> 378 fs[EL_BAG] >> 379 simp[ASSOC_BAG_UNION]); 380 381val unibag_AA_A = Q.prove(`unibag ({|A;A|} ��� ��) = unibag ({|A|} ��� ��)`, 382 simp[unibag_thm]); 383 384Theorem G_unibag: 385 ����� A. G �� A <=> G (unibag ��) A 386Proof 387 rw[] >> EQ_TAC 388 >- (`�����. FINITE_BAG �� ==> ���A. G �� A ==> G (unibag ��) A` 389 suffices_by metis_tac[G_FINITE] >> 390 gen_tac >> 391 Induct_on `BAG_CARD ��` >> 392 rw[] 393 >- (`�� = {||}` by metis_tac[BCARD_0] >> 394 fs[]) 395 >- (Cases_on `unibag �� = ��` >- fs[] >> 396 drule_then strip_assume_tac unibag_DECOMPOSE >> 397 rename [`�� = {|B;B|} ��� ��0`,`SUC n = BAG_CARD ��`] >> 398 `G ({|B|} ��� ��0) A` by metis_tac[G_lc] >> 399 `BAG_CARD ({|B|} ��� ��0) = n` by fs[BAG_CARD_THM] >> 400 `FINITE_BAG ({|B|} ��� ��0)` by fs[] >> 401 metis_tac[unibag_AA_A])) 402 >- metis_tac[unibag_SUB_BAG,G_lw,G_FINITE,unibag_FINITE] 403QED 404 405Theorem N_G: 406 ���D A. N D A ==> G (BAG_OF_SET D) A 407Proof 408 Induct_on `N` >> 409 rw[G_rules] 410 >- (irule G_rand >> conj_tac 411 >- (`G (BAG_OF_SET (D' ��� D)) A` suffices_by metis_tac[UNION_COMM] >> 412 simp[BAG_OF_SET_UNION] >> 413 metis_tac[G_lw_BAG_MERGE,G_FINITE]) 414 >- (simp[BAG_OF_SET_UNION] >> 415 metis_tac[G_lw_BAG_MERGE,G_FINITE])) 416 >- (`G {|A|} A` by metis_tac[G_ax,BAG_IN_BAG_INSERT,FINITE_BAG] >> 417 `G {|A And B|} A` by metis_tac[G_landl] >> 418 `G ((BAG_OF_SET D) ��� {||}) A` by metis_tac[G_cut] >> 419 metis_tac[BAG_UNION_EMPTY]) 420 >- (`G {|A'|} A'` by metis_tac[G_ax,BAG_IN_BAG_INSERT,FINITE_BAG] >> 421 `G {|A And A'|} A'` by metis_tac[G_landr] >> 422 `G ((BAG_OF_SET D) ��� {||}) A'` by metis_tac[G_cut] >> 423 metis_tac[BAG_UNION_EMPTY]) 424 >- (irule G_rimp >> 425 fs[BAG_OF_SET_INSERT] >> 426 irule G_lw >> 427 simp[] >> 428 drule G_FINITE >> 429 rw[] >> 430 qexists_tac `BAG_MERGE {|A|} (BAG_OF_SET D)` >> 431 simp[BAG_MERGE_ELBAG_SUB_BAG_INSERT]) 432 >- (rename[`N D (A Imp B)`] >> 433 simp[BAG_OF_SET_UNION] >> 434 `FINITE_BAG (BAG_OF_SET D')` by metis_tac[N_FINITE,FINITE_BAG_OF_SET] >> 435 `G (BAG_INSERT B (BAG_OF_SET D')) B` 436 by simp[G_ax,BAG_IN_BAG_INSERT] >> 437 `G (BAG_INSERT (A Imp B) (BAG_OF_SET D')) B` 438 by metis_tac[G_limp] >> 439 `G ((BAG_OF_SET D) ��� (BAG_OF_SET D')) B` 440 by metis_tac[G_cut] >> 441 `G (unibag (BAG_OF_SET D ��� BAG_OF_SET D')) B` by metis_tac[G_unibag] >> 442 fs[unibag_UNION]) 443 >- (rename [`N (_ INSERT _) C`] >> 444 fs[BAG_OF_SET_UNION,BAG_OF_SET_INSERT] >> 445 qabbrev_tac `�� = ((BAG_OF_SET D) ��� (BAG_OF_SET D1) ��� (BAG_OF_SET D2))` >> 446 `FINITE_BAG (BAG_INSERT A ��)` 447 by (simp[Abbr`��`,FINITE_BAG_THM] >> 448 metis_tac[FINITE_BAG_OF_SET,N_FINITE,FINITE_INSERT]) >> 449 `G (BAG_INSERT A ��) C` 450 by (`G (BAG_MERGE {|A|} ��) C` 451 suffices_by metis_tac[BAG_MERGE_ELBAG_SUB_BAG_INSERT,G_lw] >> 452 simp[Abbr`��`] >> 453 irule G_lw >> 454 conj_tac >- fs[FINITE_BAG_MERGE,FINITE_BAG_THM] >> 455 qexists_tac `BAG_MERGE {|A|} (BAG_OF_SET D1)` >> 456 simp[] >> 457 fs[BAG_MERGE,BAG_INSERT,EMPTY_BAG, 458 BAG_OF_SET,BAG_UNION,SUB_BAG,BAG_INN,IN_DEF] >> 459 rw[] >> 460 fs[]) >> 461 `FINITE_BAG (BAG_INSERT B ��)` 462 by (simp[Abbr`��`,FINITE_BAG_THM] >> 463 metis_tac[FINITE_BAG_OF_SET,N_FINITE,FINITE_INSERT]) >> 464 `G (BAG_INSERT B ��) C` 465 by (`G (BAG_MERGE {|B|} ��) C` 466 suffices_by metis_tac[BAG_MERGE_ELBAG_SUB_BAG_INSERT,G_lw] >> 467 simp[Abbr`��`] >> 468 irule G_lw >> 469 conj_tac >- fs[FINITE_BAG_MERGE,FINITE_BAG_THM] >> 470 qexists_tac `BAG_MERGE {|B|} (BAG_OF_SET D2)` >> 471 simp[] >> 472 fs[BAG_MERGE,BAG_INSERT,EMPTY_BAG, 473 BAG_OF_SET,BAG_UNION,SUB_BAG,BAG_INN,IN_DEF] >> 474 rw[] >> 475 fs[]) >> 476 `G �� (A Or B)` 477 by (simp[Abbr`��`] >> 478 irule G_lw_BAG_UNION >> 479 conj_tac >- metis_tac[FINITE_INSERT,N_FINITE,FINITE_BAG_OF_SET] >> 480 irule G_lw_BAG_UNION >> 481 conj_tac >- metis_tac[FINITE_INSERT,N_FINITE,FINITE_BAG_OF_SET] >> 482 metis_tac[]) >> 483 `G (BAG_INSERT (A Or B) ��) C` by metis_tac[G_lor] >> 484 `G ((BAG_OF_SET D) ��� ��) C` by metis_tac[G_cut] >> 485 `G (unibag (BAG_OF_SET D ��� ��)) C` by metis_tac[G_unibag] >> 486 `(unibag (BAG_OF_SET D ��� ��)) 487 = BAG_MERGE (BAG_MERGE (BAG_OF_SET D) (BAG_OF_SET D1)) (BAG_OF_SET D2)` 488 suffices_by metis_tac[] >> 489 rw[Abbr`��`,unibag_UNION,BAG_MERGE,FUN_EQ_THM]) 490 >- (`G {|Bot|} A` by metis_tac[G_bot,BAG_IN_BAG_INSERT,FINITE_BAG] >> 491 metis_tac[G_cut,BAG_UNION_EMPTY]) 492QED 493 494Theorem G_N: 495 ����� A. G �� A ==> N (SET_OF_BAG ��) A 496Proof 497 Induct_on `G` >> rw[N_rules] 498 >- (`���b. �� = BAG_INSERT A b` by metis_tac[BAG_DECOMPOSE] >> 499 fs[] >> 500 simp[SET_OF_BAG_INSERT, Once INSERT_SING_UNION] >> 501 `N {A} A` by metis_tac[N_ax] >> 502 simp[UNION_COMM] >> 503 irule N_lw_SUBSET >> 504 conj_tac >- metis_tac[FINITE_UNION,FINITE_SET_OF_BAG,FINITE_DEF] >> 505 metis_tac[SUBSET_UNION]) 506 >- (`���b. �� = BAG_INSERT Bot b` by metis_tac[BAG_DECOMPOSE] >> 507 fs[] >> 508 simp[SET_OF_BAG_INSERT, Once INSERT_SING_UNION] >> 509 `N {Bot} Bot` by metis_tac[N_ax] >> 510 `N {Bot} A` by metis_tac[N_bot] >> 511 irule N_lw_SUBSET >> 512 conj_tac >- metis_tac[FINITE_UNION,FINITE_SET_OF_BAG,FINITE_DEF] >> 513 metis_tac[SUBSET_UNION]) 514 >- fs[SET_OF_BAG,BAG_UNION,BAG_INSERT] 515 >- (rename [`N _ C`] >> 516 fs[SET_OF_BAG_INSERT] >> 517 `N {A And B} (A And B)` by metis_tac[N_ax] >> 518 `N {A And B} A` by metis_tac[N_andel] >> 519 `N ((A INSERT (SET_OF_BAG ��)) DELETE A) (A Imp C)` 520 by metis_tac[N_impi_DELETE] >> 521 fs[DELETE_DEF] >> 522 `N (((SET_OF_BAG ��) DIFF {A}) ��� {A And B}) C` by metis_tac[N_impe] >> 523 `N ((A And B) INSERT ((SET_OF_BAG ��) DIFF {A})) C` 524 by metis_tac[UNION_COMM,INSERT_SING_UNION] >> 525 irule N_lw_SUBSET >> 526 conj_tac >- metis_tac[N_FINITE,FINITE_INSERT] >> 527 qexists_tac `(A And B) INSERT SET_OF_BAG �� DIFF {A}` >> 528 rw[SUBSET_DEF]) 529 >- (rename [`N _ C`] >> 530 `N {A And B} (A And B)` by metis_tac[N_ax] >> 531 `N {A And B} B` by metis_tac[N_ander] >> 532 qabbrev_tac `��'= SET_OF_BAG (BAG_INSERT B ��)` >> 533 `N (B INSERT ��') C` by metis_tac[N_lw] >> 534 `N (��' DELETE B) (B Imp C)` 535 by (Cases_on `B ��� ��'` 536 >- (`�����0. (��' = B INSERT ��0) ��� B NOTIN ��0` 537 by metis_tac[DECOMPOSITION] >> 538 fs[] >> 539 `(B INSERT ��0) DELETE B = ��0` 540 by (dsimp[EXTENSION] >> 541 metis_tac[]) >> 542 simp[N_impi]) 543 >- (simp[DELETE_NON_ELEMENT_RWT,N_impi])) >> 544 `N ((��' DELETE B) ��� {A And B}) C` by metis_tac[N_impe] >> 545 `N ((A And B) INSERT (��' DELETE B)) C` 546 by metis_tac[UNION_COMM,INSERT_SING_UNION] >> 547 fs[Abbr`��'`,SET_OF_BAG_INSERT] >> 548 irule N_lw_SUBSET >> 549 conj_tac >- metis_tac[N_FINITE,FINITE_INSERT] >> 550 fs[DELETE_DEF] >> 551 qexists_tac `(A And B) INSERT SET_OF_BAG �� DIFF {B}` >> 552 rw[SUBSET_DEF]) 553 >- (rename [`N _ (A And B)`] >> metis_tac[N_andi,UNION_IDEMPOT]) 554 >- (rename [`N _ C`] >> 555 qabbrev_tac `�� = (A Or B) INSERT (SET_OF_BAG ��)` >> 556 qabbrev_tac `��' = A INSERT (SET_OF_BAG ��)` >> 557 qabbrev_tac `��'' = B INSERT (SET_OF_BAG ��)` >> 558 fs[SET_OF_BAG_INSERT] >> 559 `FINITE_BAG ��` by metis_tac[G_FINITE,FINITE_BAG_THM] >> 560 `N (A INSERT ��) C` 561 by (irule N_lw_SUBSET >> 562 simp[Abbr`��`] >> 563 qexists_tac `��'` >> 564 simp[Abbr`��'`,SUBSET_INSERT_RIGHT]) >> 565 `N (B INSERT ��) C` 566 by (irule N_lw_SUBSET >> 567 simp[Abbr`��`] >> 568 qexists_tac `��''` >> 569 simp[Abbr`��''`,SUBSET_INSERT_RIGHT]) >> 570 `N {(A Or B)} (A Or B)` by metis_tac[N_ax] >> 571 `FINITE ({A Or B} ��� (SET_OF_BAG ��))` 572 by (`FINITE (SET_OF_BAG ��)` 573 by metis_tac[FINITE_SET_OF_BAG] >> 574 metis_tac[FINITE_UNION,FINITE_DEF]) >> 575 `N ({A Or B} ��� (SET_OF_BAG ��)) (A Or B)` 576 by metis_tac[SUBSET_UNION,N_lw_SUBSET] >> 577 `N �� (A Or B)` 578 by (simp[Abbr`��`,Abbr`��'`,Abbr`��''`] >> 579 irule N_lw_SUBSET >> 580 rw[] >> 581 qexists_tac `{A Or B}` >> 582 simp[]) >> 583 `N (�� ��� �� ��� ��) C` by metis_tac[N_ore] >> 584 metis_tac[UNION_IDEMPOT]) 585 >- (rename [`N _ C`] >> 586 fs[SET_OF_BAG_INSERT] >> 587 `FINITE_BAG ��` by metis_tac[G_FINITE,FINITE_BAG_THM] >> 588 `FINITE (SET_OF_BAG ��)` by metis_tac[FINITE_SET_OF_BAG] >> 589 `N {A Imp B} (A Imp B)` by metis_tac[N_ax] >> 590 `N ((A Imp B) INSERT (SET_OF_BAG ��)) B` 591 by metis_tac[INSERT_SING_UNION,N_impe] >> 592 irule N_lw_SUBSET >> 593 rw[] >> 594 `N (B INSERT (SET_OF_BAG ��)) C` 595 by metis_tac[N_lw_SUBSET,FINITE_INSERT] >> 596 `N (SET_OF_BAG ��) (B Imp C)` by metis_tac[N_impi] >> 597 `N ((SET_OF_BAG ��) ��� ((A Imp B) INSERT SET_OF_BAG ��)) C` 598 by metis_tac[N_impe] >> 599 `N ((A Imp B) INSERT SET_OF_BAG ��) C` 600 by metis_tac[UNION_COMM,UNION_ASSOC,UNION_IDEMPOT,INSERT_SING_UNION]>> 601 qexists_tac `(A Imp B) INSERT (SET_OF_BAG ��)` >> 602 rw[] >> 603 fs[SUBSET_INSERT_RIGHT]) 604 >- (rename [`N _ (A Imp B)`] >> 605 fs[SET_OF_BAG_INSERT] >> 606 metis_tac[N_impi]) 607 >- (rename [`G (BAG_INSERT A ��) B`] >> 608 fs[SET_OF_BAG_INSERT] >> 609 `N ((A INSERT SET_OF_BAG ��) DELETE A) (A Imp B)` 610 by metis_tac[N_impi_DELETE] >> 611 fs[DELETE_DEF] >> 612 `N ((SET_OF_BAG �� DIFF {A}) ��� (SET_OF_BAG ��)) B` by metis_tac[N_impe] >> 613 irule N_lw_SUBSET >> 614 reverse(rw[]) 615 >- (qexists_tac `SET_OF_BAG �� DIFF {A} ��� SET_OF_BAG ��` >> 616 rw[] 617 >- (irule SUBSET_TRANS >> 618 qexists_tac `(SET_OF_BAG ��)` >> 619 fs[SET_OF_BAG_INSERT,SET_OF_BAG_UNION]) 620 >- fs[SET_OF_BAG_UNION]) 621 >> metis_tac[G_FINITE,FINITE_BAG_THM]) 622QED 623 624Theorem G_iff_N: 625����� A. G �� A <=> N (SET_OF_BAG ��) A 626Proof 627 rw[G_N] >> 628 EQ_TAC >- rw[G_N] >> 629 rw[] >> 630 `G (unibag ��) A` by metis_tac[N_G] >> 631 metis_tac[G_unibag] 632QED 633 634val _ = export_theory() 635