Skip to content

Commit

Permalink
Provide old_dxrule in preamble; continue fixing broken scripts
Browse files Browse the repository at this point in the history 
In scripts that fail, I now think best practice is to find-and-replace
drule with old_drule rather than rebinding to allow future editors to
get the benefit of the new drule.
  • Loading branch information
@mn200
mn200 committed Aug 14, 2019
1 parent df1f937 commit ad1ba92
Show file tree
Hide file tree
Showing 4 changed files with 175 additions and 169 deletions.
94 changes: 47 additions & 47 deletions compiler/backend/proofs/data_to_wordProofScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ val _ = set_grammar_ancestry
val _ = hide "next";

val clean_tac = rpt var_eq_tac \\ rpt (qpat_x_assum `T` kall_tac)
fun rpt_drule th = drule (th |> GEN_ALL) \\ rpt (disch_then drule \\ fs [])
fun rpt_drule th = old_drule (th |> GEN_ALL) \\ rpt (disch_then old_drule \\ fs [])

val state_rel_def = data_to_word_gcProofTheory.state_rel_def
val code_rel_def = data_to_word_gcProofTheory.code_rel_def
Expand Down Expand Up @@ -91,8 +91,8 @@ Proof
asm_exists_tac >> fs[] >> rpt strip_tac >> fs[] >>
imp_res_tac cut_state_opt_const \\ fs[state_rel_def])
\\ Cases_on `a`
\\ drule (GEN_ALL assign_thm) \\ full_simp_tac(srw_ss())[]
\\ rpt (disch_then drule)
\\ drule assign_thm \\ full_simp_tac(srw_ss())[]
\\ rpt (disch_then old_drule)
\\ disch_then (qspecl_then [`n`,`l`,`dest`] strip_assume_tac)
\\ full_simp_tac(srw_ss())[] \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
\\ imp_res_tac do_app_io_events_mono \\ rev_full_simp_tac(srw_ss())[]
Expand Down Expand Up @@ -137,7 +137,7 @@ Proof
(t with locals := insert 1 (Word (alloc_size k)) t.locals))
:('a result option)#( ('a,'c,'ffi) wordSem$state)`
\\ full_simp_tac(srw_ss())[]
\\ drule (GEN_ALL alloc_lemma)
\\ drule alloc_lemma
\\ rpt (disch_then drule)
\\ rw [] \\ fs [])
\\ fs [SilentFFI_def,wordSemTheory.evaluate_def,list_Seq_def,eq_eval]
Expand All @@ -146,14 +146,14 @@ Proof
ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``,
wordSemTheory.get_var_def,lookup_insert]
\\ fs [cut_env_adjust_set_insert_1,cut_env_adjust_set_insert_3]
\\ drule (GEN_ALL cut_env_IMP_cut_env)
\\ drule cut_env_IMP_cut_env
\\ Cases_on `dataSem$cut_env names s.locals` \\ fs []
\\ disch_then drule \\ strip_tac \\ fs []
\\ pairarg_tac \\ fs []
\\ drule (GEN_ALL state_rel_cut_env_cut_env)
\\ drule state_rel_cut_env_cut_env
\\ rpt (disch_then drule)
\\ strip_tac
\\ drule (GEN_ALL alloc_lemma) \\ fs [] \\ rveq
\\ drule alloc_lemma \\ fs [] \\ rveq
\\ `dataSem$cut_env names x = SOME x` by
(fs [dataSemTheory.cut_env_def] \\ rveq \\ fs [lookup_inter_alt,domain_inter])
\\ rpt (disch_then drule)
Expand Down Expand Up @@ -254,7 +254,7 @@ Proof
\\ rename1 `_ = SOME x9` \\ Cases_on `x9` \\ full_simp_tac(srw_ss())[]
\\ Cases_on `handler` \\ full_simp_tac(srw_ss())[]
\\ `t.clock = s.clock` by full_simp_tac(srw_ss())[state_rel_def]
\\ drule (GEN_ALL find_code_thm) \\ rpt (disch_then drule)
\\ drule find_code_thm \\ rpt (disch_then drule)
\\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
\\ Cases_on `s.clock = 0` \\ fs[] \\ srw_tac[][] \\ fs[]
THEN1 (fs[call_env_def,wordSemTheory.call_env_def,state_rel_def])
Expand Down Expand Up @@ -420,7 +420,7 @@ Theorem compile_correct_lemma:
| SOME (Rerr (Rabort e)) => (res1 = SOME TimeOut) /\ t1.ffi = s1.ffi)
Proof
rpt strip_tac
\\ drule data_compile_correct \\ full_simp_tac(srw_ss())[]
\\ old_drule data_compile_correct \\ full_simp_tac(srw_ss())[]
\\ ntac 2 (disch_then drule) \\ full_simp_tac(srw_ss())[comp_def]
\\ strip_tac
\\ qexists_tac `t1`
Expand Down Expand Up @@ -514,7 +514,7 @@ Proof
\\ `state_rel x0 l1 l2 s (t2 with permute := perm') [] []` by
(full_simp_tac(srw_ss())[state_rel_def] \\ rev_full_simp_tac(srw_ss())[]
\\ Cases_on `s.stack` \\ full_simp_tac(srw_ss())[] \\ metis_tac [])
\\ drule compile_correct_lemma \\ fs []
\\ old_drule compile_correct_lemma \\ fs []
\\ disch_then (drule o ONCE_REWRITE_RULE [CONJ_COMM])
\\ fs [] \\ strip_tac \\ fs []
THEN1 (rveq \\ fs [] \\ every_case_tac \\ fs[])
Expand All @@ -533,7 +533,7 @@ val state_rel_ext_with_clock = Q.prove(
`state_rel_ext a b c s1 s2 ==>
state_rel_ext a b c (s1 with clock := k) (s2 with clock := k)`,
full_simp_tac(srw_ss())[state_rel_ext_def] \\ srw_tac[][]
\\ drule state_rel_with_clock
\\ old_drule state_rel_with_clock
\\ strip_tac \\ asm_exists_tac \\ full_simp_tac(srw_ss())[]
\\ qexists_tac `l` \\ full_simp_tac(srw_ss())[]
\\ fs [wordSemTheory.state_component_equality]
Expand Down Expand Up @@ -562,17 +562,17 @@ Proof
last_x_assum(qspec_then`k'`mp_tac)>>simp[] >>
(fn g => subterm (fn tm => Cases_on`^(assert(has_pair_type)tm)`) (#2 g) g) >>
strip_tac >>
drule compile_correct >> simp[] >> full_simp_tac(srw_ss())[] >>
old_drule compile_correct >> simp[] >> full_simp_tac(srw_ss())[] >>
simp[RIGHT_FORALL_IMP_THM,GSYM AND_IMP_INTRO] >>
impl_tac >- (
strip_tac >> full_simp_tac(srw_ss())[] ) >>
drule(GEN_ALL state_rel_ext_with_clock) >>
drule state_rel_ext_with_clock >>
disch_then(qspec_then`k'`strip_assume_tac) >> full_simp_tac(srw_ss())[] >>
disch_then drule >>
simp[comp_def] >> strip_tac >>
qmatch_assum_abbrev_tac`option_CASE (FST p) _ _` >>
Cases_on`p`>>pop_assum(strip_assume_tac o SYM o REWRITE_RULE[markerTheory.Abbrev_def]) >>
drule (GEN_ALL wordPropsTheory.evaluate_add_clock) >>
drule wordPropsTheory.evaluate_add_clock >>
simp[RIGHT_FORALL_IMP_THM] >>
impl_tac >- (strip_tac >> full_simp_tac(srw_ss())[]) >>
disch_then(qspec_then`ck`mp_tac) >>
Expand All @@ -583,25 +583,25 @@ Proof
srw_tac[][extend_with_resource_limit_def] >> full_simp_tac(srw_ss())[] >>
`r' <> Rerr(Rabort Rtype_error)` by(CCONTR_TAC >> fs[]) >>
`r' <> Rerr(Rabort Rtimeout_error)` by(CCONTR_TAC >> fs[]) >>
drule(dataPropsTheory.evaluate_add_clock)>>simp[]>>
old_drule(dataPropsTheory.evaluate_add_clock)>>simp[]>>
disch_then(qspec_then`k'`mp_tac)>>simp[]>>strip_tac>>
drule(compile_correct)>>simp[]>>
drule(GEN_ALL state_rel_ext_with_clock)>>simp[]>>
old_drule(compile_correct)>>simp[]>>
drule state_rel_ext_with_clock >>simp[]>>
disch_then(qspec_then `k+k'` assume_tac)>>disch_then drule>>
simp[inc_clock_def]>>strip_tac>>
qpat_x_assum `evaluate _ = (r,_)` assume_tac>>
dxrule(GEN_ALL wordPropsTheory.evaluate_add_clock)>>
dxrule wordPropsTheory.evaluate_add_clock >>
disch_then(qspec_then `ck+k` mp_tac)>>
impl_tac>-(CCONTR_TAC>>fs[])>>
simp[inc_clock_def]>>strip_tac>>
rpt(PURE_FULL_CASE_TAC>>fs[]>>rveq>>fs[])) >>
srw_tac[][] >> full_simp_tac(srw_ss())[] >>
drule compile_correct >> simp[] >>
old_drule compile_correct >> simp[] >>
simp[RIGHT_FORALL_IMP_THM,GSYM AND_IMP_INTRO] >>
impl_tac >- (
last_x_assum(qspec_then`k`mp_tac)>>simp[] >>
srw_tac[][] >> strip_tac >> full_simp_tac(srw_ss())[] ) >>
drule(state_rel_ext_with_clock) >> simp[] >> strip_tac >>
old_drule(state_rel_ext_with_clock) >> simp[] >> strip_tac >>
disch_then drule >>
simp[comp_def] >> strip_tac >>
first_x_assum(qspec_then`k+ck`mp_tac) >>
Expand All @@ -616,16 +616,16 @@ Proof
last_x_assum(qspec_then`k`mp_tac)>>simp[] >>
(fn g => subterm (fn tm => Cases_on`^(assert(has_pair_type)tm)`) (#2 g) g) >>
strip_tac >>
drule compile_correct >> simp[] >>
old_drule compile_correct >> simp[] >>
simp[RIGHT_FORALL_IMP_THM,GSYM AND_IMP_INTRO] >>
impl_tac >- ( strip_tac >> full_simp_tac(srw_ss())[] ) >>
drule(state_rel_ext_with_clock) >>
old_drule(state_rel_ext_with_clock) >>
simp[] >> strip_tac >>
disch_then drule >>
simp[comp_def] >> strip_tac >>
qmatch_assum_abbrev_tac`option_CASE (FST p) _ _` >>
Cases_on`p`>>pop_assum(strip_assume_tac o SYM o REWRITE_RULE[markerTheory.Abbrev_def]) >>
drule (GEN_ALL wordPropsTheory.evaluate_add_clock) >>
drule wordPropsTheory.evaluate_add_clock >>
simp[RIGHT_FORALL_IMP_THM] >>
impl_tac >- (strip_tac >> full_simp_tac(srw_ss())[]) >>
disch_then(qspec_then`ck`mp_tac) >>
Expand All @@ -637,13 +637,13 @@ Proof
qpat_x_assum`∀x y. _`(qspec_then`k`mp_tac)>>
(fn g => subterm (fn tm => Cases_on`^(assert(has_pair_type)tm)`) (#2 g) g) >>
strip_tac >>
drule(compile_correct)>>
old_drule(compile_correct)>>
simp[RIGHT_FORALL_IMP_THM,GSYM AND_IMP_INTRO] >>
impl_tac >- (
strip_tac >> full_simp_tac(srw_ss())[] >>
last_x_assum(qspec_then`k`mp_tac) >>
simp[] ) >>
drule(state_rel_ext_with_clock) >>
old_drule(state_rel_ext_with_clock) >>
simp[] >> strip_tac >>
disch_then drule >>
simp[comp_def] >> strip_tac >>
Expand All @@ -657,7 +657,7 @@ Proof
first_x_assum(qspec_then`k+ck`mp_tac) >>
fsrw_tac[ARITH_ss][inc_clock_def] >>
qhdtm_x_assum`wordSem$evaluate`mp_tac >>
drule(GEN_ALL wordPropsTheory.evaluate_add_clock)>>
drule wordPropsTheory.evaluate_add_clock >>
simp[]>>
disch_then(qspec_then`ck`mp_tac)>>
last_x_assum(qspec_then`k`mp_tac) >>
Expand All @@ -676,7 +676,7 @@ Proof
dataPropsTheory.evaluate_add_clock_io_events_mono,
dataPropsTheory.initial_state_with_simp,
dataPropsTheory.initial_state_simp]) >>
drule build_lprefix_lub_thm >>
old_drule build_lprefix_lub_thm >>
simp[lprefix_lub_def] >> strip_tac >>
match_mp_tac (GEN_ALL LPREFIX_TRANS) >>
simp[LPREFIX_fromList] >>
Expand Down Expand Up @@ -716,14 +716,14 @@ Proof
reverse conj_tac >> strip_tac >- (
qmatch_assum_abbrev_tac`n < LENGTH (_ (_ (SND p)))` >>
Cases_on`p`>>pop_assum(assume_tac o SYM o REWRITE_RULE[markerTheory.Abbrev_def]) >>
drule compile_correct >>
old_drule compile_correct >>
simp[GSYM AND_IMP_INTRO,RIGHT_FORALL_IMP_THM] >>
impl_tac >- (
last_x_assum(qspec_then`k`mp_tac)>>srw_tac[][]>>
strip_tac >> full_simp_tac(srw_ss())[] ) >>
drule(state_rel_ext_with_clock) >>
old_drule(state_rel_ext_with_clock) >>
simp[] >> strip_tac >>
disch_then drule >>
disch_then old_drule >>
simp[comp_def] >> strip_tac >>
qexists_tac`k+ck`>>full_simp_tac(srw_ss())[inc_clock_def]>>
Cases_on`res1=SOME NotEnoughSpace`>>full_simp_tac(srw_ss())[]>-(
Expand All @@ -738,14 +738,14 @@ Proof
rpt(first_x_assum(qspec_then`k+ck`mp_tac)>>simp[]) >>
every_case_tac >> fs[]) >>
(fn g => subterm (fn tm => Cases_on`^(Term.subst [{redex = #1(dest_exists(#2 g)), residue = ``k:num``}] (assert(has_pair_type)tm))`) (#2 g) g) >>
drule compile_correct >>
old_drule compile_correct >>
simp[GSYM AND_IMP_INTRO,RIGHT_FORALL_IMP_THM] >>
impl_tac >- (
last_x_assum(qspec_then`k`mp_tac)>>srw_tac[][]>>
strip_tac >> full_simp_tac(srw_ss())[] ) >>
drule(state_rel_ext_with_clock) >>
old_drule(state_rel_ext_with_clock) >>
simp[] >> strip_tac >>
disch_then drule >>
disch_then old_drule >>
simp[comp_def] >> strip_tac >>
full_simp_tac(srw_ss())[inc_clock_def] >>
Cases_on`res1=SOME NotEnoughSpace`>>full_simp_tac(srw_ss())[]>-(
Expand Down Expand Up @@ -895,11 +895,11 @@ Proof
Cases_on `opname`>>
TRY(
rename1`WordOp _ _`>>
pairarg_tac>>drule extract_labels_assignWordOp>>
pairarg_tac>>old_drule extract_labels_assignWordOp>>
simp[])>>
TRY(
rename1`WordShift _ _ _`>>
pairarg_tac>>drule extract_labels_assignWordShift>>
pairarg_tac>>old_drule extract_labels_assignWordShift>>
simp[])>>
fs[extract_labels_def,GiveUp_def,assign_def,assign_def_extras]>>
BasicProvers.EVERY_CASE_TAC>>
Expand Down Expand Up @@ -1294,7 +1294,7 @@ Proof
Induct \\ rw[fake_moves_def] \\ rw[]
\\ pairarg_tac \\ fs[]
\\ fs[CaseEq"option"] \\ rw[]
\\ first_x_assum drule \\ rw[]
\\ first_x_assum old_drule \\ rw[]
\\ rw[fake_move_def]
QED

Expand Down Expand Up @@ -1356,7 +1356,7 @@ val word_get_code_labels_full_ssa_cc_trans = Q.prove(`
\\ fs[setup_ssa_def]
\\ pairarg_tac \\ fs[]
\\ rveq \\ fs[]
\\ drule word_get_code_labels_ssa_cc_trans
\\ old_drule word_get_code_labels_ssa_cc_trans
\\ rw[]);

Theorem word_good_handlers_fake_moves:
Expand All @@ -1368,7 +1368,7 @@ Proof
Induct \\ rw[fake_moves_def] \\ rw[]
\\ pairarg_tac \\ fs[]
\\ fs[CaseEq"option"] \\ rw[]
\\ first_x_assum drule \\ rw[]
\\ first_x_assum old_drule \\ rw[]
\\ rw[fake_move_def]
QED

Expand Down Expand Up @@ -1430,7 +1430,7 @@ val word_good_handlers_full_ssa_cc_trans = Q.prove(`
\\ fs[setup_ssa_def]
\\ pairarg_tac \\ fs[]
\\ rveq \\ fs[]
\\ drule word_good_handlers_ssa_cc_trans
\\ old_drule word_good_handlers_ssa_cc_trans
\\ rw[]);

(* inst *)
Expand Down Expand Up @@ -1508,7 +1508,7 @@ Proof
recInduct simp_if_ind
\\ rw[simp_if_def]
\\ CASE_TAC \\ simp[]
>- ( drule word_get_code_labels_apply_if_opt \\ rw[] )
>- ( old_drule word_get_code_labels_apply_if_opt \\ rw[] )
\\ every_case_tac \\ fs[]
QED

Expand Down Expand Up @@ -1540,7 +1540,7 @@ val word_good_handlers_simp_if = Q.prove(`
recInduct simp_if_ind
\\ rw[simp_if_def]
\\ CASE_TAC \\ simp[]
>- ( drule word_good_handlers_apply_if_opt \\ rw[] )
>- ( old_drule word_good_handlers_apply_if_opt \\ rw[] )
\\ every_case_tac \\ fs[]);

val word_get_code_labels_Seq_assoc = Q.prove(`
Expand Down Expand Up @@ -1613,12 +1613,12 @@ val word_get_code_labels_word_to_word = Q.prove(`
fs[word_get_code_labels_remove_must_terminate,word_get_code_labels_word_alloc]>>
fs[COND_RAND]>>
fs[word_get_code_labels_three_to_two_reg]>>
drule (word_get_code_labels_remove_dead|>SIMP_RULE std_ss [SUBSET_DEF])>>
old_drule (word_get_code_labels_remove_dead|>SIMP_RULE std_ss [SUBSET_DEF])>>
simp[word_get_code_labels_full_ssa_cc_trans,word_get_code_labels_inst_select]>>
strip_tac>>
drule (word_get_code_labels_word_simp|>SIMP_RULE std_ss [SUBSET_DEF])>>
old_drule (word_get_code_labels_word_simp|>SIMP_RULE std_ss [SUBSET_DEF])>>
rw[]>>fs[FORALL_PROD,EXISTS_PROD,PULL_EXISTS,EVERY_MEM]>>
first_x_assum drule>>
first_x_assum old_drule>>
disch_then(qspecl_then [`q`,`q'`] mp_tac)>>
impl_tac >-
metis_tac[EL_MEM]>>
Expand Down Expand Up @@ -1741,11 +1741,11 @@ Proof
fs[MAP_MAP_o,o_DEF,LAMBDA_PROD,compile_part_def]>>
fs[SUBSET_DEF,PULL_EXISTS,Once MEM_MAP,FORALL_PROD]>>
rw[]>>
drule (data_to_word_comp_code_labels |> SIMP_RULE std_ss [SUBSET_DEF])>>
old_drule (data_to_word_comp_code_labels |> SIMP_RULE std_ss [SUBSET_DEF])>>
rw[]
>-
(first_x_assum drule>>
disch_then drule>>fs[MEM_MAP,EXISTS_PROD])
(first_x_assum old_drule>>
disch_then old_drule>>fs[MEM_MAP,EXISTS_PROD])
>>
fs[MEM_MAP]>>metis_tac[]
QED
Expand Down
6 changes: 3 additions & 3 deletions compiler/backend/proofs/stack_allocProofScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5707,17 +5707,17 @@ Proof
srw_tac[][] >>
Cases_on`r=TimeOut`>>full_simp_tac(srw_ss())[]>>
qpat_x_assum `evaluate _ = (SOME r, t)` assume_tac >>
dxrule comp_correct_thm >>
old_dxrule comp_correct_thm >>
simp[RIGHT_FORALL_IMP_THM] >>
impl_tac >- (
simp[alloc_arg_def] >>
reverse conj_tac >- metis_tac[] >>
CCONTR_TAC >> fs[]) >>
strip_tac >>
dxrule(GEN_ALL evaluate_add_clock) >>
old_dxrule(GEN_ALL evaluate_add_clock) >>
disch_then(qspec_then `k'` mp_tac) >>
impl_tac >- (CCONTR_TAC >> fs[]) >>
dxrule(GEN_ALL evaluate_add_clock) >>
dxrule evaluate_add_clock >>
disch_then(qspec_then `ck + k` mp_tac) >>
impl_tac >- (CCONTR_TAC >> fs[]) >>
ntac 2 strip_tac >>
Expand Down
Loading

0 comments on commit ad1ba92

Please sign in to comment.