Theory Typing_Framework_err

(*  Title:      HOL/MicroJava/BV/Typing_Framework_err.thy
    Author:     Gerwin Klein
    Copyright   2000 TUM

*)

section ‹Lifting the Typing Framework to err, app, and eff›

theory Typing_Framework_err imports SemilatAlg begin

definition wt_err_step :: "'s ord ⇒ 's err step_type ⇒ 's err list ⇒ bool"
where
  "wt_err_step r step τs ⟷ wt_step (Err.le r) Err step τs"

definition wt_app_eff :: "'s ord ⇒ (nat ⇒ 's ⇒ bool) ⇒ 's step_type ⇒ 's list ⇒ bool"
where
  "wt_app_eff r app step τs ⟷
    (∀p < size τs. app p (τs!p) ∧ (∀(q,τ) ∈ set (step p (τs!p)). τ <=_r τs!q))"

definition map_snd :: "('b ⇒ 'c) ⇒ ('a × 'b) list ⇒ ('a × 'c) list"
where
  "map_snd f = map (λ(x,y). (x, f y))"

definition error :: "nat ⇒ (nat × 'a err) list"
where
  "error n = map (λx. (x,Err)) [0..<n]"

definition err_step :: "nat ⇒ (nat ⇒ 's ⇒ bool) ⇒ 's step_type ⇒ 's err step_type"
where
  "err_step n app step p t = 
  (case t of 
    Err   ⇒ error n
  | OK τ ⇒ if app p τ then map_snd OK (step p τ) else error n)"

definition app_mono :: "'s ord ⇒ (nat ⇒ 's ⇒ bool) ⇒ nat ⇒ 's set ⇒ bool"
where
  "app_mono r app n A ⟷
    (∀s p t. s ∈ A ∧ p < n ∧ s ⊑⇩r t ⟶ app p t ⟶ app p s)"


lemmas err_step_defs = err_step_def map_snd_def error_def


lemma bounded_err_stepD:
  "⟦ bounded (err_step n app step) n;
     p < n; app p a; (q,b) ∈ set (step p a) ⟧ ⟹ q < n"
(*<*)
  apply (simp add: bounded_def err_step_def)
  apply (erule allE, erule impE, assumption)
  apply (erule_tac x = "OK a" in allE, drule bspec)
   apply (simp add: map_snd_def)
   apply fast
  apply simp
  done
(*>*)


lemma in_map_sndD: "(a,b) ∈ set (map_snd f xs) ⟹ ∃b'. (a,b') ∈ set xs"
(*<*)
  apply (induct xs)
  apply (auto simp add: map_snd_def)
  done
(*>*)


lemma bounded_err_stepI:
  "∀p. p < n ⟶ (∀s. ap p s ⟶ (∀(q,s') ∈ set (step p s). q < n))
  ⟹ bounded (err_step n ap step) n"
(*<*)
apply (clarsimp simp: bounded_def err_step_def split: err.splits)
apply (simp add: error_def image_def)
apply (blast dest: in_map_sndD)
done
(*>*)


lemma bounded_lift:
  "bounded step n ⟹ bounded (err_step n app step) n"
(*<*)
  apply (unfold bounded_def err_step_def error_def)
  apply clarify
  apply (erule allE, erule impE, assumption)
  apply (case_tac τ)
  apply (auto simp add: map_snd_def split: if_split_asm)
  done
(*>*)


lemma le_list_map_OK [simp]:
  "⋀b. (map OK a [⊑⇘Err.le r⇙] map OK b) = (a [⊑⇩r] b)"
(*<*)
  apply (induct a)
   apply simp
  apply simp
  apply (case_tac b)
   apply simp
  apply simp
  done
(*>*)


lemma map_snd_lessI:
  "set xs {⊑⇘r⇙} set ys ⟹ set (map_snd OK xs) {⊑⇘Err.le r⇙} set (map_snd OK ys)"
(*<*)
  apply (induct xs)
  apply (unfold lesubstep_type_def map_snd_def)
  apply auto
  done
(*>*)


lemma mono_lift:
  "⟦ order r A; app_mono r app n A; bounded (err_step n app step) n;
    ∀s p t. s ∈ A ∧ p < n ∧ s ⊑⇩r t ⟶ app p t ⟶ set (step p s) {⊑⇘r⇙} set (step p t) ⟧
  ⟹  mono (Err.le r) (err_step n app step) n (err A)"
(*<*)
apply (simp only: app_mono_def SemilatAlg.mono_def err_step_def)
apply clarify
apply (case_tac τ)
  defer
