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