Skip to content

Commit cd4cc8f

Browse files
maggesimaggesi
committed
Initial import.
1 parent 9324157 commit cd4cc8f

13 files changed

+4495
-0
lines changed

‎calculus.ml

+1,028
Large diffs are not rendered by default.

‎conjlist.ml

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

0 commit comments

Comments
 (0)