src/HOL/Bali/Name.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/Name.thy
     2     Author:     David von Oheimb
     3 *)
     4 subsection \<open>Java names\<close>
     5 
     6 theory Name imports Basis begin
     7 
     8 (* cf. 6.5 *) 
     9 typedecl tnam   \<comment>\<open>ordinary type name, i.e. class or interface name\<close>
    10 typedecl pname  \<comment>\<open>package name\<close>
    11 typedecl mname  \<comment>\<open>method name\<close>
    12 typedecl vname  \<comment>\<open>variable or field name\<close>
    13 typedecl label  \<comment>\<open>label as destination of break or continue\<close>
    14 
    15 datatype ename        \<comment>\<open>expression name\<close> 
    16         = VNam vname 
    17         | Res         \<comment>\<open>special name to model the return value of methods\<close>
    18 
    19 datatype lname        \<comment>\<open>names for local variables and the This pointer\<close>
    20         = EName ename 
    21         | This
    22 abbreviation VName   :: "vname \<Rightarrow> lname"
    23       where "VName n == EName (VNam n)"
    24 
    25 abbreviation Result :: lname
    26       where "Result == EName Res"
    27 
    28 datatype xname          \<comment>\<open>names of standard exceptions\<close>
    29         = Throwable
    30         | NullPointer | OutOfMemory | ClassCast   
    31         | NegArrSize  | IndOutBound | ArrStore
    32 
    33 lemma xn_cases: 
    34   "xn = Throwable   \<or> xn = NullPointer \<or>  
    35          xn = OutOfMemory \<or> xn = ClassCast \<or> 
    36          xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
    37 apply (induct xn)
    38 apply auto
    39 done
    40 
    41 
    42 datatype tname  \<comment>\<open>type names for standard classes and other type names\<close>
    43         = Object'
    44         | SXcpt'   xname
    45         | TName   tnam
    46 
    47 record   qtname = \<comment>\<open>qualified tname cf. 6.5.3, 6.5.4\<close>
    48           pid :: pname  
    49           tid :: tname
    50 
    51 class has_pname =
    52   fixes pname :: "'a \<Rightarrow> pname"
    53 
    54 instantiation pname :: has_pname
    55 begin
    56 
    57 definition
    58   pname_pname_def: "pname (p::pname) \<equiv> p"
    59 
    60 instance ..
    61 
    62 end
    63 
    64 class has_tname =
    65   fixes tname :: "'a \<Rightarrow> tname"
    66 
    67 instantiation tname :: has_tname
    68 begin
    69 
    70 definition
    71   tname_tname_def: "tname (t::tname) = t"
    72 
    73 instance ..
    74 
    75 end
    76 
    77 definition
    78   qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"
    79 
    80 translations
    81   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    82   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    83 
    84 
    85 axiomatization java_lang::pname \<comment>\<open>package java.lang\<close>
    86 
    87 definition
    88   Object :: qtname
    89   where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
    90 
    91 definition SXcpt :: "xname \<Rightarrow> qtname"
    92   where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
    93 
    94 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
    95 by (simp add: Object_def SXcpt_def)
    96 
    97 lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
    98 by (simp add: SXcpt_def)
    99 
   100 end