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