Skip to content

Commit

Permalink
Change of approach for dealing with value restriction + inference com…
Browse files Browse the repository at this point in the history 
…pleteness

The weakening theorems needed to prove type soundness aren't true if you
check for multiple possible types on a non-value definition. For
example, in the following v has type int -> int

structure M :> sig val f : int -> int end =
struct
  fun f x = x
end;
val v = (fn y => y) M.f;

However, if you drop the signature (which is something has to happen in
the type soundness proof), then you get M.f : 'a -> 'a and since the
value restriction prevents v : 'a -> 'a, there are many choices for v :
int -> int, v : bool -> bool, etc.

So now I've added a flag to type_d (and type_ds, etc) to indicate
whether to do the check. So the semantics can do the check, and the
inferencer can be complete with respect to that, but the type soundness
proof can turn off the check (since if something types with the check on
it will still type with it off).
  • Loading branch information
@SOwens
SOwens committed Nov 12, 2014
1 parent 2078451 commit 578b471
Show file tree
Hide file tree
Showing 7 changed files with 143 additions and 236 deletions.
47 changes: 24 additions & 23 deletions metatheory/typeSoundScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1809,7 +1809,7 @@ decs_type_sound_invariant mn tdecs1 tdecs2 ctMap tenvS tenvT tenvM tenvC tenv st

