Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove libScript.sml #1076

Merged
merged 1 commit into from
Oct 26, 2024
Merged

Remove libScript.sml #1076

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
72 changes: 36 additions & 36 deletions basis/TextIOProofScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -527,22 +527,22 @@ Theorem up_stdout_fastForwardFD:
Proof
rw[fastForwardFD_def,up_stdo_def]
\\ Cases_on`ALOOKUP fs.infds fd` >- (
fs[libTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[libTheory.the_def]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP] )
fs[miscTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[miscTheory.the_def]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP] )
\\ fs[] \\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` >- (
fs[libTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[libTheory.the_def]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[libTheory.the_def] )
\\ fs[libTheory.the_def]
\\ fs[fsupdate_def,libTheory.the_def,AFUPDKEY_ALOOKUP]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP]
fs[miscTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[miscTheory.the_def]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[miscTheory.the_def] )
\\ fs[miscTheory.the_def]
\\ fs[fsupdate_def,miscTheory.the_def,AFUPDKEY_ALOOKUP]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP]
>- ( rw[AFUPDKEY_o,o_DEF,PAIR_MAP] )
\\ CASE_TAC \\ fs[libTheory.the_def]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[libTheory.the_def,AFUPDKEY_comm]
\\ CASE_TAC \\ fs[miscTheory.the_def]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[miscTheory.the_def,AFUPDKEY_comm]
\\ metis_tac[STD_streams_def,SOME_11,PAIR,FST,SND]
QED

Expand All @@ -552,22 +552,22 @@ Theorem up_stderr_fastForwardFD:
Proof
rw[fastForwardFD_def,up_stdo_def]
\\ Cases_on`ALOOKUP fs.infds fd` >- (
fs[libTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[libTheory.the_def]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP] )
fs[miscTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[miscTheory.the_def]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP] )
\\ fs[] \\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` >- (
fs[libTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[libTheory.the_def]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[libTheory.the_def] )
\\ fs[libTheory.the_def]
\\ fs[fsupdate_def,libTheory.the_def,AFUPDKEY_ALOOKUP]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP]
fs[miscTheory.the_def,fsupdate_def]
\\ CASE_TAC \\ fs[miscTheory.the_def]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[miscTheory.the_def] )
\\ fs[miscTheory.the_def]
\\ fs[fsupdate_def,miscTheory.the_def,AFUPDKEY_ALOOKUP]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP]
>- ( rw[AFUPDKEY_o,o_DEF,PAIR_MAP] )
\\ CASE_TAC \\ fs[libTheory.the_def]
\\ CASE_TAC \\ fs[libTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[libTheory.the_def,AFUPDKEY_comm]
\\ CASE_TAC \\ fs[miscTheory.the_def]
\\ CASE_TAC \\ fs[miscTheory.the_def,AFUPDKEY_ALOOKUP]
\\ rw[miscTheory.the_def,AFUPDKEY_comm]
\\ metis_tac[STD_streams_def,SOME_11,PAIR,FST,SND]
QED

Expand All @@ -582,9 +582,9 @@ Theorem stdo_fastForwardFD:
fd ≠ fd' ⇒ (stdo fd' nm (fastForwardFD fs fd) out ⇔ stdo fd' nm fs out)
Proof
rw[stdo_def,fastForwardFD_def,AFUPDKEY_ALOOKUP]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ fs[AFUPDKEY_ALOOKUP] \\ rw[]
\\ CASE_TAC
QED
Expand Down Expand Up @@ -5872,7 +5872,7 @@ Proof
\\ `fs' = fs` suffices_by ( rw[std_preludeTheory.OPTION_TYPE_def] \\ xsimpl)
\\ unabbrev_all_tac
\\ simp[fastForwardFD_def,ADELKEY_AFUPDKEY,o_DEF,
libTheory.the_def, openFileFS_numchars,openFileFS_files,
miscTheory.the_def, openFileFS_numchars,openFileFS_files,
IO_fs_component_equality,openFileFS_inode_tbl]
QED

Expand Down Expand Up @@ -6774,7 +6774,7 @@ Proof
rw[forwardFD_def,fastForwardFD_def,get_file_content_def]
\\ PairCases_on ‘x'’
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF]
\\ gs[] \\ simp[miscTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF]
\\ simp[IO_fs_component_equality] \\ irule AFUPDKEY_eq
\\ rw[] \\ simp[MAX_DEF]
QED
Expand All @@ -6784,10 +6784,10 @@ Theorem fastForwardFD_same_infds[local]:
Proof
rw[fastForwardFD_def]
\\ Cases_on ‘ALOOKUP fs.infds n’
\\ simp[libTheory.the_def]
\\ simp[miscTheory.the_def]
\\ PairCases_on ‘x’ \\ simp[]
\\ Cases_on ‘ALOOKUP fs.inode_tbl x0’
\\ simp[libTheory.the_def]
\\ simp[miscTheory.the_def]
QED

