Skip to content
Permalink
Browse files

Fix now-broken drule applications (viz recent HOL change)

  • Loading branch information...
mn200 committed Aug 12, 2019
1 parent 980410c commit aed98c922e3b207e145f2bec7c3c09217c9ce952
@@ -1966,6 +1966,7 @@ val FST_rw = Q.prove(
`(\(x,_,_). x) = FST`,
fs [FUN_EQ_THM,FORALL_PROD]);

val _ = print "Proving cf_letrec_sound_aux\n";
val cf_letrec_sound_aux = Q.prove (
`!funs e.
let naryfuns = letrec_pull_params funs in
@@ -2081,6 +2082,7 @@ val cf_letrec_sound_aux = Q.prove (
rfs [terminationTheory.evaluate_def]
));

val _ = print "Proving cf_letrec_sound\n";
val cf_letrec_sound = Q.prove (
`!funs e.
(!x. MEM x (letrec_pull_params funs) ==>
@@ -2104,6 +2106,7 @@ val cf_letrec_sound = Q.prove (
fs [letrec_pull_params_names, letrec_pull_params_def]
);

val _ = print "Proving cf_cases_evaluate_match\n";
val cf_cases_evaluate_match = Q.prove (
`!v env H Q nomatch_exn rows p st h_i h_k.
EVERY (\b. sound p (SND b) (cf p (SND b))) rows ==>
@@ -2190,6 +2193,7 @@ val cf_cases_evaluate_match = Q.prove (
qexists_tac `h_g UNION h_g'` \\ SPLIT_TAC
));

val _ = print "Proving cf_ffi_sound\n";
val cf_ffi_sound = Q.prove (
`sound (p:'ffi ffi_proj) (App (FFI ffi_index) [c; r]) (\env. local (\H Q.
?cv rv. exp2v env r = SOME rv /\
@@ -2334,8 +2338,8 @@ val cf_ffi_sound = Q.prove (
\\ rw[] \\ qexists_tac `s` \\ rw []
\\ fs [FLOOKUP_FUPDATE_LIST]
\\ rw [] \\ fs [FLOOKUP_DEF]
\\ drule ((ALL_DISTINCT_FLAT_MEM_IMP |> Q.INST [`m`|->`n`]))
\\ fs [MEM_MAP,FORALL_PROD] \\ metis_tac []) \\
\\ drule ALL_DISTINCT_FLAT_MEM_IMP
\\ fs [MEM_MAP,FORALL_PROD, PULL_EXISTS] \\ metis_tac []) \\
fs [EXTENSION] \\ reverse (rw [] \\ EQ_TAC \\ rw [])
THEN1
(qpat_x_assum `_ = p0 y'` (fn th => fs [GSYM th]) \\
@@ -2371,8 +2375,8 @@ val cf_ffi_sound = Q.prove (
\\ Cases_on `MEM n ns` \\ fs [FLOOKUP_FUPDATE_LIST]
\\ `MEM ns (MAP FST p1) /\ MEM ns' (MAP FST p1)` by
(fs [MEM_MAP,EXISTS_PROD] \\ metis_tac [])
\\ progress (ALL_DISTINCT_FLAT_MEM_IMP |> Q.INST [`m`|->`n`])
\\ rveq \\ fs [] \\ res_tac \\ fs [FLOOKUP_DEF])
\\ progress ALL_DISTINCT_FLAT_MEM_IMP
\\ rveq \\ fs [FLOOKUP_DEF] \\ metis_tac[])
\\ Cases_on `ns = ns'` \\ fs [] THEN1
(rveq \\ first_x_assum drule
\\ qpat_x_assum `_ = p0 y'` (fn th => fs [GSYM th])
@@ -2405,6 +2409,7 @@ val cf_ffi_sound = Q.prove (
\\ pop_assum mp_tac
\\ fs [] \\ fs [ffi2heap_def] \\ rfs[]);

val _ = print "Proving evaluate_add_to_clock_lemma\n";
val evaluate_add_to_clock_lemma = Q.prove (
`!extra p (s: 'ffi semanticPrimitives$state) s' r e.
evaluate s e p = (s', r) ==>
@@ -2414,6 +2419,7 @@ val evaluate_add_to_clock_lemma = Q.prove (
fs [evaluatePropsTheory.evaluate_add_to_clock]
);

val _ = print "Proving evaluate_match_add_to_clock_lemma\n";
val evaluate_match_add_to_clock_lemma = Q.prove (
`!extra (s: 'ffi semanticPrimitives$state) env v rows err_v s' r.
evaluate_match s env v rows err_v = (s', r) ==>
@@ -702,7 +702,7 @@ val gc_move_list_simulation = prove(
\\ rpt (pairarg_tac \\ fs []) \\ rveq
\\ fs []
\\ imp_res_tac gen_gcTheory.gc_move_list_ok
\\ drule gc_move_simulation \\ fs []
\\ FREEZE_THEN drule gc_move_simulation \\ fs []
\\ strip_tac \\ fs [] \\ rveq
\\ first_x_assum drule
\\ fs [] \\ strip_tac
@@ -945,7 +945,7 @@ val gc_move_data_simulation = prove(
\\ rpt (pairarg_tac \\ fs [])
\\ strip_tac \\ rveq
\\ imp_res_tac gc_move_data_ok \\ fs []
\\ drule gc_move_list_simulation
\\ drule_then drule gc_move_list_simulation
\\ fs [] \\ strip_tac \\ rveq
\\ `(∀ptr' u. MEM (Pointer ptr' u) l ⇒ ptr' < conf.limit)` by metis_tac[]
\\ first_x_assum drule \\ DISCH_TAC \\ fs[] \\ rveq
@@ -2428,7 +2428,7 @@ Proof
\\ IF_CASES_TAC \\ fs []
\\ drule roots_ok_APPEND
\\ strip_tac
\\ drule refs_root_IMP_isSomeData \\ simp [])
\\ drule_then drule refs_root_IMP_isSomeData \\ simp [])
\\ fs []
\\ fs [gc_related_def]
\\ `∀i. i ∈ FDOM f ⇒ isSomeDataElement (heap_lookup (i + conf.gen_start) heap)` by (rpt strip_tac
@@ -2455,11 +2455,13 @@ Proof
\\ fs [new_f_FDOM]
\\ rpt strip_tac
\\ Cases_on `x < conf.gen_start` \\ fs []
>- (drule heap_lookup_old_IMP_ALT
>- (drule_then (first_assum o mp_then Any mp_tac)
heap_lookup_old_IMP_ALT
\\ fs [isSomeDataElement_def,gen_inv_def]
\\ metis_tac [GSYM APPEND_ASSOC])
\\ IF_CASES_TAC \\ fs []
>- (drule heap_lookup_refs_IMP_ALT
>- (drule_then (first_assum o mp_then Any mp_tac)
heap_lookup_refs_IMP_ALT
\\ fs [gen_inv_def]
\\ impl_tac \\ fs []
\\ metis_tac [])
@@ -699,10 +699,11 @@ Proof
simp[ptree_Decl_def, tokcheckl_def, tokcheck_def] >> dsimp[]
>- metis_tac[Pattern_OK, E_OK]
>- metis_tac[AndFDecls_OK]
>- (drule TypeDec_OK >> dsimp[])
>- (drule_then (first_assum o mp_then Any mp_tac) TypeDec_OK >> dsimp[])
>- (fs[DISJ_IMP_THM, FORALL_AND_THM] >>
drule (GEN_ALL Dconstructor_OK) >> dsimp[FORALL_PROD])
>- (drule TypeAbbrevDec_OK >> dsimp[] >> rw[] >>
>- (drule_then (first_assum o mp_then Any mp_tac) TypeAbbrevDec_OK >>
dsimp[] >> rw[] >>
qmatch_abbrev_tac `∃d. foo ++ SOME x = SOME d` >>
Cases_on `foo` >> simp[])
>- fs[DISJ_IMP_THM, FORALL_AND_THM])
@@ -2049,7 +2049,7 @@ Proof
split_pair_case_tac
>> fs []
>> rename1 `evaluate _ _ _ = (st1, r1)`
>> drule (hd (CONJUNCTS exp_type_sound))
>> FREEZE_THEN drule (hd (CONJUNCTS exp_type_sound))
>> fs [type_sound_invariant_def]
>> disch_then drule
>> disch_then (qspec_then `Empty` mp_tac)

0 comments on commit aed98c9

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