Skip to content
Permalink
Browse files

Find and fix more definition-saves that cause loss of "compute"

  • Loading branch information...
mn200 committed Apr 15, 2019
1 parent 4c7ed00 commit b2c1007e2e54c223bcc1b1cb29e00c496a52e275
@@ -283,7 +283,8 @@ val merge_def = tDefine "merge" `
impl_tac >> simp[] >> Cases_on `ys` >> fs[] >> Cases_on `xs` >> fs[] >>
rename1 `SUC (LENGTH _) = LENGTH ll` >> Cases_on `ll` >> fs[])
val merge_def =
save_thm("merge_def[simp]", SIMP_RULE (bool_ss ++ ETA_ss) [] merge_def)
save_thm("merge_def[simp,compute]",
SIMP_RULE (bool_ss ++ ETA_ss) [] merge_def)

(* Avoid MAP2 *)
val merge_tup_def = tDefine "merge_tup" `
@@ -2167,7 +2167,7 @@ val v_rel_def = tDefine "v_rel" `
(WF_REL_TAC `measure (v_size o FST o SND o SND)` \\ simp [v1_size_append, v_size_def]
\\ rpt strip_tac \\ imp_res_tac v_size_lemma \\ simp []);

val v_rel_def = save_thm("v_rel_def[simp]",
val v_rel_def = save_thm("v_rel_def[simp,compute]",
v_rel_def |> SIMP_RULE (bool_ss ++ ETA_ss) []);

val v_rel_ind = theorem "v_rel_ind";
@@ -5034,7 +5034,7 @@ val val_approx_bodies_def = tDefine"val_approx_bodies_def"`
val val_approx_bodies_def =
val_approx_bodies_def
|> SIMP_RULE(srw_ss()++ETA_ss)[]
|> curry save_thm "val_approx_bodies_def[simp]";
|> curry save_thm "val_approx_bodies_def[simp,compute]";
Theorem val_approx_bodies_cons
`val_approx_bodies (x::ys) = val_approx_bodies [x] ++ val_approx_bodies ys`
@@ -5092,7 +5092,7 @@ val val_approx_dests_def = tDefine"val_approx_dests_def"`
val val_approx_dests_def =
val_approx_dests_def
|> SIMP_RULE(srw_ss()++ETA_ss)[]
|> curry save_thm "val_approx_dests_def[simp]";
|> curry save_thm "val_approx_dests_def[simp,compute]";
Theorem val_approx_dests_cons
`val_approx_dests a (x::ys) = val_approx_dests a [x] ∪ val_approx_dests a ys`
@@ -3998,7 +3998,7 @@ val state_rel_thm = Define `

val state_rel_thm = save_thm("state_rel_thm",state_rel_thm);

