author  blanchet 
Tue, 09 Sep 2014 20:51:36 +0200  
changeset 58249  180f1b3508ed 
parent 37956  ee939247b2fb 
child 58310  91ea607a34d8 
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 

58249
180f1b3508ed
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
blanchet
parents:
37956
diff
changeset

17 
datatype_new prim_ty {* primitive type, cf. 4.2 *} 
32960
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 

58249
180f1b3508ed
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
blanchet
parents:
37956
diff
changeset

23 
datatype_new ref_ty {* reference type, cf. 4.3 *} 
32960
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 

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

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

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

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

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

37 
where "T.[] == RefT (ArrayT T)" 
12854  38 

37956  39 
definition 
40 
the_Class :: "ty \<Rightarrow> qtname" 

41 
where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **) 

12854  42 

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

44 
by (auto simp add: the_Class_def) 

45 

46 
end 