src/HOL/MicroJava/Comp/CorrComp.thy

   (characterized by class and signature) *)
 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)))"
+  (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)))"
 
 lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
 by (simp add: env_of_jmb_def split_beta)
 
 

 lemma wtpd_blk: 
   "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
   wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
  \<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
   apply (simp add: wtpd_stmt_def env_of_jmb_def)
-  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
+  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
      apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   done
 
 lemma wtpd_res: 
   "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
   wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
  \<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
   apply (simp add: wtpd_expr_def env_of_jmb_def)
-  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
+  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
      apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   done
 
 
 (**********************************************************************)

   (\<forall> lvals. 
   length lvars = length lvals \<longrightarrow>
    {cG, D, S} \<turnstile>
    {h, os, (a' # pvs @ lvals)}
    >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
-   {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
+   {h, os, (locvars_xstate G C S (Norm (h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))))})"
   apply (simp only: compInitLvars_def)
   apply (frule method_yields_wf_java_mdecl, assumption, assumption)
 
   apply (simp only: wf_java_mdecl_def)
   apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")

   "\<lbrakk> wf_java_prog G; (x, h, l)::\<preceq>(env_of_jmb G C S); 
   is_class G dynT;
   method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
   list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
   \<Longrightarrow>
-  (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
+  (np a' x, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
   apply (frule wf_prog_ws_prog)
   apply (frule method_in_md [THEN conjunct2], assumption+)
   apply (frule method_yields_wf_java_mdecl, assumption, assumption)
   apply (simp add: env_of_jmb_def gs_def conforms_def split_beta)
   apply (simp add: wf_java_mdecl_def)

             apply (simp only: drop_append)
             apply (simp (no_asm_simp))
            apply (simp (no_asm_simp))
 
           (* show s3::\<preceq>\<dots> *)
-          apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
+          apply (rule_tac xs = "(np a' x, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))" and st=blk in state_ok_exec)
              apply assumption
             apply (simp (no_asm_simp) only: env_of_jmb_fst)
            apply assumption
           apply (simp (no_asm_use) only: env_of_jmb_fst)