# HG changeset patch
# User kleing
# Date 1011129690 -3600
# Node ID 7b7051ae49a04dd3182e24b63d892f141f8ff873
# Parent  fc3a6054907534103acd5eef980eabcb31ac8150
tuned for directly executable definitions

diff -r fc3a60549075 -r 7b7051ae49a0 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Tue Jan 15 21:09:31 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Jan 15 22:21:30 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* Effect of Instructions on the State Type *}
 
-theory Effect = JVMType + JVMExec:
+theory Effect = JVMType + JVMExceptions:
 
 types
   succ_type = "(p_count \<times> state_type option) list"
@@ -97,6 +97,23 @@
   eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type"
   "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"
 
+constdefs
+  isPrimT :: "ty \<Rightarrow> bool"
+  "isPrimT T == case T of PrimT T' \<Rightarrow> True | RefT T' \<Rightarrow> False"
+
+  isRefT :: "ty \<Rightarrow> bool"
+  "isRefT T == case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> True"
+
+lemma isPrimT [simp]:
+  "isPrimT T = (\<exists>T'. T = PrimT T')" by (simp add: isPrimT_def split: ty.splits)
+
+lemma isRefT [simp]:
+  "isRefT T = (\<exists>T'. T = RefT T')" by (simp add: isRefT_def split: ty.splits)
+
+
+lemma "list_all2 P a b \<Longrightarrow> \<forall>(x,y) \<in> set (zip a b). P x y"
+  by (simp add: list_all2_def) 
+
 
 text "Conditions under which eff is applicable:"
 consts
@@ -126,23 +143,22 @@
 "app' (Swap, G, maxs, rT, (ts1#ts2#ST,LT))        = True"
 "app' (IAdd, G, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) 
                                                  = True"
-"app' (Ifcmpeq b, G, maxs, rT, (ts#ts'#ST,LT))    = ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> 
-                                              (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'))"
+"app' (Ifcmpeq b, G, maxs, rT, (ts#ts'#ST,LT))    = (isPrimT ts \<and> ts' = ts \<or> 
+                                                     isRefT ts \<and> isRefT ts')"
 "app' (Goto b, G, maxs, rT, s)                    = True"
 "app' (Return, G, maxs, rT, (T#ST,LT))            = (G \<turnstile> T \<preceq> rT)"
-"app' (Throw, G, maxs, rT, (T#ST,LT))             = (\<exists>r. T = RefT r)"
+"app' (Throw, G, maxs, rT, (T#ST,LT))             = isRefT T"
+
 "app' (Invoke C mn fpTs, G, maxs, rT, s)          = 
    (length fpTs < length (fst s) \<and> 
    (let apTs = rev (take (length fpTs) (fst s));
         X    = hd (drop (length fpTs) (fst s)) 
     in  
-        G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> 
-        (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))"
-
+        G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
+        list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"
+  
 "app' (i,G,maxs,rT,s)                             = False"
 
-
-
 constdefs
   xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
   "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
@@ -276,8 +292,7 @@
 lemma appIfcmpeq[simp]:
 "app (Ifcmpeq b) G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 
  ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" 
-  by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
-
+  by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
 
 lemma appReturn[simp]:
 "app Return G maxs rT pc et (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" 
@@ -299,6 +314,7 @@
   method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> 
   (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")
 proof (cases (open) s)
+  note list_all2_def [simp]
   case Pair
   have "?app (a,b) ==> ?P (a,b)"
   proof -
@@ -323,17 +339,26 @@
     show ?thesis by (unfold app_def, clarsimp) blast
   qed
   with Pair 
-  have "?app s ==> ?P s" by simp
+  have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) clarsimp
+  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp simp add: min_def)
   ultimately
-  show ?thesis by blast
+  show ?thesis by (rule iffI) 
 qed 
 
 lemma effNone: 
   "(pc', s') \<in> set (eff i G pc et None) \<Longrightarrow> s' = None"
   by (auto simp add: eff_def xcpt_eff_def norm_eff_def)
 
+
+text {* some helpers to make the specification directly executable: *}
+declare list_all2_Nil [code]
+declare list_all2_Cons [code]
+
+lemma xcpt_app_lemma [code]:
+  "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
+  by (simp add: list_all_conv)
+
 lemmas [simp del] = app_def xcpt_app_def
 
 end