From 48a421d7a393f35b150221d8dec6d3caca9befe6 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sat, 10 Feb 2024 21:47:42 +0100 Subject: [PATCH] Make bvl/bvi/dataLang have ref definition separate from closLang --- .../backend/proofs/bvl_inlineProofScript.sml | 2 +- .../backend/proofs/clos_to_bvlProofScript.sml | 19 +++++++++-- .../proofs/data_to_word_assignProofScript.sml | 4 ++- .../proofs/data_to_word_memoryProofScript.sml | 2 ++ compiler/backend/semantics/bviSemScript.sml | 1 + compiler/backend/semantics/bvlPropsScript.sml | 11 ++++--- compiler/backend/semantics/bvlSemScript.sml | 20 +++++++++--- .../backend/semantics/dataPropsScript.sml | 32 +++++++++---------- compiler/backend/semantics/dataSemScript.sml | 6 ++-- 9 files changed, 66 insertions(+), 31 deletions(-) diff --git a/compiler/backend/proofs/bvl_inlineProofScript.sml b/compiler/backend/proofs/bvl_inlineProofScript.sml index 577ab661ec..63b6177775 100644 --- a/compiler/backend/proofs/bvl_inlineProofScript.sml +++ b/compiler/backend/proofs/bvl_inlineProofScript.sml @@ -1924,7 +1924,7 @@ Theorem state_cc_compile_inc_eq: (in_cc limit (remove_ticks_cc (let_op_cc o1 o2 cc))) Proof fs [state_cc_def,compile_inc_def,in_cc_def,FUN_EQ_THM,remove_ticks_cc_def, - let_op_cc_def] \\ rw [] + let_op_cc_def,FORALL_PROD] \\ rw [] \\ rpt (pairarg_tac \\ fs []) \\ rveq \\ fs [MAP_optimise] QED diff --git a/compiler/backend/proofs/clos_to_bvlProofScript.sml b/compiler/backend/proofs/clos_to_bvlProofScript.sml index 228dc96dab..23a6df19fa 100644 --- a/compiler/backend/proofs/clos_to_bvlProofScript.sml +++ b/compiler/backend/proofs/clos_to_bvlProofScript.sml @@ -1022,6 +1022,19 @@ val compile_oracle_inv_def = Define` ^dummy_compile_oracle_inv max_app s_code s_cc s_co t_code t_cc t_co ⇔ T`; *) +val ref_rel_def = Define` + (ref_rel R (closSem$ValueArray vs) (bvlSem$ValueArray ws) ⇔ LIST_REL R vs ws) ∧ + (ref_rel R (ByteArray f as) (ByteArray g bs) ⇔ f = g ∧ as = bs) ∧ + (ref_rel _ _ _ = F)` +val _ = export_rewrites["ref_rel_def"]; + +Theorem ref_rel_simp[simp]: + (ref_rel R (ValueArray vs) y ⇔ ∃ws. y = ValueArray ws ∧ LIST_REL R vs ws) ∧ + (ref_rel R (ByteArray f bs) y ⇔ y = ByteArray f bs) +Proof + Cases_on`y`>>simp[ref_rel_def] >> srw_tac[][EQ_IMP_THM] +QED + val state_rel_def = Define ` state_rel f (s:('c,'ffi) closSem$state) (t:('c,'ffi) bvlSem$state) <=> (s.ffi = t.ffi) /\ @@ -3860,7 +3873,7 @@ Proof full_simp_tac(srw_ss())[SUBMAP_DEF,FAPPLY_FUPDATE_THM,FDIFF_def,DRESTRICT_DEF] >> srw_tac[][] >> METIS_TAC[]) \\ Cases_on `op = Update` \\ full_simp_tac(srw_ss())[] THEN1 (full_simp_tac(srw_ss())[closSemTheory.do_app_def,bvlSemTheory.do_app_def] - \\ fs[case_eq_thms,bool_case_eq] \\ rveq + \\ fs[case_eq_thms,bool_case_eq,AllCaseEqs()] \\ rveq \\ fs[SWAP_REVERSE_SYM] \\ rveq \\ fs[v_rel_SIMP] \\ rveq \\ fs[SWAP_REVERSE,PULL_EXISTS] @@ -4073,7 +4086,7 @@ Proof simp[Abbr`pp`,LEAST_NOTIN_FDOM]) \\ Cases_on `op = UpdateByte` \\ full_simp_tac(srw_ss())[] THEN1 ( full_simp_tac(srw_ss())[closSemTheory.do_app_def,bvlSemTheory.do_app_def] - \\ fs[case_eq_thms,PULL_EXISTS,bool_case_eq] + \\ fs[case_eq_thms,PULL_EXISTS,bool_case_eq,AllCaseEqs()] \\ rw[] \\ fs[SWAP_REVERSE_SYM] \\ rw[] \\ fs[v_rel_SIMP] \\ rw[] \\ imp_res_tac evaluate_const @@ -4297,7 +4310,7 @@ Proof \\ Cases_on`∃fl. op = CopyByte fl` \\ fs[] >- ( fs[closSemTheory.do_app_def,bvlSemTheory.do_app_def,PULL_EXISTS] \\ Cases_on`fl` - \\ fs[case_eq_thms,v_case_eq_thms,PULL_EXISTS,SWAP_REVERSE_SYM] + \\ fs[case_eq_thms,v_case_eq_thms,PULL_EXISTS,SWAP_REVERSE_SYM,AllCaseEqs()] \\ rveq \\ fs[v_rel_SIMP] \\ rw[] \\ fs[FLOOKUP_UPDATE] \\ rw[] \\ TRY (drule (GEN_ALL state_rel_refs_lookup) \\ disch_then imp_res_tac \\ fs[FLOOKUP_UPDATE]) \\ TRY ( diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml index 07eba0ca66..49a72b330d 100644 --- a/compiler/backend/proofs/data_to_word_assignProofScript.sml +++ b/compiler/backend/proofs/data_to_word_assignProofScript.sml @@ -1958,7 +1958,7 @@ Theorem do_app_aux_safe_for_space_mono: (do_app_aux op xs s = Rval (r,s1)) /\ s1.safe_for_space ==> s.safe_for_space Proof Cases_on `op` \\ - fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, + fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,AllCaseEqs(), bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_space_def, with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,check_lim_def, @@ -13573,6 +13573,8 @@ Proof \\ gvs [good_dimindex_def,dimword_def] QED +val _ = Parse.hide "free"; + Theorem assign_Build: (∃parts. op = Build parts) ==> ^assign_thm_goal Proof[exclude_simps = EXP_LE_LOG_SIMP EXP_LT_LOG_SIMP LE_EXP_LOG_SIMP diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml index ec0c8874c5..a3fd32e269 100644 --- a/compiler/backend/proofs/data_to_word_memoryProofScript.sml +++ b/compiler/backend/proofs/data_to_word_memoryProofScript.sml @@ -12631,6 +12631,8 @@ Proof \\ imp_res_tac SUBSET_FINITE_I QED +val _ = Parse.hide "free"; + Theorem memory_rel_do_build: ∀parts i st free curr sp map0 map0' refs ts refs1 v m v ws. do_build map0 i parts refs (SOME ts) = (v,refs1,SOME ts1) ∧ diff --git a/compiler/backend/semantics/bviSemScript.sml b/compiler/backend/semantics/bviSemScript.sml index 17a228c127..c9395a9e39 100644 --- a/compiler/backend/semantics/bviSemScript.sml +++ b/compiler/backend/semantics/bviSemScript.sml @@ -3,6 +3,7 @@ *) open preamble bviTheory; local open backend_commonTheory bvlSemTheory in end; +local open backendPropsTheory in end; val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"] diff --git a/compiler/backend/semantics/bvlPropsScript.sml b/compiler/backend/semantics/bvlPropsScript.sml index f764b3efa6..08b98dedcc 100644 --- a/compiler/backend/semantics/bvlPropsScript.sml +++ b/compiler/backend/semantics/bvlPropsScript.sml @@ -2,7 +2,7 @@ Properties about BVL and its semantics *) open preamble bvlTheory bvlSemTheory bvl_constTheory; -open closPropsTheory backend_commonTheory; +open backend_commonTheory; val _ = temp_delsimps ["NORMEQ_CONV"] @@ -31,9 +31,12 @@ Proof QED fun get_thms ty = { case_def = TypeBase.case_def_of ty, nchotomy = TypeBase.nchotomy_of ty } -val case_eq_thms = LIST_CONJ (closSemTheory.case_eq_thms:: - map (prove_case_eq_thm o get_thms) - [``:v``,``:'a ffi_result``]) +val case_eq_thms = LIST_CONJ + (CaseEq "eq_result" :: CaseEq "const_part" :: CaseEq "word_size" :: + CaseEq "result" :: CaseEq "error_result" :: + map (prove_case_eq_thm o get_thms) + [``:v``,``:'a ref``,``:'a option``,``:'a list``,``:'a + 'b``, + ``:closLang$op``,``:'a ffi_result``]) val case_eq_thms = CONJ bool_case_eq (CONJ pair_case_eq case_eq_thms) val _ = save_thm ("case_eq_thms", case_eq_thms); diff --git a/compiler/backend/semantics/bvlSemScript.sml b/compiler/backend/semantics/bvlSemScript.sml index 1691311adc..a913cd5c50 100644 --- a/compiler/backend/semantics/bvlSemScript.sml +++ b/compiler/backend/semantics/bvlSemScript.sml @@ -3,6 +3,7 @@ *) open preamble bvlTheory closSemTheory open clos_to_bvlTheory (* for closure_tag and num_added_globals *) +local open backendPropsTheory in end; val _ = new_theory"bvlSem" @@ -10,16 +11,26 @@ val _ = Parse.hide "str"; (* --- Semantics of BVL --- *) +Datatype: + ref = ValueArray ('a list) + | ByteArray bool (word8 list) + (* T = compare-by-contents, immutable + F = compare-by-pointer, mutable *) + (* in closLang all are ByteArray F, + ByteArray T introduced in BVL to implement ByteVector *) +End + (* these parts are shared by bytecode and, if bytecode is to be supported, need to move to a common ancestor *) -val _ = Datatype ` +Datatype: v = Number int (* integer *) | Word64 word64 | Block num (v list) (* cons block: tag and payload *) | CodePtr num (* code pointer *) - | RefPtr num (* pointer to ref cell *)`; + | RefPtr num (* pointer to ref cell *) +End val Boolv_def = Define` Boolv b = bvlSem$Block (bool_to_tag b) []` @@ -29,7 +40,7 @@ val Unit_def = Define` (* -- *) -val _ = Datatype ` +Datatype: state = <| globals : (bvlSem$v option) list ; refs : num |-> bvlSem$v ref @@ -37,7 +48,8 @@ val _ = Datatype ` ; compile : 'c -> (num # num # bvl$exp) list -> (word8 list # word64 list # 'c) option ; compile_oracle : num -> 'c # (num # num # bvl$exp) list ; code : (num # bvl$exp) num_map - ; ffi : 'ffi ffi_state |> ` + ; ffi : 'ffi ffi_state |> +End val v_to_list_def = Define` (v_to_list (Block tag []) = diff --git a/compiler/backend/semantics/dataPropsScript.sml b/compiler/backend/semantics/dataPropsScript.sml index 61153a092a..3bfe0d4d37 100644 --- a/compiler/backend/semantics/dataPropsScript.sml +++ b/compiler/backend/semantics/dataPropsScript.sml @@ -211,7 +211,7 @@ val do_app_with_stack = time Q.prove( \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def] >> @@ -234,7 +234,7 @@ val do_app_with_stack_and_locals = time Q.prove( \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def] >> @@ -252,7 +252,7 @@ Proof \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,check_lim_def] >> @@ -268,7 +268,7 @@ Proof \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,check_lim_def] >> @@ -288,7 +288,7 @@ val do_app_with_locals = time Q.prove( \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,check_lim_def] >> @@ -432,7 +432,7 @@ val do_app_swap_tac = , MAX_DEF , check_lim_def] \\ TRY (pairarg_tac \\ fs []) - \\ TRY (fs [list_case_eq,option_case_eq,v_case_eq,bool_case_eq,closSemTheory.ref_case_eq + \\ TRY (fs [list_case_eq,option_case_eq,v_case_eq,bool_case_eq,bvlSemTheory.ref_case_eq , ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, state_component_equality , semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,pair_case_eq , limits_component_equality,stack_consumed_def] @@ -611,7 +611,7 @@ val full_fs = fs[ get_var_def, set_var_def val full_cases = fs [ list_case_eq,option_case_eq , v_case_eq , bool_case_eq - , closSemTheory.ref_case_eq + , bvlSemTheory.ref_case_eq , ffiTheory.ffi_result_case_eq , ffiTheory.oracle_result_case_eq , semanticPrimitivesTheory.eq_result_case_eq @@ -1622,7 +1622,7 @@ Proof Cases_on `op` >> TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) >> ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,stack_consumed_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,space_consumed_with_clock, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,space_consumed_with_clock, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,size_of_heap_with_clock,check_lim_def] >> @@ -1642,7 +1642,7 @@ Proof Cases_on `op` >> TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) >> ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,stack_consumed_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,space_consumed_with_clock, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,space_consumed_with_clock, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,size_of_heap_with_clock,check_lim_def] >> @@ -1662,7 +1662,7 @@ Proof Cases_on `op` >> TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) >> ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def, - with_fresh_ts_def,closSemTheory.ref_case_eq, + with_fresh_ts_def,bvlSemTheory.ref_case_eq, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,check_lim_def] >> @@ -1700,7 +1700,7 @@ Proof \\ srw_tac[][] >> fs[]) >- (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,cut_state_opt_def,cut_state_def , bool_case_eq,ffiTheory.call_FFI_def,semanticPrimitivesTheory.result_case_eq - , with_fresh_ts_def,closSemTheory.ref_case_eq + , with_fresh_ts_def,bvlSemTheory.ref_case_eq , ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq , semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq , pair_case_eq,consume_space_def] @@ -1786,7 +1786,7 @@ Proof Cases_on `x` >> TRY (rename [‘EqualConst cc’] >> Cases_on ‘cc’) >> ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def, - with_fresh_ts_def,closSemTheory.ref_case_eq, + with_fresh_ts_def,bvlSemTheory.ref_case_eq, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,check_lim_def] >> @@ -2004,7 +2004,7 @@ Proof Cases_on `op` \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,check_lim_def, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,op_space_reset_def,data_spaceTheory.op_space_req_def] @@ -2553,7 +2553,7 @@ Proof ntac 2( fs[do_app_aux_def,cc_co_only_diff_def,do_app_def,do_stack_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,stack_consumed_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,stack_consumed_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,space_consumed_def, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def, @@ -2592,7 +2592,7 @@ Proof Cases_on ‘op’ \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ fs [] >> fs[do_app_aux_def,cc_co_only_diff_def,do_app_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def, @@ -2771,7 +2771,7 @@ Proof Cases_on ‘op’ \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ fs [] >> fs[do_app_aux_def,cc_co_only_diff_def,do_app_def,do_stack_def,list_case_eq,option_case_eq,v_case_eq, bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def, - with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def, + with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def, ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq, pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def, diff --git a/compiler/backend/semantics/dataSemScript.sml b/compiler/backend/semantics/dataSemScript.sml index 3082239839..c6295a0f1b 100644 --- a/compiler/backend/semantics/dataSemScript.sml +++ b/compiler/backend/semantics/dataSemScript.sml @@ -1,8 +1,10 @@ (* The formal semantics of dataLang *) -open preamble data_simpTheory data_liveTheory data_spaceTheory dataLangTheory closSemTheory +open preamble data_simpTheory data_liveTheory data_spaceTheory + dataLangTheory bvlSemTheory data_to_wordTheory (* TODO: immoral, semantics shouldn't depend on compiler *); +local open backendPropsTheory in end; val _ = new_theory"dataSem"; @@ -1249,7 +1251,7 @@ val list_thms = { nchotomy = list_nchotomy, case_def = list_case_def }; val option_thms = { nchotomy = option_nchotomy, case_def = option_case_def }; val op_thms = { nchotomy = closLangTheory.op_nchotomy, case_def = closLangTheory.op_case_def }; val v_thms = { nchotomy = theorem"v_nchotomy", case_def = definition"v_case_def" }; -val ref_thms = { nchotomy = closSemTheory.ref_nchotomy, case_def = closSemTheory.ref_case_def }; +val ref_thms = { nchotomy = bvlSemTheory.ref_nchotomy, case_def = bvlSemTheory.ref_case_def }; val ffi_result_thms = { nchotomy = ffiTheory.ffi_result_nchotomy, case_def = ffiTheory.ffi_result_case_def }; val word_size_thms = { nchotomy = astTheory.word_size_nchotomy, case_def = astTheory.word_size_case_def }; val eq_result_thms = { nchotomy = semanticPrimitivesTheory.eq_result_nchotomy, case_def = semanticPrimitivesTheory.eq_result_case_def };