Skip to content
Permalink
Browse files

Merge pull request #643 from CakeML/cleanup

Update given various spt theorems have moved to HOL
  • Loading branch information...
xrchz committed May 11, 2019
2 parents 53fd12a + c3401d4 commit 96ec9c17d55e54ccc04d7858e8f7a1257f8452ec
@@ -678,7 +678,7 @@ Theorem tick_compile_prog_res_range
THEN1
(fs [domain_union,EXTENSION]
\\ reverse conj_tac THEN1 metis_tac []
\\ fs [subspt_alt,lookup_insert] \\ rw []
\\ fs [subspt_lookup,lookup_insert] \\ rw []
\\ fs [lookup_union,lookup_insert,lookup_def,case_eq_thms]
\\ metis_tac [lookup_NONE_domain])
\\ fs [GSYM union_assoc]
@@ -699,7 +699,7 @@ Theorem tick_compile_prog_res_range
\\ fs [SUBSET_DEF] \\ res_tac
\\ imp_res_tac subspt_domain_SUBSET
\\ fs [EXTENSION,SUBSET_DEF] \\ metis_tac [])
\\ fs [subspt_alt]
\\ fs [subspt_lookup]
\\ fs [lookup_union,fromAList_def,lookup_insert]
\\ rw [] \\ fs[domain_lookup]
\\ rw [] \\ fs []);
@@ -769,7 +769,7 @@ val tick_compile_prog_IMP_exp_rel = prove(
THEN1
(match_mp_tac subspt_exp_rel
\\ qexists_tac `src_code`
\\ conj_tac THEN1 fs [subspt_alt,lookup_union]
\\ conj_tac THEN1 fs [subspt_lookup,lookup_union]
\\ match_mp_tac exp_rel_tick_inline \\ metis_tac [])
\\ first_x_assum drule
\\ disch_then (qspec_then `k` mp_tac) \\ fs []
@@ -784,7 +784,7 @@ val tick_compile_prog_IMP_exp_rel = prove(
(first_x_assum drule \\ strip_tac \\ fs []
\\ match_mp_tac (subspt_exp_rel |> ONCE_REWRITE_RULE [CONJ_COMM])
\\ asm_exists_tac \\ fs []
\\ fs [subspt_alt,lookup_union])
\\ fs [subspt_lookup,lookup_union])
\\ CCONTR_TAC \\ fs [] \\ metis_tac [])
\\ reverse (rw [])
THEN1 (fs [DISJOINT_DEF,domain_union,EXTENSION] \\ metis_tac [])
@@ -794,14 +794,14 @@ val tick_compile_prog_IMP_exp_rel = prove(
\\ fs [lookup_union,case_eq_thms,GSYM lookup_NONE_domain]
\\ match_mp_tac subspt_exp_rel
\\ qexists_tac `src_code`
\\ conj_tac THEN1 fs [subspt_alt,lookup_union]
\\ conj_tac THEN1 fs [subspt_lookup,lookup_union]
\\ match_mp_tac exp_rel_tick_inline \\ metis_tac [])
\\ fs [lookup_union,case_eq_thms,GSYM lookup_NONE_domain,lookup_insert,lookup_def]
\\ pop_assum (assume_tac o GSYM)
\\ first_x_assum drule \\ strip_tac \\ fs []
\\ match_mp_tac (subspt_exp_rel |> ONCE_REWRITE_RULE [CONJ_COMM])
\\ asm_exists_tac \\ fs []
\\ fs [subspt_alt,lookup_union]);
\\ fs [subspt_lookup,lookup_union]);

