# 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" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ hd vs = Null) \. heap_free two)" *}) +apply (tactic {* inst1_tac "R14" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. 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" "\u a. Normal (?PP a\?x) u" *}) +apply (tactic {* inst1_tac "P'34" "\u a. Normal (?PP a\?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 "\ = length pTs'" + by (simp add: widens_def list_all2_def) + also from wf_dynM + have "\ = 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 "\name=mn,parTs=pTs'\" e a vs s2] + [of "mthd dynM" G invDeclC "\name=mn,parTs=pTs'\" 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 \ (qtname \ memberdecl) \ qtname \ qtname \ bool" - ("_ \ _ in _ permits'_acc'_to _" [61,61,61,61] 60) + ("_ \ _ in _ permits'_acc'_from _" [61,61,61,61] 60) -"G\membr in class permits_acc_to accclass +"G\membr in class permits_acc_from accclass \ (case (accmodi membr) of Private \ (declclass membr = accclass) | Package \ (pid (declclass membr) = pid accclass) @@ -849,7 +849,7 @@ inductive "accessible_fromR G accclass" intros Immediate: "\G\membr member_of class; G\(Class class) accessible_in (pid accclass); - G\membr in class permits_acc_to accclass + G\membr in class permits_acc_from accclass \ \ G\membr of class accessible_from accclass" Overriding: "\G\membr member_of class; @@ -902,7 +902,7 @@ inductive "dyn_accessible_fromR G accclass" intros Immediate: "\G\membr member_in class; - G\membr in class permits_acc_to accclass + G\membr in class permits_acc_from accclass \ \ G\membr in class dyn_accessible_from accclass" Overriding: "\G\membr member_in class; @@ -1141,15 +1141,15 @@ by (induct set: overridesR) (auto simp add: inheritable_in_def) lemma permits_acc_inheritance: - "\G\m in statC permits_acc_to accC; G\dynC \\<^sub>C statC - \ \ G\m in dynC permits_acc_to accC" + "\G\m in statC permits_acc_from accC; G\dynC \\<^sub>C statC + \ \ G\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: - "\G\m in C permits_acc_to accC; G\m member_in C; is_static m - \ \ G\m in (declclass m) permits_acc_to accC" + "\G\m in C permits_acc_from accC; G\m member_in C; is_static m + \ \ G\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 @@ "\G\membr of C accessible_from accC;is_field membr\ \ G\membr member_of C \ G\(Class C) accessible_in (pid accC) \ - G\membr in C permits_acc_to accC" + G\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: "\G\membr of statC accessible_from accC; is_field membr; G \ dynC \\<^sub>C statC\ -\ G\membr in dynC permits_acc_to accC" +\ G\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\m member_of C" - "G \ m in C permits_acc_to S" + "G \ 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 @@ "\G\membr of C accessible_from accC; is_field membr\ \ G\membr member_of C \ G\(Class C) accessible_in (pid accC) \ - G\membr in C permits_acc_to accC" + G\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 \ lname set \ term \ 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\c1\\" and wt_c2: "Env\c2\\" 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))) \ 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 "\ l. abrupt s1 \ Some (Jump (Break l))" + from eval_e _ wt_e have "\ j. abrupt s1 \ 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 \ (Base, mdecl Base_foo) in Base permits_acc_to S" + "tprg \ (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 \ (Ext, mdecl Ext_foo) in Ext permits_acc_to S" + "tprg \ (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\hd ys)(xs[\]tl ys)) z = (tab'(x\hd ys)(xs[\]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\y)(xs[\]ys')) z = (tab'(x\y)(xs[\]ys')) z" + by (rules intro: Hyps map_upd_cong_ext) + with Cons show ?thesis + by simp + qed qed lemma map_upd_override: "(tab(x\y)) x = (tab'(x\y)) x" by simp - -lemma map_upds_override_cong: -"\ tab tab' zs. x\ set ws \ - (tab(ws[\]zs)) x = (tab'(ws[\]zs)) x" -proof (induct ws) - case Nil thus ?case by simp -next - case (Cons w ws tab tab' zs) - have x: "x \ 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 \ set ws" - by simp - with Cons.hyps show ?thesis - by simp - qed -qed - -lemma map_upds_in_suffix: assumes x: "x \ set xs" - shows "\ tab qs. (tab(ps @ xs[\]qs)) x = (tab(xs[\]drop (length ps) qs)) x" -proof (induct ps) - case Nil thus ?case by simp -next - case (Cons p ps tab qs) - have "(tab(p\hd qs)(ps @ xs[\](tl qs))) x - =(tab(p\hd qs)(xs[\]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: "\ tab qs. length ps = length qs \ tab(ps@xs[\]qs) = tab(ps[\]qs)(xs[\][])" 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\hd ys)) vn = Some z'" - by (rule map_upd_Some_expand [of tab,elim_format]) blast - hence "\ z. (tab (x\hd ys)(xs[\]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\y)) vn = Some z'" + by (rule map_upd_Some_expand [of tab,elim_format]) blast + hence "\z. ((tab(x\y))(xs[\]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 \ (tab(x\y)) vn = (tab'(x\y)) vn" by (simp add: fun_upd_def) -lemma map_eq_upds_eq: - "\ tab tab' ys. - tab vn = tab' vn \ (tab(xs[\]ys)) vn = (tab'(xs[\]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\hd ys)) vn = (tab'(x\hd ys)) vn" - by (rule map_eq_upd_eq) - hence "(tab(x\hd ys)(xs[\]tl ys)) vn = (tab'(x\hd ys)(xs[\]tl ys)) vn" - by (rule Cons.hyps) - thus ?case - by simp -qed - lemma map_upd_in_expansion_map_swap: "\(tab(x\y)) vn = Some z;tab vn \ Some z\ \ (tab'(x\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\hd ys)(xs[\]tl ys)) vn = Some z" and - tab_not_z: "tab vn \ Some z" - by simp + have some: "(tab(x # xs[\]ys)) vn = Some z" . + have tab_not_z: "tab vn \ Some z". show ?case - proof (cases "(tab(x\hd ys)) vn \ Some z") - case True - with some have "(tab'(x\hd ys)(xs[\]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\hd ys)) vn = Some z" by blast - moreover - from tabx_z tab_not_z - have "(tab'(x\hd ys)) vn = Some z" - by (rule map_upd_in_expansion_map_swap) - ultimately - have "(tab(x\hd ys)) vn =(tab'(x\hd ys)) vn" - by simp - hence "(tab(x\hd ys)(xs[\]tl ys)) vn = (tab'(x\hd ys)(xs[\]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\y)) vn \ Some z") + case True + with some ys have "(tab'(x\y)(xs[\]tl)) vn = Some z" + by (fastsimp intro: Cons.hyps) + with ys show ?thesis + by simp + next + case False + hence tabx_z: "(tab(x\y)) vn = Some z" by blast + moreover + from tabx_z tab_not_z + have "(tab'(x\y)) vn = Some z" + by (rule map_upd_in_expansion_map_swap) + ultimately + have "(tab(x\y)) vn =(tab'(x\y)) vn" + by simp + hence "(tab(x\y)(xs[\]tl)) vn = (tab'(x\y)(xs[\]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\hd ys)) vn = Some el" - by - (rule Cons.hyps,auto) - moreover from Cons.prems - have "(tab'(x\hd ys)(xs[\]tl ys)) vn = None" - by simp - hence "(tab'(x\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[\]ys)) vn = Some el". + have tab'_vn: "(tab'(x # xs[\]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\y)) vn = Some el" + by - (rule Cons.hyps,auto) + moreover from tab'_vn ys + have "(tab'(x\y)(xs[\]tl)) vn = None" + by simp + hence "(tab'(x\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\y)(xs[\]ys)) a) b) @@ -1531,22 +1508,30 @@ lemma dom_map_upd: "\ tab. dom (tab(x\y)) = dom tab \ {x}" by (auto simp add: dom_def fun_upd_def) -lemma dom_map_upds: "\ tab ys. dom (tab(xs[\]ys)) = dom tab \ set xs" +lemma dom_map_upds: "\ tab ys. length xs = length ys + \ dom (tab(xs[\]ys)) = dom tab \ 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\hd ys)(xs[\]tl ys)) = dom (tab(x\hd ys)) \ set xs" . - moreover - have "dom (tab(x\hd ys)) = dom tab \ {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\y)(xs[\]tl)) = dom (tab(x\y)) \ set xs" + by - (rule Hyp,simp) + moreover + have "dom (tab(x\hd ys)) = dom tab \ {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 \ 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[\]pvs))=set (pars m)" by (simp add: dom_map_upds) show ?thesis @@ -1609,6 +1597,7 @@ qed qed + lemma da_e2_BinOp: assumes da: "\prg=G,cls=accC,lcl=L\ \dom (locals (store s0)) \\BinOp binop e1 e2\\<^sub>e\ 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 "\ = length pTs'" + by (simp add: widens_def list_all2_def) + also from wf_dynM + have "\ = 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 "\name=mn,parTs=pTs'\" e a vs s2] + [of "mthd dynM" G invDeclC "\name=mn,parTs=pTs'\" vs e a s2] by simp also from check have "dom (locals (store s3)) \ 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 \ m in C permits_acc_to accC" and "accmodi m = Private" . + have "G \ 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\m member_in C" - "G \ m in C permits_acc_to accC" + "G \ 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 \ f in C permits_acc_to accC" and "accmodi f = Package" . + have "G \ 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 \ f in C permits_acc_to accC" . + have "G \ f in C permits_acc_from accC" . moreover assume "accmodi f = Protected" and "is_field f" and "\ is_static f" and "pid (declclass f) \ pid accC" @@ -3039,7 +3040,7 @@ assume "accmodi f = Protected" and "is_field f" and "is_static f" and "pid (declclass f) \ pid accC" moreover - have "G \ f in C permits_acc_to accC" . + have "G \ f in C permits_acc_from accC" . ultimately have "G\ accC \\<^sub>C declclass f" by (auto simp add: permits_acc_def)