tuned
authorkleing
Tue Apr 30 13:00:29 2002 +0200 (2002-04-30)
changeset 1310190b31354fe15
parent 13100 ff00791319e2
child 13102 b6f8aae5f152
tuned
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Apr 30 12:15:48 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Apr 30 13:00:29 2002 +0200
     1.3 @@ -24,9 +24,9 @@
     1.4    distinct_classes: "list_nam \<noteq> test_nam"
     1.5    distinct_fields:  "val_nam \<noteq> next_nam"
     1.6  
     1.7 -text {* Shorthands for definitions we will have to use often in the
     1.8 +text {* Abbreviations for definitions we will have to use often in the
     1.9  proofs below: *}
    1.10 -lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
    1.11 +lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def 
    1.12  lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
    1.13                       OutOfMemoryC_def ClassCastC_def
    1.14  lemmas class_defs  = list_class_def test_class_def
    1.15 @@ -306,10 +306,10 @@
    1.16      (                               [list], [OK list, OK list, OK list]),
    1.17      (                         [list, list], [OK list, OK list, OK list]),
    1.18      (                         [PrimT Void], [OK list, OK list, OK list]),
    1.19 -    (                   [list, PrimT Void], [OK list, OK list, OK list]),
    1.20 -    (             [list, list, PrimT Void], [OK list, OK list, OK list]),
    1.21 -    (             [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
    1.22 -    ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
    1.23 +    (                                   [], [OK list, OK list, OK list]),
    1.24 +    (                               [list], [OK list, OK list, OK list]),
    1.25 +    (                         [list, list], [OK list, OK list, OK list]),
    1.26 +    (                         [PrimT Void], [OK list, OK list, OK list])]"
    1.27  
    1.28  lemma wt_makelist [simp]:
    1.29    "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
    1.30 @@ -336,29 +336,29 @@
    1.31    apply (simp add: match_exception_entry_def) 
    1.32    apply simp
    1.33    apply (simp add: app_def xcpt_app_def)
    1.34 +  apply simp 
    1.35    apply simp
    1.36    apply simp
    1.37 -  apply (simp add: app_def xcpt_app_def)
    1.38 -  apply simp
    1.39 +  apply (simp add: app_def xcpt_app_def) 
    1.40    apply simp
    1.41    done
    1.42  
    1.43  text {* The whole program is welltyped: *}
    1.44  constdefs 
    1.45    Phi :: prog_type ("\<Phi>")
    1.46 -  "\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
    1.47 -              if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
    1.48 +  "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
    1.49 +             if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
    1.50    
    1.51  lemma wf_prog:
    1.52 -  "wt_jvm_prog E \<Phi>"
    1.53 +  "wt_jvm_prog E \<Phi>" 
    1.54    apply (unfold wt_jvm_prog_def)
    1.55    apply (rule wf_mb'E [OF wf_struct])
    1.56    apply (simp add: E_def)
    1.57    apply clarify
    1.58    apply (fold E_def)
    1.59 -  apply (simp add: system_defs class_defs Phi_def)
    1.60 +  apply (simp add: system_defs class_defs Phi_def) 
    1.61    apply auto
    1.62 -  done
    1.63 +  done 
    1.64  
    1.65  
    1.66  section "Conformance"
    1.67 @@ -443,7 +443,7 @@
    1.68  
    1.69  lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
    1.70  
    1.71 -generate_code
    1.72 +generate_code 
    1.73    test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
    1.74      [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
    1.75    test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
     2.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Apr 30 12:15:48 2002 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Apr 30 13:00:29 2002 +0200
     2.3 @@ -17,6 +17,20 @@
     2.4    "make_cert step phi B \<equiv> 
     2.5       map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..length phi(] @ [B]"
     2.6  
     2.7 +constdefs
     2.8 +  list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
     2.9 +  "list_ex P xs \<equiv> \<exists>x \<in> set xs. P x"
    2.10 +
    2.11 +lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def)
    2.12 +lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def)
    2.13 +
    2.14 +lemma [code]:
    2.15 +  "is_target step phi pc' =
    2.16 +  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]"
    2.17 +  apply (simp add: list_ex_def is_target_def set_mem_eq)
    2.18 +  apply force
    2.19 +  done
    2.20 +
    2.21  locale lbvc = lbv + 
    2.22    fixes phi :: "'a list" ("\<phi>")
    2.23    fixes c   :: "'a list" 
     3.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Apr 30 12:15:48 2002 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Apr 30 13:00:29 2002 +0200
     3.3 @@ -37,11 +37,10 @@
     3.4  wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow>
     3.5                    's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
     3.6  primrec
     3.7 -"wtl_inst_list []      cert f r T B step pc s = s"
     3.8 -"wtl_inst_list (i#ins) cert f r T B step pc s = 
     3.9 +"wtl_inst_list []     cert f r T B step pc s = s"
    3.10 +"wtl_inst_list (i#is) cert f r T B step pc s = 
    3.11      (let s' = wtl_cert cert f r T B step pc s in
    3.12 -      if s' = T \<or> s = T then T else wtl_inst_list ins cert f r T B step (pc+1) s')"
    3.13 -
    3.14 +      if s' = T \<or> s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')"
    3.15  
    3.16  constdefs
    3.17    cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool"
     4.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Apr 30 12:15:48 2002 +0200
     4.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Apr 30 13:00:29 2002 +0200
     4.3 @@ -72,10 +72,10 @@
     4.4          Load 0,
     4.5          Load 1,
     4.6          Invoke list_name append_name [Class list_name],
     4.7 +        Pop,
     4.8          Load 0,
     4.9          Load 2,
    4.10          Invoke list_name append_name [Class list_name],
    4.11 -        LitPush Unit,
    4.12          Return]"
    4.13  
    4.14    test_class :: "jvm_method class"