src/HOL/MicroJava/BV/BVExample.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40077 c8a9eaaa2f59
child 44035 322d1657c40c
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*  Title:      HOL/MicroJava/BV/BVExample.thy
     2     Author:     Gerwin Klein
     3 *)
     4 
     5 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
     6 
     7 theory BVExample
     8 imports
     9   "../JVM/JVMListExample"
    10   BVSpecTypeSafe
    11   JVM
    12   "~~/src/HOL/Library/Executable_Set"
    13 begin
    14 
    15 text {*
    16   This theory shows type correctness of the example program in section 
    17   \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
    18   explicitly providing a welltyping. It also shows that the start
    19   state of the program conforms to the welltyping; hence type safe
    20   execution is guaranteed.
    21 *}
    22 
    23 section "Setup"
    24 text {*
    25   Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
    26   anonymous, we describe distinctness of names in the example by axioms:
    27 *}
    28 axioms 
    29   distinct_classes: "list_nam \<noteq> test_nam"
    30   distinct_fields:  "val_nam \<noteq> next_nam"
    31 
    32 text {* Abbreviations for definitions we will have to use often in the
    33 proofs below: *}
    34 lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def 
    35 lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
    36                      OutOfMemoryC_def ClassCastC_def
    37 lemmas class_defs  = list_class_def test_class_def
    38 
    39 text {* These auxiliary proofs are for efficiency: class lookup,
    40 subclass relation, method and field lookup are computed only once:
    41 *}
    42 lemma class_Object [simp]:
    43   "class E Object = Some (undefined, [],[])"
    44   by (simp add: class_def system_defs E_def)
    45 
    46 lemma class_NullPointer [simp]:
    47   "class E (Xcpt NullPointer) = Some (Object, [], [])"
    48   by (simp add: class_def system_defs E_def)
    49 
    50 lemma class_OutOfMemory [simp]:
    51   "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
    52   by (simp add: class_def system_defs E_def)
    53 
    54 lemma class_ClassCast [simp]:
    55   "class E (Xcpt ClassCast) = Some (Object, [], [])"
    56   by (simp add: class_def system_defs E_def)
    57 
    58 lemma class_list [simp]:
    59   "class E list_name = Some list_class"
    60   by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
    61  
    62 lemma class_test [simp]:
    63   "class E test_name = Some test_class"
    64   by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
    65 
    66 lemma E_classes [simp]:
    67   "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, 
    68                         Xcpt ClassCast, Xcpt OutOfMemory, Object}"
    69   by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
    70 
    71 text {* The subclass releation spelled out: *}
    72 lemma subcls1:
    73   "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
    74                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
    75 apply (simp add: subcls1_def2)
    76 apply (simp add: name_defs class_defs system_defs E_def class_def)
    77 apply (simp add: Sigma_def)
    78 apply auto
    79 done
    80 
    81 text {* The subclass relation is acyclic; hence its converse is well founded: *}
    82 lemma notin_rtrancl:
    83   "(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False"
    84   by (auto elim: converse_rtranclE)
    85 
    86 lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
    87   apply (rule acyclicI)
    88   apply (simp add: subcls1)
    89   apply (auto dest!: tranclD)
    90   apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
    91   done
    92 
    93 lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
    94   apply (rule finite_acyclic_wf_converse)
    95   apply (simp add: subcls1 del: insert_iff)
    96   apply (rule acyclic_subcls1_E)
    97   done  
    98 
    99 text {* Method and field lookup: *}
   100 lemma method_Object [simp]:
   101   "method (E, Object) = Map.empty"
   102   by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
   103 
   104 lemma method_append [simp]:
   105   "method (E, list_name) (append_name, [Class list_name]) =
   106   Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
   107   apply (insert class_list)
   108   apply (unfold list_class_def)
   109   apply (drule method_rec_lemma [OF _ wf_subcls1_E])
   110   apply simp
   111   done
   112 
   113 lemma method_makelist [simp]:
   114   "method (E, test_name) (makelist_name, []) = 
   115   Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
   116   apply (insert class_test)
   117   apply (unfold test_class_def)
   118   apply (drule method_rec_lemma [OF _ wf_subcls1_E])
   119   apply simp
   120   done
   121 
   122 lemma field_val [simp]:
   123   "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
   124   apply (unfold TypeRel.field_def)
   125   apply (insert class_list)
   126   apply (unfold list_class_def)
   127   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   128   apply simp
   129   done
   130 
   131 lemma field_next [simp]:
   132   "field (E, list_name) next_name = Some (list_name, Class list_name)"
   133   apply (unfold TypeRel.field_def)
   134   apply (insert class_list)
   135   apply (unfold list_class_def)
   136   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   137   apply (simp add: name_defs distinct_fields [symmetric])
   138   done
   139 
   140 lemma [simp]: "fields (E, Object) = []"
   141    by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
   142  
   143 lemma [simp]: "fields (E, Xcpt NullPointer) = []"
   144   by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
   145 
   146 lemma [simp]: "fields (E, Xcpt ClassCast) = []"
   147   by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
   148 
   149 lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
   150   by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
   151 
   152 lemma [simp]: "fields (E, test_name) = []"
   153   apply (insert class_test)
   154   apply (unfold test_class_def)
   155   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   156   apply simp
   157   done
   158 
   159 lemmas [simp] = is_class_def
   160 
   161 text {*
   162   The next definition and three proof rules implement an algorithm to
   163   enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
   164   transforms a goal of the form
   165   @{prop [display] "pc < n \<Longrightarrow> P pc"} 
   166   into a series of goals
   167   @{prop [display] "P 0"} 
   168   @{prop [display] "P (Suc 0)"} 
   169 
   170   @{text "\<dots>"}
   171 
   172   @{prop [display] "P n"} 
   173 *}
   174 definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where
   175   "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
   176 
   177 lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   178   by (simp add: intervall_def)
   179 
   180 lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   181   apply (cases "x=n0")
   182   apply (auto simp add: intervall_def)
   183   done
   184 
   185 lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
   186   by (unfold intervall_def) arith
   187 
   188 
   189 section "Program structure"
   190 
   191 text {*
   192   The program is structurally wellformed:
   193 *}
   194 
   195 lemma wf_struct:
   196   "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
   197 proof -
   198   have "unique E" 
   199     by (simp add: system_defs E_def class_defs name_defs distinct_classes)
   200   moreover
   201   have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
   202   hence "wf_syscls E" by (rule wf_syscls)
   203   moreover
   204   have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
   205   moreover
   206   have "wf_cdecl ?mb E NullPointerC" 
   207     by (auto elim: notin_rtrancl 
   208             simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
   209   moreover
   210   have "wf_cdecl ?mb E ClassCastC" 
   211     by (auto elim: notin_rtrancl 
   212             simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
   213   moreover
   214   have "wf_cdecl ?mb E OutOfMemoryC" 
   215     by (auto elim: notin_rtrancl 
   216             simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
   217   moreover
   218   have "wf_cdecl ?mb E (list_name, list_class)"
   219     apply (auto elim!: notin_rtrancl 
   220             simp add: wf_cdecl_def wf_fdecl_def list_class_def 
   221                       wf_mdecl_def wf_mhead_def subcls1)
   222     apply (auto simp add: name_defs distinct_classes distinct_fields)
   223     done    
   224   moreover
   225   have "wf_cdecl ?mb E (test_name, test_class)" 
   226     apply (auto elim!: notin_rtrancl 
   227             simp add: wf_cdecl_def wf_fdecl_def test_class_def 
   228                       wf_mdecl_def wf_mhead_def subcls1)
   229     apply (auto simp add: name_defs distinct_classes distinct_fields)
   230     done       
   231   ultimately
   232   show ?thesis 
   233     by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
   234 qed
   235 
   236 section "Welltypings"
   237 text {*
   238   We show welltypings of the methods @{term append_name} in class @{term list_name}, 
   239   and @{term makelist_name} in class @{term test_name}:
   240 *}
   241 lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
   242 declare appInvoke [simp del]
   243 
   244 definition phi_append :: method_type ("\<phi>\<^sub>a") where
   245   "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
   246    (                                    [], [Class list_name, Class list_name]),
   247    (                     [Class list_name], [Class list_name, Class list_name]),
   248    (                     [Class list_name], [Class list_name, Class list_name]),
   249    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   250    ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
   251    (                     [Class list_name], [Class list_name, Class list_name]),
   252    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   253    (                          [PrimT Void], [Class list_name, Class list_name]),
   254    (                        [Class Object], [Class list_name, Class list_name]),
   255    (                                    [], [Class list_name, Class list_name]),
   256    (                     [Class list_name], [Class list_name, Class list_name]),
   257    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   258    (                                    [], [Class list_name, Class list_name]),
   259    (                          [PrimT Void], [Class list_name, Class list_name])]"
   260 
   261 
   262 lemma bounded_append [simp]:
   263   "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
   264   apply (simp add: check_bounded_def)
   265   apply (simp add: eval_nat_numeral append_ins_def)
   266   apply (rule allI, rule impI)
   267   apply (elim pc_end pc_next pc_0)
   268   apply auto
   269   done
   270 
   271 lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"
   272   apply (auto simp add: check_types_def phi_append_def JVM_states_unfold)
   273   apply (unfold list_def)
   274   apply auto
   275   done
   276   
   277 lemma wt_append [simp]:
   278   "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
   279              [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
   280   apply (simp add: wt_method_def wt_start_def wt_instr_def)
   281   apply (simp add: phi_append_def append_ins_def)
   282   apply clarify
   283   apply (elim pc_end pc_next pc_0)
   284   apply simp
   285   apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
   286   apply simp
   287   apply simp
   288   apply (fastsimp simp add: sup_state_conv subcls1)
   289   apply simp
   290   apply (simp add: app_def xcpt_app_def)
   291   apply simp
   292   apply simp
   293   apply simp
   294   apply (simp add: match_exception_entry_def)
   295   apply (simp add: match_exception_entry_def)
   296   apply simp
   297   apply simp
   298   done
   299 
   300 text {* Some abbreviations for readability *} 
   301 abbreviation Clist :: ty 
   302   where "Clist == Class list_name"
   303 abbreviation Ctest :: ty
   304   where "Ctest == Class test_name"
   305 
   306 definition phi_makelist :: method_type ("\<phi>\<^sub>m") where
   307   "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
   308     (                                   [], [OK Ctest, Err     , Err     ]),
   309     (                              [Clist], [OK Ctest, Err     , Err     ]),
   310     (                       [Clist, Clist], [OK Ctest, Err     , Err     ]),
   311     (                              [Clist], [OK Clist, Err     , Err     ]),
   312     (               [PrimT Integer, Clist], [OK Clist, Err     , Err     ]),
   313     (                                   [], [OK Clist, Err     , Err     ]),
   314     (                              [Clist], [OK Clist, Err     , Err     ]),
   315     (                       [Clist, Clist], [OK Clist, Err     , Err     ]),
   316     (                              [Clist], [OK Clist, OK Clist, Err     ]),
   317     (               [PrimT Integer, Clist], [OK Clist, OK Clist, Err     ]),
   318     (                                   [], [OK Clist, OK Clist, Err     ]),
   319     (                              [Clist], [OK Clist, OK Clist, Err     ]),
   320     (                       [Clist, Clist], [OK Clist, OK Clist, Err     ]),
   321     (                              [Clist], [OK Clist, OK Clist, OK Clist]),
   322     (               [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]),
   323     (                                   [], [OK Clist, OK Clist, OK Clist]),
   324     (                              [Clist], [OK Clist, OK Clist, OK Clist]),
   325     (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
   326     (                         [PrimT Void], [OK Clist, OK Clist, OK Clist]),
   327     (                                   [], [OK Clist, OK Clist, OK Clist]),
   328     (                              [Clist], [OK Clist, OK Clist, OK Clist]),
   329     (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
   330     (                         [PrimT Void], [OK Clist, OK Clist, OK Clist])]"
   331 
   332 lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
   333   apply (simp add: check_bounded_def)
   334   apply (simp add: eval_nat_numeral make_list_ins_def)
   335   apply (rule allI, rule impI)
   336   apply (elim pc_end pc_next pc_0)
   337   apply auto
   338   done
   339 
   340 lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)"
   341   apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)
   342   apply (unfold list_def)
   343   apply auto
   344   done
   345 
   346 lemma wt_makelist [simp]:
   347   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   348   apply (simp add: wt_method_def)
   349   apply (simp add: make_list_ins_def phi_makelist_def)
   350   apply (simp add: wt_start_def eval_nat_numeral)
   351   apply (simp add: wt_instr_def)
   352   apply clarify
   353   apply (elim pc_end pc_next pc_0)
   354   apply (simp add: match_exception_entry_def)
   355   apply simp
   356   apply simp
   357   apply simp
   358   apply (simp add: match_exception_entry_def)
   359   apply (simp add: match_exception_entry_def) 
   360   apply simp
   361   apply simp
   362   apply simp
   363   apply (simp add: match_exception_entry_def)
   364   apply (simp add: match_exception_entry_def) 
   365   apply simp
   366   apply simp
   367   apply simp
   368   apply (simp add: match_exception_entry_def)
   369   apply (simp add: match_exception_entry_def) 
   370   apply simp
   371   apply (simp add: app_def xcpt_app_def)
   372   apply simp 
   373   apply simp
   374   apply simp
   375   apply (simp add: app_def xcpt_app_def) 
   376   apply simp
   377   done
   378 
   379 text {* The whole program is welltyped: *}
   380 definition Phi :: prog_type ("\<Phi>") where
   381   "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
   382              if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
   383 
   384 lemma wf_prog:
   385   "wt_jvm_prog E \<Phi>" 
   386   apply (unfold wt_jvm_prog_def)
   387   apply (rule wf_mb'E [OF wf_struct])
   388   apply (simp add: E_def)
   389   apply clarify
   390   apply (fold E_def)
   391   apply (simp add: system_defs class_defs Phi_def) 
   392   apply auto
   393   done 
   394 
   395 
   396 section "Conformance"
   397 text {* Execution of the program will be typesafe, because its
   398   start state conforms to the welltyping: *}
   399 
   400 lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
   401   apply (rule BV_correct_initial)
   402     apply (rule wf_prog)
   403    apply simp
   404   apply simp
   405   done
   406 
   407 
   408 section "Example for code generation: inferring method types"
   409 
   410 definition test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
   411              exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list" where
   412   "test_kil G C pTs rT mxs mxl et instr =
   413    (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
   414         start  = OK first#(replicate (size instr - 1) (OK None))
   415     in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
   416 
   417 lemma [code]:
   418   "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
   419   apply (unfold unstables_def)
   420   apply (rule equalityI)
   421   apply (rule subsetI)
   422   apply (erule CollectE)
   423   apply (erule conjE)
   424   apply (rule UN_I)
   425   apply simp
   426   apply simp
   427   apply (rule subsetI)
   428   apply (erule UN_E)
   429   apply (case_tac "\<not> stable r step ss p")
   430   apply simp+
   431   done
   432 
   433 definition some_elem :: "'a set \<Rightarrow> 'a" where
   434   "some_elem = (%S. SOME x. x : S)"
   435 
   436 consts_code
   437   "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
   438 
   439 text {* This code setup is just a demonstration and \emph{not} sound! *}
   440 
   441 lemma False
   442 proof -
   443   have "some_elem (set [False, True]) = False"
   444     by evaluation
   445   moreover have "some_elem (set [True, False]) = True"
   446     by evaluation
   447   ultimately show False
   448     by (simp add: some_elem_def)
   449 qed
   450 
   451 lemma [code]:
   452   "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
   453     (\<lambda>(ss, w).
   454         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
   455     (ss, w)"
   456   unfolding iter_def More_Set.is_empty_def some_elem_def ..
   457 
   458 lemma JVM_sup_unfold [code]:
   459  "JVMType.sup S m n = lift2 (Opt.sup
   460        (Product.sup (Listn.sup (JType.sup S))
   461          (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" 
   462   apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def
   463          stk_esl_def reg_sl_def Product.esl_def  
   464          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
   465   by simp
   466 
   467 lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
   468 
   469 lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
   470 
   471 code_module BV
   472 contains
   473   test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
   474     [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
   475   test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
   476 ML BV.test1
   477 ML BV.test2
   478 
   479 end