Theory Language_Composition
theory Language_Composition
imports Strongly_Secure_Skip_Assign
begin
context Strongly_Secure_Programs
begin
theorem Compositionality_Seq:
assumes relatedpart1: "[c1] ≈⇘d⇙ [c1']"
assumes relatedpart2: "[c2] ≈⇘d⇙ [c2']"
shows "[c1;c2] ≈⇘d⇙ [c1';c2']"
proof -
define R0 where "R0 = {(S1,S2). ∃c1 c1' c2 c2' W W'.
S1 = (c1;c2)#W ∧ S2 = (c1';c2')#W' ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧ W ≈⇘d⇙ W'}"
from relatedpart1 relatedpart2 trivialpair_in_USdB
have inR0: "([c1;c2],[c1';c2']) ∈ R0"
by (simp add: R0_def)
have uptoR0: "d_Bisimulation_Up_To_USdB d R0"
proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
from USdBsym
show "sym R0"
by (simp add: sym_def R0_def, fastforce)
next
fix S1 S2
assume inR0: "(S1,S2) ∈ R0"
with USdBeqlen show "length S1 = length S2"
by (auto simp add: R0_def)
next
fix S1 S2 RS m1 m2 m1' i
assume inR0: "(S1,S2) ∈ R0"
assume irange: "i < length S1"
assume S1step: "⟨S1!i,m1⟩ → ⟨RS,m2⟩"
assume dequal: "m1 =⇘d⇙ m1'"
from inR0 obtain c1 c1' c2 c2' V V'
where R0def': "S1 = (c1;c2)#V ∧ S2 = (c1';c2')#V' ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧ V ≈⇘d⇙ V'"
by (simp add: R0_def, force)
with irange have case_distinction1:
"i = 0 ∨ (V ≠ [] ∧ i ≠ 0)"
by auto
moreover
have case1: "i = 0 ⟹
∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
proof -
assume i0: "i = 0"
with R0def' S1step obtain c3 W where case_distinction:
"RS = [c2] ∧ ⟨c1,m1⟩ → ⟨[],m2⟩
∨ RS = (c3;c2)#W ∧ ⟨c1,m1⟩ → ⟨c3#W,m2⟩"
by (simp, metis MWLfSteps_det_cases(3))
moreover
{
assume RSassump: "RS = [c2]"
assume StepAssump: "⟨c1,m1⟩ → ⟨[],m2⟩"
from USdBeqlen[of "[]"] StepAssump R0def'
USdB_Strong_d_Bisimulation dequal
strongdB_aux[of "d" "≈⇘d⇙" "i"
"[c1]" "[c1']" "m1" "[]" "m2" "m1'"] i0
obtain W' m2' where c1c1'reason:
"⟨c1',m1'⟩ → ⟨W',m2'⟩ ∧ W' = []
∧ [] ≈⇘d⇙ W' ∧ m2 =⇘d⇙ m2'"
by fastforce
with c1c1'reason have conclpart:
"⟨c1';c2',m1'⟩ → ⟨[c2'],m2'⟩ ∧ m2 =⇘d⇙ m2'"
by (simp add: MWLfSteps_det.seq1)
with RSassump R0def' i0 have case1_concl:
"∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by (simp, rule_tac x="[c2']" in exI, auto)
}
moreover
{
assume RSassump: "RS = (c3;c2)#W"
assume StepAssump: "⟨c1,m1⟩ → ⟨c3#W,m2⟩"
from StepAssump R0def' USdB_Strong_d_Bisimulation dequal
strongdB_aux[of "d" "≈⇘d⇙" "i" "[c1]" "[c1']" "m1"
"c3#W" "m2" "m1'"] i0
obtain V'' m2' where c1c1'reason:
"⟨c1',m1'⟩ → ⟨V'',m2'⟩
∧ (c3#W) ≈⇘d⇙ V'' ∧ m2 =⇘d⇙ m2'"
by fastforce
with USdBeqlen[of "c3#W" "V''"] obtain c3' W'
where V''reason:
"V'' = c3'#W' ∧ length W = length W'"
by (cases V'', force, force)
with c1c1'reason have conclpart1:
"⟨c1';c2',m1'⟩ → ⟨(c3';c2')#W',m2'⟩ ∧ m2 =⇘d⇙ m2'"
by (simp add: MWLfSteps_det.seq2)
from V''reason c1c1'reason
USdB_decomp_head_tail[of "c3" "W"]
USdB_Strong_d_Bisimulation
have c3aWinUSDB:
"[c3] ≈⇘d⇙ [c3'] ∧ W ≈⇘d⇙ W'"
by blast
with R0def' have conclpart2:
"((c3;c2)#W,(c3';c2')#W') ∈ R0"
by (auto simp add: R0_def)
with i0 RSassump R0def' V''reason conclpart1
have case2_concl:
"∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by (rule_tac x="(c3';c2')#W'" in exI, auto)
}
ultimately
show "∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by blast
qed
moreover
have case2: "⟦ V ≠ []; i ≠ 0 ⟧
⟹ ∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
proof -
assume Vnonempt: "V ≠ []"
assume inot0: "i ≠ 0"
with Vnonempt irange R0def' have i1range:
"(i-Suc 0) < length V"
by simp
from inot0 R0def' have S1ieq: "S1!i = V!(i-Suc 0)"
by auto
from inot0 R0def' have "S2!i = V'!(i-Suc 0)"
by auto
with S1ieq R0def' S1step i1range dequal
USdB_Strong_d_Bisimulation
strongdB_aux[of "d" "USdB d"
"i-Suc 0" "V" "V'" "m1" "RS" "m2" "m1'"]
show "∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by force
qed
ultimately show "∃RS' m2'. ⟨S2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by auto
qed
hence "R0 ⊆ ≈⇘d⇙"
by (rule Up_To_Technique)
with inR0 show ?thesis
by auto
qed
theorem Compositionality_Fork:
fixes V::"('exp,'id) MWLfCom list"
assumes relatedmain: "[c] ≈⇘d⇙ [c']"
assumes relatedthreads: "V ≈⇘d⇙ V'"
shows "[fork c V] ≈⇘d⇙ [fork c' V']"
proof -
define R0 where "R0 = {(F1,F2). ∃c1 c1' W W'.
F1 = [fork c1 W] ∧ F2 = [fork c1' W']
∧ [c1] ≈⇘d⇙ [c1'] ∧ W ≈⇘d⇙ W'}"
from relatedmain relatedthreads
have inR0: "([fork c V],[fork c' V']) ∈ R0"
by (simp add: R0_def)
have uptoR0: "d_Bisimulation_Up_To_USdB d R0"
proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
from USdBsym show "sym R0"
by (simp add: R0_def sym_def, auto)
next
fix F1 F2
assume inR0: "(F1,F2) ∈ R0"
with R0_def USdBeqlen show "length F1 = length F2"
by auto
next
fix F1 F2 c1V m1 m2 m1' i
assume inR0: "(F1,F2) ∈ R0"
assume irange: "i < length F1"
assume F1step: "⟨F1!i,m1⟩ → ⟨c1V,m2⟩"
assume dequal: "m1 =⇘d⇙ m1'"
from inR0 obtain c1 c1' V V'
where R0def': "F1 = [fork c1 V] ∧ F2 = [fork c1' V'] ∧
[c1] ≈⇘d⇙ [c1'] ∧ V ≈⇘d⇙ V'"
by (simp add: R0_def, force)
from irange R0def' F1step
have rew: "c1V = c1#V ∧ m2 = m1"
by (simp, metis MWLf_semantics.MWLfSteps_det_cases(6))
from irange R0def' MWLfSteps_det.fork have F2step:
"⟨F2!i,m1'⟩ → ⟨c1'#V',m1'⟩"
by force
from R0def' USdB_comp_head_tail have conclpart:
"((c1#V,c1'#V') ∈ R0 ∨ (c1#V) ≈⇘d⇙ (c1'#V'))"
by auto
with irange rew inR0 F1step dequal R0def' F2step
show "∃c1V' m2'. ⟨F2!i,m1'⟩ → ⟨c1V',m2'⟩ ∧
((c1V,c1V') ∈ R0 ∨ c1V ≈⇘d⇙ c1V') ∧ m2 =⇘d⇙ m2'"
by fastforce
qed
hence "R0 ⊆ ≈⇘d⇙"
by (rule Up_To_Technique)
with inR0 show ?thesis
by auto
qed
theorem Compositionality_If:
assumes dind_or_branchesrelated:
"b ≡⇘d⇙ b' ∨ [c1] ≈⇘d⇙ [c2] ∨ [c1'] ≈⇘d⇙ [c2']"
assumes branch1related: "[c1] ≈⇘d⇙ [c1']"
assumes branch2related: "[c2] ≈⇘d⇙ [c2']"
shows "[if b then c1 else c2 fi] ≈⇘d⇙ [if b' then c1' else c2' fi]"
proof -
define R1 where "R1 = {(I1,I2). ∃c1 c1' c2 c2' b b'.
I1 = [if b then c1 else c2 fi] ∧ I2 = [if b' then c1' else c2' fi] ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧ b ≡⇘d⇙ b'}"
define R2 where "R2 = {(I1,I2). ∃c1 c1' c2 c2' b b'.
I1 = [if b then c1 else c2 fi] ∧ I2 = [if b' then c1' else c2' fi] ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧
([c1] ≈⇘d⇙ [c2] ∨ [c1'] ≈⇘d⇙ [c2'])}"
define R0 where "R0 = R1 ∪ R2"
from dind_or_branchesrelated branch1related branch2related
have inR0: "([if b then c1 else c2 fi],[if b' then c1' else c2' fi]) ∈ R0"
by (simp add: R0_def R1_def R2_def)
have uptoR0: "d_Bisimulation_Up_To_USdB d R0"
proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
from USdBsym d_indistinguishable_sym
have symR1: "sym R1"
by (simp add: sym_def R1_def, fastforce)
from USdBsym
have symR2: "sym R2"
by (simp add: sym_def R2_def, fastforce)
from symR1 symR2 show "sym R0"
by (simp add: sym_def R0_def)
next
fix I1 I2
assume inR0: "(I1,I2) ∈ R0"
thus "length I1 = length I2"
by (simp add: R0_def R1_def R2_def, auto)
next
fix I1 I2 RS m1 m1' m2 i
assume inR0: "(I1,I2) ∈ R0"
assume irange: "i < length I1"
assume I1step: "⟨I1!i,m1⟩ → ⟨RS,m2⟩"
assume dequal: "m1 =⇘d⇙ m1'"
have inR1case: "(I1,I2) ∈ R1
⟹ ∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
proof -
assume inR1: "(I1,I2) ∈ R1"
then obtain c1 c1' c2 c2' b b' where R1def':
"I1 = [if b then c1 else c2 fi]
∧ I2 = [if b' then c1' else c2' fi] ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧ b ≡⇘d⇙ b'"
by (simp add: R1_def, force)
moreover
from irange R1def' I1step have case_distinction:
"RS = [c1] ∧ BMap (E b m1) = True ∨
RS = [c2] ∧ BMap (E b m1) = False"
by (simp, metis MWLf_semantics.MWLfSteps_det_cases(4))
moreover
{
assume bevalT: "BMap (E b m1) = True"
assume RSassump: "RS = [c1]"
from irange bevalT I1step R1def' RSassump have memeq:
"m2 = m1"
by (simp, metis MWLf_semantics.MWLfSteps_det_cases(4))
from bevalT R1def' dequal have b'evalT:
"BMap (E b' m1') = True"
by (simp add: d_indistinguishable_def)
hence I2step_case1:
"⟨if b' then c1' else c2' fi,m1'⟩ → ⟨[c1'],m1'⟩"
by (simp add: MWLfSteps_det.iftrue)
with irange dequal RSassump memeq R1def'
have case1_concl:
"∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by auto
}
moreover
{
assume bevalF: "BMap (E b m1) = False"
assume RSassump: "RS = [c2]"
from irange bevalF I1step R1def' RSassump have memeq:
"m1 = m2"
by (simp, metis MWLf_semantics.MWLfSteps_det_cases(4))
from bevalF R1def' dequal have b'evalF:
"BMap (E b' m1') = False"
by (simp add: d_indistinguishable_def)
hence I2step_case1:
"⟨if b' then c1' else c2' fi,m1'⟩ → ⟨[c2'],m1'⟩"
by (simp add: MWLfSteps_det.iffalse)
with irange dequal RSassump memeq R1def'
have case1_concl:
"∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by auto
}
ultimately show
"∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by auto
qed
have inR2case: "(I1,I2) ∈ R2
⟹ ∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
proof -
assume inR2: "(I1,I2) ∈ R2"
then obtain c1 c1' c2 c2' b b' where R2def':
"I1 = [if b then c1 else c2 fi]
∧ I2 = [if b' then c1' else c2' fi] ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧
([c1] ≈⇘d ⇙[c2] ∨ [c1'] ≈⇘d⇙ [c2'])"
by (simp add: R2_def, force)
moreover
from irange R2def' I1step have case_distinction_left:
"(RS = [c1] ∨ RS = [c2]) ∧ m2 = m1"
by (simp, metis MWLf_semantics.MWLfSteps_det_cases(4))
moreover
from irange R2def' dequal obtain RS' where I2step:
"⟨I2!i,m1'⟩ → ⟨RS',m1'⟩
∧ (RS' = [c1'] ∨ RS' = [c2']) ∧ m1 =⇘d⇙ m1'"
by (simp, metis MWLfSteps_det.iffalse MWLfSteps_det.iftrue)
moreover
from USdBtrans have "⟦ [c1] ≈⇘d⇙ [c2]; [c2] ≈⇘d⇙ [c2'] ⟧
⟹ [c1] ≈⇘d⇙ [c2']"
by (unfold trans_def, blast)
moreover
from USdBtrans have "⟦ [c1] ≈⇘d⇙ [c1']; [c1'] ≈⇘d⇙ [c2'] ⟧
⟹ [c1] ≈⇘d⇙ [c2']"
by (unfold trans_def, blast)
moreover
from USdBsym have "[c1] ≈⇘d⇙ [c2] ⟹ [c2] ≈⇘d⇙ [c1]"
by (simp add: sym_def)
moreover
from USdBtrans have "⟦ [c2] ≈⇘d⇙ [c1]; [c1] ≈⇘d⇙ [c1'] ⟧
⟹ [c2] ≈⇘d⇙ [c1']"
by (unfold trans_def, blast)
moreover
from USdBsym have "[c1'] ≈⇘d⇙ [c2'] ⟹ [c2'] ≈⇘d⇙ [c1']"
by (simp add: sym_def)
moreover
from USdBtrans have "⟦ [c2] ≈⇘d⇙ [c2']; [c2'] ≈⇘d⇙ [c1'] ⟧
⟹ [c2] ≈⇘d⇙ [c1']"
by (unfold trans_def, blast)
ultimately show
"∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by auto
qed
from inR0 inR1case inR2case show
"∃RS' m2'. ⟨I2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
by (auto simp add: R0_def)
qed
hence "R0 ⊆ ≈⇘d⇙"
by (rule Up_To_Technique)
with inR0 show ?thesis
by auto
qed
theorem Compositionality_While:
assumes dind: "b ≡⇘d⇙ b'"
assumes bodyrelated: "[c] ≈⇘d⇙ [c']"
shows "[while b do c od] ≈⇘d⇙ [while b' do c' od]"
proof -
define R1 where "R1 = {(S1,S2). ∃c1 c1' c2 c2' b b' W W'.
S1 = (c1;(while b do c2 od))#W ∧
S2 = (c1';(while b' do c2' od))#W' ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧ W ≈⇘d⇙ W' ∧ b ≡⇘d⇙ b'}"
define R2 where "R2 = {(W1,W2). ∃c1 c1' b b'.
W1 = [while b do c1 od] ∧ W2 = [while b' do c1' od] ∧
[c1] ≈⇘d⇙ [c1'] ∧ b ≡⇘d⇙ b'}"
define R0 where "R0 = R1 ∪ R2"
from dind bodyrelated
have inR0: "([while b do c od],[while b' do c' od]) ∈ R0"
by (simp add: R0_def R1_def R2_def)
have uptoR0: "d_Bisimulation_Up_To_USdB d R0"
proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
from USdBsym d_indistinguishable_sym have symR1: "sym R1"
by (simp add: sym_def R1_def, fastforce)
from USdBsym d_indistinguishable_sym have symR2: "sym R2"
by (simp add: sym_def R2_def, fastforce)
from symR1 symR2 show "sym R0"
by (simp add: sym_def R0_def)
next
fix W1 W2
assume inR0: "(W1,W2) ∈ R0"
with USdBeqlen show "length W1 = length W2"
by (simp add: R0_def R1_def R2_def, force)
next
fix W1 W2 i m1 m1' RS m2
assume inR0: "(W1,W2) ∈ R0"
assume irange: "i < length W1"
assume W1step: "⟨W1!i,m1⟩ → ⟨RS,m2⟩"
assume dequal: "m1 =⇘d⇙ m1'"
from inR0 show "∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R0 ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
proof (simp add: R0_def, auto)
assume inR1: "(W1,W2) ∈ R1"
then obtain c1 c1' c2 c2' b b' V V'
where R1def': "W1 = (c1;(while b do c2 od))#V
∧ W2 = (c1';(while b' do c2' od))#V' ∧
[c1] ≈⇘d⇙ [c1'] ∧ [c2] ≈⇘d⇙ [c2'] ∧ V ≈⇘d⇙ V' ∧ b ≡⇘d⇙ b'"
by (simp add: R1_def, force)
with irange have case_distinction1: "i = 0 ∨
(V ≠ [] ∧ i ≠ 0)"
by auto
moreover
have case1: "i = 0 ⟹
∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
proof -
assume i0: "i = 0"
with R1def' W1step obtain c3 W where case_distinction:
"RS = [while b do c2 od] ∧ ⟨c1,m1⟩ → ⟨[],m2⟩
∨ RS = (c3;(while b do c2 od))#W ∧ ⟨c1,m1⟩ → ⟨c3#W,m2⟩"
by (simp, metis MWLfSteps_det_cases(3))
moreover
{
assume RSassump: "RS = [while b do c2 od]"
assume StepAssump: "⟨c1,m1⟩ → ⟨[],m2⟩"
from USdBeqlen[of "[]"] StepAssump R1def'
USdB_Strong_d_Bisimulation dequal
strongdB_aux[of "d" "≈⇘d⇙" "i"
"[c1]" "[c1']" "m1" "[]" "m2" "m1'"] i0
obtain W' m2' where c1c1'reason:
"⟨c1',m1'⟩ → ⟨W',m2'⟩ ∧ W' = []
∧ [] ≈⇘d⇙ W' ∧ m2 =⇘d⇙ m2'"
by fastforce
with c1c1'reason have conclpart1:
"⟨c1';(while b' do c2' od),m1'⟩
→ ⟨[while b' do c2' od],m2'⟩ ∧ m2 =⇘d⇙ m2'"
by (simp add: MWLfSteps_det.seq1)
from R1def' have conclpart2:
"([while b do c2 od],[while b' do c2' od]) ∈ R2"
by (simp add: R2_def)
with conclpart1 RSassump i0 R1def'
have case1_concl:
"∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by auto
}
moreover
{
assume RSassump: "RS = (c3;(while b do c2 od))#W"
assume StepAssump: "⟨c1,m1⟩ → ⟨c3#W,m2⟩"
from StepAssump R1def' USdB_Strong_d_Bisimulation dequal
strongdB_aux[of "d" "≈⇘d⇙" "i"
"[c1]" "[c1']" "m1" "c3#W" "m2" "m1'"] i0
obtain V'' m2' where c1c1'reason:
"⟨c1',m1'⟩ → ⟨V'',m2'⟩
∧ (c3#W) ≈⇘d⇙ V'' ∧ m2 =⇘d⇙ m2'"
by fastforce
with USdBeqlen[of "c3#W" "V''"] obtain c3' W'
where V''reason: "V'' = c3'#W'"
by (cases V'', force, force)
with c1c1'reason have conclpart1:
"⟨c1';(while b' do c2' od),m1'⟩ →
⟨(c3';(while b' do c2' od))#W',m2'⟩
∧ m2 =⇘d⇙ m2'"
by (simp add: MWLfSteps_det.seq2)
from V''reason
c1c1'reason USdB_decomp_head_tail[of "c3" "W"]
USdB_Strong_d_Bisimulation
have c3aWinUSDB:
"[c3] ≈⇘d⇙ [c3'] ∧ W ≈⇘d⇙ W'"
by blast
with R1def' have conclpart2:
"((c3;(while b do c2 od))#W,
(c3';(while b' do c2' od))#W') ∈ R1"
by (simp add: R1_def)
with i0 RSassump R1def' V''reason conclpart1
have case2_concl:
"∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by auto
}
ultimately
show "∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by blast
qed
moreover
have case2: "⟦ V ≠ []; i ≠ 0 ⟧
⟹ ∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
proof -
assume Vnonempt: "V ≠ []"
assume inot0: "i ≠ 0"
with Vnonempt irange R1def' have i1range:
"(i-Suc 0) < length V"
by simp
from inot0 R1def' have W1ieq: "W1!i = V!(i-Suc 0)"
by auto
from inot0 R1def' have "W2!i = V'!(i-Suc 0)"
by auto
with W1ieq R1def' W1step i1range dequal
USdB_Strong_d_Bisimulation
strongdB_aux[of "d" "USdB d"
"i-Suc 0" "V" "V'" "m1" "RS" "m2" "m1'"]
show "∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by force
qed
ultimately show "∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by auto
next
assume inR2: "(W1,W2) ∈ R2"
then obtain c1 c1' b b' where R2def':
"W1 = [while b do c1 od] ∧ W2 = [while b' do c1' od] ∧
[c1] ≈⇘d⇙ [c1'] ∧ b ≡⇘d⇙ b'"
by (auto simp add: R2_def)
moreover
from irange R2def' W1step have case_distinction:
"RS = [c1;(while b do c1 od)] ∧ BMap (E b m1) = True ∨
RS = [] ∧ BMap (E b m1) = False"
by (simp,metis MWLf_semantics.MWLfSteps_det_cases(5))
moreover
{
assume bevalT: "BMap (E b m1)"
assume RSassump: "RS = [c1;(while b do c1 od)]"
from irange bevalT W1step R2def' RSassump have memeq:
"m2 = m1"
by (simp,metis MWLf_semantics.MWLfSteps_det_cases(5))
from bevalT R2def' dequal have b'evalT: "BMap (E b' m1')"
by (simp add: d_indistinguishable_def)
hence W2step_case1:
"⟨while b' do c1' od,m1'⟩
→ ⟨[c1';(while b' do c1' od)],m1'⟩"
by (simp add: MWLfSteps_det.whiletrue)
from trivialpair_in_USdB R2def' have inWR2:
"([c1;(while b do c1 od)],
[c1';(while b' do c1' od)]) ∈ R1"
by (auto simp add: R1_def)
with irange dequal RSassump memeq W2step_case1 R2def'
have case1_concl:
"∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by auto
}
moreover
{
assume bevalF: "BMap (E b m1) = False"
assume RSassump: "RS = []"
from irange bevalF W1step R2def' RSassump have memeq:
"m2 = m1"
by (simp,metis MWLf_semantics.MWLfSteps_det_cases(5))
from bevalF R2def' dequal have b'equalF:
"BMap (E b' m1') = False"
by (simp add: d_indistinguishable_def)
hence W2step_case2:
"⟨while b' do c1' od,m1'⟩ → ⟨[],m1'⟩"
by (simp add: MWLfSteps_det.whilefalse)
with trivialpair_in_USdB irange dequal RSassump
memeq R2def'
have case1_concl:
"∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by force
}
ultimately
show "∃RS' m2'. ⟨W2!i,m1'⟩ → ⟨RS',m2'⟩ ∧
((RS,RS') ∈ R1 ∨ (RS,RS') ∈ R2 ∨ RS ≈⇘d⇙ RS')
∧ m2 =⇘d⇙ m2'"
by auto
qed
qed
hence "R0 ⊆ ≈⇘d⇙"
by (rule Up_To_Technique)
with inR0 show ?thesis
by auto
qed
end
end