src/HOL/Bali/Type.thy
author haftmann
Mon, 01 Mar 2010 13:40:23 +0100
changeset 35416 d8d7d1b785af
parent 35069 09154b995ed8
child 35431 8758fe1fc9f8
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
header {* Java types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory Type imports Name begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\item only the most important primitive types
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item the null type is regarded as reference type
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    17
datatype prim_ty        --{* primitive type, cf. 4.2 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    18
        = Void          --{* result type of void methods *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    19
        | Boolean
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    20
        | Integer
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    23
datatype ref_ty         --{* reference type, cf. 4.3 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    24
        = NullT         --{* null type, cf. 4.1 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    25
        | IfaceT qtname --{* interface type *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    26
        | ClassT qtname --{* class type *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    27
        | ArrayT ty     --{* array type *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    29
and ty                  --{* any type, cf. 4.1 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    30
        = PrimT prim_ty --{* primitive type *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    31
        | RefT  ref_ty  --{* reference type *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
  "prim_ty" <= (type) "Type.prim_ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
  "ref_ty"  <= (type) "Type.ref_ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  "ty"      <= (type) "Type.ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    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
c0401da7726d use plain SOME;
wenzelm
parents: 14171
diff changeset
    45
 "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
by (auto simp add: the_Class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
end