author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14981  e73f8140af78 
child 17160  fb65eda72fc7 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Value.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 
header {* Java values *} 

6 

7 

8 

16417  9 
theory Value imports Type begin 
12854  10 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

11 
typedecl loc {* locations, i.e. abstract references on objects *} 
12854  12 
arities loc :: "type" 
13 

14 
datatype val 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

15 
= Unit {* dummy result value of void methods *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

16 
 Bool bool {* Boolean value *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

17 
 Intg int {* integer value *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

18 
 Null {* null reference *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

19 
 Addr loc {* addresses, i.e. locations of objects *} 
12854  20 

21 

22 
translations "val" <= (type) "Term.val" 

23 
"loc" <= (type) "Term.loc" 

24 

25 
consts the_Bool :: "val \<Rightarrow> bool" 

26 
primrec "the_Bool (Bool b) = b" 

27 
consts the_Intg :: "val \<Rightarrow> int" 

28 
primrec "the_Intg (Intg i) = i" 

29 
consts the_Addr :: "val \<Rightarrow> loc" 

30 
primrec "the_Addr (Addr a) = a" 

31 

32 
types dyn_ty = "loc \<Rightarrow> ty option" 

33 
consts 

34 
typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

35 
defpval :: "prim_ty \<Rightarrow> val" {* default value for primitive types *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

36 
default_val :: " ty \<Rightarrow> val" {* default value for all types *} 
12854  37 

38 
primrec "typeof dt Unit = Some (PrimT Void)" 

39 
"typeof dt (Bool b) = Some (PrimT Boolean)" 

40 
"typeof dt (Intg i) = Some (PrimT Integer)" 

41 
"typeof dt Null = Some NT" 

42 
"typeof dt (Addr a) = dt a" 

43 

44 
primrec "defpval Void = Unit" 

45 
"defpval Boolean = Bool False" 

46 
"defpval Integer = Intg 0" 

47 
primrec "default_val (PrimT pt) = defpval pt" 

48 
"default_val (RefT r ) = Null" 

49 

50 
end 