# Theory LBVCorrect

Up to index of Isabelle/HOL/MicroJava

theory LBVCorrect
imports LBVSpec Typing_Framework
begin

    (*
        ID:         $Id: LBVCorrect.thy,v 1.36 2005/06/17 14:13:08 haftmann Exp $
        Author:     Gerwin Klein
        Copyright   1999 Technische Universitaet Muenchen
    *)

    header {* \isaheader{Correctness of the LBV} *}

    theory LBVCorrect imports LBVSpec Typing_Framework begin

    locale (open) lbvs = lbv +
      fixes s0  :: 'a ("s0")
      fixes c   :: "'a list"
      fixes ins :: "'b list"
      fixes phi :: "'a list" ("φ")
      defines phi_def:
      "φ ≡ map (λpc. if c!pc = ⊥ then wtl (take pc ins) c 0 s0 else c!pc)
           [0..<length ins]"

      assumes bounded: "bounded step (length ins)"
      assumes cert: "cert_ok c (length ins) \<top> ⊥ A"
      assumes pres: "pres_type step (length ins) A"

    lemma (in lbvs) phi_None [intro?]:
      "[| pc < length ins; c!pc = ⊥ |] ==> φ ! pc = wtl (take pc ins) c 0 s0"
      by (simp add: phi_def)

    lemma (in lbvs) phi_Some [intro?]:
      "[| pc < length ins; c!pc ≠ ⊥ |] ==> φ ! pc = c ! pc"
      by (simp add: phi_def)

    lemma (in lbvs) phi_len [simp]:
      "length φ = length ins"
      by (simp add: phi_def)

    lemma (in lbvs) wtl_suc_pc:
      assumes all: "wtl ins c 0 s0 ≠ \<top>"
      assumes pc:  "pc+1 < length ins"
      shows "wtl (take (pc+1) ins) c 0 s0 ≤r φ!(pc+1)"
    proof -
      from all pc
      have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) ≠ T" by (rule wtl_all)
      with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
    qed

    lemma (in lbvs) wtl_stable:
      assumes wtl: "wtl ins c 0 s0 ≠ \<top>"
      assumes s0:  "s0 ∈ A"
      assumes pc:  "pc < length ins"
      shows "stable r step φ pc"
    proof (unfold stable_def, clarify)
      fix pc' s' assume step: "(pc',s') ∈ set (step pc (φ ! pc))"
                          (is "(pc',s') ∈ set (?step pc)")

      from bounded pc step have pc': "pc' < length ins" by (rule boundedD)

      have tkpc: "wtl (take pc ins) c 0 s0 ≠ \<top>" (is "?s1 ≠ _") by (rule wtl_take)
      have s2: "wtl (take (pc+1) ins) c 0 s0 ≠ \<top>" (is "?s2 ≠ _") by (rule wtl_take)

      from wtl pc have wt_s1: "wtc c pc ?s1 ≠ \<top>" by (rule wtl_all)

      have c_Some: "∀pc t. pc < length ins --> c!pc ≠ ⊥ --> φ!pc = c!pc"
        by (simp add: phi_def)
      have c_None: "c!pc = ⊥ ==> φ!pc = ?s1" ..

      from wt_s1 pc c_None c_Some
      have inst: "wtc c pc ?s1  = wti c pc (φ!pc)"
        by (simp add: wtc split: split_if_asm)

      have "?s1 ∈ A" by (rule wtl_pres)
      with pc c_Some cert c_None
      have "φ!pc ∈ A" by (cases "c!pc = ⊥") (auto dest: cert_okD1)
      with pc pres
      have step_in_A: "snd`set (?step pc) ⊆ A" by (auto dest: pres_typeD2)

      show "s' <=_r φ!pc'"
      proof (cases "pc' = pc+1")
        case True
        with pc' cert
        have cert_in_A: "c!(pc+1) ∈ A" by (auto dest: cert_okD1)
        from True pc' have pc1: "pc+1 < length ins" by simp
        with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)
        with inst
        have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
        also
        from s2 merge have "… ≠ \<top>" (is "?merge ≠ _") by simp
        with cert_in_A step_in_A
        have "?merge = (map snd [(p',t')∈?step pc. p'=pc+1] ++_f (c!(pc+1)))"
          by (rule merge_not_top_s)
        finally
        have "s' <=_r ?s2" using step_in_A cert_in_A True step
          by (auto intro: pp_ub1')
        also
        from wtl pc1 have "?s2 <=_r φ!(pc+1)" by (rule wtl_suc_pc)
        also note True [symmetric]
        finally show ?thesis by simp
      next
        case False
        from wt_s1 inst
        have "merge c pc (?step pc) (c!(pc+1)) ≠ \<top>" by (simp add: wti)
        with step_in_A
        have "∀(pc', s')∈set (?step pc). pc'≠pc+1 --> s' <=_r c!pc'"
          by - (rule merge_not_top)
        with step False
        have ok: "s' <=_r c!pc'" by blast
        moreover
        from ok
        have "c!pc' = ⊥ ==> s' = ⊥" by simp
        moreover
        from c_Some pc'
        have "c!pc' ≠ ⊥ ==> φ!pc' = c!pc'" by auto
        ultimately
        show ?thesis by (cases "c!pc' = ⊥") auto
      qed
    qed

    lemma (in lbvs) phi_not_top:
      assumes wtl: "wtl ins c 0 s0 ≠ \<top>"
      assumes pc:  "pc < length ins"
      shows "φ!pc ≠ \<top>"
    proof (cases "c!pc = ⊥")
      case False with pc
      have "φ!pc = c!pc" ..
      also from cert pc have "… ≠ \<top>" by (rule cert_okD4)
      finally show ?thesis .
    next
      case True with pc
      have "φ!pc = wtl (take pc ins) c 0 s0" ..
      also from wtl have "… ≠ \<top>" by (rule wtl_take)
      finally show ?thesis .
    qed

    lemma (in lbvs) phi_in_A:
      assumes wtl: "wtl ins c 0 s0 ≠ \<top>"
      assumes s0:  "s0 ∈ A"
      shows "φ ∈ list (length ins) A"
    proof -
      { fix x assume "x ∈ set φ"
        then obtain xs ys where "φ = xs @ x # ys"
          by (auto simp add: in_set_conv_decomp)
        then obtain pc where pc: "pc < length φ" and x: "φ!pc = x"
          by (simp add: that [of "length xs"] nth_append)

        from wtl s0 pc
        have "wtl (take pc ins) c 0 s0 ∈ A" by (auto intro!: wtl_pres)
        moreover
        from pc have "pc < length ins" by simp
        with cert have "c!pc ∈ A" ..
        ultimately
        have "φ!pc ∈ A" using pc by (simp add: phi_def)
        hence "x ∈ A" using x by simp
      }
      hence "set φ ⊆ A" ..
      thus ?thesis by (unfold list_def) simp
    qed

    lemma (in lbvs) phi0:
      assumes wtl: "wtl ins c 0 s0 ≠ \<top>"
      assumes 0:   "0 < length ins"
      shows "s0 <=_r φ!0"
    proof (cases "c!0 = ⊥")
      case True
      with 0 have "φ!0 = wtl (take 0 ins) c 0 s0" ..
      moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
      ultimately have "φ!0 = s0" by simp
      thus ?thesis by simp
    next
      case False
      with 0 have "phi!0 = c!0" ..
      moreover
      have "wtl (take 1 ins) c 0 s0 ≠ \<top>"  by (rule wtl_take)
      with 0 False
      have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
      ultimately
      show ?thesis by simp
    qed

    theorem (in lbvs) wtl_sound:
      assumes "wtl ins c 0 s0 ≠ \<top>"
      assumes "s0 ∈ A"
      shows "∃ts. wt_step r \<top> step ts"
    proof -
      have "wt_step r \<top> step φ"
      proof (unfold wt_step_def, intro strip conjI)
        fix pc assume "pc < length φ"
        then obtain "pc < length ins" by simp
        show "φ!pc ≠ \<top>" by (rule phi_not_top)
        show "stable r step φ pc" by (rule wtl_stable)
      qed
      thus ?thesis ..
    qed

    theorem (in lbvs) wtl_sound_strong:
      assumes "wtl ins c 0 s0 ≠ \<top>"
      assumes "s0 ∈ A"
      assumes "0 < length ins"
      shows "∃ts ∈ list (length ins) A. wt_step r \<top> step ts ∧ s0 <=_r ts!0"
    proof -
      have "φ ∈ list (length ins) A" by (rule phi_in_A)
      moreover
      have "wt_step r \<top> step φ"
      proof (unfold wt_step_def, intro strip conjI)
        fix pc assume "pc < length φ"
        then obtain "pc < length ins" by simp
        show "φ!pc ≠ \<top>" by (rule phi_not_top)
        show "stable r step φ pc" by (rule wtl_stable)
      qed
      moreover
      have "s0 <=_r φ!0" by (rule phi0)
      ultimately
      show ?thesis by fast
    qed

    end

lemma phi_None:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; pc < length ins; c ! pc = B |]
      ==> map (%pc. if c ! pc = B
                    then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                    else c ! pc)
           [0..<length ins] !
          pc =
          wtl_inst_list (take pc ins) c f r T B step 0 s0.0