val dec_type_soundness = Q.store_thm ("dec_type_soundness",
`!mn tenvT tenvM tenvC tenv d tenvT' tenvC' tenv' tenvS ck menv cenv env count st tdecs1 tdecs1' tdecs2 ctMap.
type_d mn tdecs1 tenvT tenvM tenvC tenv d tdecs1' tenvT' tenvC' tenv' ∧
type_d F mn tdecs1 tenvT tenvM tenvC tenv d tdecs1' tenvT' tenvC' tenv' ∧
decs_type_sound_invariant mn tdecs1 tdecs2 ctMap tenvS tenvT tenvM tenvC tenv st menv cenv env
⇒
dec_diverges (menv,cenv,env) (st,tdecs2) d ∨
Expand Down Expand Up @@ -2077,9 +2077,10 @@ val still_has_lists = Q.prove (
metis_tac [SND]);

val decs_type_soundness = Q.store_thm ("decs_type_soundness",
`!mn tdecs1 tenvT tenvM tenvC tenv ds tdecs1' tenvT' tenvC' tenv'.
type_ds mn tdecs1 tenvT tenvM tenvC tenv ds tdecs1' tenvT' tenvC' tenv' ⇒
`!uniq mn tdecs1 tenvT tenvM tenvC tenv ds tdecs1' tenvT' tenvC' tenv'.
type_ds uniq mn tdecs1 tenvT tenvM tenvC tenv ds tdecs1' tenvT' tenvC' tenv' ⇒
∀tenvS menv cenv env st tdecs2 ctMap count.
uniq = F ∧
decs_type_sound_invariant mn tdecs1 tdecs2 ctMap tenvS tenvT tenvM tenvC tenv st menv cenv env
⇒
decs_diverges mn (menv,cenv,env) (st,tdecs2) ds ∨
Expand Down Expand Up @@ -2240,8 +2241,8 @@ rw [Once type_v_cases, bind_tenv_def] >>
metis_tac []);

val type_ds_no_dup_types_helper = Q.prove (
`!mn mdecls tdecls edecls tenvT tenvM tenvC tenv ds mdecls' tdecls' edecls' tenvT' tenvC' tenv'.
type_ds mn (mdecls,tdecls,edecls) tenvT tenvM tenvC tenv ds (mdecls',tdecls',edecls') tenvT' tenvC' tenv'
`!uniq mn mdecls tdecls edecls tenvT tenvM tenvC tenv ds mdecls' tdecls' edecls' tenvT' tenvC' tenv'.
type_ds uniq mn (mdecls,tdecls,edecls) tenvT tenvM tenvC tenv ds (mdecls',tdecls',edecls') tenvT' tenvC' tenv'
⇒
DISJOINT tdecls tdecls' ∧
tdecls' =
Expand Down Expand Up @@ -2273,8 +2274,8 @@ val type_ds_no_dup_types_helper = Q.prove (
metis_tac []);

val type_ds_no_dup_types = Q.prove (
`!mn decls tenvT tenvM tenvC tenv ds decls' tenvT' tenvC' tenv'.
type_ds mn decls tenvT tenvM tenvC tenv ds decls' tenvT' tenvC' tenv'
`!uniq mn decls tenvT tenvM tenvC tenv ds decls' tenvT' tenvC' tenv'.
type_ds uniq mn decls tenvT tenvM tenvC tenv ds decls' tenvT' tenvC' tenv'
⇒
no_dup_types ds`,
induct_on `ds` >>
Expand Down Expand Up @@ -2326,7 +2327,7 @@ val type_ds_no_dup_types = Q.prove (
val top_type_soundness = Q.store_thm ("top_type_soundness",
`!decls1 tenvT tenvM tenvC tenv envM envC envE count store1 decls1' tenvT' tenvM' tenvC' tenv' top decls2.
type_sound_invariants NONE (decls1,tenvT,tenvM,tenvC,tenv,decls2,envM,envC,envE,store1) ∧
type_top decls1 tenvT tenvM tenvC tenv top decls1' tenvT' tenvM' tenvC' tenv' ∧
type_top F decls1 tenvT tenvM tenvC tenv top decls1' tenvT' tenvM' tenvC' tenv' ∧
¬top_diverges (envM, envC, envE) (store1,decls2, FST decls1) top ⇒
?r cenv2 store2 decls2'.
(r ≠ Rerr Rtype_error) ∧
Expand All @@ -2341,7 +2342,7 @@ val top_type_soundness = Q.store_thm ("top_type_soundness",
PairCases_on `decls1` >>
fs [weak_decls_other_mods_def, weak_decls_only_mods_def, mk_id_def] >>
metis_tac []) >>
`type_d NONE decls_no_sig tenvT tenvM_no_sig tenvC_no_sig tenv d decls1' tenvT'' cenv' tenv'`
`type_d F NONE decls_no_sig tenvT tenvM_no_sig tenvC_no_sig tenv d decls1' tenvT'' cenv' tenv'`
by metis_tac [weak_decls_refl,weak_decls_other_mods_refl, type_d_weakening, consistent_con_env_def] >>
`decs_type_sound_invariant NONE decls_no_sig decls2 ctMap tenvS tenvT tenvM_no_sig tenvC_no_sig tenv store1 envM envC envE`
by (rw [decs_type_sound_invariant_def] >>
Expand Down Expand Up @@ -2411,7 +2412,7 @@ val top_type_soundness = Q.store_thm ("top_type_soundness",
CCONTR_TAC >>
fs [decls_to_mods_def, decls_ok_def, mk_id_def, SUBSET_DEF, GSPECIFICATION] >>
metis_tac [NOT_SOME_NONE, SOME_11]) >>
`type_ds (SOME mn) decls_no_sig tenvT tenvM_no_sig tenvC_no_sig tenv ds decls' tenvT'' cenv' tenv''`
`type_ds F (SOME mn) decls_no_sig tenvT tenvM_no_sig tenvC_no_sig tenv ds decls' tenvT'' cenv' tenv''`
by metis_tac [type_ds_weakening, consistent_con_env_def] >>
`decs_type_sound_invariant (SOME mn) decls_no_sig decls2 ctMap tenvS tenvT tenvM_no_sig tenvC_no_sig tenv store1 envM envC envE`
by (rw [decs_type_sound_invariant_def] >>
Expand Down Expand Up @@ -2581,7 +2582,7 @@ val FST_union_decls = Q.prove (
val prog_type_soundness = Q.store_thm ("prog_type_soundness",
`!decls1 tenvT tenvM tenvC tenv envM envC envE count store1 decls1' tenvT' tenvM' tenvC' tenv' prog decls2.
type_sound_invariants (NONE:('a,v) result option) (decls1,tenvT,tenvM,tenvC,tenv,decls2,envM,envC,envE,store1) ∧
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv' ∧
type_prog F decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv' ∧
¬prog_diverges (envM, envC, envE) (store1,decls2, FST decls1) prog ⇒
?cenv2 store2 decls2'.
(?envM2 envE2.
Expand All @@ -2594,7 +2595,7 @@ val prog_type_soundness = Q.store_thm ("prog_type_soundness",
induct_on `prog` >>
rw [] >>
ONCE_REWRITE_TAC [evaluate_prog_cases] >>
qpat_assum `type_prog x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10` mp_tac >>
qpat_assum `type_prog x100 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10` mp_tac >>
simp_tac (srw_ss()) [Once type_prog_cases, EXISTS_OR_THM]
>- (rw [update_type_sound_inv_def, empty_decls_def] >>
PairCases_on `tenvC` >>
Expand Down Expand Up @@ -2673,8 +2674,8 @@ val prog_type_soundness = Q.store_thm ("prog_type_soundness",
rw [FST_union_decls]));

val type_no_dup_top_types_lem = Q.prove (
`!decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
`!uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
⇒
ALL_DISTINCT (prog_to_top_types prog) ∧
DISJOINT (FST (SND decls1)) (IMAGE (mk_id NONE) (set (prog_to_top_types prog)))`,
Expand Down Expand Up @@ -2718,8 +2719,8 @@ val type_no_dup_top_types_lem = Q.prove (
metis_tac []));

val type_no_dup_top_types_lem2 = Q.prove (
`!decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
`!uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
⇒
no_dup_top_types prog (x,IMAGE TypeId (FST (SND decls1)),y)`,
rw [no_dup_top_types_def]
Expand All @@ -2734,7 +2735,7 @@ val type_no_dup_top_types_lem2 = Q.prove (

val type_no_dup_top_types = Q.prove (
`!decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv' ∧
type_prog uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv' ∧
consistent_decls decls2 decls_no_sig ∧
weak_decls_only_mods decls_no_sig decls1
⇒
Expand All @@ -2756,8 +2757,8 @@ val type_no_dup_top_types = Q.prove (
metis_tac [])

val type_no_dup_mods_lem = Q.prove (
`!decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
`!uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
⇒
ALL_DISTINCT (prog_to_mods prog) ∧
DISJOINT (FST decls1) (set (prog_to_mods prog))`,
Expand All @@ -2777,17 +2778,17 @@ val type_no_dup_mods_lem = Q.prove (
metis_tac []));

val type_no_dup_mods = Q.prove (
`!decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
`!uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'.
type_prog uniq decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv'
⇒
no_dup_mods prog (x, y, FST decls1)`,
rw [no_dup_mods_def] >>
metis_tac [type_no_dup_mods_lem, DISJOINT_SYM]);

val whole_prog_type_soundness = Q.store_thm ("whole_prog_type_soundness",
`!decls1 tenvT tenvM tenvC tenv envM envC envE count store1 decls1' tenvT' tenvM' tenvC' tenv' prog decls2.
`! decls1 tenvT tenvM tenvC tenv envM envC envE count store1 decls1' tenvT' tenvM' tenvC' tenv' prog decls2.
type_sound_invariants (NONE:('a,v) result option) (decls1,tenvT,tenvM,tenvC,tenv,decls2,envM,envC,envE,store1) ∧
type_prog decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv' ∧
type_prog F decls1 tenvT tenvM tenvC tenv prog decls1' tenvT' tenvM' tenvC' tenv' ∧
¬prog_diverges (envM, envC, envE) (store1,decls2, FST decls1) prog ⇒
?cenv2 store2 decls2'.
(?envM2 envE2.
Expand Down
60 changes: 30 additions & 30 deletions metatheory/typeSysPropsScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2542,8 +2542,8 @@ val type_ctxts_freevars = Q.store_thm ("type_ctxts_freevars",
(* ---------- type_d ---------- *)

val type_d_tenv_ok = Q.store_thm ("type_d_tenv_ok",
`!tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' tenvM'' tenvC''.
type_d tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ∧
`!uniq tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' tenvM'' tenvC''.
type_d uniq tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ∧
(num_tvs tenv = 0)
⇒
tenv_ok (bind_var_list2 tenv' Empty)`,
Expand All @@ -2556,8 +2556,8 @@ val type_d_tenv_ok = Q.store_thm ("type_d_tenv_ok",

(*weakened*)
val type_d_tenvT_ok = Q.store_thm ("type_d_tenvT_ok",
`!tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' tenvM'' tenvC''.
type_d tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ∧
`!uniq tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' tenvM'' tenvC''.
type_d uniq tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ∧
tenvT_ok tenvT
⇒
flat_tenvT_ok tenvT'`,
Expand All @@ -2580,9 +2580,9 @@ val type_d_tenvT_ok = Q.store_thm ("type_d_tenvT_ok",
fs [EVERY_MEM]);

val type_d_ctMap_ok = Q.store_thm ("type_d_ctMap_ok",
`!tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' tenvM'' tenvC''.
`!uniq tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' tenvM'' tenvC''.
tenvT_ok tenvT ∧
type_d tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv'
type_d uniq tvs tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv'
⇒
ctMap_ok (flat_to_ctMap tenvC') ∧
ALL_DISTINCT (MAP FST (flat_to_ctMap_list tenvC'))`,
Expand Down Expand Up @@ -2612,8 +2612,8 @@ val type_d_ctMap_ok = Q.store_thm ("type_d_ctMap_ok",
metis_tac [check_freevars_type_name_subst]));

val ctMap_ok_pres = Q.store_thm ("ctMap_ok_pres",
`!mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ctMap.
type_d mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ∧
`!uniq mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ctMap.
type_d uniq mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv' ∧
tenvT_ok tenvT ∧
ctMap_ok ctMap
⇒
Expand All @@ -2626,8 +2626,8 @@ val ctMap_ok_pres = Q.store_thm ("ctMap_ok_pres",
rw []);

val type_d_mod = Q.store_thm ("type_d_mod",
`!mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv'.
type_d mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv'
`!uniq mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv'.
type_d uniq mn tdecs tenvT tenvM tenvC tenv d tdecs' tenvT' tenvC' tenv'
⇒
FST tdecs' = {} ∧
decls_to_mods tdecs' ⊆ { mn }`,
Expand All @@ -2641,7 +2641,7 @@ val type_d_mod = Q.store_thm ("type_d_mod",
fs [GSPECIFICATION]);

val type_d_ctMap_disjoint = Q.store_thm ("type_d_ctMap_disjoint",
`type_d mn tdecs1 tenvT tenvM tenvC tenv d tdecs1' tenvT' tenvC' tenv' ∧
`type_d uniq mn tdecs1 tenvT tenvM tenvC tenv d tdecs1' tenvT' tenvC' tenv' ∧
consistent_ctMap tdecs1 ctMap
⇒
DISJOINT (FDOM (flat_to_ctMap tenvC')) (FDOM ctMap) ∧
Expand All @@ -2667,8 +2667,8 @@ val type_d_ctMap_disjoint = Q.store_thm ("type_d_ctMap_disjoint",
(* ---------- type_ds ---------- *)

val type_ds_tenv_ok = Q.store_thm ("type_ds_tenv_ok",
`!tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv' ⇒
`!uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv' ⇒
(num_tvs tenv = 0) ⇒
tenv_ok (bind_var_list2 tenv' Empty)`,
ho_match_mp_tac type_ds_ind >>
Expand All @@ -2679,8 +2679,8 @@ val type_ds_tenv_ok = Q.store_thm ("type_ds_tenv_ok",
metis_tac [tenv_ok_bvl2]));

val type_ds_mod = Q.store_thm ("type_ds_mod",
`!mn tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds mn tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'
`!uniq mn tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds uniq mn tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'
⇒
FST tdecs' = {} ∧
decls_to_mods tdecs' ⊆ {mn}`,
Expand All @@ -2701,8 +2701,8 @@ val type_ds_mod = Q.store_thm ("type_ds_mod",
metis_tac []);

val type_ds_ctMap_ok = Q.store_thm ("type_ds_ctMap_ok",
`!tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'
`!uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'
⇒
tenvT_ok tenvT
⇒
Expand All @@ -2728,8 +2728,8 @@ val type_ds_ctMap_ok = Q.store_thm ("type_ds_ctMap_ok",
rw []));

val type_ds_tenvC_ok = Q.store_thm ("type_ds_tenvC_ok",
`!tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv' ⇒
`!uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv' ⇒
tenvT_ok tenvT ⇒
flat_tenvC_ok tenvC'`,
ho_match_mp_tac type_ds_strongind >>
Expand All @@ -2745,8 +2745,8 @@ val type_ds_tenvC_ok = Q.store_thm ("type_ds_tenvC_ok",
rw [tenvT_ok_def, FEVERY_ALL_FLOOKUP, flookup_fupdate_list]));

val type_ds_tenvT_ok = Q.store_thm ("type_ds_tenvT_ok",
`!tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv' ⇒
`!uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv'.
type_ds uniq tvs tdecs tenvT tenvM tenvC tenv ds tdecs' tenvT' tenvC' tenv' ⇒
tenvT_ok tenvT
⇒
flat_tenvT_ok tenvT'`,
Expand Down Expand Up @@ -3011,8 +3011,8 @@ val type_e_closed = prove(
metis_tac []);

val type_d_closed = prove(
``∀mno decls tenvT tmenv tcenv tenv d w x y z.
type_d mno decls tenvT tmenv tcenv tenv d w x y z ⇒
``∀uniq mno decls tenvT tmenv tcenv tenv d w x y z.
type_d uniq mno decls tenvT tmenv tcenv tenv d w x y z ⇒
FV_dec d ⊆ (IMAGE Short (tenv_names tenv) ∪ tmenv_dom tmenv)``,
ho_match_mp_tac type_d_ind >>
strip_tac >- (
Expand Down Expand Up @@ -3043,8 +3043,8 @@ val type_d_closed = prove(
simp[]);

val type_d_new_dec_vs = Q.prove (
`!mn decls tenvT tenvM tenvC tenv d decls' tenvT' tenvC' tenv'.
type_d mn decls tenvT tenvM tenvC tenv d decls' tenvT' tenvC' tenv'
`!uniq mn decls tenvT tenvM tenvC tenv d decls' tenvT' tenvC' tenv'.
type_d uniq mn decls tenvT tenvM tenvC tenv d decls' tenvT' tenvC' tenv'
⇒
set (new_dec_vs d) = set (MAP FST tenv')`,
rw [type_d_cases, new_dec_vs_def] >>
Expand All @@ -3055,7 +3055,7 @@ val type_d_new_dec_vs = Q.prove (
metis_tac [type_funs_dom]);

val type_ds_closed = prove(
``∀mn decls tenvT tmenv cenv tenv ds w x y z. type_ds mn decls tenvT tmenv cenv tenv ds w x y z ⇒
``∀uniq mn decls tenvT tmenv cenv tenv ds w x y z. type_ds uniq mn decls tenvT tmenv cenv tenv ds w x y z ⇒
!mn'. mn = SOME mn' ⇒
FV_decs ds ⊆ (IMAGE Short (tenv_names tenv) ∪ tmenv_dom tmenv)``,
ho_match_mp_tac type_ds_ind >>
Expand All @@ -3071,8 +3071,8 @@ val type_ds_closed = prove(
metis_tac [type_d_new_dec_vs,MEM_MAP]);

val type_top_closed = store_thm("type_top_closed",
``∀decls tenvT tmenv tcenv tenv top decls' tT' tm' tc' te'.
type_top decls tenvT tmenv tcenv tenv top decls' tT' tm' tc' te'
``∀uniq decls tenvT tmenv tcenv tenv top decls' tT' tm' tc' te'.
type_top uniq decls tenvT tmenv tcenv tenv top decls' tT' tm' tc' te'
⇒
FV_top top ⊆ (IMAGE Short (tenv_names tenv) ∪ tmenv_dom tmenv)``,
ho_match_mp_tac type_top_ind >>
Expand Down Expand Up @@ -3156,8 +3156,8 @@ val consistent_mod_env_dom = Q.prove (
metis_tac []);

val type_sound_inv_closed = Q.store_thm ("type_sound_inv_closed",
`∀top rs new_tenvM new_tenvC new_tenv new_decls new_tenvT decls' store.
type_top rs.tdecs rs.tenvT rs.tenvM rs.tenvC rs.tenv top new_decls new_tenvT new_tenvM new_tenvC new_tenv ∧
`∀uniq top rs new_tenvM new_tenvC new_tenv new_decls new_tenvT decls' store.
type_top uniq rs.tdecs rs.tenvT rs.tenvM rs.tenvC rs.tenv top new_decls new_tenvT new_tenvM new_tenvC new_tenv ∧
type_sound_invariants NONE (rs.tdecs,rs.tenvT,rs.tenvM,rs.tenvC,rs.tenv,decls',rs.sem_env.sem_envM,rs.sem_env.sem_envC,rs.sem_env.sem_envE,store)
⇒
FV_top top ⊆ all_env_dom (rs.sem_env.sem_envM,rs.sem_env.sem_envC,rs.sem_env.sem_envE)`,
Expand Down
Loading

0 comments on commit 578b471

Please sign in to comment.