Update Isabelle snapshots

Except RISC-V duopod, which doesn't seem to build for me at the moment

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