exception merge, cleanup, tuned
authorkleing
Sun Dec 16 00:18:17 2001 +0100 (2001-12-16)
changeset 12517360e3215f029
parent 12516 d09d0f160888
child 12518 521f2da133be
exception merge, cleanup, tuned
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
     1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Sun Dec 16 00:17:44 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Sun Dec 16 00:18:17 2001 +0100
     1.3 @@ -8,14 +8,14 @@
     1.4  
     1.5  theory Conform = State + WellType:
     1.6  
     1.7 -types	'c env_ = "'c prog \<times> (vname \<leadsto> ty)" (* same as env of WellType.thy *)
     1.8 +types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)"  -- "same as @{text env} of @{text WellType.thy}"
     1.9  
    1.10  constdefs
    1.11  
    1.12    hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50)
    1.13   "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
    1.14  
    1.15 -  conf :: "'c prog => aheap => val => ty => bool"	
    1.16 +  conf :: "'c prog => aheap => val => ty => bool" 
    1.17                                     ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
    1.18   "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    1.19  
    1.20 @@ -29,7 +29,7 @@
    1.21    hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
    1.22   "G|-h h [ok]    == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
    1.23  
    1.24 -  conforms :: "state => java_mb env_ => bool"	("_ ::<= _" [51,51] 50)
    1.25 +  conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
    1.26   "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
    1.27  
    1.28  
    1.29 @@ -112,7 +112,8 @@
    1.30  apply (simp)
    1.31  done
    1.32  
    1.33 -lemma defval_conf [rule_format (no_asm)]: "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
    1.34 +lemma defval_conf [rule_format (no_asm)]: 
    1.35 +  "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
    1.36  apply (unfold conf_def)
    1.37  apply (rule_tac "y" = "T" in ty.exhaust)
    1.38  apply  (erule ssubst)
    1.39 @@ -127,7 +128,8 @@
    1.40  apply auto
    1.41  done
    1.42  
    1.43 -lemma conf_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"
    1.44 +lemma conf_widen [rule_format (no_asm)]: 
    1.45 +  "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"
    1.46  apply (unfold conf_def)
    1.47  apply (rule val.induct)
    1.48  apply (auto intro: widen_trans)
    1.49 @@ -168,7 +170,8 @@
    1.50  apply (fast dest: non_npD)
    1.51  done
    1.52  
    1.53 -lemma non_np_objD' [rule_format (no_asm)]: "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
    1.54 +lemma non_np_objD' [rule_format (no_asm)]: 
    1.55 +  "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
    1.56    (\<forall>C. t = ClassT C --> C \<noteq> Object) -->  
    1.57    (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
    1.58  apply(rule_tac "y" = "t" in ref_ty.exhaust)
    1.59 @@ -176,7 +179,9 @@
    1.60  apply (fast dest: non_np_objD)
    1.61  done
    1.62  
    1.63 -lemma conf_list_gext_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"
    1.64 +lemma conf_list_gext_widen [rule_format (no_asm)]: 
    1.65 +  "wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> 
    1.66 +  list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"
    1.67  apply(induct_tac "vs")
    1.68   apply(clarsimp)
    1.69  apply(clarsimp)
    1.70 @@ -208,7 +213,8 @@
    1.71  apply auto
    1.72  done
    1.73  
    1.74 -lemma lconf_init_vars_lemma [rule_format (no_asm)]: "\<forall>x. P x --> R (dv x) x ==> (\<forall>x. map_of fs f = Some x --> P x) -->  
    1.75 +lemma lconf_init_vars_lemma [rule_format (no_asm)]: 
    1.76 +  "\<forall>x. P x --> R (dv x) x ==> (\<forall>x. map_of fs f = Some x --> P x) -->  
    1.77    (\<forall>T. map_of fs f = Some T -->  
    1.78    (\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and>  R v T))"
    1.79  apply( induct_tac "fs")
    1.80 @@ -231,7 +237,9 @@
    1.81  apply auto
    1.82  done
    1.83  
    1.84 -lemma lconf_ext_list [rule_format (no_asm)]: "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
    1.85 +lemma lconf_ext_list [rule_format (no_asm)]: 
    1.86 +  "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. nodups vns --> length Ts = length vns --> 
    1.87 +  list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
    1.88  apply (unfold lconf_def)
    1.89  apply( induct_tac "vns")
    1.90  apply(  clarsimp)
    1.91 @@ -291,12 +299,14 @@
    1.92  apply( fast dest: conforms_localD elim!: conformsI lconf_hext)
    1.93  done
    1.94  
    1.95 -lemma conforms_upd_obj: "[|(h,l)::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] ==> (h(a\<mapsto>obj),l)::\<preceq>(G, lT)"
    1.96 -apply( rule conforms_hext)
    1.97 -apply   auto
    1.98 -apply( rule hconfI)
    1.99 -apply( drule conforms_heapD)
   1.100 -apply( tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
   1.101 +lemma conforms_upd_obj: 
   1.102 +  "[|(h,l)::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] ==> (h(a\<mapsto>obj),l)::\<preceq>(G, lT)"
   1.103 +apply(rule conforms_hext)
   1.104 +apply  auto
   1.105 +apply(rule hconfI)
   1.106 +apply(drule conforms_heapD)
   1.107 +apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] 
   1.108 +                addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
   1.109  done
   1.110  
   1.111  lemma conforms_upd_local: 
     2.1 --- a/src/HOL/MicroJava/J/Decl.thy	Sun Dec 16 00:17:44 2001 +0100
     2.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Sun Dec 16 00:18:17 2001 +0100
     2.3 @@ -4,38 +4,28 @@
     2.4      Copyright   1999 Technische Universitaet Muenchen
     2.5  *)
     2.6  
     2.7 -header "Class Declarations and whole Programs"
     2.8 +header "Class Declarations and Programs"
     2.9  
    2.10  theory Decl = Type:
    2.11  
    2.12 -types	fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
    2.13 -	= "vname \<times> ty"
    2.14 +types 
    2.15 +  fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
    2.16 +
    2.17 +  sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
    2.18 +
    2.19 +  'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
    2.20 +
    2.21 +  'c class = "cname \<times> fdecl list \<times> 'c mdecl list" 
    2.22 +  -- "class = superclass, fields, methods"
    2.23 +
    2.24 +  'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
    2.25 +
    2.26 +  'c prog  = "'c cdecl list"     -- "program"
    2.27  
    2.28  
    2.29 -types	sig		(* signature of a method, cf. 8.4.2 *)
    2.30 -	= "mname \<times> ty list"
    2.31 -
    2.32 -	'c mdecl		(* method declaration in a class *)
    2.33 -	= "sig \<times> ty \<times> 'c"
    2.34 -
    2.35 -types	'c class		(* class *)
    2.36 -	= "cname \<times> fdecl list \<times> 'c mdecl list"
    2.37 -	(* superclass, fields, methods*)
    2.38 -
    2.39 -	'c cdecl		(* class declaration, cf. 8.1 *)
    2.40 -	= "cname \<times> 'c class"
    2.41 -
    2.42 -consts
    2.43 -
    2.44 -  Object  :: cname	(* name of root class *)
    2.45 -  ObjectC :: "'c cdecl"	(* decl of root class *)
    2.46 -
    2.47 -defs 
    2.48 -
    2.49 - ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))"
    2.50 -
    2.51 -
    2.52 -types 'c prog = "'c cdecl list"
    2.53 +constdefs
    2.54 +  ObjectC :: "'c cdecl" -- "decl of root class"
    2.55 +  "ObjectC \<equiv> (Object, (arbitrary, [], []))"
    2.56  
    2.57  
    2.58  translations
    2.59 @@ -46,12 +36,14 @@
    2.60    "cdecl c" <= (type) "cname \<times> (c class)"
    2.61    "prog  c" <= (type) "(c cdecl) list"
    2.62  
    2.63 -constdefs
    2.64  
    2.65 -  class		:: "'c prog => (cname \<leadsto> 'c class)"
    2.66 -  "class        \<equiv> map_of"
    2.67 -  is_class	:: "'c prog => cname => bool"
    2.68 - "is_class G C  \<equiv> class G C \<noteq> None"
    2.69 +constdefs
    2.70 +  class :: "'c prog => (cname \<leadsto> 'c class)"
    2.71 +  "class \<equiv> map_of"
    2.72 +
    2.73 +  is_class :: "'c prog => cname => bool"
    2.74 +  "is_class G C \<equiv> class G C \<noteq> None"
    2.75 +
    2.76  
    2.77  lemma finite_is_class: "finite {C. is_class G C}"
    2.78  apply (unfold is_class_def class_def)
    2.79 @@ -60,11 +52,9 @@
    2.80  done
    2.81  
    2.82  consts
    2.83 -
    2.84 -  is_type	:: "'c prog => ty    => bool"
    2.85 -
    2.86 +  is_type :: "'c prog => ty    => bool"
    2.87  primrec
    2.88 -"is_type G (PrimT pt) = True"
    2.89 -"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
    2.90 +  "is_type G (PrimT pt) = True"
    2.91 +  "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
    2.92  
    2.93  end
     3.1 --- a/src/HOL/MicroJava/J/Eval.thy	Sun Dec 16 00:17:44 2001 +0100
     3.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Sun Dec 16 00:18:17 2001 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4      Copyright   1999 Technische Universitaet Muenchen
     3.5  *)
     3.6  
     3.7 -header "Operational Evaluation (big-step) Semantics"
     3.8 +header "Operational Evaluation (big step) Semantics"
     3.9  
    3.10  theory Eval = State + WellType:
    3.11  
    3.12 @@ -40,24 +40,24 @@
    3.13    "G\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \<in> exec G"
    3.14    "G\<turnstile>s -c    ->    s' " == "(s, c,    s') \<in> exec G"
    3.15  
    3.16 +
    3.17  inductive "eval G" "evals G" "exec G" intros
    3.18  
    3.19 -(* evaluation of expressions *)
    3.20 +  (* evaluation of expressions *)
    3.21  
    3.22 -  (* cf. 15.5 *)
    3.23 -  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"
    3.24 +  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"  -- "cf. 15.5"
    3.25  
    3.26 -  (* cf. 15.8.1 *)
    3.27 +  -- "cf. 15.8.1"
    3.28    NewC: "[| h = heap s; (a,x) = new_Addr h;
    3.29              h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
    3.30           G\<turnstile>Norm s -NewC C\<succ>Addr a-> c_hupd h' (x,s)"
    3.31  
    3.32 -  (* cf. 15.15 *)
    3.33 +  -- "cf. 15.15"
    3.34    Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
    3.35              x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
    3.36           G\<turnstile>Norm s0 -Cast C e\<succ>v-> (x2,s1)"
    3.37  
    3.38 -  (* cf. 15.7.1 *)
    3.39 +  -- "cf. 15.7.1"
    3.40    Lit:  "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
    3.41  
    3.42    BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
    3.43 @@ -66,29 +66,27 @@
    3.44                             | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
    3.45           G\<turnstile>Norm s -BinOp bop e1 e2\<succ>v-> s2"
    3.46  
    3.47 -  (* cf. 15.13.1, 15.2 *)
    3.48 +  -- "cf. 15.13.1, 15.2"
    3.49    LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
    3.50  
    3.51 -  (* cf. 15.25.1 *)
    3.52 +  -- "cf. 15.25.1"
    3.53    LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
    3.54              l' = (if x = None then l(va\<mapsto>v) else l) |] ==>
    3.55           G\<turnstile>Norm s -va::=e\<succ>v-> (x,(h,l'))"
    3.56  
    3.57 -
    3.58 -  (* cf. 15.10.1, 15.2 *)
    3.59 +  -- "cf. 15.10.1, 15.2"
    3.60    FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1); 
    3.61              v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
    3.62           G\<turnstile>Norm s0 -{T}e..fn\<succ>v-> (np a' x1,s1)"
    3.63  
    3.64 -  (* cf. 15.25.1 *)
    3.65 +  -- "cf. 15.25.1"
    3.66    FAss: "[| G\<turnstile>     Norm s0  -e1\<succ>a'-> (x1,s1); a = the_Addr a';
    3.67              G\<turnstile>(np a' x1,s1) -e2\<succ>v -> (x2,s2);
    3.68              h  = heap s2; (c,fs) = the (h a);
    3.69              h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
    3.70           G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
    3.71  
    3.72 -
    3.73 -  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
    3.74 +  -- "cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15"
    3.75    Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
    3.76              G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
    3.77              (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
    3.78 @@ -96,48 +94,51 @@
    3.79              G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
    3.80           G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
    3.81  
    3.82 -(* evaluation of expression lists *)
    3.83  
    3.84 -  (* cf. 15.5 *)
    3.85 +  -- "evaluation of expression lists"
    3.86 +
    3.87 +  -- "cf. 15.5"
    3.88    XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
    3.89  
    3.90 -  (* cf. 15.11.??? *)
    3.91 +  -- "cf. 15.11.???"
    3.92    Nil:  "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
    3.93  
    3.94 -  (* cf. 15.6.4 *)
    3.95 +  -- "cf. 15.6.4"
    3.96    Cons: "[| G\<turnstile>Norm s0 -e  \<succ> v -> s1;
    3.97              G\<turnstile>     s1 -es[\<succ>]vs-> s2 |] ==>
    3.98           G\<turnstile>Norm s0 -e#es[\<succ>]v#vs-> s2"
    3.99  
   3.100 -(* execution of statements *)
   3.101  
   3.102 -  (* cf. 14.1 *)
   3.103 +  -- "execution of statements"
   3.104 +
   3.105 +  -- "cf. 14.1"
   3.106    XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
   3.107  
   3.108 -  (* cf. 14.5 *)
   3.109 +  -- "cf. 14.5"
   3.110    Skip: "G\<turnstile>Norm s -Skip-> Norm s"
   3.111  
   3.112 -  (* cf. 14.7 *)
   3.113 +  -- "cf. 14.7"
   3.114    Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
   3.115           G\<turnstile>Norm s0 -Expr e-> s1"
   3.116  
   3.117 -  (* cf. 14.2 *)
   3.118 +  -- "cf. 14.2"
   3.119    Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
   3.120              G\<turnstile>     s1 -c2-> s2|] ==>
   3.121           G\<turnstile>Norm s0 -c1;; c2-> s2"
   3.122  
   3.123 -  (* cf. 14.8.2 *)
   3.124 +  -- "cf. 14.8.2"
   3.125    Cond: "[| G\<turnstile>Norm s0  -e\<succ>v-> s1;
   3.126              G\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
   3.127           G\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
   3.128  
   3.129 -  (* cf. 14.10, 14.10.1 *)
   3.130 +  -- "cf. 14.10, 14.10.1"
   3.131    LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
   3.132           G\<turnstile>Norm s0 -While(e) c-> s1"
   3.133    LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1;  the_Bool v;
   3.134 -	    G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
   3.135 +      G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
   3.136           G\<turnstile>Norm s0 -While(e) c-> s3"
   3.137  
   3.138 +
   3.139  lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)]
   3.140  
   3.141  lemma NewCI: "[|new_Addr (heap s) = (a,x);  
     4.1 --- a/src/HOL/MicroJava/J/Example.thy	Sun Dec 16 00:17:44 2001 +0100
     4.2 +++ b/src/HOL/MicroJava/J/Example.thy	Sun Dec 16 00:18:17 2001 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      isabelle/Bali/Example.thy
     4.5 +(*  Title:      HOL/MicroJava/J/Example.thy
     4.6      ID:         $Id$
     4.7      Author:     David von Oheimb
     4.8      Copyright   1999 Technische Universitaet Muenchen
     4.9 @@ -41,12 +41,12 @@
    4.10  datatype vnam_ = vee_ | x_ | e_
    4.11  
    4.12  consts
    4.13 -
    4.14    cnam_ :: "cnam_ => cname"
    4.15    vnam_ :: "vnam_ => vnam"
    4.16  
    4.17 -axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
    4.18 -
    4.19 +-- "@{text cnam_} and @{text vnam_} are intended to be isomorphic 
    4.20 +    to @{text cnam} and @{text vnam}"
    4.21 +axioms 
    4.22    inj_cnam_:  "(cnam_ x = cnam_ y) = (x = y)"
    4.23    inj_vnam_:  "(vnam_ x = vnam_ y) = (x = y)"
    4.24  
    4.25 @@ -56,7 +56,6 @@
    4.26  declare inj_cnam_ [simp] inj_vnam_ [simp]
    4.27  
    4.28  syntax
    4.29 -
    4.30    Base :: cname
    4.31    Ext  :: cname
    4.32    vee  :: vname
    4.33 @@ -64,15 +63,13 @@
    4.34    e    :: vname
    4.35  
    4.36  translations
    4.37 -
    4.38    "Base" == "cnam_ Base_"
    4.39 -  "Ext"	 == "cnam_ Ext_"
    4.40 +  "Ext"  == "cnam_ Ext_"
    4.41    "vee"  == "VName (vnam_ vee_)"
    4.42 -  "x"	 == "VName (vnam_ x_)"
    4.43 -  "e"	 == "VName (vnam_ e_)"
    4.44 +  "x"  == "VName (vnam_ x_)"
    4.45 +  "e"  == "VName (vnam_ e_)"
    4.46  
    4.47  axioms
    4.48 -
    4.49    Base_not_Object: "Base \<noteq> Object"
    4.50    Ext_not_Object:  "Ext  \<noteq> Object"
    4.51    e_not_This:      "e \<noteq> This"
    4.52 @@ -83,28 +80,26 @@
    4.53  declare Ext_not_Object  [THEN not_sym, simp]
    4.54  
    4.55  consts
    4.56 -
    4.57    foo_Base::  java_mb
    4.58    foo_Ext ::  java_mb
    4.59    BaseC   :: "java_mb cdecl"
    4.60    ExtC    :: "java_mb cdecl"
    4.61 -  test	  ::  stmt
    4.62 -  foo	  ::  mname
    4.63 -  a	  ::  loc
    4.64 +  test    ::  stmt
    4.65 +  foo   ::  mname
    4.66 +  a   ::  loc
    4.67    b       ::  loc
    4.68  
    4.69  defs
    4.70 -
    4.71    foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
    4.72    BaseC_def:"BaseC == (Base, (Object, 
    4.73 -			     [(vee, PrimT Boolean)], 
    4.74 -			     [((foo,[Class Base]),Class Base,foo_Base)]))"
    4.75 +           [(vee, PrimT Boolean)], 
    4.76 +           [((foo,[Class Base]),Class Base,foo_Base)]))"
    4.77    foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    4.78 -				       (LAcc x)..vee:=Lit (Intg 1)),
    4.79 -				   Lit Null)"
    4.80 +               (LAcc x)..vee:=Lit (Intg Numeral1)),
    4.81 +           Lit Null)"
    4.82    ExtC_def: "ExtC  == (Ext,  (Base  , 
    4.83 -			     [(vee, PrimT Integer)], 
    4.84 -			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    4.85 +           [(vee, PrimT Integer)], 
    4.86 +           [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    4.87  
    4.88    test_def:"test == Expr(e::=NewC Ext);; 
    4.89                      Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
    4.90 @@ -112,22 +107,21 @@
    4.91  
    4.92  syntax
    4.93  
    4.94 -  NP	:: xcpt
    4.95 -  tprg 	::"java_mb prog"
    4.96 -  obj1	:: obj
    4.97 -  obj2	:: obj
    4.98 -  s0 	:: state
    4.99 -  s1 	:: state
   4.100 -  s2 	:: state
   4.101 -  s3 	:: state
   4.102 -  s4 	:: state
   4.103 +  NP  :: xcpt
   4.104 +  tprg  ::"java_mb prog"
   4.105 +  obj1  :: obj
   4.106 +  obj2  :: obj
   4.107 +  s0  :: state
   4.108 +  s1  :: state
   4.109 +  s2  :: state
   4.110 +  s3  :: state
   4.111 +  s4  :: state
   4.112  
   4.113  translations
   4.114 -
   4.115    "NP"   == "NullPointer"
   4.116    "tprg" == "[ObjectC, BaseC, ExtC]"
   4.117    "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
   4.118 -			   ((vee, Ext )\<mapsto>Intg 0))"
   4.119 +         ((vee, Ext )\<mapsto>Intg 0))"
   4.120    "s0" == " Norm    (empty, empty)"
   4.121    "s1" == " Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   4.122    "s2" == " Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
   4.123 @@ -141,7 +135,7 @@
   4.124  lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
   4.125  apply (simp (no_asm_simp))
   4.126  done
   4.127 -declare map_of_Cons [simp del]; (* sic! *)
   4.128 +declare map_of_Cons [simp del] -- "sic!"
   4.129  
   4.130  lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
   4.131  apply (unfold ObjectC_def class_def)
   4.132 @@ -150,7 +144,7 @@
   4.133  
   4.134  lemma class_tprg_Base [simp]: 
   4.135  "class tprg Base = Some (Object,  
   4.136 -	  [(vee, PrimT Boolean)],  
   4.137 +    [(vee, PrimT Boolean)],  
   4.138            [((foo, [Class Base]), Class Base, foo_Base)])"
   4.139  apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
   4.140  apply (simp (no_asm))
   4.141 @@ -158,7 +152,7 @@
   4.142  
   4.143  lemma class_tprg_Ext [simp]: 
   4.144  "class tprg Ext = Some (Base,  
   4.145 -	  [(vee, PrimT Integer)],  
   4.146 +    [(vee, PrimT Integer)],  
   4.147            [((foo, [Class Base]), Class Ext, foo_Ext)])"
   4.148  apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
   4.149  apply (simp (no_asm))
   4.150 @@ -328,25 +322,25 @@
   4.151  ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
   4.152  lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
   4.153    Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
   4.154 -apply (tactic t) (* ;; *)
   4.155 -apply  (tactic t) (* Expr *)
   4.156 -apply  (tactic t) (* LAss *)
   4.157 -apply    simp (* e \<noteq> This *)
   4.158 -apply    (tactic t) (* LAcc *)
   4.159 +apply (tactic t) -- ";;"
   4.160 +apply  (tactic t) -- "Expr"
   4.161 +apply  (tactic t) -- "LAss"
   4.162 +apply    simp -- {* @{text "e \<noteq> This"} *}
   4.163 +apply    (tactic t) -- "LAcc"
   4.164  apply     (simp (no_asm))
   4.165  apply    (simp (no_asm))
   4.166 -apply   (tactic t) (* NewC *)
   4.167 +apply   (tactic t) -- "NewC"
   4.168  apply   (simp (no_asm))
   4.169  apply  (simp (no_asm))
   4.170 -apply (tactic t) (* Expr *)
   4.171 -apply (tactic t) (* Call *)
   4.172 -apply   (tactic t) (* LAcc *)
   4.173 +apply (tactic t) -- "Expr"
   4.174 +apply (tactic t) -- "Call"
   4.175 +apply   (tactic t) -- "LAcc"
   4.176  apply    (simp (no_asm))
   4.177  apply   (simp (no_asm))
   4.178 -apply  (tactic t) (* Cons *)
   4.179 -apply   (tactic t) (* Lit *)
   4.180 +apply  (tactic t) -- "Cons"
   4.181 +apply   (tactic t) -- "Lit"
   4.182  apply   (simp (no_asm))
   4.183 -apply  (tactic t) (* Nil *)
   4.184 +apply  (tactic t) -- "Nil"
   4.185  apply (simp (no_asm))
   4.186  apply (rule max_spec_foo_Base)
   4.187  done
   4.188 @@ -359,38 +353,38 @@
   4.189  " [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
   4.190    tprg\<turnstile>s0 -test-> ?s"
   4.191  apply (unfold test_def)
   4.192 -(* ?s = s3 *)
   4.193 -apply (tactic e) (* ;; *)
   4.194 -apply  (tactic e) (* Expr *)
   4.195 -apply  (tactic e) (* LAss *)
   4.196 -apply   (tactic e) (* NewC *)
   4.197 +-- "?s = s3 "
   4.198 +apply (tactic e) -- ";;"
   4.199 +apply  (tactic e) -- "Expr"
   4.200 +apply  (tactic e) -- "LAss"
   4.201 +apply   (tactic e) -- "NewC"
   4.202  apply    force
   4.203  apply   force
   4.204  apply  (simp (no_asm))
   4.205  apply (erule thin_rl)
   4.206 -apply (tactic e) (* Expr *)
   4.207 -apply (tactic e) (* Call *)
   4.208 -apply       (tactic e) (* LAcc *)
   4.209 +apply (tactic e) -- "Expr"
   4.210 +apply (tactic e) -- "Call"
   4.211 +apply       (tactic e) -- "LAcc"
   4.212  apply      force
   4.213 -apply     (tactic e) (* Cons *)
   4.214 -apply      (tactic e) (* Lit *)
   4.215 -apply     (tactic e) (* Nil *)
   4.216 +apply     (tactic e) -- "Cons"
   4.217 +apply      (tactic e) -- "Lit"
   4.218 +apply     (tactic e) -- "Nil"
   4.219  apply    (simp (no_asm))
   4.220  apply   (force simp add: foo_Ext_def)
   4.221  apply  (simp (no_asm))
   4.222 -apply  (tactic e) (* Expr *)
   4.223 -apply  (tactic e) (* FAss *)
   4.224 -apply       (tactic e) (* Cast *)
   4.225 -apply        (tactic e) (* LAcc *)
   4.226 +apply  (tactic e) -- "Expr"
   4.227 +apply  (tactic e) -- "FAss"
   4.228 +apply       (tactic e) -- "Cast"
   4.229 +apply        (tactic e) -- "LAcc"
   4.230  apply       (simp (no_asm))
   4.231  apply      (simp (no_asm))
   4.232  apply     (simp (no_asm))
   4.233 -apply     (tactic e) (* XcptE *)
   4.234 +apply     (tactic e) -- "XcptE"
   4.235  apply    (simp (no_asm))
   4.236  apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
   4.237  apply  (simp (no_asm))
   4.238  apply (simp (no_asm))
   4.239 -apply (tactic e) (* XcptE *)
   4.240 +apply (tactic e) -- "XcptE"
   4.241  done
   4.242  
   4.243  end
     5.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Sun Dec 16 00:17:44 2001 +0100
     5.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Sun Dec 16 00:18:17 2001 +0100
     5.3 @@ -13,9 +13,8 @@
     5.4  section "unique"
     5.5   
     5.6  constdefs
     5.7 -
     5.8    unique  :: "('a \<times> 'b) list => bool"
     5.9 - "unique  == nodups \<circ> map fst"
    5.10 +  "unique  == nodups \<circ> map fst"
    5.11  
    5.12  
    5.13  lemma fst_in_set_lemma [rule_format (no_asm)]: 
    5.14 @@ -71,4 +70,3 @@
    5.15  done
    5.16  
    5.17  end
    5.18 -
     6.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Dec 16 00:17:44 2001 +0100
     6.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Dec 16 00:18:17 2001 +0100
     6.3 @@ -161,7 +161,7 @@
     6.4  declare fun_upd_same [simp]
     6.5  ML{*
     6.6  val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
     6.7 -	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
     6.8 +  (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
     6.9  *}
    6.10  ML{*
    6.11  Unify.search_bound := 40;
    6.12 @@ -181,15 +181,16 @@
    6.13  apply( rule eval_evals_exec_induct)
    6.14  apply( unfold c_hupd_def)
    6.15  
    6.16 -(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
    6.17 +-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
    6.18  apply( simp_all)
    6.19  apply( tactic "ALLGOALS strip_tac")
    6.20 -apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
    6.21 -apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
    6.22 +apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
    6.23 +                 THEN_ALL_NEW Full_simp_tac) *})
    6.24 +apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
    6.25  
    6.26 -(* Level 7 *)
    6.27 +-- "Level 7"
    6.28  
    6.29 -(* 15 NewC *)
    6.30 +-- "15 NewC"
    6.31  apply( drule new_AddrD)
    6.32  apply( erule disjE)
    6.33  prefer 2
    6.34 @@ -201,13 +202,13 @@
    6.35  apply(  rule_tac [2] rtrancl_refl)
    6.36  apply( simp (no_asm))
    6.37  
    6.38 -(* for Cast *)
    6.39 +-- "for Cast"
    6.40  defer 1
    6.41  
    6.42 -(* 14 Lit *)
    6.43 +-- "14 Lit"
    6.44  apply( erule conf_litval)
    6.45  
    6.46 -(* 13 BinOp *)
    6.47 +-- "13 BinOp"
    6.48  apply (tactic "forward_hyp_tac")
    6.49  apply (tactic "forward_hyp_tac")
    6.50  apply( rule conjI, erule (1) hext_trans)
    6.51 @@ -216,46 +217,48 @@
    6.52  apply( drule eval_no_xcpt)
    6.53  apply( simp split add: binop.split)
    6.54  
    6.55 -(* 12 LAcc *)
    6.56 +-- "12 LAcc"
    6.57  apply( fast elim: conforms_localD [THEN lconfD])
    6.58  
    6.59 -(* for FAss *)
    6.60 -apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
    6.61 +-- "for FAss"
    6.62 +apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
    6.63 +       THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
    6.64  
    6.65 -(* for if *)
    6.66 +-- "for if"
    6.67  apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
    6.68  
    6.69  apply (tactic "forward_hyp_tac")
    6.70  
    6.71 -(* 11+1 if *)
    6.72 +-- "11+1 if"
    6.73  prefer 8
    6.74  apply(  fast intro: hext_trans)
    6.75  prefer 8
    6.76  apply(  fast intro: hext_trans)
    6.77  
    6.78 -(* 10 Expr *)
    6.79 +-- "10 Expr"
    6.80  prefer 6
    6.81  apply( fast)
    6.82  
    6.83 -(* 9 ??? *)
    6.84 +-- "9 ???"
    6.85  apply( simp_all)
    6.86  
    6.87 -(* 8 Cast *)
    6.88 +-- "8 Cast"
    6.89  prefer 8
    6.90  apply (rule impI)
    6.91  apply (drule raise_if_NoneD)
    6.92  apply (clarsimp)
    6.93  apply (fast elim: Cast_conf)
    6.94  
    6.95 -(* 7 LAss *)
    6.96 +-- "7 LAss"
    6.97  apply (fold fun_upd_def)
    6.98 -apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) 1 *})
    6.99 +apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
   6.100 +                 THEN_ALL_NEW Full_simp_tac) 1 *})
   6.101  apply( blast intro: conforms_upd_local conf_widen)
   6.102  
   6.103 -(* 6 FAcc *)
   6.104 +-- "6 FAcc"
   6.105  apply( fast elim!: FAcc_type_sound)
   6.106  
   6.107 -(* 5 While *)
   6.108 +-- "5 While"
   6.109  prefer 5
   6.110  apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
   6.111  apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
   6.112 @@ -263,15 +266,15 @@
   6.113  
   6.114  apply (tactic "forward_hyp_tac")
   6.115  
   6.116 -(* 4 Cons *)
   6.117 +-- "4 Cons"
   6.118  prefer 3
   6.119  apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
   6.120  
   6.121 -(* 3 ;; *)
   6.122 +-- "3 ;;"
   6.123  prefer 3
   6.124  apply( fast intro: hext_trans)
   6.125  
   6.126 -(* 2 FAss *)
   6.127 +-- "2 FAss"
   6.128  apply( case_tac "x2 = None")
   6.129  prefer 2
   6.130  apply(  simp (no_asm_simp))
   6.131 @@ -281,9 +284,9 @@
   6.132  apply( erule FAss_type_sound, rule HOL.refl, assumption+)
   6.133  
   6.134  apply( tactic prune_params_tac)
   6.135 -(* Level 52 *)
   6.136 +-- "Level 52"
   6.137  
   6.138 -(* 1 Call *)
   6.139 +-- "1 Call"
   6.140  apply( case_tac "x")
   6.141  prefer 2
   6.142  apply(  clarsimp)
     7.1 --- a/src/HOL/MicroJava/J/State.thy	Sun Dec 16 00:17:44 2001 +0100
     7.2 +++ b/src/HOL/MicroJava/J/State.thy	Sun Dec 16 00:18:17 2001 +0100
     7.3 @@ -8,58 +8,57 @@
     7.4  
     7.5  theory State = TypeRel + Value:
     7.6  
     7.7 -types	fields_
     7.8 -	= "(vname \<times> cname \<leadsto> val)" (* field name, defining class, value *)
     7.9 +types 
    7.10 +  fields_ = "(vname \<times> cname \<leadsto> val)"  -- "field name, defining class, value"
    7.11  
    7.12 -        obj = "cname \<times> fields_"	(* class instance with class name and fields *)
    7.13 +  obj = "cname \<times> fields_"    -- "class instance with class name and fields"
    7.14  
    7.15  constdefs
    7.16 -  obj_ty	:: "obj => ty"
    7.17 +  obj_ty  :: "obj => ty"
    7.18   "obj_ty obj  == Class (fst obj)"
    7.19  
    7.20 -  init_vars	:: "('a \<times> ty) list => ('a \<leadsto> val)"
    7.21 - "init_vars	== map_of o map (\<lambda>(n,T). (n,default_val T))"
    7.22 +  init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
    7.23 + "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
    7.24    
    7.25 -datatype xcpt		(* exceptions *)
    7.26 -	= NullPointer
    7.27 -	| ClassCast
    7.28 -	| OutOfMemory
    7.29 +
    7.30 +types aheap  = "loc \<leadsto> obj"    -- {* "@{text heap}" used in a translation below *}
    7.31 +      locals = "vname \<leadsto> val"  -- "simple state, i.e. variable contents"
    7.32  
    7.33 -types	aheap  = "loc \<leadsto> obj" (** "heap" used in a translation below **)
    7.34 -        locals = "vname \<leadsto> val"	
    7.35 +      state  = "aheap \<times> locals"      -- "heap, local parameter including This"
    7.36 +      xstate = "xcpt option \<times> state" -- "state including exception information"
    7.37 +
    7.38  
    7.39 -        state		(* simple state, i.e. variable contents *)
    7.40 -	= "aheap \<times> locals"
    7.41 -	(* heap, local parameter including This *)
    7.42 +text {*
    7.43 +  System exceptions are allocated in all heaps, 
    7.44 +  and they don't carry any information other than their type: *}
    7.45 +axioms
    7.46 +  system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)"
    7.47  
    7.48 -	xstate		(* state including exception information *)
    7.49 -	 = "xcpt option \<times> state"
    7.50  
    7.51  syntax
    7.52 -  heap		:: "state => aheap"
    7.53 -  locals	:: "state => locals"
    7.54 -  Norm		:: "state => xstate"
    7.55 +  heap    :: "state => aheap"
    7.56 +  locals  :: "state => locals"
    7.57 +  Norm    :: "state => xstate"
    7.58  
    7.59  translations
    7.60    "heap"   => "fst"
    7.61    "locals" => "snd"
    7.62 -  "Norm s" == "(None,s)"  
    7.63 +  "Norm s" == "(None,s)"
    7.64  
    7.65  constdefs
    7.66 -
    7.67 -  new_Addr	:: "aheap => loc \<times> xcpt option"
    7.68 +  new_Addr  :: "aheap => loc \<times> xcpt option"
    7.69   "new_Addr h == SOME (a,x). (h a = None \<and>  x = None) |  x = Some OutOfMemory"
    7.70  
    7.71 -  raise_if	:: "bool => xcpt => xcpt option => xcpt option"
    7.72 +  raise_if  :: "bool => xcpt => xcpt option => xcpt option"
    7.73   "raise_if c x xo == if c \<and>  (xo = None) then Some x else xo"
    7.74  
    7.75 -  np		:: "val => xcpt option => xcpt option"
    7.76 +  np    :: "val => xcpt option => xcpt option"
    7.77   "np v == raise_if (v = Null) NullPointer"
    7.78  
    7.79 -  c_hupd	:: "aheap => xstate => xstate"
    7.80 +  c_hupd  :: "aheap => xstate => xstate"
    7.81   "c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
    7.82  
    7.83 -  cast_ok	:: "'c prog => cname => aheap => val => bool"
    7.84 +  cast_ok :: "'c prog => cname => aheap => val => bool"
    7.85   "cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
    7.86  
    7.87  lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
    7.88 @@ -93,7 +92,8 @@
    7.89  apply auto
    7.90  done
    7.91  
    7.92 -lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \<noteq> None"
    7.93 +lemma raise_if_Some2 [simp]: 
    7.94 +  "raise_if c z (if x = None then Some y else x) \<noteq> None"
    7.95  apply (unfold raise_if_def)
    7.96  apply(induct_tac "x")
    7.97  apply auto
    7.98 @@ -105,12 +105,14 @@
    7.99  apply auto
   7.100  done
   7.101  
   7.102 -lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \<not> c \<and>  y = None"
   7.103 +lemma raise_if_NoneD [rule_format (no_asm)]: 
   7.104 +  "raise_if c x y = None --> \<not> c \<and>  y = None"
   7.105  apply (unfold raise_if_def)
   7.106  apply auto
   7.107  done
   7.108  
   7.109 -lemma np_NoneD [rule_format (no_asm)]: "np a' x' = None --> x' = None \<and>  a' \<noteq> Null"
   7.110 +lemma np_NoneD [rule_format (no_asm)]: 
   7.111 +  "np a' x' = None --> x' = None \<and>  a' \<noteq> Null"
   7.112  apply (unfold np_def raise_if_def)
   7.113  apply auto
   7.114  done
     8.1 --- a/src/HOL/MicroJava/J/Term.thy	Sun Dec 16 00:17:44 2001 +0100
     8.2 +++ b/src/HOL/MicroJava/J/Term.thy	Sun Dec 16 00:18:17 2001 +0100
     8.3 @@ -8,25 +8,24 @@
     8.4  
     8.5  theory Term = Value:
     8.6  
     8.7 -datatype binop = Eq | Add    (* function codes for binary operation *)
     8.8 +datatype binop = Eq | Add    -- "function codes for binary operation"
     8.9  
    8.10  datatype expr
    8.11 -  = NewC cname               (* class instance creation *)
    8.12 -  | Cast cname expr          (* type cast *)
    8.13 -  | Lit val                  (* literal value, also references *)
    8.14 -  | BinOp binop expr expr    (* binary operation *)
    8.15 -  | LAcc vname               (* local (incl. parameter) access *)
    8.16 -  | LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
    8.17 -  | FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
    8.18 +  = NewC cname               -- "class instance creation"
    8.19 +  | Cast cname expr          -- "type cast"
    8.20 +  | Lit val                  -- "literal value, also references"
    8.21 +  | BinOp binop expr expr    -- "binary operation"
    8.22 +  | LAcc vname               -- "local (incl. parameter) access"
    8.23 +  | LAss vname expr          ("_::=_" [90,90]90)      -- "local assign"
    8.24 +  | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) -- "field access"
    8.25    | FAss cname expr vname 
    8.26 -                    expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
    8.27 +                    expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
    8.28    | Call cname expr mname 
    8.29 -    "ty list" "expr list"    (* method call*) ("{_}_.._'( {_}_')"
    8.30 -                                                            [10,90,99,10,10] 90)
    8.31 +    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
    8.32  
    8.33  datatype stmt
    8.34 -  = Skip                     (* empty statement *)
    8.35 -  | Expr expr                (* expression statement *)
    8.36 +  = Skip                     -- "empty statement"
    8.37 +  | Expr expr                -- "expression statement"
    8.38    | Comp stmt stmt       ("_;; _"             [61,60]60)
    8.39    | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    8.40    | Loop expr stmt       ("While '(_') _"     [80,79]70)
     9.1 --- a/src/HOL/MicroJava/J/Type.thy	Sun Dec 16 00:17:44 2001 +0100
     9.2 +++ b/src/HOL/MicroJava/J/Type.thy	Sun Dec 16 00:18:17 2001 +0100
     9.3 @@ -8,29 +8,47 @@
     9.4  
     9.5  theory Type = JBasis:
     9.6  
     9.7 -typedecl cname  (* class name *)
     9.8 -typedecl vnam   (* variable or field name *)
     9.9 -typedecl mname  (* method name *)
    9.10 +typedecl cnam 
    9.11 +
    9.12 + -- "exceptions"
    9.13 +datatype 
    9.14 +  xcpt   
    9.15 +  = NullPointer
    9.16 +  | ClassCast
    9.17 +  | OutOfMemory
    9.18  
    9.19 -datatype vname    (* names for This pointer and local/field variables *)
    9.20 +-- "class names"
    9.21 +datatype cname  
    9.22 +  = Object 
    9.23 +  | Xcpt xcpt 
    9.24 +  | Cname cname 
    9.25 +
    9.26 +typedecl vnam   -- "variable or field name"
    9.27 +typedecl mname  -- "method name"
    9.28 +
    9.29 +-- "names for @{text This} pointer and local/field variables"
    9.30 +datatype vname 
    9.31    = This
    9.32    | VName vnam
    9.33  
    9.34 -datatype prim_ty  (* primitive type, cf. 4.2 *)
    9.35 -  = Void          (* 'result type' of void methods *)
    9.36 +-- "primitive type, cf. 4.2"
    9.37 +datatype prim_ty 
    9.38 +  = Void          -- "'result type' of void methods"
    9.39    | Boolean
    9.40    | Integer
    9.41  
    9.42 -datatype ref_ty   (* reference type, cf. 4.3 *)
    9.43 -  = NullT         (* null type, cf. 4.1 *)
    9.44 -  | ClassT cname  (* class type *)
    9.45 +-- "reference type, cf. 4.3"
    9.46 +datatype ref_ty   
    9.47 +  = NullT         -- "null type, cf. 4.1"
    9.48 +  | ClassT cname  -- "class type"
    9.49  
    9.50 -datatype ty       (* any type, cf. 4.1 *)
    9.51 -  = PrimT prim_ty (* primitive type *)
    9.52 -  | RefT  ref_ty  (* reference type *)
    9.53 +-- "any type, cf. 4.1"
    9.54 +datatype ty 
    9.55 +  = PrimT prim_ty -- "primitive type"
    9.56 +  | RefT  ref_ty  -- "reference type"
    9.57  
    9.58  syntax
    9.59 -  NT    :: "          ty"
    9.60 +  NT    :: "ty"
    9.61    Class :: "cname  => ty"
    9.62  
    9.63  translations
    10.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Sun Dec 16 00:17:44 2001 +0100
    10.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Sun Dec 16 00:18:17 2001 +0100
    10.3 @@ -9,9 +9,9 @@
    10.4  theory TypeRel = Decl:
    10.5  
    10.6  consts
    10.7 -  subcls1 :: "'c prog => (cname \<times> cname) set"  (* subclass *)
    10.8 -  widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
    10.9 -  cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
   10.10 +  subcls1 :: "'c prog => (cname \<times> cname) set"  -- "subclass"
   10.11 +  widen   :: "'c prog => (ty    \<times> ty   ) set"  -- "widening"
   10.12 +  cast    :: "'c prog => (cname \<times> cname) set"  -- "casting"
   10.13  
   10.14  syntax (xsymbols)
   10.15    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
   10.16 @@ -31,9 +31,8 @@
   10.17    "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
   10.18    "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
   10.19  
   10.20 +-- "direct subclass, cf. 8.1.3"
   10.21  inductive "subcls1 G" intros
   10.22 -
   10.23 -  (* direct subclass, cf. 8.1.3 *)
   10.24    subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
   10.25    
   10.26  lemma subcls1D: 
   10.27 @@ -91,7 +90,7 @@
   10.28    field  :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty     )" (* ###curry *)
   10.29    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
   10.30  
   10.31 -(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
   10.32 +-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
   10.33  defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
   10.34                             ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   10.35  
   10.36 @@ -105,7 +104,7 @@
   10.37  done
   10.38  
   10.39  
   10.40 -(* list of fields of a class, including inherited and hidden ones *)
   10.41 +-- "list of fields of a class, including inherited and hidden ones"
   10.42  defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) []    (\<lambda>C fs ms ts.
   10.43                             map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   10.44  
   10.45 @@ -129,14 +128,15 @@
   10.46  done
   10.47  
   10.48  
   10.49 -inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3
   10.50 -			     i.e. sort of syntactic subtyping *)
   10.51 -  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
   10.52 +-- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
   10.53 +inductive "widen G" intros 
   10.54 +  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
   10.55    subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
   10.56    null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
   10.57  
   10.58 -inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *)
   10.59 -                          (* left out casts on primitve types    *)
   10.60 +-- "casting conversion, cf. 5.5 / 5.1.5"
   10.61 +-- "left out casts on primitve types"
   10.62 +inductive "cast G" intros
   10.63    widen:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
   10.64    subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
   10.65  
   10.66 @@ -173,45 +173,11 @@
   10.67  apply (auto elim: widen.subcls)
   10.68  done
   10.69  
   10.70 -lemma widen_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
   10.71 -apply (erule widen.induct)
   10.72 -apply   safe
   10.73 -apply  (frule widen_Class)
   10.74 -apply  (frule_tac [2] widen_RefT)
   10.75 -apply  safe
   10.76 -apply(erule (1) rtrancl_trans)
   10.77 -done
   10.78 -
   10.79 -
   10.80 -(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   10.81 +theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   10.82  proof -
   10.83 -  assume "G\<turnstile>S\<preceq>U"
   10.84 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
   10.85 -  proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
   10.86 -    case refl
   10.87 -    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
   10.88 -      ( * fix T' show "PROP ?P T T".* )
   10.89 -  next
   10.90 -    case subcls
   10.91 -    fix T assume "G\<turnstile>Class D\<preceq>T"
   10.92 -    then obtain E where "T = Class E" by (blast dest: widen_Class)
   10.93 -    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
   10.94 -  next
   10.95 -    case null
   10.96 -    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
   10.97 -    then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
   10.98 -    thus "G\<turnstile>NT\<preceq>RT" by auto
   10.99 -  qed
  10.100 -qed
  10.101 -*)
  10.102 -
  10.103 -theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
  10.104 -proof -
  10.105 -  assume "G\<turnstile>S\<preceq>U"
  10.106 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
  10.107 +  assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
  10.108    proof induct
  10.109 -    case (refl T T')
  10.110 -    thus "G\<turnstile>T\<preceq>T'" .
  10.111 +    case (refl T T') thus "G\<turnstile>T\<preceq>T'" .
  10.112    next
  10.113      case (subcls C D T)
  10.114      then obtain E where "T = Class E" by (blast dest: widen_Class)
    11.1 --- a/src/HOL/MicroJava/J/Value.thy	Sun Dec 16 00:17:44 2001 +0100
    11.2 +++ b/src/HOL/MicroJava/J/Value.thy	Sun Dec 16 00:18:17 2001 +0100
    11.3 @@ -8,15 +8,19 @@
    11.4  
    11.5  theory Value = Type:
    11.6  
    11.7 -typedecl loc (* locations, i.e. abstract references on objects *)
    11.8 +typedecl loc_ -- "locations, i.e. abstract references on objects" 
    11.9 +
   11.10 +datatype loc 
   11.11 +  = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
   11.12 +  | Loc loc_     -- "usual locations (references on objects)"
   11.13  
   11.14  datatype val
   11.15 -  = Unit        (* dummy result value of void methods *)
   11.16 -  | Null        (* null reference *)
   11.17 -  | Bool bool   (* Boolean value *)
   11.18 -  | Intg int    (* integer value, name Intg instead of Int because
   11.19 -                   of clash with HOL/Set.thy *)
   11.20 -  | Addr loc    (* addresses, i.e. locations of objects *)
   11.21 +  = Unit        -- "dummy result value of void methods"
   11.22 +  | Null        -- "null reference"
   11.23 +  | Bool bool   -- "Boolean value"
   11.24 +  | Intg int    -- "integer value, name Intg instead of Int because
   11.25 +                   of clash with HOL/Set.thy" 
   11.26 +  | Addr loc    -- "addresses, i.e. locations of objects "
   11.27  
   11.28  consts
   11.29    the_Bool :: "val => bool"
   11.30 @@ -33,8 +37,8 @@
   11.31    "the_Addr (Addr a) = a"
   11.32  
   11.33  consts
   11.34 -  defpval :: "prim_ty => val"  (* default value for primitive types *)
   11.35 -  default_val :: "ty => val"   (* default value for all types *)
   11.36 +  defpval :: "prim_ty => val"  -- "default value for primitive types"
   11.37 +  default_val :: "ty => val"   -- "default value for all types"
   11.38  
   11.39  primrec
   11.40    "defpval Void    = Unit"
    12.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Sun Dec 16 00:17:44 2001 +0100
    12.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Sun Dec 16 00:18:17 2001 +0100
    12.3 @@ -57,7 +57,7 @@
    12.4  done
    12.5  
    12.6  lemma class_Object [simp]: 
    12.7 -	"wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
    12.8 +  "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
    12.9  apply (unfold wf_prog_def ObjectC_def class_def)
   12.10  apply (auto intro: map_of_SomeI)
   12.11  done
   12.12 @@ -205,13 +205,15 @@
   12.13  apply auto
   12.14  done
   12.15  
   12.16 -lemma widen_fields_defpl: "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
   12.17 +lemma widen_fields_defpl: 
   12.18 +  "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
   12.19    G\<turnstile>C\<preceq>C fd"
   12.20  apply( drule (1) widen_fields_defpl')
   12.21  apply (fast)
   12.22  done
   12.23  
   12.24 -lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
   12.25 +lemma unique_fields: 
   12.26 +  "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
   12.27  apply( erule subcls1_induct)
   12.28  apply(   assumption)
   12.29  apply(  safe dest!: wf_cdecl_supD)
   12.30 @@ -232,7 +234,8 @@
   12.31  apply(auto dest!: widen_fields_defpl)
   12.32  done
   12.33  
   12.34 -lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
   12.35 +lemma fields_mono_lemma [rule_format (no_asm)]: 
   12.36 +  "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
   12.37    x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
   12.38  apply(erule converse_rtrancl_induct)
   12.39  apply( safe dest!: subcls1D)
   12.40 @@ -260,7 +263,8 @@
   12.41  apply (fast dest: fields_mono)
   12.42  done
   12.43  
   12.44 -lemma method_wf_mdecl [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
   12.45 +lemma method_wf_mdecl [rule_format (no_asm)]: 
   12.46 +  "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
   12.47       method (G,C) sig = Some (md,mh,m) 
   12.48     --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
   12.49  apply( erule subcls1_induct)
   12.50 @@ -322,10 +326,13 @@
   12.51   "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;  
   12.52       method (G,D) sig = Some (md, rT, b) |]  
   12.53    ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
   12.54 -apply(auto dest: subcls_widen_methd method_wf_mdecl simp add: wf_mdecl_def wf_mhead_def split_def)
   12.55 +apply(auto dest: subcls_widen_methd method_wf_mdecl 
   12.56 +           simp add: wf_mdecl_def wf_mhead_def split_def)
   12.57  done
   12.58  
   12.59 -lemma method_in_md [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
   12.60 +lemma method_in_md [rule_format (no_asm)]: 
   12.61 +  "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
   12.62 +  --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
   12.63  apply (erule (1) subcls1_induct)
   12.64   apply (simp)
   12.65  apply (erule conjE)
   12.66 @@ -366,7 +373,8 @@
   12.67  done
   12.68  
   12.69  
   12.70 -lemma fields_is_type_lemma [rule_format (no_asm)]: "[|is_class G C; wf_prog wf_mb G|] ==>  
   12.71 +lemma fields_is_type_lemma [rule_format (no_asm)]: 
   12.72 +  "[|is_class G C; wf_prog wf_mb G|] ==>  
   12.73    \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
   12.74  apply( erule (1) subcls1_induct)
   12.75  apply(  simp (no_asm_simp))
   12.76 @@ -385,7 +393,8 @@
   12.77  apply auto
   12.78  done
   12.79  
   12.80 -lemma fields_is_type: "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
   12.81 +lemma fields_is_type: 
   12.82 +  "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
   12.83    is_type G f"
   12.84  apply(drule map_of_SomeD)
   12.85  apply(drule (2) fields_is_type_lemma)
   12.86 @@ -401,31 +410,19 @@
   12.87  
   12.88    assume m: "(sig,rT,code) \<in> set mdecls"
   12.89    moreover
   12.90 -  from wf
   12.91 -  have "class G Object = Some (arbitrary, [], [])"
   12.92 -    by simp 
   12.93 +  from wf have "class G Object = Some (arbitrary, [], [])" by simp 
   12.94    moreover
   12.95 -  from wf C
   12.96 -  have c: "class G C = Some (S,fs,mdecls)"
   12.97 +  from wf C have c: "class G C = Some (S,fs,mdecls)"
   12.98      by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
   12.99    ultimately
  12.100 -  have O: "C \<noteq> Object"
  12.101 -    by auto
  12.102 -      
  12.103 -  from wf C
  12.104 -  have "unique mdecls"
  12.105 -    by (unfold wf_prog_def wf_cdecl_def) auto
  12.106 +  have O: "C \<noteq> Object" by auto      
  12.107  
  12.108 -  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
  12.109 -    by - (induct mdecls, auto)
  12.110 -
  12.111 -  with m
  12.112 -  have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
  12.113 +  from wf C have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
  12.114 +  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)
  12.115 +  with m have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
  12.116      by (force intro: map_of_SomeI)
  12.117 -
  12.118    with wf C m c O
  12.119 -  show ?thesis
  12.120 -    by (auto simp add: is_class_def dest: method_rec)
  12.121 +  show ?thesis by (auto simp add: is_class_def dest: method_rec)
  12.122  qed
  12.123  
  12.124  end
    13.1 --- a/src/HOL/MicroJava/J/WellType.thy	Sun Dec 16 00:17:44 2001 +0100
    13.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Sun Dec 16 00:18:17 2001 +0100
    13.3 @@ -21,16 +21,17 @@
    13.4  \end{itemize}
    13.5  \end{description}
    13.6  *}
    13.7 -types	lenv (* local variables, including method parameters and This *)
    13.8 -	= "vname \<leadsto> ty"
    13.9 -        'c env
   13.10 -	= "'c prog \<times> lenv"
   13.11 +
   13.12 +text "local variables, including method parameters and This:"
   13.13 +types 
   13.14 +  lenv   = "vname \<leadsto> ty"
   13.15 +  'c env = "'c prog \<times> lenv"
   13.16  
   13.17  syntax
   13.18    prg    :: "'c env => 'c prog"
   13.19    localT :: "'c env => (vname \<leadsto> ty)"
   13.20  
   13.21 -translations	
   13.22 +translations  
   13.23    "prg"    => "fst"
   13.24    "localT" => "snd"
   13.25  
   13.26 @@ -42,15 +43,15 @@
   13.27  
   13.28  defs
   13.29    more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
   13.30 -		                            list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
   13.31 +                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
   13.32    
   13.33 -  (* applicable methods, cf. 15.11.2.1 *)
   13.34 +  -- "applicable methods, cf. 15.11.2.1"
   13.35    appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
   13.36 -		                 {((Class md,rT),pTs') |md rT mb pTs'.
   13.37 -		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
   13.38 -		                  list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
   13.39 +                     {((Class md,rT),pTs') |md rT mb pTs'.
   13.40 +                      method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
   13.41 +                      list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
   13.42  
   13.43 -  (* maximally specific methods, cf. 15.11.2.2 *)
   13.44 +  -- "maximally specific methods, cf. 15.11.2.2"
   13.45    max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
   13.46                                         (\<forall>m'\<in>appl_methds G C sig.
   13.47                                           more_spec G m' m --> m' = m)}"
   13.48 @@ -77,13 +78,14 @@
   13.49    typeof :: "(loc => ty option) => val => ty option"
   13.50  
   13.51  primrec
   13.52 -	"typeof dt  Unit    = Some (PrimT Void)"
   13.53 -	"typeof dt  Null    = Some NT"
   13.54 -	"typeof dt (Bool b) = Some (PrimT Boolean)"
   13.55 -	"typeof dt (Intg i) = Some (PrimT Integer)"
   13.56 -	"typeof dt (Addr a) = dt a"
   13.57 +  "typeof dt  Unit    = Some (PrimT Void)"
   13.58 +  "typeof dt  Null    = Some NT"
   13.59 +  "typeof dt (Bool b) = Some (PrimT Boolean)"
   13.60 +  "typeof dt (Intg i) = Some (PrimT Integer)"
   13.61 +  "typeof dt (Addr a) = dt a"
   13.62  
   13.63 -lemma is_type_typeof [rule_format (no_asm), simp]: "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
   13.64 +lemma is_type_typeof [rule_format (no_asm), simp]: 
   13.65 +  "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
   13.66  apply (rule val.induct)
   13.67  apply     auto
   13.68  done
   13.69 @@ -95,9 +97,9 @@
   13.70  done
   13.71  
   13.72  types
   13.73 -	java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
   13.74 -(* method body with parameter names, local variables, block, result expression.
   13.75 -   local variables might include This, which is hidden anyway *)
   13.76 +  java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
   13.77 +-- "method body with parameter names, local variables, block, result expression."
   13.78 +-- "local variables might include This, which is hidden anyway"
   13.79  
   13.80  consts
   13.81    ty_expr :: "java_mb env => (expr      \<times> ty     ) set"
   13.82 @@ -116,30 +118,27 @@
   13.83  
   13.84  
   13.85  translations
   13.86 -	"E\<turnstile>e :: T" == "(e,T) \<in> ty_expr  E"
   13.87 -	"E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
   13.88 -	"E\<turnstile>c \<surd>"    == "c     \<in> wt_stmt  E"
   13.89 +  "E\<turnstile>e :: T" == "(e,T) \<in> ty_expr  E"
   13.90 +  "E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
   13.91 +  "E\<turnstile>c \<surd>"    == "c     \<in> wt_stmt  E"
   13.92    
   13.93  inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
   13.94 -
   13.95 -(* well-typed expressions *)
   13.96 +  
   13.97 +  NewC: "[| is_class (prg E) C |] ==>
   13.98 +         E\<turnstile>NewC C::Class C"  -- "cf. 15.8"
   13.99  
  13.100 -  (* cf. 15.8 *)
  13.101 -  NewC:	"[| is_class (prg E) C |] ==>
  13.102 -         E\<turnstile>NewC C::Class C"
  13.103 -
  13.104 -  (* cf. 15.15 *)
  13.105 -  Cast:	"[| E\<turnstile>e::Class C; is_class (prg E) D;
  13.106 +  -- "cf. 15.15"
  13.107 +  Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
  13.108              prg E\<turnstile>C\<preceq>? D |] ==>
  13.109           E\<turnstile>Cast D e::Class D"
  13.110  
  13.111 -  (* cf. 15.7.1 *)
  13.112 -  Lit:	  "[| typeof (\<lambda>v. None) x = Some T |] ==>
  13.113 +  -- "cf. 15.7.1"
  13.114 +  Lit:    "[| typeof (\<lambda>v. None) x = Some T |] ==>
  13.115           E\<turnstile>Lit x::T"
  13.116  
  13.117    
  13.118 -  (* cf. 15.13.1 *)
  13.119 -  LAcc:	"[| localT E v = Some T; is_type (prg E) T |] ==>
  13.120 +  -- "cf. 15.13.1"
  13.121 +  LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
  13.122           E\<turnstile>LAcc v::T"
  13.123  
  13.124    BinOp:"[| E\<turnstile>e1::T;
  13.125 @@ -148,42 +147,42 @@
  13.126                          else T' = T \<and> T = PrimT Integer|] ==>
  13.127              E\<turnstile>BinOp bop e1 e2::T'"
  13.128  
  13.129 -  (* cf. 15.25, 15.25.1 *)
  13.130 +  -- "cf. 15.25, 15.25.1"
  13.131    LAss: "[| v ~= This;
  13.132              E\<turnstile>LAcc v::T;
  13.133 -	    E\<turnstile>e::T';
  13.134 +      E\<turnstile>e::T';
  13.135              prg E\<turnstile>T'\<preceq>T |] ==>
  13.136           E\<turnstile>v::=e::T'"
  13.137  
  13.138 -  (* cf. 15.10.1 *)
  13.139 +  -- "cf. 15.10.1"
  13.140    FAcc: "[| E\<turnstile>a::Class C; 
  13.141              field (prg E,C) fn = Some (fd,fT) |] ==>
  13.142              E\<turnstile>{fd}a..fn::fT"
  13.143  
  13.144 -  (* cf. 15.25, 15.25.1 *)
  13.145 +  -- "cf. 15.25, 15.25.1"
  13.146    FAss: "[| E\<turnstile>{fd}a..fn::T;
  13.147              E\<turnstile>v        ::T';
  13.148              prg E\<turnstile>T'\<preceq>T |] ==>
  13.149           E\<turnstile>{fd}a..fn:=v::T'"
  13.150  
  13.151  
  13.152 -  (* cf. 15.11.1, 15.11.2, 15.11.3 *)
  13.153 +  -- "cf. 15.11.1, 15.11.2, 15.11.3"
  13.154    Call: "[| E\<turnstile>a::Class C;
  13.155              E\<turnstile>ps[::]pTs;
  13.156              max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
  13.157           E\<turnstile>{C}a..mn({pTs'}ps)::rT"
  13.158  
  13.159 -(* well-typed expression lists *)
  13.160 +-- "well-typed expression lists"
  13.161  
  13.162 -  (* cf. 15.11.??? *)
  13.163 +  -- "cf. 15.11.???"
  13.164    Nil: "E\<turnstile>[][::][]"
  13.165  
  13.166 -  (* cf. 15.11.??? *)
  13.167 +  -- "cf. 15.11.???"
  13.168    Cons:"[| E\<turnstile>e::T;
  13.169             E\<turnstile>es[::]Ts |] ==>
  13.170          E\<turnstile>e#es[::]T#Ts"
  13.171  
  13.172 -(* well-typed statements *)
  13.173 +-- "well-typed statements"
  13.174  
  13.175    Skip:"E\<turnstile>Skip\<surd>"
  13.176  
  13.177 @@ -194,13 +193,13 @@
  13.178             E\<turnstile>s2\<surd> |] ==>
  13.179          E\<turnstile>s1;; s2\<surd>"
  13.180  
  13.181 -  (* cf. 14.8 *)
  13.182 +  -- "cf. 14.8"
  13.183    Cond:"[| E\<turnstile>e::PrimT Boolean;
  13.184             E\<turnstile>s1\<surd>;
  13.185             E\<turnstile>s2\<surd> |] ==>
  13.186           E\<turnstile>If(e) s1 Else s2\<surd>"
  13.187  
  13.188 -  (* cf. 14.10 *)
  13.189 +  -- "cf. 14.10"
  13.190    Loop:"[| E\<turnstile>e::PrimT Boolean;
  13.191             E\<turnstile>s\<surd> |] ==>
  13.192          E\<turnstile>While(e) s\<surd>"
  13.193 @@ -209,14 +208,14 @@
  13.194  
  13.195   wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
  13.196  "wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
  13.197 -	length pTs = length pns \<and>
  13.198 -	nodups pns \<and>
  13.199 -	unique lvars \<and>
  13.200 +  length pTs = length pns \<and>
  13.201 +  nodups pns \<and>
  13.202 +  unique lvars \<and>
  13.203          This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
  13.204 -	(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
  13.205 -	(\<forall>(vn,T)\<in>set lvars. is_type G T) &
  13.206 -	(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
  13.207 -	 E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
  13.208 +  (\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
  13.209 +  (\<forall>(vn,T)\<in>set lvars. is_type G T) &
  13.210 +  (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
  13.211 +   E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
  13.212  
  13.213  syntax 
  13.214   wf_java_prog :: "java_mb prog => bool"
  13.215 @@ -234,7 +233,8 @@
  13.216  apply ( drule (1) fields_is_type)
  13.217  apply (  simp (no_asm_simp))
  13.218  apply  (assumption)
  13.219 -apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI simp add: wf_mdecl_def)
  13.220 +apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI 
  13.221 +            simp add: wf_mdecl_def)
  13.222  done
  13.223  
  13.224  lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]