src/HOL/Bali/Example.thy
changeset 35416 d8d7d1b785af
parent 35067 af4c18c30593
child 36319 8feb2c4bef1a
     1.1 --- a/src/HOL/Bali/Example.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -153,23 +153,18 @@
     1.4    
     1.5    foo    :: mname
     1.6  
     1.7 -constdefs
     1.8 -  
     1.9 -  foo_sig   :: sig
    1.10 - "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
    1.11 +definition foo_sig :: sig
    1.12 + where "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
    1.13    
    1.14 -  foo_mhead :: mhead
    1.15 - "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
    1.16 +definition foo_mhead :: mhead
    1.17 + where "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
    1.18  
    1.19 -constdefs
    1.20 -  
    1.21 -  Base_foo :: mdecl
    1.22 - "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
    1.23 +definition Base_foo :: mdecl
    1.24 + where "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
    1.25                          mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
    1.26  
    1.27 -constdefs
    1.28 -  Ext_foo  :: mdecl
    1.29 - "Ext_foo  \<equiv> (foo_sig, 
    1.30 +definition Ext_foo :: mdecl
    1.31 + where "Ext_foo  \<equiv> (foo_sig, 
    1.32                \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
    1.33                 mbody=\<lparr>lcls=[]
    1.34                       ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
    1.35 @@ -177,12 +172,10 @@
    1.36                                  Return (Lit Null)\<rparr>
    1.37                \<rparr>)"
    1.38  
    1.39 -constdefs
    1.40 -  
    1.41 -arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
    1.42 +definition arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" where
    1.43  "arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
    1.44  
    1.45 -BaseCl :: "class"
    1.46 +definition BaseCl :: "class" where
    1.47  "BaseCl \<equiv> \<lparr>access=Public,
    1.48             cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
    1.49                      (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
    1.50 @@ -192,7 +185,7 @@
    1.51             super=Object,
    1.52             superIfs=[HasFoo]\<rparr>"
    1.53    
    1.54 -ExtCl  :: "class"
    1.55 +definition ExtCl  :: "class" where
    1.56  "ExtCl  \<equiv> \<lparr>access=Public,
    1.57             cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
    1.58             methods=[Ext_foo],
    1.59 @@ -200,7 +193,7 @@
    1.60             super=Base,
    1.61             superIfs=[]\<rparr>"
    1.62  
    1.63 -MainCl :: "class"
    1.64 +definition MainCl :: "class" where
    1.65  "MainCl \<equiv> \<lparr>access=Public,
    1.66             cfields=[], 
    1.67             methods=[], 
    1.68 @@ -209,16 +202,14 @@
    1.69             superIfs=[]\<rparr>"
    1.70  (* The "main" method is modeled seperately (see tprg) *)
    1.71  
    1.72 -constdefs
    1.73 -  
    1.74 -  HasFooInt :: iface
    1.75 - "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
    1.76 +definition HasFooInt :: iface
    1.77 + where "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
    1.78  
    1.79 -  Ifaces ::"idecl list"
    1.80 - "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
    1.81 +definition Ifaces ::"idecl list"
    1.82 + where "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
    1.83  
    1.84 - "Classes" ::"cdecl list"
    1.85 - "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
    1.86 +definition "Classes" ::"cdecl list"
    1.87 + where "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
    1.88  
    1.89  lemmas table_classes_defs = 
    1.90       Classes_def standard_classes_def ObjectC_def SXcptC_def
    1.91 @@ -273,8 +264,7 @@
    1.92    tprg :: prog where
    1.93    "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
    1.94  
    1.95 -constdefs
    1.96 -  test    :: "(ty)list \<Rightarrow> stmt"
    1.97 +definition test :: "(ty)list \<Rightarrow> stmt" where
    1.98   "test pTs \<equiv> e:==NewC Ext;; 
    1.99             \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
   1.100             \<spacespace> Catch((SXcpt NullPointer) z)