author  haftmann 
Mon, 01 Mar 2010 13:40:23 +0100  
changeset 35416  d8d7d1b785af 
parent 35069  09154b995ed8 
child 35431  8758fe1fc9f8 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Type.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 

5 
header {* Java types *} 

6 

16417  7 
theory Type imports Name begin 
12854  8 

9 
text {* 

10 
simplifications: 

11 
\begin{itemize} 

12 
\item only the most important primitive types 

13 
\item the null type is regarded as reference type 

14 
\end{itemize} 

15 
*} 

16 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

17 
datatype prim_ty {* primitive type, cf. 4.2 *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

18 
= Void {* result type of void methods *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

19 
 Boolean 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

20 
 Integer 
12854  21 

22 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

23 
datatype ref_ty {* reference type, cf. 4.3 *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

24 
= NullT {* null type, cf. 4.1 *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

25 
 IfaceT qtname {* interface type *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

26 
 ClassT qtname {* class type *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

27 
 ArrayT ty {* array type *} 
12854  28 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

29 
and ty {* any type, cf. 4.1 *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

30 
= PrimT prim_ty {* primitive type *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
16417
diff
changeset

31 
 RefT ref_ty {* reference type *} 
12854  32 

33 
translations 

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

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

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

37 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

38 
abbreviation "NT == RefT NullT" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

39 
abbreviation "Iface I == RefT (IfaceT I)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

40 
abbreviation "Class C == RefT (ClassT C)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

41 
abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

42 
where "T.[] == RefT (ArrayT T)" 
12854  43 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

44 
definition the_Class :: "ty \<Rightarrow> qtname" where 
14766  45 
"the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **) 
12854  46 

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

48 
by (auto simp add: the_Class_def) 

49 

50 
end 