Theory Lasso
section ‹Lassos›
theory Lasso
imports Automata
begin
record 'v lasso =
lasso_reach :: "'v list"
lasso_va :: "'v"
lasso_cysfx :: "'v list"
definition "lasso_v0 L ≡ case lasso_reach L of [] ⇒ lasso_va L | (v0#_) ⇒ v0"
definition lasso_cycle where "lasso_cycle L = lasso_va L # lasso_cysfx L"
definition "lasso_of_prpl prpl ≡ case prpl of (pr,pl) ⇒ ⦇
lasso_reach = pr,
lasso_va = hd pl,
lasso_cysfx = tl pl ⦈"
definition "prpl_of_lasso L ≡ (lasso_reach L, lasso_va L # lasso_cysfx L)"
lemma prpl_of_lasso_simps[simp]:
"fst (prpl_of_lasso L) = lasso_reach L"
"snd (prpl_of_lasso L) = lasso_va L # lasso_cysfx L"
unfolding prpl_of_lasso_def by auto
lemma lasso_of_prpl_simps[simp]:
"lasso_reach (lasso_of_prpl prpl) = fst prpl"
"snd prpl ≠ [] ⟹ lasso_cycle (lasso_of_prpl prpl) = snd prpl"
unfolding lasso_of_prpl_def lasso_cycle_def by (auto split: prod.split)
definition run_of_lasso :: "'q lasso ⇒ 'q word"
where "run_of_lasso L ≡ lasso_reach L ⌢ (lasso_cycle L)⇧ω"
lemma run_of_lasso_of_prpl:
"pl ≠ [] ⟹ run_of_lasso (lasso_of_prpl (pr, pl)) = pr ⌢ pl⇧ω"
unfolding run_of_lasso_def lasso_of_prpl_def lasso_cycle_def
by auto
definition "map_lasso f L ≡ ⦇
lasso_reach = map f (lasso_reach L),
lasso_va = f (lasso_va L),
lasso_cysfx = map f (lasso_cysfx L)
⦈"
lemma map_lasso_simps[simp]:
"lasso_reach (map_lasso f L) = map f (lasso_reach L)"
"lasso_va (map_lasso f L) = f (lasso_va L)"
"lasso_cysfx (map_lasso f L) = map f (lasso_cysfx L)"
"lasso_v0 (map_lasso f L) = f (lasso_v0 L)"
"lasso_cycle (map_lasso f L) = map f (lasso_cycle L)"
unfolding map_lasso_def lasso_v0_def lasso_cycle_def
by (auto split: list.split)
lemma map_lasso_run[simp]:
shows "run_of_lasso (map_lasso f L) = f o (run_of_lasso L)"
by (auto simp add: map_lasso_def run_of_lasso_def conc_def iter_def
lasso_cycle_def lasso_v0_def fun_eq_iff not_less nth_Cons'
nz_le_conv_less)
context graph begin
definition is_lasso_pre :: "'v lasso ⇒ bool"
where "is_lasso_pre L ≡
lasso_v0 L ∈ V0
∧ path E (lasso_v0 L) (lasso_reach L) (lasso_va L)
∧ path E (lasso_va L) (lasso_cycle L) (lasso_va L)"
definition "is_lasso_prpl_pre prpl ≡ case prpl of (pr, pl) ⇒ ∃v0 va.
v0∈V0
∧ pl ≠ []
∧ path E v0 pr va
∧ path E va pl va"
lemma is_lasso_pre_prpl_of_lasso[simp]:
"is_lasso_prpl_pre (prpl_of_lasso L) ⟷ is_lasso_pre L"
unfolding is_lasso_pre_def prpl_of_lasso_def is_lasso_prpl_pre_def
unfolding lasso_v0_def lasso_cycle_def
by (auto simp: path_simps split: list.split)
lemma is_lasso_prpl_pre_conv:
"is_lasso_prpl_pre prpl
⟷ (snd prpl≠[] ∧ is_lasso_pre (lasso_of_prpl prpl))"
unfolding is_lasso_pre_def lasso_of_prpl_def is_lasso_prpl_pre_def
unfolding lasso_v0_def lasso_cycle_def
apply (cases prpl)
apply (rename_tac a b)
apply (case_tac b)
apply (auto simp: path_simps split: list.splits)
done
lemma is_lasso_pre_empty[simp]: "V0 = {} ⟹ ¬is_lasso_pre L"
unfolding is_lasso_pre_def by auto
lemma run_of_lasso_pre:
assumes "is_lasso_pre L"
shows "is_run (run_of_lasso L)"
and "run_of_lasso L 0 ∈ V0"
using assms
unfolding is_lasso_pre_def is_run_def run_of_lasso_def
lasso_cycle_def lasso_v0_def
by (auto simp: ipath_conc_conv ipath_iter_conv path_cons_conv conc_fst
split: list.splits)
end
context gb_graph begin
definition is_lasso
:: "'Q lasso ⇒ bool"
where "is_lasso L ≡
is_lasso_pre L
∧ (∀A∈F. (set (lasso_cycle L)) ∩ A ≠ {})"
definition "is_lasso_prpl prpl ≡
is_lasso_prpl_pre prpl
∧ (∀A∈F. set (snd prpl) ∩ A ≠ {})"
lemma is_lasso_prpl_of_lasso[simp]:
"is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
unfolding is_lasso_def is_lasso_prpl_def
unfolding lasso_v0_def lasso_cycle_def
by auto
lemma is_lasso_prpl_conv:
"is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
apply safe
apply simp_all
done
lemma is_lasso_empty[simp]: "V0 = {} ⟹ ¬is_lasso L"
unfolding is_lasso_def by auto
lemma lasso_accepted:
assumes L: "is_lasso L"
shows "is_acc_run (run_of_lasso L)"
proof -
obtain "pr" va pls where
[simp]: "L = ⦇lasso_reach = pr,lasso_va = va,lasso_cysfx = pls⦈"
by (cases L)
from L have "is_run (run_of_lasso L)"
unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
moreover from L have "(∀A∈F. set (va#pls) ∩ A ≠ {})"
by (auto simp: is_lasso_def lasso_cycle_def)
moreover from L have "(run_of_lasso L) 0 ∈ V0"
unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
ultimately show "is_acc_run (run_of_lasso L)"
unfolding is_acc_run_def is_acc_def run_of_lasso_def
lasso_cycle_def lasso_v0_def
by (fastforce intro: limit_inter_INF)
qed
lemma lasso_prpl_acc_run:
"is_lasso_prpl (pr, pl) ⟹ is_acc_run (pr ⌢ iter pl)"
apply (clarsimp simp: is_lasso_prpl_conv)
apply (drule lasso_accepted)
apply (simp add: run_of_lasso_of_prpl)
done
end
context gb_graph
begin
lemma accepted_lasso:
assumes [simp, intro]: "finite (E⇧* `` V0)"
assumes A: "is_acc_run r"
shows "∃L. is_lasso L"
proof -
from A have
RUN: "is_run r"
and ACC: "∀A∈F. limit r ∩ A ≠ {}"
by (auto simp: is_acc_run_limit_alt)
from RUN have [simp]: "r 0 ∈ V0" and RUN': "ipath E r"
by (simp_all add: is_run_def)
txt ‹Choose a node that is visited infinitely often›
from RUN have RAN_REACH: "range r ⊆ E⇧*``V0"
by (auto simp: is_run_def dest: ipath_to_rtrancl)
hence "finite (range r)" by (auto intro: finite_subset)
then obtain u where "u∈limit r" using limit_nonempty by blast
hence U_REACH: "u∈E⇧*``V0" using RAN_REACH limit_in_range by force
then obtain v0 "pr" where PR: "v0∈V0" "path E v0 pr u"
by (auto intro: rtrancl_is_path)
moreover
txt ‹Build a path from ‹u› to ‹u›, that contains nodes from
each acceptance set›
have "∃pl. pl≠[] ∧ path E u pl u ∧ (∀A∈F. set pl ∩ A ≠ {})"
using finite_F ACC
proof (induction rule: finite_induct)
case empty
from run_limit_two_connectedI[OF RUN' ‹u∈limit r› ‹u∈limit r›]
obtain p where [simp]: "p≠[]" and P: "path E u p u"
by (rule trancl_is_path)
thus ?case by blast
next
case (insert A F)
from insert.IH insert.prems obtain pl where
[simp]: "pl≠[]"
and P: "path E u pl u"
and ACC: "(∀A'∈F. set pl ∩ A' ≠ {})"
by auto
from insert.prems obtain v where VACC: "v∈A" "v∈limit r" by auto
from run_limit_two_connectedI[OF RUN' ‹u∈limit r› ‹v∈limit r›]
obtain p1 where [simp]: "p1≠[]"
and P1: "path E u p1 v"
by (rule trancl_is_path)
from run_limit_two_connectedI[OF RUN' ‹v∈limit r› ‹u∈limit r›]
obtain p2 where [simp]: "p2≠[]"
and P2: "path E v p2 u"
by (rule trancl_is_path)
note P also note P1 also (path_conc) note P2 finally (path_conc)
have "path E u (pl@p1@p2) u" by simp
moreover from P2 have "v∈set (p1@p2)"
by (cases p2) (auto simp: path_cons_conv)
with ACC VACC have "(∀A'∈insert A F. set (pl@p1@p2) ∩ A' ≠ {})" by auto
moreover have "pl@p1@p2 ≠ []" by auto
ultimately show ?case by (intro exI conjI)
qed
then obtain pl where "pl ≠ []" "path E u pl u" "(∀A∈F. set pl ∩ A ≠ {})"
by blast
then obtain pls where "path E u (u#pls) u" "∀A∈F. set (u#pls) ∩ A ≠ {}"
by (cases pl) (auto simp add: path_simps)
ultimately show ?thesis
apply -
apply (rule
exI[where x="⦇lasso_reach = pr,lasso_va = u,lasso_cysfx = pls⦈"])
unfolding is_lasso_def lasso_v0_def lasso_cycle_def is_lasso_pre_def
apply (cases "pr")
apply (simp_all add: path_simps)
done
qed
end
context b_graph
begin
definition is_lasso where "is_lasso L ≡
is_lasso_pre L
∧ (set (lasso_cycle L)) ∩ F ≠ {}"
definition is_lasso_prpl where "is_lasso_prpl L ≡
is_lasso_prpl_pre L
∧ (set (snd L)) ∩ F ≠ {}"
lemma is_lasso_pre_ext[simp]:
"gbg.is_lasso_pre T m = is_lasso_pre"
unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
unfolding to_gbg_ext_def
by auto
lemma is_lasso_gbg:
"gbg.is_lasso T m = is_lasso"
unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
apply simp
apply (auto simp: to_gbg_ext_def lasso_cycle_def)
done
lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]
lemma is_lasso_prpl_of_lasso[simp]:
"is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
unfolding is_lasso_def is_lasso_prpl_def
unfolding lasso_v0_def lasso_cycle_def
by auto
lemma is_lasso_prpl_conv:
"is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
apply safe
apply auto
done
lemma lasso_prpl_acc_run:
"is_lasso_prpl (pr, pl) ⟹ is_acc_run (pr ⌢ iter pl)"
apply (clarsimp simp: is_lasso_prpl_conv)
apply (drule lasso_accepted)
apply (simp add: run_of_lasso_of_prpl)
done
end
context igb_graph begin
definition "is_lasso L ≡
is_lasso_pre L
∧ (∀i<num_acc. ∃q∈set (lasso_cycle L). i∈acc q)"
definition "is_lasso_prpl L ≡
is_lasso_prpl_pre L
∧ (∀i<num_acc. ∃q∈set (snd L). i∈acc q)"
lemma is_lasso_prpl_of_lasso[simp]:
"is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
unfolding is_lasso_def is_lasso_prpl_def
unfolding lasso_v0_def lasso_cycle_def
by auto
lemma is_lasso_prpl_conv:
"is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
apply safe
apply auto
done
lemma is_lasso_pre_ext[simp]:
"gbg.is_lasso_pre T m = is_lasso_pre"
unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
unfolding to_gbg_ext_def
by auto
lemma is_lasso_gbg: "gbg.is_lasso T m = is_lasso"
unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
apply simp
apply (simp_all add: to_gbg_ext_def)
apply (intro ext)
apply (fo_rule arg_cong | intro ext)+
apply (auto simp: F_def accn_def intro!: ext)
done
lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]
lemma lasso_prpl_acc_run:
"is_lasso_prpl (pr, pl) ⟹ is_acc_run (pr ⌢ iter pl)"
apply (clarsimp simp: is_lasso_prpl_conv)
apply (drule lasso_accepted)
apply (simp add: run_of_lasso_of_prpl)
done
lemma degen_lasso_sound:
assumes A: "degen.is_lasso T m L"
shows "is_lasso (map_lasso fst L)"
proof -
from A have
V0: "lasso_v0 L ∈ degen.V0 T m" and
REACH: "path (degen.E T m)
(lasso_v0 L) (lasso_reach L) (lasso_va L)" and
LOOP: "path (degen.E T m)
(lasso_va L) (lasso_cycle L) (lasso_va L)" and
ACC: "(set (lasso_cycle L)) ∩ degen.F T m ≠ {}"
unfolding degen.is_lasso_def degen.is_lasso_pre_def by auto
{
fix i
assume "i<num_acc"
hence "∃q∈set (lasso_cycle L). i ∈ local.acc (fst q) ∧ snd q = i"
proof (induction i)
case 0
thus ?case using ACC unfolding degeneralize_ext_def by fastforce
next
case (Suc i)
then obtain q where "(q,i)∈set (lasso_cycle L)" and "i∈acc q" by auto
with LOOP obtain pl' where SPL: "set (lasso_cycle L) = set pl'"
and PS: "path (degen.E T m) (q,i) pl' (q,i)"
by (blast elim: path_loop_shift)
from SPL have "pl'≠[]" by (auto simp: lasso_cycle_def)
then obtain pl'' where [simp]: "pl'=(q,i)#pl''"
using PS by (cases pl') (auto simp: path_simps)
then obtain q2 pl''' where
[simp]: "pl'' = (q2,(i + 1) mod num_acc)#pl'''"
using PS ‹i∈acc q› ‹Suc i < num_acc›
apply (cases pl'')
apply (auto
simp: path_simps degeneralize_ext_def
split: if_split_asm)
done
from PS have
"path (degen.E T m) (q2,Suc i) pl'' (q,i)"
using ‹Suc i < num_acc›
by (auto simp: path_simps)
from degen_visit_acc[OF this] obtain qa
where "(qa,Suc i)∈set pl''" "Suc i ∈ acc qa"
by auto
thus ?case
by (rule_tac bexI[where x="(qa,Suc i)"]) (auto simp: SPL)
qed
} note aux=this
from degen_V0_sound[OF V0]
degen_path_sound[OF REACH]
degen_path_sound[OF LOOP] aux
show ?thesis
unfolding is_lasso_def is_lasso_pre_def
by auto
qed
end
definition lasso_rel_ext_internal_def: "⋀Re R. lasso_rel_ext Re R ≡ {
(⦇ lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', …=m' ⦈,
⦇ lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, …=m ⦈) |
r' r va' va cysfx' cysfx m' m.
(r',r) ∈ ⟨R⟩list_rel
∧ (va',va)∈R
∧ (cysfx', cysfx) ∈ ⟨R⟩list_rel
∧ (m',m) ∈ Re
}"
lemma lasso_rel_ext_def: "⋀ Re R. ⟨Re,R⟩lasso_rel_ext = {
(⦇ lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', …=m' ⦈,
⦇ lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, …=m ⦈) |
r' r va' va cysfx' cysfx m' m.
(r',r) ∈ ⟨R⟩list_rel
∧ (va',va)∈R
∧ (cysfx', cysfx) ∈ ⟨R⟩list_rel
∧ (m',m) ∈ Re
}"
unfolding lasso_rel_ext_internal_def relAPP_def by auto
lemma lasso_rel_ext_sv[relator_props]:
"⋀ Re R. ⟦ single_valued Re; single_valued R ⟧ ⟹ single_valued (⟨Re,R⟩lasso_rel_ext)"
unfolding lasso_rel_ext_def
apply (rule single_valuedI)
apply safe
apply (blast dest: single_valuedD list_rel_sv[THEN single_valuedD])+
done
lemma lasso_rel_ext_id[relator_props]:
"⋀Re R. ⟦ Re=Id; R=Id ⟧ ⟹ ⟨Re,R⟩lasso_rel_ext = Id"
unfolding lasso_rel_ext_def
apply simp
apply safe
by (metis lasso.surjective)
consts i_lasso_ext :: "interface ⇒ interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of lasso_rel_ext i_lasso_ext]
find_consts "(_,_) lasso_scheme"
term lasso_reach_update
lemma lasso_param[param, autoref_rules]:
"⋀Re R. (lasso_reach, lasso_reach) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
"⋀Re R. (lasso_va, lasso_va) ∈ ⟨Re,R⟩lasso_rel_ext → R"
"⋀Re R. (lasso_cysfx, lasso_cysfx) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
"⋀Re R. (lasso_ext, lasso_ext)
∈ ⟨R⟩list_rel → R → ⟨R⟩list_rel → Re → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso_reach_update, lasso_reach_update)
∈ (⟨R⟩list_rel → ⟨R⟩list_rel) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso_va_update, lasso_va_update)
∈ (R→R) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso_cysfx_update, lasso_cysfx_update)
∈ (⟨R⟩list_rel → ⟨R⟩list_rel) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso.more_update, lasso.more_update)
∈ (Re→Re) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
unfolding lasso_rel_ext_def
by (auto dest: fun_relD)
lemma lasso_param2[param, autoref_rules]:
"⋀Re R. (lasso_v0, lasso_v0) ∈ ⟨Re,R⟩lasso_rel_ext → R"
"⋀Re R. (lasso_cycle, lasso_cycle) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
"⋀Re R. (map_lasso, map_lasso)
∈ (R→R') → ⟨Re,R⟩lasso_rel_ext → ⟨unit_rel,R'⟩lasso_rel_ext"
unfolding lasso_v0_def[abs_def] lasso_cycle_def[abs_def] map_lasso_def[abs_def]
by parametricity+
lemma lasso_of_prpl_param: "⟦(l',l)∈⟨R⟩list_rel ×⇩r ⟨R⟩list_rel; snd l ≠ []⟧
⟹ (lasso_of_prpl l', lasso_of_prpl l) ∈ ⟨unit_rel,R⟩lasso_rel_ext"
unfolding lasso_of_prpl_def
apply (cases l, cases l', clarsimp)
apply (case_tac b, simp, case_tac ba, clarsimp_all)
apply parametricity
done
context begin interpretation autoref_syn .
lemma lasso_of_prpl_autoref[autoref_rules]:
assumes "SIDE_PRECOND (snd l ≠ [])"
assumes "(l',l)∈⟨R⟩list_rel ×⇩r ⟨R⟩list_rel"
shows "(lasso_of_prpl l',
(OP lasso_of_prpl
::: ⟨R⟩list_rel ×⇩r ⟨R⟩list_rel → ⟨unit_rel,R⟩lasso_rel_ext)$l)
∈ ⟨unit_rel,R⟩lasso_rel_ext"
using assms
apply (simp add: lasso_of_prpl_param)
done
end
subsection ‹Implementing runs by lassos›
definition lasso_run_rel_def_internal:
"lasso_run_rel R ≡ br run_of_lasso (λ_. True) O (nat_rel → R)"
lemma lasso_run_rel_def:
"⟨R⟩lasso_run_rel = br run_of_lasso (λ_. True) O (nat_rel → R)"
unfolding lasso_run_rel_def_internal relAPP_def by simp
lemma lasso_run_rel_sv[relator_props]:
"single_valued R ⟹ single_valued (⟨R⟩lasso_run_rel)"
unfolding lasso_run_rel_def
by tagged_solver
consts i_run :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of lasso_run_rel i_run]
definition [simp]: "op_map_run ≡ (o)"
lemma [autoref_op_pat]: "(o) ≡ op_map_run" by simp
lemma map_lasso_run_refine[autoref_rules]:
shows "(map_lasso,op_map_run) ∈ (R→R') → ⟨R⟩lasso_run_rel → ⟨R'⟩lasso_run_rel"
unfolding lasso_run_rel_def op_map_run_def
proof (intro fun_relI)
fix f f' l r
assume [param]: "(f,f')∈R→R'" and
"(l, r) ∈ br run_of_lasso (λ_. True) O (nat_rel → R)"
then obtain r' where [param]: "(r',r)∈nat_rel → R"
and [simp]: "r' = run_of_lasso l"
by (auto simp: br_def)
have "(map_lasso f l, f o r') ∈ br run_of_lasso (λ_. True)"
by (simp add: br_def)
also have "(f o r', f' o r) ∈ nat_rel → R'" by parametricity
finally (relcompI) show
"(map_lasso f l, f' o r) ∈ br run_of_lasso (λ_. True) O (nat_rel → R')"
.
qed
end