lemma phi_Some:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; pc < length ins; c ! pc ≠ B |]
      ==> map (%pc. if c ! pc = B
                    then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                    else c ! pc)
           [0..<length ins] !
          pc =
          c ! pc

lemma phi_len:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A |]
      ==> length
           (map (%pc. if c ! pc = B
                      then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                      else c ! pc)
             [0..<length ins]) =
          length ins

lemma wtl_suc_pc:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         pc + 1 < length ins |]
      ==> wtl_inst_list (take (pc + 1) ins) c f r T B step 0 s0.0
          <=_r map (%pc. if c ! pc = B
                         then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                         else c ! pc)
                [0..<length ins] !
               (pc + 1)

lemma wtl_stable:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         s0.0 ∈ A; pc < length ins |]
      ==> stable r step
           (map (%pc. if c ! pc = B
                      then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                      else c ! pc)
             [0..<length ins])
           pc

lemma phi_not_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         pc < length ins |]
      ==> map (%pc. if c ! pc = B
                    then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                    else c ! pc)
           [0..<length ins] !
          pc ≠
          T

lemma phi_in_A:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         s0.0 ∈ A |]
      ==> map (%pc. if c ! pc = B
                    then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                    else c ! pc)
           [0..<length ins]
          ∈ list (length ins) A

lemma phi0:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         0 < length ins |]
      ==> s0.0
          <=_r map (%pc. if c ! pc = B
                         then wtl_inst_list (take pc ins) c f r T B step 0 s0.0
                         else c ! pc)
                [0..<length ins] !
               0

theorem wtl_sound:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         s0.0 ∈ A |]
      ==> ∃ts. wt_step r T step ts

theorem wtl_sound_strong:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         bounded step (length ins); cert_ok c (length ins) T B A;
         pres_type step (length ins) A; wtl_inst_list ins c f r T B step 0 s0.0 ≠ T;
         s0.0 ∈ A; 0 < length ins |]
      ==> ∃ts∈list (length ins) A. wt_step r T step ts ∧ s0.0 <=_r ts ! 0