header {* \isaheader{Monotonicity of eff and app} *}
theory EffectMono imports Effect begin
declare not_Err_eq [iff]
lemma app⇣i_mono:
assumes wf: "wf_prog p P"
assumes less: "P \<turnstile> τ ≤⇩i τ'"
shows "app⇣i (i,P,mxs,mpc,rT,τ') ==> app⇣i (i,P,mxs,mpc,rT,τ)"
proof -
assume app: "app⇣i (i,P,mxs,mpc,rT,τ')"
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and
[simp]: "τ' = (ST',LT')"
by (cases τ, cases τ')
from less have [simp]: "size ST = size ST'" and [simp]: "size LT = size LT'"
by (auto dest: list_all2_lengthD)
note [iff] = list_all2_Cons2 widen_Class
note [simp] = fun_of_def
from app less show "app⇣i (i,P,mxs,mpc,rT,τ)"
proof (cases i)
case Load
with app less show ?thesis by (auto dest!: list_all2_nthD)
next
case (Invoke M n)
with app have n: "n < size ST'" by simp
{ assume "ST!n = NT" hence ?thesis using n app Invoke by simp }
moreover {
assume "ST'!n = NT"
moreover with n less have "ST!n = NT"
by (auto dest: list_all2_nthD)
ultimately have ?thesis using n app Invoke by simp
}
moreover {
assume ST: "ST!n ≠ NT" and ST': "ST'!n ≠ NT"
from ST' app Invoke obtain D Ts T m C' where
D: "ST' ! n = Class D" and
Ts: "P \<turnstile> rev (take n ST') [≤] Ts" and
D_M: "P \<turnstile> D sees M: Ts->T = m in C'"
by auto
from n D less have "P \<turnstile> ST!n ≤ ST'!n"
by (fastforce dest: list_all2_nthD2)
with D ST obtain D' where
D': "ST!n = Class D'" and DsubC: "P \<turnstile> D' \<preceq>⇧* D" by auto
from wf D_M DsubC obtain Ts' T' m' C'' where
D'_M: "P \<turnstile> D' sees M: Ts'->T' = m' in C''" and
Ts': "P \<turnstile> Ts [≤] Ts'"
by (blast dest: sees_method_mono)
from less have "P \<turnstile> rev (take n ST) [≤] rev (take n ST')" by simp
also note Ts also note Ts'
finally have "P \<turnstile> rev (take n ST) [≤] Ts'" .
with D'_M D' app less Invoke have ?thesis by fastforce
}
ultimately show ?thesis by blast
next
case Getfield
with app less show ?thesis by (fastforce intro: rtrancl_trans)
next
case (Putfield F C)
with app less show ?thesis by (fastforce intro: widen_trans rtrancl_trans)
next
case Return
with app less show ?thesis by (fastforce intro: widen_trans)
qed (auto elim!: refTE not_refTE)
qed
lemma succs_mono:
assumes wf: "wf_prog p P" and app⇣i: "app⇣i (i,P,mxs,mpc,rT,τ')"
shows "P \<turnstile> τ ≤⇩i τ' ==> set (succs i τ pc) ⊆ set (succs i τ' pc)"
proof (cases i)
case (Invoke M n)
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ')
assume "P \<turnstile> τ ≤⇩i τ'"
moreover
with app⇣i Invoke have "n < size ST" by (auto dest: list_all2_lengthD)
ultimately
have "P \<turnstile> ST!n ≤ ST'!n" by (auto simp add: fun_of_def dest: list_all2_nthD)
with Invoke show ?thesis by auto
qed auto
lemma app_mono:
assumes wf: "wf_prog p P"
assumes less': "P \<turnstile> τ ≤' τ'"
shows "app i P m rT pc mpc xt τ' ==> app i P m rT pc mpc xt τ"
proof (cases τ)
case None thus ?thesis by simp
next
case (Some τ⇣1)
moreover
with less' obtain τ⇣2 where τ⇣2: "τ' = Some τ⇣2" by (cases τ') auto
ultimately have less: "P \<turnstile> τ⇣1 ≤⇩i τ⇣2" using less' by simp
assume "app i P m rT pc mpc xt τ'"
with Some τ⇣2 obtain
app⇣i: "app⇣i (i, P, pc, m, rT, τ⇣2)" and
xcpt: "xcpt_app i P pc m xt τ⇣2" and
succs: "∀(pc',s')∈set (eff i P pc xt (Some τ⇣2)). pc' < mpc"
by (auto simp add: app_def)
from wf less app⇣i have "app⇣i (i, P, pc, m, rT, τ⇣1)" by (rule app⇣i_mono)
moreover
from less have "size (fst τ⇣1) = size (fst τ⇣2)"
by (cases τ⇣1, cases τ⇣2) (auto dest: list_all2_lengthD)
with xcpt have "xcpt_app i P pc m xt τ⇣1" by (simp add: xcpt_app_def)
moreover
from wf app⇣i less have "∀pc. set (succs i τ⇣1 pc) ⊆ set (succs i τ⇣2 pc)"
by (blast dest: succs_mono)
with succs
have "∀(pc',s')∈set (eff i P pc xt (Some τ⇣1)). pc' < mpc"
by (cases τ⇣1, cases τ⇣2)
(auto simp add: eff_def norm_eff_def xcpt_eff_def dest: bspec)
ultimately
show ?thesis using Some by (simp add: app_def)
qed
lemma eff⇣i_mono:
assumes wf: "wf_prog p P"
assumes less: "P \<turnstile> τ ≤⇩i τ'"
assumes app⇣i: "app i P m rT pc mpc xt (Some τ')"
assumes succs: "succs i τ pc ≠ []" "succs i τ' pc ≠ []"
shows "P \<turnstile> eff⇣i (i,P,τ) ≤⇩i eff⇣i (i,P,τ')"
proof -
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and
[simp]: "τ' = (ST',LT')"
by (cases τ, cases τ')
note [simp] = eff_def app_def fun_of_def
from less have "P \<turnstile> (Some τ) ≤' (Some τ')" by simp
from wf this app⇣i
have app: "app i P m rT pc mpc xt (Some τ)" by (rule app_mono)
from less app app⇣i show ?thesis
proof (cases i)
case Throw with succs have False by simp
thus ?thesis ..
next
case Return with succs have False by simp
thus ?thesis ..
next
case (Load i)
from Load app obtain y where
y: "i < size LT" "LT!i = OK y" by clarsimp
from Load app⇣i obtain y' where
y': "i < size LT'" "LT'!i = OK y'" by clarsimp
from less have "P \<turnstile> LT [≤⇩\<top>] LT'" by simp
with y y' have "P \<turnstile> y ≤ y'" by (auto dest: list_all2_nthD)
with Load less y y' app app⇣i
show ?thesis by auto
next
case Store with less app app⇣i
show ?thesis by (auto simp add: list_all2_update_cong)
next
case (Invoke M n)
with app⇣i have n: "n < size ST'" by simp
from less have [simp]: "size ST = size ST'"
by (auto dest: list_all2_lengthD)
from Invoke succs have ST: "ST!n ≠ NT" and ST': "ST'!n ≠ NT"
by (auto split: split_if_asm)
from ST' app⇣i Invoke obtain D Ts T m C' where
D: "ST' ! n = Class D" and
D_M: "P \<turnstile> D sees M: Ts->T = m in C'"
by auto
from n D less have "P \<turnstile> ST!n ≤ ST'!n"
by (fastforce dest: list_all2_nthD2)
with D ST obtain D' where
D': "ST ! n = Class D'" and DsubC: "P \<turnstile> D' \<preceq>⇧* D"
by (auto simp: widen_Class)
from wf D_M DsubC obtain Ts' T' m' C'' where
D'_M: "P \<turnstile> D' sees M: Ts'->T' = m' in C''" and
Ts': "P \<turnstile> T' ≤ T"
by (blast dest: sees_method_mono)
with Invoke n D D' D_M less
show ?thesis by (auto intro: list_all2_dropI)
qed auto
qed
end