diff options
Diffstat (limited to 'snapshots')
| -rw-r--r-- | snapshots/isabelle/riscv/Riscv_lemmas.thy | 13 | ||||
| -rw-r--r-- | snapshots/isabelle/riscv/Riscv_types.thy | 5 |
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*) |