Update RISC-V snapshot

2 files changed, 17 insertions, 1 deletions

diff --git a/snapshots/isabelle/riscv/Riscv_lemmas.thy b/snapshots/isabelle/riscv/Riscv_lemmas.thy
index b2f4e80d..108208ca 100644
--- a/snapshots/isabelle/riscv/Riscv_lemmas.thy
+++ b/snapshots/isabelle/riscv/Riscv_lemmas.thy
@@ -67,6 +67,19 @@ proof -
   then show ?thesis by (auto simp: vector_of_regval_def regval_of_vector_def)
 qed
 
+lemma option_of_rv_rv_of_option[simp]:
+  assumes "\<And>v. of_rv (rv_of v) = Some v"
+  shows "option_of_regval of_rv (regval_of_option rv_of v) = Some v"
+  using assms by (cases v) (auto simp: option_of_regval_def regval_of_option_def)
+
+lemma list_of_rv_rv_of_list[simp]:
+  assumes "\<And>v. of_rv (rv_of v) = Some v"
+  shows "list_of_regval of_rv (regval_of_list rv_of v) = Some v"
+proof -
+  from assms have "of_rv \<circ> rv_of = Some" by auto
+  with assms show ?thesis by (induction v) (auto simp: list_of_regval_def regval_of_list_def)
+qed
+
 lemma liftS_read_reg_tlb39[simp]:
   "liftS (read_reg tlb39_ref) = readS (tlb39 \<circ> regstate)"
   by (auto simp: liftState_read_reg_readS register_defs)
diff --git a/snapshots/isabelle/riscv/Riscv_types.thy b/snapshots/isabelle/riscv/Riscv_types.thy
index b4fc7f6c..71dce180 100644
--- a/snapshots/isabelle/riscv/Riscv_types.thy
+++ b/snapshots/isabelle/riscv/Riscv_types.thy
@@ -636,7 +636,10 @@ definition regval_of_list  :: "('a \<Rightarrow> register_value)\<Rightarrow> 'a
 (*val option_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (maybe 'a)*)
 definition option_of_regval  :: "(register_value \<Rightarrow> 'a option)\<Rightarrow> register_value \<Rightarrow>('a option)option "  where 
      " option_of_regval of_regval1 = ( \<lambda>x .  
-  (case  x of   Regval_option v => map_option of_regval1 v | _ => None ) )"
+  (case  x of
+        Regval_option v => Some (Option.bind v of_regval1)
+    | _ => None
+  ) )"
 
 
 (*val regval_of_option : forall 'a. ('a -> register_value) -> maybe 'a -> register_value*)