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, 0 insertions, 48 deletions
diff --git a/snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy b/snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy deleted file mode 100644 index d6ca4d7d..00000000 --- a/snapshots/isabelle/riscv/Riscv_duopod_lemmas.thy +++ /dev/null @@ -1,48 +0,0 @@ -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 |