Theorem INSTREAM_STR_fastForwardFD:
Expand All @@ -6805,13 +6805,13 @@ Proof
\\ rename [‘ALOOKUP fs.infds fd = SOME zz’]
\\ PairCases_on ‘zz’
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF])
\\ gs[] \\ simp[miscTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF])
\\ conj_tac
>- (gs[get_mode_def,fastForwardFD_def,get_file_content_def]
\\ rename [‘ALOOKUP fs.infds fd = SOME zz’]
\\ PairCases_on ‘zz’
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP])
\\ gs[] \\ simp[miscTheory.the_def,AFUPDKEY_ALOOKUP])
\\ xsimpl \\ simp[fastForwardFD_eq_forwardFD] \\ xsimpl
QED

Expand Down Expand Up @@ -7951,12 +7951,12 @@ Proof
>- (qexists_tac ‘c’ \\ gs[get_file_content_def,fastForwardFD_def]
\\ PairCases_on ‘x'’
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF])
\\ gs[] \\ simp[miscTheory.the_def,AFUPDKEY_ALOOKUP,MAX_DEF])
\\ conj_tac
>- (gs[get_mode_def,fastForwardFD_def,get_file_content_def]
\\ PairCases_on ‘x'’
\\ qmatch_assum_rename_tac ‘ALOOKUP _ _ = SOME (ino,mode,off')’
\\ gs[] \\ simp[libTheory.the_def,AFUPDKEY_ALOOKUP])
\\ gs[] \\ simp[miscTheory.the_def,AFUPDKEY_ALOOKUP])
\\ xsimpl \\ simp[fastForwardFD_eq_forwardFD] \\ xsimpl
QED

