src/HOL/Bali/DeclConcepts.thy
changeset 35315 fbdc860d87a3
parent 35067 af4c18c30593
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 22 17:02:39 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Feb 23 10:11:12 2010 +0100
     1.3 @@ -79,41 +79,60 @@
     1.4  text {* overloaded selector @{text accmodi} to select the access modifier 
     1.5  out of various HOL types *}
     1.6  
     1.7 -axclass has_accmodi < "type"
     1.8 -consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
     1.9 +class has_accmodi =
    1.10 +  fixes accmodi:: "'a \<Rightarrow> acc_modi"
    1.11 +
    1.12 +instantiation acc_modi :: has_accmodi
    1.13 +begin
    1.14  
    1.15 -instance acc_modi::has_accmodi ..
    1.16 +definition
    1.17 +  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    1.18  
    1.19 -defs (overloaded)
    1.20 -acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    1.21 +instance ..
    1.22 +
    1.23 +end
    1.24  
    1.25  lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
    1.26  by (simp add: acc_modi_accmodi_def)
    1.27  
    1.28 -instance decl_ext_type:: ("type") has_accmodi ..
    1.29 +instantiation decl_ext_type:: (type) has_accmodi
    1.30 +begin
    1.31  
    1.32 -defs (overloaded)
    1.33 -decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    1.34 +definition
    1.35 +  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    1.36  
    1.37 +instance ..
    1.38 +
    1.39 +end
    1.40  
    1.41  lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
    1.42  by (simp add: decl_acc_modi_def)
    1.43  
    1.44 -instance * :: ("type",has_accmodi) has_accmodi ..
    1.45 +instantiation * :: (type, has_accmodi) has_accmodi
    1.46 +begin
    1.47  
    1.48 -defs (overloaded)
    1.49 -pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    1.50 +definition
    1.51 +  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    1.52 +
    1.53 +instance ..
    1.54 +
    1.55 +end
    1.56  
    1.57  lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
    1.58  by (simp add: pair_acc_modi_def)
    1.59  
    1.60 -instance memberdecl :: has_accmodi ..
    1.61 +instantiation memberdecl :: has_accmodi
    1.62 +begin
    1.63  
    1.64 -defs (overloaded)
    1.65 -memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
    1.66 +definition
    1.67 +  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
    1.68                                            fdecl f \<Rightarrow> accmodi f
    1.69                                          | mdecl m \<Rightarrow> accmodi m)"
    1.70  
    1.71 +instance ..
    1.72 +
    1.73 +end
    1.74 +
    1.75  lemma memberdecl_fdecl_acc_modi_simp[simp]:
    1.76   "accmodi (fdecl m) = accmodi m"
    1.77  by (simp add: memberdecl_acc_modi_def)
    1.78 @@ -125,21 +144,35 @@
    1.79  text {* overloaded selector @{text declclass} to select the declaring class 
    1.80  out of various HOL types *}
    1.81  
    1.82 -axclass has_declclass < "type"
    1.83 -consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
    1.84 +class has_declclass =
    1.85 +  fixes declclass:: "'a \<Rightarrow> qtname"
    1.86 +
    1.87 +instantiation qtname_ext_type :: (type) has_declclass
    1.88 +begin
    1.89  
    1.90 -instance qtname_ext_type::("type") has_declclass ..
    1.91 +definition
    1.92 +  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
    1.93 +
    1.94 +instance ..
    1.95  
    1.96 -defs (overloaded)
    1.97 -qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
    1.98 +end
    1.99 +
   1.100 +lemma qtname_declclass_def:
   1.101 +  "declclass q \<equiv> (q::qtname)"
   1.102 +  by (induct q) (simp add: declclass_qtname_ext_type_def)
   1.103  
   1.104  lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
   1.105  by (simp add: qtname_declclass_def)
   1.106  
   1.107 -instance * :: ("has_declclass","type") has_declclass ..
   1.108 +instantiation * :: (has_declclass, type) has_declclass
   1.109 +begin
   1.110  
   1.111 -defs (overloaded)
   1.112 -pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
   1.113 +definition
   1.114 +  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
   1.115 +
   1.116 +instance ..
   1.117 +
   1.118 +end
   1.119  
   1.120  lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
   1.121  by (simp add: pair_declclass_def)
   1.122 @@ -147,25 +180,38 @@
   1.123  text {* overloaded selector @{text is_static} to select the static modifier 
   1.124  out of various HOL types *}
   1.125  
   1.126 +class has_static =
   1.127 +  fixes is_static :: "'a \<Rightarrow> bool"
   1.128  
   1.129 -axclass has_static < "type"
   1.130 -consts is_static :: "'a::has_static \<Rightarrow> bool"
   1.131 +instantiation decl_ext_type :: (has_static) has_static
   1.132 +begin
   1.133  
   1.134 -instance decl_ext_type :: ("has_static") has_static ..
   1.135 +instance ..
   1.136 +
   1.137 +end
   1.138  
   1.139 -instance member_ext_type :: ("type") has_static ..
   1.140 +instantiation member_ext_type :: (type) has_static
   1.141 +begin
   1.142 +
   1.143 +instance ..
   1.144  
   1.145 -defs (overloaded)
   1.146 -static_field_type_is_static_def: 
   1.147 - "is_static (m::('b member_scheme)) \<equiv> static m"
   1.148 +end
   1.149 +
   1.150 +axiomatization where
   1.151 +  static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> static m"
   1.152  
   1.153  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
   1.154  by (simp add: static_field_type_is_static_def)
   1.155  
   1.156 -instance * :: ("type","has_static") has_static ..
   1.157 +instantiation * :: (type, has_static) has_static
   1.158 +begin
   1.159  
   1.160 -defs (overloaded)
   1.161 -pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
   1.162 +definition
   1.163 +  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
   1.164 +
   1.165 +instance ..
   1.166 +
   1.167 +end
   1.168  
   1.169  lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
   1.170  by (simp add: pair_is_static_def)
   1.171 @@ -173,14 +219,19 @@
   1.172  lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
   1.173  by (simp add: pair_is_static_def)
   1.174  
   1.175 -instance memberdecl:: has_static ..
   1.176 +instantiation memberdecl :: has_static
   1.177 +begin
   1.178  
   1.179 -defs (overloaded)
   1.180 +definition
   1.181  memberdecl_is_static_def: 
   1.182   "is_static m \<equiv> (case m of
   1.183                      fdecl f \<Rightarrow> is_static f
   1.184                    | mdecl m \<Rightarrow> is_static m)"
   1.185  
   1.186 +instance ..
   1.187 +
   1.188 +end
   1.189 +
   1.190  lemma memberdecl_is_static_fdecl_simp[simp]:
   1.191   "is_static (fdecl f) = is_static f"
   1.192  by (simp add: memberdecl_is_static_def)
   1.193 @@ -389,18 +440,32 @@
   1.194  text {* overloaded selector @{text resTy} to select the result type 
   1.195  out of various HOL types *}
   1.196  
   1.197 -axclass has_resTy < "type"
   1.198 -consts resTy:: "'a::has_resTy \<Rightarrow> ty"
   1.199 +class has_resTy =
   1.200 +  fixes resTy:: "'a \<Rightarrow> ty"
   1.201 +
   1.202 +instantiation decl_ext_type :: (has_resTy) has_resTy
   1.203 +begin
   1.204  
   1.205 -instance decl_ext_type :: ("has_resTy") has_resTy ..
   1.206 +instance ..
   1.207 +
   1.208 +end
   1.209 +
   1.210 +instantiation member_ext_type :: (has_resTy) has_resTy
   1.211 +begin
   1.212  
   1.213 -instance member_ext_type :: ("has_resTy") has_resTy ..
   1.214 +instance ..
   1.215  
   1.216 -instance mhead_ext_type :: ("type") has_resTy ..
   1.217 +end
   1.218 +
   1.219 +instantiation mhead_ext_type :: (type) has_resTy
   1.220 +begin
   1.221  
   1.222 -defs (overloaded)
   1.223 -mhead_ext_type_resTy_def: 
   1.224 - "resTy (m::('b mhead_scheme)) \<equiv> resT m"
   1.225 +instance ..
   1.226 +
   1.227 +end
   1.228 +
   1.229 +axiomatization where
   1.230 +  mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> resT m"
   1.231  
   1.232  lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
   1.233  by (simp add: mhead_ext_type_resTy_def)
   1.234 @@ -408,10 +473,15 @@
   1.235  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
   1.236  by (simp add: mhead_def mhead_resTy_simp)
   1.237  
   1.238 -instance * :: ("type","has_resTy") has_resTy ..
   1.239 +instantiation * :: ("type","has_resTy") has_resTy
   1.240 +begin
   1.241  
   1.242 -defs (overloaded)
   1.243 -pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
   1.244 +definition
   1.245 +  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
   1.246 +
   1.247 +instance ..
   1.248 +
   1.249 +end
   1.250  
   1.251  lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
   1.252  by (simp add: pair_resTy_def)