--- 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
--- 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
--- 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)
--- 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
--- 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
-- {*
--- 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]:
--- 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";
--- 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'))"
--- 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)