src/HOL/MicroJava/Comp/CorrComp.thy

 done
 
 
 (***********************************************************************)
 
-constdefs
-  progression :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
+definition progression :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
                  aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow>
                  bytecode \<Rightarrow>
                  aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow> 
                  bool"
-  ("{_,_,_} \<turnstile> {_, _, _} >- _ \<rightarrow> {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60)
+  ("{_,_,_} \<turnstile> {_, _, _} >- _ \<rightarrow> {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60) where
   "{G,C,S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1} ==
   \<forall> pre post frs.
   (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow>
    G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) -jvm\<rightarrow>
        (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)"

 apply (rule exec_all_one_step)
 apply auto
 done
 
 (*****)
-constdefs
-  jump_fwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
+definition jump_fwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
                  aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
-                 instr \<Rightarrow> bytecode \<Rightarrow> bool"
+                 instr \<Rightarrow> bytecode \<Rightarrow> bool" where
   "jump_fwd G C S hp lvars os0 os1 instr instrs ==
   \<forall> pre post frs.
   (gis (gmb G C S) = pre @ instr # instrs @ post) \<longrightarrow>
    exec_all G (None,hp,(os0,lvars,C,S, length pre)#frs)
     (None,hp,(os1,lvars,C,S,(length pre) + (length instrs) + 1)#frs)"

 apply (rule jump_fwd_one_step) apply assumption+
 done
 
 
 (* note: instrs and instr reversed wrt. jump_fwd *)
-constdefs
-  jump_bwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
+definition jump_bwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
                  aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
-                 bytecode \<Rightarrow> instr \<Rightarrow> bool"
+                 bytecode \<Rightarrow> instr \<Rightarrow> bool" where
   "jump_bwd G C S hp lvars os0 os1 instrs instr ==
   \<forall> pre post frs.
   (gis (gmb G C S) = pre @ instrs @ instr # post) \<longrightarrow>
    exec_all G (None,hp,(os0,lvars,C,S, (length pre) + (length instrs))#frs)
     (None,hp,(os1,lvars,C,S, (length pre))#frs)"

 
 
 (**********************************************************************)
 
 (* class C with signature S is defined in program G *)
-constdefs class_sig_defined :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> bool"
+definition class_sig_defined :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> bool" where
   "class_sig_defined G C S == 
   is_class G C \<and> (\<exists> D rT mb. (method (G, C) S = Some (D, rT, mb)))"
 
 
 (* The environment of a java method body 
   (characterized by class and signature) *)
-constdefs env_of_jmb :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> java_mb env"
+definition env_of_jmb :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> java_mb env" where
   "env_of_jmb G C S == 
   (let (mn,pTs) = S;
        (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
   (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"
 

 apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
 done
 
 (**********************************************************************)
 
-constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool"
+definition wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool" where
   "wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)"
-  wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool"
+
+definition wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool" where
   "wtpd_exprs E e == (\<exists> T. E\<turnstile>e [::] T)"
-  wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" 
+
+definition wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" where
   "wtpd_stmt E c == (E\<turnstile>c \<surd>)"
 
 lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \<Longrightarrow> is_class (prg E) C"
 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)