| author | nipkow |
| Fri, 26 Nov 1999 08:46:59 +0100 | |
| changeset 8034 | 6fc37b5c5e98 |
| parent 8011 | d14c4e9e9c8e |
| child 8038 | a13c3b80d3d4 |
| permissions | -rw-r--r-- |
| nipkow@8011 | 1 |
(* Title: HOL/MicroJava/JVM/Store.thy |
| nipkow@8011 | 2 |
ID: $Id$ |
| nipkow@8011 | 3 |
Author: Cornelia Pusch |
| nipkow@8011 | 4 |
Copyright 1999 Technische Universitaet Muenchen |
| nipkow@8011 | 5 |
|
| nipkow@8011 | 6 |
The store. |
| nipkow@8011 | 7 |
|
| nipkow@8011 | 8 |
The JVM builds on many notions already defined in Java. |
| nipkow@8011 | 9 |
Conform provides notions for the type safety proof of the Bytecode Verifier. |
| nipkow@8011 | 10 |
*) |
| nipkow@8011 | 11 |
|
| nipkow@8011 | 12 |
Store = Conform + |
| nipkow@8011 | 13 |
|
| nipkow@8011 | 14 |
syntax |
| nipkow@8034 | 15 |
map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _")
|
| nipkow@8011 | 16 |
translations |
| nipkow@8034 | 17 |
"t !! x" == "the (t x)" |
| nipkow@8011 | 18 |
|
| nipkow@8011 | 19 |
constdefs |
| nipkow@8011 | 20 |
newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
|
| nipkow@8011 | 21 |
"newref s \\<equiv> \\<epsilon>v. s v = None" |
| nipkow@8011 | 22 |
|
| nipkow@8011 | 23 |
end |