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