--- 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]