val in_do_app_lemma = prove(
``in_state_rel limit s1 t1 ==>
@@ -846,7 +846,7 @@ val in_do_app_lemma = prove(
\\ asm_exists_tac \\ fs []
\\ reverse conj_tac
THEN1 (unabbrev_all_tac \\ fs [DISJOINT_DEF,EXTENSION] \\ metis_tac [])
\\ rw [] \\ fs [subspt_alt]
\\ rw [] \\ fs [subspt_lookup]
\\ first_x_assum drule \\ strip_tac
\\ rename1 `lookup k2 t1.code = SOME (arity2,v)`
\\ Cases_on `lookup k2 s1.code`
@@ -62,7 +62,7 @@ val aux_code_installed_APPEND = Q.prove(
Theorem aux_code_installed_subspt
`!x c1 c2. aux_code_installed x c1 /\ subspt c1 c2 ==>
aux_code_installed x c2`
(Induct \\ fs [aux_code_installed_def,subspt_alt,FORALL_PROD]
(Induct \\ fs [aux_code_installed_def,subspt_lookup,FORALL_PROD]
\\ rw [] \\ fs [] \\ res_tac \\ fs []);

val _ = temp_overload_on("in_ns_0",``λn. n MOD bvl_to_bvi_namespaces = 0``);
@@ -1907,7 +1907,7 @@ val compile_exps_correct = Q.prove(
\\ drule bvi_letProofTheory.evaluate_compile_exp
\\ impl_tac THEN1 (Cases_on `res` \\ fs [semanticPrimitivesPropsTheory.map_result_def])
\\ strip_tac \\ fs []
\\ imp_res_tac evaluate_code_mono \\ fs [subspt_alt]
\\ imp_res_tac evaluate_code_mono \\ fs [subspt_lookup]
\\ res_tac \\ fs []
\\ `dec_clock 1 (inc_clock (c' + 1) t2) = inc_clock c' t2` by
(EVAL_TAC \\ fs [] \\ NO_TAC)
@@ -1978,7 +1978,7 @@ val compile_exps_correct = Q.prove(
\\ full_simp_tac(srw_ss())[aux_code_installed_def,
iEval_def,find_code_def,compile_aux_def]
\\ IMP_RES_TAC (GEN_ALL evaluate_MAP_Var) \\ full_simp_tac(srw_ss())[]
\\ imp_res_tac bviPropsTheory.evaluate_code_mono \\ fs [subspt_alt]
\\ imp_res_tac bviPropsTheory.evaluate_code_mono \\ fs [subspt_lookup]
\\ `evaluate ([d2],MAP (adjust_bv b2) vs ++ MAP (adjust_bv b2) env,
inc_clock c t1) =
evaluate ([d2],MAP (adjust_bv b2) vs,inc_clock c t1)` by
@@ -2235,7 +2235,7 @@ val compile_exps_correct = Q.prove(
\\ qexists_tac `n6` \\ fs []
\\ match_mp_tac aux_code_installed_subspt
\\ asm_exists_tac \\ fs []
\\ fs [subspt_alt,lookup_union])
\\ fs [subspt_lookup,lookup_union])
\\ `lookup (num_stubs + name * nss) t2.code = NONE` by
(fs [names_ok_def,domain_lookup,PULL_EXISTS]
\\ Cases_on `lookup (num_stubs + name * nss) t2.code` \\ fs []
@@ -2250,14 +2250,14 @@ val compile_exps_correct = Q.prove(
(match_mp_tac aux_code_installed_subspt
\\ qexists_tac `(fromAList (append p1))`
\\ reverse conj_tac THEN1
(fs [subspt_alt,lookup_union] \\ rw [] \\ simp [case_eq_thms]
(fs [subspt_lookup,lookup_union] \\ rw [] \\ simp [case_eq_thms]
\\ fs [IN_DISJOINT]
\\ rename1 `lookup kk _ = _`
\\ first_x_assum (qspec_then `kk` mp_tac)
\\ fs [lookup_fromAList] \\ imp_res_tac ALOOKUP_MEM
\\ fs [domain_lookup]
\\ Cases_on `lookup kk t2.code` \\ fs []
\\ fs [MEM_MAP,FORALL_PROD] \\ PairCases_on `v` \\ metis_tac [])
\\ fs [MEM_MAP,FORALL_PROD] \\ PairCases_on `y` \\ metis_tac [])
\\ match_mp_tac aux_code_installed_sublist \\ fs [])
\\ imp_res_tac ALOOKUP_MEM
\\ fs [names_ok_def]
@@ -2280,7 +2280,7 @@ val compile_exps_correct = Q.prove(
CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac`c` \\ simp[] \\ rveq \\
simp[adjust_bv_def]
\\ fs[state_rel_def,domain_lookup]
\\ imp_res_tac evaluate_mono \\ fs [subspt_alt,domain_lookup]
\\ imp_res_tac evaluate_mono \\ fs [subspt_lookup,domain_lookup]
\\ res_tac \\ fs []
\\ Cases_on`v` \\ res_tac
\\ pairarg_tac \\ fs[])
@@ -948,7 +948,7 @@ Theorem close_spt_thm
mp_tac subspt_domain_spt_fold_union >>
rw[] >> fs[SUBSET_DEF] >>
first_x_assum mp_tac >> impl_tac >> fs[] >>
fs[subspt_alt, lookup_inter, domain_difference] >> rw[] >>
fs[subspt_lookup, lookup_inter, domain_difference] >> rw[] >>
EVERY_CASE_TAC >> fs[])
)
>- (
@@ -2573,13 +2573,8 @@ Theorem INJ_UPDATE
(simp_tac std_ss [BIJ_DEF,SURJ_DEF,INJ_DEF,IN_INSERT,APPLY_UPDATE_THM]
\\ metis_tac []);

(* exists in HOL as subspt_lookup *)
Theorem subspt_alt
`subspt t1 t2 <=> !k v. lookup k t1 = SOME v ==> lookup k t2 = SOME v`
(fs [subspt_def,domain_lookup] \\ rw [] \\ eq_tac \\ rw []
\\ res_tac \\ fs []);

(* TODO - exists as an IFF in HOL already (subspt_domain) *)
(* TODO: candidate for move to HOL;
subspt_domain exists already but is specialised to unit *)
Theorem subspt_domain_SUBSET
`subspt t1 t2 ==> domain t1 SUBSET domain t2`
(fs [subspt_def,SUBSET_DEF]);
@@ -3414,108 +3409,6 @@ Theorem lookup_copy_shape

(* BEGIN TODO: move to sptreeTheory *)

val mk_BN_thm = prove(
``!t1 t2. mk_BN t1 t2 =
if isEmpty t1 /\ isEmpty t2 then LN else BN t1 t2``,
REPEAT Cases >> EVAL_TAC);

val mk_BS_thm = prove(
``!t1 t2. mk_BS t1 x t2 =
if isEmpty t1 /\ isEmpty t2 then LS x else BS t1 x t2``,
REPEAT Cases >> EVAL_TAC);

val oddevenlemma = prove(
``2n * y + 1 <> 2 * x + 2``,
disch_then (mp_tac o AP_TERM ``EVEN``) >>
simp[EVEN_ADD, EVEN_MULT]);

Theorem size_domain
`∀ t . size t = CARD (domain t)`
(Induct_on `t`
>- rw[size_def, domain_def]
>- rw[size_def, domain_def]
>> rw[pred_setTheory.CARD_UNION_EQN, pred_setTheory.CARD_INJ_IMAGE]
>| [
`IMAGE (λn. 2 * n + 2) (domain t) ∩ IMAGE (λn. 2 * n + 1) (domain t') = {}`
by (rw[GSYM pred_setTheory.DISJOINT_DEF, pred_setTheory.IN_DISJOINT]
>> Cases_on `ODD x`
>> fs[ODD_EXISTS, ADD1, oddevenlemma]
)
>> simp[] ,
`(({0} ∩ IMAGE (λn. 2 * n + 2) (domain t)) = {}) /\
(({0} UNION (IMAGE (\n. 2 * n + 2) (domain t)))
INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})`
by (rw[GSYM pred_setTheory.DISJOINT_DEF, pred_setTheory.IN_DISJOINT]
>> Cases_on `ODD x`
>> fs[ODD_EXISTS, ADD1, oddevenlemma]
)
>> simp[]
]
);

Theorem num_set_domain_eq
`∀ t1 t2:num_set . wf t1 ∧ wf t2 ⇒
(domain t1 = domain t2 ⇔ t1 = t2)`
(rw[] >> EQ_TAC >> rw[spt_eq_thm] >> fs[EXTENSION, domain_lookup] >>
pop_assum (qspec_then `n` mp_tac) >> strip_tac >>
Cases_on `lookup n t1` >> fs[] >> Cases_on `lookup n t2` >> fs[]
);

Theorem union_num_set_sym
`∀ t1:num_set t2 . union t1 t2 = union t2 t1`
(Induct >> fs[union_def] >> rw[] >> CASE_TAC >> fs[union_def]
);

Theorem mk_wf_union
`∀ t1 t2 . mk_wf (union t1 t2) = union (mk_wf t1) (mk_wf t2)`
(rw[] >> `wf(union (mk_wf t1) (mk_wf t2)) ∧ wf(mk_wf (union t1 t2))` by
metis_tac[wf_mk_wf, wf_union] >>
rw[spt_eq_thm] >> fs[lookup_union, lookup_mk_wf]
);

Theorem domain_difference
`∀ t1 t2 . domain (difference t1 t2) = (domain t1) DIFF (domain t2)`
(simp[pred_setTheory.EXTENSION, domain_lookup, lookup_difference] >>
rw [] >> Cases_on `lookup x t1`
>- fs[]
>> fs[] >> Cases_on `lookup x t2`
>- rw[] >- rw[]
);

Theorem difference_sub
`(difference a b = LN) ⇒ (domain a ⊆ domain b)`
(rw[] >>
`(domain (difference a b) = {})` by rw[domain_def] >>
fs[EXTENSION, domain_difference, SUBSET_DEF] >>
metis_tac[]
);

Theorem wf_difference
`∀ t1 t2 . (wf t1 ∧ wf t2) ⇒ wf (difference t1 t2)`
(Induct >> rw[difference_def, wf_def] >> CASE_TAC >> fs[wf_def]
>> rw[wf_def, wf_mk_BN, wf_mk_BS]
);

Theorem delete_fail
`∀ n t . (wf t) ⇒ (n ∉ domain t ⇔ (delete n t = t))`
(simp[domain_lookup] >>
recInduct lookup_ind >>
rw[lookup_def, wf_def, delete_def, mk_BN_thm, mk_BS_thm]
);

Theorem size_delete
`∀ n t . (size (delete n t) =
if (lookup n t = NONE) then (size t) else (size t - 1))`
(rw[size_def] >>
fs[lookup_NONE_domain] >>
TRY (qpat_assum `n NOTIN d` (qspecl_then [] mp_tac)) >>
rfs[delete_fail, size_def] >>
fs[lookup_NONE_domain] >>
fs[size_domain] >>
fs[lookup_NONE_domain] >>
fs[size_domain]
);

Theorem lookup_zero
`∀ n t x. (lookup n t = SOME x) ==> (size t <> 0)`
(recInduct lookup_ind

0 comments on commit 96ec9c1

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