src/HOL/MicroJava/BV/DFA_err.thy

tuned for 99-2 release

(*  Title:      HOL/BCV/DFA_err.thy
    ID:         $Id$
    Author:     Gerwin Klein
    Copyright   2000 TUM

*)

header "Static and Dynamic Welltyping"

theory DFA_err = DFA_Framework:

constdefs

dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) => 
               's err list => bool"
"dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts"

static_wt :: "'s ord => (nat => 's => bool) => 
              (nat => 's => 's) => (nat => nat list) =>  's list => bool"
"static_wt r app step succs ts == 
  !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"

err_step :: "(nat => 's => bool) => (nat => 's => 's) => 
             (nat => 's err => 's err)"
"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"

non_empty :: "(nat => nat list) => bool"
"non_empty succs == !p. succs p ~= []"


lemma non_emptyD:
  "non_empty succs ==> ? q. q:set(succs p)"
proof (unfold non_empty_def)
  assume "!p. succs p ~= []"
  hence "succs p ~= []" ..
  then obtain x xs where "succs p = x#xs"
    by (auto simp add: neq_Nil_conv)
  thus ?thesis 
    by auto
qed

lemma dynamic_imp_static:
  "[| bounded succs (size ts); non_empty succs;
      dynamic_wt r (err_step app step) succs ts |] 
  ==> static_wt r app step succs (map ok_val ts)"
proof (unfold static_wt_def, intro strip, rule conjI)

  assume b:  "bounded succs (size ts)"
  assume n:  "non_empty succs"
  assume wt: "dynamic_wt r (err_step app step) succs ts"

  fix p 
  assume "p < length (map ok_val ts)"
  hence lp: "p < length ts" by simp

  from wt lp
  have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err" 
    by (unfold dynamic_wt_def welltyping_def) simp

  show app: "app p (map ok_val ts ! p)"
  proof -
    from n
    obtain q where q: "q:set(succs p)"
      by (auto dest: non_emptyD)

    from wt lp q
    obtain s where
      OKp:  "ts ! p = OK s" and
      less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
      by (unfold dynamic_wt_def welltyping_def stable_def) 
         (auto iff: not_Err_eq)

    from lp b q
    have lq: "q < length ts"
      by (unfold bounded_def) blast
    hence "ts!q ~= Err" ..
    then
    obtain s' where OKq: "ts ! q = OK s'"
      by (auto iff: not_Err_eq)      

    with OKp less
    have "app p s"
      by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)

    with lp OKp
    show ?thesis
      by simp
  qed
  
  show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
  proof (intro strip)
    fix q
    assume q: "q:set (succs p)"

    from wt lp q
    obtain s where
      OKp:  "ts ! p = OK s" and
      less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
      by (unfold dynamic_wt_def welltyping_def stable_def) 
         (auto iff: not_Err_eq)

    from lp b q
    have lq: "q < length ts"
      by (unfold bounded_def) blast
    hence "ts!q ~= Err" ..
    then
    obtain s' where OKq: "ts ! q = OK s'"
      by (auto iff: not_Err_eq)      

    from lp lq OKp OKq app less
    show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
      by (simp add: err_step_def lift_def)
  qed
qed


lemma static_imp_dynamic:
  "[| static_wt r app step succs ts; bounded succs (size ts) |] 
  ==> dynamic_wt r (err_step app step) succs (map OK ts)"
proof (unfold dynamic_wt_def welltyping_def, intro strip, rule conjI)
  assume bounded: "bounded succs (size ts)"
  assume static:  "static_wt r app step succs ts"
  fix p assume "p < length (map OK ts)" 
  hence p: "p < length ts" by simp
  thus "map OK ts ! p \<noteq> Err" by simp
  { fix q
    assume q: "q : set (succs p)"
    with p static obtain 
      "app p (ts ! p)" "step p (ts ! p) <=_r ts ! q"
      by (unfold static_wt_def) blast
    moreover
    from q p bounded
    have "q < size ts" by (unfold bounded_def) blast
    hence "map OK ts ! q = OK (ts!q)" by simp
    moreover
    have "p < size ts" by (rule p)
    ultimately     
    have "err_step app step p (map OK ts ! p) <=_(Err.le r) map OK ts ! q"
      by (simp add: err_step_def lift_def)
  }
  thus "stable (Err.le r) (err_step app step) succs (map OK ts) p"
    by (unfold stable_def) blast
qed

end