equal
deleted
inserted
replaced
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 *) |
4 *) |
5 |
5 |
6 header {* Example of a proof based on the Bali axiomatic semantics *} |
6 header {* Example of a proof based on the Bali axiomatic semantics *} |
7 |
7 |
8 theory AxExample = AxSem + Example: |
8 theory AxExample imports AxSem Example begin |
9 |
9 |
10 constdefs |
10 constdefs |
11 arr_inv :: "st \<Rightarrow> bool" |
11 arr_inv :: "st \<Rightarrow> bool" |
12 "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and> |
12 "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and> |
13 values obj (Inl (arr, Base)) = Some (Addr a) \<and> |
13 values obj (Inl (arr, Base)) = Some (Addr a) \<and> |