src/HOL/Bali/Type.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 32960 69916a850301
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Type.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Java types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     8
theory Type imports Name begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item only the most important primitive types
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\item the null type is regarded as reference type
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
	| Boolean
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
	| Integer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
  "prim_ty" <= (type) "Type.prim_ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  "ref_ty"  <= (type) "Type.ref_ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
  "ty"      <= (type) "Type.ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
	 NT	:: "       \<spacespace> ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
	 Iface	:: "qtname  \<Rightarrow> ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
	 Class	:: "qtname  \<Rightarrow> ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
	 Array	:: "ty     \<Rightarrow> ty"	("_.[]" [90] 90)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
	"NT"      == "RefT   NullT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
	"Iface I" == "RefT (IfaceT I)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
	"Class C" == "RefT (ClassT C)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
	"T.[]"    == "RefT (ArrayT T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
  the_Class :: "ty \<Rightarrow> qtname"
14766
c0401da7726d use plain SOME;
wenzelm
parents: 14171
diff changeset
    53
 "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
by (auto simp add: the_Class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
end