added NanoJava
authoroheimb
Sat Jun 16 20:06:42 2001 +0200 (2001-06-16)
changeset 11376bf98ad1c22c6
parent 11375 a6730c90e753
child 11377 0f16ad464c62
added NanoJava
src/HOL/IsaMakefile
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/OpSem.thy
src/HOL/NanoJava/ROOT.ML
src/HOL/NanoJava/State.thy
src/HOL/NanoJava/Term.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/NanoJava/document/root.bib
src/HOL/NanoJava/document/root.tex
     1.1 --- a/src/HOL/IsaMakefile	Wed Jun 13 16:30:12 2001 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sat Jun 16 20:06:42 2001 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    HOL-MicroJava \
     1.5    HOL-MiniML \
     1.6    HOL-Modelcheck \
     1.7 +  HOL-NanoJava \
     1.8    HOL-NumberTheory \
     1.9    HOL-Prolog \
    1.10    HOL-Subst \
    1.11 @@ -460,6 +461,15 @@
    1.12    MicroJava/document/root.bib MicroJava/document/root.tex
    1.13  	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
    1.14  
    1.15 +## HOL-NanoJava
    1.16 +
    1.17 +HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
    1.18 +
    1.19 +$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
    1.20 +  NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
    1.21 +  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
    1.22 +  NanoJava/document/root.bib NanoJava/document/root.tex
    1.23 +	@$(ISATOOL) usedir $(OUT)/HOL NanoJava
    1.24  
    1.25  ## HOL-CTL
    1.26  
    1.27 @@ -581,7 +591,7 @@
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 -	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
    1.32 +	@rm -f  $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
    1.33  		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
    1.34  		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
    1.35  		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
    1.36 @@ -589,8 +599,8 @@
    1.37  		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.38  		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.39  		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.40 -		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
    1.41 -		$(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
    1.42 +		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-CTL.gz \
    1.43 +		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
    1.44  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
    1.45  		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
    1.46  		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/NanoJava/AxSem.thy	Sat Jun 16 20:06:42 2001 +0200
     2.3 @@ -0,0 +1,122 @@
     2.4 +(*  Title:      HOL/NanoJava/AxSem.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     David von Oheimb
     2.7 +    Copyright   2001 Technische Universitaet Muenchen
     2.8 +*)
     2.9 +
    2.10 +header "Axiomatic Semantics (Hoare Logic)"
    2.11 +
    2.12 +theory AxSem = State:
    2.13 +
    2.14 +types assn   = "state => bool"
    2.15 +      triple = "assn \<times> stmt \<times> assn"
    2.16 +translations
    2.17 +  "assn"   \<leftharpoondown> (type)"state => bool"
    2.18 +  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
    2.19 +
    2.20 +consts   hoare   :: "(triple set \<times> triple set) set"
    2.21 +syntax (xsymbols)
    2.22 + "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
    2.23 + "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
    2.24 +                                   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    2.25 +syntax
    2.26 + "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
    2.27 + "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
    2.28 +                                  ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
    2.29 +
    2.30 +translations "A |\<turnstile> C"       \<rightleftharpoons> "(A,C) \<in> hoare"
    2.31 +             "A  \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
    2.32 +
    2.33 +inductive hoare
    2.34 +intros
    2.35 +
    2.36 +  Skip:  "A |- {P} Skip {P}"
    2.37 +
    2.38 +  Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
    2.39 +
    2.40 +  Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q}; 
    2.41 +            A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q}  |] ==>
    2.42 +            A |- {P} If(e) c1 Else c2 {Q}"
    2.43 +
    2.44 +  Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
    2.45 +         A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
    2.46 +
    2.47 +  NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
    2.48 +              x:=new C {P}"
    2.49 +
    2.50 +  Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
    2.51 +              P (lupd(x|->s<y>) s)} x:=(C)y {P}"
    2.52 +
    2.53 +  FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
    2.54 +
    2.55 +  FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
    2.56 +
    2.57 +  Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and> 
    2.58 +                    s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
    2.59 +                  Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
    2.60 +             A |- {P} x:={C}y..m(p) {Q}"
    2.61 +
    2.62 +  Meth: "\<forall>D. A |- {\<lambda>s. \<exists>a. s<This> = Addr a \<and> D=obj_class s a \<and> D <=C C \<and> P s}
    2.63 +                  Impl D m {Q} ==>
    2.64 +             A |- {P} Meth C m {Q}"
    2.65 +
    2.66 +  (*\<Union>z instead of \<forall>z in the conclusion and
    2.67 +      z restricted to type state due to limitations of the inductive paackage *)
    2.68 +  Impl: "A\<union>   (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||- 
    2.69 +               (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
    2.70 +         A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
    2.71 +
    2.72 +(* structural rules *)
    2.73 +
    2.74 +  (* z restricted to type state due to limitations of the inductive paackage *)
    2.75 +  Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
    2.76 +             \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
    2.77 +            A |- {P} c {Q }"
    2.78 +
    2.79 +  Asm:  "   a \<in> A ==> A ||- {a}"
    2.80 +
    2.81 +  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
    2.82 +
    2.83 +  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
    2.84 +
    2.85 +
    2.86 +subsection "Derived Rules"
    2.87 +
    2.88 +lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
    2.89 +apply (rule hoare.Conseq)
    2.90 +apply  (rule allI, assumption)
    2.91 +apply fast
    2.92 +done
    2.93 +
    2.94 +lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
    2.95 +apply (rule hoare.ConjI)
    2.96 +apply clarify
    2.97 +apply (drule hoare.ConjE)
    2.98 +apply  fast
    2.99 +apply assumption
   2.100 +done
   2.101 +
   2.102 +lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
   2.103 +by (auto intro: hoare.ConjI hoare.ConjE)
   2.104 +
   2.105 +lemma Impl': 
   2.106 + "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
   2.107 +                (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
   2.108 +      A     ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
   2.109 +apply (drule Union[THEN iffD2])
   2.110 +apply (drule hoare.Impl)
   2.111 +apply (drule Union[THEN iffD1])
   2.112 +apply (erule spec)
   2.113 +done
   2.114 +
   2.115 +lemma Impl1: 
   2.116 + "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
   2.117 +                 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; 
   2.118 +  (C,m)\<in> ms\<rbrakk> \<Longrightarrow> 
   2.119 +       A    \<turnstile> {P z C m} Impl C m {Q (z::state) C m}"
   2.120 +apply (drule Impl')
   2.121 +apply (erule Weaken)
   2.122 +apply (auto del: image_eqI intro: rev_image_eqI)
   2.123 +done
   2.124 +
   2.125 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/NanoJava/Decl.thy	Sat Jun 16 20:06:42 2001 +0200
     3.3 @@ -0,0 +1,68 @@
     3.4 +(*  Title:      HOL/NanoJava/Decl.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     David von Oheimb
     3.7 +    Copyright   2001 Technische Universitaet Muenchen
     3.8 +*)
     3.9 +
    3.10 +header "Types, class Declarations, and whole programs"
    3.11 +
    3.12 +theory Decl = Term:
    3.13 +
    3.14 +datatype ty
    3.15 +  = NT           (* null type  *)
    3.16 +  | Class cname  (* class type *)
    3.17 +
    3.18 +types	fdecl		(* field declaration *)
    3.19 +	= "vnam \<times> ty"
    3.20 +
    3.21 +
    3.22 +record  methd		(* method declaration *)
    3.23 +	= par :: ty 
    3.24 +          res :: ty 
    3.25 +          lcl ::"(vname \<times> ty) list"
    3.26 +          bdy :: stmt
    3.27 +
    3.28 +types	mdecl    	(* method declaration *)
    3.29 +        = "mname \<times> methd"
    3.30 +
    3.31 +record	class		(* class *)
    3.32 +	= super   :: cname
    3.33 +          fields  ::"fdecl list"
    3.34 +          methods ::"mdecl list"
    3.35 +
    3.36 +types	cdecl		(* class declaration *)
    3.37 +	= "cname \<times> class"
    3.38 +
    3.39 +types   prog
    3.40 +        = "cdecl list"
    3.41 +
    3.42 +translations
    3.43 +  "fdecl" \<leftharpoondown> (type)"vname \<times> ty"
    3.44 +  "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
    3.45 +  "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
    3.46 +  "cdecl" \<leftharpoondown> (type)"cname \<times> class"
    3.47 +  "prog " \<leftharpoondown> (type)"cdecl list"
    3.48 +
    3.49 +consts
    3.50 +
    3.51 +  Prog    :: prog	(* program as a global value *)
    3.52 +
    3.53 +consts
    3.54 +
    3.55 +  Object  :: cname	(* name of root class *)
    3.56 +
    3.57 +
    3.58 +constdefs
    3.59 +  class	     :: "cname \<leadsto> class"
    3.60 + "class      \<equiv> map_of Prog"
    3.61 +
    3.62 +  is_class   :: "cname => bool"
    3.63 + "is_class C \<equiv> class C \<noteq> None"
    3.64 +
    3.65 +lemma finite_is_class: "finite {C. is_class C}"
    3.66 +apply (unfold is_class_def class_def)
    3.67 +apply (fold dom_def)
    3.68 +apply (rule finite_dom_map_of)
    3.69 +done
    3.70 +
    3.71 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Sat Jun 16 20:06:42 2001 +0200
     4.3 @@ -0,0 +1,237 @@
     4.4 +(*  Title:      HOL/NanoJava/Equivalence.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     David von Oheimb
     4.7 +    Copyright   2001 Technische Universitaet Muenchen
     4.8 +*)
     4.9 +
    4.10 +header "Equivalence of Operational and Axiomatic Semantics"
    4.11 +
    4.12 +theory Equivalence = OpSem + AxSem:
    4.13 +
    4.14 +subsection "Validity"
    4.15 +
    4.16 +constdefs
    4.17 +  valid   :: "[assn,stmt,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    4.18 + "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c-n-> t) --> Q t"
    4.19 +
    4.20 + nvalid   :: "[nat,       triple    ] => bool" ("|=_: _"  [61,61] 60)
    4.21 + "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c-n-> t --> P s --> Q t"
    4.22 +
    4.23 + nvalids  :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
    4.24 + "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
    4.25 +
    4.26 + cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"[61,61] 60)
    4.27 + "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
    4.28 +
    4.29 +syntax (xsymbols)
    4.30 +  valid   :: "[assn,stmt,assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    4.31 + nvalid   :: "[nat,       triple    ] => bool" ("\<Turnstile>_: _"   [61,61] 60)
    4.32 + nvalids  :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
    4.33 + cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
    4.34 +
    4.35 +syntax
    4.36 +  nvalid1::"[nat,        assn,stmt,assn] => bool" ( "|=_:.{(1_)}/ (_)/ {(1_)}"
    4.37 +                                                         [61,3,90,3] 60)
    4.38 + cnvalid1::"[triple set, assn,stmt,assn] => bool" ("_ ||=.{(1_)}/ (_)/ {(1_)}"
    4.39 +                                                         [61,3,90,3] 60)
    4.40 +syntax (xsymbols)
    4.41 +  nvalid1::"[nat,        assn,stmt,assn] => bool" (  "\<Turnstile>_:.{(1_)}/ (_)/ {(1_)}"
    4.42 +                                                         [61,3,90,3] 60)
    4.43 + cnvalid1::"[triple set, assn,stmt,assn] => bool" ( "_ |\<Turnstile>.{(1_)}/ (_)/ {(1_)}"
    4.44 +                                                         [61,3,90,3] 60)
    4.45 +translations
    4.46 + " \<Turnstile>n:.{P} c {Q}" \<rightleftharpoons> " \<Turnstile>n:  (P,c,Q)"
    4.47 + "A |\<Turnstile>.{P} c {Q}" \<rightleftharpoons> "A |\<Turnstile> {(P,c,Q)}"
    4.48 +
    4.49 +lemma nvalid1_def2: "\<Turnstile>n:.{P} c {Q} \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    4.50 +by (simp add: nvalid_def Let_def)
    4.51 +
    4.52 +lemma cnvalid1_def2: 
    4.53 +  "A |\<Turnstile>.{P} c {Q} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
    4.54 +by(simp add: nvalid1_def2 nvalids_def cnvalids_def)
    4.55 +
    4.56 +lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n:.{P} c {Q})"
    4.57 +apply (simp add: valid_def nvalid1_def2)
    4.58 +apply blast
    4.59 +done
    4.60 +
    4.61 +
    4.62 +subsection "Soundness"
    4.63 +
    4.64 +declare exec_elim_cases [elim!]
    4.65 +
    4.66 +lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
    4.67 +by (clarsimp simp add: nvalid1_def2)
    4.68 +
    4.69 +lemma Impl_nvalid_Suc: "\<Turnstile>n:.{P} body C m {Q} \<Longrightarrow> \<Turnstile>Suc n:.{P} Impl C m {Q}"
    4.70 +by (clarsimp simp add: nvalid1_def2)
    4.71 +
    4.72 +lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
    4.73 +by (force simp add: split_paired_all nvalid1_def2 intro: exec_mono)
    4.74 +
    4.75 +lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow>  Ball A (nvalid n)"
    4.76 +by (fast intro: nvalid_SucD)
    4.77 +
    4.78 +lemma Loop_sound_lemma [rule_format (no_asm)]: 
    4.79 +"\<lbrakk>\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<e> \<noteq> Null \<longrightarrow> P t; s -c0-n0\<rightarrow> t\<rbrakk> \<Longrightarrow> 
    4.80 +  P s \<longrightarrow> c0 = While (e) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<e> = Null"
    4.81 +apply (erule exec.induct)
    4.82 +apply clarsimp+
    4.83 +done
    4.84 +
    4.85 +lemma Impl_sound_lemma: 
    4.86 +"\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
    4.87 +          (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
    4.88 +by blast
    4.89 +
    4.90 +lemma hoare_sound_main: "A |\<turnstile> C \<Longrightarrow> A |\<Turnstile> C"
    4.91 +apply (erule hoare.induct)
    4.92 +apply (simp_all only: cnvalid1_def2)
    4.93 +apply clarsimp
    4.94 +apply clarsimp
    4.95 +apply (clarsimp split add: split_if_asm)
    4.96 +apply (clarsimp,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
    4.97 +apply clarsimp
    4.98 +apply clarsimp
    4.99 +apply clarsimp
   4.100 +apply clarsimp
   4.101 +apply (clarsimp del: Meth_elim_cases) (* Call *)
   4.102 +apply (clarsimp del: Impl_elim_cases) (* Meth *)
   4.103 +defer
   4.104 +apply blast (* Conseq *)
   4.105 +apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
   4.106 +apply blast
   4.107 +apply blast
   4.108 +apply blast
   4.109 +(* Impl *)
   4.110 +apply (erule thin_rl)
   4.111 +apply (rule allI)
   4.112 +apply (induct_tac "n")
   4.113 +apply  (clarify intro!: Impl_nvalid_0)
   4.114 +apply (clarify  intro!: Impl_nvalid_Suc)
   4.115 +apply (drule nvalids_SucD)
   4.116 +apply (erule (1) impE)
   4.117 +apply (drule (4) Impl_sound_lemma)
   4.118 +done
   4.119 +
   4.120 +theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
   4.121 +apply (simp only: valid_def2)
   4.122 +apply (drule hoare_sound_main)
   4.123 +apply (unfold cnvalids_def nvalids_def)
   4.124 +apply fast
   4.125 +done
   4.126 +
   4.127 +
   4.128 +subsection "(Relative) Completeness"
   4.129 +
   4.130 +constdefs MGT    :: "stmt => state => triple"
   4.131 +         "MGT c z \<equiv> (\<lambda> s. z = s, c, %t. \<exists>n. z -c-n-> t)"
   4.132 +
   4.133 +lemma MGF_implies_complete:
   4.134 + "\<forall>z. {} |\<turnstile> {MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
   4.135 +apply (simp only: valid_def2)
   4.136 +apply (unfold MGT_def)
   4.137 +apply (erule hoare.Conseq)
   4.138 +apply (clarsimp simp add: nvalid1_def2)
   4.139 +done
   4.140 +
   4.141 +
   4.142 +declare exec.intros[intro!]
   4.143 +
   4.144 +lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
   4.145 +  A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
   4.146 +apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
   4.147 +       in hoare.Conseq)
   4.148 +apply  (rule allI)
   4.149 +apply  (rule hoare.Loop)
   4.150 +apply  (erule hoare.Conseq)
   4.151 +apply  clarsimp
   4.152 +apply  (blast intro:rtrancl_into_rtrancl)
   4.153 +apply (erule thin_rl)
   4.154 +apply clarsimp
   4.155 +apply (erule_tac x = z in allE)
   4.156 +apply clarsimp
   4.157 +apply (erule converse_rtrancl_induct)
   4.158 +apply  blast
   4.159 +apply clarsimp
   4.160 +apply (drule (1) exec_max2)
   4.161 +apply (blast del: exec_elim_cases)
   4.162 +done
   4.163 +
   4.164 +lemma MGF_lemma[rule_format]:
   4.165 + "(\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z}) \<longrightarrow> (\<forall>z. A |\<turnstile> {MGT c z})"
   4.166 +apply (simp add: MGT_def)
   4.167 +apply (induct_tac c)
   4.168 +apply (tactic "ALLGOALS Clarify_tac")
   4.169 +
   4.170 +apply (rule Conseq1 [OF hoare.Skip])
   4.171 +apply blast
   4.172 +
   4.173 +apply (rule hoare.Comp)
   4.174 +apply  (erule spec)
   4.175 +apply (erule hoare.Conseq)
   4.176 +apply (erule thin_rl, erule thin_rl)
   4.177 +apply clarsimp
   4.178 +apply (drule (1) exec_max2)
   4.179 +apply blast
   4.180 +
   4.181 +apply (rule hoare.Cond)
   4.182 +apply  (erule hoare.Conseq)
   4.183 +apply  (erule thin_rl, erule thin_rl)
   4.184 +apply  force
   4.185 +apply (erule hoare.Conseq)
   4.186 +apply (erule thin_rl, erule thin_rl)
   4.187 +apply force
   4.188 +
   4.189 +apply (erule MGF_Loop)
   4.190 +
   4.191 +apply (rule Conseq1 [OF hoare.NewC])
   4.192 +apply blast
   4.193 +
   4.194 +apply (rule Conseq1 [OF hoare.Cast])
   4.195 +apply blast
   4.196 +
   4.197 +apply (rule Conseq1 [OF hoare.FAcc])
   4.198 +apply blast
   4.199 +
   4.200 +apply (rule Conseq1 [OF hoare.FAss])
   4.201 +apply blast
   4.202 +
   4.203 +apply (rule hoare.Call)
   4.204 +apply (rule allI)
   4.205 +apply (rule hoare.Meth)
   4.206 +apply (rule allI)
   4.207 +apply (drule spec, drule spec, erule hoare.Conseq)
   4.208 +apply blast
   4.209 +
   4.210 +apply (rule hoare.Meth)
   4.211 +apply (rule allI)
   4.212 +apply (drule spec, drule spec, erule hoare.Conseq)
   4.213 +apply blast
   4.214 +
   4.215 +apply blast
   4.216 +done
   4.217 +
   4.218 +lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
   4.219 +apply (unfold MGT_def)
   4.220 +apply (rule Impl1)
   4.221 +apply  (rule_tac [2] UNIV_I)
   4.222 +apply clarsimp
   4.223 +apply (rule hoare.ConjI)
   4.224 +apply clarsimp
   4.225 +apply (rule ssubst [OF Impl_body_eq])
   4.226 +apply (fold MGT_def)
   4.227 +apply (rule MGF_lemma)
   4.228 +apply (rule hoare.Asm)
   4.229 +apply force
   4.230 +done
   4.231 +
   4.232 +theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
   4.233 +apply (rule MGF_implies_complete)
   4.234 +apply  (erule_tac [2] asm_rl)
   4.235 +apply (rule allI)
   4.236 +apply (rule MGF_lemma)
   4.237 +apply (rule MGF_Impl)
   4.238 +done
   4.239 +
   4.240 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/NanoJava/OpSem.thy	Sat Jun 16 20:06:42 2001 +0200
     5.3 @@ -0,0 +1,89 @@
     5.4 +(*  Title:      HOL/NanoJava/OpSem.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     David von Oheimb
     5.7 +    Copyright   2001 Technische Universitaet Muenchen
     5.8 +*)
     5.9 +
    5.10 +header "Operational Evaluation Semantics"
    5.11 +
    5.12 +theory OpSem = State:
    5.13 +
    5.14 +consts
    5.15 +  exec :: "(state \<times> stmt \<times> nat \<times> state) set"
    5.16 +syntax (xsymbols)
    5.17 +  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_\<rightarrow> _" [98,90,99,98] 89)
    5.18 +syntax
    5.19 +  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_-> _" [98,90,99,98] 89)
    5.20 +translations
    5.21 +  "s -c-n-> s'" == "(s, c, n, s') \<in> exec"
    5.22 +
    5.23 +inductive exec intros
    5.24 +
    5.25 +  Skip: "   s -Skip-n-> s"
    5.26 +
    5.27 +  Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
    5.28 +            s0 -c1;; c2-n-> s2"
    5.29 +
    5.30 +  Cond: "[| s -(if s<e> \<noteq> Null then c1 else c2)-n-> s' |] ==>
    5.31 +            s -If(e) c1 Else c2-n-> s'"
    5.32 +
    5.33 +  LoopF:"   s0<e> = Null ==>
    5.34 +            s0 -While(e) c-n-> s0"
    5.35 +  LoopT:"[| s0<e> \<noteq> Null; s0 -c-n-> s1; s1 -While(e) c-n-> s2 |] ==>
    5.36 +            s0 -While(e) c-n-> s2"
    5.37 +
    5.38 +  NewC: "   new_Addr s = Addr a ==>
    5.39 +            s -x:=new C-n-> lupd(x\<mapsto>Addr a)(new_obj a C s)"
    5.40 +
    5.41 +  Cast: "  (case s<y> of Null => True | Addr a => obj_class s a \<preceq>C C) ==>
    5.42 +            s -x:=(C)y-n-> lupd(x\<mapsto>s<y>) s"
    5.43 +
    5.44 +  FAcc: "   s<y> = Addr a ==>
    5.45 +            s -x:=y..f-n-> lupd(x\<mapsto>get_field s a f) s"
    5.46 +
    5.47 +  FAss: "   s<y> = Addr a ==>
    5.48 +            s -y..f:=x-n-> upd_obj a f (s<x>) s"
    5.49 +
    5.50 +  Call: "lupd(This\<mapsto>s<y>)(lupd(Param\<mapsto>s<p>)(init_locs C m s))-Meth C m -n-> s'==>
    5.51 +            s -x:={C}y..m(p)-n-> lupd(x\<mapsto>s'<Res>)(set_locs s s')"
    5.52 +
    5.53 +  Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
    5.54 +            s -Impl (obj_class s a) m-n-> s' |] ==>
    5.55 +            s -Meth C m-n-> s'"
    5.56 +
    5.57 +  Impl: "   s -body C m-    n-> s' ==>
    5.58 +            s -Impl C m-Suc n-> s'"
    5.59 +
    5.60 +inductive_cases exec_elim_cases':
    5.61 +	"s -Skip            -n-> t"
    5.62 +	"s -c1;; c2         -n-> t"
    5.63 +	"s -If(e) c1 Else c2-n-> t"
    5.64 +	"s -While(e) c      -n-> t"
    5.65 +	"s -x:=new C        -n-> t"
    5.66 +	"s -x:=(C)y         -n-> t"
    5.67 +	"s -x:=y..f         -n-> t"
    5.68 +	"s -y..f:=x         -n-> t"
    5.69 +	"s -x:={C}y..m(p)   -n-> t"
    5.70 +inductive_cases Meth_elim_cases: "s -Meth C m -n-> t"
    5.71 +inductive_cases Impl_elim_cases: "s -Impl C m -n-> t"
    5.72 +lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
    5.73 +
    5.74 +lemma exec_mono [rule_format]: "s -c-n\<rightarrow> t \<Longrightarrow> \<forall>m. n \<le> m \<longrightarrow> s -c-m\<rightarrow> t"
    5.75 +apply (erule exec.induct)
    5.76 +prefer 12 (* Impl *)
    5.77 +apply clarify
    5.78 +apply (rename_tac n)
    5.79 +apply (case_tac n)
    5.80 +apply (blast intro:exec.intros)+
    5.81 +done
    5.82 +
    5.83 +lemma exec_max2: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-        n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
    5.84 +                   s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
    5.85 +by (fast intro: exec_mono le_maxI1 le_maxI2)
    5.86 +
    5.87 +lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl C m-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body C m-n\<rightarrow> t)"
    5.88 +apply (rule ext)
    5.89 +apply (fast elim: exec_elim_cases intro: exec.Impl)
    5.90 +done
    5.91 +
    5.92 +end
    5.93 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/NanoJava/ROOT.ML	Sat Jun 16 20:06:42 2001 +0200
     6.3 @@ -0,0 +1,1 @@
     6.4 +use_thy "Equivalence";
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/NanoJava/State.thy	Sat Jun 16 20:06:42 2001 +0200
     7.3 @@ -0,0 +1,111 @@
     7.4 +(*  Title:      HOL/NanoJava/State.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     David von Oheimb
     7.7 +    Copyright   2001 Technische Universitaet Muenchen
     7.8 +*)
     7.9 +
    7.10 +header "Program State"
    7.11 +
    7.12 +theory State = TypeRel:
    7.13 +
    7.14 +constdefs
    7.15 +
    7.16 +  body :: "cname => mname => stmt"
    7.17 + "body C m \<equiv> bdy (the (method C m))"
    7.18 +
    7.19 +text {* locations, i.e.\ abstract references to objects *}
    7.20 +typedecl loc 
    7.21 +arities  loc :: "term"
    7.22 +
    7.23 +datatype val
    7.24 +  = Null        (* null reference *)
    7.25 +  | Addr loc    (* address, i.e. location of object *)
    7.26 +
    7.27 +types	fields
    7.28 +	= "(vnam \<leadsto> val)"
    7.29 +
    7.30 +        obj = "cname \<times> fields"
    7.31 +
    7.32 +translations
    7.33 +
    7.34 +  "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option"
    7.35 +  "obj"    \<leftharpoondown> (type)"cname \<times> fields"
    7.36 +
    7.37 +constdefs
    7.38 +
    7.39 +  init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
    7.40 + "init_vars m == option_map (\<lambda>T. Null) o m"
    7.41 +  
    7.42 +text {* private *}
    7.43 +types	heap   = "loc   \<leadsto> obj"
    7.44 +        locals = "vname \<leadsto> val"	
    7.45 +
    7.46 +text {* private *}
    7.47 +record  state
    7.48 +	= heap   :: heap
    7.49 +          locals :: locals
    7.50 +
    7.51 +translations
    7.52 +
    7.53 +  "heap"   \<leftharpoondown> (type)"loc   => obj option"
    7.54 +  "locals" \<leftharpoondown> (type)"vname => val option"
    7.55 +  "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
    7.56 +
    7.57 +constdefs
    7.58 +
    7.59 +  init_locs     :: "cname => mname => state => state"
    7.60 + "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m))))|)"
    7.61 +
    7.62 +text {* The first parameter of @{term set_locs} is of type @{typ state} 
    7.63 +        rather than @{typ locals} in order to keep @{typ locals} private.*}
    7.64 +constdefs
    7.65 +  set_locs  :: "state => state => state"
    7.66 + "set_locs s s' \<equiv> s' (| locals := locals s |)"
    7.67 +
    7.68 +  get_local     :: "state => vname => val" ("_<_>" [99,0] 99)
    7.69 + "get_local s x  \<equiv> the (locals s x)"
    7.70 +
    7.71 +(* local function: *)
    7.72 +  get_obj       :: "state => loc => obj"
    7.73 + "get_obj s a \<equiv> the (heap s a)"
    7.74 +
    7.75 +  obj_class     :: "state => loc => cname"
    7.76 + "obj_class s a \<equiv> fst (get_obj s a)"
    7.77 +
    7.78 +  get_field     :: "state => loc => vnam => val"
    7.79 + "get_field s a f \<equiv> the (snd (get_obj s a) f)"
    7.80 +
    7.81 +constdefs
    7.82 +
    7.83 +(* local function: *)
    7.84 +  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_|->_')" [10,10] 1000)
    7.85 + "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
    7.86 +
    7.87 +  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000)
    7.88 + "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
    7.89 +
    7.90 +syntax (xsymbols)
    7.91 +  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
    7.92 +  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
    7.93 +
    7.94 +constdefs
    7.95 +
    7.96 +  new_obj    :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state"
    7.97 + "new_obj a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
    7.98 +
    7.99 +  upd_obj    :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
   7.100 + "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"
   7.101 +
   7.102 +  new_Addr	:: "state => val"
   7.103 + "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"
   7.104 +
   7.105 +lemma new_AddrD: 
   7.106 +"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null"
   7.107 +apply (unfold new_Addr_def)
   7.108 +apply (erule subst)
   7.109 +apply (rule someI)
   7.110 +apply (rule disjI2)
   7.111 +apply (rule HOL.refl)
   7.112 +done
   7.113 +
   7.114 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/NanoJava/Term.thy	Sat Jun 16 20:06:42 2001 +0200
     8.3 @@ -0,0 +1,46 @@
     8.4 +(*  Title:      HOL/NanoJava/Term.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     David von Oheimb
     8.7 +    Copyright   2001 Technische Universitaet Muenchen
     8.8 +*)
     8.9 +
    8.10 +header "Statements and expression emulations"
    8.11 +
    8.12 +theory Term = Main:
    8.13 +
    8.14 +typedecl cname  (* class name *)
    8.15 +typedecl vnam   (* variable or field name *)
    8.16 +typedecl mname  (* method name *)
    8.17 +arities  cname :: "term"
    8.18 +         vnam  :: "term"
    8.19 +         mname :: "term"
    8.20 +
    8.21 +datatype vname  (* variable for special names *)
    8.22 +  = This        (* This pointer *)
    8.23 +  | Param       (* method parameter *)
    8.24 +  | Res         (* method result *)
    8.25 +  | VName vnam 
    8.26 +
    8.27 +datatype stmt
    8.28 +  = Skip                   (* empty statement *)
    8.29 +  | Comp       stmt stmt   ("_;; _"             [91,90]    90)
    8.30 +  | Cond vname stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
    8.31 +  | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
    8.32 +
    8.33 +  | NewC vname cname       ("_:=new _"  [99,   99] 95) (* object creation  *)
    8.34 +  | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
    8.35 +  | FAcc vname vname vnam  ("_:=_.._"   [99,99,99] 95) (* field access     *)
    8.36 +  | FAss vname vnam  vname ("_.._:=_"   [99,99,99] 95) (* field assigment  *)
    8.37 +  | Call vname cname vname mname vname                 (* method call      *)
    8.38 +                           ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
    8.39 +  | Meth cname mname       (* virtual method *)
    8.40 +  | Impl cname mname       (* method implementation *)
    8.41 +
    8.42 +(*###TO Product_Type_lemmas.ML*)
    8.43 +lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
    8.44 +apply (rule_tac x = "(a,b)" in image_eqI)
    8.45 +apply  auto
    8.46 +done
    8.47 +
    8.48 +end
    8.49 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Sat Jun 16 20:06:42 2001 +0200
     9.3 @@ -0,0 +1,145 @@
     9.4 +(*  Title:      HOL/NanoJava/TypeRel.thy
     9.5 +    ID:         $Id$
     9.6 +    Author:     David von Oheimb
     9.7 +    Copyright   2001 Technische Universitaet Muenchen
     9.8 +*)
     9.9 +
    9.10 +header "Type relations"
    9.11 +
    9.12 +theory TypeRel = Decl:
    9.13 +
    9.14 +consts
    9.15 +  widen   :: "(ty    \<times> ty   ) set"  (* widening *)
    9.16 +  subcls1 :: "(cname \<times> cname) set"  (* subclass *)
    9.17 +
    9.18 +syntax (xsymbols)
    9.19 +  widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
    9.20 +  subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _"  [71,71] 70)
    9.21 +  subcls  :: "[cname, cname] => bool" ("_ \<preceq>C _"   [71,71] 70)
    9.22 +syntax
    9.23 +  widen   :: "[ty   , ty   ] => bool" ("_ <= _"   [71,71] 70)
    9.24 +  subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
    9.25 +  subcls  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
    9.26 +
    9.27 +translations
    9.28 +  "C \<prec>C1 D" == "(C,D) \<in> subcls1"
    9.29 +  "C \<preceq>C  D" == "(C,D) \<in> subcls1^*"
    9.30 +  "S \<preceq>   T" == "(S,T) \<in> widen"
    9.31 +
    9.32 +consts
    9.33 +  method :: "cname => (mname \<leadsto> methd)"
    9.34 +  field  :: "cname => (vnam  \<leadsto> ty)"
    9.35 +
    9.36 +
    9.37 +text {* The rest of this theory is not actually used. *}
    9.38 +
    9.39 +defs
    9.40 +  (* direct subclass relation *)
    9.41 + subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
    9.42 +  
    9.43 +inductive widen intros (*widening, viz. method invocation conversion,
    9.44 +			           i.e. sort of syntactic subtyping *)
    9.45 +  refl   [intro!, simp]:           "T \<preceq> T"
    9.46 +  subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    9.47 +  null   [intro!]:                "NT \<preceq> R"
    9.48 +
    9.49 +lemma subcls1D: 
    9.50 +  "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
    9.51 +apply (unfold subcls1_def)
    9.52 +apply auto
    9.53 +done
    9.54 +
    9.55 +lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D"
    9.56 +apply (unfold subcls1_def)
    9.57 +apply auto
    9.58 +done
    9.59 +
    9.60 +lemma subcls1_def2: 
    9.61 +"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
    9.62 +apply (unfold subcls1_def is_class_def)
    9.63 +apply auto
    9.64 +done
    9.65 +
    9.66 +lemma finite_subcls1: "finite subcls1"
    9.67 +apply(subst subcls1_def2)
    9.68 +apply(rule finite_SigmaI [OF finite_is_class])
    9.69 +apply(rule_tac B = "{super (the (class C))}" in finite_subset)
    9.70 +apply  auto
    9.71 +done
    9.72 +
    9.73 +constdefs
    9.74 +
    9.75 +  ws_prog  :: "bool"
    9.76 + "ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> 
    9.77 +                              is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
    9.78 +
    9.79 +lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow>  
    9.80 +  is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
    9.81 +apply (unfold ws_prog_def class_def)
    9.82 +apply (drule_tac map_of_SomeD)
    9.83 +apply auto
    9.84 +done
    9.85 +
    9.86 +lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
    9.87 +by (fast dest: subcls1D ws_progD)
    9.88 +
    9.89 +(* context (theory "Transitive_Closure") *)
    9.90 +lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    9.91 +apply (rule allI)
    9.92 +apply (erule irrefl_tranclI)
    9.93 +done
    9.94 +
    9.95 +lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
    9.96 +
    9.97 +lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y"
    9.98 +apply (rule irrefl_trancl_rD)
    9.99 +apply (rule subcls1_irrefl_lemma2)
   9.100 +apply auto
   9.101 +done
   9.102 +
   9.103 +lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
   9.104 +
   9.105 +lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
   9.106 +by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
   9.107 +
   9.108 +
   9.109 +consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
   9.110 +
   9.111 +recdef class_rec "subcls1\<inverse>"
   9.112 +      "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> arbitrary 
   9.113 +                                        | Some m \<Rightarrow> if wf (subcls1\<inverse>) 
   9.114 +       then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
   9.115 +       else arbitrary)"
   9.116 +(hints intro: subcls1I)
   9.117 +
   9.118 +lemma class_rec: "\<lbrakk>class C = Some m;  ws_prog\<rbrakk> \<Longrightarrow>
   9.119 + class_rec C f = (if C = Object then empty else class_rec (super m) f) ++ 
   9.120 +                 map_of (f m)";
   9.121 +apply (drule wf_subcls1)
   9.122 +apply (rule class_rec.simps [THEN trans [THEN fun_cong]])
   9.123 +apply  assumption
   9.124 +apply simp
   9.125 +done
   9.126 +
   9.127 +(* methods of a class, with inheritance and hiding *)
   9.128 +defs method_def: "method C \<equiv> class_rec C methods"
   9.129 +
   9.130 +lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
   9.131 +method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
   9.132 +apply (unfold method_def)
   9.133 +apply (erule (1) class_rec [THEN trans]);
   9.134 +apply simp
   9.135 +done
   9.136 +
   9.137 +
   9.138 +(* fields of a class, with inheritance and hiding *)
   9.139 +defs field_def: "field C \<equiv> class_rec C fields"
   9.140 +
   9.141 +lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
   9.142 +field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
   9.143 +apply (unfold field_def)
   9.144 +apply (erule (1) class_rec [THEN trans]);
   9.145 +apply simp
   9.146 +done
   9.147 +
   9.148 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/NanoJava/document/root.bib	Sat Jun 16 20:06:42 2001 +0200
    10.3 @@ -0,0 +1,58 @@
    10.4 +@inproceedings{NipkowOP00,
    10.5 +        author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
    10.6 +        title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
    10.7 +        booktitle = {Foundations of Secure Computation},
    10.8 +        series= {NATO Science Series F: Computer and Systems Sciences},
    10.9 +        volume = {175},
   10.10 +        year = {2000},
   10.11 +        publisher = {IOS Press},
   10.12 +        editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
   10.13 +        abstract = {This paper introduces the subset $micro$Java of Java,
   10.14 +essentially by omitting everything but classes.
   10.15 +The type system and semantics of this language
   10.16 +(and a corresponding abstract Machine $micro$JVM)
   10.17 +are formalized in the theorem prover Isabelle/HOL.
   10.18 +Type safety both of $micro$Java and the $micro$JVM
   10.19 +are mechanically verified.
   10.20 +
   10.21 +To make the paper self-contained, it starts with
   10.22 +introductions to Isabelle/HOL and the art of
   10.23 +embedding languages in theorem provers.},
   10.24 +        CRClassification = {D.3.1, F.3.2},
   10.25 +        CRGenTerms = {Languages, Reliability, Theory, Verification},
   10.26 +        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
   10.27 +        pages = {117--144}
   10.28 +}
   10.29 +
   10.30 +
   10.31 +@article{DvO-CPE01,
   10.32 +        author = {David von Oheimb},
   10.33 +        title = {Hoare Logic for {J}ava in {Isabelle/HOL}},
   10.34 +        journal = {Concurrency: Practice and Experience},
   10.35 +        year = {2001},
   10.36 +        url = {http://www4.in.tum.de/papers/DvO-CPE01.html},
   10.37 +        abstract = {
   10.38 +This article presents a Hoare-style calculus for a substantial subset 
   10.39 +of Java Card, which we call Java_light. In particular, the language 
   10.40 +includes side-effecting expressions, mutual recursion, dynamic method 
   10.41 +binding, full exception handling, and static class initialization.
   10.42 +
   10.43 +The Hoare logic of partial correctness is proved not only sound (w.r.t.
   10.44 +our operational semantics of Java_light, described in detail elsewhere)
   10.45 +but even complete. It is the first logic for an object-oriented 
   10.46 +language that is provably complete.
   10.47 +The completeness proof uses a refinement of the Most General Formula 
   10.48 +approach. The proof of soundness gives new insights into the role of 
   10.49 +type safety. Further by-products of this work are a new general 
   10.50 +methodology for handling side-effecting expressions and their results, 
   10.51 +the discovery of the strongest possible rule of consequence, and a 
   10.52 +flexible Call rule for mutual recursion. 
   10.53 +We also give a small but non-trivial application example.
   10.54 +
   10.55 +All definitions and proofs have been done formally with the interactive 
   10.56 +theorem prover Isabelle/HOL. This guarantees not only rigorous definitions, 
   10.57 +but also gives maximal confidence in the results obtained.},
   10.58 +        CRClassification = {D.2.4, D.3.1, F.3.1},
   10.59 +        CRGenTerms = {Languages, Verification, Theory},
   10.60 +        note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
   10.61 +}
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/NanoJava/document/root.tex	Sat Jun 16 20:06:42 2001 +0200
    11.3 @@ -0,0 +1,57 @@
    11.4 +\documentclass[11pt,a4paper]{article}
    11.5 +\usepackage{latexsym,isabelle,isabellesym,latexsym,pdfsetup}
    11.6 +
    11.7 +\urlstyle{tt}
    11.8 +\pagestyle{myheadings}
    11.9 +
   11.10 +\addtolength{\hoffset}{-1,5cm}
   11.11 +\addtolength{\textwidth}{4cm}
   11.12 +\addtolength{\voffset}{-2cm}
   11.13 +\addtolength{\textheight}{4cm}
   11.14 +
   11.15 +%subsection instead of section to make the toc readable
   11.16 +\renewcommand{\thesubsection}{\arabic{subsection}}
   11.17 +\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
   11.18 +\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
   11.19 +
   11.20 +%remove spaces from the isabelle environment (trivlist makes them too large)
   11.21 +\renewenvironment{isabelle}
   11.22 +{\begin{isabellebody}}
   11.23 +{\end{isabellebody}}
   11.24 +
   11.25 +\newcommand{\nJava}{\it NanoJava}
   11.26 +
   11.27 +%remove clutter from the toc
   11.28 +\setcounter{secnumdepth}{3}
   11.29 +\setcounter{tocdepth}{2}
   11.30 +
   11.31 +\begin{document}
   11.32 +
   11.33 +\title{\nJava}
   11.34 +\author{David von Oheimb \\ Tobias Nipkow}
   11.35 +\maketitle
   11.36 +
   11.37 +\begin{abstract}\noindent
   11.38 +  These theories define {\nJava}, a very small fragment of the programming 
   11.39 +  language Java (with essentially just classes) derived from the one given 
   11.40 +  in \cite{NipkowOP00}.
   11.41 +  For {\nJava}, an operational semantics is given as well as a Hoare logic,
   11.42 +  which is proved both sound and (relatively) complete. The Hoare logic
   11.43 +  implements a new approach for handling auxiliary variables.
   11.44 +  A more complex Hoare logic covering a much larger subset of Java is described
   11.45 +  in \cite{DvO-CPE01}.\\
   11.46 +See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
   11.47 +\end{abstract}
   11.48 +
   11.49 +\tableofcontents
   11.50 +\parindent 0pt \parskip 0.5ex
   11.51 +
   11.52 +\newpage
   11.53 +\input{session}
   11.54 +
   11.55 +\newpage
   11.56 +\nocite{*}
   11.57 +\bibliographystyle{abbrv}
   11.58 +\bibliography{root}
   11.59 +
   11.60 +\end{document}