header {* \isaheader{Monotonicity of eff and app} *}
theory EffectMono imports Effect begin
declare not_Err_eq [iff]
declare widens_trans[trans]
lemma appi_mono:
assumes wf: "wf_prog p P"
assumes less: "P \<turnstile> τ ≤i τ'"
shows "appi (i,P,mxs,mpc,rT,τ') ==> appi (i,P,mxs,mpc,rT,τ)"
proof -
assume app: "appi (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 "appi (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
have "if is_external_call P (ST' ! n) M then ∃U. P \<turnstile> ST' ! n•M(rev (take n ST')) :: U
else ∃D Ts T m C'. ST' ! n = Class D ∧ P \<turnstile> D sees M:Ts -> T = m in C' ∧ P \<turnstile> rev (take n ST') [≤] Ts"
by fastsimp
moreover
from less have "P \<turnstile> ST!n ≤ ST'!n"
by(auto dest: list_all2_nthD2[OF _ n])
{ fix D Ts T m C'
assume 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'"
and nec: "¬ is_external_call P (ST' ! n) M"
from D_M wf_Object_method_empty[OF wf]
have "D ≠ Object" by(auto)
with `P \<turnstile> ST!n ≤ ST'!n`
obtain D' where
D': "ST!n = Class D'" and DsubC: "P \<turnstile> D' \<preceq>* D"
using D ST 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 D nec have ?thesis
by(auto dest: external_call_not_sees_method[OF wf]) }
moreover {
fix U
assume exc: "is_external_call P (ST' ! n) M"
and wtext: "P \<turnstile> ST' ! n•M(rev (take n ST')) :: U"
from exc have "is_external_call P (ST ! n) M"
using `P \<turnstile> ST!n ≤ ST'!n` ST by(rule is_external_call_widen_mono)
moreover from less have "P \<turnstile> rev (take n ST) [≤] rev (take n ST')" by auto
with wtext `P \<turnstile> ST!n ≤ ST'!n` ST obtain U' where "P \<turnstile> ST ! n•M(rev (take n ST)) :: U'"
and "P \<turnstile> U' ≤ U" by(auto dest: external_WTrt_widen_mono)
ultimately have ?thesis using app Invoke by auto }
ultimately have ?thesis by(auto split: split_if_asm) }
ultimately show ?thesis by blast
next
case (Getfield F C)
with app less wf_Object_field_empty[OF wf] show ?thesis
by(fastsimp simp add: sees_field_def dest: has_fields_fun)
next
case (Putfield F C)
with app less wf_Object_field_empty[OF wf] show ?thesis
by (fastsimp intro: widen_trans rtrancl_trans simp add: sees_field_def dest: has_fields_fun)
next
case Return
with app less show ?thesis by (fastsimp intro: widen_trans)
next
case ALoad
with app less show ?thesis
apply(clarsimp)
by(case_tac "T = NT", auto simp add: widen_Array)
next
case AStore
with app less show ?thesis
apply(clarsimp)
by(case_tac "U = NT", auto simp add: widen_Array)
next
case ALength
with app less show ?thesis by(auto simp add: widen_Array)
next
case (Checkcast T)
with app less show ?thesis
by(auto elim!: refTE simp: widen_Array)
next
case ThrowExc
with app less show ?thesis
by(auto elim!: refTE simp: widen_Array)
next
case MEnter
with app less show ?thesis
by(auto elim!: refTE simp: widen_Array)
next
case MExit
with app less show ?thesis
by(auto elim!: refTE simp: widen_Array)
next
case (BinOpInstr bop)
with app less show ?thesis by(force dest: WTrt_binop_widen_mono)
qed (auto elim!: refTE not_refTE)
qed
lemma succs_mono:
assumes wf: "wf_prog p P" and appi: "appi (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 appi 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
next
case ALoad
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ')
assume "P \<turnstile> τ ≤i τ'"
moreover
with appi ALoad have "1 < size ST" by (auto dest: list_all2_lengthD)
ultimately
have "P \<turnstile> ST!1 ≤ ST'!1" by (auto simp add: fun_of_def dest: list_all2_nthD)
with ALoad show ?thesis by auto
next
case AStore
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ')
assume "P \<turnstile> τ ≤i τ'"
moreover
with appi AStore have "2 < size ST" by (auto dest: list_all2_lengthD)
ultimately
have "P \<turnstile> ST!2 ≤ ST'!2" by (auto simp add: fun_of_def dest: list_all2_nthD)
with AStore show ?thesis by auto
next
case ALength
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ')
assume "P \<turnstile> τ ≤i τ'"
moreover
with appi ALength have "0 < size ST" by (auto dest: list_all2_lengthD)
ultimately
have "P \<turnstile> ST!0 ≤ ST'!0" by (auto simp add: fun_of_def dest: list_all2_nthD)
with ALength show ?thesis by auto
next
case MEnter
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ')
assume "P \<turnstile> τ ≤i τ'"
moreover
with appi MEnter have "0 < size ST" by (auto dest: list_all2_lengthD)
ultimately
have "P \<turnstile> ST!0 ≤ ST'!0" by (auto simp add: fun_of_def dest: list_all2_nthD)
with MEnter show ?thesis by auto
next
case MExit
obtain ST LT ST' LT' where
[simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ')
assume "P \<turnstile> τ ≤i τ'"
moreover
with appi MExit have "0 < size ST" by (auto dest: list_all2_lengthD)
ultimately
have "P \<turnstile> ST!0 ≤ ST'!0" by (auto simp add: fun_of_def dest: list_all2_nthD)
with MExit 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
appi: "appi (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 appi have "appi (i, P, pc, m, rT, τ1)" by (rule appi_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 appi 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 effi_mono:
assumes wf: "wf_prog p P"
assumes less: "P \<turnstile> τ ≤i τ'"
assumes appi: "app i P m rT pc mpc xt (Some τ')"
assumes succs: "succs i τ pc ≠ []" "succs i τ' pc ≠ []"
shows "P \<turnstile> effi (i,P,τ) ≤i effi (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 appi
have app: "app i P m rT pc mpc xt (Some τ)" by (rule app_mono)
from less app appi show ?thesis
proof (cases i)
case ThrowExc 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 appi 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 appi
show ?thesis by auto
next
case Store with less app appi
show ?thesis by (auto simp add: list_all2_update_cong)
next
case (Invoke M n)
with appi 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)
from ST' appi Invoke
have "if is_external_call P (ST' ! n) M then ∃U. P \<turnstile> ST' ! n•M(rev (take n ST')) :: U
else ∃D Ts T m C'. ST' ! n = Class D ∧ P \<turnstile> D sees M:Ts -> T = m in C' ∧ P \<turnstile> rev (take n ST') [≤] Ts"
by fastsimp
moreover
from less have "P \<turnstile> ST!n ≤ ST'!n"
by(auto dest: list_all2_nthD2[OF _ n])
{ fix D Ts T m C'
assume D: "ST' ! n = Class D"
and D_M: "P \<turnstile> D sees M: Ts->T = m in C'"
and nec: "¬ is_external_call P (ST' ! n) M"
from D_M wf_Object_method_empty[OF wf]
have "D ≠ Object" by(auto)
with `P \<turnstile> ST!n ≤ ST'!n` obtain D' where
D': "ST!n = Class D'" and DsubC: "P \<turnstile> D' \<preceq>* D"
using D ST by(auto simp: widen_Class)
from D_M `P \<turnstile> ST!n ≤ ST'!n` D ST D'
have nexc: "¬ is_external_call P (ST ! n) M"
by(auto dest!: external_call_not_sees_method[OF wf])
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 nexc nec
have ?thesis by(auto intro: list_all2_dropI) }
moreover
{ fix U
assume nexc': "is_external_call P (ST' ! n) M"
and wtext: "P \<turnstile> ST' ! n•M(rev (take n ST')) :: U"
moreover with `P \<turnstile> ST!n ≤ ST'!n` ST
have "is_external_call P (ST ! n) M"
by-(rule is_external_call_widen_mono)
moreover from less have "P \<turnstile> rev (take n ST) [≤] rev (take n ST')" by auto
with wtext `P \<turnstile> ST!n ≤ ST'!n` ST obtain U' where "P \<turnstile> ST ! n•M(rev (take n ST)) :: U'"
and "P \<turnstile> U' ≤ U" by(auto dest: external_WTrt_widen_mono)
ultimately have ?thesis using Invoke ST less by(auto dest: external_WT_The_conv) }
ultimately show ?thesis by(auto split: split_if_asm)
next
case ALoad with less app appi succs
show ?thesis by(auto split: split_if_asm dest: Array_Array_widen)
next
case AStore with less app appi succs
show ?thesis by(auto split: split_if_asm dest: Array_Array_widen)
next
case (BinOpInstr bop)
with less app appi succs show ?thesis
by auto(force dest: WTrt_binop_widen_mono WTrt_binop_fun)
qed auto
qed
end