Theory LTS
section ‹Labelled transition systems›
theory LTS
imports
"../Basic/Auxiliary"
Coinductive.TLList
begin
no_notation floor ("⌊_⌋")
lemma rel_option_mono:
"⟦ rel_option R x y; ⋀x y. R x y ⟹ R' x y ⟧ ⟹ rel_option R' x y"
by(cases x)(case_tac [!] y, auto)
lemma nth_concat_conv:
"n < length (concat xss)
⟹ ∃m n'. concat xss ! n = (xss ! m) ! n' ∧ n' < length (xss ! m) ∧
m < length xss ∧ n = (∑i<m. length (xss ! i)) + n'"
using lnth_lconcat_conv[of n "llist_of (map llist_of xss)"]
sum_comp_morphism[where h = enat and g = "λi. length (xss ! i)"]
by(clarsimp simp add: lconcat_llist_of zero_enat_def[symmetric]) blast
definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ 'b ⇒ 'a ⇒ 'c"
where "flip f = (λb a. f a b)"
text ‹Create a dynamic list ‹flip_simps› of theorems for flip›
ML ‹
structure FlipSimpRules = Named_Thms
(
val name = @{binding flip_simps}
val description = "Simplification rules for flip in bisimulations"
)
›
setup ‹FlipSimpRules.setup›
lemma flip_conv [flip_simps]: "flip f b a = f a b"
by(simp add: flip_def)
lemma flip_flip [flip_simps, simp]: "flip (flip f) = f"
by(simp add: flip_def)
lemma list_all2_flip [flip_simps]: "list_all2 (flip P) xs ys = list_all2 P ys xs"
unfolding flip_def list_all2_conv_all_nth by auto
lemma llist_all2_flip [flip_simps]: "llist_all2 (flip P) xs ys = llist_all2 P ys xs"
unfolding flip_def llist_all2_conv_all_lnth by auto
lemma rtranclp_flipD:
assumes "(flip r)^** x y"
shows "r^** y x"
using assms
by(induct rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl simp add: flip_conv)
lemma rtranclp_flip [flip_simps]:
"(flip r)^** = flip r^**"
by(auto intro!: ext simp add: flip_conv intro: rtranclp_flipD)
lemma rel_prod_flip [flip_simps]:
"rel_prod (flip R) (flip S) = flip (rel_prod R S)"
by(auto intro!: ext simp add: flip_def)
lemma rel_option_flip [flip_simps]:
"rel_option (flip R) = flip (rel_option R)"
by(simp add: fun_eq_iff rel_option_iff flip_def)
lemma tllist_all2_flip [flip_simps]:
"tllist_all2 (flip P) (flip Q) xs ys ⟷ tllist_all2 P Q ys xs"
proof
assume "tllist_all2 (flip P) (flip Q) xs ys"
thus "tllist_all2 P Q ys xs"
by(coinduct rule: tllist_all2_coinduct)(auto dest: tllist_all2_is_TNilD tllist_all2_tfinite2_terminalD tllist_all2_thdD intro: tllist_all2_ttlI simp add: flip_def)
next
assume "tllist_all2 P Q ys xs"
thus "tllist_all2 (flip P) (flip Q) xs ys"
by(coinduct rule: tllist_all2_coinduct)(auto dest: tllist_all2_is_TNilD tllist_all2_tfinite2_terminalD tllist_all2_thdD intro: tllist_all2_ttlI simp add: flip_def)
qed
subsection ‹Labelled transition systems›
type_synonym ('a, 'b) trsys = "'a ⇒ 'b ⇒ 'a ⇒ bool"
locale trsys =
fixes trsys :: "('s, 'tl) trsys" ("_/ -_→/ _" [50, 0, 50] 60)
begin
abbreviation Trsys :: "('s, 'tl list) trsys" ("_/ -_→*/ _" [50,0,50] 60)
where "⋀tl. s -tl→* s' ≡ rtrancl3p trsys s tl s'"
coinductive inf_step :: "'s ⇒ 'tl llist ⇒ bool" ("_ -_→* ∞" [50, 0] 80)
where inf_stepI: "⟦ trsys a b a'; a' -bs→* ∞ ⟧ ⟹ a -LCons b bs→* ∞"
coinductive inf_step_table :: "'s ⇒ ('s × 'tl × 's) llist ⇒ bool" ("_ -_→*t ∞" [50, 0] 80)
where
inf_step_tableI:
"⋀tl. ⟦ trsys s tl s'; s' -stls→*t ∞ ⟧
⟹ s -LCons (s, tl, s') stls→*t ∞"
definition inf_step2inf_step_table :: "'s ⇒ 'tl llist ⇒ ('s × 'tl × 's) llist"
where
"inf_step2inf_step_table s tls =
unfold_llist
(λ(s, tls). lnull tls)
(λ(s, tls). (s, lhd tls, SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞))
(λ(s, tls). (SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞, ltl tls))
(s, tls)"
coinductive Rtrancl3p :: "'s ⇒ ('tl, 's) tllist ⇒ bool"
where
Rtrancl3p_stop: "(⋀tl s'. ¬ s -tl→ s') ⟹ Rtrancl3p s (TNil s)"
| Rtrancl3p_into_Rtrancl3p: "⋀tl. ⟦ s -tl→ s'; Rtrancl3p s' tlss ⟧ ⟹ Rtrancl3p s (TCons tl tlss)"
inductive_simps Rtrancl3p_simps:
"Rtrancl3p s (TNil s')"
"Rtrancl3p s (TCons tl' tlss)"
inductive_cases Rtrancl3p_cases:
"Rtrancl3p s (TNil s')"
"Rtrancl3p s (TCons tl' tlss)"
coinductive Runs :: "'s ⇒ 'tl llist ⇒ bool"
where
Stuck: "(⋀tl s'. ¬ s -tl→ s') ⟹ Runs s LNil"
| Step: "⋀tl. ⟦ s -tl→ s'; Runs s' tls ⟧ ⟹ Runs s (LCons tl tls)"
coinductive Runs_table :: "'s ⇒ ('s × 'tl × 's) llist ⇒ bool"
where
Stuck: "(⋀tl s'. ¬ s -tl→ s') ⟹ Runs_table s LNil"
| Step: "⋀tl. ⟦ s -tl→ s'; Runs_table s' stlss ⟧ ⟹ Runs_table s (LCons (s, tl, s') stlss)"
inductive_simps Runs_table_simps:
"Runs_table s LNil"
"Runs_table s (LCons stls stlss)"
lemma inf_step_not_finite_llist:
assumes r: "s -bs→* ∞"
shows "¬ lfinite bs"
proof
assume "lfinite bs" thus False using r
by(induct arbitrary: s rule: lfinite.induct)(auto elim: inf_step.cases)
qed
lemma inf_step2inf_step_table_LNil [simp]: "inf_step2inf_step_table s LNil = LNil"
by(simp add: inf_step2inf_step_table_def)
lemma inf_step2inf_step_table_LCons [simp]:
fixes tl shows
"inf_step2inf_step_table s (LCons tl tls) =
LCons (s, tl, SOME s'. trsys s tl s' ∧ s' -tls→* ∞)
(inf_step2inf_step_table (SOME s'. trsys s tl s' ∧ s' -tls→* ∞) tls)"
by(simp add: inf_step2inf_step_table_def)
lemma lnull_inf_step2inf_step_table [simp]:
"lnull (inf_step2inf_step_table s tls) ⟷ lnull tls"
by(simp add: inf_step2inf_step_table_def)
lemma inf_step2inf_step_table_eq_LNil:
"inf_step2inf_step_table s tls = LNil ⟷ tls = LNil"
using lnull_inf_step2inf_step_table unfolding lnull_def .
lemma lhd_inf_step2inf_step_table [simp]:
"¬ lnull tls
⟹ lhd (inf_step2inf_step_table s tls) =
(s, lhd tls, SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞)"
by(simp add: inf_step2inf_step_table_def)
lemma ltl_inf_step2inf_step_table [simp]:
"ltl (inf_step2inf_step_table s tls) =
inf_step2inf_step_table (SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞) (ltl tls)"
by(cases tls) simp_all
lemma lmap_inf_step2inf_step_table: "lmap (fst ∘ snd) (inf_step2inf_step_table s tls) = tls"
by(coinduction arbitrary: s tls) auto
lemma inf_step_imp_inf_step_table:
assumes "s -tls→* ∞"
shows "∃stls. s -stls→*t ∞ ∧ tls = lmap (fst ∘ snd) stls"
proof -
from assms have "s -inf_step2inf_step_table s tls→*t ∞"
proof(coinduction arbitrary: s tls)
case (inf_step_table s tls)
thus ?case
proof cases
case (inf_stepI tl s' tls')
let ?s' = "SOME s'. trsys s tl s' ∧ s' -tls'→* ∞"
have "trsys s tl ?s' ∧ ?s' -tls'→* ∞" by(rule someI)(blast intro: inf_stepI)
thus ?thesis using ‹tls = LCons tl tls'› by auto
qed
qed
moreover have "tls = lmap (fst ∘ snd) (inf_step2inf_step_table s tls)"
by(simp only: lmap_inf_step2inf_step_table)
ultimately show ?thesis by blast
qed
lemma inf_step_table_imp_inf_step:
"s-stls→*t ∞ ⟹s -lmap (fst ∘ snd) stls→* ∞"
proof(coinduction arbitrary: s stls rule: inf_step.coinduct)
case (inf_step s tls)
thus ?case by cases auto
qed
lemma Runs_table_into_Runs:
"Runs_table s stlss ⟹ Runs s (lmap (λ(s, tl, s'). tl) stlss)"
proof(coinduction arbitrary: s stlss)
case (Runs s tls)
thus ?case by (cases)auto
qed
lemma Runs_into_Runs_table:
assumes "Runs s tls"
obtains stlss
where "tls = lmap (λ(s, tl, s'). tl) stlss"
and "Runs_table s stlss"
proof -
define stlss where "stlss s tls = unfold_llist
(λ(s, tls). lnull tls)
(λ(s, tls). (s, lhd tls, SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls)))
(λ(s, tls). (SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls), ltl tls))
(s, tls)"
for s tls
have [simp]:
"⋀s. stlss s LNil = LNil"
"⋀s tl tls. stlss s (LCons tl tls) = LCons (s, tl, SOME s'. s -tl→ s' ∧ Runs s' tls) (stlss (SOME s'. s -tl→ s' ∧ Runs s' tls) tls)"
"⋀s tls. lnull (stlss s tls) ⟷ lnull tls"
"⋀s tls. ¬ lnull tls ⟹ lhd (stlss s tls) = (s, lhd tls, SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls))"
"⋀s tls. ¬ lnull tls ⟹ ltl (stlss s tls) = stlss (SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls)) (ltl tls)"
by(simp_all add: stlss_def)
from assms have "tls = lmap (λ(s, tl, s'). tl) (stlss s tls)"
proof(coinduction arbitrary: s tls)
case Eq_llist
thus ?case by cases(auto 4 3 intro: someI2)
qed
moreover
from assms have "Runs_table s (stlss s tls)"
proof(coinduction arbitrary: s tls)
case (Runs_table s stlss')
thus ?case
proof(cases)
case (Step s' tls' tl)
let ?P = "λs'. s -tl→ s' ∧ Runs s' tls'"
from ‹s -tl→ s'› ‹Runs s' tls'› have "?P s'" ..
hence "?P (Eps ?P)" by(rule someI)
with Step have ?Step by auto
thus ?thesis ..
qed simp
qed
ultimately show ?thesis by(rule that)
qed
lemma Runs_lappendE:
assumes "Runs σ (lappend tls tls')"
and "lfinite tls"
obtains σ' where "σ -list_of tls→* σ'"
and "Runs σ' tls'"
proof(atomize_elim)
from ‹lfinite tls› ‹Runs σ (lappend tls tls')›
show "∃σ'. σ -list_of tls→* σ' ∧ Runs σ' tls'"
proof(induct arbitrary: σ)
case lfinite_LNil thus ?case by(auto)
next
case (lfinite_LConsI tls tl)
from ‹Runs σ (lappend (LCons tl tls) tls')›
show ?case unfolding lappend_code
proof(cases)
case (Step σ')
from ‹Runs σ' (lappend tls tls') ⟹ ∃σ''. σ' -list_of tls→* σ'' ∧ Runs σ'' tls'› ‹Runs σ' (lappend tls tls')›
obtain σ'' where "σ' -list_of tls→* σ''" "Runs σ'' tls'" by blast
from ‹σ -tl→ σ'› ‹σ' -list_of tls→* σ''›
have "σ -tl # list_of tls→* σ''" by(rule rtrancl3p_step_converse)
with ‹lfinite tls› have "σ -list_of (LCons tl tls)→* σ''" by(simp)
with ‹Runs σ'' tls'› show ?thesis by blast
qed
qed
qed
lemma Trsys_into_Runs:
assumes "s -tls→* s'"
and "Runs s' tls'"
shows "Runs s (lappend (llist_of tls) tls')"
using assms
by(induct rule: rtrancl3p_converse_induct)(auto intro: Runs.Step)
lemma rtrancl3p_into_Rtrancl3p:
"⟦ rtrancl3p trsys a bs a'; ⋀b a''. ¬ a' -b→ a'' ⟧ ⟹ Rtrancl3p a (tllist_of_llist a' (llist_of bs))"
by(induct rule: rtrancl3p_converse_induct)(auto intro: Rtrancl3p.intros)
lemma Rtrancl3p_into_Runs:
"Rtrancl3p s tlss ⟹ Runs s (llist_of_tllist tlss)"
by(coinduction arbitrary: s tlss rule: Runs.coinduct)(auto elim: Rtrancl3p.cases)
lemma Runs_into_Rtrancl3p:
assumes "Runs s tls"
obtains tlss where "tls = llist_of_tllist tlss" "Rtrancl3p s tlss"
proof
let ?Q = "λs tls s'. s -lhd tls→ s' ∧ Runs s' (ltl tls)"
define tlss where "tlss = corec_tllist
(λ(s, tls). lnull tls) (λ(s, tls). s)
(λ(s, tls). lhd tls)
(λ_. False) undefined (λ(s, tls). (SOME s'. ?Q s tls s', ltl tls))"
have [simp]:
"tlss (s, LNil) = TNil s"
"tlss (s, LCons tl tls) = TCons tl (tlss (SOME s'. ?Q s (LCons tl tls) s', tls))"
for s tl tls by(auto simp add: tlss_def intro: tllist.expand)
show "tls = llist_of_tllist (tlss (s, tls))" using assms
by(coinduction arbitrary: s tls)(erule Runs.cases; fastforce intro: someI2)
show "Rtrancl3p s (tlss (s, tls))" using assms
by(coinduction arbitrary: s tls)(erule Runs.cases; simp; iprover intro: someI2[where Q="trsys _ _"] someI2[where Q="λs'. Runs s' _"])
qed
lemma fixes tl
assumes "Rtrancl3p s tlss" "tfinite tlss"
shows Rtrancl3p_into_Trsys: "Trsys s (list_of (llist_of_tllist tlss)) (terminal tlss)"
and terminal_Rtrancl3p_final: "¬ terminal tlss -tl→ s'"
using assms(2,1) by(induction arbitrary: s rule: tfinite_induct)(auto simp add: Rtrancl3p_simps intro: rtrancl3p_step_converse)
end
subsection ‹Labelled transition systems with internal actions›
locale τtrsys = trsys +
constrains trsys :: "('s, 'tl) trsys"
fixes τmove :: "('s, 'tl) trsys"
begin
inductive silent_move :: "'s ⇒ 's ⇒ bool" ("_ -τ→ _" [50, 50] 60)
where [intro]: "!!tl. ⟦ trsys s tl s'; τmove s tl s' ⟧ ⟹ s -τ→ s'"
declare silent_move.cases [elim]
lemma silent_move_iff: "silent_move = (λs s'. (∃tl. trsys s tl s' ∧ τmove s tl s'))"
by(auto simp add: fun_eq_iff)
abbreviation silent_moves :: "'s ⇒ 's ⇒ bool" ("_ -τ→* _" [50, 50] 60)
where "silent_moves == silent_move^**"
abbreviation silent_movet :: "'s ⇒ 's ⇒ bool" ("_ -τ→+ _" [50, 50] 60)
where "silent_movet == silent_move^++"
coinductive τdiverge :: "'s ⇒ bool" ("_ -τ→ ∞" [50] 60)
where
τdivergeI: "⟦ s -τ→ s'; s' -τ→ ∞ ⟧ ⟹ s -τ→ ∞"
coinductive τinf_step :: "'s ⇒ 'tl llist ⇒ bool" ("_ -τ-_→* ∞" [50, 0] 60)
where
τinf_step_Cons: "⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; s'' -τ-tls→* ∞ ⟧ ⟹ s -τ-LCons tl tls→* ∞"
| τinf_step_Nil: "s -τ→ ∞ ⟹ s -τ-LNil→* ∞"
coinductive τinf_step_table :: "'s ⇒ ('s × 's × 'tl × 's) llist ⇒ bool" ("_ -τ-_→*t ∞" [50, 0] 80)
where
τinf_step_table_Cons:
"⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; s'' -τ-tls→*t ∞ ⟧ ⟹ s -τ-LCons (s, s', tl, s'') tls→*t ∞"
| τinf_step_table_Nil:
"s -τ→ ∞ ⟹ s -τ-LNil→*t ∞"
definition τinf_step2τinf_step_table :: "'s ⇒ 'tl llist ⇒ ('s × 's × 'tl × 's) llist"
where
"τinf_step2τinf_step_table s tls =
unfold_llist
(λ(s, tls). lnull tls)
(λ(s, tls). let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
in (s, s', lhd tls, s''))
(λ(s, tls). let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
in (s'', ltl tls))
(s, tls)"
definition silent_move_from :: "'s ⇒ 's ⇒ 's ⇒ bool"
where "silent_move_from s0 s1 s2 ⟷ silent_moves s0 s1 ∧ silent_move s1 s2"
inductive τrtrancl3p :: "'s ⇒ 'tl list ⇒ 's ⇒ bool" ("_ -τ-_→* _" [50, 0, 50] 60)
where
τrtrancl3p_refl: "τrtrancl3p s [] s"
| τrtrancl3p_step: "⋀tl. ⟦ s -tl→ s'; ¬ τmove s tl s'; τrtrancl3p s' tls s'' ⟧ ⟹ τrtrancl3p s (tl # tls) s''"
| τrtrancl3p_τstep: "⋀tl. ⟦ s -tl→ s'; τmove s tl s'; τrtrancl3p s' tls s'' ⟧ ⟹ τrtrancl3p s tls s''"
coinductive τRuns :: "'s ⇒ ('tl, 's option) tllist ⇒ bool" ("_ ⇓ _" [50, 50] 51)
where
Terminate: "⟦ s -τ→* s'; ⋀tl s''. ¬ s' -tl→ s'' ⟧ ⟹ s ⇓ TNil ⌊s'⌋"
| Diverge: "s -τ→ ∞ ⟹ s ⇓ TNil None"
| Proceed: "⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; s'' ⇓ tls ⟧ ⟹ s ⇓ TCons tl tls"
inductive_simps τRuns_simps:
"s ⇓ TNil (Some s')"
"s ⇓ TNil None"
"s ⇓ TCons tl' tls"
coinductive τRuns_table :: "'s ⇒ ('tl × 's, 's option) tllist ⇒ bool"
where
Terminate: "⟦ s -τ→* s'; ⋀tl s''. ¬ s' -tl→ s'' ⟧ ⟹ τRuns_table s (TNil ⌊s'⌋)"
| Diverge: "s -τ→ ∞ ⟹ τRuns_table s (TNil None)"
| Proceed:
"⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; τRuns_table s'' tls ⟧
⟹ τRuns_table s (TCons (tl, s'') tls)"
definition silent_move2 :: "'s ⇒ 'tl ⇒ 's ⇒ bool"
where "⋀tl. silent_move2 s tl s' ⟷ s -tl→ s' ∧ τmove s tl s'"
abbreviation silent_moves2 :: "'s ⇒ 'tl list ⇒ 's ⇒ bool"
where "silent_moves2 ≡ rtrancl3p silent_move2"
coinductive τRuns_table2 :: "'s ⇒ ('tl list × 's × 'tl × 's, ('tl list × 's) + 'tl llist) tllist ⇒ bool"
where
Terminate: "⟦ silent_moves2 s tls s'; ⋀tl s''. ¬ s' -tl→ s'' ⟧ ⟹ τRuns_table2 s (TNil (Inl (tls, s')))"
| Diverge: "trsys.inf_step silent_move2 s tls ⟹ τRuns_table2 s (TNil (Inr tls))"
| Proceed:
"⋀tl. ⟦ silent_moves2 s tls s'; s' -tl→ s''; ¬ τmove s' tl s''; τRuns_table2 s'' tlsstlss ⟧
⟹ τRuns_table2 s (TCons (tls, s', tl, s'') tlsstlss)"
inductive_simps τRuns_table2_simps:
"τRuns_table2 s (TNil tlss)"
"τRuns_table2 s (TCons tlsstls tlsstlss)"
lemma inf_step_table_all_τ_into_τdiverge:
"⟦ s -stls→*t ∞; ∀(s, tl, s') ∈ lset stls. τmove s tl s' ⟧ ⟹ s -τ→ ∞"
proof(coinduction arbitrary: s stls)
case (τdiverge s)
thus ?case by cases (auto simp add: silent_move_iff, blast)
qed
lemma inf_step_table_lappend_llist_ofD:
"s -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞
⟹ (s -map (fst ∘ snd) stls→* x) ∧ (x -LCons (x, tl', x') xs→*t ∞)"
proof(induct stls arbitrary: s)
case Nil thus ?case by(auto elim: inf_step_table.cases intro: inf_step_table.intros rtrancl3p_refl)
next
case (Cons st stls)
note IH = ‹⋀s. s -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞ ⟹
s -map (fst ∘ snd) stls→* x ∧ x -LCons (x, tl', x') xs→*t ∞›
from ‹s -lappend (llist_of (st # stls)) (LCons (x, tl', x') xs)→*t ∞›
show ?case
proof cases
case (inf_step_tableI s' stls' tl)
hence [simp]: "st = (s, tl, s')" "stls' = lappend (llist_of stls) (LCons (x, tl', x') xs)"
and "s -tl→ s'" "s' -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞" by simp_all
from IH[OF ‹s' -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞›]
have "s' -map (fst ∘ snd) stls→* x" "x -LCons (x, tl', x') xs→*t ∞" by auto
with ‹s -tl→ s'› show ?thesis by(auto simp add: o_def intro: rtrancl3p_step_converse)
qed
qed
lemma inf_step_table_lappend_llist_of_τ_into_τmoves:
assumes "lfinite stls"
shows "⟦ s -lappend stls (LCons (x, tl' x') xs)→*t ∞; ∀(s, tl, s')∈lset stls. τmove s tl s' ⟧ ⟹ s -τ→* x"
using assms
proof(induct arbitrary: s rule: lfinite.induct)
case lfinite_LNil thus ?case by(auto elim: inf_step_table.cases)
next
case (lfinite_LConsI stls st)
note IH = ‹⋀s. ⟦s -lappend stls (LCons (x, tl' x') xs)→*t ∞; ∀(s, tl, s')∈lset stls. τmove s tl s' ⟧ ⟹ s -τ→* x›
obtain s1 tl1 s1' where [simp]: "st = (s1, tl1, s1')" by(cases st)
from ‹s -lappend (LCons st stls) (LCons (x, tl' x') xs)→*t ∞›
show ?case
proof cases
case (inf_step_tableI X' STLS TL)
hence [simp]: "s1 = s" "TL = tl1" "X' = s1'" "STLS = lappend stls (LCons (x, tl' x') xs)"
and "s -tl1→ s1'" and "s1' -lappend stls (LCons (x, tl' x') xs)→*t ∞" by simp_all
from ‹∀(s, tl, s')∈lset (LCons st stls). τmove s tl s'› have "τmove s tl1 s1'" by simp
moreover
from IH[OF ‹s1' -lappend stls (LCons (x, tl' x') xs)→*t ∞›] ‹∀(s, tl, s')∈lset (LCons st stls). τmove s tl s'›
have "s1' -τ→* x" by simp
ultimately show ?thesis using ‹s -tl1→ s1'› by(auto intro: converse_rtranclp_into_rtranclp)
qed
qed
lemma inf_step_table_into_τinf_step:
"s -stls→*t ∞ ⟹ s -τ-lmap (fst ∘ snd) (lfilter (λ(s, tl, s'). ¬ τmove s tl s') stls)→* ∞"
proof(coinduction arbitrary: s stls)
case (τinf_step s stls)
let ?P = "λ(s, tl, s'). ¬ τmove s tl s'"
show ?case
proof(cases "lfilter ?P stls")
case LNil
with τinf_step have ?τinf_step_Nil
by(auto intro: inf_step_table_all_τ_into_τdiverge simp add: lfilter_eq_LNil)
thus ?thesis ..
next
case (LCons stls' xs)
obtain x tl x' where "stls' = (x, tl, x')" by(cases stls')
with LCons have stls: "lfilter ?P stls = LCons (x, tl, x') xs" by simp
from lfilter_eq_LConsD[OF this] obtain stls1 stls2
where stls1: "stls = lappend stls1 (LCons (x, tl, x') stls2)"
and "lfinite stls1"
and τs: "∀(s, tl, s')∈lset stls1. τmove s tl s'"
and nτ: "¬ τmove x tl x'" and xs: "xs = lfilter ?P stls2" by blast
from ‹lfinite stls1› τinf_step τs have "s -τ→* x" unfolding stls1
by(rule inf_step_table_lappend_llist_of_τ_into_τmoves)
moreover from ‹lfinite stls1› have "llist_of (list_of stls1) = stls1" by(simp add: llist_of_list_of)
with τinf_step stls1 have "s -lappend (llist_of (list_of stls1)) (LCons (x, tl, x') stls2)→*t ∞" by simp
from inf_step_table_lappend_llist_ofD[OF this]
have "x -LCons (x, tl, x') stls2→*t ∞" ..
hence "x -tl→ x'" "x' -stls2→*t ∞" by(auto elim: inf_step_table.cases)
ultimately have ?τinf_step_Cons using xs nτ by(auto simp add: stls o_def)
thus ?thesis ..
qed
qed
lemma inf_step_into_τinf_step:
assumes "s -tls→* ∞"
shows "∃A. s -τ-lnths tls A→* ∞"
proof -
from inf_step_imp_inf_step_table[OF assms]
obtain stls where "s -stls→*t ∞" and tls: "tls = lmap (fst ∘ snd) stls" by blast
from ‹s -stls→*t ∞› have "s -τ-lmap (fst ∘ snd) (lfilter (λ(s, tl, s'). ¬ τmove s tl s') stls)→* ∞"
by(rule inf_step_table_into_τinf_step)
hence "s -τ-lnths tls {n. enat n < llength stls ∧ (λ(s, tl, s'). ¬ τmove s tl s') (lnth stls n)}→* ∞"
unfolding lfilter_conv_lnths tls by simp
thus ?thesis by blast
qed
lemma silent_moves_into_τrtrancl3p:
"s -τ→* s' ⟹ s -τ-[]→* s'"
by(induct rule: converse_rtranclp_induct)(blast intro: τrtrancl3p.intros)+
lemma τrtrancl3p_into_silent_moves:
"s -τ-[]→* s' ⟹ s -τ→* s'"
apply(induct s tls≡"[] :: 'tl list" s' rule: τrtrancl3p.induct)
apply(auto intro: converse_rtranclp_into_rtranclp)
done
lemma τrtrancl3p_Nil_eq_τmoves:
"s -τ-[]→* s' ⟷ s -τ→* s'"
by(blast intro: silent_moves_into_τrtrancl3p τrtrancl3p_into_silent_moves)
lemma τrtrancl3p_trans [trans]:
"⟦ s -τ-tls→* s'; s' -τ-tls'→* s'' ⟧ ⟹ s -τ-tls @ tls'→* s''"
apply(induct rule: τrtrancl3p.induct)
apply(auto intro: τrtrancl3p.intros)
done
lemma τrtrancl3p_SingletonE:
fixes tl
assumes red: "s -τ-[tl]→* s'''"
obtains s' s'' where "s -τ→* s'" "s' -tl→ s''" "¬ τmove s' tl s''" "s'' -τ→* s'''"
proof(atomize_elim)
from red show "∃s' s''. s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ→* s'''"
proof(induct s tls≡"[tl]" s''')
case (τrtrancl3p_step s s' s'')
from ‹s -tl→ s'› ‹¬ τmove s tl s'› ‹s' -τ-[]→* s''› show ?case
by(auto simp add: τrtrancl3p_Nil_eq_τmoves)
next
case (τrtrancl3p_τstep s s' s'' tl')
then obtain t' t'' where "s' -τ→* t'" "t' -tl→ t''" "¬ τmove t' tl t''" "t'' -τ→* s''" by auto
moreover
from ‹s -tl'→ s'› ‹τmove s tl' s'› have "s -τ→* s'" by blast
ultimately show ?case by(auto intro: rtranclp_trans)
qed
qed
lemma τrtrancl3p_snocI:
"⋀tl. ⟦ τrtrancl3p s tls s''; s'' -τ→* s'''; s''' -tl→ s'; ¬ τmove s''' tl s' ⟧
⟹ τrtrancl3p s (tls @ [tl]) s'"
apply(erule τrtrancl3p_trans)
apply(fold τrtrancl3p_Nil_eq_τmoves)
apply(drule τrtrancl3p_trans)
apply(erule (1) τrtrancl3p_step)
apply(rule τrtrancl3p_refl)
apply simp
done
lemma τdiverge_rtranclp_silent_move:
"⟦ silent_move^** s s'; s' -τ→ ∞ ⟧ ⟹ s -τ→ ∞"
by(induct rule: converse_rtranclp_induct)(auto intro: τdivergeI)
lemma τdiverge_trancl_coinduct [consumes 1, case_names τdiverge]:
assumes X: "X s"
and step: "⋀s. X s ⟹ ∃s'. silent_move^++ s s' ∧ (X s' ∨ s' -τ→ ∞)"
shows "s -τ→ ∞"
proof -
from X have "∃s'. silent_move^** s s' ∧ X s'" by blast
thus ?thesis
proof(coinduct)
case (τdiverge s)
then obtain s' where "silent_move⇧*⇧* s s'" "X s'" by blast
from step[OF ‹X s'›] obtain s'''
where "silent_move^++ s' s'''" "X s''' ∨ s''' -τ→ ∞" by blast
from ‹silent_move⇧*⇧* s s'› show ?case
proof(cases rule: converse_rtranclpE[consumes 1, case_names refl step])
case refl
moreover from tranclpD[OF ‹silent_move^++ s' s'''›] obtain s''
where "silent_move s' s''" "silent_move^** s'' s'''" by blast
ultimately show ?thesis using ‹silent_move^** s'' s'''› ‹X s''' ∨ s''' -τ→ ∞›
by(auto intro: τdiverge_rtranclp_silent_move)
next
case (step S)
moreover from ‹silent_move⇧*⇧* S s'› ‹silent_move^++ s' s'''›
have "silent_move^** S s'''" by(rule rtranclp_trans[OF _ tranclp_into_rtranclp])
ultimately show ?thesis using ‹X s''' ∨ s''' -τ→ ∞› by(auto intro: τdiverge_rtranclp_silent_move)
qed
qed
qed
lemma τdiverge_trancl_measure_coinduct [consumes 2, case_names τdiverge]:
assumes major: "X s t" "wfP μ"
and step: "⋀s t. X s t ⟹ ∃s' t'. (μ t' t ∧ s' = s ∨ silent_move^++ s s') ∧ (X s' t' ∨ s' -τ→ ∞)"
shows "s -τ→ ∞"
proof -
{ fix s t
assume "X s t"
with ‹wfP μ› have "∃s' t'. silent_move^++ s s' ∧ (X s' t' ∨ s' -τ→ ∞)"
proof(induct arbitrary: s rule: wfP_induct[consumes 1])
case (1 t)
hence IH: "⋀s' t'. ⟦ μ t' t; X s' t' ⟧ ⟹
∃s'' t''. silent_move^++ s' s'' ∧ (X s'' t'' ∨ s'' -τ→ ∞)" by blast
from step[OF ‹X s t›] obtain s' t'
where "μ t' t ∧ s' = s ∨ silent_move⇧+⇧+ s s'" "X s' t' ∨ s' -τ→ ∞" by blast
from ‹μ t' t ∧ s' = s ∨ silent_move⇧+⇧+ s s'› show ?case
proof
assume "μ t' t ∧ s' = s"
hence "μ t' t" and [simp]: "s' = s" by simp_all
from ‹X s' t' ∨ s' -τ→ ∞› show ?thesis
proof
assume "X s' t'"
from IH[OF ‹μ t' t› this] show ?thesis by simp
next
assume "s' -τ→ ∞" thus ?thesis
by cases(auto simp add: silent_move_iff)
qed
next
assume "silent_move⇧+⇧+ s s'"
thus ?thesis using ‹X s' t' ∨ s' -τ→ ∞› by blast
qed
qed }
note X = this
from ‹X s t› have "∃t. X s t" ..
thus ?thesis
proof(coinduct rule: τdiverge_trancl_coinduct)
case (τdiverge s)
then obtain t where "X s t" ..
from X[OF this] show ?case by blast
qed
qed
lemma τinf_step2τinf_step_table_LNil [simp]: "τinf_step2τinf_step_table s LNil = LNil"
by(simp add: τinf_step2τinf_step_table_def)
lemma τinf_step2τinf_step_table_LCons [simp]:
fixes s tl ss tls
defines "ss ≡ SOME (s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls→* ∞"
shows
"τinf_step2τinf_step_table s (LCons tl tls) =
LCons (s, fst ss, tl, snd ss) (τinf_step2τinf_step_table (snd ss) tls)"
by(simp add: ss_def τinf_step2τinf_step_table_def split_beta)
lemma lnull_τinf_step2τinf_step_table [simp]:
"lnull (τinf_step2τinf_step_table s tls) ⟷ lnull tls"
by(simp add: τinf_step2τinf_step_table_def)
lemma lhd_τinf_step2τinf_step_table [simp]:
"¬ lnull tls ⟹ lhd (τinf_step2τinf_step_table s tls) =
(let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
in (s, s', lhd tls, s''))"
unfolding τinf_step2τinf_step_table_def Let_def by simp
lemma ltl_τinf_step2τinf_step_table [simp]:
"¬ lnull tls ⟹ ltl (τinf_step2τinf_step_table s tls) =
(let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
in τinf_step2τinf_step_table s'' (ltl tls))"
unfolding τinf_step2τinf_step_table_def Let_def
by(simp add: split_beta)
lemma lmap_τinf_step2τinf_step_table: "lmap (fst ∘ snd ∘ snd) (τinf_step2τinf_step_table s tls) = tls"
by(coinduction arbitrary: s tls)(auto simp add: split_beta)
lemma τinf_step_into_τinf_step_table:
"s -τ-tls→* ∞ ⟹ s -τ-τinf_step2τinf_step_table s tls→*t ∞"
proof(coinduction arbitrary: s tls)
case (τinf_step_table s tls)
thus ?case
proof(cases)
case (τinf_step_Cons s' s'' tls' tl)
let ?ss = "SOME (s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls'→* ∞"
from τinf_step_Cons have tls: "tls = LCons tl tls'" and "s -τ→* s'" "s' -tl→ s''"
"¬ τmove s' tl s''" "s'' -τ-tls'→* ∞" by simp_all
hence "(λ(s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls'→* ∞) (s', s'')" by simp
hence "(λ(s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls'→* ∞) ?ss" by(rule someI)
with tls have ?τinf_step_table_Cons by auto
thus ?thesis ..
next
case τinf_step_Nil
then have ?τinf_step_table_Nil by simp
thus ?thesis ..
qed
qed
lemma τinf_step_imp_τinf_step_table:
assumes "s -τ-tls→* ∞"
shows "∃sstls. s -τ-sstls→*t ∞ ∧ tls = lmap (fst ∘ snd ∘ snd) sstls"
using τinf_step_into_τinf_step_table[OF assms]
by(auto simp only: lmap_τinf_step2τinf_step_table)
lemma τinf_step_table_into_τinf_step:
"s -τ-sstls→*t ∞ ⟹ s -τ-lmap (fst ∘ snd ∘ snd) sstls→* ∞"
proof(coinduction arbitrary: s sstls)
case (τinf_step s tls)
thus ?case by cases(auto simp add: o_def)
qed
lemma silent_move_fromI [intro]:
"⟦ silent_moves s0 s1; silent_move s1 s2 ⟧ ⟹ silent_move_from s0 s1 s2"
by(simp add: silent_move_from_def)
lemma silent_move_fromE [elim]:
assumes "silent_move_from s0 s1 s2"
obtains "silent_moves s0 s1" "silent_move s1 s2"
using assms by(auto simp add: silent_move_from_def)
lemma rtranclp_silent_move_from_imp_silent_moves:
assumes s'x: "silent_move⇧*⇧* s' x"
shows "(silent_move_from s')^** x z ⟹ silent_moves s' z"
by(induct rule: rtranclp_induct)(auto intro: s'x)
lemma τdiverge_not_wfP_silent_move_from:
assumes "s -τ→ ∞"
shows "¬ wfP (flip (silent_move_from s))"
proof
assume "wfP (flip (silent_move_from s))"
moreover define Q where "Q = {s'. silent_moves s s' ∧ s' -τ→ ∞}"
hence "s ∈ Q" using ‹s -τ→ ∞› by(auto)
ultimately have "∃z∈Q. ∀y. silent_move_from s z y ⟶ y ∉ Q"
unfolding wfP_eq_minimal flip_simps by blast
then obtain z where "z ∈ Q"
and min: "⋀y. silent_move_from s z y ⟹ y ∉ Q" by blast
from ‹z ∈ Q› have "silent_moves s z" "z -τ→ ∞" unfolding Q_def by auto
from ‹z -τ→ ∞› obtain y where "silent_move z y" "y -τ→ ∞" by cases auto
from ‹silent_moves s z› ‹silent_move z y› have "silent_move_from s z y" ..
hence "y ∉ Q" by(rule min)
moreover from ‹silent_moves s z› ‹silent_move z y› ‹y -τ→ ∞›
have "y ∈ Q" unfolding Q_def by auto
ultimately show False by contradiction
qed
lemma wfP_silent_move_from_unroll:
assumes wfPs': "⋀s'. s -τ→ s' ⟹ wfP (flip (silent_move_from s'))"
shows "wfP (flip (silent_move_from s))"
unfolding wfP_eq_minimal flip_conv
proof(intro allI impI)
fix Q and x :: 's
assume "x ∈ Q"
show "∃z∈Q. ∀y. silent_move_from s z y ⟶ y ∉ Q"
proof(cases "∃s'. s -τ→ s' ∧ (∃x'. silent_moves s' x' ∧ x' ∈ Q)")
case False
hence "∀y. silent_move_from s x y ⟶ ¬ y ∈ Q"
by(cases "x=s")(auto, blast elim: converse_rtranclpE intro: rtranclp.rtrancl_into_rtrancl)
with ‹x ∈ Q› show ?thesis by blast
next
case True
then obtain s' x' where "s -τ→ s'" and "silent_moves s' x'" and "x' ∈ Q"
by auto
from ‹s -τ→ s'› have "wfP (flip (silent_move_from s'))" by(rule wfPs')
from this ‹x' ∈ Q› obtain z where "z ∈ Q" and min: "⋀y. silent_move_from s' z y ⟹ ¬ y ∈ Q"
and "(silent_move_from s')^** x' z"
by (rule wfP_minimalE) (unfold flip_simps, blast)
{ fix y
assume "silent_move_from s z y"
with ‹(silent_move_from s')^** x' z› ‹silent_move^** s' x'›
have "silent_move_from s' z y"
by(blast intro: rtranclp_silent_move_from_imp_silent_moves)
hence "¬ y ∈ Q" by(rule min) }
with ‹z ∈ Q› show ?thesis by(auto simp add: intro!: bexI)
qed
qed
lemma not_wfP_silent_move_from_τdiverge:
assumes "¬ wfP (flip (silent_move_from s))"
shows "s -τ→ ∞"
using assms
proof(coinduct)
case (τdiverge s)
{ assume wfPs': "⋀s'. s -τ→ s' ⟹ wfP (flip (silent_move_from s'))"
hence "wfP (flip (silent_move_from s))" by(rule wfP_silent_move_from_unroll) }
with τdiverge have "∃s'. s -τ→ s' ∧ ¬ wfP (flip (silent_move_from s'))" by auto
thus ?case by blast
qed
lemma τdiverge_neq_wfP_silent_move_from:
"s -τ→ ∞ ≠ wfP (flip (silent_move_from s))"
by(auto intro: not_wfP_silent_move_from_τdiverge dest: τdiverge_not_wfP_silent_move_from)
lemma not_τdiverge_to_no_τmove:
assumes "¬ s -τ→ ∞"
shows "∃s'. s -τ→* s' ∧ (∀s''. ¬ s' -τ→ s'')"
proof -
define S where "S = s"
from ‹¬ τdiverge s› have "wfP (flip (silent_move_from S))" unfolding S_def
using τdiverge_neq_wfP_silent_move_from[of s] by simp
moreover have "silent_moves S s" unfolding S_def ..
ultimately show ?thesis
proof(induct rule: wfP_induct')
case (wfP s)
note IH = ‹⋀y. ⟦flip (silent_move_from S) y s; S -τ→* y ⟧
⟹ ∃s'. y -τ→* s' ∧ (∀s''. ¬ s' -τ→ s'')›
show ?case
proof(cases "∃s'. silent_move s s'")
case False thus ?thesis by auto
next
case True
then obtain s' where "s -τ→ s'" ..
with ‹S -τ→* s› have "flip (silent_move_from S) s' s"
unfolding flip_conv by(rule silent_move_fromI)
moreover from ‹S -τ→* s› ‹s -τ→ s'› have "S -τ→* s'" ..
ultimately have "∃s''. s' -τ→* s'' ∧ (∀s'''. ¬ s'' -τ→ s''')" by(rule IH)
then obtain s'' where "s' -τ→* s''" "∀s'''. ¬ s'' -τ→ s'''" by blast
from ‹s -τ→ s'› ‹s' -τ→* s''› have "s -τ→* s''" by(rule converse_rtranclp_into_rtranclp)
with ‹∀s'''. ¬ s'' -τ→ s'''› show ?thesis by blast
qed
qed
qed
lemma τdiverge_conv_τRuns:
"s -τ→ ∞ ⟷ s ⇓ TNil None"
by(auto intro: τRuns.Diverge elim: τRuns.cases)
lemma τinf_step_into_τRuns:
"s -τ-tls→* ∞ ⟹ s ⇓ tllist_of_llist None tls"
proof(coinduction arbitrary: s tls)
case (τRuns s tls')
thus ?case by cases(auto simp add: τdiverge_conv_τRuns)
qed
lemma τ_into_τRuns:
"⟦ s -τ→ s'; s' ⇓ tls ⟧ ⟹ s ⇓ tls"
by(blast elim: τRuns.cases intro: τRuns.intros τdiverge.intros converse_rtranclp_into_rtranclp)
lemma τrtrancl3p_into_τRuns:
assumes "s -τ-tls→* s'"
and "s' ⇓ tls'"
shows "s ⇓ lappendt (llist_of tls) tls'"
using assms
by induct(auto intro: τRuns.Proceed τ_into_τRuns)
lemma τRuns_table_into_τRuns:
"τRuns_table s stlsss ⟹ s ⇓ tmap fst id stlsss"
proof(coinduction arbitrary: s stlsss)
case (τRuns s tls)
thus ?case by cases(auto simp add: o_def id_def)
qed
definition τRuns2τRuns_table :: "'s ⇒ ('tl, 's option) tllist ⇒ ('tl × 's, 's option) tllist"
where
"τRuns2τRuns_table s tls = unfold_tllist
(λ(s, tls). is_TNil tls)
(λ(s, tls). terminal tls)
(λ(s, tls). (thd tls, SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls))
(λ(s, tls). (SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls, ttl tls))
(s, tls)"
lemma is_TNil_τRuns2τRuns_table [simp]:
"is_TNil (τRuns2τRuns_table s tls) ⟷ is_TNil tls"
thm unfold_tllist.disc
by(simp add: τRuns2τRuns_table_def)
lemma thd_τRuns2τRuns_table [simp]:
"¬ is_TNil tls ⟹
thd (τRuns2τRuns_table s tls) =
(thd tls, SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls)"
by(simp add: τRuns2τRuns_table_def)
lemma ttl_τRuns2τRuns_table [simp]:
"¬ is_TNil tls ⟹
ttl (τRuns2τRuns_table s tls) =
τRuns2τRuns_table (SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls) (ttl tls)"
by(simp add: τRuns2τRuns_table_def)
lemma terminal_τRuns2τRuns_table [simp]:
"is_TNil tls ⟹ terminal (τRuns2τRuns_table s tls) = terminal tls"
by(simp add: τRuns2τRuns_table_def)
lemma τRuns2τRuns_table_simps [simp, nitpick_simp]:
"τRuns2τRuns_table s (TNil so) = TNil so"
"⋀tl.
τRuns2τRuns_table s (TCons tl tls) =
(let s'' = SOME s''. ∃s'. s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' ⇓ tls
in TCons (tl, s'') (τRuns2τRuns_table s'' tls))"
apply(simp add: τRuns2τRuns_table_def)
apply(rule tllist.expand)
apply(simp_all)
done
lemma τRuns2τRuns_table_inverse:
"tmap fst id (τRuns2τRuns_table s tls) = tls"
by(coinduction arbitrary: s tls) auto
lemma τRuns_into_τRuns_table:
assumes "s ⇓ tls"
shows "∃stlsss. tls = tmap fst id stlsss ∧ τRuns_table s stlsss"
proof(intro exI conjI)
from assms show "τRuns_table s (τRuns2τRuns_table s tls)"
proof(coinduction arbitrary: s tls)
case (τRuns_table s tls)
thus ?case
proof cases
case (Terminate s')
hence ?Terminate by simp
thus ?thesis ..
next
case Diverge
hence ?Diverge by simp
thus ?thesis by simp
next
case (Proceed s' s'' tls' tl)
let ?P = "λs''. ∃s'. s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' ⇓ tls'"
from Proceed have "?P s''" by auto
hence "?P (Eps ?P)" by(rule someI)
hence ?Proceed using ‹tls = TCons tl tls'›
by(auto simp add: split_beta)
thus ?thesis by simp
qed
qed
qed(simp add: τRuns2τRuns_table_inverse)
lemma τRuns_lappendtE:
assumes "σ ⇓ lappendt tls tls'"
and "lfinite tls"
obtains σ' where "σ -τ-list_of tls→* σ'"
and "σ' ⇓ tls'"
proof(atomize_elim)
from ‹lfinite tls› ‹σ ⇓ lappendt tls tls'›
show "∃σ'. σ -τ-list_of tls→* σ' ∧ σ' ⇓ tls'"
proof(induct arbitrary: σ)
case lfinite_LNil thus ?case by(auto intro: τrtrancl3p_refl)
next
case (lfinite_LConsI tls tl)
from ‹σ ⇓ lappendt (LCons tl tls) tls'›
show ?case unfolding lappendt_LCons
proof(cases)
case (Proceed σ' σ'')
from ‹σ'' ⇓ lappendt tls tls' ⟹ ∃σ'''. σ'' -τ-list_of tls→* σ''' ∧ σ''' ⇓ tls'› ‹σ'' ⇓ lappendt tls tls'›
obtain σ''' where "σ'' -τ-list_of tls→* σ'''" "σ''' ⇓ tls'" by blast
from ‹σ' -tl→ σ''› ‹¬ τmove σ' tl σ''› ‹σ'' -τ-list_of tls→* σ'''›
have "σ' -τ-tl # list_of tls→* σ'''" by(rule τrtrancl3p_step)
with ‹σ -τ→* σ'› have "σ -τ-[] @ (tl # list_of tls)→* σ'''"
unfolding τrtrancl3p_Nil_eq_τmoves[symmetric] by(rule τrtrancl3p_trans)
with ‹lfinite tls› have "σ -τ-list_of (LCons tl tls)→* σ'''" by(simp add: list_of_LCons)
with ‹σ''' ⇓ tls'› show ?thesis by blast
qed
qed
qed
lemma τRuns_total:
"∃tls. σ ⇓ tls"
proof
let ?τhalt = "λσ σ'. σ -τ→* σ' ∧ (∀tl σ''. ¬ σ' -tl→ σ'')"
let ?τdiverge = "λσ. σ -τ→ ∞"
let ?proceed = "λσ (tl, σ''). ∃σ'. σ -τ→* σ' ∧ σ' -tl→ σ'' ∧ ¬ τmove σ' tl σ''"
define tls where "tls = unfold_tllist
(λσ. (∃σ'. ?τhalt σ σ') ∨ ?τdiverge σ)
(λσ. if ∃σ'. ?τhalt σ σ' then Some (SOME σ'. ?τhalt σ σ') else None)
(λσ. fst (SOME tlσ'. ?proceed σ tlσ'))
(λσ. snd (SOME tlσ'. ?proceed σ tlσ')) σ"
then show "σ ⇓ tls"
proof(coinduct σ tls rule: τRuns.coinduct)
case (τRuns σ tls)
show ?case
proof(cases "∃σ'. ?τhalt σ σ'")
case True
hence "?τhalt σ (SOME σ'. ?τhalt σ σ')" by(rule someI_ex)
hence ?Terminate using True unfolding τRuns by simp
thus ?thesis ..
next
case False
note τhalt = this
show ?thesis
proof(cases "?τdiverge σ")
case True
hence ?Diverge using False unfolding τRuns by simp
thus ?thesis by simp
next
case False
from not_τdiverge_to_no_τmove[OF this]
obtain σ' where σ_σ': "σ -τ→* σ'"
and no_τ: "⋀σ''. ¬ σ' -τ→ σ''" by blast
from σ_σ' τhalt obtain tl σ'' where "σ' -tl→ σ''" by auto
moreover with no_τ[of σ''] have "¬ τmove σ' tl σ''" by auto
ultimately have "?proceed σ (tl, σ'')" using σ_σ' by auto
hence "?proceed σ (SOME tlσ. ?proceed σ tlσ)" by(rule someI)
hence ?Proceed using False τhalt unfolding τRuns
by(subst unfold_tllist.code) fastforce
thus ?thesis by simp
qed
qed
qed
qed
lemma silent_move2_into_silent_move:
fixes tl
assumes "silent_move2 s tl s'"
shows "s -τ→ s'"
using assms by(auto simp add: silent_move2_def)
lemma silent_move_into_silent_move2:
assumes "s -τ→ s'"
shows "∃tl. silent_move2 s tl s'"
using assms by(auto simp add: silent_move2_def)
lemma silent_moves2_into_silent_moves:
assumes "silent_moves2 s tls s'"
shows "s -τ→* s'"
using assms
by(induct)(blast intro: silent_move2_into_silent_move rtranclp.rtrancl_into_rtrancl)+
lemma silent_moves_into_silent_moves2:
assumes "s -τ→* s'"
shows "∃tls. silent_moves2 s tls s'"
using assms
by(induct)(blast dest: silent_move_into_silent_move2 intro: rtrancl3p_step)+
lemma inf_step_silent_move2_into_τdiverge:
"trsys.inf_step silent_move2 s tls ⟹ s -τ→ ∞"
proof(coinduction arbitrary: s tls)
case (τdiverge s)
thus ?case
by(cases rule: trsys.inf_step.cases[consumes 1])(auto intro: silent_move2_into_silent_move)
qed
lemma τdiverge_into_inf_step_silent_move2:
assumes "s -τ→ ∞"
obtains tls where "trsys.inf_step silent_move2 s tls"
proof -
define tls where "tls = unfold_llist
(λ_. False)
(λs. fst (SOME (tl, s'). silent_move2 s tl s' ∧ s' -τ→ ∞))
(λs. snd (SOME (tl, s'). silent_move2 s tl s' ∧ s' -τ→ ∞))
s" (is "_ = ?tls s")
with assms have "s -τ→ ∞ ∧ tls = ?tls s" by simp
hence "trsys.inf_step silent_move2 s tls"
proof(coinduct rule: trsys.inf_step.coinduct[consumes 1, case_names inf_step, case_conclusion inf_step step])
case (inf_step s tls)
let ?P = "λ(tl, s'). silent_move2 s tl s' ∧ s' -τ→ ∞"
from inf_step obtain "s -τ→ ∞" and tls: "tls = ?tls s" ..
from ‹s -τ→ ∞› obtain s' where "s -τ→ s'" "s' -τ→ ∞" by cases
from ‹s -τ→ s'› obtain tl where "silent_move2 s tl s'"
by(blast dest: silent_move_into_silent_move2)
with ‹s' -τ→ ∞› have "?P (tl, s')" by simp
hence "?P (Eps ?P)" by(rule someI)
thus ?case using tls
by(subst (asm) unfold_llist.code)(auto)
qed
thus thesis by(rule that)
qed
lemma τRuns_into_τrtrancl3p:
assumes runs: "s ⇓ tlss"
and fin: "tfinite tlss"
and terminal: "terminal tlss = Some s'"
shows "τrtrancl3p s (list_of (llist_of_tllist tlss)) s'"
using fin runs terminal
proof(induct arbitrary: s rule: tfinite_induct)
case TNil thus ?case by cases(auto intro: silent_moves_into_τrtrancl3p)
next
case (TCons tl tlss)
from ‹s ⇓ TCons tl tlss› obtain s'' s'''
where step: "s -τ→* s''"
and step2: "s'' -tl→ s'''" "¬ τmove s'' tl s'''"
and "s''' ⇓ tlss" by cases
from ‹terminal (TCons tl tlss) = ⌊s'⌋› have "terminal tlss = ⌊s'⌋" by simp
with ‹s''' ⇓ tlss› have "s''' -τ-list_of (llist_of_tllist tlss)→* s'" by(rule TCons)
with step2 have "s'' -τ-tl # list_of (llist_of_tllist tlss)→* s'" by(rule τrtrancl3p_step)
with step have "s -τ-[] @ tl # list_of (llist_of_tllist tlss)→* s'"
by(rule τrtrancl3p_trans[OF silent_moves_into_τrtrancl3p])
thus ?case using ‹tfinite tlss› by simp
qed
lemma τRuns_terminal_stuck:
assumes Runs: "s ⇓ tlss"
and fin: "tfinite tlss"
and terminal: "terminal tlss = Some s'"
and proceed: "s' -tls→ s''"
shows False
using fin Runs terminal
proof(induct arbitrary: s rule: tfinite_induct)
case TNil thus ?case using proceed by cases auto
next
case TCons thus ?case by(fastforce elim: τRuns.cases)
qed
lemma Runs_table_silent_diverge:
"⟦ Runs_table s stlss; ∀(s, tl, s') ∈ lset stlss. τmove s tl s'; ¬ lfinite stlss ⟧
⟹ s -τ→ ∞"
proof(coinduction arbitrary: s stlss)
case (τdiverge s)
thus ?case by cases(auto 5 2)
qed
lemma Runs_table_silent_rtrancl:
assumes "lfinite stlss"
and "Runs_table s stlss"
and "∀(s, tl, s') ∈ lset stlss. τmove s tl s'"
shows "s -τ→* llast (LCons s (lmap (λ(s, tl, s'). s') stlss))" (is ?thesis1)
and "llast (LCons s (lmap (λ(s, tl, s'). s') stlss)) -tl'→ s'' ⟹ False" (is "PROP ?thesis2")
proof -
from assms have "?thesis1 ∧ (llast (LCons s (lmap (λ(s, tl, s'). s') stlss)) -tl'→ s'' ⟶ False)"
proof(induct arbitrary: s)
case lfinite_LNil thus ?case by(auto elim: Runs_table.cases)
next
case (lfinite_LConsI stlss stls)
from ‹Runs_table s (LCons stls stlss)›
obtain tl s' where [simp]: "stls = (s, tl, s')"
and "s -tl→ s'" and Run': "Runs_table s' stlss" by cases
from ‹∀(s, tl, s')∈lset (LCons stls stlss). τmove s tl s'›
have "τmove s tl s'" and silent': "∀(s, tl, s')∈lset stlss. τmove s tl s'" by simp_all
from ‹s -tl→ s'› ‹τmove s tl s'› have "s -τ→ s'" by auto
moreover from Run' silent'
have "s' -τ→* llast (LCons s' (lmap (λ(s, tl, s'). s') stlss)) ∧
(llast (LCons s' (lmap (λ(s, tl, s'). s') stlss)) -tl'→ s'' ⟶ False)"
by(rule lfinite_LConsI)
ultimately show ?case by(auto)
qed
thus ?thesis1 "PROP ?thesis2" by blast+
qed
lemma Runs_table_silent_lappendD:
fixes s stlss
defines "s' ≡ llast (LCons s (lmap (λ(s, tl, s'). s') stlss))"
assumes Runs: "Runs_table s (lappend stlss stlss')"
and fin: "lfinite stlss"
and silent: "∀(s, tl, s') ∈ lset stlss. τmove s tl s'"
shows "s -τ→* s'" (is ?thesis1)
and "Runs_table s' stlss'" (is ?thesis2)
and "stlss' ≠ LNil ⟹ s' = fst (lhd stlss')" (is "PROP ?thesis3")
proof -
from fin Runs silent
have "?thesis1 ∧ ?thesis2 ∧ (stlss' ≠ LNil ⟶ s' = fst (lhd stlss'))"
unfolding s'_def
proof(induct arbitrary: s)
case lfinite_LNil thus ?case
by(auto simp add: neq_LNil_conv Runs_table_simps)
next
case lfinite_LConsI thus ?case
by(clarsimp simp add: neq_LNil_conv Runs_table_simps)(blast intro: converse_rtranclp_into_rtranclp)
qed
thus ?thesis1 ?thesis2 "PROP ?thesis3" by simp_all
qed
lemma Runs_table_into_τRuns:
fixes s stlss
defines "tls ≡ tmap (λ(s, tl, s'). tl) id (tfilter None (λ(s, tl, s'). ¬ τmove s tl s') (tllist_of_llist (Some (llast (LCons s (lmap (λ(s, tl, s'). s') stlss)))) stlss))"
(is "_ ≡ ?conv s stlss")
assumes "Runs_table s stlss"
shows "τRuns s tls"
using assms
proof(coinduction arbitrary: s tls stlss)
case (τRuns s tls stlss)
note tls = ‹tls = ?conv s stlss›
and Run = ‹Runs_table s stlss›
show ?case
proof(cases tls)
case [simp]: (TNil so)
from tls
have silent: "∀(s, tl, s') ∈ lset stlss. τmove s tl s'"
by(auto simp add: TNil_eq_tmap_conv tfilter_empty_conv)
show ?thesis
proof(cases "lfinite stlss")
case False
with Run silent have "s -τ→ ∞" by(rule Runs_table_silent_diverge)
hence ?Diverge using False tls by(simp add: TNil_eq_tmap_conv tfilter_empty_conv)
thus ?thesis by simp
next
case True
with Runs_table_silent_rtrancl[OF this Run silent]
have ?Terminate using tls
by(auto simp add: TNil_eq_tmap_conv tfilter_empty_conv terminal_tllist_of_llist split_def)
thus ?thesis by simp
qed
next
case [simp]: (TCons tl tls')
from tls obtain s' s'' stlss'
where tl': "tfilter None (λ(s, tl, s'). ¬ τmove s tl s') (tllist_of_llist ⌊llast (LCons s (lmap (λ(s, tl, s'). s') stlss))⌋ stlss) = TCons (s', tl, s'') stlss'"
and tls': "tls' = tmap (λ(s, tl, s'). tl) id stlss'"
by(simp add: TCons_eq_tmap_conv split_def id_def split_paired_Ex) blast
from tfilter_eq_TConsD[OF tl']
obtain stlsτ rest
where stlss_eq: "tllist_of_llist ⌊llast (LCons s (lmap (λ(s, tl, s'). s') stlss))⌋ stlss = lappendt stlsτ (TCons (s', tl, s'') rest)"
and fin: "lfinite stlsτ"
and silent: "∀(s, tl, s')∈lset stlsτ. τmove s tl s'"
and "¬ τmove s' tl s''"
and stlss': "stlss' = tfilter None (λ(s, tl, s'). ¬ τmove s tl s') rest"
by(auto simp add: split_def)
from stlss_eq fin obtain rest'
where stlss: "stlss = lappend stlsτ rest'"
and rest': "tllist_of_llist ⌊llast (LCons s (lmap (λ(s, tl, s'). s') stlss))⌋ rest' = TCons (s', tl, s'') rest"
unfolding tllist_of_llist_eq_lappendt_conv by auto
hence "rest' ≠ LNil" by clarsimp
from Run[unfolded stlss] fin silent
have "s -τ→* llast (LCons s (lmap (λ(s, tl, s'). s') stlsτ))"
and "Runs_table (llast (LCons s (lmap (λ(s, tl, s'). s') stlsτ))) rest'"
and "llast (LCons s (lmap (λ(s, tl, s'). s') stlsτ)) = fst (lhd rest')"
by(rule Runs_table_silent_lappendD)+(simp add: ‹rest' ≠ LNil›)
moreover with rest' ‹rest' ≠ LNil› stlss fin obtain rest''
where rest': "rest' = LCons (s', tl, s'') rest''"
and rest: "rest = tllist_of_llist ⌊llast (LCons s'' (lmap (λ(s, tl, s'). s') rest''))⌋ rest''"
by(clarsimp simp add: neq_LNil_conv llast_LCons lmap_lappend_distrib)
ultimately have "s -τ→* s'" "s' -tl→ s''" "Runs_table s'' rest''"
by(simp_all add: Runs_table_simps)
hence ?Proceed using ‹¬ τmove s' tl s''› tls' stlss' rest
by(auto simp add: id_def)
thus ?thesis by simp
qed
qed
lemma τRuns_table2_into_τRuns:
"τRuns_table2 s tlsstlss
⟹ s ⇓ tmap (λ(tls, s', tl, s''). tl) (λx. case x of Inl (tls, s') ⇒ Some s' | Inr _ ⇒ None) tlsstlss"
proof(coinduction arbitrary: s tlsstlss)
case (τRuns s tlsstlss)
thus ?case by cases(auto intro: silent_moves2_into_silent_moves inf_step_silent_move2_into_τdiverge)
qed
lemma τRuns_into_τRuns_table2:
assumes "s ⇓ tls"
obtains tlsstlss
where "τRuns_table2 s tlsstlss"
and "tls = tmap (λ(tls, s', tl, s''). tl) (λx. case x of Inl (tls, s') ⇒ Some s' | Inr _ ⇒ None) tlsstlss"
proof -
let ?terminal = "λs tls. case terminal tls of
None ⇒ Inr (SOME tls'. trsys.inf_step silent_move2 s tls')
| Some s' ⇒ let tls' = SOME tls'. silent_moves2 s tls' s' in Inl (tls', s')"
let ?P = "λs tls (tls'', s', s''). silent_moves2 s tls'' s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls"
define tlsstlss where "tlsstlss s tls = unfold_tllist
(λ(s, tls). is_TNil tls)
(λ(s, tls). ?terminal s tls)
(λ(s, tls). let (tls'', s', s'') = Eps (?P s tls) in (tls'', s', thd tls, s''))
(λ(s, tls). let (tls'', s', s'') = Eps (?P s tls) in (s'', ttl tls))
(s, tls)"
for s tls
have [simp]:
"⋀s tls. is_TNil (tlsstlss s tls) ⟷ is_TNil tls"
"⋀s tls. is_TNil tls ⟹ terminal (tlsstlss s tls) = ?terminal s tls"
"⋀s tls. ¬ is_TNil tls ⟹ thd (tlsstlss s tls) = (let (tls'', s', s'') = Eps (?P s tls) in (tls'', s', thd tls, s''))"
"⋀s tls. ¬ is_TNil tls ⟹ ttl (tlsstlss s tls) = (let (tls'', s', s'') = Eps (?P s tls) in tlsstlss s'' (ttl tls))"
by(simp_all add: tlsstlss_def split_beta)
have [simp]:
"⋀s. tlsstlss s (TNil None) = TNil (Inr (SOME tls'. trsys.inf_step silent_move2 s tls'))"
"⋀s s'. tlsstlss s (TNil (Some s')) = TNil (Inl (SOME tls'. silent_moves2 s tls' s', s'))"
unfolding tlsstlss_def by simp_all
let ?conv = "tmap (λ(tls, s', tl, s''). tl) (λx. case x of Inl (tls, s') ⇒ Some s' | Inr _ ⇒ None)"
from assms have "τRuns_table2 s (tlsstlss s tls)"
proof(coinduction arbitrary: s tls)
case (τRuns_table2 s tls)
thus ?case
proof(cases)
case (Terminate s')
let ?P = "λtls'. silent_moves2 s tls' s'"
from ‹s -τ→* s'› obtain tls' where "?P tls'" by(blast dest: silent_moves_into_silent_moves2)
hence "?P (Eps ?P)" by(rule someI)
with Terminate have ?Terminate by auto
thus ?thesis by simp
next
case Diverge
let ?P = "λtls'. trsys.inf_step silent_move2 s tls'"
from ‹s -τ→ ∞› obtain tls' where "?P tls'" by(rule τdiverge_into_inf_step_silent_move2)
hence "?P (Eps ?P)" by(rule someI)
hence ?Diverge using ‹tls = TNil None› by simp
thus ?thesis by simp
next
case (Proceed s' s'' tls' tl)
from ‹s -τ→* s'› obtain tls'' where "silent_moves2 s tls'' s'"
by(blast dest: silent_moves_into_silent_moves2)
with Proceed have "?P s tls (tls'', s', s'')" by simp
hence "?P s tls (Eps (?P s tls))" by(rule someI)
hence ?Proceed using Proceed unfolding tlsstlss_def
by(subst unfold_tllist.code)(auto simp add: split_def)
thus ?thesis by simp
qed
qed
moreover
from assms have "tls = ?conv (tlsstlss s tls)"
proof(coinduction arbitrary: s tls)
case (Eq_tllist s tls)
thus ?case
proof(cases)
case (Proceed s' s'' tls' tl)
from ‹s -τ→* s'› obtain tls'' where "silent_moves2 s tls'' s'"
by(blast dest: silent_moves_into_silent_moves2)
with Proceed have "?P s tls (tls'', s', s'')" by simp
hence "?P s tls (Eps (?P s tls))" by(rule someI)
thus ?thesis using ‹tls = TCons tl tls'› by auto
qed auto
qed
ultimately show thesis by(rule that)
qed
lemma τRuns_table2_into_Runs:
assumes "τRuns_table2 s tlsstlss"
shows "Runs s (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist tlsstlss)) (LCons (case terminal tlsstlss of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil)))"
(is "Runs _ (?conv tlsstlss)")
using assms
proof(coinduction arbitrary: s tlsstlss)
case (Runs s tlsstlss)
thus ?case
proof(cases)
case (Terminate tls' s')
from ‹silent_moves2 s tls' s'› show ?thesis
proof(cases rule: rtrancl3p_converseE)
case refl
hence ?Stuck using Terminate by simp
thus ?thesis ..
next
case (step tls'' tl s'')
from ‹silent_moves2 s'' tls'' s'› ‹⋀tl s''. ¬ s' -tl→ s''›
have "τRuns_table2 s'' (TNil (Inl (tls'', s')))" ..
with ‹tls' = tl # tls''› ‹silent_move2 s tl s''› ‹tlsstlss = TNil (Inl (tls', s'))›
have ?Step by(auto simp add: silent_move2_def intro!: exI)
thus ?thesis ..
qed
next
case (Diverge tls')
from ‹trsys.inf_step silent_move2 s tls'›
obtain tl tls'' s' where "silent_move2 s tl s'"
and "tls' = LCons tl tls''" "trsys.inf_step silent_move2 s' tls''"
by(cases rule: trsys.inf_step.cases[consumes 1]) auto
from ‹trsys.inf_step silent_move2 s' tls''›
have "τRuns_table2 s' (TNil (Inr tls''))" ..
hence ?Step using ‹tlsstlss = TNil (Inr tls')› ‹tls' = LCons tl tls''› ‹silent_move2 s tl s'›
by(auto simp add: silent_move2_def intro!: exI)
thus ?thesis ..
next
case (Proceed tls' s' s'' tlsstlss' tl)
from ‹silent_moves2 s tls' s'› have ?Step
proof(cases rule: rtrancl3p_converseE)
case refl with Proceed show ?thesis by auto
next
case (step tls'' tl' s''')
from ‹silent_moves2 s''' tls'' s'› ‹s' -tl→ s''› ‹¬ τmove s' tl s''› ‹τRuns_table2 s'' tlsstlss'›
have "τRuns_table2 s''' (TCons (tls'', s', tl, s'') tlsstlss')" ..
with ‹tls' = tl' # tls''› ‹silent_move2 s tl' s'''› ‹tlsstlss = TCons (tls', s', tl, s'') tlsstlss'›
show ?thesis by(auto simp add: silent_move2_def intro!: exI)
qed
thus ?thesis ..
qed
qed
lemma τRuns_table2_silentsD:
fixes tl
assumes Runs: "τRuns_table2 s tlsstlss"
and tset: "(tls, s', tl', s'') ∈ tset tlsstlss"
and set: "tl ∈ set tls"
shows "∃s''' s''''. silent_move2 s''' tl s''''"
using tset Runs
proof(induct arbitrary: s rule: tset_induct)
case (find tlsstlss')
from ‹τRuns_table2 s (TCons (tls, s', tl', s'') tlsstlss')›
have "silent_moves2 s tls s'" by cases
thus ?case using set by induct auto
next
case step thus ?case by(auto simp add: τRuns_table2_simps)
qed
lemma τRuns_table2_terminal_silentsD:
assumes Runs: "τRuns_table2 s tlsstlss"
and fin: "lfinite (llist_of_tllist tlsstlss)"
and terminal: "terminal tlsstlss = Inl (tls, s'')"
shows "∃s'. silent_moves2 s' tls s''"
using fin Runs terminal
proof(induct "llist_of_tllist tlsstlss" arbitrary: tlsstlss s)
case lfinite_LNil thus ?case
by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
next
case (lfinite_LConsI xs tlsstls)
thus ?case by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
qed
lemma τRuns_table2_terminal_inf_stepD:
assumes Runs: "τRuns_table2 s tlsstlss"
and fin: "lfinite (llist_of_tllist tlsstlss)"
and terminal: "terminal tlsstlss = Inr tls"
shows "∃s'. trsys.inf_step silent_move2 s' tls"
using fin Runs terminal
proof(induct "llist_of_tllist tlsstlss" arbitrary: s tlsstlss)
case lfinite_LNil thus ?case
by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
next
case (lfinite_LConsI xs tlsstls)
thus ?case by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
qed
lemma τRuns_table2_lappendtD:
assumes Runs: "τRuns_table2 s (lappendt tlsstlss tlsstlss')"
and fin: "lfinite tlsstlss"
shows "∃s'. τRuns_table2 s' tlsstlss'"
using fin Runs
by(induct arbitrary: s)(auto simp add: τRuns_table2_simps)
end
lemma τmoves_False: "τtrsys.silent_move r (λs ta s'. False) = (λs s'. False)"
by(auto simp add: τtrsys.silent_move_iff)
lemma τrtrancl3p_False_eq_rtrancl3p: "τtrsys.τrtrancl3p r (λs tl s'. False) = rtrancl3p r"
proof(intro ext iffI)
fix s tls s'
assume "τtrsys.τrtrancl3p r (λs tl s'. False) s tls s'"
thus "rtrancl3p r s tls s'" by(rule τtrsys.τrtrancl3p.induct)(blast intro: rtrancl3p_step_converse)+
next
fix s tls s'
assume "rtrancl3p r s tls s'"
thus "τtrsys.τrtrancl3p r (λs tl s'. False) s tls s'"
by(induct rule: rtrancl3p_converse_induct)(auto intro: τtrsys.τrtrancl3p.intros)
qed
lemma τdiverge_empty_τmove:
"τtrsys.τdiverge r (λs ta s'. False) = (λs. False)"
by(auto intro!: ext elim: τtrsys.τdiverge.cases τtrsys.silent_move.cases)
end