src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14045 a34d89ce6097
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
kleing@13224
     1
(*  Title:      HOL/MicroJava/BV/JVM.thy
kleing@13224
     2
    ID:         $Id$
kleing@13224
     3
    Author:     Tobias Nipkow, Gerwin Klein
kleing@13224
     4
    Copyright   2000 TUM
kleing@13224
     5
*)
kleing@13224
     6
kleing@13224
     7
header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
kleing@13224
     8
kleing@13224
     9
theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec:
kleing@13224
    10
kleing@13224
    11
kleing@13224
    12
constdefs
kleing@13224
    13
  exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
kleing@13224
    14
  "exec G maxs rT et bs == 
kleing@13224
    15
  err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
kleing@13224
    16
kleing@13224
    17
constdefs
kleing@13224
    18
  opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
kleing@13224
    19
  "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
kleing@13224
    20
kleing@13224
    21
kleing@13224
    22
section {*  Executability of @{term check_bounded} *}
kleing@13224
    23
consts
kleing@13224
    24
  list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
kleing@13224
    25
primrec
kleing@13224
    26
  "list_all'_rec P n []     = True"
kleing@13224
    27
  "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
kleing@13224
    28
kleing@13224
    29
constdefs
kleing@13224
    30
  list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
kleing@13224
    31
  "list_all' P xs \<equiv> list_all'_rec P 0 xs"
kleing@13224
    32
kleing@13224
    33
lemma list_all'_rec:
kleing@13224
    34
  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
kleing@13224
    35
  apply (induct xs)
kleing@13224
    36
  apply auto
kleing@13224
    37
  apply (case_tac p)
kleing@13224
    38
  apply auto
kleing@13224
    39
  done
kleing@13224
    40
kleing@13224
    41
lemma list_all' [iff]:
kleing@13224
    42
  "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
kleing@13224
    43
  by (unfold list_all'_def) (simp add: list_all'_rec)
kleing@13224
    44
kleing@13224
    45
lemma list_all_ball:
kleing@13224
    46
  "list_all P xs = (\<forall>x \<in> set xs. P x)"
kleing@13224
    47
  by (induct xs) auto
kleing@13224
    48
kleing@13224
    49
lemma [code]:
kleing@13224
    50
  "check_bounded ins et = 
