src/HOL/Bali/Type.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:      HOL/Bali/Type.thy
     2     Author:     David von Oheimb
     3 *)
     4 
     5 subsection \<open>Java types\<close>
     6 
     7 theory Type imports Name begin
     8 
     9 text \<open>
    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 \<close>
    16 
    17 datatype prim_ty        \<comment>\<open>primitive type, cf. 4.2\<close>
    18         = Void          \<comment>\<open>result type of void methods\<close>
    19         | Boolean
    20         | Integer
    21 
    22 
    23 datatype ref_ty         \<comment>\<open>reference type, cf. 4.3\<close>
    24         = NullT         \<comment>\<open>null type, cf. 4.1\<close>
    25         | IfaceT qtname \<comment>\<open>interface type\<close>
    26         | ClassT qtname \<comment>\<open>class type\<close>
    27         | ArrayT ty     \<comment>\<open>array type\<close>
    28 
    29 and ty                  \<comment>\<open>any type, cf. 4.1\<close>
    30         = PrimT prim_ty \<comment>\<open>primitive type\<close>
    31         | RefT  ref_ty  \<comment>\<open>reference type\<close>
    32 
    33 abbreviation "NT == RefT NullT"
    34 abbreviation "Iface I == RefT (IfaceT I)"
    35 abbreviation "Class C == RefT (ClassT C)"
    36 abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
    37   where "T.[] == RefT (ArrayT T)"
    38 
    39 definition
    40   the_Class :: "ty \<Rightarrow> qtname"
    41   where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
    42  
    43 lemma the_Class_eq [simp]: "the_Class (Class C)= C"
    44 by (auto simp add: the_Class_def)
    45 
    46 end