theory Initial_Cooperation_Program
imports
Cooperation_Program
Auxx.Cut_Points
begin
context lts
begin
definition exists_cut :: "('f,'v,'t,'l) cooperation_problem ⇒ 'l ⇒ bool" where
"exists_cut P l ≡
(∃ τ ∈ transition_rules P. source τ = Flat l ∧ target τ = Sharp l ∧ skip_transition τ)"
lemma cut_transition:
assumes cut: "exists_cut P l"
and α: "assignment α" "α ⊨ assertion P (Flat l)"
and lc: "assertion P (Flat l) = assertion P (Sharp l)"
shows "(State α (Flat l), State α (Sharp l)) ∈ transition P"
proof -
from assms[unfolded exists_cut_def] obtain τ where *: "τ ∈ transition_rules P"
"source τ = Flat l" "target τ = sharp.Sharp l" "skip_transition τ" by auto
from skip_transition[OF *(1) *(4), of α] α lc
show ?thesis unfolding *(2-3) by auto
qed
definition "copy_prog P R l ≡
lts.initial P = Flat ` (lts.initial R) ∧
exists_cut P l ∧
(∀ τ ∈ transition_rules R. flat_transition τ ∈ transition_rules P ∧ sharp_transition τ ∈ transition_rules P) ∧
(assertion P = assertion R ∘ natural)"
definition "copy_progs Ps R CP ≡
cut_points (call_graph_of_lts R) CP ∧
(∀ l ∈ CP. ∃ P ∈ Ps. copy_prog P R l)"
context fixes P :: "('f,'v,'t,'l sharp)lts" and R :: "('f,'v,'t,'l) lts" and l :: "'l" assumes copy: "copy_prog P R l" begin
private lemmas * = copy[unfolded copy_prog_def]
lemma copy_progD1: "lts.initial P = Flat ` (lts.initial R)" by (insert *, auto)
lemma copy_progD2: "exists_cut P l" by (insert *, auto)
lemma copy_progD3:
assumes "τ ∈ transition_rules R"
shows "flat_transition τ ∈ transition_rules P" and "sharp_transition τ ∈ transition_rules P"
by (insert assms *, auto)
lemma copy_progD4: "assertion P = assertion R ∘ natural" by (insert *, auto)
end
lemmas copy_progD[dest] = copy_progD1 copy_progD2 copy_progD3 copy_progD4
lemma copy_progI[intro]:
assumes "lts.initial P = Flat ` (lts.initial R)"
and "exists_cut P l"
and "⋀τ. τ ∈ transition_rules R ⟹ flat_transition τ ∈ transition_rules P"
and "⋀τ. τ ∈ transition_rules R ⟹ sharp_transition τ ∈ transition_rules P"
and "assertion P = assertion R ∘ natural"
shows "copy_prog P R l" unfolding copy_prog_def using assms by auto
lemma initial_states_copy_prog[simp]: assumes "copy_prog P R l"
shows "initial_states P = flat_state ` initial_states R"
proof -
from assms
have "initial_states P ⊇ flat_state ` initial_states R"
by (auto simp: initial_states_def image_def copy_progD1 copy_progD4)
moreover
{
fix s
assume "s ∈ initial_states P"
from this[unfolded initial_states_def copy_progD1[OF assms]] obtain l where
loc: "location s = Flat l" and l: "l ∈ lts.initial R"
and s: "state_lts P s" by auto
then have "s ∈ flat_state ` initial_states R" unfolding initial_states_def image_def
unfolding copy_progD4[OF assms]
by (cases s, auto intro: exI[of _ "State _ _"])
}
ultimately show ?thesis by auto
qed
definition cut_chain where "cut_chain (cutpoint::nat) seq i ≡
if i ≤ cutpoint then flat_state (seq i)
else sharp_state (seq (i-1))"
lemma cut_chain_simps[simp]:
"i ≤ cp ⟹ cut_chain cp seq i = flat_state (seq i)"
"¬ (i ≤ cp) ⟹ cut_chain cp seq i = sharp_state (seq (i-1))"
unfolding cut_chain_def by auto
lemma shift_cut_chain:
"n > cp ⟹ shift (cut_chain cp seq) n = sharp_state ∘ shift seq (n-1)"
by(auto simp: cut_chain_def)
lemma sharp_chain:
assumes chain: "chain (transitions_step lc τs) seq"
shows "chain (transitions_step (lift_state_conditions lc) (sharp_transition ` τs)) (sharp_state ∘ seq)"
proof
let ?seq = "sharp_state ∘ seq"
let ?lc = "lift_state_conditions lc"
fix i
from chain obtain τ
where τ: "τ ∈ τs" and step: "(seq i, seq (Suc i)) ∈ transition_step lc τ" by force
from step have "(?seq i, ?seq (Suc i)) ∈ transition_step ?lc (sharp_transition τ)"
by (auto intro!: sharp_transition)
with τ show "(?seq i, ?seq (Suc i)) ∈ transitions_step ?lc (sharp_transition ` τs)" by auto
qed
lemma initial_cooperation_program:
assumes fin: "finite (transition_rules R)"
and copy: "copy_progs Ps R CP"
and lts: "lts R"
and SN: "⋀ P. P ∈ Ps ⟹ cooperation_SN P"
shows "lts_termination R"
proof (rule ccontr)
let ?transition_step = "transition_step_lts R"
let ?lifted_step = "transition_step (lift_state_conditions (state_lts R))"
interpret indexed_rewriting ?transition_step .
assume "¬ lts_termination R"
then obtain seq
where init: "seq 0 ∈ initial_states R" and chain: "chain (transition R) seq" by auto
from chain_imp_recurring[OF fin chain[unfolded transition_def]]
obtain m τs where τs: "τs ⊆ transition_rules R" and rec: "recurring τs (shift seq m)" by auto
interpret sharp_morphism: rule_morphism sharp_state τs sharp_transition ?transition_step ?lifted_step
by (standard, auto simp: sharp_transition)
interpret flat_morphism: rule_morphism flat_state τs flat_transition ?transition_step ?lifted_step
by (standard, auto simp: flat_transition)
{
fix i
assume "i ≥ m"
then have "i = m + (i - m)" by auto
with recurring_imp_chain[OF rec, rule_format, of "i - m"] have
"(seq i, seq (Suc i)) ∈ ⋃ (?transition_step ` τs)" by auto
} note steps = this
define L where "L = { location (seq k) | k. k ≥ m}"
{
fix l1 l2
assume l1: "l1 ∈ L" and l2: "l2 ∈ L"
from l1[unfolded L_def] obtain k1 where kl1: "location (seq k1) = l1" and k1: "k1 ≥ m" by auto
from l2[unfolded L_def] obtain k2 where kl2: "location (seq k2) = l2" and k2: "k2 ≥ m" by auto
from steps[OF k2] obtain τ where step: "(seq k2, seq (Suc k2)) ∈ ?transition_step τ"
and tau: "τ ∈ τs" by auto
with kl2 have tau_l2: "source τ = l2" by (cases τ, auto)
from recurring_imp_INFM[OF rec tau, unfolded INFM_nat_le, rule_format, of "Suc k1"]
obtain n where *: "n ≥ Suc k1" "(seq (n + m), seq (Suc (n + m))) ∈ ?transition_step τ" by auto
define k2 where "k2 = n + m"
from * have k2: "k2 > k1" and step: "(seq k2, seq (Suc k2)) ∈ ?transition_step τ"
unfolding k2_def by auto
then have kl2: "location (seq k2) = l2" using tau_l2 by auto
define diff where "diff = k2 - k1"
from k2 have k2: "k2 = k1 + diff" "diff > 0" unfolding diff_def by auto
let ?CG = "call_graph_of_lts R ↾ L"
have "(location (seq k1), location (seq (k1 + diff))) ∈ ?CG^^diff"
proof (induct diff)
case (Suc diff)
let ?a = "seq (k1 + diff)" let ?b = "seq (Suc (k1 + diff))"
have "(location ?a, location ?b) ∈ ?CG"
proof -
from k1 have m: "k1 + diff ≥ m" by auto
from steps[OF m] obtain τ where *: "τ ∈ τs" "(?a, ?b) ∈ ?transition_step τ" by auto
from *(1) τs have tau: "τ ∈ transition_rules R" by auto
have "(location ?a, location ?b) ∈ call_graph_of_lts R"
unfolding call_graph_of_lts_def
by (standard, intro exI, rule conjI[OF _ tau], insert *(2), cases τ, auto)
moreover have "location ?a ∈ L" "location ?b ∈ L" using m unfolding L_def by auto
ultimately show ?thesis by auto
qed
with Suc show ?case by auto
qed auto
then have "(location (seq k1), location (seq k2)) ∈ ?CG^+" unfolding k2(1)[symmetric] using k2(2)
using trancl_power by blast
then have "(l1,l2) ∈ (call_graph_of_lts R ↾ L)⇧+" unfolding kl1 kl2 .
}
then have L_component: "L × L ⊆ (call_graph_of_lts R ↾ L)⇧+" by auto
have L_empty: "L ≠ {}" unfolding L_def by auto
note copy = copy[unfolded copy_progs_def]
from copy have "cut_points (call_graph_of_lts R) CP" by auto
from this[unfolded cut_points_def, rule_format, OF L_empty L_component] obtain l where
lCP: "l ∈ CP" and "l ∈ L" by auto
from this(2)[unfolded L_def] obtain n where ln: "l = location (seq n)" and nm: "n ≥ m" by auto
from copy lCP obtain P where P: "P ∈ Ps" and copy: "copy_prog P R l" by auto
let ?transition_stepP = "transition_step_lts P"
interpret P: indexed_rewriting ?transition_stepP .
note lift = copy_progD4[OF copy]
have rec: "recurring τs (shift seq n)" using recurring_shift[OF rec, of "n - m"] nm
by auto
let ?τs = "sharp_transition ` τs"
let ?seq = "cut_chain n seq"
from SN[OF P] show False
proof (elim indexed_rewriting.cooperation_SN_onE)
show "?seq 0 ∈ initial_states P" using init copy by auto
show "P.cooperation_chain (flat_transitions_of P) (sharp_transitions_of P) ?seq"
proof
show "P.recurring ?τs (shift ?seq (Suc n))" (is "P.recurring _ ?s'")
using sharp_morphism.recurring_morphism[OF rec]
by(subst shift_cut_chain, auto simp: lift lift_state_conditions_def o_def)
next
fix i assume i: "i < Suc n"
show "(?seq i, ?seq (Suc i)) ∈ ⋃ (transition_step_lts P ` flat_transitions_of P)"
proof (cases "i = n")
case True
obtain α where 1: "seq n = State α l" using ln by (cases "seq n", auto)
have 2: "(seq n, seq (Suc n)) ∈ transition R" using chain by auto
from 2 have "state_lts R (State α l)" by (auto simp: 1)
then have "(flat_state (seq n), sharp_state (seq n)) ∈ transition P"
unfolding 1 relabel_state.simps
by (intro cut_transition[OF copy_progD2[OF copy], of "α"], auto simp: lift o_def)
then obtain τ
where τ: "τ ∈ transition_rules P"
and step: "(flat_state (seq n), sharp_state (seq n)) ∈ ?transition_stepP τ" by (unfold transition_def, auto)
then have "source τ = Flat l" unfolding 1 by auto
with τ step True show ?thesis by (auto intro: exI[of _ τ])
next
case False
with i have i: "i < n" by auto
from chain obtain τ
where τ: "τ ∈ transition_rules R" and *: "(seq i, seq (Suc i)) ∈ ?transition_step τ" by (unfold transition_def, auto)
from τ copy have "flat_transition τ ∈ flat_transitions_of P" by auto
with τ flat_transition[OF *, unfolded lift] i
show ?thesis by (auto intro!: exI[of _ "flat_transition τ"] simp:lift_state_conditions_def o_def lift)
qed
next
show "sharp_transition ` τs ⊆ sharp_transitions_of P"
proof
fix τ' assume "τ' ∈ sharp_transition ` τs"
then obtain τ where "τ ∈ τs" "τ' = sharp_transition τ" by auto
with τs copy_progD(4)[OF copy]
show "τ' ∈ sharp_transitions_of P" by auto
qed
qed
qed
qed
end
fun make_copy_prog where
"make_copy_prog (Lts_Impl init τs lc) cutpoints =
Lts_Impl (map Flat init)
(map (λ(tr,τ). (Flat tr, flat_transition τ)) τs @ cutpoints @
map (λ(tr,τ). (Sharp tr, sharp_transition τ)) τs)
(map (λ(tr,τ). (Flat tr, τ)) lc @ map (λ(tr,τ). (Sharp tr, τ)) lc) "
type_synonym ('f,'v,'t,'l,'tr)initial_cp_proof =
"('tr sharp × ('f, 'v, 't, 'l sharp) transition_rule) list"
context pre_lts_checker
begin
definition "check_exists_cut taus n =
check (∃τ ∈ set taus.
source τ = Flat n ∧ target τ = Sharp n ∧ isOK(check_skip_transition τ))
(showsl_lit (STR ''missing skip transition for '') o showsl n)"
definition check_copy_prog where
"check_copy_prog Pi Cp = do {
check_allm (check_exists_cut (map snd (transitions_impl Pi))) Cp
}"
definition create_initial_cp_prog where
"create_initial_cp_prog P cp_trans_list =
check_return (
do {
let cp_trans = concat cp_trans_list;
let cut_points = remdups (map (λ(tr,τ). natural (source τ)) cp_trans);
check_cut_points (call_graph_impl P) (set cut_points)
<+? (λ s. showsl_lit (STR ''problem in ensuring validity of cutpoints⏎'') o s);
check_allm (λ (n,cp). check (transition_rule cp)
(showsl n o showsl_lit (STR '' is non valid transition rule''))) cp_trans;
check_allm (check_exists_cut (map snd cp_trans)) cut_points
}) (map (λ cp_trans. (make_copy_prog P cp_trans)) cp_trans_list)"
end
declare pre_lts_checker.check_copy_prog_def[code]
declare pre_lts_checker.check_exists_cut_def[code]
declare pre_lts_checker.create_initial_cp_prog_def[code]
context lts_checker begin
lemma transition_rule_flat_transition[simp]: "transition_rule (flat_transition t) = transition_rule t"
by (cases t, auto)
lemma transition_rule_sharp_transition[simp]: "transition_rule (sharp_transition t) = transition_rule t"
by (cases t, auto)
lemma create_initial_cp_prog:
assumes ok: "create_initial_cp_prog P cp_trans_list = return CPs"
and cSN: "⋀ CP. CP ∈ set CPs ⟹ cooperation_SN_impl CP"
and P: "lts_impl P"
shows "lts_termination (lts_of P)"
proof -
define all_cp_trans where "all_cp_trans ≡ concat cp_trans_list"
note ok = ok[unfolded create_initial_cp_prog_def Let_def all_cp_trans_def[symmetric], simplified]
from ok have "⋀ n y. (n, y) ∈ set all_cp_trans ⟹ transition_rule y" by auto
then have cp_trans: "⋀ cp_trans tr τ. cp_trans ∈ set cp_trans_list ⟹ (tr, τ) ∈ set cp_trans ⟹ transition_rule τ"
by (auto simp: all_cp_trans_def)
define CP where "CP = ((λ(tr, τ). natural (source τ)) ` set all_cp_trans)"
from ok have "isOK (check_cut_points (call_graph_impl P) CP)" by (auto simp: CP_def)
from check_cut_points[OF this] have "cut_points (call_graph_of_lts (lts_of P)) CP" by simp
show ?thesis
proof (rule initial_cooperation_program[OF _ _ lts_impl[OF P]]; (unfold copy_progs_def, intro conjI ballI)?)
show "finite (transition_rules (lts_of P))" by auto
show "cut_points (call_graph_of_lts (lts_of P)) CP" by fact
fix l
assume "l ∈ CP"
with ok have "isOK(check_exists_cut (map snd all_cp_trans) l)" unfolding CP_def by auto
from this[unfolded all_cp_trans_def check_exists_cut_def, simplified]
obtain cp_trans where mem: "cp_trans ∈ set cp_trans_list"
and cut: "exists_cut (lts_of (make_copy_prog P cp_trans)) l"
unfolding exists_cut_def by (cases P, auto simp: all_cp_trans_def dest!: check_skip_transition intro!: cp_trans)
define R where "R = make_copy_prog P cp_trans"
note cut = cut[folded R_def]
have lc: "assertion (lts_of R) = assertion (lts_of P) o natural"
proof (cases P)
case (Lts_Impl a b lc)
note d = map_of_default_def lookup_default_def lookup_of_alist
let ?lc = "map (λ(tr, y). (Flat tr, y)) lc @ map (λ(tr, y). (sharp.Sharp tr, y)) lc"
have id: "?thesis = (map_of_default True⇩f ?lc = (λx. map_of_default True⇩f lc (natural x)))" (is "_ = (?l = ?r)")
unfolding Lts_Impl R_def by (simp add: o_def assertion_of_def)
have id2: "map_of ?lc l = map_of lc (natural l)" for l
proof (cases l)
case (Flat ll)
have None: "map_of (map (λ(tr, y). (sharp.Sharp tr, y)) lc) l = None" unfolding Flat map_of_eq_None_iff by auto
have "map_of ?lc l = map_of (map (λ(tr, y). (Flat tr, y)) lc) l"
unfolding map_of_append
by (rule map_add_left_None, rule None)
also have "… = map_of lc ll" unfolding Flat by (induct lc, auto)
finally show ?thesis unfolding Flat by simp
next
case (Sharp ll)
have None: "map_of (map (λ(tr, y). (sharp.Flat tr, y)) lc) l = None" unfolding Sharp map_of_eq_None_iff by auto
have "map_of ?lc l = map_of (map (λ(tr, y). (Sharp tr, y)) lc) l"
unfolding map_of_append
by (rule map_add_find_left, rule None)
also have "… = map_of lc ll" unfolding Sharp by (induct lc, auto)
finally show ?thesis unfolding Sharp by simp
qed
show ?thesis unfolding id d using id2 by (intro ext, auto split: option.splits)
qed
from ok have mem: "R ∈ set CPs" using mem unfolding R_def by auto
have "copy_prog (lts_of R) (lts_of P) l"
by (intro copy_progI[OF _ cut _ _ lc], unfold R_def, (cases P, auto)+)
with mem show "∃ R ∈ lts_of ` set CPs. copy_prog R (lts_of P) l" by auto
next
fix R
assume "R ∈ lts_of ` set CPs"
then obtain RR where mem: "RR ∈ set CPs" and R: "R = lts_of RR" by auto
from ok mem obtain cp_trans where mem': "cp_trans ∈ set cp_trans_list"
and RR: "RR = make_copy_prog P cp_trans" by auto
have lts: "lts_impl RR" unfolding RR by (insert P mem' cp_trans, cases P, auto)
with cSN[OF mem] show "cooperation_SN R" unfolding R by (elim cooperation_SN_implE, auto)
qed
qed
end
end