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