# Theory Typing_Framework_err

Up to index of Isabelle/HOL/MicroJava

theory Typing_Framework_err
imports Typing_Framework SemilatAlg
begin

    (*  Title:      HOL/MicroJava/BV/Typing_Framework_err.thy
        ID:         $Id: Typing_Framework_err.thy,v 1.11 2005/06/17 14:13:08 haftmann Exp $
        Author:     Gerwin Klein
        Copyright   2000 TUM

    *)

    header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}

    theory Typing_Framework_err imports Typing_Framework SemilatAlg begin

    constdefs

    wt_err_step :: "'s ord => 's err step_type => 's err list => bool"
    "wt_err_step r step ts ≡ wt_step (Err.le r) Err step ts"

    wt_app_eff :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool"
    "wt_app_eff r app step ts ≡
      ∀p < size ts. app p (ts!p) ∧ (∀(q,t) ∈ set (step p (ts!p)). t <=_r ts!q)"

    map_snd :: "('b => 'c) => ('a × 'b) list => ('a × 'c) list"
    "map_snd f ≡ map (λ(x,y). (x, f y))"

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

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

    app_mono :: "'s ord => (nat => 's => bool) => nat => 's set => bool"
    "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 (unfold bounded_def)
    apply clarify
    apply (simp add: err_step_def split: err.splits)
    apply (simp add: error_def)
     apply blast
    apply (simp split: split_if_asm)
     apply (blast dest: in_map_sndD)
    apply (simp add: error_def)
    apply blast
    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 s)
      apply (auto simp add: map_snd_def split: split_if_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:
      "x <=|r| y ==> map_snd OK x <=|Err.le r| map_snd OK y"
      apply (induct x)
      apply (unfold lesubstep_type_def map_snd_def)
      apply auto
      done

    lemma mono_lift:
      "order r ==> 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 --> step p s <=|r| step p t ==>
      mono (Err.le r) (err_step n app step) n (err A)"
    apply (unfold app_mono_def mono_def err_step_def)
    apply clarify
    apply (case_tac s)
     apply simp
    apply simp
    apply (case_tac t)
     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
    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 s)
     apply simp
     apply (drule in_errorD)
     apply simp
    apply (simp add: map_snd_def split: split_if_asm)
     apply fast
    apply (drule in_errorD)
    apply simp
    done

    text {*
      There used to be a condition here that each instruction must have a
      successor. This is not needed any more, because the definition of
      @{term error} trivially ensures that there is a successor for
      the critical case where @{term app} does not hold.
    *}
    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

lemmas err_step_defs:

      err_step n app step p t ==
      case t of Err => error n
      | OK t' => if app p t' then map_snd OK (step p t') else error n

      map_snd f == map (%(x, y). (x, f y))

      error n == map (%x. (x, Err)) [0..<n]

lemmas err_step_defs:

      err_step n app step p t ==
      case t of Err => error n
      | OK t' => if app p t' then map_snd OK (step p t') else error n

      map_snd f == map (%(x, y). (x, f y))

      error n == map (%x. (x, Err)) [0..<n]

lemma bounded_err_stepD:

      [| bounded (err_step n app step) n; p < n; app p a; (q, b) ∈ set (step p a) |]
      ==> q < n

lemma in_map_sndD:

      (a, b) ∈ set (map_snd f xs) ==> ∃b'. (a, b') ∈ set xs

lemma bounded_err_stepI:

      ∀p<n. ∀s. ap p s --> (∀(q, s')∈set (step p s). q < n)
      ==> bounded (err_step n ap step) n

lemma bounded_lift:

      bounded step n ==> bounded (err_step n app step) n

lemma le_list_map_OK:

      (map OK a <=[Err.le r] map OK b) = (a <=[r] b)

lemma map_snd_lessI:

      x <=|r| y ==> map_snd OK x <=|Err.le r| map_snd OK y

lemma mono_lift:

      [| order r; 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 --> step p s <=|r| step p t |]
      ==> SemilatAlg.mono (Err.le r) (err_step n app step) n (err A)

lemma in_errorD:

      (x, y) ∈ set (error n) ==> y = Err

lemma pres_type_lift:

      ∀s∈A. ∀p<n. app p s --> (∀(q, s')∈set (step p s). s' ∈ A)
      ==> pres_type (err_step n app step) n (err A)

lemma wt_err_imp_wt_app_eff:

      [| wt_err_step r (err_step (length ts) app step) ts;
         bounded (err_step (length ts) app step) (length ts) |]
      ==> wt_app_eff r app step (map ok_val ts)

lemma wt_app_eff_imp_wt_err:

      [| wt_app_eff r app step ts;
         bounded (err_step (length ts) app step) (length ts) |]
      ==> wt_err_step r (err_step (length ts) app step) (map OK ts)