# HG changeset patch
# User oheimb
# Date 962700872 -7200
# Node ID f4d76cb264331b1f106537c1266eebbcd392a658
# Parent  b31c2132176af87f20c25bb4c59584dca66607e7
added BinOp

diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/Conform.ML
--- 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);
diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/Eval.thy
--- 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"
 
diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/JTypeSafe.ML
--- 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 *)
diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/State.thy
--- 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"
diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/Term.thy
--- 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)
diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/WellType.thy
--- 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>"
 
diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/ROOT.ML
--- 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";