diff options
| author | Alasdair | 2020-05-21 16:43:30 +0100 |
|---|---|---|
| committer | Alasdair | 2020-05-21 16:43:30 +0100 |
| commit | 07ceceff23cf4aac2c6fe8de764cb404e21c7828 (patch) | |
| tree | b07c800a6e43f6174f324234d54bb53c31d17e8e /src/state.ml | |
| parent | 8320ddc4b19d622f8ab5ab8625dde45fccbf383b (diff) | |
| parent | 33be6201fa34557a46652658445f9c48c819ad34 (diff) | |
Merge branch 'mono-tweaks' of github.com:rems-project/sail into mono-tweaks
Diffstat (limited to 'src/state.ml')
| -rw-r--r-- | src/state.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/state.ml b/src/state.ml index 478a3fd5..8d487d3e 100644 --- a/src/state.ml +++ b/src/state.ml @@ -410,12 +410,12 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id' = remove_trailing_underscores id in separate_map hardline string [ "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\""; - " by (auto simp: liftState_read_reg_readS register_defs)"; + " \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = read_regS " ^ id ^ "_ref\""; + " by (intro liftState_read_reg) (auto simp: register_defs)"; ""; "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\""; - " by (auto simp: liftState_write_reg_updateS register_defs)" + " \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = write_regS " ^ id ^ "_ref v\""; + " by (intro liftState_write_reg) (auto simp: register_defs)" ] in string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^ |