src/HOL/MicroJava/BV/BVExample.thy
author kleing
Tue Feb 26 15:45:32 2002 +0100 (2002-02-26)
changeset 12951 a9fdcb71d252
child 12972 da7345ff18e1
permissions -rw-r--r--
introduces SystemClasses and BVExample
     1 (*  Title:      HOL/MicroJava/BV/BVExample.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4 *)
     5 
     6 header {* Example Welltypings *}
     7 
     8 theory BVExample = JVMListExample + Correct:
     9 
    10 section "Setup"
    11 text {*
    12   Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
    13   anonymous, we describe distinctness of names in the example by axioms:
    14 *}
    15 axioms 
    16   distinct_classes: "list_nam \<noteq> test_nam"
    17   distinct_fields:  "val_nam \<noteq> next_nam"
    18 
    19 text {* Shorthands for definitions we will have to use often in the
    20 proofs below: *}
    21 lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
    22 lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
    23                      OutOfMemoryC_def ClassCastC_def
    24 lemmas class_defs  = list_class_def test_class_def
    25 
    26 text {* These auxiliary proofs are for efficiency: class lookup,
    27 subclass relation, method and field lookup are computed only once:
    28 *}
    29 lemma class_Object [simp]:
    30   "class E Object = Some (arbitrary, [],[])"
    31   by (simp add: class_def system_defs E_def)
    32 
    33 lemma class_NullPointer [simp]:
    34   "class E (Xcpt NullPointer) = Some (Object, [], [])"
    35   by (simp add: class_def system_defs E_def)
    36 
    37 lemma class_OutOfMemory [simp]:
    38   "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
    39   by (simp add: class_def system_defs E_def)
    40 
    41 lemma class_ClassCast [simp]:
    42   "class E (Xcpt ClassCast) = Some (Object, [], [])"
    43   by (simp add: class_def system_defs E_def)
    44 
    45 lemma class_list [simp]:
    46   "class E list_name = Some list_class"
    47   by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
    48  
    49 lemma class_test [simp]:
    50   "class E test_name = Some test_class"
    51   by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
    52 
    53 lemma E_classes [simp]:
    54   "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, 
    55                         Xcpt ClassCast, Xcpt OutOfMemory, Object}"
    56   by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
    57 
    58 text {* The subclass releation spelled out: *}
    59 lemma subcls1:
    60   "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
    61                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
    62   apply (simp add: subcls1_def2)
    63   apply (simp add: name_defs class_defs system_defs E_def class_def)
    64   apply (auto split: split_if_asm)
    65   done
    66 
    67 text {* The subclass relation is acyclic; hence its converse is well founded: *}
    68 lemma notin_rtrancl:
    69   "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
    70   by (auto elim: converse_rtranclE)  
    71 
    72 lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
    73   apply (rule acyclicI)
    74   apply (simp add: subcls1)
    75   apply (auto dest!: tranclD)
    76   apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
    77   done
    78 
    79 lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
    80   apply (rule finite_acyclic_wf_converse)
    81   apply (simp add: subcls1)
    82   apply (rule acyclic_subcls1_E)
    83   done  
    84 
    85 text {* Method and field lookup: *}
    86 lemma method_Object [simp]:
    87   "method (E, Object) = empty"
    88   by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
    89 
    90 lemma method_append [simp]:
    91   "method (E, list_name) (append_name, [Class list_name]) =
    92   Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
    93   apply (insert class_list)
    94   apply (unfold list_class_def)
    95   apply (drule method_rec_lemma [OF _ wf_subcls1_E])
    96   apply simp
    97   done
    98 
    99 lemma method_makelist [simp]:
   100   "method (E, test_name) (makelist_name, []) = 
   101   Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
   102   apply (insert class_test)
   103   apply (unfold test_class_def)
   104   apply (drule method_rec_lemma [OF _ wf_subcls1_E])
   105   apply simp
   106   done
   107 
   108 lemma field_val [simp]:
   109   "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
   110   apply (unfold field_def)
   111   apply (insert class_list)
   112   apply (unfold list_class_def)
   113   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   114   apply simp
   115   done
   116 
   117 lemma field_next [simp]:
   118   "field (E, list_name) next_name = Some (list_name, Class list_name)"
   119   apply (unfold field_def)
   120   apply (insert class_list)
   121   apply (unfold list_class_def)
   122   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   123   apply (simp add: name_defs distinct_fields [symmetric])
   124   done
   125 
   126 lemma [simp]: "fields (E, Object) = []"
   127    by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
   128  
   129 lemma [simp]: "fields (E, Xcpt NullPointer) = []"
   130   by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
   131 
   132 lemma [simp]: "fields (E, Xcpt ClassCast) = []"
   133   by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
   134 
   135 lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
   136   by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
   137 
   138 lemma [simp]: "fields (E, test_name) = []"
   139   apply (insert class_test)
   140   apply (unfold test_class_def)
   141   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
   142   apply simp
   143   done
   144 
   145 lemmas [simp] = is_class_def
   146 
   147 text {*
   148   The next definition and three proof rules implement an algorithm to
   149   enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
   150   transforms a goal of the form
   151   @{prop [display] "pc < n \<Longrightarrow> P pc"} 
   152   into a series of goals
   153   @{prop [display] "P 0"} 
   154   @{prop [display] "P (Suc 0)"} 
   155 
   156   @{text "\<dots>"}
   157 
   158   @{prop [display] "P n"} 
   159 *}
   160 constdefs 
   161   intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
   162   "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
   163 
   164 lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   165   by (simp add: intervall_def)
   166 
   167 lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   168   apply (cases "x=n0")
   169   apply (auto simp add: intervall_def) 
   170   apply arith
   171   done
   172 
   173 lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
   174   by (unfold intervall_def) arith
   175 
   176 
   177 section "Program structure"
   178 
   179 text {*
   180   The program is structurally wellformed:
   181 *}
   182 lemma wf_struct:
   183   "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
   184 proof -
   185   have "unique E" 
   186     by (simp add: system_defs E_def class_defs name_defs distinct_classes)
   187   moreover
   188   have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
   189   hence "wf_syscls E" by (rule wf_syscls)
   190   moreover
   191   have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
   192   moreover
   193   have "wf_cdecl ?mb E NullPointerC" 
   194     by (auto elim: notin_rtrancl 
   195             simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
   196   moreover
   197   have "wf_cdecl ?mb E ClassCastC" 
   198     by (auto elim: notin_rtrancl 
   199             simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
   200   moreover
   201   have "wf_cdecl ?mb E OutOfMemoryC" 
   202     by (auto elim: notin_rtrancl 
   203             simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
   204   moreover
   205   have "wf_cdecl ?mb E (list_name, list_class)"
   206     apply (auto elim!: notin_rtrancl 
   207             simp add: wf_cdecl_def wf_fdecl_def list_class_def 
   208                       wf_mdecl_def wf_mhead_def subcls1)
   209     apply (auto simp add: name_defs distinct_classes distinct_fields)
   210     done    
   211   moreover
   212   have "wf_cdecl ?mb E (test_name, test_class)" 
   213     apply (auto elim!: notin_rtrancl 
   214             simp add: wf_cdecl_def wf_fdecl_def test_class_def 
   215                       wf_mdecl_def wf_mhead_def subcls1)
   216     apply (auto simp add: name_defs distinct_classes distinct_fields)
   217     done       
   218   ultimately
   219   show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
   220 qed
   221 
   222 section "Welltypings"
   223 text {*
   224   We show welltypings of the methods @{term append_name} in class @{term list_name}, 
   225   and @{term makelist_name} in class @{term test_name}:
   226 *}
   227 lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
   228 declare appInvoke [simp del]
   229 
   230 constdefs
   231   phi_append :: method_type ("\<phi>\<^sub>a")
   232   "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
   233    (                                    [], [Class list_name, Class list_name]),
   234    (                     [Class list_name], [Class list_name, Class list_name]),
   235    (                     [Class list_name], [Class list_name, Class list_name]),
   236    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   237    ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
   238    (                     [Class list_name], [Class list_name, Class list_name]),
   239    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
   240    (                          [PrimT Void], [Class list_name, Class list_name]),
   241    (                        [Class Object], [Class list_name, Class list_name]),
   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, Class list_name]),
   245    (                                    [], [Class list_name, Class list_name]),
   246    (                          [PrimT Void], [Class list_name, Class list_name])]"
   247 
   248 lemma wt_append [simp]:
   249   "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
   250              [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
   251   apply (simp add: wt_method_def append_ins_def phi_append_def 
   252                    wt_start_def wt_instr_def)
   253   apply clarify
   254   apply (elim pc_end pc_next pc_0)
   255   apply simp
   256   apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
   257   apply simp
   258   apply simp
   259   apply (fastsimp simp add: sup_state_conv subcls1)
   260   apply simp
   261   apply (simp add: app_def xcpt_app_def)
   262   apply simp
   263   apply simp
   264   apply simp
   265   apply (simp add: match_exception_entry_def)
   266   apply (simp add: match_exception_entry_def)
   267   apply simp
   268   apply simp
   269   done
   270 
   271 text {* Some shorthands to make the welltyping of method @{term
   272 makelist_name} easier to read *} 
   273 syntax
   274   list :: ty 
   275   test :: ty
   276 translations
   277   "list" == "Class list_name"
   278   "test" == "Class test_name"
   279 
   280 constdefs
   281   phi_makelist :: method_type ("\<phi>\<^sub>m")
   282   "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
   283     (                                   [], [OK test, Err    , Err    ]),
   284     (                               [list], [OK test, Err    , Err    ]),
   285     (                         [list, list], [OK test, Err    , Err    ]),
   286     (                               [list], [OK list, Err    , Err    ]),
   287     (                [PrimT Integer, list], [OK list, Err    , Err    ]),
   288     (                                   [], [OK list, Err    , Err    ]),
   289     (                               [list], [OK list, Err    , Err    ]),
   290     (                         [list, list], [OK list, Err    , Err    ]),
   291     (                               [list], [OK list, OK list, Err    ]),
   292     (                [PrimT Integer, list], [OK list, OK list, Err    ]),
   293     (                                   [], [OK list, OK list, Err    ]),
   294     (                               [list], [OK list, OK list, Err    ]),
   295     (                         [list, list], [OK list, OK list, Err    ]),
   296     (                               [list], [OK list, OK list, OK list]),
   297     (                [PrimT Integer, list], [OK list, OK list, OK list]),
   298     (                                   [], [OK list, OK list, OK list]),
   299     (                               [list], [OK list, OK list, OK list]),
   300     (                         [list, list], [OK list, OK list, OK list]),
   301     (                         [PrimT Void], [OK list, OK list, OK list]),
   302     (                   [list, PrimT Void], [OK list, OK list, OK list]),
   303     (             [list, list, PrimT Void], [OK list, OK list, OK list]),
   304     (             [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
   305     ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
   306 
   307 lemma wt_makelist [simp]:
   308   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   309   apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
   310   apply (simp add: wt_start_def nat_number_of)
   311   apply (simp add: wt_instr_def)
   312   apply clarify
   313   apply (elim pc_end pc_next pc_0)
   314   apply (simp add: match_exception_entry_def)
   315   apply simp
   316   apply simp
   317   apply simp
   318   apply (simp add: match_exception_entry_def)
   319   apply (simp add: match_exception_entry_def) 
   320   apply simp
   321   apply simp
   322   apply simp
   323   apply (simp add: match_exception_entry_def)
   324   apply (simp add: match_exception_entry_def) 
   325   apply simp
   326   apply simp
   327   apply simp
   328   apply (simp add: match_exception_entry_def)
   329   apply (simp add: match_exception_entry_def) 
   330   apply simp
   331   apply (simp add: app_def xcpt_app_def)
   332   apply simp
   333   apply simp
   334   apply (simp add: app_def xcpt_app_def)
   335   apply simp
   336   apply simp
   337   done
   338 
   339 text {* The whole program is welltyped: *}
   340 constdefs 
   341   Phi :: prog_type ("\<Phi>")
   342   "\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
   343               if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
   344   
   345 lemma wf_prog:
   346   "wt_jvm_prog E \<Phi>"
   347   apply (unfold wt_jvm_prog_def)
   348   apply (rule wf_mb'E [OF wf_struct])
   349   apply (simp add: E_def)
   350   apply clarify
   351   apply (fold E_def)
   352   apply (simp add: system_defs class_defs Phi_def)
   353   apply auto
   354   done
   355 
   356 
   357 section "Conformance"
   358 text {* Execution of the program will be typesafe, because its
   359   start state conforms to the welltyping: *}
   360 
   361 lemma [simp]: "preallocated start_heap"
   362   apply (unfold start_heap_def preallocated_def)
   363   apply auto
   364   apply (case_tac x)
   365   apply auto
   366   done
   367 
   368 lemma "E,\<Phi> \<turnstile>JVM start_state \<surd>"
   369   apply (simp add: correct_state_def start_state_def test_class_def)
   370   apply (simp add: hconf_def start_heap_def oconf_def lconf_def)
   371   apply (simp add: Phi_def phi_makelist_def)
   372   apply (simp add: correct_frame_def)
   373   apply (simp add: make_list_ins_def)
   374   apply (simp add: conf_def start_heap_def)
   375   done
   376 
   377 end