diff options
| author | Thomas Bauereiss | 2018-07-07 22:47:28 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-09 14:47:48 +0100 |
| commit | 2529f5a65d70dfffe40ead73ae49aaa4d78fefb4 (patch) | |
| tree | 0fc1951dd3dc76442f7cae52aa59d35cbf4aff70 /src | |
| parent | 90ea9c794ffe47365b7e856eba4ee8af0aefa0ca (diff) | |
Add some syntactic sugar for Isabelle
Diffstat (limited to 'src')
| -rw-r--r-- | src/state.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/state.ml b/src/state.ml index e788ab6a..245d450c 100644 --- a/src/state.ml +++ b/src/state.ml @@ -367,15 +367,15 @@ 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]:"; - " \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\""; + " \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\""; " by (auto simp: liftState_read_reg_readS register_defs)"; ""; "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; - " \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\""; + " \"\\<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)" ] in - string "abbreviation \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^ + string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^ hardline ^^ hardline ^^ register_defs ^^ hardline ^^ hardline ^^ |