kleing@13224
    51
  (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> 
kleing@13224
    52
   list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
kleing@13224
    53
  by (simp add: list_all_ball check_bounded_def)
kleing@13224
    54
  
kleing@13224
    55
kleing@13224
    56
section {* Connecting JVM and Framework *}
kleing@13224
    57
kleing@13224
    58
lemma check_bounded_is_bounded:
kleing@13224
    59
  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"  
kleing@13224
    60
  by (unfold bounded_def) (blast dest: check_boundedD)
kleing@13224
    61
kleing@13224
    62
lemma special_ex_swap_lemma [iff]: 
kleing@13224
    63
  "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
kleing@13224
    64
  by blast
kleing@13224
    65
kleing@13224
    66
lemmas [iff del] = not_None_eq
kleing@13224
    67
kleing@13224
    68
theorem exec_pres_type:
kleing@13224
    69
  "wf_prog wf_mb S \<Longrightarrow> 
kleing@13224
    70
  pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
kleing@13224
    71
  apply (unfold exec_def JVM_states_unfold)
kleing@13224
    72
  apply (rule pres_type_lift)
kleing@13224
    73
  apply clarify
kleing@13224
    74
  apply (case_tac s)
kleing@13224
    75
   apply simp
kleing@13224
    76
   apply (drule effNone)
kleing@13224
    77
   apply simp  
kleing@13224
    78
  apply (simp add: eff_def xcpt_eff_def norm_eff_def)
kleing@13224
    79
  apply (case_tac "bs!p")
kleing@13224
    80
kleing@13224
    81
  apply (clarsimp simp add: not_Err_eq)
kleing@13224
    82
  apply (drule listE_nth_in, assumption)
kleing@13224
    83
  apply fastsimp
kleing@13224
    84
kleing@13224
    85
  apply (fastsimp simp add: not_None_eq)
kleing@13224
    86
kleing@13224
    87
  apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
kleing@13224
    88
kleing@13224
    89
  apply clarsimp
kleing@13224
    90
  apply (erule disjE)
kleing@13224
    91
   apply fastsimp
kleing@13224
    92
  apply clarsimp
kleing@13224
    93
  apply (rule_tac x="1" in exI)
kleing@13224
    94
  apply fastsimp
kleing@13224
    95
kleing@13224
    96
  apply clarsimp
kleing@13224
    97
  apply (erule disjE)
kleing@13224
    98
   apply (fastsimp dest: field_fields fields_is_type)
kleing@13224
    99
  apply (simp add: match_some_entry split: split_if_asm)
kleing@13224
   100
  apply (rule_tac x=1 in exI)
kleing@13224
   101
  apply fastsimp
kleing@13224
   102
kleing@13224
   103
  apply clarsimp
kleing@13224
   104
  apply (erule disjE)
kleing@13224
   105
   apply fastsimp
kleing@13224
   106
  apply (simp add: match_some_entry split: split_if_asm)
kleing@13224
   107
  apply (rule_tac x=1 in exI)
kleing@13224
   108
  apply fastsimp
kleing@13224
   109
kleing@13224
   110
  apply clarsimp
kleing@13224
   111
  apply (erule disjE)
kleing@13224
   112
   apply fastsimp
kleing@13224
   113
  apply clarsimp
kleing@13224
   114
  apply (rule_tac x=1 in exI)
kleing@13224
   115
  apply fastsimp
kleing@13224
   116
kleing@13224
   117
  defer 
kleing@13224
   118
kleing@13224
   119
  apply fastsimp
kleing@13224
   120
  apply fastsimp
kleing@13224
   121
kleing@13224
   122
  apply clarsimp
kleing@13224
   123
  apply (rule_tac x="n'+2" in exI)  
kleing@13224
   124
  apply simp
kleing@13224
   125
kleing@13224
   126
  apply clarsimp
kleing@13224
   127
  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
kleing@13224
   128
  apply simp
kleing@13224
   129
kleing@13224
   130
  apply clarsimp
kleing@13224
   131
  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
kleing@13224
   132
  apply simp
kleing@13224
   133
kleing@13224
   134
  apply fastsimp
kleing@13224
   135
  apply fastsimp
kleing@13224
   136
  apply fastsimp
kleing@13224
   137
  apply fastsimp
kleing@13224
   138
kleing@13224
   139
  apply clarsimp
kleing@13224
   140
  apply (erule disjE)
kleing@13224
   141
   apply fastsimp
kleing@13224
   142
  apply clarsimp
kleing@13224
   143
  apply (rule_tac x=1 in exI)
kleing@13224
   144
  apply fastsimp
kleing@13224
   145
  
kleing@13224
   146
  apply (erule disjE)
kleing@13224
   147
   apply (clarsimp simp add: Un_subset_iff)  
kleing@13224
   148
   apply (drule method_wf_mdecl, assumption+)
kleing@13224
   149
   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
kleing@13224
   150
   apply fastsimp
kleing@13224
   151
  apply clarsimp
kleing@13224
   152
  apply (rule_tac x=1 in exI)
kleing@13224
   153
  apply fastsimp
kleing@13224
   154
  done
kleing@13224
   155
kleing@13224
   156
lemmas [iff] = not_None_eq
kleing@13224
   157
kleing@13224
   158
lemma sup_state_opt_unfold:
kleing@13224
   159
  "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
kleing@13224
   160
  by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
kleing@13224
   161
kleing@13224
   162
kleing@13224
   163
lemma app_mono:
kleing@13224
   164
  "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
kleing@13224
   165
  by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
kleing@13224
   166
  
kleing@13224
   167
kleing@13224
   168
lemma list_appendI:
kleing@13224
   169
  "\<lbrakk>a \<in> list x A; b \<in> list y A\<rbrakk> \<Longrightarrow> a @ b \<in> list (x+y) A"
kleing@13224
   170
  apply (unfold list_def)
kleing@13224
   171
  apply (simp (no_asm))
kleing@13224
   172
  apply blast
kleing@13224
   173
  done
kleing@13224
   174
kleing@13224
   175
lemma list_map [simp]:
kleing@13224
   176
  "(map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)"
kleing@13224
   177
  apply (unfold list_def)
kleing@13224
   178
  apply simp
kleing@13224
   179
  done
kleing@13224
   180
kleing@13224
   181
lemma [iff]:
kleing@13224
   182
  "(OK ` A \<subseteq> err B) = (A \<subseteq> B)"
kleing@13224
   183
  apply (unfold err_def)
kleing@13224
   184
  apply blast
kleing@13224
   185
  done
kleing@13224
   186
kleing@13224
   187
lemma [intro]:
kleing@13224
   188
  "x \<in> A \<Longrightarrow> replicate n x \<in> list n A"
kleing@13224
   189
  by (induct n, auto)
kleing@13224
   190
kleing@13224
   191
lemma lesubstep_type_simple:
kleing@13224
   192
  "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
kleing@13224
   193
  apply (unfold lesubstep_type_def)
kleing@13224
   194
  apply clarify
kleing@13224
   195
  apply (simp add: set_conv_nth)
kleing@13224
   196
  apply clarify
kleing@13224
   197
  apply (drule le_listD, assumption)
kleing@13224
   198
  apply (clarsimp simp add: lesub_def Product.le_def)
kleing@13224
   199
  apply (rule exI)
kleing@13224
   200
  apply (rule conjI)
kleing@13224
   201
   apply (rule exI)
kleing@13224
   202
   apply (rule conjI)
kleing@13224
   203
    apply (rule sym)
kleing@13224
   204
    apply assumption
kleing@13224
   205
   apply assumption
kleing@13224
   206
  apply assumption
kleing@13224
   207
  done
kleing@13224
   208
  
kleing@13224
   209
kleing@13224
   210
lemma eff_mono:
kleing@13224
   211
  "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
kleing@13224
   212
  \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
kleing@13224
   213
  apply (unfold eff_def)
kleing@13224
   214
  apply (rule lesubstep_type_simple)
kleing@13224
   215
  apply (rule le_list_appendI)
kleing@13224
   216
   apply (simp add: norm_eff_def)
kleing@13224
   217
   apply (rule le_listI)
kleing@13224
   218
    apply simp
kleing@13224
   219
   apply simp
kleing@13224
   220
   apply (simp add: lesub_def)
kleing@13224
   221
   apply (case_tac s)
kleing@13224
   222
    apply simp
kleing@13224
   223
   apply (simp del: split_paired_All split_paired_Ex)
kleing@13224
   224
   apply (elim exE conjE)
kleing@13224
   225
   apply simp
kleing@13224
   226
   apply (drule eff'_mono, assumption)
kleing@13224
   227
   apply assumption
kleing@13224
   228
  apply (simp add: xcpt_eff_def)
kleing@13224
   229
  apply (rule le_listI)
kleing@13224
   230
    apply simp
kleing@13224
   231
  apply simp
kleing@13224
   232
  apply (simp add: lesub_def)
kleing@13224
   233
  apply (case_tac s)
kleing@13224
   234
   apply simp
kleing@13224
   235
  apply simp
kleing@13224
   236
  apply (case_tac t)
kleing@13224
   237
   apply simp
kleing@13224
   238
  apply (clarsimp simp add: sup_state_conv)
kleing@13224
   239
  done
kleing@13224
   240
kleing@13224
   241
lemma order_sup_state_opt:
streckem@14045
   242
  "ws_prog G \<Longrightarrow> order (sup_state_opt G)"
kleing@13224
   243
  by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
kleing@13224
   244
kleing@13224
   245
theorem exec_mono:
streckem@14045
   246
  "ws_prog G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
kleing@13224
   247
  mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
kleing@13224
   248
  apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
kleing@13224
   249
  apply (rule mono_lift)
kleing@13224
   250
     apply (fold sup_state_opt_unfold opt_states_def)
kleing@13224
   251
     apply (erule order_sup_state_opt)
kleing@13224
   252
    apply (rule app_mono)
kleing@13224
   253
   apply assumption
kleing@13224
   254
  apply clarify
kleing@13224
   255
  apply (rule eff_mono)
kleing@13224
   256
  apply assumption+
kleing@13224
   257
  done
kleing@13224
   258
kleing@13224
   259
theorem semilat_JVM_slI:
streckem@14045
   260
  "ws_prog G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
kleing@13224
   261
  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
kleing@13224
   262
  apply (rule semilat_opt)
kleing@13224
   263
  apply (rule err_semilat_Product_esl)
kleing@13224
   264
  apply (rule err_semilat_upto_esl)
kleing@13224
   265
  apply (rule err_semilat_JType_esl, assumption+)
kleing@13224
   266
  apply (rule err_semilat_eslI)
kleing@13224
   267
  apply (rule Listn_sl)
kleing@13224
   268
  apply (rule err_semilat_JType_esl, assumption+)
kleing@13224
   269
  done
kleing@13224
   270
kleing@13224
   271
lemma sl_triple_conv:
kleing@13224
   272
  "JVMType.sl G maxs maxr == 
kleing@13224
   273
  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
kleing@13224
   274
  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
kleing@13224
   275
kleing@13224
   276
kleing@13224
   277
lemma map_id [rule_format]:
kleing@13224
   278
  "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
kleing@13224
   279
  by (induct xs, auto)
kleing@13224
   280
kleing@13224
   281
kleing@13224
   282
lemma is_type_pTs:
kleing@13224
   283
  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
kleing@13224
   284
  \<Longrightarrow> set pTs \<subseteq> types G"
kleing@13224
   285
proof 
kleing@13224
   286
  assume "wf_prog wf_mb G" 
kleing@13224
   287
         "(C,S,fs,mdecls) \<in> set G"
kleing@13224
   288
         "((mn,pTs),rT,code) \<in> set mdecls"
kleing@13224
   289
  hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
streckem@14045
   290
    by (rule wf_prog_wf_mdecl)
kleing@13224
   291
  hence "\<forall>t \<in> set pTs. is_type G t" 
kleing@13224
   292
    by (unfold wf_mdecl_def wf_mhead_def) auto
kleing@13224
   293
  moreover
kleing@13224
   294
  fix t assume "t \<in> set pTs"
kleing@13224
   295
  ultimately
kleing@13224
   296
  have "is_type G t" by blast
kleing@13224
   297
  thus "t \<in> types G" ..
kleing@13224
   298
qed
kleing@13224
   299
kleing@13224
   300
kleing@13224
   301
lemma jvm_prog_lift:  
kleing@13224
   302
  assumes wf: 
kleing@13224
   303
  "wf_prog (\<lambda>G C bd. P G C bd) G"
kleing@13224
   304
kleing@13224
   305
  assumes rule:
kleing@13224
   306
  "\<And>wf_mb C mn pTs C rT maxs maxl b et bd.
kleing@13224
   307
   wf_prog wf_mb G \<Longrightarrow>
kleing@13224
   308
   method (G,C) (mn,pTs) = Some (C,rT,maxs,maxl,b,et) \<Longrightarrow>
kleing@13224
   309
   is_class G C \<Longrightarrow>
kleing@13224
   310
   set pTs \<subseteq> types G \<Longrightarrow>
kleing@13224
   311
   bd = ((mn,pTs),rT,maxs,maxl,b,et) \<Longrightarrow>
kleing@13224
   312
   P G C bd \<Longrightarrow>
kleing@13224
   313
   Q G C bd"
kleing@13224
   314
 
kleing@13224
   315
  shows 
kleing@13224
   316
  "wf_prog (\<lambda>G C bd. Q G C bd) G"
kleing@13224
   317
proof -
kleing@13224
   318
  from wf show ?thesis
kleing@13224
   319
    apply (unfold wf_prog_def wf_cdecl_def)
kleing@13224
   320
    apply clarsimp
kleing@13224
   321
    apply (drule bspec, assumption)
streckem@14045
   322
    apply (unfold wf_cdecl_mdecl_def)
kleing@13224
   323
    apply clarsimp
kleing@13224
   324
    apply (drule bspec, assumption)
streckem@14045
   325
    apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
kleing@13224
   326
    apply (frule is_type_pTs [OF wf], assumption+)
kleing@13224
   327
    apply clarify
kleing@13224
   328
    apply (drule rule [OF wf], assumption+)
kleing@13224
   329
    apply (rule refl)
kleing@13224
   330
    apply assumption+
kleing@13224
   331
    done
kleing@13224
   332
qed
kleing@13224
   333
kleing@13224
   334
end