src/HOL/Bali/DeclConcepts.thy
changeset 37406 982f3e02f3c4
parent 36366 886b94b1bed7
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Fri Jun 11 17:14:01 2010 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Fri Jun 11 17:14:01 2010 +0200
     1.3 @@ -244,30 +244,30 @@
     1.4  lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
     1.5  by (cases m) (simp add: mhead_def member_is_static_simp)
     1.6  
     1.7 -constdefs  --{* some mnemotic selectors for various pairs *} 
     1.8 -           
     1.9 - "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
    1.10 - "decliface \<equiv> fst"          --{* get the interface component *}
    1.11 +-- {* some mnemotic selectors for various pairs *} 
    1.12 +
    1.13 +definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
    1.14 +  "decliface = fst"          --{* get the interface component *}
    1.15  
    1.16 - "mbr"::   "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
    1.17 - "mbr \<equiv> snd"            --{* get the memberdecl component *}
    1.18 +definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
    1.19 +  "mbr = snd"            --{* get the memberdecl component *}
    1.20  
    1.21 - "mthd"::   "('b \<times> 'a) \<Rightarrow> 'a"
    1.22 -                           --{* also used for mdecl, mhead *}
    1.23 - "mthd \<equiv> snd"              --{* get the method component *}
    1.24 +definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
    1.25 +  "mthd = snd"              --{* get the method component *}
    1.26 +    --{* also used for mdecl, mhead *}
    1.27  
    1.28 - "fld"::   "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
    1.29 -              --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
    1.30 - "fld \<equiv> snd"               --{* get the field component *}
    1.31 +definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
    1.32 +  "fld = snd"               --{* get the field component *}
    1.33 +    --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
    1.34  
    1.35 +-- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
    1.36  
    1.37 -constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
    1.38 - fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
    1.39 - "fname \<equiv> fst"
    1.40 -  
    1.41 -  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
    1.42 - "declclassf \<equiv> snd"
    1.43 +definition fname:: "vname \<times> 'a \<Rightarrow> vname" where 
    1.44 +  "fname = fst"
    1.45 +    --{* also used for fdecl *}
    1.46  
    1.47 +definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
    1.48 +  "declclassf = snd"
    1.49  
    1.50  
    1.51  lemma decliface_simp[simp]: "decliface (I,m) = I"
    1.52 @@ -318,12 +318,13 @@
    1.53  lemma declclassf_simp[simp]:"declclassf (n,c) = c"
    1.54  by (simp add: declclassf_def)
    1.55  
    1.56 -constdefs  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
    1.57 -  "fldname"  :: "(vname \<times> qtname) \<Rightarrow> vname" 
    1.58 -  "fldname \<equiv> fst"
    1.59 +  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
    1.60  
    1.61 -  "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
    1.62 -  "fldclass \<equiv> snd"
    1.63 +definition fldname :: "vname \<times> qtname \<Rightarrow> vname"  where
    1.64 +  "fldname = fst"
    1.65 +
    1.66 +definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
    1.67 +  "fldclass = snd"
    1.68  
    1.69  lemma fldname_simp[simp]: "fldname (n,c) = n"
    1.70  by (simp add: fldname_def)
    1.71 @@ -337,8 +338,8 @@
    1.72  text {* Convert a qualified method declaration (qualified with its declaring 
    1.73  class) to a qualified member declaration:  @{text methdMembr}  *}
    1.74  
    1.75 -definition methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" where
    1.76 - "methdMembr m \<equiv> (fst m,mdecl (snd m))"
    1.77 +definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
    1.78 + "methdMembr m = (fst m, mdecl (snd m))"
    1.79  
    1.80  lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
    1.81  by (simp add: methdMembr_def)