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
|
open bossLib HolKernel boolLib listTheory rich_listTheory optionTheory combinTheory arithmeticTheory pairTheory;
open ottTheory ottLib caml_typedefTheory;
open utilTheory basicTheory shiftTheory environmentTheory validTheory;
open weakenTheory shiftTheory remv_tyvarTheory type_substsTheory;
val _ = Parse.hide "S";
val _ = new_theory "store";
val store_typing_thm = Q.store_thm ("store_typing_thm",
`!E st E'. JTstore E st E' ==> !l. (MEM (name_l l) (MAP domEB E') =
?v. (list_assoc l st = SOME v) /\ is_value_of_expr v)`,
RULE_INDUCT_TAC JTstore_ind [list_assoc_def, domEB_def] [] THEN METIS_TAC []);
val empty_type_sub_inst_any_thm = Q.prove (
`!E t src_t. JTinst_any E t src_t ==> !S'. JTinst_any E t (substs_typevar_typexpr S' src_t)`,
RULE_INDUCT_TAC JTinst_any_ind [JTinst_any_fun, substs_typevar_typexpr_def]
[([``"JTinst_any_tuple"``, ``"JTinst_any_ctor"``],
SRW_TAC [] [] THEN Q.EXISTS_TAC `MAP (\x. (FST x, substs_typevar_typexpr S' (SND x))) t_t'_list` THEN
SRW_TAC [] [MAP_MAP, ETA_THM, EVERY_MAP] THEN FULL_SIMP_TAC list_ss [EVERY_MEM])]);
val empty_type_sub_pat_thm = Q.prove (
`!S E pm t E'. JTpat S E pm t E' ==> (S = []) ==> !S'. JTpat S' E pm t E'`,
RULE_INDUCT_TAC JTpat_ind [JTpat_fun]
[([``"JTpat_typed"``],
SRW_TAC [] [substs_tv_empty_thm] THEN METIS_TAC [empty_type_sub_inst_any_thm]),
([``"JTpat_construct"``, ``"JTpat_tuple"``, ``"JTpat_record"``],
SRW_TAC [] [EVERY_MEM] THEN METIS_TAC []),
([``"JTpat_construct_any"``, ``"JTpat_cons"``, ``"JTpat_or"``],
METIS_TAC [])]);
val empty_type_sub_thm = Q.prove (
`(!S E e t. JTe S E e t ==> (S = []) ==> !S'. JTe S' E e t) /\
(!S E p t t'. JTpat_matching S E p t t' ==> (S = []) ==> !S'. JTpat_matching S' E p t t') /\
(!S E lb E'. JTlet_binding S E lb E' ==> (S = []) ==> !S'. JTlet_binding S' E lb E') /\
(!S E lrbs E'. JTletrec_binding S E lrbs E' ==> (S = []) ==> !S'. JTletrec_binding S' E lrbs E')`,
RULE_INDUCT_TAC JTe_sind [JTe_fun, shiftTsig_def]
[([``"JTe_typed"``],
SRW_TAC [] [substs_tv_empty_thm] THEN METIS_TAC [empty_type_sub_inst_any_thm]),
([``"JTe_tuple"``, ``"JTe_construct"``, ``"JTe_record_constr"``, ``"JTe_record_with"``,
``"JTletrec_binding_equal_function"``],
SRW_TAC [] [EVERY_MEM] THEN METIS_TAC []),
([``"JTpat_matching_pm"``],
SRW_TAC [] [EVERY_MEM] THEN METIS_TAC [empty_type_sub_pat_thm]),
([``"JTlet_binding_poly"``],
METIS_TAC [empty_type_sub_pat_thm])]
THEN
METIS_TAC []);
val store_dom_thm = Q.prove (
`!E st E'. JTstore E st E' ==> (MAP (\x. name_l (FST x)) st = MAP domEB E')`,
RULE_INDUCT_TAC JTstore_ind [domEB_def]
[]);
local
val lem1 = Q.prove (
`!E1 st E2. JTstore E1 st E2 ==> !l v. (list_assoc l st = SOME v) ==>
?t. (!S. JTe S E1 v t) /\ (lookup E2 (name_l l) = SOME (EB_l l t))`,
RULE_INDUCT_TAC JTstore_ind [list_assoc_def] [] THEN
SRW_TAC [] [COND_EXPAND_EQ, lookup_def, shiftEB_add_thm, domEB_def] THEN METIS_TAC [empty_type_sub_thm]);
val lem2 = Q.prove (
`!E l. type_env E ==> ~MEM (name_l l) (MAP domEB E)`,
Induct THEN SRW_TAC [] [type_env_def] THEN Cases_on `h` THEN
FULL_SIMP_TAC (srw_ss()) [type_env_def, domEB_def]);
val lem3 = Q.prove (
`!E st E'. JTstore E st E' ==> (!v. ~(list_assoc l st = SOME v)) ==> ~MEM (name_l l) (MAP domEB E')`,
RULE_INDUCT_TAC JTstore_ind [list_assoc_def, domEB_def]
[] THEN SRW_TAC [] []);
val lem4 = (SIMP_RULE list_ss [] o GEN_ALL o
Q.SPECL [`[EB]`, `E`, `[]`, `v`, `t`, `[]`] o GEN_ALL o
SIMP_RULE list_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM])
(hd (CONJUNCTS weak_not_tv_thm));
val lem5 = SIMP_RULE list_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] (Q.prove (
`!E st E'. JTstore E st E' ==> !l t. Eok (EB_l l t::E) ==> JTstore (EB_l l t::E) st E'`,
RULE_INDUCT_TAC JTstore_ind [JTstore_fun]
[([``"JTstore_map"``],
SRW_TAC [] [] THEN MATCH_MP_TAC lem4 THEN
FULL_SIMP_TAC (srw_ss()) [domEB_def, MEM_MAP, Eok_def])]));
val lem6 = SIMP_RULE list_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] (Q.prove (
`!E st E'. JTstore E st E' ==> !st1 st2 l v v' t. (st = st1++[(l, v')]++st2) /\ is_value_of_expr v /\
JTe [] E v t /\ (lookup E' (name_l l) = SOME (EB_l l t)) /\ ~MEM l (MAP FST st1) ==>
JTstore E (st1++[(l, v)]++st2) E'`,
RULE_INDUCT_TAC JTstore_sind []
[] THEN
SRW_TAC [] [] THEN FULL_SIMP_TAC (srw_ss()) [lookup_def, domEB_def, COND_EXPAND_EQ, shiftEB_add_thm] THEN
SRW_TAC [] [] THEN Cases_on `st1` THEN FULL_SIMP_TAC list_ss [] THEN SRW_TAC [] [JTstore_fun] THEN
FULL_SIMP_TAC list_ss [FST]));
val lem7 = Q.prove (
`!E' E1 l t. (lookup (E' ++ E1) (name_l l) = SOME (EB_l l t)) /\ type_env E1 ==>
(lookup E' (name_l l) = SOME (EB_l l t))`,
SRW_TAC [] [lookup_append_thm] THEN Cases_on `lookup E' (name_l l)` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
IMP_RES_TAC lookup_dom_thm THEN METIS_TAC [lem2]);
val lem8 = Q.prove (
`!st'. DISJOINT (remove_vn_tv (MAP (\x. name_l (FST x)) st')) (remove_vn_tv [name_l l]) ==>
~MEM l (MAP FST st')`,
SRW_TAC [] [DISJOINT_MEM, EVERY_MEM] THEN POP_ASSUM (ASSUME_TAC o Q.SPEC `name_l l`) THEN
FULL_SIMP_TAC (srw_ss()) [remove_vn_tv_thm, MEM_MAP]);
in
val store_in_thm = Q.store_thm ("store_in_thm",
`!st L st'. JRstore st L st' ==> !E' E1 E2. type_env E1 /\ JTstore (E'++E1) st E' ==>
!S. JTLin S (E'++E1) L`,
RULE_INDUCT_TAC JRstore_ind [JTLin_cases]
[([``"JRstore_lookup"``],
SRW_TAC [] [lookup_append_thm] THEN METIS_TAC [lem1, option_case_def]),
([``"JRstore_alloc"``],
SRW_TAC [] [lem2] THEN METIS_TAC [lem3])]);
val store_out_thm = Q.store_thm ("store_out_thm",
`!st L st'. JRstore st L st' ==> !E' E'' E1 E2 E7 S. JTstore (E'++E1) st E' /\ JTLout S (E'++E1) L E7 /\
type_env E1 ==>
JTstore (E7++E'++E1) st' (E7++E')`,
RULE_INDUCT_TAC JRstore_ind [JTLout_cases]
[([``"JRstore_alloc"``],
SRW_TAC [] [JTstore_fun] THEN SRW_TAC [] [value_remv_tyvar_thm] THENL
[MATCH_MP_TAC lem5 THEN SRW_TAC [] [Eok_def] THEN METIS_TAC [ok_thm, lem2, lem3],
MATCH_MP_TAC lem4 THEN SRW_TAC [] [Eok_def, domEB_def, remv_tyvar_fv_thm] THEN
METIS_TAC [remv_tyvar_thm, MEM_MAP, name_distinct, ok_thm, lem2, lem3]]),
([``"JRstore_assign"``],
SRW_TAC [] [] THEN SRW_TAC [] [] THEN MATCH_MP_TAC lem6 THEN MAP_EVERY Q.EXISTS_TAC [`expr`, `t`] THEN
SRW_TAC [] [value_remv_tyvar_thm, lookup_append_thm] THENL
[METIS_TAC [remv_tyvar_thm],
METIS_TAC [lem7],
IMP_RES_TAC store_dom_thm THEN
`ALL_DISTINCT (remove_vn_tv (MAP domEB (E'++E1)))`
by METIS_TAC [Eok_dom_thm, ok_thm, ok_ok_thm] THEN
FULL_SIMP_TAC list_ss [ALL_DISTINCT_APPEND, remove_vn_tv_APPEND] THEN
`ALL_DISTINCT (remove_vn_tv (MAP (\x. name_l (FST x)) st' ++ [name_l l] ++
MAP (\x. name_l (FST x)) st))`
by METIS_TAC [] THEN
FULL_SIMP_TAC list_ss [ALL_DISTINCT_APPEND, remove_vn_tv_APPEND] THEN
METIS_TAC [lem8]])]);
end;
local
val lem1 = Q.prove (
`!E. type_env E ==> ~MEM EB_tv E`,
Induct THEN SRW_TAC [] [type_env_def] THEN Cases_on `h` THEN
FULL_SIMP_TAC (srw_ss ()) [type_env_def]);
val lem2 = Q.prove (
`!E. type_env E /\ MEM n (MAP domEB E) ==> ~?vn. n = name_vn vn`,
Induct THEN SRW_TAC [] [type_env_def] THEN Cases_on `h` THEN
FULL_SIMP_TAC (srw_ss ()) [type_env_def, domEB_def]);
in
val type_env_store_weak_thm = Q.store_thm ("type_env_store_weak_thm",
`!E st E'. JTstore E st E' ==> !E1 E2 E3. (E = E1++E3) /\ type_env E2 /\ Eok (E1++E2++E3) ==>
JTstore (E1++E2++E3) st E'`,
RULE_INDUCT_TAC JTstore_ind [JTstore_fun]
[([``"JTstore_map"``],
SRW_TAC [] [] THEN
MATCH_MP_TAC ((SIMP_RULE list_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] o hd o CONJUNCTS)
weak_not_tv_thm) THEN
SRW_TAC [] [lem1] THEN METIS_TAC [lem2, MEM_MAP])]);
end;
val _ = export_theory ();
|
