text ‹If we have a standard cooperation problem with left-part R (flat → flat), middle part CT
(flat → sharp) and right part P (sharp → sharp), then we can split the problem into several
ones (R, CTi, P). It only has to be guaranteed that each transition flat → sharp of CT must
be covered by some CTi, whenever the sharp-location occurs in P.›
theory Cut_Transition_Split
imports Cooperation_Program
begin
text ‹First, the abstract setting.›
context indexed_rewriting
begin
lemma cut_transition_split: assumes S: "⋀ b1 b2. (b1,b2) ∈ Induce P ⟹ f b1 ∈ S'"
and S_CT: "⋀ ct b1 b2. ct ∈ R ⟹ (b1,b2) ∈ induce ct ⟹ f b2 ∈ S' ⟹ ct ∈ CT"
and S_R: "⋀ b1 b2. (b1,b2) ∈ Induce R ⟹ f b1 ∉ S"
and RR: "⋀ aR b1 b2. aR ∈ R ⟹ (b1,b2) ∈ induce aR ⟹ f b2 ∉ S ⟹ aR ∈ RR"
and I: "f ` I ∩ S = {}"
and S': "S' ⊆ S"
and SN: "⋀ ct. ct ∈ CT ⟹ ∃ RRR. insert ct RR ⊆ RRR ∧ cooperation_SN_on RRR P I"
shows "cooperation_SN_on R P I"
proof
fix seq
assume I0: "seq 0 ∈ I" and chain: "cooperation_chain R P seq"
from cooperation_chainE[OF chain] obtain cp P' where P': "P' ⊆ P"
and rec: "recurring P' (shift seq cp)"
and R: "⋀ i. i < cp ⟹ (seq i, seq (Suc i)) ∈ Induce R" by metis
from recurring_imp_chain[OF rec, rule_format, of 0] P'
have "(seq cp, seq (Suc cp)) ∈ Induce P" by auto
from S[OF this] have fS: "f (seq cp) ∈ S'" .
from I0 I this S' have cp0: "cp ≠ 0" by auto
with R[of "cp - 1"] obtain ct where
"ct ∈ R" and cut_step: "(seq (cp - 1), seq cp) ∈ induce ct" by auto
from S_CT[OF this fS] have ct: "ct ∈ CT" .
from SN[OF this] obtain RRR where RRR: "insert ct RR ⊆ RRR" and SN: "cooperation_SN_on RRR P I" by auto
have "cooperation_chain RRR P seq"
proof (intro cooperation_chainI[OF P' rec])
fix i
assume i: "i < cp"
then show "(seq i, seq (Suc i)) ∈ Induce RRR"
proof (cases "i = cp - 1")
case True
with RRR cut_step cp0 show ?thesis by auto
next
case False
with i have "Suc i < cp" by auto
from S_R[OF R[OF this]] have fS: "f (seq (Suc i)) ∉ S" by auto
from R[OF i] obtain r where "r ∈ R" "(seq i, seq (Suc i)) ∈ induce r" by auto
from RR[OF this fS] RRR this(2) show ?thesis by auto
qed
qed
from cooperation_SN_onE[OF SN I0 this] show False .
qed
end
text ‹Next, the application to cooperation programs.›
context lts
begin
lemma cut_transition_split_cooperation_SN: assumes S: "source ` (sharp_transitions_of P) = S"
and S_CT: "⋀ ct. ct ∈ flat_transitions_of P ⟹ target ct ∈ S ⟹ ct ∈ CT"
and RR: "⋀ r. r ∈ flat_transitions_of P ⟹ ¬ is_sharp (target r) ⟹ r ∈ RR"
and I: "⋀ l. l ∈ lts.initial P ⟹ ¬ is_sharp l"
and SN: "⋀ ct. ct ∈ CT ⟹
∃ RRR. insert ct RR ⊆ RRR ∧ indexed_rewriting.cooperation_SN_on (transition_step_lts P) RRR (sharp_transitions_of P) (initial_states P)"
shows "cooperation_SN P"
proof -
let ?R = "transition_step_lts P"
interpret indexed_rewriting ?R .
show ?thesis
proof (rule indexed_rewriting.cut_transition_split[of _ _ location S _ CT "range Sharp" RR, OF _ _ _ _ _ _ SN], goal_cases)
case (1 b1 b2)
then obtain r where "(b1,b2) ∈ ?R r" and r: "r ∈ sharp_transitions_of P" by auto
then have id: "location b1 = source r" by (cases b1, cases b2, cases r, auto)
have "location b1 ∈ source ` sharp_transitions_of P" unfolding id using r by auto
with S show "location b1 ∈ S" by auto
next
case (2 ct b1 b2)
from 2(1-2) have "target ct = location b2" by (cases b1, cases b2, cases ct, auto)
from S_CT[OF 2(1) 2(3)[folded this]] show "ct ∈ CT" .
next
case (3 b1 b2)
then obtain r where "(b1,b2) ∈ ?R r" and r: "r ∈ flat_transitions_of P" by auto
then have id: "location b1 = source r" by (cases b1, cases b2, cases r, auto)
show ?case unfolding id using r by auto
next
case (4 r b1 b2)
then have id: "location b2 = target r" by (cases b1, cases b2, cases r, auto)
from RR[OF 4(1)] 4(3) show ?case unfolding id by (cases "target r", auto)
next
case 5
show ?case using I unfolding initial_states_def by force
next
case 6
show "S ⊆ range Sharp" unfolding S[symmetric] by (metis (no_types, lifting) image_Collect_subsetI is_sharp.elims(2) range_eqI)
qed
qed
lemma cut_transition_split_main: assumes
flat_sharp: "⋀ ct. ct ∈ flat_transitions_of P ⟹ is_sharp (target ct) ⟹ ∃ i ≤ (n :: nat). ct ∈ Q i"
and Q0: "⋀ ct ct'. ct ∈ Q 0 ⟹ ct' ∈ sharp_transitions_of P ⟹ target ct ≠ source ct'"
and R: "⋀ r. r ∈ flat_transitions_of P ⟹ ¬ is_sharp (target r) ⟹ r ∈ R"
and I: "⋀ l. l ∈ lts.initial P ⟹ ¬ is_sharp l"
and SN: "⋀ i. 1 ≤ i ⟹ i ≤ n ⟹
indexed_rewriting.cooperation_SN_on (transition_step_lts P) (Q i ∪ R) (sharp_transitions_of P) (initial_states P)"
shows "cooperation_SN P"
proof -
let ?CT = "⋃ (Q ` {1 .. n})"
show ?thesis
proof (rule cut_transition_split_cooperation_SN[OF refl _ R I, where CT = ?CT])
fix ct
assume ct: "ct ∈ flat_transitions_of P" "target ct ∈ source ` sharp_transitions_of P"
then have "is_sharp (target ct)" by auto
from flat_sharp[OF ct(1) this] obtain i where i: "i ≤ n" "ct ∈ Q i" by auto
{
from ct obtain ct' where ct': "ct' ∈ sharp_transitions_of P" "target ct = source ct'" by auto
assume "i = 0"
with i have "ct ∈ Q 0" by auto
from Q0[OF this ct'(1)] ct'(2) have False by auto
}
then have i1: "1 ≤ i" by (cases i, auto)
then show "ct ∈ ⋃ (Q ` {1..n})" using i by auto
next
fix ct
assume "ct ∈ ?CT"
then obtain i where "1 ≤ i" "i ≤ n" and ct: "ct ∈ Q i" by auto
from SN[OF this(1-2)]
have "indexed_rewriting.cooperation_SN_on (transition_step_lts P) (Q i ∪ R) (sharp_transitions_of P) (initial_states P)" .
with ct show "∃RRR. insert ct R ⊆ RRR ∧
indexed_rewriting.cooperation_SN_on (transition_step_lts P) RRR (sharp_transitions_of P) (initial_states P)"
by (intro exI[of _ "Q i ∪ R"], auto)
qed
qed
end
text ‹Next, an executable checker.›
type_synonym 'l cut_transition_split_repr = "'l list"
datatype 'l cut_transition_split_info = Cut_Transition_Split_Info "'l cut_transition_split_repr list"
fun cut_transition_split where
"cut_transition_split (Cut_Transition_Split_Info ct_ids) CP = do {
let (P,R) = partition (is_sharp_transition o snd) (transitions_impl CP);
let (CT,RR) = partition (is_sharp o target o snd) R;
let Slist = map (source o snd) P;
let S = set Slist;
let CT_ids = set (concat ct_ids);
check_allm (λ l. check (¬ is_sharp l)
(showsl_lit (STR ''initial state '') o showsl l o showsl_lit (STR '' must not be sharped''))) (initial CP);
check_allm (λ (t_id, ct). check (target ct ∈ S ⟶ t_id ∈ CT_ids)
(showsl_lit (STR ''did not find cut-transition '') o showsl t_id o
showsl_lit (STR '' in partition⏎relevant cut-points are: '') o showsl_list Slist)) CT;
let RRP = RR @ P;
return (map (λ ct_ids'.
Lts_Impl (initial CP) ((filter (λ ct. fst ct ∈ set ct_ids') CT) @ RRP) (assertion_impl CP)) ct_ids)
} <+? (λ s. showsl_lit (STR ''error in splitting cut transitions on LTS⏎'') o s)"
context lts
begin
lemma cut_transition_split: assumes SN: "⋀ CP'. CP' ∈ set CPs ⟹ cooperation_SN_impl CP'"
and res: "cut_transition_split info CP = return CPs"
shows "cooperation_SN_impl CP"
proof (cases info)
case (Cut_Transition_Split_Info ct_ids) note * = this
let ?CP = "lts_of CP"
obtain R P where p1: "partition (is_sharp_transition ∘ snd) (transitions_impl CP) = (P,R)" by auto
from arg_cong[OF p1, of fst, unfolded partition_filter1]
have P: "P = filter (is_sharp_transition o snd) (transitions_impl CP)" by auto
from arg_cong[OF p1, of snd, unfolded partition_filter2]
have R: "R = filter (Not o is_sharp_transition o snd) (transitions_impl CP)" by (auto simp: o_def)
then have RR: "snd ` set R = flat_transitions_of ?CP" by auto
have PP: "snd ` set P = sharp_transitions_of ?CP" unfolding P by auto
then have S: "source ` sharp_transitions_of ?CP = source ` snd ` set P" by auto
obtain RR CT where p2: "partition (is_sharp ∘ target ∘ snd) R = (CT,RR)" by auto
note CT_RR = partition_filter_conv[of "(is_sharp ∘ target ∘ snd)" R, unfolded p2]
then have CT: "CT = filter (is_sharp ∘ target ∘ snd) R" and RRR: "RR = filter (Not o is_sharp ∘ target o snd) R"
by (auto simp: o_def)
note res = res[unfolded * cut_transition_split.simps Let_def p1 p2 split, simplified]
from res have init: "⋀ l. l ∈ lts.initial (lts_of CP) ⟹ ¬ is_sharp l" by auto
let ?n = "length ct_ids"
let ?Q = "λ j. if j = 0 then { t. ∃ i. (i,t) ∈ set CT ∧ i ∉ set (concat ct_ids)}
else { t. ∃ i. (i,t) ∈ set CT ∧ i ∈ set (ct_ids ! (j - 1))}"
define Q where "Q = ?Q"
show ?thesis
proof (intro cooperation_SN_implI cut_transition_split_main[OF _ _ _ init, of _ ?n Q "snd ` set RR"]; (unfold RR[symmetric])?)
fix r
assume "r ∈ snd ` set R" "¬ is_sharp (target r)"
then show "r ∈ snd ` set RR" using CT_RR by auto
next
fix ct
assume *: "ct ∈ snd ` set R" "is_sharp (target ct)"
then have ct: "ct ∈ snd ` set CT" unfolding CT unfolding P R by auto
then obtain t_id where tid: "(t_id,ct) ∈ set CT" by auto
show "∃i≤?n. ct ∈ Q i"
proof (cases "t_id ∈ set (concat ct_ids)")
case False
with tid show ?thesis by (intro exI[of _ 0], auto simp: Q_def)
next
case True
then obtain cts where "t_id ∈ set cts" and "cts ∈ set ct_ids" by auto
from this(2)[unfolded set_conv_nth] this(1) obtain j where "j < ?n" "t_id ∈ set (ct_ids ! j)" by auto
with tid show ?thesis by (intro exI[of _ "Suc j"], auto simp: Q_def)
qed
next
fix j :: nat
let ?j = "j - 1"
let ?cts = "ct_ids ! ?j"
assume j: "1 ≤ j" "j ≤ ?n" and CP: "lts_impl CP"
then have "?j < ?n" by auto
then have ct_ids: "ct_ids ! ?j ∈ set ct_ids" unfolding set_conv_nth by auto
let ?NR = "Lts_Impl (lts_impl.initial CP) ([ct←CT . fst ct ∈ set ?cts] @ RR @ P) (assertion_impl CP)"
let ?N = "lts_of ?NR"
from res ct_ids
have NR: "?NR ∈ set CPs" by auto
have sub: "sub_lts_impl ?NR CP" unfolding RRR P R CT by (cases CP, auto simp: mset_filter subseteq_mset_def)
from sub_lts_impl[OF sub CP] have lts: "lts_impl ?NR".
from SN[OF NR, unfolded cooperation_SN_impl_def, rule_format, OF lts]
have SN: "cooperation_SN ?N" .
also have "transition_step_lts ?N = transition_step_lts ?CP"
by (cases CP, auto simp: assertion_of_def)
also have "initial_states ?N = initial_states ?CP"
by (cases CP, auto simp: assertion_of_def initial_states_def)
also have "sharp_transitions_of ?N = sharp_transitions_of ?CP"
unfolding PP[symmetric] by (cases CP, auto simp: P RRR R CT)
also have "flat_transitions_of ?N = Q j ∪ snd ` set RR"
unfolding CT RRR R P Q_def using j by (cases CP, auto)
finally
show "indexed_rewriting.cooperation_SN_on (transition_step_lts (lts_of CP)) (Q j ∪ snd ` set RR)
(sharp_transitions_of (lts_of CP)) (initial_states (lts_of CP))" .
next
fix ct ct'
assume ct: "ct ∈ Q 0" "ct' ∈ sharp_transitions_of (lts_of CP)"
from this[unfolded Q_def] obtain t_id where "(t_id,ct) ∈ set CT" "t_id ∉ set (concat ct_ids)" by auto
with res have "target ct ∉ (source ∘ snd) ` set P" by auto
with ct(2) show "target ct ≠ source ct'" unfolding P by (auto simp: o_def)
qed
qed
end
lemma length_cut_transition_split: assumes "cut_transition_split (Cut_Transition_Split_Info infos) cp = return xs"
shows "length infos = length xs"
using assms by auto
declare cut_transition_split.simps[simp del]
end