--- a/src/HOL/MicroJava/BV/BVSpec.thy Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Jan 18 17:38:56 2001 +0100
@@ -12,30 +12,30 @@
constdefs
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool"
"wt_instr i G rT phi mxs max_pc pc ==
- app i G mxs rT (phi!pc) \<and>
- (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
+ app i G mxs rT (phi!pc) \\<and>
+ (\\<forall> pc' \\<in> set (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!pc'))"
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
"wt_start G C pTs mxl phi ==
- G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
+ G \\<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool"
"wt_method G C pTs rT mxs mxl ins phi ==
let max_pc = length ins
in
- 0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
+ 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and>
+ (\\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
"wt_jvm_prog G phi ==
- wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)).
+ wf_prog (\\<lambda>G C (sig,rT,(maxs,maxl,b)).
wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G"
lemma wt_jvm_progD:
-"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi ==> (\\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
@@ -48,27 +48,27 @@
lemma wt_jvm_prog_impl_wt_start:
"[| wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==>
- 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
+ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)"
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
text {* for most instructions wt\_instr collapses: *}
lemma
"succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc =
- (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
+ (app i G mxs rT (phi!pc) \\<and> pc+1 < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
by (simp add: wt_instr_def)
-(* move to WellForm *)
+(* ### move to WellForm *)
lemma methd:
- "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
- ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
+ "[| wf_prog wf_mb G; (C,S,fs,mdecls) \\<in> set G; (sig,rT,code) \\<in> set mdecls |]
+ ==> method (G,C) sig = Some(C,rT,code) \\<and> is_class G C"
proof -
assume wf: "wf_prog wf_mb G"
- assume C: "(C,S,fs,mdecls) \<in> set G"
+ assume C: "(C,S,fs,mdecls) \\<in> set G"
- assume m: "(sig,rT,code) \<in> set mdecls"
+ assume m: "(sig,rT,code) \\<in> set mdecls"
moreover
from wf
have "class G Object = Some (arbitrary, [], [])"
@@ -76,25 +76,25 @@
moreover
from wf C
have c: "class G C = Some (S,fs,mdecls)"
- by (auto simp add: wf_prog_def intro: map_of_SomeI)
+ by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
ultimately
- have O: "C \<noteq> Object"
+ have O: "C \\<noteq> Object"
by auto
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)"
+ 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)"
+ 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 dest: method_rec [of _ _ C])
+ by (auto simp add: is_class_def dest: method_rec [of _ _ C])
qed
--- a/src/HOL/MicroJava/BV/JType.thy Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Thu Jan 18 17:38:56 2001 +0100
@@ -21,7 +21,7 @@
| ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
subtype :: "'c prog => ty => ty => bool"
- "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
+ "subtype G T1 T2 == G \\<turnstile> T1 \\<preceq> T2"
is_ty :: "'c prog => ty => bool"
"is_ty G T == case T of PrimT P => True | RefT R =>
@@ -34,10 +34,10 @@
esl :: "'c prog => ty esl"
"esl G == (types G, subtype G, sup G)"
-lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
+lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
by (auto elim: widen.elims)
-lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
+lemma PrimT_PrimT2: "(G \\<turnstile> PrimT p \\<preceq> xb) = (xb = PrimT p)"
by (auto elim: widen.elims)
lemma is_tyI:
@@ -62,11 +62,11 @@
next
fix R assume R: "T = RefT R"
with wf
- have "R = ClassT Object \<Longrightarrow> ?thesis" by simp
+ have "R = ClassT Object \\<Longrightarrow> ?thesis" by simp
moreover
from R wf ty
- have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
- by (auto simp add: is_ty_def subcls1_def
+ have "R \\<noteq> ClassT Object \\<Longrightarrow> ?thesis"
+ by (auto simp add: is_ty_def subcls1_def is_class_def
elim: converse_rtranclE
split: ref_ty.splits)
ultimately
@@ -163,7 +163,7 @@
lemma sup_subtype_greater:
"[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
is_type G t1; is_type G t2; sup G t1 t2 = OK s |]
- ==> subtype G t1 s \<and> subtype G t2 s"
+ ==> subtype G t1 s \\<and> subtype G t2 s"
proof -
assume wf_prog: "wf_prog wf_mb G"
assume single_valued: "single_valued (subcls1 G)"
@@ -173,16 +173,16 @@
assume is_class: "is_class G c1" "is_class G c2"
with wf_prog
obtain
- "G \<turnstile> c1 \<preceq>C Object"
- "G \<turnstile> c2 \<preceq>C Object"
+ "G \\<turnstile> c1 \\<preceq>C Object"
+ "G \\<turnstile> c2 \\<preceq>C Object"
by (blast intro: subcls_C_Object)
with wf_prog single_valued
obtain u where
"is_lub ((subcls1 G)^* ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
with acyclic
- have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \<and>
- G \<turnstile> c2 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
+ have "G \\<turnstile> c1 \\<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \\<and>
+ G \\<turnstile> c2 \\<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
} note this [simp]
@@ -206,11 +206,11 @@
{ fix c1 c2 D
assume is_class: "is_class G c1" "is_class G c2"
- assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
+ assume le: "G \\<turnstile> c1 \\<preceq>C D" "G \\<turnstile> c2 \\<preceq>C D"
from wf_prog is_class
obtain
- "G \<turnstile> c1 \<preceq>C Object"
- "G \<turnstile> c2 \<preceq>C Object"
+ "G \\<turnstile> c1 \\<preceq>C Object"
+ "G \\<turnstile> c2 \\<preceq>C Object"
by (blast intro: subcls_C_Object)
with wf_prog single_valued
obtain u where
@@ -221,15 +221,15 @@
by (rule some_lub_conv)
moreover
from lub le
- have "G \<turnstile> u \<preceq>C D"
+ have "G \\<turnstile> u \\<preceq>C D"
by (simp add: is_lub_def is_ub_def)
ultimately
- have "G \<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \<preceq>C D"
+ have "G \\<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \\<preceq>C D"
by blast
} note this [intro]
have [dest!]:
- "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
+ "!!C T. G \\<turnstile> Class C \\<preceq> T ==> \\<exists>D. T=Class D \\<and> G \\<turnstile> C \\<preceq>C D"
by (frule widen_Class, auto)
assume "is_type G a" "is_type G b" "is_type G c"
@@ -262,16 +262,16 @@
from wf_prog single_valued acyclic
have
- "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and>
- (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
+ "(\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \\<and>
+ (\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
moreover
from wf_prog single_valued acyclic
have
- "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G).
- x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
+ "\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). \\<forall>z\\<in>err (types G).
+ x <=_(le (subtype G)) z \\<and> y <=_(le (subtype G)) z \\<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
by (unfold lift2_def plussub_def lesub_def le_def)
(auto intro: sup_subtype_smallest sup_exists split: err.split)
--- a/src/HOL/MicroJava/Digest.thy Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/Digest.thy Thu Jan 18 17:38:56 2001 +0100
@@ -41,22 +41,15 @@
@{thm [display] Store_correct [no_vars]}
\medskip
-{\bf lemma} @{text conf_Intg_Integer}:\\
-@{thm [display] conf_Intg_Integer [no_vars]}
-\medskip
-
-{\bf lemma} @{text Bipush_correct}:\\
-@{thm [display] Bipush_correct [no_vars]}
-\medskip
+%removed {\bf lemma} {text conf_Intg_Integer}:\\
+%removed {\bf lemma} {text Bipush_correct}:\\
{\bf lemma} @{text NT_subtype_conv}:\\
@{thm [display] NT_subtype_conv [no_vars]}
\medskip
-{\bf lemma} @{text Aconst_null_correct}:\\
-@{thm [display] Aconst_null_correct [no_vars]}
-\medskip
-
+%removed {\bf lemma} {text Aconst_null_correct}:\\
+
{\bf lemma} @{text Cast_conf2}:\\
@{thm [display] Cast_conf2 [no_vars]}
\medskip
@@ -153,17 +146,11 @@
subsubsection {* Theory Conform *}
text {*
-{\bf theorem} @{text conf_VoidI}:\\
-@{thm [display] conf_VoidI [no_vars]}
-\medskip
+%removed {\bf theorem} {text conf_VoidI}:\\
+
+%removed {\bf theorem} {text conf_BooleanI}:\\
-{\bf theorem} @{text conf_BooleanI}:\\
-@{thm [display] conf_BooleanI [no_vars]}
-\medskip
-
-{\bf theorem} @{text conf_IntegerI}:\\
-@{thm [display] conf_IntegerI [no_vars]}
-\medskip
+%removed {\bf theorem} {text conf_IntegerI}:\\
{\bf theorem} @{text defval_conf}:\\
@{thm [display] defval_conf [no_vars]}
@@ -237,54 +224,30 @@
@{thm [display] not_Some_eq [no_vars]}
\medskip
-{\bf lemma} @{text lift_top_refl}:\\
-@{thm [display] lift_top_refl [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_refl}:\\
-{\bf lemma} @{text lift_top_trans}:\\
-@{thm [display] lift_top_trans [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_trans}:\\
-{\bf lemma} @{text lift_top_Err_any}:\\
-@{thm [display] lift_top_Err_any [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_Err_any}:\\
-{\bf lemma} @{text lift_top_OK_OK}:\\
-@{thm [display] lift_top_OK_OK [no_vars]}
-\medskip
-
-{\bf lemma} @{text lift_top_any_OK}:\\
-@{thm [display] lift_top_any_OK [no_vars]}
-\medskip
-
-{\bf lemma} @{text lift_top_OK_any}:\\
-@{thm [display] lift_top_OK_any [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_OK_OK}:\\
+
+%removed {\bf lemma} @{text lift_top_any_OK}:\\
+
+%removed {\bf lemma} @{text lift_top_OK_any}:\\
-{\bf lemma} @{text lift_bottom_refl}:\\
-@{thm [display] lift_bottom_refl [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_refl}:\\
-{\bf lemma} @{text lift_bottom_trans}:\\
-@{thm [display] lift_bottom_trans [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_trans}:\\
-{\bf lemma} @{text lift_bottom_any_None}:\\
-@{thm [display] lift_bottom_any_None [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_any_None}:\\
-{\bf lemma} @{text lift_bottom_Some_Some}:\\
-@{thm [display] lift_bottom_Some_Some [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_Some_Some}:\\
-{\bf lemma} @{text lift_bottom_any_Some}:\\
-@{thm [display] lift_bottom_any_Some [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_any_Some}:\\
-{\bf lemma} @{text lift_bottom_Some_any}:\\
-@{thm [display] lift_bottom_Some_any [no_vars]}
-\medskip
-
+%removed {\bf lemma} @{text lift_bottom_Some_any}:\\
+
{\bf theorem} @{text sup_ty_opt_refl}:\\
@{thm [display] sup_ty_opt_refl [no_vars]}
\medskip
@@ -683,14 +646,10 @@
subsubsection {* Theory JBasis *}
text {*
-{\bf theorem} @{text image_rev}:\\
-@{thm [display] image_rev [no_vars]}
-\medskip
-
-{\bf theorem} @{text some_subset_the}:\\
-@{thm [display] some_subset_the [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text image_rev}:\\
+
+%removed {\bf theorem} {text some_subset_the}:\\
+
{\bf theorem} @{text fst_in_set_lemma}:\\
@{thm [display] fst_in_set_lemma [no_vars]}
\medskip
@@ -711,18 +670,14 @@
@{thm [display] unique_map_inj [no_vars]}
\medskip
-{\bf theorem} @{text unique_map_Pair}:\\
-@{thm [display] unique_map_Pair [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text unique_map_Pair}:\\
+
{\bf theorem} @{text image_cong}:\\
@{thm [display] image_cong [no_vars]}
\medskip
-{\bf theorem} @{text unique_map_of_Some_conv}:\\
-@{thm [display] unique_map_of_Some_conv [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text unique_map_of_Some_conv}:\\
+
{\bf theorem} @{text Ball_set_table}:\\
@{thm [display] Ball_set_table [no_vars]}
\medskip
@@ -859,15 +814,10 @@
@{thm [display] wtl_method_complete [no_vars]}
\medskip
-{\bf lemma} @{text unique_set}:\\
-@{thm [display] unique_set [no_vars]}
-\medskip
+%removed {\bf lemma} {text unique_set}:\\
-{\bf lemma} @{text unique_epsilon}:\\
-@{thm [display] unique_epsilon [no_vars]}
-\medskip
+%removed {\bf lemma} {text unique_epsilon}:\\
-{\bf theorem} @{text wtl_complete}:\\
@{thm [display] wtl_complete [no_vars]}
\medskip
@@ -915,14 +865,6 @@
@{thm [display] wtl_method_correct [no_vars]}
\medskip
-{\bf lemma} @{text unique_set}:\\
-@{thm [display] unique_set [no_vars]}
-\medskip
-
-{\bf lemma} @{text unique_epsilon}:\\
-@{thm [display] unique_epsilon [no_vars]}
-\medskip
-
{\bf theorem} @{text wtl_correct}:\\
@{thm [display] wtl_correct [no_vars]}
\medskip
@@ -995,13 +937,9 @@
@{thm [display] appStore [no_vars]}
\medskip
-{\bf lemma} @{text appBipush}:\\
-@{thm [display] appBipush [no_vars]}
-\medskip
+%removed {\bf lemma} {text appBipush}:\\
-{\bf lemma} @{text appAconst}:\\
-@{thm [display] appAconst [no_vars]}
-\medskip
+%removed {\bf lemma} {text appAconst}:\\
{\bf lemma} @{text appGetField}:\\
@{thm [display] appGetField [no_vars]}
@@ -1107,10 +1045,7 @@
subsubsection {* Theory Store *}
text {*
-{\bf theorem} @{text newref_None}:\\
-@{thm [display] newref_None [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text newref_None}:\\
*}
subsubsection {* Theory Term *}
@@ -1230,9 +1165,7 @@
@{thm [display] unique_fields [no_vars]}
\medskip
-{\bf theorem} @{text widen_fields_mono}:\\
-@{thm [display] widen_fields_mono [no_vars]}
-\medskip
+%removed {\bf theorem} {text widen_fields_mono}:\\
{\bf theorem} @{text widen_cfs_fields}:\\
@{thm [display] widen_cfs_fields [no_vars]}
@@ -1254,9 +1187,7 @@
@{thm [display] method_in_md [no_vars]}
\medskip
-{\bf theorem} @{text is_type_fields}:\\
-@{thm [display] is_type_fields [no_vars]}
-\medskip
+%removed {\bf theorem} {text is_type_fields}:\\
*}
--- a/src/HOL/MicroJava/J/Decl.ML Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.ML Thu Jan 18 17:38:56 2001 +0100
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-Goal "finite {C. is_class G C}";
+Goalw [is_class_def, class_def] "finite {C. is_class G C}";
by (fold_goals_tac [dom_def]);
by (rtac finite_dom_map_of 1);
qed "finite_is_class";
--- a/src/HOL/MicroJava/J/Decl.thy Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Thu Jan 18 17:38:56 2001 +0100
@@ -46,15 +46,12 @@
"cdecl c" <= (type) "cname \\<times> (c class)"
"prog c" <= (type) "(c cdecl) list"
-consts
+constdefs
class :: "'c prog => (cname \\<leadsto> 'c class)"
+ "class \\<equiv> map_of"
is_class :: "'c prog => cname => bool"
-
-translations
-
- "class" => "map_of"
- "is_class G C" == "class G C \\<noteq> None"
+ "is_class G C \\<equiv> class G C \\<noteq> None"
consts
--- a/src/HOL/MicroJava/J/Example.ML Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.ML Thu Jan 18 17:38:56 2001 +0100
@@ -13,17 +13,19 @@
Delsimps[map_of_Cons]; (* sic! *)
Addsimps[map_of_Cons1, map_of_Cons2];
-Goalw [ObjectC_def] "class tprg Object = Some (arbitrary, [], [])";
+Goalw [ObjectC_def,class_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, \
+Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def]
+"class tprg Base = Some (Object, \
\ [(vee, PrimT Boolean)], \
\ [((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, \
+Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def]
+"class tprg Ext = Some (Base, \
\ [(vee, PrimT Integer)], \
\ [((foo, [Class Base]), Class Ext, foo_Ext)])";
by (Simp_tac 1);
@@ -49,7 +51,8 @@
qed "not_Base_subcls_Ext";
AddSEs [not_Base_subcls_Ext];
-Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
+Goalw [ObjectC_def, BaseC_def, ExtC_def, class_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";
@@ -99,6 +102,8 @@
qed "fields_Object";
Addsimps [fields_Object];
+Addsimps [is_class_def];
+
Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]";
by (stac fields_rec_ 1);
by Auto_tac;
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Thu Jan 18 17:38:56 2001 +0100
@@ -61,7 +61,7 @@
by( SELECT_GOAL Auto_tac 1);
by( Clarify_tac 1);
by( Full_simp_tac 1);
-by( EVERY [forward_tac [hext_objD] 1, atac 1]);
+by( EVERY [ftac hext_objD 1, atac 1]);
by( etac exE 1);
by( Asm_full_simp_tac 1);
by( Clarify_tac 1);
@@ -102,12 +102,6 @@
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); class G C = Some y; \
\ max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
@@ -125,7 +119,7 @@
by( datac non_np_objD' 2 1);
by( Clarsimp_tac 1);
by( Clarsimp_tac 1);
-by( EVERY'[forward_tac [hext_objD], atac] 1);
+by( EVERY'[ftac hext_objD, atac] 1);
by( Clarsimp_tac 1);
by( datac Call_lemma 3 1);
by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1);
@@ -276,7 +270,7 @@
by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
by prune_params_tac;
-(* Level 50 *)
+(* Level 52 *)
(* 1 Call *)
by( case_tac "x" 1);
@@ -298,6 +292,8 @@
by( fast_tac (HOL_cs addEs [hext_trans]) 1);
by( datac ty_expr_is_type 1 1);
by(Clarsimp_tac 1);
+by(rewtac is_class_def);
+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";
--- a/src/HOL/MicroJava/J/TypeRel.ML Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML Thu Jan 18 17:38:56 2001 +0100
@@ -12,7 +12,7 @@
by Auto_tac;
qed "subcls1I";
-Goalw [subcls1_def]
+Goalw [subcls1_def, is_class_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";
@@ -25,12 +25,12 @@
qed "finite_subcls1";
-Goal "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
+Goalw [is_class_def] "(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";
+Goalw [is_class_def] "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;
--- a/src/HOL/MicroJava/J/WellForm.ML Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML Thu Jan 18 17:38:56 2001 +0100
@@ -4,19 +4,19 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-Goalw [wf_prog_def]
+Goalw [wf_prog_def, class_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";
-Goalw [wf_prog_def, ObjectC_def]
+Goalw [wf_prog_def, ObjectC_def, class_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];
-Goal "wf_prog wf_mb G ==> is_class G Object";
+Goalw [is_class_def] "wf_prog wf_mb G ==> is_class G Object";
by (Asm_simp_tac 1);
qed "is_class_Object";
Addsimps [is_class_Object];
@@ -68,7 +68,7 @@
by(Auto_tac);
qed "subcls_induct";
-val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
+val prems = goalw thy [is_class_def] "[|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 (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";
@@ -83,14 +83,15 @@
by( case_tac "C = Object" 1);
by( Fast_tac 1);
by Safe_tac;
-by( forward_tac [class_wf] 1);
+by( ftac class_wf 1);
by( atac 1);
-by( forward_tac [wf_cdecl_supD] 1);
+by( ftac wf_cdecl_supD 1);
by( atac 1);
by( subgoal_tac "G\\<turnstile>C\\<prec>C1a" 1);
by( etac subcls1I 2);
by( rtac (hd (tl (tl (tl prems)))) 1);
+by (rewtac is_class_def);
by Auto_tac;
qed "subcls1_induct";
--- a/src/HOL/MicroJava/J/WellType.ML Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML Thu Jan 18 17:38:56 2001 +0100
@@ -19,9 +19,11 @@
by( datac widen_methd 2 1);
by( Clarify_tac 1);
by( ftac subcls_is_class2 1);
+by (rewtac is_class_def);
by (Asm_simp_tac 1);
by( dtac method_wf_mdecl 1);
by( rewtac wf_mdecl_def);
+by( rewtac is_class_def);
by Auto_tac;
qed "Call_lemma";