# HG changeset patch # User haftmann # Date 1276269241 -7200 # Node ID 982f3e02f3c47fa49e0c571f68a0c53f2ae4eb0a # Parent 7c49988afd0e5d5c2bfe931b429b801f8e66dfe0 modernized specifications diff -r 7c49988afd0e -r 982f3e02f3c4 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Fri Jun 11 17:14:01 2010 +0200 +++ b/src/HOL/Bali/DeclConcepts.thy Fri Jun 11 17:14:01 2010 +0200 @@ -244,30 +244,30 @@ lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m" by (cases m) (simp add: mhead_def member_is_static_simp) -constdefs --{* some mnemotic selectors for various pairs *} - - "decliface":: "(qtname \ ('a::type) decl_scheme) \ qtname" - "decliface \ fst" --{* get the interface component *} +-- {* some mnemotic selectors for various pairs *} + +definition decliface :: "qtname \ 'a decl_scheme \ qtname" where + "decliface = fst" --{* get the interface component *} - "mbr":: "(qtname \ memberdecl) \ memberdecl" - "mbr \ snd" --{* get the memberdecl component *} +definition mbr :: "qtname \ memberdecl \ memberdecl" where + "mbr = snd" --{* get the memberdecl component *} - "mthd":: "('b \ 'a) \ 'a" - --{* also used for mdecl, mhead *} - "mthd \ snd" --{* get the method component *} +definition mthd :: "'b \ 'a \ 'a" where + "mthd = snd" --{* get the method component *} + --{* also used for mdecl, mhead *} - "fld":: "('b \ ('a::type) decl_scheme) \ ('a::type) decl_scheme" - --{* also used for @{text "((vname \ qtname)\ field)"} *} - "fld \ snd" --{* get the field component *} +definition fld :: "'b \ 'a decl_scheme \ 'a decl_scheme" where + "fld = snd" --{* get the field component *} + --{* also used for @{text "((vname \ qtname)\ field)"} *} +-- {* some mnemotic selectors for @{text "(vname \ qtname)"} *} -constdefs --{* some mnemotic selectors for @{text "(vname \ qtname)"} *} - fname:: "(vname \ 'a) \ vname" --{* also used for fdecl *} - "fname \ fst" - - declclassf:: "(vname \ qtname) \ qtname" - "declclassf \ snd" +definition fname:: "vname \ 'a \ vname" where + "fname = fst" + --{* also used for fdecl *} +definition declclassf:: "(vname \ qtname) \ qtname" where + "declclassf = snd" lemma decliface_simp[simp]: "decliface (I,m) = I" @@ -318,12 +318,13 @@ lemma declclassf_simp[simp]:"declclassf (n,c) = c" by (simp add: declclassf_def) -constdefs --{* some mnemotic selectors for @{text "(vname \ qtname)"} *} - "fldname" :: "(vname \ qtname) \ vname" - "fldname \ fst" + --{* some mnemotic selectors for @{text "(vname \ qtname)"} *} - "fldclass" :: "(vname \ qtname) \ qtname" - "fldclass \ snd" +definition fldname :: "vname \ qtname \ vname" where + "fldname = fst" + +definition fldclass :: "vname \ qtname \ qtname" where + "fldclass = snd" lemma fldname_simp[simp]: "fldname (n,c) = n" by (simp add: fldname_def) @@ -337,8 +338,8 @@ text {* Convert a qualified method declaration (qualified with its declaring class) to a qualified member declaration: @{text methdMembr} *} -definition methdMembr :: "(qtname \ mdecl) \ (qtname \ memberdecl)" where - "methdMembr m \ (fst m,mdecl (snd m))" +definition methdMembr :: "qtname \ mdecl \ qtname \ memberdecl" where + "methdMembr m = (fst m, mdecl (snd m))" lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)" by (simp add: methdMembr_def) diff -r 7c49988afd0e -r 982f3e02f3c4 src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Fri Jun 11 17:14:01 2010 +0200 +++ b/src/HOL/Bali/WellType.thy Fri Jun 11 17:14:01 2010 +0200 @@ -103,22 +103,23 @@ "mheads G S (ClassT C) = cmheads G S C" "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)" -constdefs +definition --{* applicable methods, cf. 15.11.2.1 *} - appl_methds :: "prog \ qtname \ ref_ty \ sig \ (emhead \ ty list)\ set" - "appl_methds G S rt \ \ sig. + appl_methds :: "prog \ qtname \ ref_ty \ sig \ (emhead \ ty list)\ set" where + "appl_methds G S rt = (\ sig. {(mh,pTs') |mh pTs'. mh \ mheads G S rt \name=name sig,parTs=pTs'\ \ - G\(parTs sig)[\]pTs'}" + G\(parTs sig)[\]pTs'})" +definition --{* more specific methods, cf. 15.11.2.2 *} - more_spec :: "prog \ emhead \ ty list \ emhead \ ty list \ bool" - "more_spec G \ \(mh,pTs). \(mh',pTs'). G\pTs[\]pTs'" + more_spec :: "prog \ emhead \ ty list \ emhead \ ty list \ bool" where + "more_spec G = (\(mh,pTs). \(mh',pTs'). G\pTs[\]pTs')" (*more_spec G \\((d,h),pTs). \((d',h'),pTs'). G\RefT d\RefT d'\G\pTs[\]pTs'*) +definition --{* maximally specific methods, cf. 15.11.2.2 *} - max_spec :: "prog \ qtname \ ref_ty \ sig \ (emhead \ ty list)\ set" - - "max_spec G S rt sig \{m. m \appl_methds G S rt sig \ + max_spec :: "prog \ qtname \ ref_ty \ sig \ (emhead \ ty list)\ set" where + "max_spec G S rt sig = {m. m \appl_methds G S rt sig \ (\m'\appl_methds G S rt sig. more_spec G m' m \ m'=m)}" diff -r 7c49988afd0e -r 982f3e02f3c4 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Fri Jun 11 17:14:01 2010 +0200 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Jun 11 17:14:01 2010 +0200 @@ -15,48 +15,53 @@ to type \emph{checking}. *} -constdefs +definition -- "The program counter will always be inside the method:" - check_bounded :: "instr list \ exception_table \ bool" - "check_bounded ins et \ + check_bounded :: "instr list \ exception_table \ bool" where + "check_bounded ins et \ (\pc < length ins. \pc' \ set (succs (ins!pc) pc). pc' < length ins) \ (\e \ set et. fst (snd (snd e)) < length ins)" +definition -- "The method type only contains declared classes:" - check_types :: "jvm_prog \ nat \ nat \ JVMType.state list \ bool" - "check_types G mxs mxr phi \ set phi \ states G mxs mxr" + check_types :: "jvm_prog \ nat \ nat \ JVMType.state list \ bool" where + "check_types G mxs mxr phi \ set phi \ states G mxs mxr" +definition -- "An instruction is welltyped if it is applicable and its effect" -- "is compatible with the type at all successor instructions:" wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count, - exception_table,p_count] \ bool" - "wt_instr i G rT phi mxs max_pc et pc \ + exception_table,p_count] \ bool" where + "wt_instr i G rT phi mxs max_pc et pc \ app i G mxs rT pc et (phi!pc) \ (\(pc',s') \ set (eff i G pc et (phi!pc)). pc' < max_pc \ G \ s' <=' phi!pc')" +definition -- {* The type at @{text "pc=0"} conforms to the method calling convention: *} - wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \ bool" - "wt_start G C pTs mxl phi == + wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \ bool" where + "wt_start G C pTs mxl phi \ G \ Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" +definition -- "A method is welltyped if the body is not empty, if execution does not" -- "leave the body, if the method type covers all instructions and mentions" -- "declared classes only, if the method calling convention is respected, and" -- "if all instructions are welltyped." wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, - exception_table,method_type] \ bool" - "wt_method G C pTs rT mxs mxl ins et phi \ - let max_pc = length ins in + exception_table,method_type] \ bool" where + "wt_method G C pTs rT mxs mxl ins et phi \ + (let max_pc = length ins in 0 < max_pc \ length phi = length ins \ check_bounded ins et \ check_types G mxs (1+length pTs+mxl) (map OK phi) \ wt_start G C pTs mxl phi \ - (\pc. pc wt_instr (ins!pc) G rT phi mxs max_pc et pc)" + (\pc. pc wt_instr (ins!pc) G rT phi mxs max_pc et pc))" +definition -- "A program is welltyped if it is wellformed and all methods are welltyped" - wt_jvm_prog :: "[jvm_prog,prog_type] \ bool" - "wt_jvm_prog G phi == + wt_jvm_prog :: "[jvm_prog,prog_type] \ bool" where + "wt_jvm_prog G phi \ wf_prog (\G C (sig,rT,(maxs,maxl,b,et)). wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G" diff -r 7c49988afd0e -r 982f3e02f3c4 src/HOL/MicroJava/JVM/JVMDefensive.thy --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Jun 11 17:14:01 2010 +0200 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Jun 11 17:14:01 2010 +0200 @@ -117,10 +117,10 @@ | Normal s' \ if check G s' then Normal (exec (G, s')) else TypeError" -constdefs +definition exec_all_d :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" - ("_ |- _ -jvmd-> _" [61,61,61]60) - "G |- s -jvmd-> t \ + ("_ |- _ -jvmd-> _" [61,61,61]60) where + "G |- s -jvmd-> t \ (s,t) \ ({(s,t). exec_d G s = TypeError \ t = TypeError} \ {(s,t). \t'. exec_d G s = Normal (Some t') \ t = Normal t'})\<^sup>*"