src/HOL/MicroJava/BV/Typing_Framework_err.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15425 6356d2523f73
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
nipkow@11229
     1
(*  Title:      HOL/MicroJava/BV/Typing_Framework_err.thy
nipkow@11229
     2
    ID:         $Id$
nipkow@11229
     3
    Author:     Gerwin Klein
nipkow@11229
     4
    Copyright   2000 TUM
nipkow@11229
     5
nipkow@11229
     6
*)
nipkow@11229
     7
kleing@13224
     8
header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}
nipkow@11229
     9
kleing@13062
    10
theory Typing_Framework_err = Typing_Framework + SemilatAlg:
nipkow@11229
    11
nipkow@11229
    12
constdefs
nipkow@11229
    13
kleing@13066
    14
wt_err_step :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
kleing@13066
    15
"wt_err_step r step ts \<equiv> wt_step (Err.le r) Err step ts"
kleing@12516
    16
kleing@13066
    17
wt_app_eff :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
kleing@13066
    18
"wt_app_eff r app step ts \<equiv>
kleing@12516
    19
  \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
kleing@12516
    20
kleing@12516
    21
map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list"
kleing@13066
    22
"map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
kleing@13066
    23
kleing@13066
    24
error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
nipkow@15425
    25
"error n \<equiv> map (\<lambda>x. (x,Err)) [0..<n]"
nipkow@11229
    26
kleing@13066
    27
err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
kleing@13066
    28
"err_step n app step p t \<equiv> 
kleing@13066
    29
  case t of 
kleing@13066
    30
    Err   \<Rightarrow> error n
kleing@13066
    31
  | OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n"
nipkow@11229
    32
kleing@13224
    33
app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
kleing@13224
    34
"app_mono r app n A \<equiv>
kleing@13224
    35
 \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
kleing@13224
    36
kleing@13224
    37
kleing@13066
    38
lemmas err_step_defs = err_step_def map_snd_def error_def
kleing@12516
    39
kleing@13224
    40
kleing@13067
    41
lemma bounded_err_stepD:
kleing@13067
    42
  "bounded (err_step n app step) n \<Longrightarrow> 
kleing@13067
    43
  p < n \<Longrightarrow>  app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> 
kleing@13067
    44
  q < n"
kleing@13067
    45
  apply (simp add: bounded_def err_step_def)
kleing@13067
    46
  apply (erule allE, erule impE, assumption)
kleing@13067
    47
  apply (erule_tac x = "OK a" in allE, drule bspec)
kleing@13067
    48
   apply (simp add: map_snd_def)
kleing@13067
    49
   apply fast
kleing@13067
    50
  apply simp
kleing@13067
    51
  done
kleing@13067
    52
kleing@13067
    53
kleing@13067
    54
lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
kleing@13067
    55
  apply (induct xs)
kleing@13067
    56
  apply (auto simp add: map_snd_def)
kleing@13067
    57
  done
nipkow@11229
    58
kleing@12516
    59
kleing@13067
    60
lemma bounded_err_stepI:
kleing@13067
    61
  "\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
kleing@13067
    62
  \<Longrightarrow> bounded (err_step n ap step) n"
kleing@13067
    63
apply (unfold bounded_def)
kleing@13067
    64
apply clarify
kleing@13067
    65
apply (simp add: err_step_def split: err.splits)
kleing@13067
    66
apply (simp add: error_def)
kleing@13067
    67
 apply blast
kleing@13067
    68
apply (simp split: split_if_asm) 
kleing@13067
    69
 apply (blast dest: in_map_sndD)
kleing@13067
    70
apply (simp add: error_def)
kleing@13067
    71
apply blast
kleing@13067
    72
done
kleing@13067
    73
kleing@13067
    74
kleing@13224
    75
lemma bounded_lift:
kleing@13224
    76
  "bounded step n \<Longrightarrow> bounded (err_step n app step) n"
kleing@13224
    77
  apply (unfold bounded_def err_step_def error_def)
kleing@13224
    78
  apply clarify
kleing@13224
    79
  apply (erule allE, erule impE, assumption)
kleing@13224
    80
  apply (case_tac s)
kleing@13224
    81
  apply (auto simp add: map_snd_def split: split_if_asm)
kleing@13224
    82
  done
kleing@13224
    83
kleing@13224
    84
kleing@13224
    85
lemma le_list_map_OK [simp]:
kleing@13224
    86
  "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
kleing@13224
    87
  apply (induct a)
kleing@13224
    88
   apply simp
kleing@13224
    89
  apply simp
kleing@13224
    90
  apply (case_tac b)
kleing@13224
    91
   apply simp
kleing@13224
    92
  apply simp
kleing@13224
    93
  done
kleing@13224
    94
kleing@13224
    95
kleing@13224
    96
lemma map_snd_lessI:
kleing@13224
    97
  "x <=|r| y \<Longrightarrow> map_snd OK x <=|Err.le r| map_snd OK y"
