--- 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 \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
- "decliface \<equiv> fst" --{* get the interface component *}
+-- {* some mnemotic selectors for various pairs *}
+
+definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
+ "decliface = fst" --{* get the interface component *}
- "mbr":: "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
- "mbr \<equiv> snd" --{* get the memberdecl component *}
+definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
+ "mbr = snd" --{* get the memberdecl component *}
- "mthd":: "('b \<times> 'a) \<Rightarrow> 'a"
- --{* also used for mdecl, mhead *}
- "mthd \<equiv> snd" --{* get the method component *}
+definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
+ "mthd = snd" --{* get the method component *}
+ --{* also used for mdecl, mhead *}
- "fld":: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
- --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
- "fld \<equiv> snd" --{* get the field component *}
+definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
+ "fld = snd" --{* get the field component *}
+ --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
+-- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
-constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
- fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
- "fname \<equiv> fst"
-
- declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
- "declclassf \<equiv> snd"
+definition fname:: "vname \<times> 'a \<Rightarrow> vname" where
+ "fname = fst"
+ --{* also used for fdecl *}
+definition declclassf:: "(vname \<times> qtname) \<Rightarrow> 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 \<times> qtname)"} *}
- "fldname" :: "(vname \<times> qtname) \<Rightarrow> vname"
- "fldname \<equiv> fst"
+ --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
- "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
- "fldclass \<equiv> snd"
+definition fldname :: "vname \<times> qtname \<Rightarrow> vname" where
+ "fldname = fst"
+
+definition fldclass :: "vname \<times> qtname \<Rightarrow> 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 \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" where
- "methdMembr m \<equiv> (fst m,mdecl (snd m))"
+definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
+ "methdMembr m = (fst m, mdecl (snd m))"
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
by (simp add: methdMembr_def)
--- 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 \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
- "appl_methds G S rt \<equiv> \<lambda> sig.
+ appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "appl_methds G S rt = (\<lambda> sig.
{(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and>
- G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
+ G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
+definition
--{* more specific methods, cf. 15.11.2.2 *}
- more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
- "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
+ more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
+ "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
+definition
--{* maximally specific methods, cf. 15.11.2.2 *}
- max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
-
- "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
+ max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
--- 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 \<Rightarrow> exception_table \<Rightarrow> bool"
- "check_bounded ins et \<equiv>
+ check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool" where
+ "check_bounded ins et \<longleftrightarrow>
(\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
(\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
+definition
-- "The method type only contains declared classes:"
- check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
- "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
+ check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where
+ "check_types G mxs mxr phi \<longleftrightarrow> set phi \<subseteq> 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] \<Rightarrow> bool"
- "wt_instr i G rT phi mxs max_pc et pc \<equiv>
+ exception_table,p_count] \<Rightarrow> bool" where
+ "wt_instr i G rT phi mxs max_pc et pc \<longleftrightarrow>
app i G mxs rT pc et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> 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] \<Rightarrow> bool"
- "wt_start G C pTs mxl phi ==
+ wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where
+ "wt_start G C pTs mxl phi \<longleftrightarrow>
G \<turnstile> 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] \<Rightarrow> bool"
- "wt_method G C pTs rT mxs mxl ins et phi \<equiv>
- let max_pc = length ins in
+ exception_table,method_type] \<Rightarrow> bool" where
+ "wt_method G C pTs rT mxs mxl ins et phi \<longleftrightarrow>
+ (let max_pc = length ins in
0 < max_pc \<and>
length phi = length ins \<and>
check_bounded ins et \<and>
check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc)"
+ (\<forall>pc. pc<max_pc \<longrightarrow> 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] \<Rightarrow> bool"
- "wt_jvm_prog G phi ==
+ wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool" where
+ "wt_jvm_prog G phi \<longleftrightarrow>
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
--- 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' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
-constdefs
+definition
exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
- ("_ |- _ -jvmd-> _" [61,61,61]60)
- "G |- s -jvmd-> t \<equiv>
+ ("_ |- _ -jvmd-> _" [61,61,61]60) where
+ "G |- s -jvmd-> t \<longleftrightarrow>
(s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
{(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"