adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

isabelle-2021: update CamkesCdlRefine 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-09-16 16:37:43 +10:00 committed by Gerwin Klein
parent 997adaf9f3
commit d92b4dcadb
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
camkes/cdl-refine/Eval_CAMKES_CDL.thy
View File

@ -529,13 +529,15 @@ lemma bintrunc_1_1:
lemmas word_rel_simps_small =
order_refl (* shortcut *)
rel_simps simp_thms
word_less_alt word_le_def word_uint_eq_iff uint_eq_0 uint_1
word_less_alt word_le_def word_uint_eq_iff uint_0_eq uint_1
(* need bintrunc to reduce numerals mod word size *)
uint_bintrunc bintrunc_numeral_simps bintrunc_1_1
numeral_One BIT_bin_simps BIT_special_simps
(* evaluating word size for bintrunc -- yuck *)
len_num0 len_num1 len_bit0 len_bit1
arith_simps mult_1_right pred_numeral_simps numeral_plus_one
arith_special
(* test for simpset *)
ML \<open>
@ -581,10 +583,11 @@ lemma pow_2_numeral:
(* needed to evaluate "ptr + 2^sz" expressions *)
lemmas word_pow_arith_simps =
pow_2_numeral uint_word_arith_bintrs
uint_eq_0 uint_1 uint_bintrunc bintrunc_Sucs numeral_One
uint_0_eq uint_1 uint_bintrunc bintrunc_Suc_numeral numeral_One
arith_simps arith_special
nat_0 nat_one_as_int[symmetric] nat_numeral nat_numeral_diff_1 mult_1_right
lemmas object_slots_eval_simps
[simplified fun_upds_to_map_of] = (* NB: convert Map.empty for FP_Eval compatibility *)
object_slots_def cdl_object.case