wneuper/isa: src/HOL/MicroJava/BV/BVExample.thy@4d278bbb5cc8

     1 (*  Title:      HOL/MicroJava/BV/BVExample.thy

     2     Author:     Gerwin Klein

     3 *)

     5 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}

     7 theory BVExample

     8 imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set

     9 begin

    11 text {*

    12   This theory shows type correctness of the example program in section

    13   \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by

    14   explicitly providing a welltyping. It also shows that the start

    15   state of the program conforms to the welltyping; hence type safe

    16   execution is guaranteed.

    17 *}

    19 section "Setup"

    20 text {*

    21   Since the types @{typ cnam}, @{text vnam}, and @{text mname} are

    22   anonymous, we describe distinctness of names in the example by axioms:

    23 *}

    24 axioms

    25   distinct_classes: "list_nam \<noteq> test_nam"

    26   distinct_fields:  "val_nam \<noteq> next_nam"

    28 text {* Abbreviations for definitions we will have to use often in the

    29 proofs below: *}

    30 lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def

    31 lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def

    32                      OutOfMemoryC_def ClassCastC_def

    33 lemmas class_defs  = list_class_def test_class_def

    35 text {* These auxiliary proofs are for efficiency: class lookup,

    36 subclass relation, method and field lookup are computed only once:

    37 *}

    38 lemma class_Object [simp]:

    39   "class E Object = Some (undefined, [],[])"

    40   by (simp add: class_def system_defs E_def)

    42 lemma class_NullPointer [simp]:

    43   "class E (Xcpt NullPointer) = Some (Object, [], [])"

    44   by (simp add: class_def system_defs E_def)

    46 lemma class_OutOfMemory [simp]:

    47   "class E (Xcpt OutOfMemory) = Some (Object, [], [])"

    48   by (simp add: class_def system_defs E_def)

    50 lemma class_ClassCast [simp]:

    51   "class E (Xcpt ClassCast) = Some (Object, [], [])"

    52   by (simp add: class_def system_defs E_def)

    54 lemma class_list [simp]:

    55   "class E list_name = Some list_class"

    56   by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])

    58 lemma class_test [simp]:

    59   "class E test_name = Some test_class"

    60   by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])

    62 lemma E_classes [simp]:

    63   "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer,

    64                         Xcpt ClassCast, Xcpt OutOfMemory, Object}"

    65   by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)

    67 text {* The subclass releation spelled out: *}

    68 lemma subcls1:

    69   "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),

    70                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"

    71 apply (simp add: subcls1_def2)

    72 apply (simp add: name_defs class_defs system_defs E_def class_def)

    73 apply (auto simp: expand_fun_eq)

    74 done

    76 text {* The subclass relation is acyclic; hence its converse is well founded: *}

    77 lemma notin_rtrancl:

    78   "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False"

    79   by (auto elim: converse_rtranclpE)

    81 lemma acyclic_subcls1_E: "acyclicP (subcls1 E)"

    82   apply (rule acyclicI [to_pred])

    83   apply (simp add: subcls1)

    84   apply (auto dest!: tranclpD)

    85   apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)

    86   done

    88 lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)"

    89   apply (rule finite_acyclic_wf_converse [to_pred])

    90   apply (simp add: subcls1 del: insert_iff)

    91   apply (rule acyclic_subcls1_E)

    92   done

    94 text {* Method and field lookup: *}

    95 lemma method_Object [simp]:

    96   "method (E, Object) = Map.empty"

    97   by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])

    99 lemma method_append [simp]:

   100   "method (E, list_name) (append_name, [Class list_name]) =

   101   Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"

   102   apply (insert class_list)

   103   apply (unfold list_class_def)

   104   apply (drule method_rec_lemma [OF _ wf_subcls1_E])

   105   apply simp

   106   done

   108 lemma method_makelist [simp]:

   109   "method (E, test_name) (makelist_name, []) =

   110   Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"

   111   apply (insert class_test)

   112   apply (unfold test_class_def)

   113   apply (drule method_rec_lemma [OF _ wf_subcls1_E])

   114   apply simp

   115   done

   117 lemma field_val [simp]:

   118   "field (E, list_name) val_name = Some (list_name, PrimT Integer)"

   119   apply (unfold TypeRel.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

   124   done

   126 lemma field_next [simp]:

   127   "field (E, list_name) next_name = Some (list_name, Class list_name)"

   128   apply (unfold TypeRel.field_def)

   129   apply (insert class_list)

   130   apply (unfold list_class_def)

   131   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])

   132   apply (simp add: name_defs distinct_fields [symmetric])

   133   done

   135 lemma [simp]: "fields (E, Object) = []"

   136    by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])

   138 lemma [simp]: "fields (E, Xcpt NullPointer) = []"

   139   by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])

   141 lemma [simp]: "fields (E, Xcpt ClassCast) = []"

   142   by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])

   144 lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"

   145   by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])

   147 lemma [simp]: "fields (E, test_name) = []"

   148   apply (insert class_test)

   149   apply (unfold test_class_def)

   150   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])

   151   apply simp

   152   done

   154 lemmas [simp] = is_class_def

   156 text {*

   157   The next definition and three proof rules implement an algorithm to

   158   enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"}

   159   transforms a goal of the form

   160   @{prop [display] "pc < n \<Longrightarrow> P pc"}

   161   into a series of goals

   162   @{prop [display] "P 0"}

   163   @{prop [display] "P (Suc 0)"}

   165   @{text "\<dots>"}

   167   @{prop [display] "P n"}

   168 *}

   169 constdefs

   170   intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")

   171   "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"

   173 lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"

   174   by (simp add: intervall_def)

   176 lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"

   177   apply (cases "x=n0")

   178   apply (auto simp add: intervall_def)

   179   done

   181 lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x"

   182   by (unfold intervall_def) arith

   185 section "Program structure"

   187 text {*

   188   The program is structurally wellformed:

   189 *}

   191 lemma wf_struct:

   192   "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")

   193 proof -

   194   have "unique E"

   195     by (simp add: system_defs E_def class_defs name_defs distinct_classes)

   196   moreover

   197   have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)

   198   hence "wf_syscls E" by (rule wf_syscls)

   199   moreover

   200   have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)

   201   moreover

   202   have "wf_cdecl ?mb E NullPointerC"

   203     by (auto elim: notin_rtrancl

   204             simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)

   205   moreover

   206   have "wf_cdecl ?mb E ClassCastC"

   207     by (auto elim: notin_rtrancl

   208             simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)

   209   moreover

   210   have "wf_cdecl ?mb E OutOfMemoryC"

   211     by (auto elim: notin_rtrancl

   212             simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)

   213   moreover

   214   have "wf_cdecl ?mb E (list_name, list_class)"

   215     apply (auto elim!: notin_rtrancl

   216             simp add: wf_cdecl_def wf_fdecl_def list_class_def

   217                       wf_mdecl_def wf_mhead_def subcls1)

   218     apply (auto simp add: name_defs distinct_classes distinct_fields)

   219     done

   220   moreover

   221   have "wf_cdecl ?mb E (test_name, test_class)"

   222     apply (auto elim!: notin_rtrancl

   223             simp add: wf_cdecl_def wf_fdecl_def test_class_def

   224                       wf_mdecl_def wf_mhead_def subcls1)

   225     apply (auto simp add: name_defs distinct_classes distinct_fields)

   226     done

   227   ultimately

   228   show ?thesis

   229     by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)

   230 qed

   232 section "Welltypings"

   233 text {*

   234   We show welltypings of the methods @{term append_name} in class @{term list_name},

   235   and @{term makelist_name} in class @{term test_name}:

   236 *}

   237 lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def

   238 declare appInvoke [simp del]

   240 constdefs

   241   phi_append :: method_type ("\<phi>\<^sub>a")

   242   "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [

   243    (                                    [], [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]),

   246    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),

   247    ([NT, Class list_name, 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    (                          [PrimT Void], [Class list_name, Class list_name]),

   251    (                        [Class Object], [Class list_name, Class list_name]),

   252    (                                    [], [Class list_name, Class list_name]),

   253    (                     [Class list_name], [Class list_name, Class list_name]),

   254    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),

   255    (                                    [], [Class list_name, Class list_name]),

   256    (                          [PrimT Void], [Class list_name, Class list_name])]"

   259 lemma bounded_append [simp]:

   260   "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"

   261   apply (simp add: check_bounded_def)

   262   apply (simp add: nat_number append_ins_def)

   263   apply (rule allI, rule impI)

   264   apply (elim pc_end pc_next pc_0)

   265   apply auto

   266   done

   268 lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"

   269   apply (auto simp add: check_types_def phi_append_def JVM_states_unfold)

   270   apply (unfold list_def)

   271   apply auto

   272   done

   274 lemma wt_append [simp]:

   275   "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins

   276              [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"

   277   apply (simp add: wt_method_def wt_start_def wt_instr_def)

   278   apply (simp add: phi_append_def append_ins_def)

   279   apply clarify

   280   apply (elim pc_end pc_next pc_0)

   281   apply simp

   282   apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)

   283   apply simp

   284   apply simp

   285   apply (fastsimp simp add: sup_state_conv subcls1)

   286   apply simp

   287   apply (simp add: app_def xcpt_app_def)

   288   apply simp

   289   apply simp

   290   apply simp

   291   apply (simp add: match_exception_entry_def)

   292   apply (simp add: match_exception_entry_def)

   293   apply simp

   294   apply simp

   295   done

   297 text {* Some abbreviations for readability *}

   298 syntax

   299   Clist :: ty

   300   Ctest :: ty

   301 translations

   302   "Clist" == "Class list_name"

   303   "Ctest" == "Class test_name"

   305 constdefs

   306   phi_makelist :: method_type ("\<phi>\<^sub>m")

   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])]"

   332 lemma bounded_makelist [simp]: "check_bounded make_list_ins []"

   333   apply (simp add: check_bounded_def)

   334   apply (simp add: nat_number make_list_ins_def)

   335   apply (rule allI, rule impI)

   336   apply (elim pc_end pc_next pc_0)

   337   apply auto

   338   done

   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

   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 nat_number)

   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

   379 text {* The whole program is welltyped: *}

   380 constdefs

   381   Phi :: prog_type ("\<Phi>")

   382   "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else

   383              if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"

   385 lemma wf_prog:

   386   "wt_jvm_prog E \<Phi>"

   387   apply (unfold wt_jvm_prog_def)

   388   apply (rule wf_mb'E [OF wf_struct])

   389   apply (simp add: E_def)

   390   apply clarify

   391   apply (fold E_def)

   392   apply (simp add: system_defs class_defs Phi_def)

   393   apply auto

   394   done

   397 section "Conformance"

   398 text {* Execution of the program will be typesafe, because its

   399   start state conforms to the welltyping: *}

   401 lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"

   402   apply (rule BV_correct_initial)

   403     apply (rule wf_prog)

   404    apply simp

   405   apply simp

   406   done

   409 section "Example for code generation: inferring method types"

   411 definition 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" where

   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)"

   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

   434 definition some_elem :: "'a set \<Rightarrow> 'a" where

   435   "some_elem = (%S. SOME x. x : S)"

   437 consts_code

   438   "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")

   440 text {* This code setup is just a demonstration and \emph{not} sound! *}

   442 lemma False

   443 proof -

   444   have "some_elem (set [False, True]) = False"

   445     by evaluation

   446   moreover have "some_elem (set [True, False]) = True"

   447     by evaluation

   448   ultimately show False

   449     by (simp add: some_elem_def)

   450 qed

   452 lemma [code]:

   453   "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)

   454     (\<lambda>(ss, w).

   455         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))

   456     (ss, w)"

   457   unfolding iter_def List_Set.is_empty_def some_elem_def ..

   459 lemma JVM_sup_unfold [code]:

   460  "JVMType.sup S m n = lift2 (Opt.sup

   461        (Product.sup (Listn.sup (JType.sup S))

   462          (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))"

   463   apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def

   464          stk_esl_def reg_sl_def Product.esl_def

   465          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)

   466   by simp

   468 lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold

   470 lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp

   472 code_module BV

   473 contains

   474   test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0

   475     [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"

   476   test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"

   477 ML BV.test1

   478 ML BV.test2

   480 end

author	haftmann
	Mon, 29 Jun 2009 16:17:55 +0200
changeset 31866	4d278bbb5cc8
parent 31852	a16bb835e97d
child 31998	2c7a24f74db9
permissions	-rw-r--r--