Adapted to changes in Map.thy
authorschirmer
Wed May 14 20:29:18 2003 +0200 (2003-05-14)
changeset 14030cd928c0ac225
parent 14029 fe031a7c75bc
child 14031 3240066af013
Adapted to changes in Map.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/ROOT.ML
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
     1.1 --- a/src/HOL/Bali/AxExample.thy	Wed May 14 15:22:37 2003 +0200
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Wed May 14 20:29:18 2003 +0200
     1.3 @@ -130,12 +130,12 @@
     1.4  apply      (tactic "ax_tac 1" (* FVar *))
     1.5  apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
     1.6  apply      (tactic "ax_tac 1")
     1.7 -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)" *})
     1.8 +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)" *})
     1.9  apply     fastsimp
    1.10  prefer 4
    1.11  apply    (rule ax_derivs.Done [THEN conseq1],force)
    1.12  apply   (rule ax_subst_Val_allI)
    1.13 -apply   (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
    1.14 +apply   (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
    1.15  apply   (simp (no_asm) del: peek_and_def2)
    1.16  apply   (tactic "ax_tac 1")
    1.17  prefer 2
     2.1 --- a/src/HOL/Bali/AxSound.thy	Wed May 14 15:22:37 2003 +0200
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Wed May 14 20:29:18 2003 +0200
     2.3 @@ -1557,10 +1557,25 @@
     2.4  	      from is_static_eq 
     2.5  	      have "(invmode (mthd dynM) e) = (invmode statM e)"
     2.6  		by (simp add: invmode_def)
     2.7 -	      with s3 dynM' is_static_eq normal_s2 mode 
     2.8 +	      moreover
     2.9 +	      have "length (pars (mthd dynM)) = length vs" 
    2.10 +	      proof -
    2.11 +		from normal_s2 conf_args
    2.12 +		have "length vs = length pTs"
    2.13 +		  by (simp add: list_all2_def)
    2.14 +		also from pTs_widen
    2.15 +		have "\<dots> = length pTs'"
    2.16 +		  by (simp add: widens_def list_all2_def)
    2.17 +		also from wf_dynM
    2.18 +		have "\<dots> = length (pars (mthd dynM))"
    2.19 +		  by (simp add: wf_mdecl_def wf_mhead_def)
    2.20 +		finally show ?thesis ..
    2.21 +	      qed
    2.22 +	      moreover note s3 dynM' is_static_eq normal_s2 mode 
    2.23 +	      ultimately
    2.24  	      have "parameters (mthd dynM) = dom (locals (store s3))"
    2.25  		using dom_locals_init_lvars 
    2.26 -                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
    2.27 +                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
    2.28  		by simp
    2.29  	      thus ?thesis using eq_s3'_s3 by simp
    2.30  	    qed
     3.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed May 14 15:22:37 2003 +0200
     3.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed May 14 20:29:18 2003 +0200
     3.3 @@ -772,9 +772,9 @@
     3.4  constdefs 
     3.5  permits_acc:: 
     3.6   "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
     3.7 -                   ("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60)
     3.8 +                   ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
     3.9  
    3.10 -"G\<turnstile>membr in class permits_acc_to accclass 
    3.11 +"G\<turnstile>membr in class permits_acc_from accclass 
    3.12    \<equiv> (case (accmodi membr) of
    3.13         Private   \<Rightarrow> (declclass membr = accclass)
    3.14       | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
    3.15 @@ -849,7 +849,7 @@
    3.16  inductive "accessible_fromR G accclass" intros
    3.17  Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
    3.18                G\<turnstile>(Class class) accessible_in (pid accclass);
    3.19 -              G\<turnstile>membr in class permits_acc_to accclass 
    3.20 +              G\<turnstile>membr in class permits_acc_from accclass 
    3.21               \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
    3.22  
    3.23  Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
    3.24 @@ -902,7 +902,7 @@
    3.25    
    3.26  inductive "dyn_accessible_fromR G accclass" intros
    3.27  Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
    3.28 -              G\<turnstile>membr in class permits_acc_to accclass 
    3.29 +              G\<turnstile>membr in class permits_acc_from accclass 
    3.30               \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
    3.31  
    3.32  Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
    3.33 @@ -1141,15 +1141,15 @@
    3.34  by (induct set: overridesR) (auto simp add: inheritable_in_def)
    3.35  
    3.36  lemma permits_acc_inheritance:
    3.37 - "\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
    3.38 -  \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC"
    3.39 + "\<lbrakk>G\<turnstile>m in statC permits_acc_from accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
    3.40 +  \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_from accC"
    3.41  by (cases "accmodi m")
    3.42     (auto simp add: permits_acc_def
    3.43              intro: subclseq_trans) 
    3.44  
    3.45  lemma permits_acc_static_declC:
    3.46 - "\<lbrakk>G\<turnstile>m in C permits_acc_to accC; G\<turnstile>m member_in C; is_static m
    3.47 -  \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_to accC"
    3.48 + "\<lbrakk>G\<turnstile>m in C permits_acc_from accC; G\<turnstile>m member_in C; is_static m
    3.49 +  \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_from accC"
    3.50  by (cases "accmodi m") (auto simp add: permits_acc_def)
    3.51  
    3.52  lemma dyn_accessible_from_static_declC: 
    3.53 @@ -1179,13 +1179,13 @@
    3.54   "\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 
    3.55    \<Longrightarrow> G\<turnstile>membr member_of C \<and>
    3.56        G\<turnstile>(Class C) accessible_in (pid accC) \<and>
    3.57 -      G\<turnstile>membr in C permits_acc_to accC"
    3.58 +      G\<turnstile>membr in C permits_acc_from accC"
    3.59  by (cases set: accessible_fromR)
    3.60     (auto simp add: is_field_def split: memberdecl.splits) 
    3.61  
    3.62  lemma field_accessible_from_permits_acc_inheritance:
    3.63  "\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk>
    3.64 -\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC"
    3.65 +\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_from accC"
    3.66  by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
    3.67  
    3.68  
    3.69 @@ -1202,7 +1202,7 @@
    3.70    proof (induct rule: accessible_fromR.induct)
    3.71      fix C m
    3.72      assume "G\<turnstile>m member_of C"
    3.73 -           "G \<turnstile> m in C permits_acc_to S"
    3.74 +           "G \<turnstile> m in C permits_acc_from S"
    3.75             "accmodi m = Package"      
    3.76      then show "?P C m"
    3.77        by (auto dest: member_of_Package simp add: permits_acc_def)
    3.78 @@ -1244,7 +1244,7 @@
    3.79   "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
    3.80   \<Longrightarrow> G\<turnstile>membr member_of C \<and>
    3.81       G\<turnstile>(Class C) accessible_in (pid accC) \<and>
    3.82 -     G\<turnstile>membr in C permits_acc_to accC"
    3.83 +     G\<turnstile>membr in C permits_acc_from accC"
    3.84  by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
    3.85        
    3.86  
     4.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Wed May 14 15:22:37 2003 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Wed May 14 20:29:18 2003 +0200
     4.3 @@ -511,7 +511,7 @@
     4.4           nrm :: "lname set" --{* Definetly assigned variables 
     4.5                                   for normal completion*}
     4.6           brk :: "breakass" --{* Definetly assigned variables for 
     4.7 -                                abnormal completion with a break *}
     4.8 +                                abrupt completion with a break *}
     4.9  
    4.10  consts da :: "(env \<times> lname set \<times> term \<times> assigned) set"  
    4.11  text {* The environment @{term env} is only needed for the 
    4.12 @@ -638,7 +638,7 @@
    4.13       and so we can't guarantee that any variable will be assigned in @{term c1}.
    4.14       The @{text Finally} statement completes
    4.15       normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
    4.16 -     completes abnormally with a break, then @{term c2} also will be executed 
    4.17 +     completes abruptly with a break, then @{term c2} also will be executed 
    4.18       and may terminate normally or with a break. The overall break map then is
    4.19       the intersection of the maps of both paths. If @{term c2} terminates 
    4.20       normally we have to extend all break sets in @{term "brk C1"} with 
     5.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed May 14 15:22:37 2003 +0200
     5.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed May 14 20:29:18 2003 +0200
     5.3 @@ -2851,11 +2851,6 @@
     5.4         wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
     5.5         wt_c2: "Env\<turnstile>c2\<Colon>\<surd>" 
     5.6        by (elim wt_elim_cases)
     5.7 -    from wt_e da_e G
     5.8 -    obtain nrm_s1: "?NormalAssigned s1 E" and 
     5.9 -           brk_s1: "?BreakAssigned (Norm s0) s1 E" and
    5.10 -           res_s1: "?ResAssigned (Norm s0) s1"
    5.11 -      by (elim If.hyps [elim_format]) simp+
    5.12      from If.hyps have
    5.13       s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
    5.14        by (elim dom_locals_eval_mono_elim)
    5.15 @@ -2930,7 +2925,7 @@
    5.16        then obtain abr where abr: "abrupt s1 = Some abr"
    5.17  	by (cases s1) auto
    5.18        moreover
    5.19 -      from eval_e _ wt_e have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"
    5.20 +      from eval_e _ wt_e have "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
    5.21  	by (rule eval_expression_no_jump) (simp_all add: G wf)
    5.22        moreover
    5.23        have "s2 = s1"
    5.24 @@ -2939,7 +2934,7 @@
    5.25          with abr show ?thesis  
    5.26  	  by (cases s1) simp
    5.27        qed
    5.28 -      ultimately show ?thesis using res_s1 by simp
    5.29 +      ultimately show ?thesis by simp
    5.30      qed
    5.31    next
    5.32  -- {* 
     6.1 --- a/src/HOL/Bali/Example.thy	Wed May 14 15:22:37 2003 +0200
     6.2 +++ b/src/HOL/Bali/Example.thy	Wed May 14 20:29:18 2003 +0200
     6.3 @@ -697,7 +697,7 @@
     6.4  by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
     6.5  
     6.6  lemma Base_foo_permits_acc:
     6.7 - "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
     6.8 + "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
     6.9  by ( simp add: permits_acc_def Base_foo_def)
    6.10  
    6.11  lemma Base_foo_accessible [simp]:
    6.12 @@ -720,7 +720,7 @@
    6.13  done
    6.14  
    6.15  lemma Ext_foo_permits_acc:
    6.16 - "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
    6.17 + "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
    6.18  by ( simp add: permits_acc_def Ext_foo_def)
    6.19  
    6.20  lemma Ext_foo_accessible [simp]:
     7.1 --- a/src/HOL/Bali/ROOT.ML	Wed May 14 15:22:37 2003 +0200
     7.2 +++ b/src/HOL/Bali/ROOT.ML	Wed May 14 20:29:18 2003 +0200
     7.3 @@ -1,4 +1,11 @@
     7.4 -set timing;
     7.5 +(*  Title:      isabelle/Bali/ROOT3.ML
     7.6 +    ID:         $Id$
     7.7 +    Author:     David von Oheimb
     7.8 +    Copyright   1999 Technische Universitaet Muenchen
     7.9 +
    7.10 +The Hoare logic for Bali
    7.11 +*)
    7.12 +
    7.13  update_thy "AxExample";
    7.14  update_thy "AxSound";
    7.15  update_thy "AxCompl";
     8.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed May 14 15:22:37 2003 +0200
     8.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed May 14 20:29:18 2003 +0200
     8.3 @@ -1230,54 +1230,23 @@
     8.4    case Nil thus ?case by simp
     8.5  next
     8.6    case (Cons x xs tab tab' ys)
     8.7 -  have "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z"
     8.8 -    by (rule Cons.hyps) (rule map_upd_cong_ext)
     8.9 -  thus ?case
    8.10 -    by simp
    8.11 +  note Hyps = this
    8.12 +  show ?case
    8.13 +  proof (cases ys)
    8.14 +    case Nil
    8.15 +    thus ?thesis by simp
    8.16 +  next
    8.17 +    case (Cons y ys')
    8.18 +    have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
    8.19 +      by (rules intro: Hyps map_upd_cong_ext)
    8.20 +    with Cons show ?thesis
    8.21 +      by simp
    8.22 +  qed
    8.23  qed
    8.24     
    8.25  lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
    8.26    by simp
    8.27  
    8.28 -
    8.29 -lemma map_upds_override_cong:
    8.30 -"\<And> tab tab' zs. x\<in> set ws \<Longrightarrow> 
    8.31 - (tab(ws[\<mapsto>]zs)) x = (tab'(ws[\<mapsto>]zs)) x"
    8.32 -proof (induct ws)
    8.33 -  case Nil thus ?case by simp
    8.34 -next
    8.35 -  case (Cons w ws tab tab' zs)
    8.36 -  have x: "x \<in> set (w#ws)" .
    8.37 -  show ?case
    8.38 -  proof (cases "x=w")
    8.39 -    case True thus ?thesis
    8.40 -      by simp (rule map_upds_cong_ext, rule map_upd_override)
    8.41 -  next
    8.42 -    case False
    8.43 -    with x have "x \<in> set ws"
    8.44 -      by simp
    8.45 -    with Cons.hyps show ?thesis
    8.46 -      by simp
    8.47 -  qed
    8.48 -qed
    8.49 -
    8.50 -lemma map_upds_in_suffix: assumes x: "x \<in> set xs" 
    8.51 - shows "\<And> tab qs. (tab(ps @ xs[\<mapsto>]qs)) x = (tab(xs[\<mapsto>]drop (length ps) qs)) x"
    8.52 -proof (induct ps)
    8.53 -  case Nil thus ?case by simp
    8.54 -next
    8.55 -  case (Cons p ps tab qs)
    8.56 -  have "(tab(p\<mapsto>hd qs)(ps @ xs[\<mapsto>](tl qs))) x
    8.57 -          =(tab(p\<mapsto>hd qs)(xs[\<mapsto>]drop (length ps) (tl qs))) x"
    8.58 -    by (rule Cons.hyps)
    8.59 -  moreover
    8.60 -  have "drop (Suc (length ps)) qs=drop (length ps) (tl qs)"
    8.61 -    by (cases qs) simp+
    8.62 -  ultimately show ?case
    8.63 -    by simp (rule map_upds_override_cong)
    8.64 -qed
    8.65 - 
    8.66 -
    8.67  lemma map_upds_eq_length_suffix: "\<And> tab qs. 
    8.68          length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
    8.69  proof (induct ps)
    8.70 @@ -1327,13 +1296,21 @@
    8.71    case Nil thus ?case by simp
    8.72  next
    8.73    case (Cons x xs tab ys z)
    8.74 -  have "tab vn = Some z" .
    8.75 -  then obtain z' where "(tab(x\<mapsto>hd ys)) vn = Some z'" 
    8.76 -    by (rule map_upd_Some_expand [of tab,elim_format]) blast
    8.77 -  hence "\<exists> z. (tab (x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
    8.78 -    by (rule Cons.hyps)
    8.79 -  thus ?case
    8.80 -    by simp
    8.81 +  have z: "tab vn = Some z" .
    8.82 +  show ?case
    8.83 +  proof (cases ys)
    8.84 +    case Nil
    8.85 +    with z show ?thesis by simp
    8.86 +  next
    8.87 +    case (Cons y ys')
    8.88 +    have ys: "ys = y#ys'".
    8.89 +    from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
    8.90 +      by (rule map_upd_Some_expand [of tab,elim_format]) blast
    8.91 +    hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
    8.92 +      by (rule Cons.hyps)
    8.93 +    with ys show ?thesis
    8.94 +      by simp
    8.95 +  qed
    8.96  qed
    8.97  
    8.98  
    8.99 @@ -1349,22 +1326,6 @@
   8.100  lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
   8.101  by (simp add: fun_upd_def)
   8.102  
   8.103 -lemma map_eq_upds_eq: 
   8.104 -  "\<And> tab tab' ys. 
   8.105 -   tab vn = tab' vn \<Longrightarrow> (tab(xs[\<mapsto>]ys)) vn = (tab'(xs[\<mapsto>]ys)) vn"
   8.106 -proof (induct xs)
   8.107 -  case Nil thus ?case by simp 
   8.108 -next
   8.109 -  case (Cons x xs tab tab' ys)
   8.110 -  have "tab vn = tab' vn" .
   8.111 -  hence "(tab(x\<mapsto>hd ys)) vn = (tab'(x\<mapsto>hd ys)) vn"
   8.112 -    by (rule map_eq_upd_eq)
   8.113 -  hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
   8.114 -    by (rule Cons.hyps)
   8.115 -  thus ?case 
   8.116 -    by simp
   8.117 -qed
   8.118 -
   8.119  lemma map_upd_in_expansion_map_swap:
   8.120   "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
   8.121                   \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
   8.122 @@ -1377,32 +1338,37 @@
   8.123    case Nil thus ?case by simp
   8.124  next
   8.125    case (Cons x xs tab tab' ys z)
   8.126 -  from Cons.prems obtain 
   8.127 -    some: "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z" and
   8.128 -    tab_not_z: "tab vn \<noteq> Some z"
   8.129 -    by simp
   8.130 +  have some: "(tab(x # xs[\<mapsto>]ys)) vn = Some z" .
   8.131 +  have tab_not_z: "tab vn \<noteq> Some z".
   8.132    show ?case
   8.133 -  proof (cases "(tab(x\<mapsto>hd ys)) vn \<noteq> Some z")
   8.134 -    case True
   8.135 -    with some have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
   8.136 -      by (rule Cons.hyps)
   8.137 -    thus ?thesis 
   8.138 -      by simp
   8.139 +  proof (cases "ys")
   8.140 +    case Nil with some tab_not_z show ?thesis by simp
   8.141    next
   8.142 -    case False
   8.143 -    hence tabx_z: "(tab(x\<mapsto>hd ys)) vn = Some z" by blast
   8.144 -    moreover
   8.145 -    from tabx_z tab_not_z
   8.146 -    have "(tab'(x\<mapsto>hd ys)) vn = Some z" 
   8.147 -      by (rule map_upd_in_expansion_map_swap)
   8.148 -    ultimately
   8.149 -    have "(tab(x\<mapsto>hd ys)) vn =(tab'(x\<mapsto>hd ys)) vn"
   8.150 -      by simp
   8.151 -    hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
   8.152 -      by (rule map_eq_upds_eq)
   8.153 -    with some 
   8.154 -    show ?thesis 
   8.155 -      by simp
   8.156 +    case (Cons y tl)
   8.157 +    have ys: "ys = y#tl".
   8.158 +    show ?thesis
   8.159 +    proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
   8.160 +      case True
   8.161 +      with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
   8.162 +	by (fastsimp intro: Cons.hyps)
   8.163 +      with ys show ?thesis 
   8.164 +	by simp
   8.165 +    next
   8.166 +      case False
   8.167 +      hence tabx_z: "(tab(x\<mapsto>y)) vn = Some z" by blast
   8.168 +      moreover
   8.169 +      from tabx_z tab_not_z
   8.170 +      have "(tab'(x\<mapsto>y)) vn = Some z" 
   8.171 +	by (rule map_upd_in_expansion_map_swap)
   8.172 +      ultimately
   8.173 +      have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
   8.174 +	by simp
   8.175 +      hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
   8.176 +	by (rule map_upds_cong_ext)
   8.177 +      with some ys
   8.178 +      show ?thesis 
   8.179 +	by simp
   8.180 +    qed
   8.181    qed
   8.182  qed
   8.183     
   8.184 @@ -1464,17 +1430,28 @@
   8.185    case Nil thus ?case by simp
   8.186  next
   8.187    case (Cons x xs tab tab' ys)
   8.188 -  from Cons.prems
   8.189 -  have "(tab(x\<mapsto>hd ys)) vn = Some el"
   8.190 -    by - (rule Cons.hyps,auto)
   8.191 -  moreover from Cons.prems 
   8.192 -  have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = None" 
   8.193 -    by simp
   8.194 -  hence "(tab'(x\<mapsto>hd ys)) vn = None"
   8.195 -    by (rule map_upds_None_cut)
   8.196 -  ultimately show "tab vn = Some el" 
   8.197 -    by (rule map_upd_cut_irrelevant)
   8.198 +  have tab_vn: "(tab(x # xs[\<mapsto>]ys)) vn = Some el".
   8.199 +  have tab'_vn: "(tab'(x # xs[\<mapsto>]ys)) vn = None".
   8.200 +  show ?case
   8.201 +  proof (cases ys)
   8.202 +    case Nil
   8.203 +    with tab_vn show ?thesis by simp
   8.204 +  next
   8.205 +    case (Cons y tl)
   8.206 +    have ys: "ys=y#tl".
   8.207 +    with tab_vn tab'_vn 
   8.208 +    have "(tab(x\<mapsto>y)) vn = Some el"
   8.209 +      by - (rule Cons.hyps,auto)
   8.210 +    moreover from tab'_vn ys
   8.211 +    have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
   8.212 +      by simp
   8.213 +    hence "(tab'(x\<mapsto>y)) vn = None"
   8.214 +      by (rule map_upds_None_cut)
   8.215 +    ultimately show "tab vn = Some el" 
   8.216 +      by (rule map_upd_cut_irrelevant)
   8.217 +  qed
   8.218  qed
   8.219 +
   8.220     
   8.221  lemma dom_vname_split:
   8.222   "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
   8.223 @@ -1531,22 +1508,30 @@
   8.224  lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
   8.225  by (auto simp add: dom_def fun_upd_def)
   8.226  
   8.227 -lemma dom_map_upds: "\<And> tab ys. dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
   8.228 +lemma dom_map_upds: "\<And> tab ys. length xs = length ys 
   8.229 +  \<Longrightarrow> dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
   8.230  proof (induct xs)
   8.231    case Nil thus ?case by (simp add: dom_def)
   8.232  next
   8.233    case (Cons x xs tab ys)
   8.234 -  have "dom (tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) = dom (tab(x\<mapsto>hd ys)) \<union> set xs" .
   8.235 -  moreover 
   8.236 -  have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
   8.237 -    by (rule dom_map_upd)
   8.238 -  ultimately
   8.239 +  note Hyp = Cons.hyps
   8.240 +  have len: "length (x#xs)=length ys".
   8.241    show ?case
   8.242 -    by simp
   8.243 +  proof (cases ys)
   8.244 +    case Nil with len show ?thesis by simp
   8.245 +  next
   8.246 +    case (Cons y tl)
   8.247 +    with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
   8.248 +      by - (rule Hyp,simp)
   8.249 +    moreover 
   8.250 +    have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
   8.251 +      by (rule dom_map_upd)
   8.252 +    ultimately
   8.253 +    show ?thesis using Cons
   8.254 +      by simp
   8.255 +  qed
   8.256  qed
   8.257   
   8.258 -
   8.259 -
   8.260  lemma dom_ename_case_None_simp:
   8.261   "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
   8.262    apply (auto simp add: dom_def image_def )
   8.263 @@ -1583,14 +1568,17 @@
   8.264   "f ` g ` A = (f \<circ> g) ` A"
   8.265  by (auto simp add: image_def)
   8.266  
   8.267 +
   8.268  lemma dom_locals_init_lvars: 
   8.269    assumes m: "m=(mthd (the (methd G C sig)))"  
   8.270 +  assumes len: "length (pars m) = length pvs"
   8.271    shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
   8.272             = parameters m"
   8.273  proof -
   8.274    from m
   8.275    have static_m': "is_static m = static m"
   8.276      by simp
   8.277 +  from len
   8.278    have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
   8.279      by (simp add: dom_map_upds)
   8.280    show ?thesis
   8.281 @@ -1609,6 +1597,7 @@
   8.282    qed
   8.283  qed
   8.284  
   8.285 +
   8.286  lemma da_e2_BinOp:
   8.287    assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   8.288                    \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
   8.289 @@ -3283,10 +3272,25 @@
   8.290  	      from is_static_eq 
   8.291  	      have "(invmode (mthd dynM) e) = (invmode statM e)"
   8.292  		by (simp add: invmode_def)
   8.293 -	      with init_lvars dynM' is_static_eq normal_s2 mode 
   8.294 +	      moreover
   8.295 +	      have "length (pars (mthd dynM)) = length vs" 
   8.296 +	      proof -
   8.297 +		from normal_s2 conf_args
   8.298 +		have "length vs = length pTs"
   8.299 +		  by (simp add: list_all2_def)
   8.300 +		also from pTs_widen
   8.301 +		have "\<dots> = length pTs'"
   8.302 +		  by (simp add: widens_def list_all2_def)
   8.303 +		also from wf_dynM
   8.304 +		have "\<dots> = length (pars (mthd dynM))"
   8.305 +		  by (simp add: wf_mdecl_def wf_mhead_def)
   8.306 +		finally show ?thesis ..
   8.307 +	      qed
   8.308 +	      moreover note init_lvars dynM' is_static_eq normal_s2 mode 
   8.309 +	      ultimately
   8.310  	      have "parameters (mthd dynM) = dom (locals (store s3))"
   8.311  		using dom_locals_init_lvars 
   8.312 -                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
   8.313 +                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
   8.314  		by simp
   8.315  	      also from check
   8.316  	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
     9.1 --- a/src/HOL/Bali/WellForm.thy	Wed May 14 15:22:37 2003 +0200
     9.2 +++ b/src/HOL/Bali/WellForm.thy	Wed May 14 20:29:18 2003 +0200
     9.3 @@ -509,7 +509,8 @@
     9.4  A program declaration is wellformed if:
     9.5  \begin{itemize}
     9.6  \item the class ObjectC of Object is defined
     9.7 -\item every method of has an access modifier distinct from Package. This is
     9.8 +\item every method of Object has an access modifier distinct from Package. 
     9.9 +      This is
    9.10        necessary since every interface automatically inherits from Object.  
    9.11        We must know, that every time a Object method is "overriden" by an 
    9.12        interface method this is also overriden by the class implementing the
    9.13 @@ -2922,7 +2923,7 @@
    9.14    show ?thesis
    9.15    proof (induct)
    9.16      case (Immediate C m)
    9.17 -    have "G \<turnstile> m in C permits_acc_to accC" and "accmodi m = Private" .
    9.18 +    have "G \<turnstile> m in C permits_acc_from accC" and "accmodi m = Private" .
    9.19      then show ?case
    9.20        by (simp add: permits_acc_def)
    9.21    next
    9.22 @@ -2948,7 +2949,7 @@
    9.23    proof (induct rule: dyn_accessible_fromR.induct)
    9.24      case (Immediate C m)
    9.25      assume "G\<turnstile>m member_in C"
    9.26 -           "G \<turnstile> m in C permits_acc_to accC"
    9.27 +           "G \<turnstile> m in C permits_acc_from accC"
    9.28             "accmodi m = Package"      
    9.29      then show "?P m"
    9.30        by (auto simp add: permits_acc_def)
    9.31 @@ -2987,7 +2988,7 @@
    9.32    show ?thesis
    9.33    proof (induct)
    9.34      case (Immediate C f)
    9.35 -    have "G \<turnstile> f in C permits_acc_to accC" and "accmodi f = Package" .
    9.36 +    have "G \<turnstile> f in C permits_acc_from accC" and "accmodi f = Package" .
    9.37      then show ?case
    9.38        by (simp add: permits_acc_def)
    9.39    next
    9.40 @@ -3011,7 +3012,7 @@
    9.41    show ?thesis
    9.42    proof (induct)
    9.43      case (Immediate C f)
    9.44 -    have "G \<turnstile> f in C permits_acc_to accC" .
    9.45 +    have "G \<turnstile> f in C permits_acc_from accC" .
    9.46      moreover 
    9.47      assume "accmodi f = Protected" and  "is_field f" and "\<not> is_static f" and
    9.48             "pid (declclass f) \<noteq> pid accC"
    9.49 @@ -3039,7 +3040,7 @@
    9.50      assume "accmodi f = Protected" and  "is_field f" and "is_static f" and
    9.51             "pid (declclass f) \<noteq> pid accC"
    9.52      moreover 
    9.53 -    have "G \<turnstile> f in C permits_acc_to accC" .
    9.54 +    have "G \<turnstile> f in C permits_acc_from accC" .
    9.55      ultimately
    9.56      have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
    9.57        by (auto simp add: permits_acc_def)