# Theory LBVCorrect

Up to index of Isabelle/HOL/HOL-MicroJava-skip_proofs

theory LBVCorrect
imports LBVSpec
`(*  Author:     Gerwin Klein    Copyright   1999 Technische Universitaet Muenchen*)header {* \isaheader{Correctness of the LBV} *}theory LBVCorrectimports LBVSpec Typing_Frameworkbeginlocale lbvs = lbv +  fixes s0  :: 'a ("s⇩0")  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 s⇩0 ≠ \<top>"   assumes pc:  "pc+1 < length ins"  shows "wtl (take (pc+1) ins) c 0 s0 \<sqsubseteq>⇩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)qedlemma (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)  from wtl have tkpc: "wtl (take pc ins) c 0 s0 ≠ \<top>" (is "?s1 ≠ _") by (rule wtl_take)  from wtl 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)  from pc 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)  from pres cert s0 wtl pc 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') \<leftarrow> ?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   qedqed  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 .qedlemma (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 pres cert 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) simpqedlemma (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 simpnext  case False  with 0 have "phi!0 = c!0" ..  moreover   from wtl 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 simpqedtheorem (in lbvs) wtl_sound:  assumes wtl: "wtl ins c 0 s0 ≠ \<top>"   assumes s0: "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 have pc: "pc < length ins" by simp    with wtl show "φ!pc ≠ \<top>" by (rule phi_not_top)    from wtl s0 pc show "stable r step φ pc" by (rule wtl_stable)  qed  thus ?thesis ..qedtheorem (in lbvs) wtl_sound_strong:  assumes wtl: "wtl ins c 0 s0 ≠ \<top>"   assumes s0: "s0 ∈ A"   assumes nz: "0 < length ins"  shows "∃ts ∈ list (length ins) A. wt_step r \<top> step ts ∧ s0 <=_r ts!0"proof -  from wtl s0 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 have pc: "pc < length ins" by simp    with wtl show "φ!pc ≠ \<top>" by (rule phi_not_top)    from wtl s0 pc show "stable r step φ pc" by (rule wtl_stable)  qed  moreover  from wtl nz have "s0 <=_r φ!0" by (rule phi0)  ultimately  show ?thesis by fastqedend`