# HG changeset patch
# User schirmer
# Date 1052936958 -7200
# Node ID cd928c0ac225aa82077dc5fca27d02da8c219993
# Parent  fe031a7c75bcad55fe088e564d36d33dbd0fed6d
Adapted to changes in Map.thy

diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/AxExample.thy	Wed May 14 20:29:18 2003 +0200
@@ -130,12 +130,12 @@
 apply      (tactic "ax_tac 1" (* FVar *))
 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
 apply      (tactic "ax_tac 1")
-apply     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> hd vs = Null) \<and>. heap_free two)" *})
+apply     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
 apply     fastsimp
 prefer 4
 apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)
-apply   (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply   (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
 apply   (simp (no_asm) del: peek_and_def2)
 apply   (tactic "ax_tac 1")
 prefer 2
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/AxSound.thy	Wed May 14 20:29:18 2003 +0200
@@ -1557,10 +1557,25 @@
 	      from is_static_eq 
 	      have "(invmode (mthd dynM) e) = (invmode statM e)"
 		by (simp add: invmode_def)
-	      with s3 dynM' is_static_eq normal_s2 mode 
+	      moreover
+	      have "length (pars (mthd dynM)) = length vs" 
+	      proof -
+		from normal_s2 conf_args
+		have "length vs = length pTs"
+		  by (simp add: list_all2_def)
+		also from pTs_widen
+		have "\<dots> = length pTs'"
+		  by (simp add: widens_def list_all2_def)
+		also from wf_dynM
+		have "\<dots> = length (pars (mthd dynM))"
+		  by (simp add: wf_mdecl_def wf_mhead_def)
+		finally show ?thesis ..
+	      qed
+	      moreover note s3 dynM' is_static_eq normal_s2 mode 
+	      ultimately
 	      have "parameters (mthd dynM) = dom (locals (store s3))"
 		using dom_locals_init_lvars 
-                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
+                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
 		by simp
 	      thus ?thesis using eq_s3'_s3 by simp
 	    qed
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed May 14 20:29:18 2003 +0200
@@ -772,9 +772,9 @@
 constdefs 
 permits_acc:: 
  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
-                   ("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60)
+                   ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
 
-"G\<turnstile>membr in class permits_acc_to accclass 
+"G\<turnstile>membr in class permits_acc_from accclass 
   \<equiv> (case (accmodi membr) of
        Private   \<Rightarrow> (declclass membr = accclass)
      | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
@@ -849,7 +849,7 @@
 inductive "accessible_fromR G accclass" intros
 Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
               G\<turnstile>(Class class) accessible_in (pid accclass);
-              G\<turnstile>membr in class permits_acc_to accclass 
+              G\<turnstile>membr in class permits_acc_from accclass 
              \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
 
 Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
@@ -902,7 +902,7 @@
   
 inductive "dyn_accessible_fromR G accclass" intros
 Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
-              G\<turnstile>membr in class permits_acc_to accclass 
+              G\<turnstile>membr in class permits_acc_from accclass 
              \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
 
 Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
@@ -1141,15 +1141,15 @@
 by (induct set: overridesR) (auto simp add: inheritable_in_def)
 
 lemma permits_acc_inheritance:
- "\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
-  \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC"
+ "\<lbrakk>G\<turnstile>m in statC permits_acc_from accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
+  \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_from accC"
 by (cases "accmodi m")
    (auto simp add: permits_acc_def
             intro: subclseq_trans) 
 
 lemma permits_acc_static_declC:
- "\<lbrakk>G\<turnstile>m in C permits_acc_to accC; G\<turnstile>m member_in C; is_static m
-  \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_to accC"
+ "\<lbrakk>G\<turnstile>m in C permits_acc_from accC; G\<turnstile>m member_in C; is_static m
+  \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_from accC"
 by (cases "accmodi m") (auto simp add: permits_acc_def)
 
 lemma dyn_accessible_from_static_declC: 
@@ -1179,13 +1179,13 @@
  "\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 
   \<Longrightarrow> G\<turnstile>membr member_of C \<and>
       G\<turnstile>(Class C) accessible_in (pid accC) \<and>
-      G\<turnstile>membr in C permits_acc_to accC"
+      G\<turnstile>membr in C permits_acc_from accC"
 by (cases set: accessible_fromR)
    (auto simp add: is_field_def split: memberdecl.splits) 
 
 lemma field_accessible_from_permits_acc_inheritance:
 "\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk>
-\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC"
+\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_from accC"
 by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
 
 
@@ -1202,7 +1202,7 @@
   proof (induct rule: accessible_fromR.induct)
     fix C m
     assume "G\<turnstile>m member_of C"
-           "G \<turnstile> m in C permits_acc_to S"
+           "G \<turnstile> m in C permits_acc_from S"
            "accmodi m = Package"      
     then show "?P C m"
       by (auto dest: member_of_Package simp add: permits_acc_def)
@@ -1244,7 +1244,7 @@
  "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
  \<Longrightarrow> G\<turnstile>membr member_of C \<and>
      G\<turnstile>(Class C) accessible_in (pid accC) \<and>
-     G\<turnstile>membr in C permits_acc_to accC"
+     G\<turnstile>membr in C permits_acc_from accC"
 by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
       
 
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Wed May 14 20:29:18 2003 +0200
@@ -511,7 +511,7 @@
          nrm :: "lname set" --{* Definetly assigned variables 
                                  for normal completion*}
          brk :: "breakass" --{* Definetly assigned variables for 
-                                abnormal completion with a break *}
+                                abrupt completion with a break *}
 
 consts da :: "(env \<times> lname set \<times> term \<times> assigned) set"  
 text {* The environment @{term env} is only needed for the 
@@ -638,7 +638,7 @@
      and so we can't guarantee that any variable will be assigned in @{term c1}.
      The @{text Finally} statement completes
      normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
-     completes abnormally with a break, then @{term c2} also will be executed 
+     completes abruptly with a break, then @{term c2} also will be executed 
      and may terminate normally or with a break. The overall break map then is
      the intersection of the maps of both paths. If @{term c2} terminates 
      normally we have to extend all break sets in @{term "brk C1"} with 
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed May 14 20:29:18 2003 +0200
@@ -2851,11 +2851,6 @@
        wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
        wt_c2: "Env\<turnstile>c2\<Colon>\<surd>" 
       by (elim wt_elim_cases)
-    from wt_e da_e G
-    obtain nrm_s1: "?NormalAssigned s1 E" and 
-           brk_s1: "?BreakAssigned (Norm s0) s1 E" and
-           res_s1: "?ResAssigned (Norm s0) s1"
-      by (elim If.hyps [elim_format]) simp+
     from If.hyps have
      s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
       by (elim dom_locals_eval_mono_elim)
@@ -2930,7 +2925,7 @@
       then obtain abr where abr: "abrupt s1 = Some abr"
 	by (cases s1) auto
       moreover
-      from eval_e _ wt_e have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"
+      from eval_e _ wt_e have "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
 	by (rule eval_expression_no_jump) (simp_all add: G wf)
       moreover
       have "s2 = s1"
@@ -2939,7 +2934,7 @@
         with abr show ?thesis  
 	  by (cases s1) simp
       qed
-      ultimately show ?thesis using res_s1 by simp
+      ultimately show ?thesis by simp
     qed
   next
 -- {* 
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/Example.thy	Wed May 14 20:29:18 2003 +0200
@@ -697,7 +697,7 @@
 by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
 
 lemma Base_foo_permits_acc:
- "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
+ "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
 by ( simp add: permits_acc_def Base_foo_def)
 
 lemma Base_foo_accessible [simp]:
@@ -720,7 +720,7 @@
 done
 
 lemma Ext_foo_permits_acc:
- "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
+ "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
 by ( simp add: permits_acc_def Ext_foo_def)
 
 lemma Ext_foo_accessible [simp]:
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/ROOT.ML
--- a/src/HOL/Bali/ROOT.ML	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/ROOT.ML	Wed May 14 20:29:18 2003 +0200
@@ -1,4 +1,11 @@
-set timing;
+(*  Title:      isabelle/Bali/ROOT3.ML
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1999 Technische Universitaet Muenchen
+
+The Hoare logic for Bali
+*)
+
 update_thy "AxExample";
 update_thy "AxSound";
 update_thy "AxCompl";
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Wed May 14 20:29:18 2003 +0200
@@ -1230,54 +1230,23 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab tab' ys)
-  have "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z"
-    by (rule Cons.hyps) (rule map_upd_cong_ext)
-  thus ?case
-    by simp
+  note Hyps = this
+  show ?case
+  proof (cases ys)
+    case Nil
+    thus ?thesis by simp
+  next
+    case (Cons y ys')
+    have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
+      by (rules intro: Hyps map_upd_cong_ext)
+    with Cons show ?thesis
+      by simp
+  qed
 qed
    
 lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
   by simp
 
-
-lemma map_upds_override_cong:
-"\<And> tab tab' zs. x\<in> set ws \<Longrightarrow> 
- (tab(ws[\<mapsto>]zs)) x = (tab'(ws[\<mapsto>]zs)) x"
-proof (induct ws)
-  case Nil thus ?case by simp
-next
-  case (Cons w ws tab tab' zs)
-  have x: "x \<in> set (w#ws)" .
-  show ?case
-  proof (cases "x=w")
-    case True thus ?thesis
-      by simp (rule map_upds_cong_ext, rule map_upd_override)
-  next
-    case False
-    with x have "x \<in> set ws"
-      by simp
-    with Cons.hyps show ?thesis
-      by simp
-  qed
-qed
-
-lemma map_upds_in_suffix: assumes x: "x \<in> set xs" 
- shows "\<And> tab qs. (tab(ps @ xs[\<mapsto>]qs)) x = (tab(xs[\<mapsto>]drop (length ps) qs)) x"
-proof (induct ps)
-  case Nil thus ?case by simp
-next
-  case (Cons p ps tab qs)
-  have "(tab(p\<mapsto>hd qs)(ps @ xs[\<mapsto>](tl qs))) x
-          =(tab(p\<mapsto>hd qs)(xs[\<mapsto>]drop (length ps) (tl qs))) x"
-    by (rule Cons.hyps)
-  moreover
-  have "drop (Suc (length ps)) qs=drop (length ps) (tl qs)"
-    by (cases qs) simp+
-  ultimately show ?case
-    by simp (rule map_upds_override_cong)
-qed
- 
-
 lemma map_upds_eq_length_suffix: "\<And> tab qs. 
         length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
 proof (induct ps)
@@ -1327,13 +1296,21 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab ys z)
-  have "tab vn = Some z" .
-  then obtain z' where "(tab(x\<mapsto>hd ys)) vn = Some z'" 
-    by (rule map_upd_Some_expand [of tab,elim_format]) blast
-  hence "\<exists> z. (tab (x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
-    by (rule Cons.hyps)
-  thus ?case
-    by simp
+  have z: "tab vn = Some z" .
+  show ?case
+  proof (cases ys)
+    case Nil
+    with z show ?thesis by simp
+  next
+    case (Cons y ys')
+    have ys: "ys = y#ys'".
+    from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
+      by (rule map_upd_Some_expand [of tab,elim_format]) blast
+    hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
+      by (rule Cons.hyps)
+    with ys show ?thesis
+      by simp
+  qed
 qed
 
 
@@ -1349,22 +1326,6 @@
 lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
 by (simp add: fun_upd_def)
 
-lemma map_eq_upds_eq: 
-  "\<And> tab tab' ys. 
-   tab vn = tab' vn \<Longrightarrow> (tab(xs[\<mapsto>]ys)) vn = (tab'(xs[\<mapsto>]ys)) vn"
-proof (induct xs)
-  case Nil thus ?case by simp 
-next
-  case (Cons x xs tab tab' ys)
-  have "tab vn = tab' vn" .
-  hence "(tab(x\<mapsto>hd ys)) vn = (tab'(x\<mapsto>hd ys)) vn"
-    by (rule map_eq_upd_eq)
-  hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
-    by (rule Cons.hyps)
-  thus ?case 
-    by simp
-qed
-
 lemma map_upd_in_expansion_map_swap:
  "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
                  \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
@@ -1377,32 +1338,37 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab tab' ys z)
-  from Cons.prems obtain 
-    some: "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z" and
-    tab_not_z: "tab vn \<noteq> Some z"
-    by simp
+  have some: "(tab(x # xs[\<mapsto>]ys)) vn = Some z" .
+  have tab_not_z: "tab vn \<noteq> Some z".
   show ?case
-  proof (cases "(tab(x\<mapsto>hd ys)) vn \<noteq> Some z")
-    case True
-    with some have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
-      by (rule Cons.hyps)
-    thus ?thesis 
-      by simp
+  proof (cases "ys")
+    case Nil with some tab_not_z show ?thesis by simp
   next
-    case False
-    hence tabx_z: "(tab(x\<mapsto>hd ys)) vn = Some z" by blast
-    moreover
-    from tabx_z tab_not_z
-    have "(tab'(x\<mapsto>hd ys)) vn = Some z" 
-      by (rule map_upd_in_expansion_map_swap)
-    ultimately
-    have "(tab(x\<mapsto>hd ys)) vn =(tab'(x\<mapsto>hd ys)) vn"
-      by simp
-    hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
-      by (rule map_eq_upds_eq)
-    with some 
-    show ?thesis 
-      by simp
+    case (Cons y tl)
+    have ys: "ys = y#tl".
+    show ?thesis
+    proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
+      case True
+      with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
+	by (fastsimp intro: Cons.hyps)
+      with ys show ?thesis 
+	by simp
+    next
+      case False
+      hence tabx_z: "(tab(x\<mapsto>y)) vn = Some z" by blast
+      moreover
+      from tabx_z tab_not_z
+      have "(tab'(x\<mapsto>y)) vn = Some z" 
+	by (rule map_upd_in_expansion_map_swap)
+      ultimately
+      have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
+	by simp
+      hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
+	by (rule map_upds_cong_ext)
+      with some ys
+      show ?thesis 
+	by simp
+    qed
   qed
 qed
    
@@ -1464,17 +1430,28 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab tab' ys)
-  from Cons.prems
-  have "(tab(x\<mapsto>hd ys)) vn = Some el"
-    by - (rule Cons.hyps,auto)
-  moreover from Cons.prems 
-  have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = None" 
-    by simp
-  hence "(tab'(x\<mapsto>hd ys)) vn = None"
-    by (rule map_upds_None_cut)
-  ultimately show "tab vn = Some el" 
-    by (rule map_upd_cut_irrelevant)
+  have tab_vn: "(tab(x # xs[\<mapsto>]ys)) vn = Some el".
+  have tab'_vn: "(tab'(x # xs[\<mapsto>]ys)) vn = None".
+  show ?case
+  proof (cases ys)
+    case Nil
+    with tab_vn show ?thesis by simp
+  next
+    case (Cons y tl)
+    have ys: "ys=y#tl".
+    with tab_vn tab'_vn 
+    have "(tab(x\<mapsto>y)) vn = Some el"
+      by - (rule Cons.hyps,auto)
+    moreover from tab'_vn ys
+    have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
+      by simp
+    hence "(tab'(x\<mapsto>y)) vn = None"
+      by (rule map_upds_None_cut)
+    ultimately show "tab vn = Some el" 
+      by (rule map_upd_cut_irrelevant)
+  qed
 qed
+
    
 lemma dom_vname_split:
  "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
@@ -1531,22 +1508,30 @@
 lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
 by (auto simp add: dom_def fun_upd_def)
 
-lemma dom_map_upds: "\<And> tab ys. dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
+lemma dom_map_upds: "\<And> tab ys. length xs = length ys 
+  \<Longrightarrow> dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
 proof (induct xs)
   case Nil thus ?case by (simp add: dom_def)
 next
   case (Cons x xs tab ys)
-  have "dom (tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) = dom (tab(x\<mapsto>hd ys)) \<union> set xs" .
-  moreover 
-  have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
-    by (rule dom_map_upd)
-  ultimately
+  note Hyp = Cons.hyps
+  have len: "length (x#xs)=length ys".
   show ?case
-    by simp
+  proof (cases ys)
+    case Nil with len show ?thesis by simp
+  next
+    case (Cons y tl)
+    with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
+      by - (rule Hyp,simp)
+    moreover 
+    have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
+      by (rule dom_map_upd)
+    ultimately
+    show ?thesis using Cons
+      by simp
+  qed
 qed
  
-
-
 lemma dom_ename_case_None_simp:
  "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
   apply (auto simp add: dom_def image_def )
@@ -1583,14 +1568,17 @@
  "f ` g ` A = (f \<circ> g) ` A"
 by (auto simp add: image_def)
 
+
 lemma dom_locals_init_lvars: 
   assumes m: "m=(mthd (the (methd G C sig)))"  
+  assumes len: "length (pars m) = length pvs"
   shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
            = parameters m"
 proof -
   from m
   have static_m': "is_static m = static m"
     by simp
+  from len
   have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
     by (simp add: dom_map_upds)
   show ?thesis
@@ -1609,6 +1597,7 @@
   qed
 qed
 
+
 lemma da_e2_BinOp:
   assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
@@ -3283,10 +3272,25 @@
 	      from is_static_eq 
 	      have "(invmode (mthd dynM) e) = (invmode statM e)"
 		by (simp add: invmode_def)
-	      with init_lvars dynM' is_static_eq normal_s2 mode 
+	      moreover
+	      have "length (pars (mthd dynM)) = length vs" 
+	      proof -
+		from normal_s2 conf_args
+		have "length vs = length pTs"
+		  by (simp add: list_all2_def)
+		also from pTs_widen
+		have "\<dots> = length pTs'"
+		  by (simp add: widens_def list_all2_def)
+		also from wf_dynM
+		have "\<dots> = length (pars (mthd dynM))"
+		  by (simp add: wf_mdecl_def wf_mhead_def)
+		finally show ?thesis ..
+	      qed
+	      moreover note init_lvars dynM' is_static_eq normal_s2 mode 
+	      ultimately
 	      have "parameters (mthd dynM) = dom (locals (store s3))"
 		using dom_locals_init_lvars 
-                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
+                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
 		by simp
 	      also from check
 	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/WellForm.thy	Wed May 14 20:29:18 2003 +0200
@@ -509,7 +509,8 @@
 A program declaration is wellformed if:
 \begin{itemize}
 \item the class ObjectC of Object is defined
-\item every method of has an access modifier distinct from Package. This is
+\item every method of Object has an access modifier distinct from Package. 
+      This is
       necessary since every interface automatically inherits from Object.  
       We must know, that every time a Object method is "overriden" by an 
       interface method this is also overriden by the class implementing the
@@ -2922,7 +2923,7 @@
   show ?thesis
   proof (induct)
     case (Immediate C m)
-    have "G \<turnstile> m in C permits_acc_to accC" and "accmodi m = Private" .
+    have "G \<turnstile> m in C permits_acc_from accC" and "accmodi m = Private" .
     then show ?case
       by (simp add: permits_acc_def)
   next
@@ -2948,7 +2949,7 @@
   proof (induct rule: dyn_accessible_fromR.induct)
     case (Immediate C m)
     assume "G\<turnstile>m member_in C"
-           "G \<turnstile> m in C permits_acc_to accC"
+           "G \<turnstile> m in C permits_acc_from accC"
            "accmodi m = Package"      
     then show "?P m"
       by (auto simp add: permits_acc_def)
@@ -2987,7 +2988,7 @@
   show ?thesis
   proof (induct)
     case (Immediate C f)
-    have "G \<turnstile> f in C permits_acc_to accC" and "accmodi f = Package" .
+    have "G \<turnstile> f in C permits_acc_from accC" and "accmodi f = Package" .
     then show ?case
       by (simp add: permits_acc_def)
   next
@@ -3011,7 +3012,7 @@
   show ?thesis
   proof (induct)
     case (Immediate C f)
-    have "G \<turnstile> f in C permits_acc_to accC" .
+    have "G \<turnstile> f in C permits_acc_from accC" .
     moreover 
     assume "accmodi f = Protected" and  "is_field f" and "\<not> is_static f" and
            "pid (declclass f) \<noteq> pid accC"
@@ -3039,7 +3040,7 @@
     assume "accmodi f = Protected" and  "is_field f" and "is_static f" and
            "pid (declclass f) \<noteq> pid accC"
     moreover 
-    have "G \<turnstile> f in C permits_acc_to accC" .
+    have "G \<turnstile> f in C permits_acc_from accC" .
     ultimately
     have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
       by (auto simp add: permits_acc_def)