src/HOL/MicroJava/BV/BVExample.thy
changeset 12951 a9fdcb71d252
child 12972 da7345ff18e1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Feb 26 15:45:32 2002 +0100
     1.3 @@ -0,0 +1,377 @@
     1.4 +(*  Title:      HOL/MicroJava/BV/BVExample.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gerwin Klein
     1.7 +*)
     1.8 +
     1.9 +header {* Example Welltypings *}
    1.10 +
    1.11 +theory BVExample = JVMListExample + Correct:
    1.12 +
    1.13 +section "Setup"
    1.14 +text {*
    1.15 +  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
    1.16 +  anonymous, we describe distinctness of names in the example by axioms:
    1.17 +*}
    1.18 +axioms 
    1.19 +  distinct_classes: "list_nam \<noteq> test_nam"
    1.20 +  distinct_fields:  "val_nam \<noteq> next_nam"
    1.21 +
    1.22 +text {* Shorthands for definitions we will have to use often in the
    1.23 +proofs below: *}
    1.24 +lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
    1.25 +lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
    1.26 +                     OutOfMemoryC_def ClassCastC_def
    1.27 +lemmas class_defs  = list_class_def test_class_def
    1.28 +
    1.29 +text {* These auxiliary proofs are for efficiency: class lookup,
    1.30 +subclass relation, method and field lookup are computed only once:
    1.31 +*}
    1.32 +lemma class_Object [simp]:
    1.33 +  "class E Object = Some (arbitrary, [],[])"
    1.34 +  by (simp add: class_def system_defs E_def)
    1.35 +
    1.36 +lemma class_NullPointer [simp]:
    1.37 +  "class E (Xcpt NullPointer) = Some (Object, [], [])"
    1.38 +  by (simp add: class_def system_defs E_def)
    1.39 +
    1.40 +lemma class_OutOfMemory [simp]:
    1.41 +  "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
    1.42 +  by (simp add: class_def system_defs E_def)
    1.43 +
    1.44 +lemma class_ClassCast [simp]:
    1.45 +  "class E (Xcpt ClassCast) = Some (Object, [], [])"
    1.46 +  by (simp add: class_def system_defs E_def)
    1.47 +
    1.48 +lemma class_list [simp]:
    1.49 +  "class E list_name = Some list_class"
    1.50 +  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
    1.51 + 
    1.52 +lemma class_test [simp]:
    1.53 +  "class E test_name = Some test_class"
    1.54 +  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
    1.55 +
    1.56 +lemma E_classes [simp]:
    1.57 +  "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, 
    1.58 +                        Xcpt ClassCast, Xcpt OutOfMemory, Object}"
    1.59 +  by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
    1.60 +
    1.61 +text {* The subclass releation spelled out: *}
    1.62 +lemma subcls1:
    1.63 +  "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
    1.64 +                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
    1.65 +  apply (simp add: subcls1_def2)
    1.66 +  apply (simp add: name_defs class_defs system_defs E_def class_def)
    1.67 +  apply (auto split: split_if_asm)
    1.68 +  done
    1.69 +
    1.70 +text {* The subclass relation is acyclic; hence its converse is well founded: *}
    1.71 +lemma notin_rtrancl:
    1.72 +  "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
    1.73 +  by (auto elim: converse_rtranclE)  
    1.74 +
    1.75 +lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
    1.76 +  apply (rule acyclicI)
    1.77 +  apply (simp add: subcls1)
    1.78 +  apply (auto dest!: tranclD)
    1.79 +  apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
    1.80 +  done
    1.81 +
    1.82 +lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
    1.83 +  apply (rule finite_acyclic_wf_converse)
    1.84 +  apply (simp add: subcls1)
    1.85 +  apply (rule acyclic_subcls1_E)
    1.86 +  done  
    1.87 +
    1.88 +text {* Method and field lookup: *}
    1.89 +lemma method_Object [simp]:
    1.90 +  "method (E, Object) = empty"
    1.91 +  by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
    1.92 +
    1.93 +lemma method_append [simp]:
    1.94 +  "method (E, list_name) (append_name, [Class list_name]) =
    1.95 +  Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
    1.96 +  apply (insert class_list)
    1.97 +  apply (unfold list_class_def)
    1.98 +  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
    1.99 +  apply simp
   1.100 +  done
   1.101 +
   1.102 +lemma method_makelist [simp]:
   1.103 +  "method (E, test_name) (makelist_name, []) = 
   1.104 +  Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
   1.105 +  apply (insert class_test)
   1.106 +  apply (unfold test_class_def)
   1.107 +  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
   1.108 +  apply simp
   1.109 +  done
   1.110 +
   1.111 +lemma field_val [simp]:
   1.112 +  "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
   1.113 +  apply (unfold field_def)
   1.114 +  apply (insert class_list)
   1.115 +  apply (unfold list_class_def)
   1.116 +  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   1.117 +  apply simp
   1.118 +  done
   1.119 +
   1.120 +lemma field_next [simp]:
   1.121 +  "field (E, list_name) next_name = Some (list_name, Class list_name)"
   1.122 +  apply (unfold field_def)
   1.123 +  apply (insert class_list)
   1.124 +  apply (unfold list_class_def)
   1.125 +  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   1.126 +  apply (simp add: name_defs distinct_fields [symmetric])
   1.127 +  done
   1.128 +
   1.129 +lemma [simp]: "fields (E, Object) = []"
   1.130 +   by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
   1.131 + 
   1.132 +lemma [simp]: "fields (E, Xcpt NullPointer) = []"
   1.133 +  by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
   1.134 +
   1.135 +lemma [simp]: "fields (E, Xcpt ClassCast) = []"
   1.136 +  by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
   1.137 +
   1.138 +lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
   1.139 +  by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
   1.140 +
   1.141 +lemma [simp]: "fields (E, test_name) = []"
   1.142 +  apply (insert class_test)
   1.143 +  apply (unfold test_class_def)
   1.144 +  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   1.145 +  apply simp
   1.146 +  done
   1.147 +
   1.148 +lemmas [simp] = is_class_def
   1.149 +
   1.150 +text {*
   1.151 +  The next definition and three proof rules implement an algorithm to
   1.152 +  enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
   1.153 +  transforms a goal of the form
   1.154 +  @{prop [display] "pc < n \<Longrightarrow> P pc"} 
   1.155 +  into a series of goals
   1.156 +  @{prop [display] "P 0"} 
   1.157 +  @{prop [display] "P (Suc 0)"} 
   1.158 +
   1.159 +  @{text "\<dots>"}
   1.160 +
   1.161 +  @{prop [display] "P n"} 
   1.162 +*}
   1.163 +constdefs 
   1.164 +  intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
   1.165 +  "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
   1.166 +
   1.167 +lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   1.168 +  by (simp add: intervall_def)
   1.169 +
   1.170 +lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   1.171 +  apply (cases "x=n0")
   1.172 +  apply (auto simp add: intervall_def) 
   1.173 +  apply arith
   1.174 +  done
   1.175 +
   1.176 +lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
   1.177 +  by (unfold intervall_def) arith
   1.178 +
   1.179 +
   1.180 +section "Program structure"
   1.181 +
   1.182 +text {*
   1.183 +  The program is structurally wellformed:
   1.184 +*}
   1.185 +lemma wf_struct:
   1.186 +  "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
   1.187 +proof -
   1.188 +  have "unique E" 
   1.189 +    by (simp add: system_defs E_def class_defs name_defs distinct_classes)
   1.190 +  moreover
   1.191 +  have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
   1.192 +  hence "wf_syscls E" by (rule wf_syscls)
   1.193 +  moreover
   1.194 +  have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
   1.195 +  moreover
   1.196 +  have "wf_cdecl ?mb E NullPointerC" 
   1.197 +    by (auto elim: notin_rtrancl 
   1.198 +            simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
   1.199 +  moreover
   1.200 +  have "wf_cdecl ?mb E ClassCastC" 
   1.201 +    by (auto elim: notin_rtrancl 
   1.202 +            simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
   1.203 +  moreover
   1.204 +  have "wf_cdecl ?mb E OutOfMemoryC" 
   1.205 +    by (auto elim: notin_rtrancl 
   1.206 +            simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
   1.207 +  moreover
   1.208 +  have "wf_cdecl ?mb E (list_name, list_class)"
   1.209 +    apply (auto elim!: notin_rtrancl 
   1.210 +            simp add: wf_cdecl_def wf_fdecl_def list_class_def 
   1.211 +                      wf_mdecl_def wf_mhead_def subcls1)
   1.212 +    apply (auto simp add: name_defs distinct_classes distinct_fields)
   1.213 +    done    
   1.214 +  moreover
   1.215 +  have "wf_cdecl ?mb E (test_name, test_class)" 
   1.216 +    apply (auto elim!: notin_rtrancl 
   1.217 +            simp add: wf_cdecl_def wf_fdecl_def test_class_def 
   1.218 +                      wf_mdecl_def wf_mhead_def subcls1)
   1.219 +    apply (auto simp add: name_defs distinct_classes distinct_fields)
   1.220 +    done       
   1.221 +  ultimately
   1.222 +  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
   1.223 +qed
   1.224 +
   1.225 +section "Welltypings"
   1.226 +text {*
   1.227 +  We show welltypings of the methods @{term append_name} in class @{term list_name}, 
   1.228 +  and @{term makelist_name} in class @{term test_name}:
   1.229 +*}
   1.230 +lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
   1.231 +declare appInvoke [simp del]
   1.232 +
   1.233 +constdefs
   1.234 +  phi_append :: method_type ("\<phi>\<^sub>a")
   1.235 +  "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
   1.236 +   (                                    [], [Class list_name, Class list_name]),
   1.237 +   (                     [Class list_name], [Class list_name, Class list_name]),
   1.238 +   (                     [Class list_name], [Class list_name, Class list_name]),
   1.239 +   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   1.240 +   ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
   1.241 +   (                     [Class list_name], [Class list_name, Class list_name]),
   1.242 +   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   1.243 +   (                          [PrimT Void], [Class list_name, Class list_name]),
   1.244 +   (                        [Class Object], [Class list_name, Class list_name]),
   1.245 +   (                                    [], [Class list_name, Class list_name]),
   1.246 +   (                     [Class list_name], [Class list_name, Class list_name]),
   1.247 +   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   1.248 +   (                                    [], [Class list_name, Class list_name]),
   1.249 +   (                          [PrimT Void], [Class list_name, Class list_name])]"
   1.250 +
   1.251 +lemma wt_append [simp]:
   1.252 +  "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
   1.253 +             [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
   1.254 +  apply (simp add: wt_method_def append_ins_def phi_append_def 
   1.255 +                   wt_start_def wt_instr_def)
   1.256 +  apply clarify
   1.257 +  apply (elim pc_end pc_next pc_0)
   1.258 +  apply simp
   1.259 +  apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
   1.260 +  apply simp
   1.261 +  apply simp
   1.262 +  apply (fastsimp simp add: sup_state_conv subcls1)
   1.263 +  apply simp
   1.264 +  apply (simp add: app_def xcpt_app_def)
   1.265 +  apply simp
   1.266 +  apply simp
   1.267 +  apply simp
   1.268 +  apply (simp add: match_exception_entry_def)
   1.269 +  apply (simp add: match_exception_entry_def)
   1.270 +  apply simp
   1.271 +  apply simp
   1.272 +  done
   1.273 +
   1.274 +text {* Some shorthands to make the welltyping of method @{term
   1.275 +makelist_name} easier to read *} 
   1.276 +syntax
   1.277 +  list :: ty 
   1.278 +  test :: ty
   1.279 +translations
   1.280 +  "list" == "Class list_name"
   1.281 +  "test" == "Class test_name"
   1.282 +
   1.283 +constdefs
   1.284 +  phi_makelist :: method_type ("\<phi>\<^sub>m")
   1.285 +  "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
   1.286 +    (                                   [], [OK test, Err    , Err    ]),
   1.287 +    (                               [list], [OK test, Err    , Err    ]),
   1.288 +    (                         [list, list], [OK test, Err    , Err    ]),
   1.289 +    (                               [list], [OK list, Err    , Err    ]),
   1.290 +    (                [PrimT Integer, list], [OK list, Err    , Err    ]),
   1.291 +    (                                   [], [OK list, Err    , Err    ]),
   1.292 +    (                               [list], [OK list, Err    , Err    ]),
   1.293 +    (                         [list, list], [OK list, Err    , Err    ]),
   1.294 +    (                               [list], [OK list, OK list, Err    ]),
   1.295 +    (                [PrimT Integer, list], [OK list, OK list, Err    ]),
   1.296 +    (                                   [], [OK list, OK list, Err    ]),
   1.297 +    (                               [list], [OK list, OK list, Err    ]),
   1.298 +    (                         [list, list], [OK list, OK list, Err    ]),
   1.299 +    (                               [list], [OK list, OK list, OK list]),
   1.300 +    (                [PrimT Integer, list], [OK list, OK list, OK list]),
   1.301 +    (                                   [], [OK list, OK list, OK list]),
   1.302 +    (                               [list], [OK list, OK list, OK list]),
   1.303 +    (                         [list, list], [OK list, OK list, OK list]),
   1.304 +    (                         [PrimT Void], [OK list, OK list, OK list]),
   1.305 +    (                   [list, PrimT Void], [OK list, OK list, OK list]),
   1.306 +    (             [list, list, PrimT Void], [OK list, OK list, OK list]),
   1.307 +    (             [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
   1.308 +    ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
   1.309 +
   1.310 +lemma wt_makelist [simp]:
   1.311 +  "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   1.312 +  apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
   1.313 +  apply (simp add: wt_start_def nat_number_of)
   1.314 +  apply (simp add: wt_instr_def)
   1.315 +  apply clarify
   1.316 +  apply (elim pc_end pc_next pc_0)
   1.317 +  apply (simp add: match_exception_entry_def)
   1.318 +  apply simp
   1.319 +  apply simp
   1.320 +  apply simp
   1.321 +  apply (simp add: match_exception_entry_def)
   1.322 +  apply (simp add: match_exception_entry_def) 
   1.323 +  apply simp
   1.324 +  apply simp
   1.325 +  apply simp
   1.326 +  apply (simp add: match_exception_entry_def)
   1.327 +  apply (simp add: match_exception_entry_def) 
   1.328 +  apply simp
   1.329 +  apply simp
   1.330 +  apply simp
   1.331 +  apply (simp add: match_exception_entry_def)
   1.332 +  apply (simp add: match_exception_entry_def) 
   1.333 +  apply simp
   1.334 +  apply (simp add: app_def xcpt_app_def)
   1.335 +  apply simp
   1.336 +  apply simp
   1.337 +  apply (simp add: app_def xcpt_app_def)
   1.338 +  apply simp
   1.339 +  apply simp
   1.340 +  done
   1.341 +
   1.342 +text {* The whole program is welltyped: *}
   1.343 +constdefs 
   1.344 +  Phi :: prog_type ("\<Phi>")
   1.345 +  "\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
   1.346 +              if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
   1.347 +  
   1.348 +lemma wf_prog:
   1.349 +  "wt_jvm_prog E \<Phi>"
   1.350 +  apply (unfold wt_jvm_prog_def)
   1.351 +  apply (rule wf_mb'E [OF wf_struct])
   1.352 +  apply (simp add: E_def)
   1.353 +  apply clarify
   1.354 +  apply (fold E_def)
   1.355 +  apply (simp add: system_defs class_defs Phi_def)
   1.356 +  apply auto
   1.357 +  done
   1.358 +
   1.359 +
   1.360 +section "Conformance"
   1.361 +text {* Execution of the program will be typesafe, because its
   1.362 +  start state conforms to the welltyping: *}
   1.363 +
   1.364 +lemma [simp]: "preallocated start_heap"
   1.365 +  apply (unfold start_heap_def preallocated_def)
   1.366 +  apply auto
   1.367 +  apply (case_tac x)
   1.368 +  apply auto
   1.369 +  done
   1.370 +
   1.371 +lemma "E,\<Phi> \<turnstile>JVM start_state \<surd>"
   1.372 +  apply (simp add: correct_state_def start_state_def test_class_def)
   1.373 +  apply (simp add: hconf_def start_heap_def oconf_def lconf_def)
   1.374 +  apply (simp add: Phi_def phi_makelist_def)
   1.375 +  apply (simp add: correct_frame_def)
   1.376 +  apply (simp add: make_list_ins_def)
   1.377 +  apply (simp add: conf_def start_heap_def)
   1.378 +  done
   1.379 +
   1.380 +end
   1.381 \ No newline at end of file