-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathconjlist.ml
190 lines (173 loc) · 8.25 KB
/
conjlist.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
(* ========================================================================= *)
(* Iterated conjunction of formulae. *)
(* *)
(* (c) Copyright, Marco Maggesi, Cosimo Perini Brogi 2020-2022. *)
(* (c) Copyright, Antonella Bilotta, Marco Maggesi, *)
(* Cosimo Perini Brogi, Leonardo Quartini 2024. *)
(* ========================================================================= *)
let CONJLIST = new_recursive_definition list_RECURSION
`CONJLIST [] = True /\
(!p X. CONJLIST (CONS p X) = if X = [] then p else p && CONJLIST X)`;;
let CONJLIST_IMP_MEM = prove
(`!p X. MEM p X ==> [S . H |~ (CONJLIST X --> p)]`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; CONJLIST] THEN
STRIP_TAC THENL
[POP_ASSUM (SUBST_ALL_TAC o GSYM) THEN
COND_CASES_TAC THEN REWRITE_TAC[MLK_imp_refl_th; MLK_and_left_th];
COND_CASES_TAC THENL [ASM_MESON_TAC[MEM]; ALL_TAC] THEN
MATCH_MP_TAC MLK_imp_trans THEN EXISTS_TAC `CONJLIST t` THEN CONJ_TAC THENL
[MATCH_ACCEPT_TAC MLK_and_right_th; ASM_SIMP_TAC[]]]);;
let CONJLIST_MONO = prove
(`!X Y. (!p. MEM p Y ==> MEM p X) ==> [S . H |~ (CONJLIST X --> CONJLIST Y)]`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; CONJLIST] THENL
[MESON_TAC[MLK_add_assum; MLK_truth_th]; ALL_TAC] THEN
COND_CASES_TAC THENL
[POP_ASSUM SUBST_VAR_TAC THEN
REWRITE_TAC[MEM] THEN MESON_TAC[CONJLIST_IMP_MEM];
ALL_TAC] THEN
DISCH_TAC THEN MATCH_MP_TAC MLK_and_intro THEN CONJ_TAC THENL
[ASM_MESON_TAC[CONJLIST_IMP_MEM];
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[]]);;
let CONJLIST_CONS = prove
(`!p X. [S . H |~ (CONJLIST (CONS p X) <-> p && CONJLIST X)]`,
REPEAT GEN_TAC THEN REWRITE_TAC[CONJLIST] THEN COND_CASES_TAC THEN
REWRITE_TAC[MLK_iff_refl_th] THEN POP_ASSUM SUBST1_TAC THEN
REWRITE_TAC[CONJLIST] THEN ONCE_REWRITE_TAC[MLK_iff_sym] THEN
MATCH_ACCEPT_TAC MLK_and_rigth_true_th);;
let CONJLIST_IMP = prove
(`!S H h t. [S . H |~ CONJLIST (CONS h t) --> p] <=>
[S . H |~ h && CONJLIST t --> p]`,
REPEAT GEN_TAC THEN EQ_TAC THEN INTRO_TAC "hp" THENL
[TRANS_TAC MLK_imp_trans `CONJLIST (CONS h t)` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MLK_iff_imp2 THEN MATCH_ACCEPT_TAC CONJLIST_CONS;
TRANS_TAC MLK_imp_trans `h && CONJLIST t` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MLK_iff_imp1 THEN MATCH_ACCEPT_TAC CONJLIST_CONS]);;
let HEAD_TAIL_IMP_CONJLIST = prove
(`!p h t. [S . H |~ (p --> h)] /\ [S . H |~ (p --> CONJLIST t)]
==> [S . H |~ (p --> CONJLIST (CONS h t))]`,
INTRO_TAC "!p h t; ph pt" THEN REWRITE_TAC[CONJLIST] THEN
COND_CASES_TAC THENL [ASM_REWRITE_TAC[]; ASM_SIMP_TAC[MLK_and_intro]]);;
let IMP_CONJLIST = prove
(`!p X. [S . H |~ p --> CONJLIST X] <=>
(!q. MEM q X ==> [S . H |~ (p --> q)])`,
GEN_TAC THEN SUBGOAL_THEN
`(!X q. [S . H |~ p --> CONJLIST X] /\ MEM q X
==> [S . H |~ p --> q]) /\
(!X. (!q. MEM q X ==> [S . H |~ p --> q])
==> [S . H |~ p --> CONJLIST X])`
(fun th -> MESON_TAC[th]) THEN
CONJ_TAC THENL
[REPEAT STRIP_TAC THEN MATCH_MP_TAC MLK_imp_trans THEN
EXISTS_TAC `CONJLIST X` THEN ASM_SIMP_TAC[CONJLIST_IMP_MEM];
ALL_TAC] THEN
LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THENL
[REWRITE_TAC[CONJLIST; MLK_imp_clauses]; ALL_TAC] THEN
DISCH_TAC THEN MATCH_MP_TAC HEAD_TAIL_IMP_CONJLIST THEN
ASM_SIMP_TAC[]);;
let CONJLIST_IMP_SUBLIST = prove
(`!X Y. Y SUBLIST X ==> [S . H |~ CONJLIST X --> CONJLIST Y]`,
REWRITE_TAC[SUBLIST; IMP_CONJLIST] THEN MESON_TAC[CONJLIST_IMP_MEM]);;
let CONJLIST_IMP_HEAD = prove
(`!p X. [S . H |~ CONJLIST (CONS p X) --> p]`,
REPEAT GEN_TAC THEN MATCH_MP_TAC CONJLIST_IMP_MEM THEN REWRITE_TAC[MEM]);;
let CONJLIST_IMP_TAIL = prove
(`!p X. [S . H |~ CONJLIST (CONS p X) --> CONJLIST X]`,
MESON_TAC[CONJLIST_IMP_SUBLIST; TAIL_SUBLIST]);;
let CONJLIST_IMP_CONJLIST = prove
(`!l m.
(!p. MEM p m ==> ?q. MEM q l /\ [S . H |~ (q --> p)])
==> [S . H |~ (CONJLIST l --> CONJLIST m)]`,
GEN_TAC THEN LIST_INDUCT_TAC THENL
[REWRITE_TAC[CONJLIST; MLK_imp_clauses]; ALL_TAC] THEN
INTRO_TAC "hp" THEN
MATCH_MP_TAC MLK_imp_trans THEN EXISTS_TAC `h && CONJLIST t` THEN
CONJ_TAC THENL
[MATCH_MP_TAC MLK_and_intro THEN
CONJ_TAC THENL
[HYP_TAC "hp: +" (SPEC `h:form`) THEN
REWRITE_TAC[MEM] THEN MESON_TAC[CONJLIST_IMP_MEM; MLK_imp_trans];
FIRST_X_ASSUM MATCH_MP_TAC THEN
INTRO_TAC "!p; p" THEN FIRST_X_ASSUM (MP_TAC o SPEC `p:form`) THEN
ASM_REWRITE_TAC[MEM]];
ALL_TAC] THEN
MESON_TAC[CONJLIST_CONS; MLK_iff_imp2]);;
let CONJLIST_APPEND = prove
(`!l m. [S . H |~ (CONJLIST (APPEND l m) <-> CONJLIST l && CONJLIST m)]`,
FIX_TAC "m" THEN LIST_INDUCT_TAC THEN REWRITE_TAC[APPEND] THENL
[REWRITE_TAC[CONJLIST] THEN ONCE_REWRITE_TAC[MLK_iff_sym] THEN
MATCH_ACCEPT_TAC MLK_and_left_true_th;
ALL_TAC] THEN
MATCH_MP_TAC MLK_iff_trans THEN
EXISTS_TAC `h && CONJLIST (APPEND t m)` THEN REWRITE_TAC[CONJLIST_CONS] THEN
MATCH_MP_TAC MLK_iff_trans THEN
EXISTS_TAC `h && (CONJLIST t && CONJLIST m)` THEN CONJ_TAC THENL
[MATCH_MP_TAC MLK_and_subst_th THEN ASM_REWRITE_TAC[MLK_iff_refl_th];
ALL_TAC] THEN
MATCH_MP_TAC MLK_iff_trans THEN
EXISTS_TAC `(h && CONJLIST t) && CONJLIST m` THEN CONJ_TAC THENL
[MESON_TAC[MLK_and_assoc_th; MLK_iff_sym]; ALL_TAC] THEN
MATCH_MP_TAC MLK_and_subst_th THEN REWRITE_TAC[MLK_iff_refl_th] THEN
ONCE_REWRITE_TAC[MLK_iff_sym] THEN MATCH_ACCEPT_TAC CONJLIST_CONS);;
let FALSE_NOT_CONJLIST = prove
(`!X. MEM False X ==> [S . H |~ (Not (CONJLIST X))]`,
INTRO_TAC "!X; X" THEN REWRITE_TAC[MLK_not_def] THEN
MATCH_MP_TAC CONJLIST_IMP_MEM THEN POP_ASSUM MATCH_ACCEPT_TAC);;
let CONJLIST_MAP_BOX = prove
(`!l. [S . H |~ (CONJLIST (MAP (Box) l) <-> Box (CONJLIST l))]`,
LIST_INDUCT_TAC THENL
[REWRITE_TAC[CONJLIST; MAP; MLK_iff_refl_th] THEN
MATCH_MP_TAC MLK_imp_antisym THEN
SIMP_TAC[MLK_add_assum; MLK_truth_th; MLK_necessitation];
ALL_TAC] THEN
REWRITE_TAC[MAP] THEN MATCH_MP_TAC MLK_iff_trans THEN
EXISTS_TAC `Box h && CONJLIST (MAP (Box) t)` THEN CONJ_TAC THENL
[MATCH_ACCEPT_TAC CONJLIST_CONS; ALL_TAC] THEN MATCH_MP_TAC MLK_iff_trans THEN
EXISTS_TAC `Box h && Box (CONJLIST t)` THEN CONJ_TAC THENL
[MATCH_MP_TAC MLK_imp_antisym THEN CONJ_TAC THEN
MATCH_MP_TAC MLK_and_intro THEN
ASM_MESON_TAC[MLK_and_left_th; MLK_and_right_th; MLK_iff_imp1;
MLK_iff_imp2; MLK_imp_trans];
ALL_TAC] THEN
MATCH_MP_TAC MLK_iff_trans THEN EXISTS_TAC `Box (h && CONJLIST t)` THEN
CONJ_TAC THENL
[MESON_TAC[MLK_box_and_th; MLK_box_and_inv_th; MLK_imp_antisym]; ALL_TAC] THEN
MATCH_MP_TAC MLK_box_iff THEN MATCH_MP_TAC MLK_necessitation THEN
ONCE_REWRITE_TAC[MLK_iff_sym] THEN MATCH_ACCEPT_TAC CONJLIST_CONS);;
let MODPROVES_DEDUCTION_LEMMA_CONJLIST = prove
(`!S H K p. [S . H |~ CONJLIST K --> p] <=>
[S . H UNION set_of_list K |~ p]`,
FIX_TAC "S p" THEN
C SUBGOAL_THEN (fun th -> MESON_TAC[th])
`!K H. [S . H |~ CONJLIST K --> p] <=>
[S . H UNION set_of_list K |~ p]` THEN
LIST_INDUCT_TAC THENL
[REWRITE_TAC[CONJLIST; set_of_list; UNION_EMPTY; MLK_imp_clauses]; ALL_TAC] THEN
GEN_TAC THEN
REWRITE_TAC[set_of_list;
SET_RULE `H UNION h:form INSERT s = h INSERT (H UNION s)`] THEN
REWRITE_TAC[CONJLIST_IMP; GSYM MLK_imp_imp] THEN
ONCE_REWRITE_TAC[MODPROVES_DEDUCTION_LEMMA] THEN
ASM_REWRITE_TAC[SET_RULE
`h:form INSERT H UNION set_of_list t =
h INSERT (H UNION set_of_list t)`]);;
let MLK_BOX_CONJLIST = prove
(`!S X. [S . {} |~ Box (CONJLIST X) <-> CONJLIST (MAP (Box) X)]`,
REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [MLK_iff_sym] THEN
MATCH_ACCEPT_TAC CONJLIST_MAP_BOX);;
g `!S p X. [S . {} |~ CONJLIST X --> p]
==> [S . {} |~ CONJLIST (MAP (Box) X) --> Box p]`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (CLAIM_TAC "asd" `[S . {} |~ Box CONJLIST X --> Box p]`);;
e (MATCH_MP_TAC MLK_imp_box);;
e (ASM_REWRITE_TAC[]);;
e (MATCH_MP_TAC MLK_imp_trans);;
e (EXISTS_TAC `Box CONJLIST X`);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN
`[S . {} |~ CONJLIST (MAP (Box) X) <-> Box CONJLIST X]
==> [S . {} |~ CONJLIST (MAP (Box) X) --> Box CONJLIST X]`
(fun(th) -> MATCH_MP_TAC th));;
e (MESON_TAC[MLK_iff_def]);;
e (REWRITE_TAC[MLK_BOX_CONJLIST; MLK_iff_sym]);;
let MKL_CONJLIST_BOX_IMP_BOX = top_thm();;