kleing@13224
    98
  apply (induct x)
kleing@13224
    99
  apply (unfold lesubstep_type_def map_snd_def)
kleing@13224
   100
  apply auto
kleing@13224
   101
  done
kleing@13224
   102
kleing@13224
   103
kleing@13224
   104
lemma mono_lift:
kleing@13224
   105
  "order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow>
kleing@13224
   106
  \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s <=|r| step p t \<Longrightarrow>
kleing@13224
   107
  mono (Err.le r) (err_step n app step) n (err A)"
kleing@13224
   108
apply (unfold app_mono_def mono_def err_step_def)
kleing@13224
   109
apply clarify
kleing@13224
   110
apply (case_tac s)
kleing@13224
   111
 apply simp 
kleing@13224
   112
apply simp
kleing@13224
   113
apply (case_tac t)
kleing@13224
   114
 apply simp
kleing@13224
   115
 apply clarify
kleing@13224
   116
 apply (simp add: lesubstep_type_def error_def)
kleing@13224
   117
 apply clarify
kleing@13224
   118
 apply (drule in_map_sndD)
kleing@13224
   119
 apply clarify
kleing@13224
   120
 apply (drule bounded_err_stepD, assumption+)
kleing@13224
   121
 apply (rule exI [of _ Err])
kleing@13224
   122
 apply simp
kleing@13224
   123
apply simp
kleing@13224
   124
apply (erule allE, erule allE, erule allE, erule impE)
kleing@13224
   125
 apply (rule conjI, assumption)
kleing@13224
   126
 apply (rule conjI, assumption)
kleing@13224
   127
 apply assumption
kleing@13224
   128
apply (rule conjI)
kleing@13224
   129
apply clarify
kleing@13224
   130
apply (erule allE, erule allE, erule allE, erule impE)
kleing@13224
   131
 apply (rule conjI, assumption)
kleing@13224
   132
 apply (rule conjI, assumption)
kleing@13224
   133
 apply assumption
kleing@13224
   134
apply (erule impE, assumption)
kleing@13224
   135
apply (rule map_snd_lessI, assumption)
kleing@13224
   136
apply clarify
kleing@13224
   137
apply (simp add: lesubstep_type_def error_def)
kleing@13224
   138
apply clarify
kleing@13224
   139
apply (drule in_map_sndD)
kleing@13224
   140
apply clarify
kleing@13224
   141
apply (drule bounded_err_stepD, assumption+)
kleing@13224
   142
apply (rule exI [of _ Err])
kleing@13224
   143
apply simp
kleing@13224
   144
done
kleing@13224
   145
 
kleing@13224
   146
lemma in_errorD:
kleing@13224
   147
  "(x,y) \<in> set (error n) \<Longrightarrow> y = Err"
kleing@13224
   148
  by (auto simp add: error_def)
kleing@13224
   149
kleing@13224
   150
lemma pres_type_lift:
kleing@13224
   151
  "\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A) 
kleing@13224
   152
  \<Longrightarrow> pres_type (err_step n app step) n (err A)"  
kleing@13224
   153
apply (unfold pres_type_def err_step_def)
kleing@13224
   154
apply clarify
kleing@13224
   155
apply (case_tac b)
kleing@13224
   156
 apply simp
kleing@13224
   157
apply (case_tac s)
kleing@13224
   158
 apply simp
kleing@13224
   159
 apply (drule in_errorD)
kleing@13224
   160
 apply simp
kleing@13224
   161
apply (simp add: map_snd_def split: split_if_asm)
kleing@13224
   162
 apply fast
kleing@13224
   163
apply (drule in_errorD)
kleing@13224
   164
apply simp
kleing@13224
   165
done
kleing@13224
   166
kleing@13224
   167
kleing@13224
   168
kleing@13067
   169
text {*
kleing@13067
   170
  There used to be a condition here that each instruction must have a
kleing@13067
   171
  successor. This is not needed any more, because the definition of
kleing@13067
   172
  @{term error} trivially ensures that there is a successor for
kleing@13067
   173
  the critical case where @{term app} does not hold. 
kleing@13067
   174
*}
kleing@13066
   175
lemma wt_err_imp_wt_app_eff:
kleing@13066
   176
  assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
kleing@13067
   177
  assumes b:  "bounded (err_step (size ts) app step) (size ts)"
kleing@13066
   178
  shows "wt_app_eff r app step (map ok_val ts)"
kleing@13066
   179
proof (unfold wt_app_eff_def, intro strip, rule conjI)
kleing@13066
   180
  fix p assume "p < size (map ok_val ts)"
kleing@13066
   181
  hence lp: "p < size ts" by simp
kleing@13067
   182
  hence ts: "0 < size ts" by (cases p) auto
kleing@13067
   183
  hence err: "(0,Err) \<in> set (error (size ts))" by (simp add: error_def)
