src/HOL/MicroJava/BV/BVExample.thy
changeset 13214 2aa33ed5f526
parent 13187 e5434b822a96
child 13727 4ab8d49ab981
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Jun 14 13:24:32 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Jun 14 23:25:36 2002 +0200
     1.3 @@ -252,11 +252,27 @@
     1.4     (                                    [], [Class list_name, Class list_name]),
     1.5     (                          [PrimT Void], [Class list_name, Class list_name])]"
     1.6  
     1.7 +
     1.8 +lemma bounded_append [simp]:
     1.9 +  "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
    1.10 +  apply (simp add: check_bounded_def)
    1.11 +  apply (simp add: nat_number append_ins_def)
    1.12 +  apply (rule allI, rule impI)
    1.13 +  apply (elim pc_end pc_next pc_0)
    1.14 +  apply auto
    1.15 +  done
    1.16 +
    1.17 +lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"
    1.18 +  apply (auto simp add: check_types_def phi_append_def JVM_states_unfold)
    1.19 +  apply (unfold list_def)
    1.20 +  apply auto
    1.21 +  done
    1.22 +  
    1.23  lemma wt_append [simp]:
    1.24    "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
    1.25               [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
    1.26 -  apply (simp add: wt_method_def append_ins_def phi_append_def 
    1.27 -                   wt_start_def wt_instr_def)
    1.28 +  apply (simp add: wt_method_def wt_start_def wt_instr_def)
    1.29 +  apply (simp add: phi_append_def append_ins_def)
    1.30    apply clarify
    1.31    apply (elim pc_end pc_next pc_0)
    1.32    apply simp
    1.33 @@ -277,42 +293,57 @@
    1.34  
    1.35  text {* Some abbreviations for readability *} 
    1.36  syntax
    1.37 -  list :: ty 
    1.38 -  test :: ty
    1.39 +  Clist :: ty 
    1.40 +  Ctest :: ty
    1.41  translations
    1.42 -  "list" == "Class list_name"
    1.43 -  "test" == "Class test_name"
    1.44 +  "Clist" == "Class list_name"
    1.45 +  "Ctest" == "Class test_name"
    1.46  
    1.47  constdefs
    1.48    phi_makelist :: method_type ("\<phi>\<^sub>m")
    1.49    "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
    1.50 -    (                                   [], [OK test, Err    , Err    ]),
    1.51 -    (                               [list], [OK test, Err    , Err    ]),
    1.52 -    (                         [list, list], [OK test, Err    , Err    ]),
    1.53 -    (                               [list], [OK list, Err    , Err    ]),
    1.54 -    (                [PrimT Integer, list], [OK list, Err    , Err    ]),
    1.55 -    (                                   [], [OK list, Err    , Err    ]),
    1.56 -    (                               [list], [OK list, Err    , Err    ]),
    1.57 -    (                         [list, list], [OK list, Err    , Err    ]),
    1.58 -    (                               [list], [OK list, OK list, Err    ]),
    1.59 -    (                [PrimT Integer, list], [OK list, OK list, Err    ]),
    1.60 -    (                                   [], [OK list, OK list, Err    ]),
    1.61 -    (                               [list], [OK list, OK list, Err    ]),
    1.62 -    (                         [list, list], [OK list, OK list, Err    ]),
    1.63 -    (                               [list], [OK list, OK list, OK list]),
    1.64 -    (                [PrimT Integer, list], [OK list, OK list, OK list]),
    1.65 -    (                                   [], [OK list, OK list, OK list]),
    1.66 -    (                               [list], [OK list, OK list, OK list]),
    1.67 -    (                         [list, list], [OK list, OK list, OK list]),
    1.68 -    (                         [PrimT Void], [OK list, OK list, OK list]),
    1.69 -    (                                   [], [OK list, OK list, OK list]),
    1.70 -    (                               [list], [OK list, OK list, OK list]),
    1.71 -    (                         [list, list], [OK list, OK list, OK list]),
    1.72 -    (                         [PrimT Void], [OK list, OK list, OK list])]"
    1.73 +    (                                   [], [OK Ctest, Err     , Err     ]),
    1.74 +    (                              [Clist], [OK Ctest, Err     , Err     ]),
    1.75 +    (                       [Clist, Clist], [OK Ctest, Err     , Err     ]),
    1.76 +    (                              [Clist], [OK Clist, Err     , Err     ]),
    1.77 +    (               [PrimT Integer, Clist], [OK Clist, Err     , Err     ]),
    1.78 +    (                                   [], [OK Clist, Err     , Err     ]),
    1.79 +    (                              [Clist], [OK Clist, Err     , Err     ]),
    1.80 +    (                       [Clist, Clist], [OK Clist, Err     , Err     ]),
    1.81 +    (                              [Clist], [OK Clist, OK Clist, Err     ]),
    1.82 +    (               [PrimT Integer, Clist], [OK Clist, OK Clist, Err     ]),
    1.83 +    (                                   [], [OK Clist, OK Clist, Err     ]),
    1.84 +    (                              [Clist], [OK Clist, OK Clist, Err     ]),
    1.85 +    (                       [Clist, Clist], [OK Clist, OK Clist, Err     ]),
    1.86 +    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
    1.87 +    (               [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]),
    1.88 +    (                                   [], [OK Clist, OK Clist, OK Clist]),
    1.89 +    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
    1.90 +    (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
    1.91 +    (                         [PrimT Void], [OK Clist, OK Clist, OK Clist]),
    1.92 +    (                                   [], [OK Clist, OK Clist, OK Clist]),
    1.93 +    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
    1.94 +    (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
    1.95 +    (                         [PrimT Void], [OK Clist, OK Clist, OK Clist])]"
    1.96 +
    1.97 +lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
    1.98 +  apply (simp add: check_bounded_def)
    1.99 +  apply (simp add: nat_number make_list_ins_def)
   1.100 +  apply (rule allI, rule impI)
   1.101 +  apply (elim pc_end pc_next pc_0)
   1.102 +  apply auto
   1.103 +  done
   1.104 +
   1.105 +lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)"
   1.106 +  apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)
   1.107 +  apply (unfold list_def)
   1.108 +  apply auto
   1.109 +  done
   1.110  
   1.111  lemma wt_makelist [simp]:
   1.112    "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   1.113 -  apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
   1.114 +  apply (simp add: wt_method_def)
   1.115 +  apply (simp add: make_list_ins_def phi_makelist_def)
   1.116    apply (simp add: wt_start_def nat_number)
   1.117    apply (simp add: wt_instr_def)
   1.118    apply clarify
   1.119 @@ -375,8 +406,8 @@
   1.120  section "Example for code generation: inferring method types"
   1.121  
   1.122  constdefs
   1.123 -  test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty List.list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
   1.124 -             exception_table \<Rightarrow> instr List.list \<Rightarrow> JVMType.state List.list"
   1.125 +  test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
   1.126 +             exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list"
   1.127    "test_kil G C pTs rT mxs mxl et instr ==
   1.128     (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
   1.129          start  = OK first#(replicate (size instr - 1) (OK None))