--- a/src/HOL/MicroJava/J/Conform.ML Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML Mon Jan 03 14:07:08 2000 +0100
@@ -75,7 +75,7 @@
ALLGOALS Asm_simp_tac]) RS mp;
val conf_widen = prove_goalw thy [conf_def]
-"\\<And>G. wf_prog wtm G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
+"\\<And>G. wf_prog wf_mb G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
rtac val_.induct 1,
ALLGOALS Simp_tac,
ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
@@ -120,7 +120,7 @@
\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>Class C'\\<preceq>Class C)"
(K[fast_tac (HOL_cs addDs [non_npD]) 1]);
-Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wtm G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
+Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
\ (\\<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);
@@ -134,7 +134,7 @@
by (Fast_tac 1);
qed_spec_mp "non_np_objD'";
-Goal "wf_prog wtm G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow> list_all2 (conf G h) vs Ts'";
+Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow> list_all2 (conf G h) vs Ts'";
by( induct_tac "vs" 1);
by( ALLGOALS Clarsimp_tac);
by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
--- a/src/HOL/MicroJava/J/Conform.thy Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Mon Jan 03 14:07:08 2000 +0100
@@ -26,7 +26,7 @@
hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
"G\\<turnstile>h h\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
- conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
+ conforms :: "state \\<Rightarrow> java_mb env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
"s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
end
--- a/src/HOL/MicroJava/J/Eval.thy Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Mon Jan 03 14:07:08 2000 +0100
@@ -10,15 +10,15 @@
Eval = State +
consts
- eval :: "javam prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set"
- evals :: "javam prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
- exec :: "javam prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set"
+ eval :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set"
+ evals :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
+ exec :: "java_mb prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set"
syntax
- eval :: "[javam prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
- evals:: "[javam prog,xstate,expr list,
+ eval :: "[java_mb prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
+ evals:: "[java_mb prog,xstate,expr list,
val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81)
- exec :: "[javam prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81)
+ exec :: "[java_mb prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81)
translations
"G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, _args x s') \\<in> eval G"
--- a/src/HOL/MicroJava/J/JBasis.ML Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML Mon Jan 03 14:07:08 2000 +0100
@@ -67,6 +67,10 @@
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])];
@@ -114,7 +118,7 @@
Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
by (induct_tac "l" 1);
-by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
+by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
qed_spec_mp "unique_map_inj";
Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Mon Jan 03 14:07:08 2000 +0100
@@ -8,7 +8,7 @@
Addsimps [split_beta];
-Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> \
+Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> \
\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)\\<Colon>\\<preceq>(G, lT)";
by( etac conforms_upd_obj 1);
by( rewtac oconf_def);
@@ -16,7 +16,7 @@
qed "NewC_conforms";
Goalw [cast_ok_def]
- "\\<lbrakk> wf_prog wtm G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
+ "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
by( case_tac1 "v = Null" 1);
by( Asm_full_simp_tac 1);
@@ -44,7 +44,7 @@
by Auto_tac;
qed "Cast_conf";
-Goal "\\<lbrakk> wf_prog wtm G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
+Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
\ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
by( dtac np_NoneD 1);
@@ -60,10 +60,10 @@
by( dtac oconf_objD 1);
by( atac 1);
by Auto_tac;
-val FAcc_type_sound = result();
+qed "FAcc_type_sound";
Goal
- "\\<lbrakk> wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \
+ "\\<lbrakk> wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
\ (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
\ (G, lT)\\<turnstile>aa\\<Colon>Class C; \
\ field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
@@ -105,9 +105,9 @@
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);
-val FAss_type_sound = result();
+qed "FAss_type_sound";
-Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wtm G; list_all2 (conf G h) pvs pTs; \
+Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
\ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
\ length pTs' = length pns; nodups pns; \
\ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
@@ -145,7 +145,7 @@
by( EVERY'[forward_tac [hext_objD], atac] 1);
by( Clarsimp_tac 1);
by( EVERY'[dtac Call_lemma, atac, atac] 1);
-by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])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);
by( mp_tac 2);
--- a/src/HOL/MicroJava/J/TypeRel.ML Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML Mon Jan 03 14:07:08 2000 +0100
@@ -14,12 +14,6 @@
\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
(K [Auto_tac]);
-context Option.thy;
-Goal "{y. x = Some y} \\<subseteq> {the x}";
-by Auto_tac;
-val some_subset_the = result();
-context thy;
-
Goal "finite (subcls1 G)";
by(stac subcls1_def2 1);
by( rtac finite_SigmaI 1);
@@ -38,21 +32,11 @@
auto_tac (claset() addDs lemmata, simpset())]);
-(*#### patch for Isabelle98-1*)
-val major::prems = goal Trancl.thy
- "\\<lbrakk> (x,y) \\<in> r^+; \
-\ \\<And>x y. (x,y) \\<in> r \\<Longrightarrow> P x y; \
-\ \\<And>x y z. \\<lbrakk> (x,y) \\<in> r^+; P x y; (y,z) \\<in> r^+; P y z \\<rbrakk> \\<Longrightarrow> P x z \
-\ \\<rbrakk> \\<Longrightarrow> P x y";
-by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
-qed "trancl_trans_induct";
-
-Goalw [is_class_def] "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> is_class G C";
+Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C";
by(etac trancl_trans_induct 1);
by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
qed "subcls_is_class";
-
(* A particular thm about wf;
looks like it is an odd instance of something more general
*)
@@ -66,7 +50,7 @@
by (Fast_tac 1);
by(rewrite_goals_tac [wf_def]);
by(Blast_tac 1);
-val wf_rel_lemma = result();
+qed "wf_rel_lemma";
(* Proving the termination conditions *)
@@ -74,7 +58,7 @@
goalw thy [subcls1_rel_def] "wf subcls1_rel";
by(rtac (wf_rel_lemma RS wf_subset) 1);
by(Force_tac 1);
-val wf_subcls1_rel = result();
+qed "wf_subcls1_rel";
val method_TC = prove_goalw_cterm [subcls1_rel_def]
(cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs)))))
@@ -111,21 +95,19 @@
val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R"
[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
-val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> C=cm | G\\<turnstile>C\\<prec>C cm"
-[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> C=cm | G\\<turnstile>C\\<prec>C cm"];
+val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> G\\<turnstile>C\\<prec>C cm"
+[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<prec>C cm"];
-Goal "\\<lbrakk>G\\<turnstile>S\\<preceq>U; \\<forall>C. is_class G C \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object;\
-\\\<forall>C. G\\<turnstile>Object\\<prec>C C \\<longrightarrow> False \\<rbrakk> \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
+Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
by( etac widen.induct 1);
by Safe_tac;
by( ALLGOALS (forward_tac [widen_Class, widen_RefT]));
by Safe_tac;
by( rtac widen.null 2);
-by( forward_tac [widen_Class_Class] 1);
-by Safe_tac;
-by( ALLGOALS(EVERY'[etac thin_rl,etac thin_rl,
- fast_tac (claset() addIs [widen.subcls,trancl_trans])]));
-qed_spec_mp "widen_trans_lemma";
+by(dtac widen_Class_Class 1);
+by(rtac widen.subcls 1);
+by(eatac rtrancl_trans 1 1);
+qed_spec_mp "widen_trans";
val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
--- a/src/HOL/MicroJava/J/TypeRel.thy Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Jan 03 14:07:08 2000 +0100
@@ -21,7 +21,7 @@
translations
"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
- "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^+"
+ "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^*"
"G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G"
"G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G"
--- a/src/HOL/MicroJava/J/WellForm.ML Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML Mon Jan 03 14:07:08 2000 +0100
@@ -5,76 +5,63 @@
*)
val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
- "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> wf_cdecl wtm G (C,c)" (K [
+ "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wf_cdecl wf_mb G (C,c)" (K [
Asm_full_simp_tac 1,
fast_tac (set_cs addDs [get_in_set]) 1]);
val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
- "\\<And>X. wf_prog wtm G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
+ "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
safe_tac set_cs,
dtac in_set_get 1,
Auto_tac]);
Addsimps [class_Object];
val is_class_Object = prove_goalw thy [is_class_def]
- "\\<And>X. wf_prog wtm G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
+ "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
Addsimps [is_class_Object];
-Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not> G\\<turnstile>D\\<prec>C C";
+Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> 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( dtac class_wf 1);
-by( atac 1);
+by( datac class_wf 1 1);
by( rewtac wf_cdecl_def);
-by( Clarsimp_tac 1);
+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]
-"\\<And>X. \\<lbrakk>wf_cdecl wtm G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
+"\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
pair_tac "r" 1,
Asm_full_simp_tac 1,
strip_tac1 1,
option_case_tac 1,
Fast_tac 1]);
-local
-val lemma = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C=Object \\<longrightarrow> R" (K [
- etac trancl_trans_induct 1,
- atac 2,
- rewtac subcls1_def,
- Auto_tac]);
-in
-val subcls_Object = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>Object\\<prec>C C\\<rbrakk> \\<Longrightarrow> R" (K [
- etac (lemma RS mp) 1,
- Auto_tac]);
-end;
-
-Goal "\\<lbrakk>wf_prog wt G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> \\<not> G\\<turnstile>D\\<prec>C C";
+Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
by(etac tranclE 1);
-by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
+by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
qed "subcls_asym";
-val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
+val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> 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]);
val acyclic_subcls1 = prove_goalw thy [acyclic_def]
- "\\<And>X. wf_prog wt G \\<Longrightarrow> acyclic (subcls1 G)" (K [
+ "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> acyclic (subcls1 G)" (K [
strip_tac1 1,
fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
-val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
+val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> 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]);
-
val major::prems = goal thy
- "\\<lbrakk>wf_prog wt G; \\<And>C. \\<forall>D. G\\<turnstile>C\\<prec>C D \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
+ "\\<lbrakk>wf_prog wf_mb G; \\<And>C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
by(cut_facts_tac [major RS wf_subcls1] 1);
by(dtac wf_trancl 1);
by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
@@ -83,9 +70,9 @@
by(Auto_tac);
qed "subcls_induct";
-val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wtm G; P Object; \
+val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wf_mb G; P Object; \
\\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
-\ wf_cdecl wtm G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
+\ wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
\ \\<rbrakk> \\<Longrightarrow> P C";
by( cut_facts_tac prems 1);
by( rtac impE 1);
@@ -111,7 +98,7 @@
by( etac subcls1I 1);
qed "subcls1_induct";
-Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) = \
+Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
@@ -125,9 +112,9 @@
by( dtac wf_cdecl_supD 1);
by( atac 1);
by( Asm_full_simp_tac 1);
-val method_rec = result();
+qed "method_rec";
-Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
@@ -142,57 +129,43 @@
by( dtac wf_cdecl_supD 1);
by( atac 1);
by( Asm_full_simp_tac 1);
-val fields_rec = result();
+qed "fields_rec";
-val method_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> method (G,Object) = empty"
+val method_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> method (G,Object) = empty"
(K [stac method_rec 1,Auto_tac]);
-val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
+val fields_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> fields (G,Object) = []"(K [
stac fields_rec 1,Auto_tac]);
Addsimps [method_Object, fields_Object];
val field_Object = prove_goalw thy [field_def]
- "\\<And>X. wf_prog wtm G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
+ "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
Addsimps [field_Object];
-val subcls_C_Object = prove_goal thy
- "\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
- etac subcls1_induct 1,
- atac 1,
- Fast_tac 1,
- safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),
- fast_tac (HOL_cs addIs [r_into_trancl]) 1,
- rtac trancl_trans 1,
- atac 2,
- rtac r_into_trancl 1,
- rtac subcls1I 1,
- ALLGOALS Asm_simp_tac]) RS mp;
+Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C Object";
+by(etac subcls1_induct 1);
+by( atac 1);
+by( Fast_tac 1);
+by(auto_tac (HOL_cs addSDs [wf_cdecl_supD], simpset()));
+by(eatac rtrancl_into_rtrancl2 1 1);
+qed "subcls_C_Object";
val is_type_rTI = prove_goalw thy [wf_mhead_def]
"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
(K [split_all_tac 1, Auto_tac]);
-val widen_Class_Object = prove_goal thy
- "\\<lbrakk>wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object" (fn prems => [
- cut_facts_tac prems 1,
- case_tac "C=Object" 1,
- hyp_subst_tac 1,
- Asm_simp_tac 1,
- rtac widen.subcls 1,
- fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);
+Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object";
+by(rtac widen.subcls 1);
+by(eatac subcls_C_Object 1 1);
+qed "widen_Class_Object";
-val widen_trans = prove_goal thy "\\<lbrakk>wf_prog wtm G; G\\<turnstile>S\\<preceq>U; G\\<turnstile>U\\<preceq>T\\<rbrakk> \\<Longrightarrow> G\\<turnstile>S\\<preceq>T"
-(fn prems=> [cut_facts_tac prems 1,
- fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,
- subcls_Object]) 1]);
+Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+\ x \\<in> set (fields (G,C)) \\<longrightarrow> 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";
-val fields_mono = prove_goal thy
-"\\<And>X. \\<lbrakk>G\\<turnstile>C'\\<prec>C C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
-\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))" (K [
- etac trancl_trans_induct 1,
- safe_tac (HOL_cs addSDs [subcls1D]),
- stac fields_rec 1,
- Auto_tac]) RS mp;
-
-Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
by( etac subcls1_induct 1);
by( atac 1);
@@ -209,24 +182,22 @@
by( dtac split_Pair_eq 1);
by( SELECT_GOAL (Auto_tac) 1);
by( rtac widen_trans 1);
-by( atac 1);
-by( etac (r_into_trancl RS widen.subcls) 1);
+by( etac (r_into_rtrancl RS widen.subcls) 1);
by( etac BallE 1);
by( contr_tac 1);
by( Asm_full_simp_tac 1);
-val widen_fields_defpl' = result();
+qed "widen_fields_defpl'";
-Goal "\\<lbrakk>is_class G C; wf_prog wtm G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
+Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
\ G\\<turnstile>Class C\\<preceq>Class fd";
-by( dtac widen_fields_defpl' 1);
-by( atac 1);
+by( datac widen_fields_defpl' 1 1);
(*###################*)
by( dtac bspec 1);
auto();
-val widen_fields_defpl = result();
+qed "widen_fields_defpl";
-Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
+Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
by( etac subcls1_induct 1);
by( atac 1);
by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
@@ -247,21 +218,27 @@
by( Asm_full_simp_tac 1);
by( dtac split_Pair_eq 1);
by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);
-val unique_fields = result();
+qed "unique_fields";
+
+(*####TO Trancl.ML*)
+Goal "(a,b):r^* ==> a=b | a~=b & (a,b):r^+";
+by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym]
+ delsimps [reflcl_trancl]) 1);
+qed "rtranclD";
Goal
-"\\<lbrakk>wf_prog wtm G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
\ map_of (fields (G,C')) f = Some ft";
by( dtac widen_Class_Class 1);
-by( etac disjE 1);
-by( Asm_simp_tac 1);
+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);
-val widen_fields_mono = result();
+qed "widen_fields_mono";
val cfs_fields_lemma = prove_goalw thy [field_def]
@@ -269,11 +246,11 @@
(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
-\ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
+\ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
-Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
-\ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
+Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
+\ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class 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]
@@ -290,21 +267,24 @@
by( thin_tac "?P \\<longrightarrow> ?Q" 1);
by( Clarify_tac 2);
by( rtac widen_trans 2);
-by( atac 2);
by( atac 3);
by( rtac widen.subcls 2);
-by( rtac r_into_trancl 2);
+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( rewtac wf_cdecl_def);
by( Asm_full_simp_tac 1);
-val method_wf_mdecl = result() RS mp;
+qed_spec_mp "method_wf_mdecl";
-Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
+Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
\ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
\ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
+by( dtac rtranclD 1);
+by( etac disjE 1);
+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]);
@@ -333,7 +313,7 @@
Goal
- "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
+ "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wf_mb G; \
\ method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
\ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by(auto_tac (claset() addSDs [widen_Class_Class]
@@ -342,7 +322,7 @@
qed "subtype_widen_methd";
-Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
+Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> 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]
@@ -362,9 +342,8 @@
by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
qed_spec_mp "method_in_md";
-writeln"OK";
-Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
by( etac subcls1_induct 1);
by( atac 1);
@@ -385,4 +364,4 @@
by( rewtac wf_fdecl_def);
by( split_all_tac 1);
by( Asm_full_simp_tac 1);
-val is_type_fields = result() RS bspec;
+bind_thm ("is_type_fields", result() RS bspec);
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Mon Jan 03 14:07:08 2000 +0100
@@ -16,7 +16,7 @@
WellForm = TypeRel +
-types 'c wtm = 'c prog => cname => 'c mdecl => bool
+types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
constdefs
@@ -26,22 +26,22 @@
wf_mhead :: "'c prog \\<Rightarrow> sig \\<Rightarrow> ty \\<Rightarrow> bool"
"wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
- wf_mdecl :: "'c wtm \\<Rightarrow> 'c wtm"
-"wf_mdecl wtm G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wtm G C (sig,rT,mb)"
+ wf_mdecl :: "'c wf_mb \\<Rightarrow> 'c wf_mb"
+"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
- wf_cdecl :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
-"wf_cdecl wtm G \\<equiv>
+ wf_cdecl :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
+"wf_cdecl wf_mb G \\<equiv>
\\<lambda>(C,(sc,fs,ms)).
(\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
- (\\<forall>m\\<in>set ms. wf_mdecl wtm G C m) \\<and> unique ms \\<and>
+ (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and>
(case sc of None \\<Rightarrow> C = Object
| Some D \\<Rightarrow>
is_class G D \\<and> \\<not> G\\<turnstile>D\\<prec>C C \\<and>
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
- wf_prog :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
-"wf_prog wtm G \\<equiv>
- let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wtm G c) \\<and> unique G"
+ wf_prog :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
+"wf_prog wf_mb G \\<equiv>
+ let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
end
--- a/src/HOL/MicroJava/J/WellType.ML Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML Mon Jan 03 14:07:08 2000 +0100
@@ -5,8 +5,8 @@
*)
Goalw [m_head_def]
-"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
-\\\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
+\\\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by( forward_tac [widen_Class_RefT] 1);
by( etac exE 1);
by( hyp_subst_tac 1);
@@ -15,18 +15,15 @@
by( strip_tac1 1);
by( split_all_tac 1);
by( dtac widen_Class_Class 1);
-by( etac disjE 1);
-by( hyp_subst_tac 1);
-by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
by( dtac subcls_widen_methd 1);
by Auto_tac;
qed "widen_methd";
Goal
-"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
-\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)";
+\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
by( dtac widen_methd 1);
by( atac 1);
by( atac 1);
@@ -35,11 +32,11 @@
by( atac 1);
by( rewtac wf_mdecl_def);
by Auto_tac;
-val Call_lemma = result();
+qed "Call_lemma";
val m_head_Object = prove_goalw thy [m_head_def]
-"\\<And>x. wf_prog wtm G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
+"\\<And>x. wf_prog wf_mb G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
Addsimps [m_head_Object];
--- a/src/HOL/MicroJava/J/WellType.thy Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Mon Jan 03 14:07:08 2000 +0100
@@ -69,20 +69,20 @@
"typeof dt (Addr a) = dt a"
types
- javam = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
+ java_mb = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
(* method body with parameter names, local variables, block, result expression *)
consts
- ty_expr :: "javam env \\<Rightarrow> (expr \\<times> ty ) set"
- ty_exprs:: "javam env \\<Rightarrow> (expr list \\<times> ty list) set"
- wt_stmt :: "javam env \\<Rightarrow> stmt set"
+ ty_expr :: "java_mb env \\<Rightarrow> (expr \\<times> ty ) set"
+ ty_exprs:: "java_mb env \\<Rightarrow> (expr list \\<times> ty list) set"
+ wt_stmt :: "java_mb env \\<Rightarrow> stmt set"
syntax
-ty_expr :: "javam env \\<Rightarrow> [expr , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_" [51,51,51]50)
-ty_exprs:: "javam env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
-wt_stmt :: "javam env \\<Rightarrow> stmt \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
+ty_expr :: "java_mb env \\<Rightarrow> [expr , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_" [51,51,51]50)
+ty_exprs:: "java_mb env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
+wt_stmt :: "java_mb env \\<Rightarrow> stmt \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
translations
"E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr E"
@@ -168,8 +168,8 @@
constdefs
- wt_java_mdecl :: javam prog => cname => javam mdecl => bool
-"wt_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
+ wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
+"wf_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
length pTs = length pns \\<and>
nodups pns \\<and>
unique lvars \\<and>
@@ -178,7 +178,7 @@
(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
- wf_java_prog :: javam prog => bool
-"wf_java_prog G \\<equiv> wf_prog wt_java_mdecl G"
+ wf_java_prog :: java_mb prog => bool
+"wf_java_prog G \\<equiv> wf_prog wf_java_mdecl G"
end