apply simp
apply (case_tac τ')
 apply simp
 apply clarify
 apply (simp add: lesubstep_type_def error_def)
 apply clarify
 apply (drule in_map_sndD)
 apply clarify
 apply (drule bounded_err_stepD, assumption+)
 apply (rule exI [of _ Err])
 apply simp
apply simp
apply (erule allE, erule allE, erule allE, erule impE)
 apply (rule conjI, assumption)
 apply (rule conjI, assumption)
 apply assumption
apply (rule conjI)
apply clarify
apply (erule allE, erule allE, erule allE, erule impE)
 apply (rule conjI, assumption)
 apply (rule conjI, assumption)
 apply assumption
apply (erule impE, assumption)
apply (rule map_snd_lessI, assumption)
apply clarify
apply (simp add: lesubstep_type_def error_def)
apply clarify
apply (drule in_map_sndD)
apply clarify
apply (drule bounded_err_stepD, assumption+)
apply (rule exI [of _ Err])
apply simp
  apply (auto simp: lesubstep_type_def error_def)  
done
(*>*)
 
lemma in_errorD: "(x,y) ∈ set (error n) ⟹ y = Err"
(*<*) by (auto simp add: error_def) (*>*)

lemma pres_type_lift:
  "∀s∈A. ∀p. p < n ⟶ app p s ⟶ (∀(q, s')∈set (step p s). s' ∈ A) 
  ⟹ pres_type (err_step n app step) n (err A)"  
(*<*)
apply (unfold pres_type_def err_step_def)
apply clarify
apply (case_tac b)
 apply simp
apply (case_tac τ)
 apply simp
 apply (drule in_errorD)
 apply simp
apply (simp add: map_snd_def split: if_split_asm)
 apply fast
apply (drule in_errorD)
apply simp
done
(*>*)


lemma wt_err_imp_wt_app_eff:
  assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
  assumes b:  "bounded (err_step (size ts) app step) (size ts)"
  shows "wt_app_eff r app step (map ok_val ts)"
(*<*)
proof (unfold wt_app_eff_def, intro strip, rule conjI)
  fix p assume "p < size (map ok_val ts)"
  hence lp: "p < size ts" by simp
  hence ts: "0 < size ts" by (cases p) auto
  hence err: "(0,Err) ∈ set (error (size ts))" by (simp add: error_def)

  from wt lp
  have [intro?]: "⋀p. p < size ts ⟹ ts ! p ≠ Err" 
    by (unfold wt_err_step_def wt_step_def) simp

  show app: "app p (map ok_val ts ! p)"
  proof (rule ccontr)
    from wt lp obtain s where
      OKp:  "ts ! p = OK s" and
      less: "∀(q,t) ∈ set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
      by (unfold wt_err_step_def wt_step_def stable_def) 
         (auto iff: not_Err_eq)
    assume "¬ app p (map ok_val ts ! p)"
    with OKp lp have "¬ app p s" by simp
    with OKp have "err_step (size ts) app step p (ts!p) = error (size ts)" 
      by (simp add: err_step_def)    
    with err ts obtain q where 
      "(q,Err) ∈ set (err_step (size ts) app step p (ts!p))" and
      q: "q < size ts" by auto    
    with less have "ts!q = Err" by auto
    moreover from q have "ts!q ≠ Err" ..
    ultimately show False by blast
  qed
  
  show "∀(q,t)∈set(step p (map ok_val ts ! p)). t ⊑⇩r map ok_val ts ! q" 
  proof clarify
    fix q t assume q: "(q,t) ∈ set (step p (map ok_val ts ! p))"

    from wt lp q
    obtain s where
      OKp:  "ts ! p = OK s" and
      less: "∀(q,t) ∈ set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
      by (unfold wt_err_step_def wt_step_def stable_def) 
         (auto iff: not_Err_eq)

    from b lp app q have lq: "q < size ts" by (rule bounded_err_stepD)
    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 q
    show "t ⊑⇩r map ok_val ts ! q"
      by (auto simp add: err_step_def map_snd_def) 
  qed
qed
(*>*)


lemma wt_app_eff_imp_wt_err:
  assumes app_eff: "wt_app_eff r app step ts"
  assumes bounded: "bounded (err_step (size ts) app step) (size ts)"
  shows "wt_err_step r (err_step (size ts) app step) (map OK ts)"
(*<*)
proof (unfold wt_err_step_def wt_step_def, intro strip, rule conjI)
  fix p assume "p < size (map OK ts)" 
  hence p: "p < size ts" by simp
  thus "map OK ts ! p ≠ Err" by simp
  { fix q t
    assume q: "(q,t) ∈ set (err_step (size ts) app step p (map OK ts ! p))" 
    with p app_eff obtain 
      "app p (ts ! p)" "∀(q,t) ∈ set (step p (ts!p)). t ⊑⇩r ts!q"
      by (unfold wt_app_eff_def) blast
    moreover
    from q p bounded have "q < size ts"
      by - (rule boundedD)
    hence "map OK ts ! q = OK (ts!q)" by simp
    moreover
    have "p < size ts" by (rule p)
    moreover note q
    ultimately     
    have "t ⊑⇘Err.le r⇙ map OK ts ! q" 
      by (auto simp add: err_step_def map_snd_def)
  }
  thus "stable (Err.le r) (err_step (size ts) app step) (map OK ts) p"
    by (unfold stable_def) blast
qed
(*>*)

end