diff options
Diffstat (limited to 'snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy')
| -rw-r--r-- | snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy b/snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy new file mode 100644 index 00000000..d6ca4d7d --- /dev/null +++ b/snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy @@ -0,0 +1,48 @@ +theory Riscv_duopod_lemmas + imports + Sail.Sail_values_lemmas + Sail.State_lemmas + Riscv_duopod +begin + +abbreviation "liftS \<equiv> liftState (get_regval, set_regval)" + +lemmas register_defs = get_regval_def set_regval_def Xs_ref_def nextPC_ref_def PC_ref_def + +lemma regval_vector_64_dec_bit[simp]: + "vector_64_dec_bit_of_regval (regval_of_vector_64_dec_bit v) = Some v" + by (auto simp: regval_of_vector_64_dec_bit_def) + +lemma vector_of_rv_rv_of_vector[simp]: + assumes "\<And>v. of_rv (rv_of v) = Some v" + shows "vector_of_regval of_rv (regval_of_vector rv_of len is_inc v) = Some v" +proof - + from assms have "of_rv \<circ> rv_of = Some" by auto + then show ?thesis by (auto simp: vector_of_regval_def regval_of_vector_def) +qed + +lemma liftS_read_reg_Xs[simp]: + "liftS (read_reg Xs_ref) = readS (Xs \<circ> regstate)" + by (auto simp: liftState_read_reg_readS register_defs) + +lemma liftS_write_reg_Xs[simp]: + "liftS (write_reg Xs_ref v) = updateS (regstate_update (Xs_update (\<lambda>_. v)))" + by (auto simp: liftState_write_reg_updateS register_defs) + +lemma liftS_read_reg_nextPC[simp]: + "liftS (read_reg nextPC_ref) = readS (nextPC \<circ> regstate)" + by (auto simp: liftState_read_reg_readS register_defs) + +lemma liftS_write_reg_nextPC[simp]: + "liftS (write_reg nextPC_ref v) = updateS (regstate_update (nextPC_update (\<lambda>_. v)))" + by (auto simp: liftState_write_reg_updateS register_defs) + +lemma liftS_read_reg_PC[simp]: + "liftS (read_reg PC_ref) = readS (PC \<circ> regstate)" + by (auto simp: liftState_read_reg_readS register_defs) + +lemma liftS_write_reg_PC[simp]: + "liftS (write_reg PC_ref v) = updateS (regstate_update (PC_update (\<lambda>_. v)))" + by (auto simp: liftState_write_reg_updateS register_defs) + +end |