--- a/src/HOL/MicroJava/J/Conform.ML Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.ML Tue Jul 04 10:54:32 2000 +0200
@@ -50,6 +50,20 @@
rtac val_.induct 1,
Auto_tac]) RS mp;
+Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
+by( Simp_tac 1);
+qed "conf_VoidI";
+
+Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
+by( Simp_tac 1);
+qed "conf_BooleanI";
+
+Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
+by( Simp_tac 1);
+qed "conf_IntegerI";
+
+Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
+
val conf_AddrI = prove_goalw thy [conf_def]
"\\<And>G. \\<lbrakk>h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>T"
(K [Asm_full_simp_tac 1]);
@@ -59,7 +73,6 @@
(K [Asm_full_simp_tac 1]);
Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
-by (Simp_tac 1);
by (res_inst_tac [("y","T")] ty.exhaust 1);
by (etac ssubst 1);
by (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
--- a/src/HOL/MicroJava/J/Eval.thy Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Tue Jul 04 10:54:32 2000 +0200
@@ -48,6 +48,12 @@
(* cf. 15.7.1 *)
Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
+ BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1;
+ G\\<turnstile>s1 -e1\\<succ>v2\\<rightarrow> s2;
+ v = (case bop of Eq \\<Rightarrow> Bool (v1 = v2)
+ | Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow>
+ G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2"
+
(* cf. 15.13.1, 15.2 *)
LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s"
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Tue Jul 04 10:54:32 2000 +0200
@@ -6,6 +6,20 @@
Type safety proof
*)
+Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
+by( Simp_tac 1);
+qed "conf_VoidI";
+
+Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
+by( Simp_tac 1);
+qed "conf_BooleanI";
+
+Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
+by( Simp_tac 1);
+qed "conf_IntegerI";
+
+Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
+
Addsimps [split_beta];
Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> \
@@ -180,6 +194,8 @@
Unify.trace_bound := 40;
Delsplits[split_if];
Delsimps[fun_upd_apply];(*###*)
+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
"wf_java_prog G \\<Longrightarrow> \
\ (G\\<turnstile>(x,(h,l)) -e \\<succ>v \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
@@ -204,7 +220,7 @@
(* Level 7 *)
-(* 13 NewC *)
+(* 14 NewC *)
by( dtac new_AddrD 1);
by( etac disjE 1);
by( Asm_simp_tac 2);
@@ -219,9 +235,18 @@
(* for Cast *)
by( defer_tac 1);
-(* 12 Lit *)
+(* 13 Lit *)
by( etac conf_litval 1);
+(* 12 BinOp *)
+by forward_hyp_tac;
+by forward_hyp_tac;
+by( EVERY'[rtac conjI, eatac hext_trans 1] 1);
+by( etac conjI 1);
+by( Clarsimp_tac 1);
+by( dtac eval_no_xcpt 1);
+by( asm_full_simp_tac (simpset() addsplits [binop.split]) 1);
+
(* 11 LAcc *)
by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
@@ -235,8 +260,6 @@
(* for if *)
by( (case_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
-val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
- (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
by forward_hyp_tac;
(* 10+1 if *)
--- a/src/HOL/MicroJava/J/State.thy Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy Tue Jul 04 10:54:32 2000 +0200
@@ -10,7 +10,7 @@
consts
the_Bool :: "val \\<Rightarrow> bool"
- the_Int :: "val \\<Rightarrow> int"
+ the_Intg :: "val \\<Rightarrow> int"
the_Addr :: "val \\<Rightarrow> loc"
defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
@@ -20,7 +20,7 @@
"the_Bool (Bool b) = b"
primrec
- "the_Int (Intg i) = i"
+ "the_Intg (Intg i) = i"
primrec
"the_Addr (Addr a) = a"
--- a/src/HOL/MicroJava/J/Term.thy Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Tue Jul 04 10:54:32 2000 +0200
@@ -21,10 +21,13 @@
types val = val_
translations "val" <= (type) "val_"
+datatype binop = Eq | Add (* function codes for binary operation *)
+
datatype expr
= NewC cname (* class instance creation *)
| Cast ty expr (* type cast *)
| Lit val (* literal value, also references *)
+ | BinOp binop expr expr (* binary operation *)
| LAcc vname (* local (incl. parameter) access *)
| LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
| FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
--- a/src/HOL/MicroJava/J/WellType.thy Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Tue Jul 04 10:54:32 2000 +0200
@@ -103,14 +103,21 @@
Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
E\\<turnstile>Lit x\\<Colon>T"
+
(* cf. 15.13.1 *)
LAcc "\\<lbrakk>localT E v = Some T; is_type (prg E) T\\<rbrakk> \\<Longrightarrow>
E\\<turnstile>LAcc v\\<Colon>T"
-
+
+ BinOp "\\<lbrakk>E\\<turnstile>e1\\<Colon>T;
+ E\\<turnstile>e2\\<Colon>T;
+ if bop = Eq then T' = PrimT Boolean
+ else T' = T \\<and> T = PrimT Integer\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>BinOp bop e1 e2\\<Colon>T'"
+
(* cf. 15.25, 15.25.1 *)
LAss "\\<lbrakk>E\\<turnstile>LAcc v\\<Colon>T;
- E\\<turnstile>e\\<Colon>T';
- prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>e\\<Colon>T';
+ prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
E\\<turnstile>v\\<Colon>=e\\<Colon>T'"
(* cf. 15.10.1 *)
@@ -148,7 +155,7 @@
Expr "\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
E\\<turnstile>Expr e\\<surd>"
- Comp "\\<lbrakk>E\\<turnstile>s1\\<surd>;
+ Comp "\\<lbrakk>E\\<turnstile>s1\\<surd>;
E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
E\\<turnstile>s1;; s2\\<surd>"
--- a/src/HOL/MicroJava/ROOT.ML Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/ROOT.ML Tue Jul 04 10:54:32 2000 +0200
@@ -4,5 +4,5 @@
Unify.search_bound := 40;
Unify.trace_bound := 40;
-with_paths ["J", "JVM", "BV"] use_thy "JTypeSafe";
+with_paths ["J" ] use_thy "JTypeSafe";
with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";