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