--- 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"
--- 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"
--- 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"
--- 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"