--- 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}; \<forall>a. A |-e {Q a} e2 {R a};
- \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and>
+ \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s))}
- Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
+ Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
A |-e {P} {C}e1..m(e2) {S}"
Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and>
@@ -88,11 +88,11 @@
Impl (D,m) {Q} ==>
A |- {P} Meth (C,m) {Q}"
- --{* @{text "\<Union>z"} instead of @{text "\<forall>z"} in the conclusion and\\
- z restricted to type state due to limitations of the inductive package *}
- Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||-
- (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
- A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"
+ --{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\
+ Z restricted to type state due to limitations of the inductive package *}
+ Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
+ (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
+ A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
--{* structural rules *}
@@ -102,15 +102,31 @@
ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
- Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
- \<forall>s t. (\<forall>z. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
+ --{* Z restricted to type state due to limitations of the inductive package *}
+ Conseq:"[| \<forall>Z::state. A |- {P' Z} c {Q' Z};
+ \<forall>s t. (\<forall>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:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
- \<forall>s v t. (\<forall>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:"[| \<forall>Z::state. A |-e {P' Z} e {Q' Z};
+ \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
+ A |-e {P} e {Q }"
+
+
+subsection "Fully polymorphic variants"
+axioms
+ Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z};
+ \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
+ A |- {P} c {Q }"
+
+ eConseq:"[| \<forall>Z. A |-e {P' Z} e {Q' Z};
+ \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
+ A |-e {P} e {Q }"
+
+ Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
+ (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
+ A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
subsection "Derived Rules"
@@ -146,17 +162,55 @@
apply assumption
done
-lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
+lemma Thin_lemma:
+ "(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
+ (A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^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: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
+by (erule (1) conjunct1 [OF Thin_lemma, rule_format])
+
+lemma eThin: "\<lbrakk>A' \<turnstile>\<^sub>e {P} e {Q}; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
+by (erule (1) conjunct2 [OF Thin_lemma, rule_format])
+
+
+lemma Union: "A |\<turnstile> (\<Union>Z. C Z) = (\<forall>Z. A |\<turnstile> C Z)"
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
-lemma Impl1:
- "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) |\<turnstile>
- (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms;
+lemma Impl1':
+ "\<lbrakk>\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
+ (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms;
Cm \<in> Ms\<rbrakk> \<Longrightarrow>
- A \<turnstile> {P z Cm} Impl Cm {Q z Cm}"
-apply (drule hoare_ehoare.Impl)
+ A \<turnstile> {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
--- 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 \<times> ty"
@@ -22,7 +22,7 @@
lcl ::"(vname \<times> ty) list"
bdy :: stmt
-text{* method declaration *}
+text{* Method declaration *}
types mdecl
= "mname \<times> methd"
@@ -31,7 +31,7 @@
fields ::"fdecl list"
methods ::"mdecl list"
-text{* class declaration *}
+text{* Class declaration *}
types cdecl
= "cname \<times> class"
--- 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 \<equiv> (\<lambda>s. z = s, c, \<lambda> t. \<exists>n. z -c- n-> t)"
+ "MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n-> t)"
MGTe :: "expr => state => etriple"
- "MGTe e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
+ "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
syntax (xsymbols)
MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
lemma MGF_implies_complete:
- "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
+ "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {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:
- "\<forall>z. {} |\<turnstile>\<^sub>e MGT\<^sub>e e z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
+ "\<forall>Z. {} |\<turnstile>\<^sub>e MGT\<^sub>e e Z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^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: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow>
- A \<turnstile> {op = z} While (x) c {\<lambda>t. \<exists>n. z -While (x) c-n\<rightarrow> t}"
-apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
+lemma MGF_Loop: "\<forall>Z. A \<turnstile> {op = Z} c {\<lambda>t. \<exists>n. Z -c-n\<rightarrow> t} \<Longrightarrow>
+ A \<turnstile> {op = Z} While (x) c {\<lambda>t. \<exists>n. Z -While (x) c-n\<rightarrow> t}"
+apply (rule_tac P' = "\<lambda>Z s. (Z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s -c-n\<rightarrow> 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: "\<forall>M z. A |\<turnstile> {MGT (Impl M) z} \<Longrightarrow>
- (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)"
+lemma MGF_lemma: "\<forall>M Z. A |\<turnstile> {MGT (Impl M) Z} \<Longrightarrow>
+ (\<forall>Z. A |\<turnstile> {MGT c Z}) \<and> (\<forall>Z. A |\<turnstile>\<^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 = "\<lambda>a s. \<exists>n. z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
+apply (rule_tac Q = "\<lambda>a s. \<exists>n. Z -expr1\<succ>Addr a-n\<rightarrow> 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 = "\<lambda>a v s. \<exists>n1 n2 t. z -expr1\<succ>a-n1\<rightarrow> t \<and> t -expr2\<succ>v-n2\<rightarrow> s" in
+apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. Z -expr1\<succ>a-n1\<rightarrow> t \<and> t -expr2\<succ>v-n2\<rightarrow> 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: "{} |\<turnstile> {MGT (Impl M) z}"
+lemma MGF_Impl: "{} |\<turnstile> {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 \<turnstile> {\<lambda>s. False} c {Q}"
+apply (rule cThin)
+apply (rule hoare_relative_complete)
+apply (auto simp add: valid_def)
+done
+
+lemma eFalse: "A \<turnstile>\<^sub>e {\<lambda>s. False} e {Q}"
+apply (rule eThin)
+apply (rule ehoare_relative_complete)
+apply (auto simp add: evalid_def)
+done
+
end
--- /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 \<noteq> Par"
+ Res_neq_This [simp]: "Res \<noteq> 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 \<preceq>C Nat = (D=Nat)"
+
+axioms method_Nat_add [simp]: "method Nat add = Some
+ \<lparr> 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 \<rparr>"
+
+axioms method_Nat_suc [simp]: "method Nat suc = Some
+ \<lparr> par=NT, res=Class Nat, lcl=[],
+ bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
+
+axioms field_Nat [simp]: "field Nat = empty(pred\<mapsto>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\<mapsto>(Nat, empty(pred\<mapsto>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 \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50)
+primrec "s:x\<ge>0 = (x\<noteq>Null)"
+ "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
+
+lemma Nat_atleast_lupd [rule_format, simp]:
+ "\<forall>s v. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
+apply (induct n)
+by auto
+
+lemma Nat_atleast_set_locs [rule_format, simp]:
+ "\<forall>s v. set_locs l s:v \<ge> n = (s:v \<ge> n)"
+apply (induct n)
+by auto
+
+lemma Nat_atleast_reset_locs [rule_format, simp]:
+ "\<forall>s v. reset_locs s:v \<ge> n = (s:v \<ge> n)"
+apply (induct n)
+by auto
+
+lemma Nat_atleast_NullD [rule_format]: "s:Null \<ge> n \<longrightarrow> False"
+apply (induct n)
+by auto
+
+lemma Nat_atleast_pred_NullD [rule_format]:
+"Null = get_field s a pred \<Longrightarrow> s:Addr a \<ge> n \<longrightarrow> n = 0"
+apply (induct n)
+by (auto dest: Nat_atleast_NullD)
+
+lemma Nat_atleast_mono [rule_format]:
+"\<forall>a. s:get_field s a pred \<ge> n \<longrightarrow> heap s a \<noteq> None \<longrightarrow> s:Addr a \<ge> n"
+apply (induct n)
+by auto
+
+lemma Nat_atleast_newC [rule_format]:
+ "heap s aa = None \<Longrightarrow> \<forall>v. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> 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:
+ "{} \<turnstile> {\<lambda>s. s:s<This> \<ge> X \<and> s:s<Par> \<ge> Y} Meth(Nat,add) {\<lambda>s. s:s<Res> \<ge> X+Y}"
+apply (rule hoare_ehoare.Meth)
+apply clarsimp
+apply (rule_tac P'= "\<lambda>Z s. (s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z) \<and> D=Nat" and
+ Q'= "\<lambda>Z s. s:s<Res> \<ge> 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 = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in Impl1)
+apply (clarsimp simp add: body_def)
+apply (rename_tac n m)
+apply (rule_tac Q = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and>
+ (\<exists>a. s<This> = Addr a \<and> 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 = "\<lambda>v s. (\<forall>m. n = Suc m \<longrightarrow> s:v \<ge> m) \<and> s:s<Par> \<ge> m" and
+ R = "\<lambda>T P s. (\<forall>m. n = Suc m \<longrightarrow> s:T \<ge> m) \<and> s:P \<ge> 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 \<Rightarrow> 0 | Suc m \<Rightarrow> 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
--- 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: "(\<lambda>t. \<exists>n. z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body M-n\<rightarrow> t)"
+lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)"
apply (rule ext)
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
done
--- 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";
--- 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 \<times> mname => stmt"
"body \<equiv> \<lambda>(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 \<leadsto> 'b) => ('a \<leadsto> val)"
"init_vars m == option_map (\<lambda>T. Null) o m"
-text {* private *}
+text {* private: *}
types heap = "loc \<leadsto> obj"
locals = "vname \<leadsto> val"
-text {* private *}
+text {* private: *}
record state
= heap :: heap
locals :: locals
@@ -56,7 +56,8 @@
"reset_locs s \<equiv> s (| locals := empty |)"
init_locs :: "cname => mname => state => state"
- "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)"
+ "init_locs C m s \<equiv> 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. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"
+
+subsection "Properties not used in the meta theory"
+
+lemma locals_upd_id [simp]: "s\<lparr>locals := locals s\<rparr> = s"
+by simp
+
+lemma lupd_get_local_same [simp]: "lupd(x\<mapsto>v) s<x> = v"
+by (simp add: lupd_def get_local_def)
+
+lemma lupd_get_local_other [simp]: "x \<noteq> y \<Longrightarrow> lupd(x\<mapsto>v) s<y> = s<y>"
+apply (drule not_sym)
+by (simp add: lupd_def get_local_def)
+
+lemma get_field_lupd [simp]:
+ "get_field (lupd(x\<mapsto>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 <x> = s<x>"
+by (simp add: new_obj_def hupd_def get_local_def)
+
+lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s"
+by (simp add: lupd_def)
+
+lemma heap_hupd_same [simp]: "heap (hupd(a\<mapsto>obj) s) a = Some obj"
+by (simp add: hupd_def)
+
+lemma heap_hupd_other [simp]: "aa \<noteq> a \<Longrightarrow> heap (hupd(aa\<mapsto>obj) s) a = heap s a"
+apply (drule not_sym)
+by (simp add: hupd_def)
+
+lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>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\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)"
+by (simp add: hupd_def lupd_def)
+
+lemma hupd_reset_locs [simp]:
+ "hupd(a\<mapsto>obj) (reset_locs s) = reset_locs (hupd(a\<mapsto>obj) s)"
+by (simp add: hupd_def reset_locs_def)
+
+lemma new_obj_lupd [simp]:
+ "new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>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\<mapsto>y) s) = lupd(x\<mapsto>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\<mapsto>(C, fs)) s) a = the \<circ> fs"
+apply (rule ext)
+by (simp add: get_field_def get_obj_def)
+
+lemma get_field_hupd_other [simp]:
+ "aa \<noteq> a \<Longrightarrow> get_field (hupd(aa\<mapsto>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 \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null"
apply (unfold new_Addr_def)
--- a/src/HOL/NanoJava/Term.thy Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Fri Sep 21 18:23:15 2001 +0200
@@ -18,7 +18,7 @@
Par :: vname --{* method parameter *}
Res :: vname --{* method result *}
-text {* Inequality axioms not required here *}
+text {* Inequality axioms are not required for the meta theory. *}
(*
axioms
This_neq_Par [simp]: "This \<noteq> Par"
@@ -29,8 +29,8 @@
datatype stmt
= Skip --{* empty statement *}
| Comp stmt stmt ("_;; _" [91,90 ] 90)
- | Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91)
- | Loop vname stmt ("While '(_') _" [99,91 ] 91)
+ | Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91)
+ | Loop vname stmt ("While '(_') _" [ 3,91 ] 91)
| LAss vname expr ("_ :== _" [99, 95] 94) --{* local assignment *}
| FAss expr fname expr ("_.._:==_" [95,99,95] 94) --{* field assignment *}
| Meth "cname \<times> mname" --{* virtual method *}
--- a/src/HOL/NanoJava/TypeRel.thy Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Fri Sep 21 18:23:15 2001 +0200
@@ -31,13 +31,13 @@
field :: "cname => (fname \<leadsto> ty)"
-text {* The rest of this theory is not actually used. *}
+subsection "Declarations and properties not used in the meta theory"
-text{* direct subclass relation *}
+text{* Direct subclass relation *}
defs
subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
-text{* widening, viz. method invocation conversion *}
+text{* Widening, viz. method invocation conversion *}
inductive widen intros
refl [intro!, simp]: "T \<preceq> T"
subcls : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
@@ -121,7 +121,7 @@
apply simp
done
---{* methods of a class, with inheritance and hiding *}
+--{* Methods of a class, with inheritance and hiding *}
defs method_def: "method C \<equiv> class_rec C methods"
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
@@ -132,7 +132,7 @@
done
---{* fields of a class, with inheritance and hiding *}
+--{* Fields of a class, with inheritance and hiding *}
defs field_def: "field C \<equiv> class_rec C fields"
lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
--- a/src/HOL/NanoJava/document/root.bib Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/document/root.bib Fri Sep 21 18:23:15 2001 +0200
@@ -1,3 +1,21 @@
+@misc{NanoJava,
+ author={Oheimb, David von and Tobias Nipkow},
+ title={Hoare Logic for {NanoJava}: Auxiliary Variables,
+ Side Effects and Virtual Methods revisited},
+ year = {2002},
+ abstract = {We give a Hoare logic for NanoJava,
+ a small fragment of Java with essentially just classes.
+ The logic is proved sound and (relatively) complete within Isabelle/HOL.
+ We introduce an elegant new approach for expressing auxiliary variables:
+ by universal quantification on the outer logical level.
+ Furthermore, we give simple means of handling side-effecting expressions
+ and dynamic binding within method calls.},
+ CRClassification = {D.3.1, F.3.2},
+ CRGenTerms = {Languages, Reliability, Theory, Verification},
+ url = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}},
+ note = {Submitted for publication.}
+}
+
@inproceedings{NipkowOP00,
author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
--- a/src/HOL/NanoJava/document/root.tex Mon Sep 17 19:49:09 2001 +0200
+++ b/src/HOL/NanoJava/document/root.tex Fri Sep 21 18:23:15 2001 +0200
@@ -36,7 +36,8 @@
implements a new approach for handling auxiliary variables.
A more complex Hoare logic covering a much larger subset of Java is described
in \cite{DvO-CPE01}.\\
-See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
+See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}
+and the conference version of this document \cite{NanoJava}.
\end{abstract}
\tableofcontents