src/HOL/Bali/Name.thy
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 38540 8c08631cb4b6
equal deleted inserted replaced
37955:f87d1105e181 37956:ee939247b2fb
    66 
    66 
    67 instantiation tname :: has_tname
    67 instantiation tname :: has_tname
    68 begin
    68 begin
    69 
    69 
    70 definition
    70 definition
    71   tname_tname_def: "tname (t::tname) \<equiv> t"
    71   tname_tname_def: "tname (t::tname) = t"
    72 
    72 
    73 instance ..
    73 instance ..
    74 
    74 
    75 end
    75 end
    76 
    76 
    77 definition
    77 definition
    78   qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
    78   qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
    79 
    79 
    80 translations
    80 translations
    81   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    81   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    82   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    82   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    83 
    83 
    84 
    84 
    85 axiomatization java_lang::pname --{* package java.lang *}
    85 axiomatization java_lang::pname --{* package java.lang *}
    86 
    86 
    87 consts 
    87 definition
    88   Object :: qtname
    88   Object :: qtname
    89   SXcpt  :: "xname \<Rightarrow> qtname"
    89   where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
    90 defs
    90 
    91   Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
    91 definition SXcpt :: "xname \<Rightarrow> qtname"
    92   SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
    92   where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
    93 
    93 
    94 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
    94 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
    95 by (simp add: Object_def SXcpt_def)
    95 by (simp add: Object_def SXcpt_def)
    96 
    96 
    97 lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
    97 lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
    98 by (simp add: SXcpt_def)
    98 by (simp add: SXcpt_def)
       
    99 
    99 end
   100 end