val state_rel_def = save_thm("state_rel_def",
val state_rel_def = save_thm("state_rel_def[compute]",
state_rel_thm |> REWRITE_RULE [memory_rel_def]);

Theorem state_rel_with_clock
@@ -7738,7 +7738,7 @@ val fix_clock_word_eq = prove(
\\ PairCases_on `x` \\ fs [] \\ fs [fix_clock_def] \\ rw []
\\ imp_res_tac word_eq_LESS_EQ \\ fs []);

val word_eq_def = save_thm("word_eq_def",
val word_eq_def = save_thm("word_eq_def[compute]",
word_eq_def |> REWRITE_RULE [fix_clock_word_eq]);

val word_eq_ind = save_thm("word_eq_ind",
@@ -650,7 +650,7 @@ val get_code_labels_def = tDefine"get_code_labels"
\\ Induct_on`es`
\\ rw[bviTheory.exp_size_def]
\\ simp[] \\ res_tac \\ simp[]);
val get_code_labels_def = get_code_labels_def |> SIMP_RULE (srw_ss()++ETA_ss)[] |> curry save_thm "get_code_labels_def[simp]"
val get_code_labels_def = get_code_labels_def |> SIMP_RULE (srw_ss()++ETA_ss)[] |> curry save_thm "get_code_labels_def[simp,compute]"

val good_code_labels_def = Define`
good_code_labels p ⇔
@@ -730,7 +730,7 @@ val get_code_labels_def = tDefine"get_code_labels"
\\ Induct_on`es`
\\ rw[bvlTheory.exp_size_def]
\\ simp[] \\ res_tac \\ simp[]);
val get_code_labels_def = get_code_labels_def |> SIMP_RULE (srw_ss()++ETA_ss)[] |> curry save_thm "get_code_labels_def[simp]"
val get_code_labels_def = get_code_labels_def |> SIMP_RULE (srw_ss()++ETA_ss)[] |> curry save_thm "get_code_labels_def[simp,compute]"

Theorem mk_tick_code_labels[simp]
`!n x. get_code_labels (mk_tick n x) = get_code_labels x`
@@ -1614,7 +1614,7 @@ val esgc_free_def = tDefine "esgc_free" `
(esgc_free (Op _ _ args) ⇔ EVERY esgc_free args)
` (WF_REL_TAC `measure exp_size` >> simp[] >> rpt strip_tac >>
imp_res_tac exp_size_MEM >> simp[])
val esgc_free_def = save_thm("esgc_free_def[simp]",
val esgc_free_def = save_thm("esgc_free_def[simp,compute]",
SIMP_RULE (bool_ss ++ ETA_ss) [] esgc_free_def)

(* state is setglobal-closure free *)
@@ -2830,7 +2830,7 @@ val obeys_max_app_def = tDefine"obeys_max_app"`
val obeys_max_app_def =
obeys_max_app_def
|> SIMP_RULE (srw_ss()++ETA_ss)[MAP_MAP_o]
|> curry save_thm "obeys_max_app_def[simp]"
|> curry save_thm "obeys_max_app_def[simp,compute]"

val no_Labels_def = tDefine"no_Labels"`
(no_Labels (Var _ _) ⇔ T) ∧
@@ -2854,7 +2854,7 @@ val no_Labels_def = tDefine"no_Labels"`
val no_Labels_def =
no_Labels_def
|> SIMP_RULE (srw_ss()++ETA_ss)[MAP_MAP_o]
|> curry save_thm "no_Labels_def[simp]"
|> curry save_thm "no_Labels_def[simp,compute]"

val app_call_dests_def = tDefine "app_call_dests" `
(app_call_dests opt [] = {}) /\
@@ -2905,7 +2905,7 @@ val app_call_dests_def = tDefine "app_call_dests" `
full_simp_tac(srw_ss())[closLangTheory.exp_size_def] >>
decide_tac);

val _ = save_thm("app_call_dests_def[simp]",app_call_dests_def);
val _ = save_thm("app_call_dests_def[simp,compute]",app_call_dests_def);

val _ = overload_on("call_dests",``app_call_dests (SOME T)``);
val _ = overload_on("app_dests",``app_call_dests (SOME F)``);
@@ -2995,7 +2995,7 @@ val get_code_labels_def = tDefine"get_code_labels" `
val get_code_labels_def =
get_code_labels_def
|> SIMP_RULE (srw_ss()++ETA_ss)[MAP_MAP_o]
|> curry save_thm "get_code_labels_def[simp]"
|> curry save_thm "get_code_labels_def[simp,compute]"

val code_locs_ind = theorem"code_locs_ind";

@@ -1033,7 +1033,7 @@ val esgc_free_def = tDefine "esgc_free" `
\\ fs [MEM_MAP] \\ rw []
\\ imp_res_tac flatLangTheory.exp_size_MEM \\ fs [])

val esgc_free_def = save_thm("esgc_free_def[simp]",
val esgc_free_def = save_thm("esgc_free_def[simp,compute]",
SIMP_RULE (bool_ss ++ ETA_ss) [] esgc_free_def)

Theorem elist_globals_eq_empty

0 comments on commit b2c1007

Please sign in to comment.
You can’t perform that action at this time.