# HG changeset patch # User oheimb # Date 1001089395 -7200 # Node ID ab004c0ecc63fe9e16d5110ce3116af83d3506d9 # Parent 7b87c95fdf3baf9ba6a9e4d240e005f6485b2e05 Minor improvements, added Example diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/AxSem.thy --- a/src/HOL/NanoJava/AxSem.thy Mon Sep 17 19:49:09 2001 +0200 +++ b/src/HOL/NanoJava/AxSem.thy Fri Sep 21 18:23:15 2001 +0200 @@ -78,9 +78,9 @@ A |-e {P} Cast C e {Q}" Call: "[| A |-e {P} e1 {Q}; \a. A |-e {Q a} e2 {R a}; - \a p l. A |- {\s'. \s. R a p s \ l = s \ + \a p ls. A |- {\s'. \s. R a p s \ ls = s \ s' = lupd(This\a)(lupd(Par\p)(reset_locs s))} - Meth (C,m) {\s. S (s) (set_locs l s)} |] ==> + Meth (C,m) {\s. S (s) (set_locs ls s)} |] ==> A |-e {P} {C}e1..m(e2) {S}" Meth: "\D. A |- {\s'. \s a. s = Addr a \ D = obj_class s a \ D <=C C \ @@ -88,11 +88,11 @@ Impl (D,m) {Q} ==> A |- {P} Meth (C,m) {Q}" - --{* @{text "\z"} instead of @{text "\z"} in the conclusion and\\ - z restricted to type state due to limitations of the inductive package *} - Impl: "\z::state. A\ (\z. (\Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- - (\Cm. (P z Cm, body Cm, Q z Cm))`Ms ==> - A ||- (\Cm. (P z Cm, Impl Cm, Q z Cm))`Ms" + --{* @{text "\Z"} instead of @{text "\Z"} in the conclusion and\\ + Z restricted to type state due to limitations of the inductive package *} + Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- + (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> + A ||- (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" --{* structural rules *} @@ -102,15 +102,31 @@ ConjE: "[|A ||- C; c \ C |] ==> A ||- {c}" - Conseq:"[| \z::state. A |- {P' z} c {Q' z}; - \s t. (\z. P' z s --> Q' z t) --> (P s --> Q t) |] ==> + --{* Z restricted to type state due to limitations of the inductive package *} + Conseq:"[| \Z::state. A |- {P' Z} c {Q' Z}; + \s t. (\Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> A |- {P} c {Q }" - --{* z restricted to type state due to limitations of the inductive package *} - eConseq:"[| \z::state. A |-e {P' z} c {Q' z}; - \s v t. (\z. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==> - A |-e {P} c {Q }" + --{* Z restricted to type state due to limitations of the inductive package *} + eConseq:"[| \Z::state. A |-e {P' Z} e {Q' Z}; + \s v t. (\Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> + A |-e {P} e {Q }" + + +subsection "Fully polymorphic variants" +axioms + Conseq:"[| \Z. A |- {P' Z} c {Q' Z}; + \s t. (\Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> + A |- {P} c {Q }" + + eConseq:"[| \Z. A |-e {P' Z} e {Q' Z}; + \s v t. (\Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> + A |-e {P} e {Q }" + + Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- + (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> + A ||- (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" subsection "Derived Rules" @@ -146,17 +162,55 @@ apply assumption done -lemma Union: "A |\ (\z. C z) = (\z. A |\ C z)" +lemma Thin_lemma: + "(A' |\ C \ (\A. A' \ A \ A |\ C )) \ + (A' \\<^sub>e {P} e {Q} \ (\A. A' \ A \ A \\<^sub>e {P} e {Q}))" +apply (rule hoare_ehoare.induct) +apply (tactic "ALLGOALS(EVERY'[Clarify_tac, REPEAT o smp_tac 1])") +apply (blast intro: hoare_ehoare.Skip) +apply (blast intro: hoare_ehoare.Comp) +apply (blast intro: hoare_ehoare.Cond) +apply (blast intro: hoare_ehoare.Loop) +apply (blast intro: hoare_ehoare.LAcc) +apply (blast intro: hoare_ehoare.LAss) +apply (blast intro: hoare_ehoare.FAcc) +apply (blast intro: hoare_ehoare.FAss) +apply (blast intro: hoare_ehoare.NewC) +apply (blast intro: hoare_ehoare.Cast) +apply (erule hoare_ehoare.Call) +apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption) +apply blast +apply (blast intro!: hoare_ehoare.Meth) +apply (blast intro!: hoare_ehoare.Impl) +apply (blast intro!: hoare_ehoare.Asm) +apply (blast intro: hoare_ehoare.ConjI) +apply (blast intro: hoare_ehoare.ConjE) +apply (rule hoare_ehoare.Conseq) +apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) +apply (rule hoare_ehoare.eConseq) +apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) +done + +lemma cThin: "\A' |\ C; A' \ A\ \ A |\ C" +by (erule (1) conjunct1 [OF Thin_lemma, rule_format]) + +lemma eThin: "\A' \\<^sub>e {P} e {Q}; A' \ A\ \ A \\<^sub>e {P} e {Q}" +by (erule (1) conjunct2 [OF Thin_lemma, rule_format]) + + +lemma Union: "A |\ (\Z. C Z) = (\Z. A |\ C Z)" by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE) -lemma Impl1: - "\\z::state. A\ (\z. (\Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) |\ - (\Cm. (P z Cm, body Cm, Q z Cm))`Ms; +lemma Impl1': + "\\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\ + (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms; Cm \ Ms\ \ - A \ {P z Cm} Impl Cm {Q z Cm}" -apply (drule hoare_ehoare.Impl) + A \ {P Z Cm} Impl Cm {Q Z Cm}" +apply (drule Impl) apply (erule Weaken) apply (auto del: image_eqI intro: rev_image_eqI) done +lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard] + end diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/Decl.thy --- a/src/HOL/NanoJava/Decl.thy Mon Sep 17 19:49:09 2001 +0200 +++ b/src/HOL/NanoJava/Decl.thy Fri Sep 21 18:23:15 2001 +0200 @@ -12,7 +12,7 @@ = NT --{* null type *} | Class cname --{* class type *} -text{* field declaration *} +text{* Field declaration *} types fdecl = "fname \ ty" @@ -22,7 +22,7 @@ lcl ::"(vname \ ty) list" bdy :: stmt -text{* method declaration *} +text{* Method declaration *} types mdecl = "mname \ methd" @@ -31,7 +31,7 @@ fields ::"fdecl list" methods ::"mdecl list" -text{* class declaration *} +text{* Class declaration *} types cdecl = "cname \ class" diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Mon Sep 17 19:49:09 2001 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Fri Sep 21 18:23:15 2001 +0200 @@ -134,7 +134,7 @@ apply blast (* Impl *) apply (rule allI) -apply (rule_tac x=z in spec) +apply (rule_tac x=Z in spec) apply (induct_tac "n") apply (clarify intro!: Impl_nvalid_0) apply (clarify intro!: Impl_nvalid_Suc) @@ -164,14 +164,14 @@ subsection "(Relative) Completeness" constdefs MGT :: "stmt => state => triple" - "MGT c z \ (\s. z = s, c, \ t. \n. z -c- n-> t)" + "MGT c Z \ (\s. Z = s, c, \ t. \n. Z -c- n-> t)" MGTe :: "expr => state => etriple" - "MGTe e z \ (\s. z = s, e, \v t. \n. z -e>v-n-> t)" + "MGTe e Z \ (\s. Z = s, e, \v t. \n. Z -e>v-n-> t)" syntax (xsymbols) MGTe :: "expr => state => etriple" ("MGT\<^sub>e") lemma MGF_implies_complete: - "\z. {} |\ { MGT c z} \ \ {P} c {Q} \ {} \ {P} c {Q}" + "\Z. {} |\ { MGT c Z} \ \ {P} c {Q} \ {} \ {P} c {Q}" apply (simp only: valid_def2) apply (unfold MGT_def) apply (erule hoare_ehoare.Conseq) @@ -179,7 +179,7 @@ done lemma eMGF_implies_complete: - "\z. {} |\\<^sub>e MGT\<^sub>e e z \ \\<^sub>e {P} e {Q} \ {} \\<^sub>e {P} e {Q}" + "\Z. {} |\\<^sub>e MGT\<^sub>e e Z \ \\<^sub>e {P} e {Q} \ {} \\<^sub>e {P} e {Q}" apply (simp only: evalid_def2) apply (unfold MGTe_def) apply (erule hoare_ehoare.eConseq) @@ -188,9 +188,9 @@ declare exec_eval.intros[intro!] -lemma MGF_Loop: "\z. A \ {op = z} c {\t. \n. z -c-n\ t} \ - A \ {op = z} While (x) c {\t. \n. z -While (x) c-n\ t}" -apply (rule_tac P' = "\z s. (z,s) \ ({(s,t). \n. s \ Null \ s -c-n\ t})^*" +lemma MGF_Loop: "\Z. A \ {op = Z} c {\t. \n. Z -c-n\ t} \ + A \ {op = Z} While (x) c {\t. \n. Z -While (x) c-n\ t}" +apply (rule_tac P' = "\Z s. (Z,s) \ ({(s,t). \n. s \ Null \ s -c-n\ t})^*" in hoare_ehoare.Conseq) apply (rule allI) apply (rule hoare_ehoare.Loop) @@ -199,7 +199,7 @@ apply (blast intro:rtrancl_into_rtrancl) apply (erule thin_rl) apply clarsimp -apply (erule_tac x = z in allE) +apply (erule_tac x = Z in allE) apply clarsimp apply (erule converse_rtrancl_induct) apply blast @@ -208,8 +208,8 @@ apply (blast del: exec_elim_cases) done -lemma MGF_lemma: "\M z. A |\ {MGT (Impl M) z} \ - (\z. A |\ {MGT c z}) \ (\z. A |\\<^sub>e MGT\<^sub>e e z)" +lemma MGF_lemma: "\M Z. A |\ {MGT (Impl M) Z} \ + (\Z. A |\ {MGT c Z}) \ (\Z. A |\\<^sub>e MGT\<^sub>e e Z)" apply (simp add: MGT_def MGTe_def) apply (rule stmt_expr.induct) apply (rule_tac [!] allI) @@ -239,7 +239,7 @@ apply fast apply (erule thin_rl) -apply (rule_tac Q = "\a s. \n. z -expr1\Addr a-n\ s" in hoare_ehoare.FAss) +apply (rule_tac Q = "\a s. \n. Z -expr1\Addr a-n\ s" in hoare_ehoare.FAss) apply (drule spec) apply (erule eConseq2) apply fast @@ -269,7 +269,7 @@ apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc]) apply fast -apply (rule_tac R = "\a v s. \n1 n2 t. z -expr1\a-n1\ t \ t -expr2\v-n2\ s" in +apply (rule_tac R = "\a v s. \n1 n2 t. Z -expr1\a-n1\ t \ t -expr2\v-n2\ s" in hoare_ehoare.Call) apply (erule spec) apply (rule allI) @@ -283,12 +283,12 @@ apply (erule thin_rl, erule thin_rl) apply (clarsimp del: Impl_elim_cases) apply (drule (2) eval_eval_exec_max) -apply (fast del: Impl_elim_cases) +apply (force del: Impl_elim_cases) done -lemma MGF_Impl: "{} |\ {MGT (Impl M) z}" +lemma MGF_Impl: "{} |\ {MGT (Impl M) Z}" apply (unfold MGT_def) -apply (rule Impl1) +apply (rule_tac 'a = state in Impl1') apply (rule_tac [2] UNIV_I) apply clarsimp apply (rule hoare_ehoare.ConjI) @@ -316,4 +316,16 @@ apply (rule MGF_Impl) done +lemma cFalse: "A \ {\s. False} c {Q}" +apply (rule cThin) +apply (rule hoare_relative_complete) +apply (auto simp add: valid_def) +done + +lemma eFalse: "A \\<^sub>e {\s. False} e {Q}" +apply (rule eThin) +apply (rule ehoare_relative_complete) +apply (auto simp add: evalid_def) +done + end diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/NanoJava/Example.thy Fri Sep 21 18:23:15 2001 +0200 @@ -0,0 +1,208 @@ +(* Title: HOL/NanoJava/Example.thy + ID: $Id$ + Author: David von Oheimb + Copyright 2001 Technische Universitaet Muenchen +*) + +header "Example" + +theory Example = Equivalence: + +text {* + +\begin{verbatim} +class Nat { + + Nat pred; + + Nat suc() + { Nat n = new Nat(); n.pred = this; return n; } + + Nat eq(Nat n) + { if (this.pred != null) if (n.pred != null) return this.pred.eq(n.pred); + else return n.pred; // false + else if (n.pred != null) return this.pred; // false + else return this.suc(); // true + } + + Nat add(Nat n) + { if (this.pred != null) return this.pred.add(n.suc()); else return n; } + + public static void main(String[] args) // test x+1=1+x + { + Nat one = new Nat().suc(); + Nat x = new Nat().suc().suc().suc().suc(); + Nat ok = x.suc().eq(x.add(one)); + System.out.println(ok != null); + } +} +\end{verbatim} + +*} + +axioms This_neq_Par [simp]: "This \ Par" + Res_neq_This [simp]: "Res \ This" + + +subsection "Program representation" + +consts N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *) +consts pred :: fname +consts suc :: mname + add :: mname +consts any :: vname +syntax dummy:: expr ("<>") + one :: expr +translations + "<>" == "LAcc any" + "one" == "{Nat}new Nat..suc(<>)" + +text {* The following properties could be derived from a more complete + program model, which we leave out for laziness. *} + +axioms Nat_no_subclasses [simp]: "D \C Nat = (D=Nat)" + +axioms method_Nat_add [simp]: "method Nat add = Some + \ par=Class Nat, res=Class Nat, lcl=[], + bdy= If((LAcc This..pred)) + (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>))) + Else Res :== LAcc Par \" + +axioms method_Nat_suc [simp]: "method Nat suc = Some + \ par=NT, res=Class Nat, lcl=[], + bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \" + +axioms field_Nat [simp]: "field Nat = empty(pred\Class Nat)" + +lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s" +by (simp add: init_locs_def init_vars_def) + +lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s" +by (simp add: init_locs_def init_vars_def) + +lemma upd_obj_new_obj_Nat [simp]: + "upd_obj a pred v (new_obj a Nat s) = hupd(a\(Nat, empty(pred\v))) s" +by (simp add: new_obj_def init_vars_def upd_obj_def Let_def) + + +subsection "``atleast'' relation for interpretation of Nat ``values''" + +consts Nat_atleast :: "state \ val \ nat \ bool" ("_:_ \ _" [51, 51, 51] 50) +primrec "s:x\0 = (x\Null)" + "s:x\Suc n = (\a. x=Addr a \ heap s a \ None \ s:get_field s a pred\n)" + +lemma Nat_atleast_lupd [rule_format, simp]: + "\s v. lupd(x\y) s:v \ n = (s:v \ n)" +apply (induct n) +by auto + +lemma Nat_atleast_set_locs [rule_format, simp]: + "\s v. set_locs l s:v \ n = (s:v \ n)" +apply (induct n) +by auto + +lemma Nat_atleast_reset_locs [rule_format, simp]: + "\s v. reset_locs s:v \ n = (s:v \ n)" +apply (induct n) +by auto + +lemma Nat_atleast_NullD [rule_format]: "s:Null \ n \ False" +apply (induct n) +by auto + +lemma Nat_atleast_pred_NullD [rule_format]: +"Null = get_field s a pred \ s:Addr a \ n \ n = 0" +apply (induct n) +by (auto dest: Nat_atleast_NullD) + +lemma Nat_atleast_mono [rule_format]: +"\a. s:get_field s a pred \ n \ heap s a \ None \ s:Addr a \ n" +apply (induct n) +by auto + +lemma Nat_atleast_newC [rule_format]: + "heap s aa = None \ \v. s:v \ n \ hupd(aa\obj) s:v \ n" +apply (induct n) +apply auto +apply (case_tac "aa=a") +apply auto +apply (tactic "smp_tac 1 1") +apply (case_tac "aa=a") +apply auto +done + + +subsection "Proof(s) using the Hoare logic" + +theorem add_triang: + "{} \ {\s. s:s \ X \ s:s \ Y} Meth(Nat,add) {\s. s:s \ X+Y}" +apply (rule hoare_ehoare.Meth) +apply clarsimp +apply (rule_tac P'= "\Z s. (s:s \ fst Z \ s:s \ snd Z) \ D=Nat" and + Q'= "\Z s. s:s \ fst Z+snd Z" in Conseq) +prefer 2 +apply (clarsimp simp add: init_locs_def init_vars_def) +apply rule +apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) +apply (rule_tac P = "\Z Cm s. s:s \ fst Z \ s:s \ snd Z" in Impl1) +apply (clarsimp simp add: body_def) +apply (rename_tac n m) +apply (rule_tac Q = "\v s. (s:s \ n \ s:s \ m) \ + (\a. s = Addr a \ v = get_field s a pred)" in hoare_ehoare.Cond) +apply (rule hoare_ehoare.FAcc) +apply (rule eConseq1) +apply (rule hoare_ehoare.LAcc) +apply fast +apply auto +prefer 2 +apply (rule hoare_ehoare.LAss) +apply (rule eConseq1) +apply (rule hoare_ehoare.LAcc) +apply (auto dest: Nat_atleast_pred_NullD) +apply (rule hoare_ehoare.LAss) +apply (rule_tac + Q = "\v s. (\m. n = Suc m \ s:v \ m) \ s:s \ m" and + R = "\T P s. (\m. n = Suc m \ s:T \ m) \ s:P \ Suc m" + in hoare_ehoare.Call) +apply (rule hoare_ehoare.FAcc) +apply (rule eConseq1) +apply (rule hoare_ehoare.LAcc) +apply clarify +apply (drule sym, rotate_tac -1, frule (1) trans) +apply simp +prefer 2 +apply clarsimp +apply (rule hoare_ehoare.Meth) +apply clarsimp +apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) +apply (rule Conseq) +apply rule +apply (rule hoare_ehoare.Asm) +apply (rule_tac a = "((case n of 0 \ 0 | Suc m \ m),m+1)" in UN_I, rule+) +apply (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono) +apply rule +apply (rule hoare_ehoare.Call) +apply (rule hoare_ehoare.LAcc) +apply rule +apply (rule hoare_ehoare.LAcc) +apply clarify +apply (rule hoare_ehoare.Meth) +apply clarsimp +apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) +apply (rule Impl1) +apply (clarsimp simp add: body_def) +apply (rule hoare_ehoare.Comp) +prefer 2 +apply (rule hoare_ehoare.FAss) +prefer 2 +apply rule +apply (rule hoare_ehoare.LAcc) +apply (rule hoare_ehoare.LAcc) +apply (rule hoare_ehoare.LAss) +apply (rule eConseq1) +apply (rule hoare_ehoare.NewC) +apply (auto dest!: new_AddrD elim: Nat_atleast_newC) +done + + +end diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/OpSem.thy --- a/src/HOL/NanoJava/OpSem.thy Mon Sep 17 19:49:09 2001 +0200 +++ b/src/HOL/NanoJava/OpSem.thy Fri Sep 21 18:23:15 2001 +0200 @@ -115,7 +115,7 @@ apply (drule (1) eval_eval_max, erule thin_rl) by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2) -lemma Impl_body_eq: "(\t. \n. z -Impl M-n\ t) = (\t. \n. z -body M-n\ t)" +lemma Impl_body_eq: "(\t. \n. Z -Impl M-n\ t) = (\t. \n. Z -body M-n\ t)" apply (rule ext) apply (fast elim: exec_elim_cases intro: exec_eval.Impl) done diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/ROOT.ML --- a/src/HOL/NanoJava/ROOT.ML Mon Sep 17 19:49:09 2001 +0200 +++ b/src/HOL/NanoJava/ROOT.ML Fri Sep 21 18:23:15 2001 +0200 @@ -1,1 +1,1 @@ -use_thy "Equivalence"; +use_thy "Example"; diff -r 7b87c95fdf3b -r ab004c0ecc63 src/HOL/NanoJava/State.thy --- a/src/HOL/NanoJava/State.thy Mon Sep 17 19:49:09 2001 +0200 +++ b/src/HOL/NanoJava/State.thy Fri Sep 21 18:23:15 2001 +0200 @@ -13,7 +13,7 @@ body :: "cname \ mname => stmt" "body \ \(C,m). bdy (the (method C m))" -text {* locations, i.e.\ abstract references to objects *} +text {* Locations, i.e.\ abstract references to objects *} typedecl loc datatype val @@ -35,11 +35,11 @@ init_vars:: "('a \ 'b) => ('a \ val)" "init_vars m == option_map (\T. Null) o m" -text {* private *} +text {* private: *} types heap = "loc \ obj" locals = "vname \ val" -text {* private *} +text {* private: *} record state = heap :: heap locals :: locals @@ -56,7 +56,8 @@ "reset_locs s \ s (| locals := empty |)" init_locs :: "cname => mname => state => state" - "init_locs C m s \ s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)" + "init_locs C m s \ s (| locals := locals s ++ + init_vars (map_of (lcl (the (method C m)))) |)" text {* The first parameter of @{term set_locs} is of type @{typ state} rather than @{typ locals} in order to keep @{typ locals} private.*} @@ -99,6 +100,87 @@ new_Addr :: "state => val" "new_Addr s == SOME v. (\a. v = Addr a \ (heap s) a = None) | v = Null" + +subsection "Properties not used in the meta theory" + +lemma locals_upd_id [simp]: "s\locals := locals s\ = s" +by simp + +lemma lupd_get_local_same [simp]: "lupd(x\v) s = v" +by (simp add: lupd_def get_local_def) + +lemma lupd_get_local_other [simp]: "x \ y \ lupd(x\v) s = s" +apply (drule not_sym) +by (simp add: lupd_def get_local_def) + +lemma get_field_lupd [simp]: + "get_field (lupd(x\y) s) a f = get_field s a f" +by (simp add: lupd_def get_field_def get_obj_def) + +lemma get_field_set_locs [simp]: + "get_field (set_locs l s) a f = get_field s a f" +by (simp add: lupd_def get_field_def set_locs_def get_obj_def) + +lemma get_field_set_locs [simp]: + "get_field (reset_locs s) a f = get_field s a f" +by (simp add: lupd_def get_field_def reset_locs_def get_obj_def) + +lemma new_obj_get_local [simp]: "new_obj a C s = s" +by (simp add: new_obj_def hupd_def get_local_def) + +lemma heap_lupd [simp]: "heap (lupd(x\y) s) = heap s" +by (simp add: lupd_def) + +lemma heap_hupd_same [simp]: "heap (hupd(a\obj) s) a = Some obj" +by (simp add: hupd_def) + +lemma heap_hupd_other [simp]: "aa \ a \ heap (hupd(aa\obj) s) a = heap s a" +apply (drule not_sym) +by (simp add: hupd_def) + +lemma hupd_hupd [simp]: "hupd(a\obj) (hupd(a\obj') s) = hupd(a\obj) s" +by (simp add: hupd_def) + +lemma heap_reset_locs [simp]: "heap (reset_locs s) = heap s" +by (simp add: reset_locs_def) + +lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s" +by (simp add: set_locs_def) + +lemma hupd_lupd [simp]: + "hupd(a\obj) (lupd(x\y) s) = lupd(x\y) (hupd(a\obj) s)" +by (simp add: hupd_def lupd_def) + +lemma hupd_reset_locs [simp]: + "hupd(a\obj) (reset_locs s) = reset_locs (hupd(a\obj) s)" +by (simp add: hupd_def reset_locs_def) + +lemma new_obj_lupd [simp]: + "new_obj a C (lupd(x\y) s) = lupd(x\y) (new_obj a C s)" +by (simp add: new_obj_def) + +lemma new_obj_reset_locs [simp]: + "new_obj a C (reset_locs s) = reset_locs (new_obj a C s)" +by (simp add: new_obj_def) + +lemma upd_obj_lupd [simp]: + "upd_obj a f v (lupd(x\y) s) = lupd(x\y) (upd_obj a f v s)" +by (simp add: upd_obj_def Let_def split_beta) + +lemma upd_obj_reset_locs [simp]: + "upd_obj a f v (reset_locs s) = reset_locs (upd_obj a f v s)" +by (simp add: upd_obj_def Let_def split_beta) + +lemma get_field_hupd_same [simp]: + "get_field (hupd(a\(C, fs)) s) a = the \ fs" +apply (rule ext) +by (simp add: get_field_def get_obj_def) + +lemma get_field_hupd_other [simp]: + "aa \ a \ get_field (hupd(aa\obj) s) a = get_field s a" +apply (rule ext) +by (simp add: get_field_def get_obj_def) + lemma new_AddrD: "new_Addr s = v \ (\