# HG changeset patch
# User kleing
# Date 1020164429 -7200
# Node ID 90b31354fe152a586e68c666000ecaa753d33c66
# Parent  ff00791319e2d112986ea5a606f8926e03717790
tuned

diff -r ff00791319e2 -r 90b31354fe15 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Apr 30 12:15:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Apr 30 13:00:29 2002 +0200
@@ -24,9 +24,9 @@
   distinct_classes: "list_nam \<noteq> test_nam"
   distinct_fields:  "val_nam \<noteq> next_nam"
 
-text {* Shorthands for definitions we will have to use often in the
+text {* Abbreviations for definitions we will have to use often in the
 proofs below: *}
-lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
+lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def 
 lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
                      OutOfMemoryC_def ClassCastC_def
 lemmas class_defs  = list_class_def test_class_def
@@ -306,10 +306,10 @@
     (                               [list], [OK list, OK list, OK list]),
     (                         [list, list], [OK list, OK list, OK list]),
     (                         [PrimT Void], [OK list, OK list, OK list]),
-    (                   [list, PrimT Void], [OK list, OK list, OK list]),
-    (             [list, list, PrimT Void], [OK list, OK list, OK list]),
-    (             [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
-    ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
+    (                                   [], [OK list, OK list, OK list]),
+    (                               [list], [OK list, OK list, OK list]),
+    (                         [list, list], [OK list, OK list, OK list]),
+    (                         [PrimT Void], [OK list, OK list, OK list])]"
 
 lemma wt_makelist [simp]:
   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
@@ -336,29 +336,29 @@
   apply (simp add: match_exception_entry_def) 
   apply simp
   apply (simp add: app_def xcpt_app_def)
+  apply simp 
   apply simp
   apply simp
-  apply (simp add: app_def xcpt_app_def)
-  apply simp
+  apply (simp add: app_def xcpt_app_def) 
   apply simp
   done
 
 text {* The whole program is welltyped: *}
 constdefs 
   Phi :: prog_type ("\<Phi>")
-  "\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
-              if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
+  "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
+             if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
   
 lemma wf_prog:
-  "wt_jvm_prog E \<Phi>"
+  "wt_jvm_prog E \<Phi>" 
   apply (unfold wt_jvm_prog_def)
   apply (rule wf_mb'E [OF wf_struct])
   apply (simp add: E_def)
   apply clarify
   apply (fold E_def)
-  apply (simp add: system_defs class_defs Phi_def)
+  apply (simp add: system_defs class_defs Phi_def) 
   apply auto
-  done
+  done 
 
 
 section "Conformance"
@@ -443,7 +443,7 @@
 
 lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
 
-generate_code
+generate_code 
   test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
     [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
   test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
diff -r ff00791319e2 -r 90b31354fe15 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Apr 30 12:15:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Apr 30 13:00:29 2002 +0200
@@ -17,6 +17,20 @@
   "make_cert step phi B \<equiv> 
      map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..length phi(] @ [B]"
 
+constdefs
+  list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+  "list_ex P xs \<equiv> \<exists>x \<in> set xs. P x"
+
+lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def)
+lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def)
+
+lemma [code]:
+  "is_target step phi pc' =
+  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]"
+  apply (simp add: list_ex_def is_target_def set_mem_eq)
+  apply force
+  done
+
 locale lbvc = lbv + 
   fixes phi :: "'a list" ("\<phi>")
   fixes c   :: "'a list" 
diff -r ff00791319e2 -r 90b31354fe15 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Apr 30 12:15:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Apr 30 13:00:29 2002 +0200
@@ -37,11 +37,10 @@
 wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow>
                   's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
 primrec
-"wtl_inst_list []      cert f r T B step pc s = s"
-"wtl_inst_list (i#ins) cert f r T B step pc s = 
+"wtl_inst_list []     cert f r T B step pc s = s"
+"wtl_inst_list (i#is) cert f r T B step pc s = 
     (let s' = wtl_cert cert f r T B step pc s in
-      if s' = T \<or> s = T then T else wtl_inst_list ins cert f r T B step (pc+1) s')"
-
+      if s' = T \<or> s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')"
 
 constdefs
   cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool"
diff -r ff00791319e2 -r 90b31354fe15 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Apr 30 12:15:48 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Apr 30 13:00:29 2002 +0200
@@ -72,10 +72,10 @@
         Load 0,
         Load 1,
         Invoke list_name append_name [Class list_name],
+        Pop,
         Load 0,
         Load 2,
         Invoke list_name append_name [Class list_name],
-        LitPush Unit,
         Return]"
 
   test_class :: "jvm_method class"