src/HOL/MicroJava/BV/BVExample.thy
changeset 13101 90b31354fe15
parent 13092 eae72c47d07f
child 13139 94648e0e4506
     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"