248 |
248 |
249 \<comment> \<open>some mnemotic selectors for various pairs\<close> |
249 \<comment> \<open>some mnemotic selectors for various pairs\<close> |
250 |
250 |
251 definition |
251 definition |
252 decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where |
252 decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where |
253 "decliface = fst" \<comment>\<open>get the interface component\<close> |
253 "decliface = fst" \<comment> \<open>get the interface component\<close> |
254 |
254 |
255 definition |
255 definition |
256 mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where |
256 mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where |
257 "mbr = snd" \<comment>\<open>get the memberdecl component\<close> |
257 "mbr = snd" \<comment> \<open>get the memberdecl component\<close> |
258 |
258 |
259 definition |
259 definition |
260 mthd :: "'b \<times> 'a \<Rightarrow> 'a" where |
260 mthd :: "'b \<times> 'a \<Rightarrow> 'a" where |
261 "mthd = snd" \<comment>\<open>get the method component\<close> |
261 "mthd = snd" \<comment> \<open>get the method component\<close> |
262 \<comment>\<open>also used for mdecl, mhead\<close> |
262 \<comment> \<open>also used for mdecl, mhead\<close> |
263 |
263 |
264 definition |
264 definition |
265 fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where |
265 fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where |
266 "fld = snd" \<comment>\<open>get the field component\<close> |
266 "fld = snd" \<comment> \<open>get the field component\<close> |
267 \<comment>\<open>also used for \<open>((vname \<times> qtname)\<times> field)\<close>\<close> |
267 \<comment> \<open>also used for \<open>((vname \<times> qtname)\<times> field)\<close>\<close> |
268 |
268 |
269 \<comment> \<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close> |
269 \<comment> \<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close> |
270 |
270 |
271 definition |
271 definition |
272 fname:: "vname \<times> 'a \<Rightarrow> vname" |
272 fname:: "vname \<times> 'a \<Rightarrow> vname" |
273 where "fname = fst" |
273 where "fname = fst" |
274 \<comment>\<open>also used for fdecl\<close> |
274 \<comment> \<open>also used for fdecl\<close> |
275 |
275 |
276 definition |
276 definition |
277 declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" |
277 declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" |
278 where "declclassf = snd" |
278 where "declclassf = snd" |
279 |
279 |
324 by (simp add: fname_def) |
324 by (simp add: fname_def) |
325 |
325 |
326 lemma declclassf_simp[simp]:"declclassf (n,c) = c" |
326 lemma declclassf_simp[simp]:"declclassf (n,c) = c" |
327 by (simp add: declclassf_def) |
327 by (simp add: declclassf_def) |
328 |
328 |
329 \<comment>\<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close> |
329 \<comment> \<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close> |
330 |
330 |
331 definition |
331 definition |
332 fldname :: "vname \<times> qtname \<Rightarrow> vname" |
332 fldname :: "vname \<times> qtname \<Rightarrow> vname" |
333 where "fldname = fst" |
333 where "fldname = fst" |
334 |
334 |