Expand Down
74 changes: 37 additions & 37 deletions basis/fsFFIPropsScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -456,19 +456,19 @@ Theorem validFD_fastForwardFD[simp]:
validFD fd (fastForwardFD fs fd) = validFD fd fs
Proof
rw[validFD_def,fastForwardFD_def,bumpFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ rw[OPTION_GUARD_COND,libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ rw[OPTION_GUARD_COND,miscTheory.the_def]
QED

Theorem validFileFD_fastForwardFD[simp]:
validFileFD fd (fastForwardFD fs x).infds ⇔ validFileFD fd fs.infds
Proof
rw[validFileFD_def, fastForwardFD_def]
\\ Cases_on`ALOOKUP fs.infds x` \\ rw[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds x` \\ rw[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ simp[AFUPDKEY_ALOOKUP]
\\ TOP_CASE_TAC \\ simp[]
\\ rw[PAIR_MAP, FST_EQ_EQUIV, PULL_EXISTS, SND_EQ_EQUIV]
Expand All @@ -479,39 +479,39 @@ Theorem fastForwardFD_inode_tbl[simp]:
(fastForwardFD fs fd).inode_tbl = fs.inode_tbl
Proof
EVAL_TAC
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ rw[OPTION_GUARD_COND,libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ rw[OPTION_GUARD_COND,miscTheory.the_def]
QED

Theorem fastForwardFD_files[simp]:
!fs fd. (fastForwardFD fs fd).files = fs.files
Proof
rw[fastForwardFD_def] >>
Cases_on`ALOOKUP fs.infds fd` >> fs[libTheory.the_def] >>
Cases_on`ALOOKUP fs.infds fd` >> fs[miscTheory.the_def] >>
pairarg_tac >> fs[] >>
Cases_on`ALOOKUP fs.inode_tbl ino` >> fs[libTheory.the_def]
Cases_on`ALOOKUP fs.inode_tbl ino` >> fs[miscTheory.the_def]
QED

Theorem ADELKEY_fastForwardFD_elim[simp]:
ADELKEY fd (fastForwardFD fs fd).infds = ADELKEY fd fs.infds
Proof
rw[fastForwardFD_def,bumpFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ rw[OPTION_GUARD_COND,libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ rw[OPTION_GUARD_COND,miscTheory.the_def]
QED

Theorem fastForwardFD_ADELKEY_same[simp]:
fastForwardFD fs fd with infds updated_by ADELKEY fd =
fs with infds updated_by ADELKEY fd
Proof
rw[fastForwardFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ pairarg_tac \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[miscTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ fs[IO_fs_component_equality,ADELKEY_unchanged]
QED

Expand All @@ -520,9 +520,9 @@ Theorem fastForwardFD_0:
fastForwardFD fs fd = fs
Proof
rw[fastForwardFD_def,get_file_content_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ fs[IO_fs_component_equality]
\\ match_mp_tac AFUPDKEY_unchanged
\\ rw[] \\ rw[PAIR_MAP_THM]
Expand All @@ -533,36 +533,36 @@ Theorem fastForwardFD_with_numchars:
fastForwardFD (fs with numchars := ns) fd = fastForwardFD fs fd with numchars := ns
Proof
rw[fastForwardFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ simp[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ simp[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ simp[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ simp[miscTheory.the_def]
QED

Theorem fastForwardFD_numchars[simp]:
(fastForwardFD fs fd).numchars = fs.numchars
Proof
rw[fastForwardFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ simp[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ simp[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ simp[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ simp[miscTheory.the_def]
QED

Theorem fastForwardFD_maxFD[simp]:
(fastForwardFD fs fd).maxFD = fs.maxFD
Proof
rw[fastForwardFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ simp[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ simp[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ simp[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ simp[miscTheory.the_def]
QED

Theorem wfFS_fastForwardFD[simp]:
!fs fd. validFD fd fs /\ wfFS fs ==> wfFS (fastForwardFD fs fd)
Proof
rw[wfFS_def,fastForwardFD_def,validFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ rw[]
>-(res_tac \\ simp[AFUPDKEY_ALOOKUP] \\ CASE_TAC \\ fs[])
>-(fs[consistentFS_def] \\ rw[] \\ res_tac)
Expand Down Expand Up @@ -975,7 +975,7 @@ Proof
rw[fastForwardFD_def,get_file_content_def,forwardFD_def,AFUPDKEY_ALOOKUP]
\\ rw[]
\\ pairarg_tac \\ fs[]
\\ pairarg_tac \\ fs[libTheory.the_def]
\\ pairarg_tac \\ fs[miscTheory.the_def]
\\ fs[IO_fs_component_equality,AFUPDKEY_o]
\\ match_mp_tac AFUPDKEY_eq
\\ simp[MAX_DEF]
Expand Down Expand Up @@ -1108,13 +1108,13 @@ Theorem fastForwardFD_lineForwardFD[simp]:
fastForwardFD (lineForwardFD fs fd) fd = fastForwardFD fs fd
Proof
rw[fastForwardFD_def,lineForwardFD_def]
\\ TOP_CASE_TAC \\ fs[libTheory.the_def]
\\ TOP_CASE_TAC \\ fs[libTheory.the_def]
\\ TOP_CASE_TAC \\ fs[libTheory.the_def]
\\ TOP_CASE_TAC \\ fs[miscTheory.the_def]
\\ TOP_CASE_TAC \\ fs[miscTheory.the_def]
\\ TOP_CASE_TAC \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ fs[forwardFD_def,AFUPDKEY_ALOOKUP,get_file_content_def]
\\ pairarg_tac \\ fs[]
\\ pairarg_tac \\ fs[libTheory.the_def]
\\ pairarg_tac \\ fs[miscTheory.the_def]
\\ fs[IO_fs_component_equality,AFUPDKEY_o]
\\ match_mp_tac AFUPDKEY_eq
\\ simp[] \\ rveq
Expand All @@ -1140,14 +1140,14 @@ Theorem lineFD_NONE_lineForwardFD_fastForwardFD:
lineForwardFD fs fd = fastForwardFD fs fd
Proof
rw[lineFD_def,lineForwardFD_def,fastForwardFD_def,get_file_content_def]
\\ fs[libTheory.the_def]
\\ pairarg_tac \\ fs[libTheory.the_def]
\\ rveq \\ fs[libTheory.the_def]
\\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[miscTheory.the_def]
\\ rveq \\ fs[miscTheory.the_def]
\\ rw[] \\ TRY (
simp[IO_fs_component_equality]
\\ match_mp_tac (GSYM AFUPDKEY_unchanged)
\\ simp[MAX_DEF] )
\\ rw[] \\ fs[forwardFD_def,libTheory.the_def]
\\ rw[] \\ fs[forwardFD_def,miscTheory.the_def]
\\ pairarg_tac \\ fs[]
QED

Expand Down Expand Up @@ -1382,9 +1382,9 @@ Theorem STD_streams_fastForwardFD:
(STD_streams (fastForwardFD fs fd) ⇔ STD_streams fs)
Proof
rw[fastForwardFD_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.infds fd` \\ fs[miscTheory.the_def]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[miscTheory.the_def]
\\ EQ_TAC \\ rw[STD_streams_def,option_case_eq,AFUPDKEY_ALOOKUP,PAIR_MAP] \\ rw[]
>- (
qmatch_assum_rename_tac`ALOOKUP _ ino = SOME r` \\
Expand Down
2 changes: 1 addition & 1 deletion candle/overloading/ml_checker/ml_cyclicityCheckerProgScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
An I/O shim for the verified cyclicity checker
*)
open preamble ml_translatorTheory ml_translatorLib ml_pmatchTheory patternMatchesTheory
open astTheory libTheory evaluateTheory semanticPrimitivesTheory
open astTheory evaluateTheory semanticPrimitivesTheory
open ml_progLib ml_progTheory evaluateTheory
open set_sepTheory cfTheory cfStoreTheory cfTacticsLib Satisfy
open cfHeapsBaseTheory basisFunctionsLib
Expand Down
2 changes: 1 addition & 1 deletion candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
HOL functions.
*)
open preamble ml_translatorTheory ml_translatorLib ml_pmatchTheory patternMatchesTheory
open astTheory libTheory evaluateTheory semanticPrimitivesTheory
open astTheory evaluateTheory semanticPrimitivesTheory
open ml_progLib ml_progTheory evaluateTheory
open set_sepTheory cfTheory cfStoreTheory cfTacticsLib Satisfy
open cfHeapsBaseTheory basisFunctionsLib
Expand Down
2 changes: 1 addition & 1 deletion candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
connection between the generated code and the input HOL functions.
*)
open preamble ml_translatorTheory ml_translatorLib ml_pmatchTheory patternMatchesTheory
open astTheory libTheory evaluateTheory semanticPrimitivesTheory
open astTheory evaluateTheory semanticPrimitivesTheory
open ml_progLib ml_progTheory evaluateTheory
open set_sepTheory cfTheory cfStoreTheory cfTacticsLib Satisfy
open cfHeapsBaseTheory basisFunctionsLib
Expand Down
2 changes: 1 addition & 1 deletion characteristic/cfScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2090,7 +2090,7 @@ val cf_strip_sound_tac =

val cf_evaluate_step_tac =
simp [evaluate_to_heap_def, evaluate_ck_def, evaluate_def] \\
fs [libTheory.opt_bind_def, PULL_EXISTS]
fs [miscTheory.opt_bind_def, PULL_EXISTS]

val cf_strip_sound_full_tac = cf_strip_sound_tac \\ cf_evaluate_step_tac

Expand Down
2 changes: 1 addition & 1 deletion compiler/backend/ag32/proofs/ag32_configProofScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ Theorem compile_imp_ffi_names:
c1.lab_conf.ffi_names = SOME (MAP ExtCall f)
Proof
Cases_on ‘c1.lab_conf.ffi_names’
\\ gvs [libTheory.the_def,backendTheory.ffinames_to_string_list_def]
\\ gvs [miscTheory.the_def,backendTheory.ffinames_to_string_list_def]
\\ gvs [backendTheory.compile_def]
\\ rpt (pairarg_tac \\ gvs [])
\\ gvs [oneline backendTheory.attach_bitmaps_def, AllCaseEqs()]
Expand Down
2 changes: 1 addition & 1 deletion compiler/backend/flat_uncheck_ctorsScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ open preamble astTheory flatLangTheory;
val _ = numLib.temp_prefer_num();

val _ = new_theory "flat_uncheck_ctors";
val _ = set_grammar_ancestry ["flatLang", "lib"];
val _ = set_grammar_ancestry ["flatLang", "misc"];
val _ = temp_tight_equality ();

Definition compile_pat_def:
Expand Down
Loading