nipkow@11229
   184
nipkow@11229
   185
  from wt lp
kleing@13066
   186
  have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err" 
kleing@13066
   187
    by (unfold wt_err_step_def wt_step_def) simp
nipkow@11229
   188
nipkow@11229
   189
  show app: "app p (map ok_val ts ! p)"
kleing@13067
   190
  proof (rule ccontr)
kleing@13067
   191
    from wt lp obtain s where
kleing@12516
   192
      OKp:  "ts ! p = OK s" and
kleing@13066
   193
      less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
kleing@13066
   194
      by (unfold wt_err_step_def wt_step_def stable_def) 
kleing@12516
   195
         (auto iff: not_Err_eq)
kleing@13067
   196
    assume "\<not> app p (map ok_val ts ! p)"
kleing@13067
   197
    with OKp lp have "\<not> app p s" by simp
kleing@13067
   198
    with OKp have "err_step (size ts) app step p (ts!p) = error (size ts)" 
kleing@13067
   199
      by (simp add: err_step_def)    
kleing@13067
   200
    with err ts obtain q where 
kleing@13067
   201
      "(q,Err) \<in> set (err_step (size ts) app step p (ts!p))" and
kleing@13067
   202
      q: "q < size ts" by auto    
kleing@13067
   203
    with less have "ts!q = Err" by auto
kleing@13067
   204
    moreover from q have "ts!q \<noteq> Err" ..
kleing@13067
   205
    ultimately show False by blast
kleing@12516
   206
  qed
kleing@12516
   207
  
kleing@12516
   208
  show "\<forall>(q,t)\<in>set(step p (map ok_val ts ! p)). t <=_r map ok_val ts ! q" 
kleing@12516
   209
  proof clarify
kleing@12516
   210
    fix q t assume q: "(q,t) \<in> set (step p (map ok_val ts ! p))"
nipkow@11229
   211
nipkow@11229
   212
    from wt lp q
nipkow@11229
   213
    obtain s where
nipkow@11229
   214
      OKp:  "ts ! p = OK s" and
kleing@13066
   215
      less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
kleing@13066
   216
      by (unfold wt_err_step_def wt_step_def stable_def) 
nipkow@11229
   217
         (auto iff: not_Err_eq)
nipkow@11229
   218
kleing@13067
   219
    from b lp app q have lq: "q < size ts" by (rule bounded_err_stepD)
kleing@12516
   220
    hence "ts!q \<noteq> Err" ..
kleing@12516
   221
    then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
nipkow@11229
   222
kleing@12516
   223
    from lp lq OKp OKq app less q
kleing@12516
   224
    show "t <=_r map ok_val ts ! q"
kleing@12516
   225
      by (auto simp add: err_step_def map_snd_def) 
nipkow@11229
   226
  qed
nipkow@11229
   227
qed
nipkow@11229
   228
nipkow@11229
   229
kleing@13066
   230
lemma wt_app_eff_imp_wt_err:
kleing@13066
   231
  assumes app_eff: "wt_app_eff r app step ts"
kleing@13066
   232
  assumes bounded: "bounded (err_step (size ts) app step) (size ts)"
kleing@13066
   233
  shows "wt_err_step r (err_step (size ts) app step) (map OK ts)"
kleing@13066
   234
proof (unfold wt_err_step_def wt_step_def, intro strip, rule conjI)
kleing@13066
   235
  fix p assume "p < size (map OK ts)" 
kleing@13066
   236
  hence p: "p < size ts" by simp
nipkow@11229
   237
  thus "map OK ts ! p \<noteq> Err" by simp
kleing@12516
   238
  { fix q t
kleing@13066
   239
    assume q: "(q,t) \<in> set (err_step (size ts) app step p (map OK ts ! p))" 
kleing@13066
   240
    with p app_eff obtain 
kleing@12516
   241
      "app p (ts ! p)" "\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q"
kleing@13066
   242
      by (unfold wt_app_eff_def) blast
nipkow@11229
   243
    moreover
kleing@13066
   244
    from q p bounded have "q < size ts"
kleing@13066
   245
      by - (rule boundedD)
nipkow@11229
   246
    hence "map OK ts ! q = OK (ts!q)" by simp
nipkow@11229
   247
    moreover
nipkow@11229
   248
    have "p < size ts" by (rule p)
kleing@12516
   249
    moreover note q
nipkow@11229
   250
    ultimately     
kleing@12516
   251
    have "t <=_(Err.le r) map OK ts ! q" 
kleing@12516
   252
      by (auto simp add: err_step_def map_snd_def)
nipkow@11229
   253
  }
kleing@13066
   254
  thus "stable (Err.le r) (err_step (size ts) app step) (map OK ts) p"
nipkow@11229
   255
    by (unfold stable_def) blast
nipkow@11229
   256
qed
nipkow@11229
   257
nipkow@11229
   258
end
kleing@13224
   259