improved superclass entry for classes and definition status of is_class, class
corrected recursive definitions of "method" and "fields"
cleanup of many proofs, removed superfluous tactics and theorems
--- a/src/HOL/MicroJava/J/Conform.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML Wed Dec 06 19:10:36 2000 +0100
@@ -6,71 +6,59 @@
section "hext";
-val hextI = prove_goalw thy [hext_def] "!!h. \
-\ \\<forall>a C fs . h a = Some (C,fs) --> \
-\ (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'" (K [Auto_tac ]);
+Goalw [hext_def]
+" \\<forall>a C fs . h a = Some (C,fs) --> \
+\ (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'";
+by Auto_tac;
+qed "hextI";
-val hext_objD = prove_goalw thy [hext_def]
-"!!h. [|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')"
- (K [Force_tac 1]);
+Goalw [hext_def] "[|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')";
+by (Force_tac 1);
+qed "hext_objD";
-val hext_refl = prove_goal thy "h\\<le>|h" (K [
- rtac hextI 1,
- Fast_tac 1]);
+Goal "h\\<le>|h";
+by (rtac hextI 1);
+by (Fast_tac 1);
+qed "hext_refl";
-val hext_new = prove_goal thy "!!h. h a = None ==> h\\<le>|h(a\\<mapsto>x)" (K [
- rtac hextI 1,
- safe_tac HOL_cs,
- ALLGOALS (case_tac "aa = a"),
- Auto_tac]);
+Goal "h a = None ==> h\\<le>|h(a\\<mapsto>x)";
+by (rtac hextI 1);
+by Auto_tac;
+qed "hext_new";
-val hext_trans = prove_goal thy "!!h. [|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''" (K [
- rtac hextI 1,
- safe_tac HOL_cs,
- fast_tac (HOL_cs addDs [hext_objD]) 1]);
+Goal "[|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''";
+by (rtac hextI 1);
+by (fast_tac (HOL_cs addDs [hext_objD]) 1);
+qed "hext_trans";
Addsimps [hext_refl, hext_new];
-val hext_upd_obj = prove_goal thy
-"!!h. h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
- rtac hextI 1,
- safe_tac HOL_cs,
- ALLGOALS (case_tac "aa = a"),
- Auto_tac]);
+Goal "h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))";
+by (rtac hextI 1);
+by Auto_tac;
+qed "hext_upd_obj";
section "conf";
-val conf_Null = prove_goalw thy [conf_def]
-"G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
+Goalw [conf_def] "G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T";
+by (Simp_tac 1);
+qed "conf_Null";
Addsimps [conf_Null];
-val conf_litval = prove_goalw thy [conf_def]
-"typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T" (K [
- rtac val_.induct 1,
- Auto_tac]) RS mp;
-
-Goalw [conf_def] "G,s\\<turnstile>Unit::\\<preceq>PrimT Void";
-by( Simp_tac 1);
-qed "conf_VoidI";
-
-Goalw [conf_def] "G,s\\<turnstile>Bool b::\\<preceq>PrimT Boolean";
-by( Simp_tac 1);
-qed "conf_BooleanI";
+Goalw [conf_def] "typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T";
+by (rtac val_.induct 1);
+by Auto_tac;
+qed_spec_mp "conf_litval";
+Addsimps[conf_litval];
-Goalw [conf_def] "G,s\\<turnstile>Intg i::\\<preceq>PrimT Integer";
-by( Simp_tac 1);
-qed "conf_IntegerI";
-
-Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
+Goalw [conf_def] "[|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T";
+by (Asm_full_simp_tac 1);
+qed "conf_AddrI";
-val conf_AddrI = prove_goalw thy [conf_def]
-"!!G. [|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T"
-(K [Asm_full_simp_tac 1]);
-
-val conf_obj_AddrI = prove_goalw thy [conf_def]
- "!!G. [|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D"
-(K [Asm_full_simp_tac 1]);
+Goalw [conf_def] "[|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D";
+by (Asm_full_simp_tac 1);
+qed "conf_obj_AddrI";
Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
by (res_inst_tac [("y","T")] ty.exhaust 1);
@@ -79,39 +67,25 @@
by (auto_tac (claset(), simpset() addsimps [widen.null]));
qed_spec_mp "defval_conf";
-val conf_upd_obj = prove_goalw thy [conf_def]
-"h a = Some (C,fs) --> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)" (fn _ => [
- rtac impI 1,
- rtac val_.induct 1,
- ALLGOALS Simp_tac,
- case_tac "loc = a" 1,
- ALLGOALS Asm_simp_tac]) RS mp;
-
-val conf_widen = prove_goalw thy [conf_def]
-"!!G. wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'" (K [
- rtac val_.induct 1,
- ALLGOALS Simp_tac,
- ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
-bind_thm ("conf_widen", conf_widen);
+Goalw [conf_def]
+"h a = Some (C,fs) ==> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)";
+by (rtac val_.induct 1);
+by Auto_tac;
+qed "conf_upd_obj";
-val conf_hext' = prove_goalw thy [conf_def]
- "!!h. h\\<le>|h' ==> (\\<forall>v T. G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T)" (K [
- REPEAT (rtac allI 1),
- rtac val_.induct 1,
- ALLGOALS Simp_tac,
- safe_tac (HOL_cs addSDs [option_map_SomeD]),
- rewtac option_map_def,
- dtac hext_objD 1,
- Auto_tac]);
-val conf_hext = conf_hext' RS spec RS spec RS mp;
-bind_thm ("conf_hext", conf_hext);
+Goalw [conf_def] "wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'";
+by (rtac val_.induct 1);
+by (auto_tac (claset() addIs [widen_trans], simpset()));
+qed_spec_mp "conf_widen";
-val new_locD = prove_goalw thy [conf_def]
- "[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a" (fn prems => [
- cut_facts_tac prems 1,
- Full_simp_tac 1,
- safe_tac HOL_cs,
- Asm_full_simp_tac 1]);
+Goalw [conf_def] "h\\<le>|h' ==> G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T";
+by (rtac val_.induct 1);
+by (auto_tac (claset() addDs [hext_objD], simpset()));
+qed_spec_mp "conf_hext";
+
+Goalw [conf_def] "[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a";
+by Auto_tac;
+qed "new_locD";
Goalw [conf_def]
"G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null | \
@@ -120,34 +94,28 @@
by(Auto_tac);
qed_spec_mp "conf_RefTD";
-val conf_NullTD = prove_goal thy "!!G. G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null" (K [
- dtac conf_RefTD 1,
- Step_tac 1,
- Auto_tac]);
+Goal "G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null";
+by (dtac conf_RefTD 1);
+by Auto_tac;
+qed "conf_NullTD";
-val non_npD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
-\ \\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t" (K [
- dtac conf_RefTD 1,
- Step_tac 1,
- Auto_tac]);
+Goal "[|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
+\ \\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t";
+by (dtac conf_RefTD 1);
+by Auto_tac;
+qed "non_npD";
-val non_np_objD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
-\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>C'\\<preceq>C C)"
- (K[fast_tac (claset() addDs [non_npD]) 1]);
+Goal "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
+\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>C'\\<preceq>C C)";
+by (fast_tac (claset() addDs [non_npD]) 1);
+qed "non_np_objD";
-Goal "a' \\<noteq> Null --> wf_prog wf_mb G --> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
+Goal "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)";
-by(rtac impI 1);
-by(rtac impI 1);
by(res_inst_tac [("y","t")] ref_ty.exhaust 1);
- by(Safe_tac);
- by(dtac conf_NullTD 1);
- by(contr_tac 1);
-by(dtac non_np_objD 1);
- by(atac 1);
- by(Fast_tac 1);
-by(Fast_tac 1);
+ by (fast_tac (claset() addDs [conf_NullTD]) 1);
+by (fast_tac (claset() addDs [non_np_objD]) 1);
qed_spec_mp "non_np_objD'";
Goal "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'";
@@ -165,20 +133,18 @@
section "lconf";
-val lconfD = prove_goalw thy [lconf_def]
- "!!X. [| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T"
- (K [Force_tac 1]);
+Goalw[lconf_def] "[| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T";
+by (Force_tac 1);
+qed "lconfD";
-val lconf_hext = prove_goalw thy [lconf_def]
- "!!X. [| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L" (K [
- fast_tac (claset() addEs [conf_hext]) 1]);
+Goalw [lconf_def] "[| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L";
+by (fast_tac (claset() addEs [conf_hext]) 1);
+qed "lconf_hext";
AddEs [lconf_hext];
Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
\ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
-by( Clarify_tac 1);
-by( case_tac "n = va" 1);
- by Auto_tac;
+by Auto_tac;
qed "lconf_upd";
Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
@@ -199,9 +165,9 @@
qed "lconf_init_vars";
AddSIs [lconf_init_vars];
-val lconf_ext = prove_goalw thy [lconf_def]
-"!!X. [|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)"
- (K [Auto_tac]);
+Goalw [lconf_def] "[|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)";
+by Auto_tac;
+qed "lconf_ext";
Goalw [lconf_def] "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)";
by( induct_tac "vns" 1);
@@ -213,14 +179,15 @@
section "oconf";
-val oconf_hext = prove_goalw thy [oconf_def]
-"!!X. G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
+Goalw [oconf_def] "G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>";
+by (Fast_tac 1);
+qed "oconf_hext";
-val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
-\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T))"(K [
- Auto_tac]);
-
-val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
+Goalw [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
+\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T))";
+by Auto_tac;
+qed "oconf_obj";
+bind_thm ("oconf_objD", oconf_obj RS iffD1 RS spec RS spec RS mp);
section "hconf";
@@ -236,19 +203,17 @@
section "conforms";
-val conforms_heapD = prove_goalw thy [conforms_def]
- "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>"
- (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
+Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>";
+by (Asm_full_simp_tac 1);
+qed "conforms_heapD";
-val conforms_localD = prove_goalw thy [conforms_def]
- "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT" (fn prems => [
- cut_facts_tac prems 1, Asm_full_simp_tac 1]);
+Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT";
+by (Asm_full_simp_tac 1);
+qed "conforms_localD";
-val conformsI = prove_goalw thy [conforms_def]
-"[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)" (fn prems => [
- cut_facts_tac prems 1,
- Simp_tac 1,
- Auto_tac]);
+Goalw [conforms_def] "[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)";
+by Auto_tac;
+qed "conformsI";
Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
by( fast_tac (HOL_cs addDs [conforms_localD]
--- a/src/HOL/MicroJava/J/Decl.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Decl.ML Wed Dec 06 19:10:36 2000 +0100
@@ -4,12 +4,8 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
- rtac finite_map_of 1]);
+Goal "finite {C. is_class G C}";
+by (fold_goals_tac [dom_def]);
+by (rtac finite_dom_map_of 1);
+qed "finite_is_class";
-val is_classI = prove_goalw thy [is_class_def]
-"!!G. class G C = Some c ==> is_class G C" (K [Auto_tac]);
-
-val is_classD = prove_goalw thy [is_class_def]
-"!!G. is_class G C ==> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
- not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
--- a/src/HOL/MicroJava/J/Decl.thy Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Dec 06 19:10:36 2000 +0100
@@ -19,7 +19,7 @@
= "sig \\<times> ty \\<times> 'c"
types 'c class (* class *)
- = "cname option \\<times> fdecl list \\<times> 'c mdecl list"
+ = "cname \\<times> fdecl list \\<times> 'c mdecl list"
(* superclass, fields, methods*)
'c cdecl (* class declaration, cf. 8.1 *)
@@ -32,23 +32,33 @@
defs
- ObjectC_def "ObjectC == (Object, (None, [], []))"
+ ObjectC_def "ObjectC == (Object, (arbitrary, [], []))"
types 'c prog = "'c cdecl list"
+
+translations
+ "fdecl" <= (type) "vname \\<times> ty"
+ "sig" <= (type) "mname \\<times> ty list"
+ "mdecl c" <= (type) "sig \\<times> ty \\<times> c"
+ "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list"
+ "cdecl c" <= (type) "cname \\<times> (c class)"
+ "prog c" <= (type) "(c cdecl) list"
+
consts
class :: "'c prog => (cname \\<leadsto> 'c class)"
+ is_class :: "'c prog => cname => bool"
- is_class :: "'c prog => cname => bool"
- is_type :: "'c prog => ty => bool"
+translations
-defs
+ "class" => "map_of"
+ "is_class G C" == "class G C \\<noteq> None"
- class_def "class == map_of"
+consts
- is_class_def "is_class G C == class G C \\<noteq> None"
+ is_type :: "'c prog => ty => bool"
primrec
"is_type G (PrimT pt) = True"
--- a/src/HOL/MicroJava/J/Eval.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Eval.ML Wed Dec 06 19:10:36 2000 +0100
@@ -7,7 +7,7 @@
Goal "[|new_Addr (heap s) = (a,x); \
\ s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
\ G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
-by (hyp_subst_tac 1);
+by (Asm_simp_tac 1);
br eval_evals_exec.NewC 1;
by Auto_tac;
qed "NewCI";
@@ -21,27 +21,32 @@
by(ALLGOALS Asm_full_simp_tac);
qed "eval_evals_exec_no_xcpt";
-val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
- dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
- Fast_tac 1]);
-val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
- dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
- Fast_tac 1]);
+Goal "G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None";
+by (dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1);
+by (Fast_tac 1);
+qed "eval_no_xcpt";
-val eval_evals_exec_xcpt = prove_goal thy
+Goal "G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None";
+by (dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1);
+by (Fast_tac 1);
+qed "evals_no_xcpt";
+
+Goal
"!!s s'. (G\\<turnstile>(x,s) -e \\<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
\ (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
-\ (G\\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)"
- (K [
- split_all_tac 1,
- rtac eval_evals_exec.induct 1,
- rewtac c_hupd_def,
- ALLGOALS Asm_full_simp_tac]);
-val eval_xcpt = prove_goal thy
-"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and> s'=s" (K [
- dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
- Fast_tac 1]);
-val exec_xcpt = prove_goal thy
-"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and> s'=s" (K [
- dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
- Fast_tac 1]);
+\ (G\\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)";
+by (split_all_tac 1);
+by (rtac eval_evals_exec.induct 1);
+by (rewtac c_hupd_def);
+by (ALLGOALS Asm_full_simp_tac);
+qed "eval_evals_exec_xcpt";
+
+Goal "G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and> s'=s";
+by (dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1);
+by (Fast_tac 1);
+qed "eval_xcpt";
+
+Goal "G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and> s'=s";
+by (dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1);
+by (Fast_tac 1);
+qed "exec_xcpt";
\ No newline at end of file
--- a/src/HOL/MicroJava/J/Example.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Example.ML Wed Dec 06 19:10:36 2000 +0100
@@ -1,35 +1,37 @@
-
-AddIs [widen.null];
Addsimps [inj_cnam_, inj_vnam_];
Addsimps [Base_not_Object,Ext_not_Object];
Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];
-val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"]
-"map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]);
-val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"]
-"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
-val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"]
-"!!X. x\\<noteq>k ==> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
+bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps")));
+Goal "map_of ((aa,bb)#ps) aa = Some bb";
+by (Simp_tac 1);
+qed "map_of_Cons1";
+Goal "aa\\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa";
+by (Asm_simp_tac 1);
+qed "map_of_Cons2";
Delsimps[map_of_Cons]; (* sic! *)
Addsimps[map_of_Cons1, map_of_Cons2];
-val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def]
- "class tprg Object = Some (None, [], [])"
- (K [Simp_tac 1]);
-val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def,
- ExtC_def] "class tprg Base = Some (Some Object, \
+Goalw [ObjectC_def] "class tprg Object = Some (arbitrary, [], [])";
+by (Simp_tac 1);
+qed "class_tprg_Object";
+
+Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Base = Some (Object, \
\ [(vee, PrimT Boolean)], \
- \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [
- Simp_tac 1]);
-val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def,
- ExtC_def] "class tprg Ext = Some (Some Base, \
+ \ [((foo, [Class Base]), Class Base, foo_Base)])";
+by (Simp_tac 1);
+qed "class_tprg_Base";
+
+Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Ext = Some (Base, \
\ [(vee, PrimT Integer)], \
- \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [
- Simp_tac 1]);
+ \ [((foo, [Class Base]), Class Ext, foo_Ext)])";
+by (Simp_tac 1);
+qed "class_tprg_Ext";
+
Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
-Goal "!!X. (Object,C) \\<in> (subcls1 tprg)^+ ==> R";
+Goal "(Object,C) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
qed "not_Object_subcls";
AddSEs [not_Object_subcls];
@@ -42,13 +44,13 @@
qed "subcls_ObjectD";
AddSDs[subcls_ObjectD];
-Goal "!!X. (Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
+Goal "(Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
qed "not_Base_subcls_Ext";
AddSEs [not_Base_subcls_Ext];
-Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
-by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
+Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
+by (auto_tac (claset(),simpset()addsplits[split_if_asm]addsimps[map_of_Cons]));
qed "class_tprgD";
Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
@@ -66,13 +68,13 @@
bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
-Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base";
+Goal "tprg\\<turnstile>Ext\\<preceq>C Base";
br subcls_direct 1;
-by (Simp_tac 1);
+by Auto_tac;
qed "Ext_subcls_Base";
Addsimps [Ext_subcls_Base];
-Goalw [] "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
+Goal "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
br widen.subcls 1;
by (Simp_tac 1);
qed "Ext_widen_Base";
@@ -89,8 +91,6 @@
val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
-Addsimps[is_class_def];
-
val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
Goal "fields (tprg, Object) = []";
--- a/src/HOL/MicroJava/J/Example.thy Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Wed Dec 06 19:10:36 2000 +0100
@@ -75,13 +75,13 @@
defs
foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
- BaseC_def "BaseC == (Base, (Some Object,
+ BaseC_def "BaseC == (Base, (Object,
[(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)"
- ExtC_def "ExtC == (Ext, (Some Base ,
+ ExtC_def "ExtC == (Ext, (Base ,
[(vee, PrimT Integer)],
[((foo,[Class Base]),Class Ext,foo_Ext)]))"
--- a/src/HOL/MicroJava/J/JBasis.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML Wed Dec 06 19:10:36 2000 +0100
@@ -4,92 +4,21 @@
Copyright 1999 TU Muenchen
*)
-val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
-
-Goalw [image_def]
- "x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and> x = f y";
-by(Auto_tac);
-qed "image_rev";
-
-fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
-
-val select_split = prove_goalw Product_Type.thy [split_def]
- "(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
-
-
-val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
- (fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
-val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
- (fn _ => [Auto_tac]);
-val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
- REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
- rtac (split_beta RS subst) 1,
- rtac (hd prems) 1]);
-val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
- REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
- res_inst_tac [("P1","P")] (split_beta RS subst) 1,
- rtac (hd prems) 1]);
-
-
-fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
-
-val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
- (fn prems => [rtac ballE 1, resolve_tac prems 1,
- eresolve_tac prems 1, eresolve_tac prems 1]);
-
-val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
+(*###TO Product_Type*)
+Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
+by (rtac refl 1);
+qed "select_split";
Addsimps [Let_def];
-(* To HOL.ML *)
-
-val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y"
- (fn prems => [
- cut_facts_tac prems 1,
- rtac some_equality 1,
- atac 1,
- etac ex1E 1,
- etac all_dupE 1,
- fast_tac HOL_cs 1]);
-
-
-val ball_insert = prove_goalw equalities.thy [Ball_def]
- "Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
- fast_tac set_cs 1]);
-
-fun option_case_tac i = EVERY [
- etac option_caseE i,
- rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
- rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i];
-
-val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
- rotate_tac ~1,asm_full_simp_tac
- (simpset() delsimps [split_paired_All,split_paired_Ex])];
-
-Goal "{y. x = Some y} \\<subseteq> {the x}";
-by Auto_tac;
-qed "some_subset_the";
-
-fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
- asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
-
-val optionE = prove_goal thy
- "[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P"
- (fn prems => [
- case_tac "opt = None" 1,
- eresolve_tac prems 1,
- not_None_tac 1,
- eresolve_tac prems 1]);
-
-fun option_case_tac2 s i = EVERY [
- case_tac s i,
- rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
- rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
-
-val option_map_SomeD = prove_goalw thy [option_map_def]
- "!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
- option_case_tac2 "x" 1,
- Auto_tac]);
+(* ### To HOL.ML *)
+Goal "[| ?!x. P x; P y |] ==> Eps P = y";
+by (rtac some_equality 1);
+by (atac 1);
+by (etac ex1E 1);
+by (etac all_dupE 1);
+by (fast_tac HOL_cs 1);
+qed "ex1_some_eq_trivial";
section "unique";
@@ -103,7 +32,7 @@
by (Simp_tac 1);
qed "unique_Nil";
-Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
+Goalw [unique_def] "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))";
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
qed "unique_Cons";
@@ -120,47 +49,14 @@
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
qed_spec_mp "unique_map_inj";
-Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
-by(etac unique_map_inj 1);
-by(rtac injI 1);
-by Auto_tac;
-qed "unique_map_Pair";
-
-Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
-by(rtac set_ext 1);
-by(simp_tac (simpset() addsimps image_def::premises()) 1);
-qed "image_cong";
-
-val split_Pair_eq = prove_goal Product_Type.thy
-"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
- etac imageE 1,
- split_all_tac 1,
- auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
-
-
(* More about Maps *)
-val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \
-\ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [
- cut_facts_tac prems 1,
- case_tac "\\<exists>x. t k = Some x" 1,
- etac exE 1,
- rotate_tac ~1 1,
- Asm_full_simp_tac 1,
- asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
- rotate_tac ~1 1,
- Asm_full_simp_tac 1]);
+(*###Addsimps [fun_upd_same, fun_upd_other];*)
-Addsimps [fun_upd_same, fun_upd_other];
-
-Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
-by(induct_tac "xys" 1);
- by(Simp_tac 1);
-by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
-qed_spec_mp "unique_map_of_Some_conv";
-
-val in_set_get = unique_map_of_Some_conv RS iffD2;
-val get_in_set = unique_map_of_Some_conv RS iffD1;
+Goal "unique l --> (k, x) : set l --> map_of l k = Some x";
+by (induct_tac "l" 1);
+by Auto_tac;
+qed_spec_mp "map_of_SomeI";
Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
by(induct_tac "l" 1);
@@ -169,50 +65,14 @@
by Auto_tac;
bind_thm("Ball_set_table",result() RS mp);
-val table_mono = prove_goal thy
-"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
-\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
- induct_tac "l" 1,
- Auto_tac,
- fast_tac (HOL_cs addSIs [in_set_get]) 1])
- RS mp RS mp RS spec RS spec RS mp;
-
-val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
-\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
- induct_tac "t" 1,
- ALLGOALS Simp_tac,
- case_tac1 "k = fst a" 1,
- Auto_tac]) RS mp;
-val table_map_Some = prove_goal thy
-"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
-\map_of t (k, k') = Some x" (K [
- induct_tac "t" 1,
- Auto_tac]) RS mp;
-
+Goal "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
+\map_of t (k, k') = Some x";
+by (induct_tac "t" 1);
+by Auto_tac;
+qed_spec_mp "table_of_remap_SomeD";
-val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
-\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
- induct_tac "t" 1,
- Auto_tac]) RS mp;
-val table_mapf_SomeD = prove_goal thy
-"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [
- induct_tac "t" 1,
- Auto_tac]) RS mp;
-
-val table_mapf_Some2 = prove_goal thy
-"!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
- forward_tac [table_mapf_SomeD] 1,
- Auto_tac,
- rtac table_mapf_Some 1,
- atac 2,
- Fast_tac 1]);
-
-val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
-
-Goal
-"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
+(* ### To Map.ML *)
+Goal "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
by (induct_tac "xs" 1);
-auto();
+by Auto_tac;
qed "map_of_map";
-
-
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Wed Dec 06 19:10:36 2000 +0100
@@ -7,29 +7,29 @@
*)
+
Addsimps [split_beta];
Goal "[|h a = None; (h, l)::\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> \
\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)::\\<preceq>(G, lT)";
by( etac conforms_upd_obj 1);
by( rewtac oconf_def);
-by( auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset()));
+by( auto_tac (claset() addSDs [fields_is_type], simpset()));
qed "NewC_conforms";
-
+
Goalw [cast_ok_def]
"[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
\ ==> G,h\\<turnstile>v::\\<preceq>Class D";
-by( case_tac1 "v = Null" 1);
+by( case_tac "v = Null" 1);
by( Asm_full_simp_tac 1);
by( dtac widen_RefT 1);
by( Clarify_tac 1);
-by( rtac widen.null 1);
by( datac non_npD 1 1);
by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
qed "Cast_conf";
Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\\<preceq>(G,lT); \
-\ x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
+\ x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\\<preceq>ft";
by( dtac np_NoneD 1);
by( etac conjE 1);
@@ -38,11 +38,8 @@
by Auto_tac;
by( dtac (conforms_heapD RS hconfD) 1);
by( atac 1);
-by( dtac widen_cfs_fields 1);
-by( atac 1);
-by( atac 1);
-by( dtac oconf_objD 1);
-by( atac 1);
+by( datac widen_cfs_fields 2 1);
+by( datac oconf_objD 1 1);
by Auto_tac;
qed "FAcc_type_sound";
@@ -62,12 +59,12 @@
by( dtac non_np_objD 1);
by( atac 1);
by( SELECT_GOAL Auto_tac 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
by( Full_simp_tac 1);
by( EVERY [forward_tac [hext_objD] 1, atac 1]);
by( etac exE 1);
by( Asm_full_simp_tac 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
by( rtac conjI 1);
by( fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
by( rtac conjI 1);
@@ -85,7 +82,7 @@
by( rtac (oconf_obj RS iffD2) 1);
by( Simp_tac 1);
by( strip_tac 1);
-by( case_tac1 "(aaa, b) = (fn, fd)" 1);
+by( case_tac "(aaa, b) = (fn, fd)" 1);
by( Asm_full_simp_tac 1);
by( fast_tac (HOL_cs addIs [conf_widen]) 1);
by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
@@ -105,8 +102,14 @@
by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
qed "Call_lemma2";
+Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
+by (etac rtrancl_induct 1);
+by (dtac subcls1D 2);
+by Auto_tac;
+qed_spec_mp "subcls_is_class2";
+
Goalw [wf_java_prog_def]
- "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); \
+ "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); class G C = Some y; \
\ max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
\ list_all2 (conf G h) pvs pTsa;\
\ (md, rT, pns, lvars, blk, res) = \
@@ -117,16 +120,14 @@
\ xi\\<le>|h' \\<and> (h', xj)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>T)); \
\ G,xh\\<turnstile>a'::\\<preceq> Class C |] ==> \
\ xc\\<le>|h' \\<and> (h', l)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>rTa)";
-by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
-by( dtac (max_spec2appl_meths RS appl_methsD) 1);
+by( dtac max_spec2mheads 1);
by( Clarify_tac 1);
by( datac non_np_objD' 2 1);
-by( strip_tac1 1);
-by( Asm_full_simp_tac 1);
+by( Clarsimp_tac 1);
by( Clarsimp_tac 1);
by( EVERY'[forward_tac [hext_objD], atac] 1);
by( Clarsimp_tac 1);
-by( EVERY'[dtac Call_lemma, atac, atac] 1);
+by( datac Call_lemma 3 1);
by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1);
by( thin_tac "method ?sig ?x = ?y" 1);
by( EVERY'[dtac spec, etac impE] 1);
@@ -142,7 +143,7 @@
(*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
by( EVERY'[dtac spec, mp_tac] 1);
by( thin_tac "?E\\<turnstile>res::?rT" 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
by( rtac conjI 1);
by( fast_tac (HOL_cs addIs [hext_trans]) 1);
by( rtac conjI 1);
@@ -163,7 +164,8 @@
Unify.search_bound := 40;
Unify.trace_bound := 40;
Delsplits[split_if];
-Delsimps[fun_upd_apply];(*###*)
+Delsimps[fun_upd_apply];
+Addsimps[fun_upd_same];
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
Goal
@@ -194,10 +196,9 @@
by( dtac new_AddrD 1);
by( etac disjE 1);
by( Asm_simp_tac 2);
-by( etac conjE 1);
-by( Asm_simp_tac 1);
+by( Clarsimp_tac 1);
by( rtac conjI 1);
-by( fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
+by( force_tac (claset() addSEs [NewC_conforms],simpset()) 1);
by( rtac conf_obj_AddrI 1);
by( rtac rtrancl_refl 2);
by( Simp_tac 1);
@@ -228,7 +229,7 @@
REPEAT o (etac conjE), hyp_subst_tac] 3);
(* for if *)
-by( (case_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
+by( (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
by forward_hyp_tac;
@@ -266,7 +267,7 @@
by( fast_tac (claset() addIs [hext_trans]) 3);
(* 2 FAss *)
-by( case_tac1 "x2 = None" 1);
+by( case_tac "x2 = None" 1);
by( Asm_simp_tac 2);
by( fast_tac (claset() addIs [hext_trans]) 2);
by( Asm_full_simp_tac 1);
@@ -274,7 +275,7 @@
by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
by prune_params_tac;
-(* Level 51 *)
+(* Level 50 *)
(* 1 Call *)
by( case_tac "x" 1);
@@ -287,14 +288,16 @@
by( Clarify_tac 1);
by( dtac evals_no_xcpt 1);
by( Asm_full_simp_tac 1);
-by( case_tac1 "a' = Null" 1);
+by( case_tac "a' = Null" 1);
by( Asm_full_simp_tac 1);
by( dtac exec_xcpt 1);
by( Asm_full_simp_tac 1);
by( dtac eval_xcpt 1);
by( Asm_full_simp_tac 1);
by( fast_tac (HOL_cs addEs [hext_trans]) 1);
-by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound)
+by( datac ty_expr_is_type 1 1);
+by(Clarsimp_tac 1);
+by( (rtac (rewrite_rule [wf_java_prog_def] Call_type_sound)
THEN_ALL_NEW Asm_simp_tac) 1);
qed "eval_evals_exec_type_sound";
@@ -318,18 +321,15 @@
\ s::\\<preceq>E; E\\<turnstile>e::Class C; method (G,C) sig \\<noteq> None|] ==> \
\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
by( datac eval_type_sound 4 1);
-by( not_None_tac 1);
-by( split_all_tac 1);
+by(Clarsimp_tac 1);
by(rewtac wf_java_prog_def);
by( forward_tac [widen_methd] 1);
by( atac 1);
-by( rtac (not_None_eq RS iffD1) 2);
by( Fast_tac 2);
-by( etac conjE 1);
by( dtac non_npD 1);
by Auto_tac;
qed "all_methods_understood";
Delsimps [split_beta];
-Addsimps[fun_upd_apply];(*###*)
+Addsimps[fun_upd_apply];
--- a/src/HOL/MicroJava/J/State.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/State.ML Wed Dec 06 19:10:36 2000 +0100
@@ -4,65 +4,69 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C"
- (K [Simp_tac 1]);
-
+Goalw [obj_ty_def] "obj_ty (C,fs) = Class C";
+by (Simp_tac 1);
+qed "obj_ty_def2";
Addsimps [obj_ty_def2];
-val new_AddrD = prove_goalw thy [new_Addr_def]
-"!!X. (a,x) = new_Addr h ==> h a = None \\<and> x = None | x = Some OutOfMemory" (K[
- asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
- rtac someI 1,
- rtac disjI2 1,
- res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
- Auto_tac ]);
-
-val raise_if_True = prove_goalw thy [raise_if_def]
- "raise_if True x y \\<noteq> None"
-(K [split_tac [split_if] 1,Auto_tac]);
-
-val raise_if_False = prove_goalw thy [raise_if_def]
- "raise_if False x y = y"
-(K [Auto_tac]);
-
-val raise_if_Some = prove_goalw thy [raise_if_def]
- "raise_if c x (Some y) \\<noteq> None" (K [Auto_tac]);
-
-val raise_if_Some2 = prove_goalw thy [raise_if_def]
-"raise_if c z (if x = None then Some y else x) \\<noteq> None" (K[
- induct_tac "x" 1,
- Auto_tac]);
-val if_None_eq = prove_goal thy
-"(if x = None then None else x) = x" (K[
- induct_tac "x" 1,
- Auto_tac]);
-
-Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
-
-val raise_if_SomeD = prove_goalw thy [raise_if_def]
- "raise_if c x y = Some z --> c \\<and> Some z = Some x | y = Some z"
-(K [split_tac [split_if] 1,Auto_tac]) RS mp;
-
-val raise_if_NoneD = prove_goalw thy [raise_if_def]
- "raise_if c x y = None --> \\<not> c \\<and> y = None"
-(K [split_tac [split_if] 1,Auto_tac]) RS mp;
+Goalw [new_Addr_def]
+"(a,x) = new_Addr h ==> h a = None \\<and> x = None | x = Some OutOfMemory";
+by(asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1);
+by(rtac someI 1);
+by(rtac disjI2 1);
+by(res_inst_tac [("r","snd (?a,Some OutOfMemory)")] trans 1);
+by Auto_tac;
+qed "new_AddrD";
-val np_NoneD = (prove_goalw thy [np_def, raise_if_def]
- "np a' x' = None --> x' = None \\<and> a' \\<noteq> Null" (fn _ => [
- split_tac [split_if] 1,
- Auto_tac ])) RS mp;
-val np_None = (prove_goalw thy [np_def, raise_if_def]
- "a' \\<noteq> Null --> np a' x' = x'" (fn _ => [
- split_tac [split_if] 1,
- Auto_tac ])) RS mp;
-val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
- (fn _ => [Auto_tac ]);
-val np_Null = prove_goalw thy [np_def, raise_if_def]
- "np Null None = Some NullPointer" (fn _ => [
- Auto_tac ]);
-val np_Addr = prove_goalw thy [np_def, raise_if_def] "np (Addr a) None = None"
- (fn _ => [Auto_tac ]);
+Goalw [raise_if_def] "raise_if True x y \\<noteq> None";
+by Auto_tac;
+qed "raise_if_True";
+
+Goalw [raise_if_def] "raise_if False x y = y";
+by Auto_tac;
+qed "raise_if_False";
+
+Goalw [raise_if_def] "raise_if c x (Some y) \\<noteq> None";
+by Auto_tac;
+qed "raise_if_Some";
+
+Goalw [raise_if_def] "raise_if c z (if x = None then Some y else x) \\<noteq> None";
+by(induct_tac "x" 1);
+by Auto_tac;
+qed "raise_if_Some2";
+
+Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2];
+
+Goalw [raise_if_def]
+ "raise_if c x y = Some z \\<longrightarrow> c \\<and> Some z = Some x | y = Some z";
+by Auto_tac;
+qed_spec_mp "raise_if_SomeD";
+
+Goalw [raise_if_def] "raise_if c x y = None --> \\<not> c \\<and> y = None";
+by Auto_tac;
+qed_spec_mp "raise_if_NoneD";
+
+Goalw [np_def, raise_if_def] "np a' x' = None --> x' = None \\<and> a' \\<noteq> Null";
+by Auto_tac;
+qed_spec_mp "np_NoneD";
+
+Goalw [np_def, raise_if_def] "a' \\<noteq> Null --> np a' x' = x'";
+by Auto_tac;
+qed_spec_mp "np_None";
+
+Goalw [np_def, raise_if_def] "np a' (Some xc) = Some xc";
+by Auto_tac;
+qed "np_Some";
+
+Goalw [np_def, raise_if_def] "np Null None = Some NullPointer";
+by Auto_tac;
+qed "np_Null";
+
+Goalw [np_def, raise_if_def] "np (Addr a) None = None";
+by Auto_tac;
+qed "np_Addr";
+
Addsimps[np_None, np_Some,np_Null,np_Addr];
Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
--- a/src/HOL/MicroJava/J/TypeRel.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML Wed Dec 06 19:10:36 2000 +0100
@@ -4,44 +4,43 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val subcls1D = prove_goalw thy [subcls1_def] "!!G. G\\<turnstile>C\\<prec>C1D ==> \
-\ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
+Goalw [subcls1_def]
+ "G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> C \\<noteq> Object \\<and> (\\<exists>fs ms. class G C = Some (D,fs,ms))";
+by Auto_tac;
+qed "subcls1D";
+Goalw [subcls1_def] "\\<lbrakk>class G C = Some (D,rest); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D";
+by Auto_tac;
+qed "subcls1I";
-val subcls1I = prove_goalw thy [subcls1_def]
-"!!G. [| class G C = Some (Some D,rest) |] ==> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
-
-val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def] "subcls1 G = \
-\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
- (K [Auto_tac]);
+Goalw [subcls1_def]
+"subcls1 G = (\\<Sigma>C\\<in>{C. is_class G C} . {D. C\\<noteq>Object \\<and> fst (the (class G C))=D})";
+by Auto_tac;
+qed "subcls1_def2";
Goal "finite (subcls1 G)";
by(stac subcls1_def2 1);
-by( rtac finite_SigmaI 1);
-by( rtac finite_is_class 1);
-by( rtac finite_subset 1);
-by( rtac some_subset_the 1);
-by( Simp_tac 1);
+by( rtac (finite_is_class RS finite_SigmaI) 1);
+by(res_inst_tac [("B","{fst (the (class G C))}")] finite_subset 1);
+by Auto_tac;
qed "finite_subcls1";
-fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [
- rtac (hd prems RS indrule) 1,
- auto_tac (claset() addDs drules, simpset())]);
-fun prove_typerel s lemmata = prove_goal thy s (fn prems => [
- cut_facts_tac prems 1,
- auto_tac (claset() addDs lemmata, simpset())]);
-
-
-Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
+Goal "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
by(etac trancl_trans_induct 1);
by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
qed "subcls_is_class";
+Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
+by (etac rtrancl_induct 1);
+by (dtac subcls1D 2);
+by Auto_tac;
+qed_spec_mp "subcls_is_class2";
+
(* A particular thm about wf;
looks like it is an odd instance of something more general
*)
Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}";
-by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
+by(full_simp_tac (simpset() delcongs [imp_cong]) 1);
by(strip_tac 1);
by(rename_tac "A x" 1);
by(case_tac "wf(R A)" 1);
@@ -68,30 +67,48 @@
(cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs)))))
(K [auto_tac (claset() addIs [subcls1I], simpset())]);
+Goalw [field_def]
+"field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT";
+by (rtac table_of_remap_SomeD 1);
+by (Asm_full_simp_tac 1);
+qed "field_fields";
-AddSIs [widen.refl];
+AddSIs [widen.refl,widen.null];
Addsimps [widen.refl];
-val prove_widen_lemma = prove_typerel_lemma [] widen.elim;
-
Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False";
br iffI 1;
be widen.elim 1;
-by(Auto_tac);
+by Auto_tac;
qed "widen_PrimT_RefT";
AddIffs [widen_PrimT_RefT];
-val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t"
- [prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)"];
-bind_thm ("widen_RefT", widen_RefT);
+Goal "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)";
+by (etac widen.elim 1);
+by Auto_tac;
+qed "widen_RefT_lemma";
+Goal "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t";
+by (dtac widen_RefT_lemma 1);
+by Auto_tac;
+qed "widen_RefT";
-val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t"
- [prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)"];
-bind_thm ("widen_RefT2", widen_RefT2);
+Goal "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)";
+by (etac widen.elim 1);
+by Auto_tac;
+qed "widen_RefT2_lemma";
+Goal "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t";
+by (dtac widen_RefT2_lemma 1);
+by Auto_tac;
+qed "widen_RefT2";
-val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)"];
-bind_thm ("widen_Class", widen_Class);
+Goal "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)";
+by (etac widen.elim 1);
+by Auto_tac;
+qed "widen_Class_lemma";
+Goal "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D";
+by (dtac widen_Class_lemma 1);
+by Auto_tac;
+qed "widen_Class";
Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False";
br iffI 1;
@@ -113,6 +130,5 @@
by Safe_tac;
by( ALLGOALS (forward_tac [widen_Class, widen_RefT]));
by Safe_tac;
-by( rtac widen.null 2);
by(eatac rtrancl_trans 1 1);
qed_spec_mp "widen_trans";
--- a/src/HOL/MicroJava/J/TypeRel.thy Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Wed Dec 06 19:10:36 2000 +0100
@@ -34,7 +34,7 @@
defs
(* direct subclass, cf. 8.1.3 *)
- subcls1_def "subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
+ subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
consts
@@ -42,15 +42,15 @@
field :: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
fields :: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times> ty) list"
-constdefs (* auxiliary relations for recursive definitions below *)
+constdefs (* auxiliary relation for recursive definitions below *)
subcls1_rel :: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
"subcls1_rel == {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
recdef method "subcls1_rel"
- "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
- | Some (sc,fs,ms) => (case sc of None => empty | Some D =>
+ "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
+ | Some (D,fs,ms) => (if C = Object then empty else
if is_class G D then method (G,D)
else arbitrary) ++
map_of (map (\\<lambda>(s, m ).
@@ -59,9 +59,9 @@
(* list of fields of a class, including inherited and hidden ones *)
recdef fields "subcls1_rel"
- "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
- | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
- (case sc of None => [] | Some D =>
+ "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
+ | Some (D,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
+ (if C = Object then [] else
if is_class G D then fields (G,D)
else arbitrary))
else arbitrary)"
--- a/src/HOL/MicroJava/J/WellForm.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML Wed Dec 06 19:10:36 2000 +0100
@@ -4,58 +4,59 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
- "!!X. [|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" (K [
- Asm_full_simp_tac 1,
- fast_tac (set_cs addDs [get_in_set]) 1]);
+Goalw [wf_prog_def]
+ "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)";
+by (Asm_full_simp_tac 1);
+by (fast_tac (set_cs addDs [map_of_SomeD]) 1);
+qed "class_wf";
-val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
- "!!X. wf_prog wf_mb G ==> class G Object = Some (None, [], [])" (K [
- safe_tac set_cs,
- dtac in_set_get 1,
- Auto_tac]);
+Goalw [wf_prog_def, ObjectC_def]
+ "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])";
+by (auto_tac (claset() addIs [map_of_SomeI], simpset()));
+qed "class_Object";
Addsimps [class_Object];
-val is_class_Object = prove_goalw thy [is_class_def]
- "!!X. wf_prog wf_mb G ==> is_class G Object" (K [Asm_simp_tac 1]);
+Goal "wf_prog wf_mb G ==> is_class G Object";
+by (Asm_simp_tac 1);
+qed "is_class_Object";
Addsimps [is_class_Object];
Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
by( forward_tac [r_into_trancl] 1);
by( dtac subcls1D 1);
-by( strip_tac1 1);
+by(Clarify_tac 1);
by( datac class_wf 1 1);
by( rewtac wf_cdecl_def);
by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym]
delsimps [reflcl_trancl]) 1);
qed "subcls1_wfD";
-val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
-"!!X. [|wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object|] ==> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
- pair_tac "r" 1,
- asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
+Goalw [wf_cdecl_def]
+"!!r. \\<lbrakk>wf_cdecl wf_mb G (C,D,r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> is_class G D";
+by (auto_tac (claset(), simpset() addsplits [option.split_asm]));
+qed "wf_cdecl_supD";
Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
by(etac tranclE 1);
-by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
+by(TRYALL(fast_tac (claset() addSDs [subcls1_wfD] addIs [trancl_trans])));
qed "subcls_asym";
-val subcls_irrefl = prove_goal thy "!!X. [|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D" (K [
- etac trancl_trans_induct 1,
- fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
- fast_tac (HOL_cs addDs [subcls_asym]) 1]);
+Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D";
+by (etac trancl_trans_induct 1);
+by (auto_tac (claset() addDs [subcls1_wfD,subcls_asym],simpset()));
+qed "subcls_irrefl";
-val acyclic_subcls1 = prove_goalw thy [acyclic_def]
- "!!X. wf_prog wf_mb G ==> acyclic (subcls1 G)" (K [
- strip_tac1 1,
- fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
+Goalw [acyclic_def] "wf_prog wf_mb G ==> acyclic (subcls1 G)";
+by (fast_tac (claset() addDs [subcls_irrefl]) 1);
+qed "acyclic_subcls1";
-val wf_subcls1 = prove_goal thy "!!X. wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" (K [
- rtac finite_acyclic_wf 1,
- stac finite_converse 1,
- rtac finite_subcls1 1,
- stac acyclic_converse 1,
- etac acyclic_subcls1 1]);
+Goal "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)";
+by (rtac finite_acyclic_wf 1);
+by ( stac finite_converse 1);
+by ( rtac finite_subcls1 1);
+by (stac acyclic_converse 1);
+by (etac acyclic_subcls1 1);
+qed "wf_subcls1";
val major::prems = goal thy
"[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
@@ -68,8 +69,8 @@
qed "subcls_induct";
val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
-\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
-\ wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
+\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \\<and> \
+\ wf_cdecl wf_mb G (C,D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
\ |] ==> P C";
by( cut_facts_tac prems 1);
by( rtac impE 1);
@@ -81,32 +82,30 @@
by( rtac impI 1);
by( case_tac "C = Object" 1);
by( Fast_tac 1);
-by( ex_ftac is_classD 1);
+by Safe_tac;
by( forward_tac [class_wf] 1);
by( atac 1);
by( forward_tac [wf_cdecl_supD] 1);
by( atac 1);
-by( strip_tac1 1);
+
+by( subgoal_tac "G\\<turnstile>C\\<prec>C1a" 1);
+by( etac subcls1I 2);
by( rtac (hd (tl (tl (tl prems)))) 1);
-by( atac 1);
-by( atac 1);
-by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
-by( fast_tac (HOL_cs addIs [r_into_trancl]) 1);
-by( etac subcls1I 1);
+by Auto_tac;
qed "subcls1_induct";
-Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
-\ (case class G C of None => empty | Some (sc,fs,ms) => \
-\ (case sc of None => empty | Some D => method (G,D)) ++ \
+Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (D,fs,ms) \\<longrightarrow> C \\<noteq> Object --> is_class G D|] ==> method (G,C) = \
+\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
+\ (if C = Object then empty else method (G,D)) ++ \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
by( asm_simp_tac (simpset() addsplits[option.split]) 1);
-auto();
+by Auto_tac;
qed "method_rec_lemma";
Goal "wf_prog wf_mb G ==> method (G,C) = \
-\ (case class G C of None => empty | Some (sc,fs,ms) => \
-\ (case sc of None => empty | Some D => method (G,D)) ++ \
+\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
+\ (if C = Object then empty else method (G,D)) ++ \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by(rtac method_rec_lemma 1);
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
@@ -119,36 +118,40 @@
by( Asm_full_simp_tac 1);
qed "method_rec";
-Goal "[|wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C --> is_class G C|] ==> fields (G,C) = \
-\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None => [] | Some D => fields (G,D))";
-by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
+Goal "[|wf ((subcls1 G)^-1); class G C = Some (D,fs,ms); C \\<noteq> Object \\<longrightarrow> is_class G D|] ==> fields (G,C) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
+by(rtac trans 1);
+by(rtac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
by( asm_simp_tac (simpset() addsplits[option.split]) 1);
qed "fields_rec_lemma";
-Goal "[|class G C = Some (sc,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
-\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None => [] | Some D => fields (G,D))";
+Goal "[|class G C = Some (D,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
+by(rtac trans 1);
by(rtac fields_rec_lemma 1);
-by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+by( asm_simp_tac (simpset() addsimps [wf_subcls1]) 1);
ba 1;
-by( option_case_tac2 "sc" 1);
-by( Asm_simp_tac 1);
-by( case_tac "C = Object" 1);
-by( rotate_tac 2 1);
-by( Asm_full_simp_tac 1);
+br refl 2;
by( datac class_wf 1 1);
-by( datac wf_cdecl_supD 1 1);
-by( Asm_full_simp_tac 1);
+by(rtac impI 1);
+by( eatac wf_cdecl_supD 1 1);
qed "fields_rec";
-val method_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> method (G,Object) = empty"
- (K [stac method_rec 1,Auto_tac]);
-val fields_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> fields (G,Object) = []"(K [
- stac fields_rec 1,Auto_tac]);
+Goal "wf_prog wf_mb G ==> method (G,Object) = empty";
+by(stac method_rec 1);
+by Auto_tac;
+qed "method_Object";
+
+Goal "wf_prog wf_mb G ==> fields (G,Object) = []";
+by(stac fields_rec 1);
+by Auto_tac;
+qed "fields_Object";
+
Addsimps [method_Object, fields_Object];
-val field_Object = prove_goalw thy [field_def]
- "!!X. wf_prog wf_mb G ==> field (G,Object) = empty" (K [Asm_simp_tac 1]);
+
+Goalw [field_def] "wf_prog wf_mb G ==> field (G,Object) = empty";
+by(Asm_simp_tac 1);
+qed "field_Object";
Addsimps [field_Object];
Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
@@ -159,17 +162,9 @@
by(eatac rtrancl_into_rtrancl2 1 1);
qed "subcls_C_Object";
-val is_type_rTI = prove_goalw thy [wf_mhead_def]
- "!!sig. wf_mhead G sig rT ==> is_type G rT"
- (K [split_all_tac 1, Auto_tac]);
-
-Goal "[|(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G|] ==> \
-\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
-by(etac trancl_trans_induct 1);
-by( safe_tac (HOL_cs addSDs [subcls1D]));
-by(stac fields_rec 1);
-by( Auto_tac);
-qed_spec_mp "fields_mono";
+Goalw [wf_mhead_def] "wf_mhead G sig rT ==> is_type G rT";
+by Auto_tac;
+qed "is_type_rTI";
Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
@@ -180,28 +175,22 @@
by( stac fields_rec 1);
by( atac 1);
by( atac 1);
-by( Simp_tac 1);
+by( simp_tac (simpset() delsplits [split_if]) 1);
by( rtac ballI 1);
by( split_all_tac 1);
by( Simp_tac 1);
by( etac UnE 1);
-by( dtac split_Pair_eq 1);
-by( SELECT_GOAL (Auto_tac) 1);
+by( Force_tac 1);
by( etac (r_into_rtrancl RS rtrancl_trans) 1);
-by( etac BallE 1);
-by( contr_tac 1);
-by( Asm_full_simp_tac 1);
+by Auto_tac;
qed "widen_fields_defpl'";
-Goal "[|is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))|] ==> \
+Goal "[|((fn,fd),fT) \\<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> \
\ G\\<turnstile>C\\<preceq>C fd";
by( datac widen_fields_defpl' 1 1);
-(*###################*)
-by( dtac bspec 1);
-auto();
+by (Fast_tac 1);
qed "widen_fields_defpl";
-
Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
by( etac subcls1_induct 1);
by( atac 1);
@@ -212,54 +201,53 @@
by( stac fields_rec 1);
by Auto_tac;
by( rotate_tac ~1 1);
-by( ex_ftac is_classD 1);
by( forward_tac [class_wf] 1);
by Auto_tac;
by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
by( etac unique_append 1);
-by( rtac unique_map_Pair 1);
-by( Step_tac 1);
-by (EVERY1[dtac widen_fields_defpl, atac, atac]);
-by( Asm_full_simp_tac 1);
-by( dtac split_Pair_eq 1);
-by( Asm_full_simp_tac 1);
+by( rtac unique_map_inj 1);
+by( Clarsimp_tac 1);
+by (rtac injI 1);
+by( Asm_full_simp_tac 1);
+by(auto_tac (claset() addSDs [widen_fields_defpl], simpset()));
qed "unique_fields";
+Goal "[|wf_prog wf_mb G; (C',C)\\<in>(subcls1 G)^*|] ==> \
+\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
+by(etac converse_rtrancl_induct 1);
+by( safe_tac (HOL_cs addSDs [subcls1D]));
+by(stac fields_rec 1);
+by( Auto_tac);
+qed_spec_mp "fields_mono_lemma";
+
Goal
-"[|wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft|] ==> \
-\ map_of (fields (G,C')) f = Some ft";
-by( dtac rtranclD 1);
-by( Auto_tac);
-by( rtac table_mono 1);
-by( atac 3);
-by( rtac unique_fields 1);
-by( etac subcls_is_class 1);
-by( atac 1);
-by( fast_tac (HOL_cs addEs [fields_mono]) 1);
-qed "widen_fields_mono";
-
+"\\<lbrakk>map_of (fields (G,C)) fn = Some f; G\\<turnstile>D\\<preceq>C C; is_class G D; wf_prog wf_mb G\\<rbrakk>\
+\ \\<Longrightarrow> map_of (fields (G,D)) fn = Some f";
+by (rtac map_of_SomeI 1);
+by (eatac unique_fields 1 1);
+by (eatac fields_mono_lemma 1 1);
+by (etac map_of_SomeD 1);
+qed "fields_mono";
-val cfs_fields_lemma = prove_goalw thy [field_def]
-"!!X. field (G,C) fn = Some (fd, fT) ==> map_of(fields (G,C)) (fn, fd) = Some fT"
-(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
+Goal
+"[|field (G,C) fn = Some (fd, fT); G\\<turnstile>D\\<preceq>C C; wf_prog wf_mb G|]==> \
+\ map_of (fields (G,D)) (fn, fd) = Some fT";
+by (dtac field_fields 1);
+by (dtac rtranclD 1);
+by Safe_tac;
+by (ftac subcls_is_class 1);
+by (dtac trancl_into_rtrancl 1);
+by (fast_tac (HOL_cs addDs [fields_mono]) 1);
+qed "widen_cfs_fields";
-val widen_cfs_fields = prove_goal thy "!!X. [|field (G,C) fn = Some (fd, fT);\
-\ G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G|] ==> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
-fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
-bind_thm ("widen_cfs_fields",widen_cfs_fields);
-
-
-Goal "wf_prog wf_mb G ==> method (G,C) sig = Some (md,mh,m)\
+Goal "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))";
-by( case_tac "is_class G C" 1);
-by( forw_inst_tac [("C","C")] method_rec 2);
-by( asm_full_simp_tac (simpset() addsimps [is_class_def]
- delsimps [not_None_eq]) 2);
by( etac subcls1_induct 1);
by( atac 1);
by( Force_tac 1);
by( forw_inst_tac [("C","C")] method_rec 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
by( rotate_tac ~1 1);
by( Asm_full_simp_tac 1);
by( dtac override_SomeD 1);
@@ -270,11 +258,10 @@
by( atac 3);
by( rtac r_into_rtrancl 2);
by( fast_tac (HOL_cs addIs [subcls1I]) 2);
-by( forward_tac [table_mapf_SomeD] 1);
-by( strip_tac1 1);
-by( Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (ftac map_of_SomeD 1);
by( rewtac wf_cdecl_def);
-by( Asm_full_simp_tac 1);
+by (Clarsimp_tac 1);
qed_spec_mp "method_wf_mdecl";
Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
@@ -285,12 +272,12 @@
by( Fast_tac 1);
by( etac conjE 1);
by( etac trancl_trans_induct 1);
-by( strip_tac1 2);
-by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
+by( Clarify_tac 2);
+by( EVERY[smp_tac 3 2]);
by( fast_tac (HOL_cs addEs [widen_trans]) 2);
-by( strip_tac1 1);
+by( Clarify_tac 1);
by( dtac subcls1D 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
by( stac method_rec 1);
by( atac 1);
by( rewtac override_def);
@@ -304,13 +291,10 @@
by( atac 1);
by( split_all_tac 1);
by( rewtac wf_cdecl_def);
-by( dtac table_mapf_Some2 1);
-by( Clarsimp_tac 1);
-by( dres_inst_tac [("xys1","ms")] get_in_set 1);
+by( dtac map_of_SomeD 1);
by Auto_tac;
qed_spec_mp "subcls_widen_methd";
-
Goal
"[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
\ method (G,D) sig = Some (md, rT, b) |] \
@@ -319,12 +303,7 @@
simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
qed "subtype_widen_methd";
-
-Goal "wf_prog wf_mb G ==> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
-by( case_tac "is_class G C" 1);
-by( forw_inst_tac [("C","C")] method_rec 2);
-by( asm_full_simp_tac (simpset() addsimps [is_class_def]
- delsimps [not_None_eq]) 2);
+Goal "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)";
by (etac subcls1_induct 1);
ba 1;
by (Asm_full_simp_tac 1);
@@ -340,26 +319,30 @@
by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
qed_spec_mp "method_in_md";
-
Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
by( etac subcls1_induct 1);
by( atac 1);
by( Asm_simp_tac 1);
-by( strip_tac1 1);
by( stac fields_rec 1);
-by( atac 1);
+by( Fast_tac 1);
by( atac 1);
-by( Asm_simp_tac 1);
-by( safe_tac set_cs);
-by( Fast_tac 2);
+by( Clarsimp_tac 1);
+by( Safe_tac);
+by( Force_tac 2);
by( dtac class_wf 1);
by( atac 1);
by( rewtac wf_cdecl_def);
-by( Asm_full_simp_tac 1);
-by( strip_tac1 1);
+by( Clarsimp_tac 1);
by( EVERY[dtac bspec 1, atac 1]);
by( rewtac wf_fdecl_def);
-by( split_all_tac 1);
-by( Asm_full_simp_tac 1);
-bind_thm ("is_type_fields", result() RS bspec);
+by Auto_tac;
+qed_spec_mp "fields_is_type_lemma";
+
+Goal "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==> \
+\ is_type G f";
+by(dtac map_of_SomeD 1);
+by(datac fields_is_type_lemma 2 1);
+by(Auto_tac);
+qed "fields_is_type";
+
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Dec 06 19:10:36 2000 +0100
@@ -30,14 +30,12 @@
wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
"wf_cdecl wf_mb G ==
- \\<lambda>(C,(sc,fs,ms)).
- (\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
+ \\<lambda>(C,(D,fs,ms)).
+ (\\<forall>f\\<in>set fs. wf_fdecl G f) \\<and> unique fs \\<and>
(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and>
- (case sc of None => C = Object
- | Some D =>
- is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and>
- (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
- method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
+ (C \\<noteq> Object \\<longrightarrow> is_class G D \\<and> \\<not>G\\<turnstile>D\\<preceq>C C \\<and>
+ (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
+ method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
wf_prog :: "'c wf_mb => 'c prog => bool"
"wf_prog wf_mb G ==
--- a/src/HOL/MicroJava/J/WellType.ML Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML Wed Dec 06 19:10:36 2000 +0100
@@ -13,18 +13,18 @@
Goal
-"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
-\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
-\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
+"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G; \
+\ class G C = Some y|] ==> \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
+\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
by( datac widen_methd 2 1);
-by( Clarsimp_tac 1);
+by( Clarify_tac 1);
+by( ftac subcls_is_class2 1);
+by (Asm_simp_tac 1);
by( dtac method_wf_mdecl 1);
-by( atac 1);
by( rewtac wf_mdecl_def);
by Auto_tac;
qed "Call_lemma";
-
Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
by (Asm_simp_tac 1);
qed "method_Object";
@@ -42,9 +42,32 @@
by (Fast_tac 1);
qed "appl_methsD";
-val is_type_typeof = prove_goal thy
- "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [
- rtac val_.induct 1,
- Fast_tac 5,
- ALLGOALS Simp_tac]) RS mp;
+bind_thm ("max_spec2mheads", insertI1 RSN (2,(equalityD2 RS subsetD)) RS
+ max_spec2appl_meths RS appl_methsD);
+
+Goal "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)";
+by (rtac val_.induct 1);
+by (Fast_tac 5);
+by Auto_tac;
+qed_spec_mp "is_type_typeof";
Addsimps [is_type_typeof];
+
+Goal "typeof (\\<lambda>a. None) v = Some T \\<longrightarrow> is_type G T";
+by (rtac val_.induct 1);
+by Auto_tac;
+qed_spec_mp "typeof_empty_is_type";
+
+Goal "wf_prog wf_mb G \\<Longrightarrow> ((G,L)\\<turnstile>e::T \\<longrightarrow> is_type G T) \\<and> \
+\ ((G,L)\\<turnstile>es[::]Ts \\<longrightarrow> Ball (set Ts) (is_type G)) \\<and> ((G,L)\\<turnstile>c \\<surd> \\<longrightarrow> True)";
+by (rtac ty_expr_ty_exprs_wt_stmt.induct 1);
+by Auto_tac;
+by ( etac typeof_empty_is_type 1);
+by ( asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
+by ( dtac field_fields 1);
+by ( datac fields_is_type 1 1);
+by ( Asm_simp_tac 1);
+ba 1;
+by (auto_tac (claset() addSDs [max_spec2mheads,method_wf_mdecl,is_type_rTI], simpset()addsimps[wf_mdecl_def]));
+qed "wt_is_type";
+
+bind_thm ("ty_expr_is_type", permute_prems 0 1 (wt_is_type RS conjunct1 RS mp));
--- a/src/HOL/MicroJava/J/WellType.thy Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Dec 06 19:10:36 2000 +0100
@@ -95,7 +95,7 @@
E\\<turnstile>NewC C::Class C"
(* cf. 15.15 *)
- Cast "[| E\\<turnstile>e::Class C;
+ Cast "[| E\\<turnstile>e::Class C; is_class (prg E) D;
prg E\\<turnstile>C\\<preceq>? D |] ==>
E\\<turnstile>Cast D e::Class D"