--- a/src/HOL/MicroJava/J/Conform.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Sun Dec 16 00:18:17 2001 +0100
@@ -8,14 +8,14 @@
theory Conform = State + WellType:
-types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" (* same as env of WellType.thy *)
+types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" -- "same as @{text env} of @{text WellType.thy}"
constdefs
hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50)
"h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
- conf :: "'c prog => aheap => val => ty => bool"
+ conf :: "'c prog => aheap => val => ty => bool"
("_,_ |- _ ::<= _" [51,51,51,51] 50)
"G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
@@ -29,7 +29,7 @@
hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
"G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
- conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
+ conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
"s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
@@ -112,7 +112,8 @@
apply (simp)
done
-lemma defval_conf [rule_format (no_asm)]: "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
+lemma defval_conf [rule_format (no_asm)]:
+ "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
apply (unfold conf_def)
apply (rule_tac "y" = "T" in ty.exhaust)
apply (erule ssubst)
@@ -127,7 +128,8 @@
apply auto
done
-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'"
+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'"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto intro: widen_trans)
@@ -168,7 +170,8 @@
apply (fast dest: non_npD)
done
-lemma non_np_objD' [rule_format (no_asm)]: "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->
+lemma non_np_objD' [rule_format (no_asm)]:
+ "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->
(\<forall>C. t = ClassT C --> C \<noteq> Object) -->
(\<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t)"
apply(rule_tac "y" = "t" in ref_ty.exhaust)
@@ -176,7 +179,9 @@
apply (fast dest: non_np_objD)
done
-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'"
+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'"
apply(induct_tac "vs")
apply(clarsimp)
apply(clarsimp)
@@ -208,7 +213,8 @@
apply auto
done
-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) -->
+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) -->
(\<forall>T. map_of fs f = Some T -->
(\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and> R v T))"
apply( induct_tac "fs")
@@ -231,7 +237,9 @@
apply auto
done
-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)"
+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)"
apply (unfold lconf_def)
apply( induct_tac "vns")
apply( clarsimp)
@@ -291,12 +299,14 @@
apply( fast dest: conforms_localD elim!: conformsI lconf_hext)
done
-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)"
-apply( rule conforms_hext)
-apply auto
-apply( rule hconfI)
-apply( drule conforms_heapD)
-apply( tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
+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)"
+apply(rule conforms_hext)
+apply auto
+apply(rule hconfI)
+apply(drule conforms_heapD)
+apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"]
+ addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
done
lemma conforms_upd_local:
--- a/src/HOL/MicroJava/J/Decl.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Sun Dec 16 00:18:17 2001 +0100
@@ -4,38 +4,28 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Class Declarations and whole Programs"
+header "Class Declarations and Programs"
theory Decl = Type:
-types fdecl (* field declaration, cf. 8.3 (, 9.3) *)
- = "vname \<times> ty"
+types
+ fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)"
+
+ sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2"
+
+ 'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class"
+
+ 'c class = "cname \<times> fdecl list \<times> 'c mdecl list"
+ -- "class = superclass, fields, methods"
+
+ 'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1"
+
+ 'c prog = "'c cdecl list" -- "program"
-types sig (* signature of a method, cf. 8.4.2 *)
- = "mname \<times> ty list"
-
- 'c mdecl (* method declaration in a class *)
- = "sig \<times> ty \<times> 'c"
-
-types 'c class (* class *)
- = "cname \<times> fdecl list \<times> 'c mdecl list"
- (* superclass, fields, methods*)
-
- 'c cdecl (* class declaration, cf. 8.1 *)
- = "cname \<times> 'c class"
-
-consts
-
- Object :: cname (* name of root class *)
- ObjectC :: "'c cdecl" (* decl of root class *)
-
-defs
-
- ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))"
-
-
-types 'c prog = "'c cdecl list"
+constdefs
+ ObjectC :: "'c cdecl" -- "decl of root class"
+ "ObjectC \<equiv> (Object, (arbitrary, [], []))"
translations
@@ -46,12 +36,14 @@
"cdecl c" <= (type) "cname \<times> (c class)"
"prog c" <= (type) "(c cdecl) list"
-constdefs
- class :: "'c prog => (cname \<leadsto> 'c class)"
- "class \<equiv> map_of"
- is_class :: "'c prog => cname => bool"
- "is_class G C \<equiv> class G C \<noteq> None"
+constdefs
+ class :: "'c prog => (cname \<leadsto> 'c class)"
+ "class \<equiv> map_of"
+
+ is_class :: "'c prog => cname => bool"
+ "is_class G C \<equiv> class G C \<noteq> None"
+
lemma finite_is_class: "finite {C. is_class G C}"
apply (unfold is_class_def class_def)
@@ -60,11 +52,9 @@
done
consts
-
- is_type :: "'c prog => ty => bool"
-
+ is_type :: "'c prog => ty => bool"
primrec
-"is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
+ "is_type G (PrimT pt) = True"
+ "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
end
--- a/src/HOL/MicroJava/J/Eval.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Sun Dec 16 00:18:17 2001 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Operational Evaluation (big-step) Semantics"
+header "Operational Evaluation (big step) Semantics"
theory Eval = State + WellType:
@@ -40,24 +40,24 @@
"G\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \<in> exec G"
"G\<turnstile>s -c -> s' " == "(s, c, s') \<in> exec G"
+
inductive "eval G" "evals G" "exec G" intros
-(* evaluation of expressions *)
+ (* evaluation of expressions *)
- (* cf. 15.5 *)
- XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"
+ XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)" -- "cf. 15.5"
- (* cf. 15.8.1 *)
+ -- "cf. 15.8.1"
NewC: "[| h = heap s; (a,x) = new_Addr h;
h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
G\<turnstile>Norm s -NewC C\<succ>Addr a-> c_hupd h' (x,s)"
- (* cf. 15.15 *)
+ -- "cf. 15.15"
Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
G\<turnstile>Norm s0 -Cast C e\<succ>v-> (x2,s1)"
- (* cf. 15.7.1 *)
+ -- "cf. 15.7.1"
Lit: "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
@@ -66,29 +66,27 @@
| Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
G\<turnstile>Norm s -BinOp bop e1 e2\<succ>v-> s2"
- (* cf. 15.13.1, 15.2 *)
+ -- "cf. 15.13.1, 15.2"
LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
- (* cf. 15.25.1 *)
+ -- "cf. 15.25.1"
LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
l' = (if x = None then l(va\<mapsto>v) else l) |] ==>
G\<turnstile>Norm s -va::=e\<succ>v-> (x,(h,l'))"
-
- (* cf. 15.10.1, 15.2 *)
+ -- "cf. 15.10.1, 15.2"
FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1);
v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
G\<turnstile>Norm s0 -{T}e..fn\<succ>v-> (np a' x1,s1)"
- (* cf. 15.25.1 *)
+ -- "cf. 15.25.1"
FAss: "[| G\<turnstile> Norm s0 -e1\<succ>a'-> (x1,s1); a = the_Addr a';
G\<turnstile>(np a' x1,s1) -e2\<succ>v -> (x2,s2);
h = heap s2; (c,fs) = the (h a);
h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
-
- (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
+ -- "cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15"
Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
@@ -96,48 +94,51 @@
G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
-(* evaluation of expression lists *)
- (* cf. 15.5 *)
+ -- "evaluation of expression lists"
+
+ -- "cf. 15.5"
XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
- (* cf. 15.11.??? *)
+ -- "cf. 15.11.???"
Nil: "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
- (* cf. 15.6.4 *)
+ -- "cf. 15.6.4"
Cons: "[| G\<turnstile>Norm s0 -e \<succ> v -> s1;
G\<turnstile> s1 -es[\<succ>]vs-> s2 |] ==>
G\<turnstile>Norm s0 -e#es[\<succ>]v#vs-> s2"
-(* execution of statements *)
- (* cf. 14.1 *)
+ -- "execution of statements"
+
+ -- "cf. 14.1"
XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
- (* cf. 14.5 *)
+ -- "cf. 14.5"
Skip: "G\<turnstile>Norm s -Skip-> Norm s"
- (* cf. 14.7 *)
+ -- "cf. 14.7"
Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
G\<turnstile>Norm s0 -Expr e-> s1"
- (* cf. 14.2 *)
+ -- "cf. 14.2"
Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
G\<turnstile> s1 -c2-> s2|] ==>
G\<turnstile>Norm s0 -c1;; c2-> s2"
- (* cf. 14.8.2 *)
+ -- "cf. 14.8.2"
Cond: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1;
G\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
G\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
- (* cf. 14.10, 14.10.1 *)
+ -- "cf. 14.10, 14.10.1"
LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
G\<turnstile>Norm s0 -While(e) c-> s1"
LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; the_Bool v;
- G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
+ G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
G\<turnstile>Norm s0 -While(e) c-> s3"
+
lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)]
lemma NewCI: "[|new_Addr (heap s) = (a,x);
--- a/src/HOL/MicroJava/J/Example.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Sun Dec 16 00:18:17 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: isabelle/Bali/Example.thy
+(* Title: HOL/MicroJava/J/Example.thy
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
@@ -41,12 +41,12 @@
datatype vnam_ = vee_ | x_ | e_
consts
-
cnam_ :: "cnam_ => cname"
vnam_ :: "vnam_ => vnam"
-axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
-
+-- "@{text cnam_} and @{text vnam_} are intended to be isomorphic
+ to @{text cnam} and @{text vnam}"
+axioms
inj_cnam_: "(cnam_ x = cnam_ y) = (x = y)"
inj_vnam_: "(vnam_ x = vnam_ y) = (x = y)"
@@ -56,7 +56,6 @@
declare inj_cnam_ [simp] inj_vnam_ [simp]
syntax
-
Base :: cname
Ext :: cname
vee :: vname
@@ -64,15 +63,13 @@
e :: vname
translations
-
"Base" == "cnam_ Base_"
- "Ext" == "cnam_ Ext_"
+ "Ext" == "cnam_ Ext_"
"vee" == "VName (vnam_ vee_)"
- "x" == "VName (vnam_ x_)"
- "e" == "VName (vnam_ e_)"
+ "x" == "VName (vnam_ x_)"
+ "e" == "VName (vnam_ e_)"
axioms
-
Base_not_Object: "Base \<noteq> Object"
Ext_not_Object: "Ext \<noteq> Object"
e_not_This: "e \<noteq> This"
@@ -83,28 +80,26 @@
declare Ext_not_Object [THEN not_sym, simp]
consts
-
foo_Base:: java_mb
foo_Ext :: java_mb
BaseC :: "java_mb cdecl"
ExtC :: "java_mb cdecl"
- test :: stmt
- foo :: mname
- a :: loc
+ test :: stmt
+ foo :: mname
+ a :: loc
b :: loc
defs
-
foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
BaseC_def:"BaseC == (Base, (Object,
- [(vee, PrimT Boolean)],
- [((foo,[Class Base]),Class Base,foo_Base)]))"
+ [(vee, PrimT Boolean)],
+ [((foo,[Class Base]),Class Base,foo_Base)]))"
foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
- (LAcc x)..vee:=Lit (Intg 1)),
- Lit Null)"
+ (LAcc x)..vee:=Lit (Intg Numeral1)),
+ Lit Null)"
ExtC_def: "ExtC == (Ext, (Base ,
- [(vee, PrimT Integer)],
- [((foo,[Class Base]),Class Ext,foo_Ext)]))"
+ [(vee, PrimT Integer)],
+ [((foo,[Class Base]),Class Ext,foo_Ext)]))"
test_def:"test == Expr(e::=NewC Ext);;
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
@@ -112,22 +107,21 @@
syntax
- NP :: xcpt
- tprg ::"java_mb prog"
- obj1 :: obj
- obj2 :: obj
- s0 :: state
- s1 :: state
- s2 :: state
- s3 :: state
- s4 :: state
+ NP :: xcpt
+ tprg ::"java_mb prog"
+ obj1 :: obj
+ obj2 :: obj
+ s0 :: state
+ s1 :: state
+ s2 :: state
+ s3 :: state
+ s4 :: state
translations
-
"NP" == "NullPointer"
"tprg" == "[ObjectC, BaseC, ExtC]"
"obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
- ((vee, Ext )\<mapsto>Intg 0))"
+ ((vee, Ext )\<mapsto>Intg 0))"
"s0" == " Norm (empty, empty)"
"s1" == " Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
"s2" == " Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
@@ -141,7 +135,7 @@
lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
apply (simp (no_asm_simp))
done
-declare map_of_Cons [simp del]; (* sic! *)
+declare map_of_Cons [simp del] -- "sic!"
lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
apply (unfold ObjectC_def class_def)
@@ -150,7 +144,7 @@
lemma class_tprg_Base [simp]:
"class tprg Base = Some (Object,
- [(vee, PrimT Boolean)],
+ [(vee, PrimT Boolean)],
[((foo, [Class Base]), Class Base, foo_Base)])"
apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
apply (simp (no_asm))
@@ -158,7 +152,7 @@
lemma class_tprg_Ext [simp]:
"class tprg Ext = Some (Base,
- [(vee, PrimT Integer)],
+ [(vee, PrimT Integer)],
[((foo, [Class Base]), Class Ext, foo_Ext)])"
apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
apply (simp (no_asm))
@@ -328,25 +322,25 @@
ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
-apply (tactic t) (* ;; *)
-apply (tactic t) (* Expr *)
-apply (tactic t) (* LAss *)
-apply simp (* e \<noteq> This *)
-apply (tactic t) (* LAcc *)
+apply (tactic t) -- ";;"
+apply (tactic t) -- "Expr"
+apply (tactic t) -- "LAss"
+apply simp -- {* @{text "e \<noteq> This"} *}
+apply (tactic t) -- "LAcc"
apply (simp (no_asm))
apply (simp (no_asm))
-apply (tactic t) (* NewC *)
+apply (tactic t) -- "NewC"
apply (simp (no_asm))
apply (simp (no_asm))
-apply (tactic t) (* Expr *)
-apply (tactic t) (* Call *)
-apply (tactic t) (* LAcc *)
+apply (tactic t) -- "Expr"
+apply (tactic t) -- "Call"
+apply (tactic t) -- "LAcc"
apply (simp (no_asm))
apply (simp (no_asm))
-apply (tactic t) (* Cons *)
-apply (tactic t) (* Lit *)
+apply (tactic t) -- "Cons"
+apply (tactic t) -- "Lit"
apply (simp (no_asm))
-apply (tactic t) (* Nil *)
+apply (tactic t) -- "Nil"
apply (simp (no_asm))
apply (rule max_spec_foo_Base)
done
@@ -359,38 +353,38 @@
" [|new_Addr (heap (snd s0)) = (a, None)|] ==>
tprg\<turnstile>s0 -test-> ?s"
apply (unfold test_def)
-(* ?s = s3 *)
-apply (tactic e) (* ;; *)
-apply (tactic e) (* Expr *)
-apply (tactic e) (* LAss *)
-apply (tactic e) (* NewC *)
+-- "?s = s3 "
+apply (tactic e) -- ";;"
+apply (tactic e) -- "Expr"
+apply (tactic e) -- "LAss"
+apply (tactic e) -- "NewC"
apply force
apply force
apply (simp (no_asm))
apply (erule thin_rl)
-apply (tactic e) (* Expr *)
-apply (tactic e) (* Call *)
-apply (tactic e) (* LAcc *)
+apply (tactic e) -- "Expr"
+apply (tactic e) -- "Call"
+apply (tactic e) -- "LAcc"
apply force
-apply (tactic e) (* Cons *)
-apply (tactic e) (* Lit *)
-apply (tactic e) (* Nil *)
+apply (tactic e) -- "Cons"
+apply (tactic e) -- "Lit"
+apply (tactic e) -- "Nil"
apply (simp (no_asm))
apply (force simp add: foo_Ext_def)
apply (simp (no_asm))
-apply (tactic e) (* Expr *)
-apply (tactic e) (* FAss *)
-apply (tactic e) (* Cast *)
-apply (tactic e) (* LAcc *)
+apply (tactic e) -- "Expr"
+apply (tactic e) -- "FAss"
+apply (tactic e) -- "Cast"
+apply (tactic e) -- "LAcc"
apply (simp (no_asm))
apply (simp (no_asm))
apply (simp (no_asm))
-apply (tactic e) (* XcptE *)
+apply (tactic e) -- "XcptE"
apply (simp (no_asm))
apply (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
apply (simp (no_asm))
apply (simp (no_asm))
-apply (tactic e) (* XcptE *)
+apply (tactic e) -- "XcptE"
done
end
--- a/src/HOL/MicroJava/J/JBasis.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Sun Dec 16 00:18:17 2001 +0100
@@ -13,9 +13,8 @@
section "unique"
constdefs
-
unique :: "('a \<times> 'b) list => bool"
- "unique == nodups \<circ> map fst"
+ "unique == nodups \<circ> map fst"
lemma fst_in_set_lemma [rule_format (no_asm)]:
@@ -71,4 +70,3 @@
done
end
-
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sun Dec 16 00:18:17 2001 +0100
@@ -161,7 +161,7 @@
declare fun_upd_same [simp]
ML{*
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
- (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
+ (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
*}
ML{*
Unify.search_bound := 40;
@@ -181,15 +181,16 @@
apply( rule eval_evals_exec_induct)
apply( unfold c_hupd_def)
-(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
+-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
apply( simp_all)
apply( tactic "ALLGOALS strip_tac")
-apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
-apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
+apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
+ THEN_ALL_NEW Full_simp_tac) *})
+apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
-(* Level 7 *)
+-- "Level 7"
-(* 15 NewC *)
+-- "15 NewC"
apply( drule new_AddrD)
apply( erule disjE)
prefer 2
@@ -201,13 +202,13 @@
apply( rule_tac [2] rtrancl_refl)
apply( simp (no_asm))
-(* for Cast *)
+-- "for Cast"
defer 1
-(* 14 Lit *)
+-- "14 Lit"
apply( erule conf_litval)
-(* 13 BinOp *)
+-- "13 BinOp"
apply (tactic "forward_hyp_tac")
apply (tactic "forward_hyp_tac")
apply( rule conjI, erule (1) hext_trans)
@@ -216,46 +217,48 @@
apply( drule eval_no_xcpt)
apply( simp split add: binop.split)
-(* 12 LAcc *)
+-- "12 LAcc"
apply( fast elim: conforms_localD [THEN lconfD])
-(* for FAss *)
-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*})
+-- "for FAss"
+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*})
-(* for if *)
+-- "for if"
apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
apply (tactic "forward_hyp_tac")
-(* 11+1 if *)
+-- "11+1 if"
prefer 8
apply( fast intro: hext_trans)
prefer 8
apply( fast intro: hext_trans)
-(* 10 Expr *)
+-- "10 Expr"
prefer 6
apply( fast)
-(* 9 ??? *)
+-- "9 ???"
apply( simp_all)
-(* 8 Cast *)
+-- "8 Cast"
prefer 8
apply (rule impI)
apply (drule raise_if_NoneD)
apply (clarsimp)
apply (fast elim: Cast_conf)
-(* 7 LAss *)
+-- "7 LAss"
apply (fold fun_upd_def)
-apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) 1 *})
+apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
+ THEN_ALL_NEW Full_simp_tac) 1 *})
apply( blast intro: conforms_upd_local conf_widen)
-(* 6 FAcc *)
+-- "6 FAcc"
apply( fast elim!: FAcc_type_sound)
-(* 5 While *)
+-- "5 While"
prefer 5
apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
@@ -263,15 +266,15 @@
apply (tactic "forward_hyp_tac")
-(* 4 Cons *)
+-- "4 Cons"
prefer 3
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
-(* 3 ;; *)
+-- "3 ;;"
prefer 3
apply( fast intro: hext_trans)
-(* 2 FAss *)
+-- "2 FAss"
apply( case_tac "x2 = None")
prefer 2
apply( simp (no_asm_simp))
@@ -281,9 +284,9 @@
apply( erule FAss_type_sound, rule HOL.refl, assumption+)
apply( tactic prune_params_tac)
-(* Level 52 *)
+-- "Level 52"
-(* 1 Call *)
+-- "1 Call"
apply( case_tac "x")
prefer 2
apply( clarsimp)
--- a/src/HOL/MicroJava/J/State.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy Sun Dec 16 00:18:17 2001 +0100
@@ -8,58 +8,57 @@
theory State = TypeRel + Value:
-types fields_
- = "(vname \<times> cname \<leadsto> val)" (* field name, defining class, value *)
+types
+ fields_ = "(vname \<times> cname \<leadsto> val)" -- "field name, defining class, value"
- obj = "cname \<times> fields_" (* class instance with class name and fields *)
+ obj = "cname \<times> fields_" -- "class instance with class name and fields"
constdefs
- obj_ty :: "obj => ty"
+ obj_ty :: "obj => ty"
"obj_ty obj == Class (fst obj)"
- init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
- "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
+ init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
+ "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-datatype xcpt (* exceptions *)
- = NullPointer
- | ClassCast
- | OutOfMemory
+
+types aheap = "loc \<leadsto> obj" -- {* "@{text heap}" used in a translation below *}
+ locals = "vname \<leadsto> val" -- "simple state, i.e. variable contents"
-types aheap = "loc \<leadsto> obj" (** "heap" used in a translation below **)
- locals = "vname \<leadsto> val"
+ state = "aheap \<times> locals" -- "heap, local parameter including This"
+ xstate = "xcpt option \<times> state" -- "state including exception information"
+
- state (* simple state, i.e. variable contents *)
- = "aheap \<times> locals"
- (* heap, local parameter including This *)
+text {*
+ System exceptions are allocated in all heaps,
+ and they don't carry any information other than their type: *}
+axioms
+ system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)"
- xstate (* state including exception information *)
- = "xcpt option \<times> state"
syntax
- heap :: "state => aheap"
- locals :: "state => locals"
- Norm :: "state => xstate"
+ heap :: "state => aheap"
+ locals :: "state => locals"
+ Norm :: "state => xstate"
translations
"heap" => "fst"
"locals" => "snd"
- "Norm s" == "(None,s)"
+ "Norm s" == "(None,s)"
constdefs
-
- new_Addr :: "aheap => loc \<times> xcpt option"
+ new_Addr :: "aheap => loc \<times> xcpt option"
"new_Addr h == SOME (a,x). (h a = None \<and> x = None) | x = Some OutOfMemory"
- raise_if :: "bool => xcpt => xcpt option => xcpt option"
+ raise_if :: "bool => xcpt => xcpt option => xcpt option"
"raise_if c x xo == if c \<and> (xo = None) then Some x else xo"
- np :: "val => xcpt option => xcpt option"
+ np :: "val => xcpt option => xcpt option"
"np v == raise_if (v = Null) NullPointer"
- c_hupd :: "aheap => xstate => xstate"
+ c_hupd :: "aheap => xstate => xstate"
"c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
- cast_ok :: "'c prog => cname => aheap => val => bool"
+ cast_ok :: "'c prog => cname => aheap => val => bool"
"cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
@@ -93,7 +92,8 @@
apply auto
done
-lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \<noteq> None"
+lemma raise_if_Some2 [simp]:
+ "raise_if c z (if x = None then Some y else x) \<noteq> None"
apply (unfold raise_if_def)
apply(induct_tac "x")
apply auto
@@ -105,12 +105,14 @@
apply auto
done
-lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \<not> c \<and> y = None"
+lemma raise_if_NoneD [rule_format (no_asm)]:
+ "raise_if c x y = None --> \<not> c \<and> y = None"
apply (unfold raise_if_def)
apply auto
done
-lemma np_NoneD [rule_format (no_asm)]: "np a' x' = None --> x' = None \<and> a' \<noteq> Null"
+lemma np_NoneD [rule_format (no_asm)]:
+ "np a' x' = None --> x' = None \<and> a' \<noteq> Null"
apply (unfold np_def raise_if_def)
apply auto
done
--- a/src/HOL/MicroJava/J/Term.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy Sun Dec 16 00:18:17 2001 +0100
@@ -8,25 +8,24 @@
theory Term = Value:
-datatype binop = Eq | Add (* function codes for binary operation *)
+datatype binop = Eq | Add -- "function codes for binary operation"
datatype expr
- = NewC cname (* class instance creation *)
- | Cast cname expr (* type cast *)
- | Lit val (* literal value, also references *)
- | BinOp binop expr expr (* binary operation *)
- | LAcc vname (* local (incl. parameter) access *)
- | LAss vname expr (* local assign *) ("_::=_" [ 90,90]90)
- | FAcc cname expr vname (* field access *) ("{_}_.._" [10,90,99 ]90)
+ = NewC cname -- "class instance creation"
+ | Cast cname expr -- "type cast"
+ | Lit val -- "literal value, also references"
+ | BinOp binop expr expr -- "binary operation"
+ | LAcc vname -- "local (incl. parameter) access"
+ | LAss vname expr ("_::=_" [90,90]90) -- "local assign"
+ | FAcc cname expr vname ("{_}_.._" [10,90,99]90) -- "field access"
| FAss cname expr vname
- expr (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
+ expr ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
| Call cname expr mname
- "ty list" "expr list" (* method call*) ("{_}_.._'( {_}_')"
- [10,90,99,10,10] 90)
+ "ty list" "expr list" ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call"
datatype stmt
- = Skip (* empty statement *)
- | Expr expr (* expression statement *)
+ = Skip -- "empty statement"
+ | Expr expr -- "expression statement"
| Comp stmt stmt ("_;; _" [61,60]60)
| Cond expr stmt stmt ("If '(_') _ Else _" [80,79,79]70)
| Loop expr stmt ("While '(_') _" [80,79]70)
--- a/src/HOL/MicroJava/J/Type.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Sun Dec 16 00:18:17 2001 +0100
@@ -8,29 +8,47 @@
theory Type = JBasis:
-typedecl cname (* class name *)
-typedecl vnam (* variable or field name *)
-typedecl mname (* method name *)
+typedecl cnam
+
+ -- "exceptions"
+datatype
+ xcpt
+ = NullPointer
+ | ClassCast
+ | OutOfMemory
-datatype vname (* names for This pointer and local/field variables *)
+-- "class names"
+datatype cname
+ = Object
+ | Xcpt xcpt
+ | Cname cname
+
+typedecl vnam -- "variable or field name"
+typedecl mname -- "method name"
+
+-- "names for @{text This} pointer and local/field variables"
+datatype vname
= This
| VName vnam
-datatype prim_ty (* primitive type, cf. 4.2 *)
- = Void (* 'result type' of void methods *)
+-- "primitive type, cf. 4.2"
+datatype prim_ty
+ = Void -- "'result type' of void methods"
| Boolean
| Integer
-datatype ref_ty (* reference type, cf. 4.3 *)
- = NullT (* null type, cf. 4.1 *)
- | ClassT cname (* class type *)
+-- "reference type, cf. 4.3"
+datatype ref_ty
+ = NullT -- "null type, cf. 4.1"
+ | ClassT cname -- "class type"
-datatype ty (* any type, cf. 4.1 *)
- = PrimT prim_ty (* primitive type *)
- | RefT ref_ty (* reference type *)
+-- "any type, cf. 4.1"
+datatype ty
+ = PrimT prim_ty -- "primitive type"
+ | RefT ref_ty -- "reference type"
syntax
- NT :: " ty"
+ NT :: "ty"
Class :: "cname => ty"
translations
--- a/src/HOL/MicroJava/J/TypeRel.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Sun Dec 16 00:18:17 2001 +0100
@@ -9,9 +9,9 @@
theory TypeRel = Decl:
consts
- subcls1 :: "'c prog => (cname \<times> cname) set" (* subclass *)
- widen :: "'c prog => (ty \<times> ty ) set" (* widening *)
- cast :: "'c prog => (cname \<times> cname) set" (* casting *)
+ subcls1 :: "'c prog => (cname \<times> cname) set" -- "subclass"
+ widen :: "'c prog => (ty \<times> ty ) set" -- "widening"
+ cast :: "'c prog => (cname \<times> cname) set" -- "casting"
syntax (xsymbols)
subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
@@ -31,9 +31,8 @@
"G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G"
"G\<turnstile>C \<preceq>? D" == "(C,D) \<in> cast G"
+-- "direct subclass, cf. 8.1.3"
inductive "subcls1 G" intros
-
- (* direct subclass, cf. 8.1.3 *)
subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
lemma subcls1D:
@@ -91,7 +90,7 @@
field :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
-(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
+-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
@@ -105,7 +104,7 @@
done
-(* list of fields of a class, including inherited and hidden ones *)
+-- "list of fields of a class, including inherited and hidden ones"
defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) [] (\<lambda>C fs ms ts.
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
@@ -129,14 +128,15 @@
done
-inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3
- i.e. sort of syntactic subtyping *)
- refl [intro!, simp]: "G\<turnstile> T \<preceq> T" (* identity conv., cf. 5.1.1 *)
+-- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
+inductive "widen G" intros
+ refl [intro!, simp]: "G\<turnstile> T \<preceq> T" -- "identity conv., cf. 5.1.1"
subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
null [intro!]: "G\<turnstile> NT \<preceq> RefT R"
-inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *)
- (* left out casts on primitve types *)
+-- "casting conversion, cf. 5.5 / 5.1.5"
+-- "left out casts on primitve types"
+inductive "cast G" intros
widen: "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
@@ -173,45 +173,11 @@
apply (auto elim: widen.subcls)
done
-lemma widen_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
-apply (erule widen.induct)
-apply safe
-apply (frule widen_Class)
-apply (frule_tac [2] widen_RefT)
-apply safe
-apply(erule (1) rtrancl_trans)
-done
-
-
-(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
+theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
proof -
- assume "G\<turnstile>S\<preceq>U"
- thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
- proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
- case refl
- fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
- ( * fix T' show "PROP ?P T T".* )
- next
- case subcls
- fix T assume "G\<turnstile>Class D\<preceq>T"
- then obtain E where "T = Class E" by (blast dest: widen_Class)
- from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
- next
- case null
- fix RT assume "G\<turnstile>RefT R\<preceq>RT"
- then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
- thus "G\<turnstile>NT\<preceq>RT" by auto
- qed
-qed
-*)
-
-theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
-proof -
- assume "G\<turnstile>S\<preceq>U"
- thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
+ assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
proof induct
- case (refl T T')
- thus "G\<turnstile>T\<preceq>T'" .
+ case (refl T T') thus "G\<turnstile>T\<preceq>T'" .
next
case (subcls C D T)
then obtain E where "T = Class E" by (blast dest: widen_Class)
--- a/src/HOL/MicroJava/J/Value.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Sun Dec 16 00:18:17 2001 +0100
@@ -8,15 +8,19 @@
theory Value = Type:
-typedecl loc (* locations, i.e. abstract references on objects *)
+typedecl loc_ -- "locations, i.e. abstract references on objects"
+
+datatype loc
+ = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
+ | Loc loc_ -- "usual locations (references on objects)"
datatype val
- = Unit (* dummy result value of void methods *)
- | Null (* null reference *)
- | Bool bool (* Boolean value *)
- | Intg int (* integer value, name Intg instead of Int because
- of clash with HOL/Set.thy *)
- | Addr loc (* addresses, i.e. locations of objects *)
+ = Unit -- "dummy result value of void methods"
+ | Null -- "null reference"
+ | Bool bool -- "Boolean value"
+ | Intg int -- "integer value, name Intg instead of Int because
+ of clash with HOL/Set.thy"
+ | Addr loc -- "addresses, i.e. locations of objects "
consts
the_Bool :: "val => bool"
@@ -33,8 +37,8 @@
"the_Addr (Addr a) = a"
consts
- defpval :: "prim_ty => val" (* default value for primitive types *)
- default_val :: "ty => val" (* default value for all types *)
+ defpval :: "prim_ty => val" -- "default value for primitive types"
+ default_val :: "ty => val" -- "default value for all types"
primrec
"defpval Void = Unit"
--- a/src/HOL/MicroJava/J/WellForm.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Sun Dec 16 00:18:17 2001 +0100
@@ -57,7 +57,7 @@
done
lemma class_Object [simp]:
- "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
+ "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
apply (unfold wf_prog_def ObjectC_def class_def)
apply (auto intro: map_of_SomeI)
done
@@ -205,13 +205,15 @@
apply auto
done
-lemma widen_fields_defpl: "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>
+lemma widen_fields_defpl:
+ "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>
G\<turnstile>C\<preceq>C fd"
apply( drule (1) widen_fields_defpl')
apply (fast)
done
-lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
+lemma unique_fields:
+ "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
apply( erule subcls1_induct)
apply( assumption)
apply( safe dest!: wf_cdecl_supD)
@@ -232,7 +234,8 @@
apply(auto dest!: widen_fields_defpl)
done
-lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>
+lemma fields_mono_lemma [rule_format (no_asm)]:
+ "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>
x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
apply(erule converse_rtrancl_induct)
apply( safe dest!: subcls1D)
@@ -260,7 +263,8 @@
apply (fast dest: fields_mono)
done
-lemma method_wf_mdecl [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>
+lemma method_wf_mdecl [rule_format (no_asm)]:
+ "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>
method (G,C) sig = Some (md,mh,m)
--> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
apply( erule subcls1_induct)
@@ -322,10 +326,13 @@
"[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;
method (G,D) sig = Some (md, rT, b) |]
==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
-apply(auto dest: subcls_widen_methd method_wf_mdecl simp add: wf_mdecl_def wf_mhead_def split_def)
+apply(auto dest: subcls_widen_methd method_wf_mdecl
+ simp add: wf_mdecl_def wf_mhead_def split_def)
done
-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)"
+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)"
apply (erule (1) subcls1_induct)
apply (simp)
apply (erule conjE)
@@ -366,7 +373,8 @@
done
-lemma fields_is_type_lemma [rule_format (no_asm)]: "[|is_class G C; wf_prog wf_mb G|] ==>
+lemma fields_is_type_lemma [rule_format (no_asm)]:
+ "[|is_class G C; wf_prog wf_mb G|] ==>
\<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
apply( erule (1) subcls1_induct)
apply( simp (no_asm_simp))
@@ -385,7 +393,8 @@
apply auto
done
-lemma fields_is_type: "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>
+lemma fields_is_type:
+ "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>
is_type G f"
apply(drule map_of_SomeD)
apply(drule (2) fields_is_type_lemma)
@@ -401,31 +410,19 @@
assume m: "(sig,rT,code) \<in> set mdecls"
moreover
- from wf
- have "class G Object = Some (arbitrary, [], [])"
- by simp
+ from wf have "class G Object = Some (arbitrary, [], [])" by simp
moreover
- from wf C
- have c: "class G C = Some (S,fs,mdecls)"
+ from wf C have c: "class G C = Some (S,fs,mdecls)"
by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
ultimately
- have O: "C \<noteq> Object"
- by auto
-
- from wf C
- have "unique mdecls"
- by (unfold wf_prog_def wf_cdecl_def) auto
+ have O: "C \<noteq> Object" by auto
- hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
- by - (induct mdecls, auto)
-
- with m
- have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
+ from wf C have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
+ hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)
+ with m have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
by (force intro: map_of_SomeI)
-
with wf C m c O
- show ?thesis
- by (auto simp add: is_class_def dest: method_rec)
+ show ?thesis by (auto simp add: is_class_def dest: method_rec)
qed
end
--- a/src/HOL/MicroJava/J/WellType.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Sun Dec 16 00:18:17 2001 +0100
@@ -21,16 +21,17 @@
\end{itemize}
\end{description}
*}
-types lenv (* local variables, including method parameters and This *)
- = "vname \<leadsto> ty"
- 'c env
- = "'c prog \<times> lenv"
+
+text "local variables, including method parameters and This:"
+types
+ lenv = "vname \<leadsto> ty"
+ 'c env = "'c prog \<times> lenv"
syntax
prg :: "'c env => 'c prog"
localT :: "'c env => (vname \<leadsto> ty)"
-translations
+translations
"prg" => "fst"
"localT" => "snd"
@@ -42,15 +43,15 @@
defs
more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
- list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
+ list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
- (* applicable methods, cf. 15.11.2.1 *)
+ -- "applicable methods, cf. 15.11.2.1"
appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
- {((Class md,rT),pTs') |md rT mb pTs'.
- method (G,C) (mn, pTs') = Some (md,rT,mb) \<and>
- list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
+ {((Class md,rT),pTs') |md rT mb pTs'.
+ method (G,C) (mn, pTs') = Some (md,rT,mb) \<and>
+ list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
- (* maximally specific methods, cf. 15.11.2.2 *)
+ -- "maximally specific methods, cf. 15.11.2.2"
max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and>
(\<forall>m'\<in>appl_methds G C sig.
more_spec G m' m --> m' = m)}"
@@ -77,13 +78,14 @@
typeof :: "(loc => ty option) => val => ty option"
primrec
- "typeof dt Unit = Some (PrimT Void)"
- "typeof dt Null = Some NT"
- "typeof dt (Bool b) = Some (PrimT Boolean)"
- "typeof dt (Intg i) = Some (PrimT Integer)"
- "typeof dt (Addr a) = dt a"
+ "typeof dt Unit = Some (PrimT Void)"
+ "typeof dt Null = Some NT"
+ "typeof dt (Bool b) = Some (PrimT Boolean)"
+ "typeof dt (Intg i) = Some (PrimT Integer)"
+ "typeof dt (Addr a) = dt a"
-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)"
+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)"
apply (rule val.induct)
apply auto
done
@@ -95,9 +97,9 @@
done
types
- java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
-(* method body with parameter names, local variables, block, result expression.
- local variables might include This, which is hidden anyway *)
+ java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
+-- "method body with parameter names, local variables, block, result expression."
+-- "local variables might include This, which is hidden anyway"
consts
ty_expr :: "java_mb env => (expr \<times> ty ) set"
@@ -116,30 +118,27 @@
translations
- "E\<turnstile>e :: T" == "(e,T) \<in> ty_expr E"
- "E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
- "E\<turnstile>c \<surd>" == "c \<in> wt_stmt E"
+ "E\<turnstile>e :: T" == "(e,T) \<in> ty_expr E"
+ "E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
+ "E\<turnstile>c \<surd>" == "c \<in> wt_stmt E"
inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
-
-(* well-typed expressions *)
+
+ NewC: "[| is_class (prg E) C |] ==>
+ E\<turnstile>NewC C::Class C" -- "cf. 15.8"
- (* cf. 15.8 *)
- NewC: "[| is_class (prg E) C |] ==>
- E\<turnstile>NewC C::Class C"
-
- (* cf. 15.15 *)
- Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
+ -- "cf. 15.15"
+ Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
prg E\<turnstile>C\<preceq>? D |] ==>
E\<turnstile>Cast D e::Class D"
- (* cf. 15.7.1 *)
- Lit: "[| typeof (\<lambda>v. None) x = Some T |] ==>
+ -- "cf. 15.7.1"
+ Lit: "[| typeof (\<lambda>v. None) x = Some T |] ==>
E\<turnstile>Lit x::T"
- (* cf. 15.13.1 *)
- LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
+ -- "cf. 15.13.1"
+ LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
E\<turnstile>LAcc v::T"
BinOp:"[| E\<turnstile>e1::T;
@@ -148,42 +147,42 @@
else T' = T \<and> T = PrimT Integer|] ==>
E\<turnstile>BinOp bop e1 e2::T'"
- (* cf. 15.25, 15.25.1 *)
+ -- "cf. 15.25, 15.25.1"
LAss: "[| v ~= This;
E\<turnstile>LAcc v::T;
- E\<turnstile>e::T';
+ E\<turnstile>e::T';
prg E\<turnstile>T'\<preceq>T |] ==>
E\<turnstile>v::=e::T'"
- (* cf. 15.10.1 *)
+ -- "cf. 15.10.1"
FAcc: "[| E\<turnstile>a::Class C;
field (prg E,C) fn = Some (fd,fT) |] ==>
E\<turnstile>{fd}a..fn::fT"
- (* cf. 15.25, 15.25.1 *)
+ -- "cf. 15.25, 15.25.1"
FAss: "[| E\<turnstile>{fd}a..fn::T;
E\<turnstile>v ::T';
prg E\<turnstile>T'\<preceq>T |] ==>
E\<turnstile>{fd}a..fn:=v::T'"
- (* cf. 15.11.1, 15.11.2, 15.11.3 *)
+ -- "cf. 15.11.1, 15.11.2, 15.11.3"
Call: "[| E\<turnstile>a::Class C;
E\<turnstile>ps[::]pTs;
max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
E\<turnstile>{C}a..mn({pTs'}ps)::rT"
-(* well-typed expression lists *)
+-- "well-typed expression lists"
- (* cf. 15.11.??? *)
+ -- "cf. 15.11.???"
Nil: "E\<turnstile>[][::][]"
- (* cf. 15.11.??? *)
+ -- "cf. 15.11.???"
Cons:"[| E\<turnstile>e::T;
E\<turnstile>es[::]Ts |] ==>
E\<turnstile>e#es[::]T#Ts"
-(* well-typed statements *)
+-- "well-typed statements"
Skip:"E\<turnstile>Skip\<surd>"
@@ -194,13 +193,13 @@
E\<turnstile>s2\<surd> |] ==>
E\<turnstile>s1;; s2\<surd>"
- (* cf. 14.8 *)
+ -- "cf. 14.8"
Cond:"[| E\<turnstile>e::PrimT Boolean;
E\<turnstile>s1\<surd>;
E\<turnstile>s2\<surd> |] ==>
E\<turnstile>If(e) s1 Else s2\<surd>"
- (* cf. 14.10 *)
+ -- "cf. 14.10"
Loop:"[| E\<turnstile>e::PrimT Boolean;
E\<turnstile>s\<surd> |] ==>
E\<turnstile>While(e) s\<surd>"
@@ -209,14 +208,14 @@
wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
- length pTs = length pns \<and>
- nodups pns \<and>
- unique lvars \<and>
+ length pTs = length pns \<and>
+ nodups pns \<and>
+ unique lvars \<and>
This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>
- (\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
- (\<forall>(vn,T)\<in>set lvars. is_type G T) &
- (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
- E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
+ (\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
+ (\<forall>(vn,T)\<in>set lvars. is_type G T) &
+ (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
+ E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
syntax
wf_java_prog :: "java_mb prog => bool"
@@ -234,7 +233,8 @@
apply ( drule (1) fields_is_type)
apply ( simp (no_asm_simp))
apply (assumption)
-apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI simp add: wf_mdecl_def)
+apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI
+ simp add: wf_mdecl_def)
done
lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]