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

4 
*) 

5 

6 
header {* Java types *} 

7 

16417  8 
theory Type imports Name begin 
12854  9 

10 
text {* 

11 
simplifications: 

12 
\begin{itemize} 

13 
\item only the most important primitive types 

14 
\item the null type is regarded as reference type 

15 
\end{itemize} 

16 
*} 

17 

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

18 
datatype prim_ty {* primitive type, cf. 4.2 *} 
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 
= Void {* result type of void methods *} 
12854  20 
 Boolean 
21 
 Integer 

22 

23 

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

24 
datatype ref_ty {* reference type, cf. 4.3 *} 
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

25 
= NullT {* null type, cf. 4.1 *} 
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

26 
 IfaceT qtname {* interface type *} 
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

27 
 ClassT qtname {* class type *} 
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

28 
 ArrayT ty {* array type *} 
12854  29 

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

30 
and ty {* any type, cf. 4.1 *} 
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

31 
= PrimT prim_ty {* primitive type *} 
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

32 
 RefT ref_ty {* reference type *} 
12854  33 

34 
translations 

35 
"prim_ty" <= (type) "Type.prim_ty" 

36 
"ref_ty" <= (type) "Type.ref_ty" 

37 
"ty" <= (type) "Type.ty" 

38 

39 
syntax 

40 
NT :: " \<spacespace> ty" 

41 
Iface :: "qtname \<Rightarrow> ty" 

42 
Class :: "qtname \<Rightarrow> ty" 

43 
Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) 

44 

45 
translations 

46 
"NT" == "RefT NullT" 

47 
"Iface I" == "RefT (IfaceT I)" 

48 
"Class C" == "RefT (ClassT C)" 

49 
"T.[]" == "RefT (ArrayT T)" 

50 

51 
constdefs 

52 
the_Class :: "ty \<Rightarrow> qtname" 

14766  53 
"the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **) 
12854  54 

55 
lemma the_Class_eq [simp]: "the_Class (Class C)= C" 

56 
by (auto simp add: the_Class_def) 

57 

58 
end 