author | oheimb |
Mon, 05 Feb 2001 20:14:15 +0100 | |
changeset 11070 | cc421547e744 |
parent 11026 | a50365d21144 |
child 11372 | 648795477bb5 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/State.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
11070 | 7 |
header "Program State" |
8011 | 8 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
9 |
theory State = TypeRel + Value: |
8011 | 10 |
|
11 |
types fields_ |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
12 |
= "(vname \<times> cname \<leadsto> val)" (* field name, defining class, value *) |
8011 | 13 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
14 |
obj = "cname \<times> fields_" (* class instance with class name and fields *) |
8011 | 15 |
|
16 |
constdefs |
|
10042 | 17 |
obj_ty :: "obj => ty" |
18 |
"obj_ty obj == Class (fst obj)" |
|
8011 | 19 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
20 |
init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
21 |
"init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))" |
8011 | 22 |
|
23 |
datatype xcpt (* exceptions *) |
|
24 |
= NullPointer |
|
25 |
| ClassCast |
|
26 |
| OutOfMemory |
|
27 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
28 |
types aheap = "loc \<leadsto> obj" (* "heap" used in a translation below *) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
29 |
locals = "vname \<leadsto> val" |
8011 | 30 |
|
31 |
state (* simple state, i.e. variable contents *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
32 |
= "aheap \<times> locals" |
8011 | 33 |
(* heap, local parameter including This *) |
34 |
||
35 |
xstate (* state including exception information *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
36 |
= "xcpt option \<times> state" |
8011 | 37 |
|
38 |
syntax |
|
10042 | 39 |
heap :: "state => aheap" |
40 |
locals :: "state => locals" |
|
41 |
Norm :: "state => xstate" |
|
8011 | 42 |
|
43 |
translations |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
44 |
"heap" => "fst" |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
45 |
"locals" => "snd" |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
46 |
"Norm s" == "(None,s)" |
8011 | 47 |
|
48 |
constdefs |
|
49 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
50 |
new_Addr :: "aheap => loc \<times> xcpt option" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
51 |
"new_Addr h == SOME (a,x). (h a = None \<and> x = None) | x = Some OutOfMemory" |
8011 | 52 |
|
10042 | 53 |
raise_if :: "bool => xcpt => xcpt option => xcpt option" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
54 |
"raise_if c x xo == if c \<and> (xo = None) then Some x else xo" |
8011 | 55 |
|
10042 | 56 |
np :: "val => xcpt option => xcpt option" |
57 |
"np v == raise_if (v = Null) NullPointer" |
|
8011 | 58 |
|
10042 | 59 |
c_hupd :: "aheap => xstate => xstate" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
60 |
"c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" |
8011 | 61 |
|
10042 | 62 |
cast_ok :: "'c prog => cname => aheap => val => bool" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
63 |
"cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
64 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
65 |
lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
66 |
apply (unfold obj_ty_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
67 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
68 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
69 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
70 |
lemma new_AddrD: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
71 |
"(a,x) = new_Addr h ==> h a = None \<and> x = None | x = Some OutOfMemory" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
72 |
apply (unfold new_Addr_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
73 |
apply(simp add: Pair_fst_snd_eq Eps_split) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
74 |
apply(rule someI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
75 |
apply(rule disjI2) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
76 |
apply(rule_tac "r" = "snd (?a,Some OutOfMemory)" in trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
77 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
78 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
79 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
80 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
81 |
lemma raise_if_True [simp]: "raise_if True x y \<noteq> None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
82 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
83 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
84 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
85 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
86 |
lemma raise_if_False [simp]: "raise_if False x y = y" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
87 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
88 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
89 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
90 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
91 |
lemma raise_if_Some [simp]: "raise_if c x (Some y) \<noteq> None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
92 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
93 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
94 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
95 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
96 |
lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \<noteq> None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
97 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
98 |
apply(induct_tac "x") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
99 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
100 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
101 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
102 |
lemma raise_if_SomeD [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
103 |
"raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some x | y = Some z" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
104 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
105 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
106 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
107 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
108 |
lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \<not> c \<and> y = None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
109 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
110 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
111 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
112 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
113 |
lemma np_NoneD [rule_format (no_asm)]: "np a' x' = None --> x' = None \<and> a' \<noteq> Null" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
114 |
apply (unfold np_def raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
115 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
116 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
117 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
118 |
lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> Null --> np a' x' = x'" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
119 |
apply (unfold np_def raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
120 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
121 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
122 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
123 |
lemma np_Some [simp]: "np a' (Some xc) = Some xc" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
124 |
apply (unfold np_def raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
125 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
126 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
127 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
128 |
lemma np_Null [simp]: "np Null None = Some NullPointer" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
129 |
apply (unfold np_def raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
130 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
131 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
132 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
133 |
lemma np_Addr [simp]: "np (Addr a) None = None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
134 |
apply (unfold np_def raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
135 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
136 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
137 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
138 |
lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
139 |
Some (if c then xc else NullPointer)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
140 |
apply (unfold raise_if_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
141 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
142 |
done |
8011 | 143 |
|
144 |
end |