Theory Simulation_Graphs_Certification
section ‹Certification Theorems Based on Subsumption and Simulation Graphs›
theory Simulation_Graphs_Certification
imports Munta_Base.Subsumption_Graphs Timed_Automata.Simulation_Graphs "HOL-Eisbach.Eisbach"
begin
subsection ‹Misc›
lemma finite_ImageI:
assumes "finite S" "∀a ∈ S. finite {b. (a, b) ∈ R}"
shows "finite (R `` S)"
proof -
have "R `` S ⊆ (⋃ x ∈ S. {y. (x, y) ∈ R})"
unfolding Image_def by auto
also have "finite …"
using assms by auto
finally show ?thesis .
qed
lemma (in Graph_Defs) steps_two_iff[simp]:
"steps [a, b] ⟷ E a b"
by (auto elim!: steps.cases)
lemma (in Graph_Defs) steps_Cons_two_iff:
"steps (a # b # as) ⟷ E a b ∧ steps (b # as)"
by (auto elim: steps.cases)
subsection ‹Certifying Cycle-Freeness in Graphs›
locale Contract1 =
fixes A B :: "'a ⇒ 'a ⇒ bool" and G :: "'a ⇒ bool"
begin
definition "E a b ≡ A a b ∧ G a ∨ ¬ G a ∧ B a b ∧ G b"
definition "E' a b ≡ G a ∧ G b ∧ (A a b ∨ (∃ c. A a c ∧ ¬ G c ∧ B c b))"
sublocale E: Graph_Defs E .
sublocale E': Graph_Defs E' .
lemma steps_contract:
assumes "E.steps (a # xs @ [b])" "G a" "G b"
shows "∃as. E'.steps (a # as @ [b])"
using assms
proof (induction xs arbitrary: a rule: length_induct)
case prems: (1 xs)
show ?case
proof (cases xs)
case Nil
with prems show ?thesis
apply (inst_existentials "[] :: 'a list")
apply simp
apply (auto simp: E_def E'_def )
done
next
case (Cons y ys)
with ‹E.steps (a # xs @ [b])› have "E a y" "E.steps (y # ys @ [b])"
by (cases, auto)+
from this(1) ‹G a› consider (graph) "A a y" "G a" "G y" | (non_graph) "A a y" "G a" "¬ G y"
unfolding E_def by auto
then show ?thesis
proof cases
case graph
with ‹E.steps (y # ys @ [b])› prems(1) ‹G b› obtain as where "E'.steps (y # as @ [b])"
unfolding ‹xs = _› by auto
also from graph have "E' a y"
unfolding E'_def by auto
finally (E'.steps.Cons[rotated]) show ?thesis
by (inst_existentials "y # as") auto
next
case non_graph
show ?thesis
proof (cases ys)
case Nil
with ‹E.steps (y # ys @ [b])› have "E y b"
by auto
with ‹¬ G y› have "B y b" "G b"
unfolding E_def by auto
with ‹A a y› ‹G a› ‹¬ G y› have "E'.steps [a, b]"
by (auto simp: E'_def)
then show ?thesis
by (inst_existentials "[] :: 'a list") auto
next
case (Cons z zs)
with ‹E.steps (y # ys @ [b])› have "E y z" "E.steps (z # zs @ [b])"
by (auto simp: E.steps_Cons_two_iff)
with ‹¬ G y› have "B y z" "G z"
unfolding E_def by auto
with ‹A a y› ‹G a› ‹¬ G y› have "E' a z"
by (auto simp: E'_def)
also from ‹E.steps (z # zs @ [b])› prems(1) obtain as where "E'.steps (z # as @ [b])"
unfolding ‹xs = _› ‹ys = _› using ‹G z› ‹G b› by force
finally (E'.steps.Cons) show ?thesis
by (inst_existentials "z # as") auto
qed
qed
qed
qed
lemma E'_G[dest, intro]:
assumes "E' x y"
shows "G x" "G y"
using assms unfolding E'_def by auto
lemma E'_steps_G:
assumes "E'.steps (x # xs)" "xs ≠ []"
shows "G x"
proof -
from ‹E'.steps _› ‹xs ≠ []› obtain y where "E' x y"
by (auto elim: E'.steps.cases)
then show ?thesis
by auto
qed
lemma E_E'_cycle:
assumes "E⇧+⇧+ x x" "G x"
shows "E'⇧+⇧+ x x"
proof -
from ‹E⇧+⇧+ x x› obtain xs where "E.steps (x # xs @ [x])"
including graph_automation by auto
with ‹G x› obtain ys where "E'.steps (x # ys @ [x])"
by (auto dest: steps_contract)
then show ?thesis
using E'.reaches1_steps_iff by blast
qed
text ‹This can be proved by rotating the cycle if ‹¬ G x››
lemma
assumes "E⇧*⇧* s x" "E⇧+⇧+ x x" "G s"
shows "E'⇧*⇧* s x ∧ E'⇧+⇧+ x x"
proof -
show ?thesis
proof (cases "G x")
case True
with ‹E⇧+⇧+ x x› have "E'⇧+⇧+ x x"
by (auto dest: E_E'_cycle)
from ‹E⇧*⇧* s x› consider (refl) "s = x" | (steps) "E⇧+⇧+ s x"
by cases (auto simp: E.reaches1_reaches_iff2)
then show ?thesis
proof cases
case refl
with ‹E'⇧+⇧+ x x› show ?thesis
by simp
next
case steps
then obtain xs where "E.steps (s # xs @ [x])"
including graph_automation by auto
with ‹G s› ‹G x› obtain ys where "E'.steps (s # ys @ [x])"
by (auto dest: steps_contract)
with ‹E'⇧+⇧+ x x› show ?thesis
including graph_automation by auto
next
oops
text ‹Certifying cycle-freeness with a topological ordering of graph components›
context
fixes f :: "'a ⇒ nat" and F :: "'a ⇒ bool"
assumes f_topo1: "∀a b. G a ∧ A a b ∧ G b ⟶ (if F a then f a < f b else f a ≤ f b)"
and f_topo2:
"∀a b c. G a ∧ A a b ∧ ¬ G b ∧ G c ∧ B b c ⟶ (if F a then f a < f c else f a ≤ f c)"
begin
lemma f_forward:
assumes "E' a b"
shows "f a ≤ f b"
using assms f_topo1 f_topo2 unfolding E'_def by (cases "F a") (auto simp: less_imp_le)
lemma f_strict:
assumes "E' a b" "F a"
shows "f a < f b"
using assms f_topo1 f_topo2 unfolding E'_def by (auto simp: less_imp_le)
text ‹We do not even need this property any more.›
lemma no_trivial_lasso:
assumes "F a" "G a" "E' a a"
shows False
using assms f_topo1 f_topo2 unfolding E'_def by (meson less_irrefl)
lemma reaches_f_mono:
assumes "E'⇧*⇧* a b"
shows "f a ≤ f b"
using assms by induction (auto intro: f_forward order.trans)
theorem no_accepting_cycle:
assumes "E'⇧+⇧+ x x"
shows "¬ F x"
proof (rule ccontr, unfold not_not)
assume "F x"
from ‹E'⇧+⇧+ x x› obtain y where "E' x y" "E'⇧*⇧* y x"
including graph_automation_aggressive by auto
from ‹E' x y› ‹F x› have "f x < f y"
by (rule f_strict)
moreover from ‹E'⇧*⇧* y x› have "f y ≤ f x"
by (rule reaches_f_mono)
ultimately show False
by simp
qed
end
end
locale Contract =
fixes E :: "'a ⇒ 'a ⇒ bool"
fixes f :: "'a ⇒ nat" and F :: "'a ⇒ bool"
assumes f_topo:
"∀a b. E a b ⟶ (if F a then f a < f b else f a ≤ f b)"
begin
sublocale E: Graph_Defs E .
lemma f_forward:
assumes "E a b"
shows "f a ≤ f b"
using assms f_topo by (cases "F a") (auto simp: less_imp_le)
lemma f_strict:
assumes "E a b" "F a"
shows "f a < f b"
using assms f_topo by (auto simp: less_imp_le)
text ‹We do not even need this property any more.›
lemma no_trivial_lasso:
assumes "F a" "G a" "E a a"
shows False
using assms f_topo by (meson less_irrefl)
lemma reaches_f_mono:
assumes "E⇧*⇧* a b"
shows "f a ≤ f b"
using assms by induction (auto intro: f_forward order.trans)
theorem no_accepting_cycle:
assumes "E⇧+⇧+ x x"
shows "¬ F x"
proof (rule ccontr, unfold not_not)
assume "F x"
from ‹E⇧+⇧+ x x› obtain y where "E x y" "E⇧*⇧* y x"
including graph_automation_aggressive by auto
from ‹E x y› ‹F x› have "f x < f y"
by (rule f_strict)
moreover from ‹E⇧*⇧* y x› have "f y ≤ f x"
by (rule reaches_f_mono)
ultimately show False
by simp
qed
end
locale Contract2 =
fixes A B :: "'a ⇒ 'a ⇒ bool" and G :: "'a ⇒ bool"
fixes f :: "'a ⇒ nat" and F :: "'a ⇒ bool"
assumes f_topo:
"∀a b c. G a ∧ A a b ∧ G c ∧ B b c ⟶ (if F a then f a < f c else f a ≤ f c)"
begin
definition "E a c ≡ ∃b. G a ∧ G c ∧ A a b ∧ B b c"
sublocale Contract E f F
by standard (auto simp: E_def f_topo)
theorem no_accepting_cycle:
assumes "E⇧+⇧+ x x"
shows "¬ F x"
using assms by (rule no_accepting_cycle)
end
subsection ‹Reachability and Over-approximation›
context
fixes E :: "'a ⇒ 'a ⇒ bool" and P :: "'a ⇒ bool"
and less_eq :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50) and less (infix "≺" 50)
assumes preorder: "class.preorder less_eq less"
assumes mono: "a ≼ b ⟹ E a a' ⟹ P a ⟹ P b ⟹ ∃ b'. E b b' ∧ a' ≼ b'"
assumes invariant: "P a ⟹ E a a' ⟹ P b"
begin
interpretation preorder less_eq less
by (rule preorder)
interpretation Simulation_Invariant
E "λ x y. ∃ z. z ≼ y ∧ E x z ∧ P z" "(≼)" P P
by standard (auto 0 4 intro: invariant dest: mono)
context
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "F a ⟹ a ≼ b ⟹ F b"
begin
corollary reachability_correct:
"∄ s'. A.reaches a s' ∧ F s'" if "∄ s'. B.reaches b s' ∧ F s'" "a ≼ b" "P a" "P b"
using that by (auto dest!: simulation_reaches)
end
end
context Simulation_Invariant
begin
context
fixes F :: "'a ⇒ bool" and F' :: "'b ⇒ bool"
assumes F_mono[intro]: "F a ⟹ a ∼ b ⟹ F' b"
begin
corollary reachability_correct:
"∄ s'. A.reaches a s' ∧ F s'" if "∄ s'. B.reaches b s' ∧ F' s'" "a ∼ b" "PA a" "PB b"
using that by (auto dest!: simulation_reaches)
end
end
subsection ‹Invariants for Un-reachability›
locale Unreachability_Invariant0 = Subsumption_Graph_Pre_Defs + preorder less_eq less +
fixes S :: "'a set" and SE :: "'a ⇒ 'a ⇒ bool"
assumes mono:
"s ≼ s' ⟹ s → t ⟹ ∃ t'. t ≼ t' ∧ s' → t'"
assumes S_E_subsumed: "s ∈ S ⟹ s → t ⟹ ∃ t' ∈ S. SE t t'"
assumes subsumptions_subsume: "SE s t ⟹ s ≼ t"
begin
definition E' where
"E' s t ≡ ∃s'. E s s' ∧ SE s' t ∧ t ∈ S"
sublocale G: Graph_Defs E' .
interpretation Simulation_Invariant E E' "(≼)" "λs. True" "λx. x ∈ S"
proof standard
fix a b a' :: ‹'a›
assume ‹a → b› ‹a' ∈ S› ‹a ≼ a'›
with mono[OF ‹a ≼ a'› ‹a → b›] obtain b' where "b ≼ b'" "a' → b'"
by auto
with S_E_subsumed[OF ‹a' ∈ S›] obtain c where "c ∈ S" "SE b' c"
by auto
with ‹a' → b'› have "E' a' c"
unfolding E'_def by auto
with ‹b ≼ b'› ‹SE b' c› subsumptions_subsume show ‹∃b'. E' a' b' ∧ b ≼ b'›
by (blast intro: order_trans)
qed (auto simp: E'_def)
context
fixes s⇩0 s⇩0'
assumes "s⇩0 ≼ s⇩0'" "s⇩0' ∈ S"
begin
lemma run_subsumed:
assumes "run (s⇩0 ## xs)"
obtains ys where "G.run (s⇩0' ## ys)" "stream_all2 (≼) xs ys" "pred_stream (λx. x ∈ S) ys"
proof -
from ‹s⇩0 ≼ _› ‹s⇩0' ∈ S› have "equiv' s⇩0 s⇩0'"
unfolding equiv'_def by auto
with assms show ?thesis
by - (drule simulation_run, auto
dest: PB_invariant.invariant_run elim: stream_all2_weaken intro!: that simp: equiv'_def)
qed
context
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "reaches s⇩0 a ⟹ F a ⟹ a ≼ b ⟹ b ∈ S ⟹ F b"
begin
corollary final_unreachable:
"∄ s'. reaches s⇩0 s' ∧ F s'" if "∀ s' ∈ S. ¬ F s'"
using ‹s⇩0 ≼ s⇩0'› ‹s⇩0' ∈ S› simulation_reaches that by blast
lemma buechi_run_lasso:
assumes "finite S" "run (s⇩0 ## xs)" "alw (ev (holds F)) (s⇩0 ## xs)"
obtains s where "G.reaches s⇩0' s" "G.reaches1 s s" "F s"
proof -
interpret Finite_Graph E' s⇩0'
by (standard, rule finite_subset[OF _ assms(1)])
(auto intro: PB_invariant.invariant_reaches ‹s⇩0' ∈ S›)
from run_subsumed[OF assms(2)] obtain ys where ys:
"G.run (s⇩0' ## ys)" "stream_all2 (≼) xs ys" "pred_stream (λx. x ∈ S) ys" .
moreover from ‹run _› have "pred_stream (reaches s⇩0) xs"
using run_reachable by blast
ultimately have "stream_all2 (λx y. x ≼ y ∧ reaches s⇩0 x ∧ y ∈ S) xs ys"
by (smt stream.pred_set stream.rel_mono_strong)
with assms(3) ‹s⇩0 ≼ _› ‹s⇩0' ∈ S› have "alw (ev (holds F)) (s⇩0' ## ys)"
by (elim alw_ev_lockstep) (erule stream.rel_intros[rotated], auto)
from buechi_run_lasso[OF ys(1) this] show ?thesis
using that .
qed
end
end
end
locale Unreachability_Invariant1 = Subsumption_Graph_Pre_Defs + preorder less_eq less +
fixes I and SE :: "'a ⇒ 'a ⇒ bool" and P
assumes mono:
"s ≼ s' ⟹ s → t ⟹ P s ⟹ P s' ⟹ ∃ t'. t ≼ t' ∧ s' → t'"
assumes S_E_subsumed: "I s ⟹ s → t ⟹ ∃ t'. I t' ∧ SE t t'"
assumes subsumptions_subsume: "SE s t ⟹ s ≼ t"
assumes I_P[intro]: "I s ⟹ P s"
assumes P_invariant: "P s ⟹ s → s' ⟹ P s'"
begin
context
assumes subsumes_P: "⋀s s'. s ≼ s' ⟹ P s'"
begin
interpretation E: Unreachability_Invariant0
where E = "λ x y. E x y ∧ P y"
and S = "{s. I s}"
apply standard
subgoal for s s' t
using subsumes_P mono by blast
using S_E_subsumed subsumptions_subsume by auto
end
text ‹Alternative for defining the simulating transition system.
Does not need the invariant at the tip of the subsumption but requires us to use
‹Simulation› instead of ‹Simulation_Invariant›.›
definition E' where
"E' s t ≡ ∃s'. E s s' ∧ SE s' t ∧ I t"
sublocale G: Graph_Defs E' .
interpretation Simulation_Invariant E E' "(≼)" P I
proof standard
fix a b a' :: ‹'a›
assume ‹a → b› ‹P a› ‹I a'› ‹a ≼ a'›
with mono[OF ‹a ≼ a'› ‹a → b›] obtain b' where "b ≼ b'" "a' → b'"
by auto
with S_E_subsumed[OF ‹I a'›] obtain c where "I c" "SE b' c"
by auto
with ‹a' → b'› have "E' a' c"
unfolding E'_def by auto
with ‹b ≼ b'› ‹SE b' c› subsumptions_subsume show ‹∃b'. E' a' b' ∧ b ≼ b'›
by (blast intro: order_trans)
qed (auto simp: E'_def P_invariant)
context
fixes s⇩0 s⇩0'
assumes "s⇩0 ≼ s⇩0'" "P s⇩0" "I s⇩0'"
begin
lemma run_subsumed:
assumes "run (s⇩0 ## xs)"
obtains ys where "G.run (s⇩0' ## ys)" "stream_all2 (≼) xs ys" "pred_stream I ys"
proof -
from ‹s⇩0 ≼ _› ‹P s⇩0› ‹I s⇩0'› have "equiv' s⇩0 s⇩0'"
unfolding equiv'_def by auto
with assms show ?thesis
by - (drule simulation_run, auto
dest: PB_invariant.invariant_run elim: stream_all2_weaken intro!: that simp: equiv'_def)
qed
context
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "P a ⟹ F a ⟹ a ≼ b ⟹ P b ⟹ F b"
begin
corollary final_unreachable:
"∄ s'. reaches s⇩0 s' ∧ F s'" if "∀s'. I s' ⟶ ¬ F s'"
using ‹s⇩0 ≼ s⇩0'› ‹P s⇩0› ‹I s⇩0'› simulation_reaches that I_P by blast
lemma buechi_run_lasso:
assumes "finite {s. I s}" "run (s⇩0 ## xs)" "alw (ev (holds F)) (s⇩0 ## xs)"
obtains s where "G.reaches s⇩0' s" "G.reaches1 s s" "F s"
proof -
interpret Finite_Graph E' s⇩0'
by (standard, rule finite_subset[OF _ assms(1)])
(auto intro: PB_invariant.invariant_reaches ‹I s⇩0'›)
from run_subsumed[OF assms(2)] obtain ys where ys:
"G.run (s⇩0' ## ys)" "stream_all2 (≼) xs ys" "pred_stream I ys" .
moreover from ‹run _› have "pred_stream P xs"
using PA_invariant.invariant_run ‹P s⇩0› by auto
ultimately have "stream_all2 (λx y. x ≼ y ∧ P x ∧ I y) xs ys"
by (smt stream.pred_set stream.rel_mono_strong)
with assms(3) ‹s⇩0 ≼ _› ‹P s⇩0› ‹I s⇩0'› have "alw (ev (holds F)) (s⇩0' ## ys)"
by (elim alw_ev_lockstep) (erule stream.rel_intros[rotated], auto)
from buechi_run_lasso[OF ys(1) this] show ?thesis
using that .
qed
end
end
end
locale Unreachability_Invariant = Subsumption_Graph_Pre_Defs + preorder less_eq less +
fixes s⇩0
fixes S :: "'a set" and SE :: "'a ⇒ 'a ⇒ bool"
assumes mono:
"s ≼ s' ⟹ s → t ⟹ s ∈ S ∨ reaches s⇩0 s ⟹ s' ∈ S ∨ reaches s⇩0 s'
⟹ ∃ t'. t ≼ t' ∧ s' → t'"
assumes S_E_subsumed: "s ∈ S ⟹ s → t ⟹ ∃ t' ∈ S. SE t t'"
assumes subsumptions_subsume: "SE s t ⟹ s ≼ t"
begin
interpretation Unreachability_Invariant1
where P = "λs. s ∈ S ∨ reaches s⇩0 s"
and I = "λs. s ∈ S"
apply standard
using mono S_E_subsumed subsumptions_subsume
apply (solves auto)+
oops
lemma reachable_S_subsumed:
"∃ s'. s' ∈ S ∧ s ≼ s'" if "s' ∈ S" "s⇩0 ≼ s'" "reaches s⇩0 s"
supply [intro] = order_trans less_trans less_imp_le
using that(3) apply induction
subgoal
using that(1,2) by blast
apply clarify
apply (drule mono)
using S_E_subsumed subsumptions_subsume by blast+
definition E' where
"E' s t ≡ ∃s'. E s s' ∧ SE s' t ∧ t ∈ S"
sublocale G: Graph_Defs E' .
context
fixes s⇩0'
assumes "s⇩0 ≼ s⇩0'" "s⇩0' ∈ S"
begin
interpretation Simulation_Invariant E E' "(≼)" "λs. reaches s⇩0 s" "λx. x ∈ S"
proof standard
fix a b a' :: ‹'a›
assume ‹a → b› ‹s⇩0 →* a› ‹a' ∈ S› ‹a ≼ a'›
with mono[OF ‹a ≼ a'› ‹a → b›] obtain b' where "b ≼ b'" "a' → b'"
by auto
with S_E_subsumed[OF ‹a' ∈ S›] obtain c where "c ∈ S" "SE b' c"
by auto
with ‹a' → b'› have "E' a' c"
unfolding E'_def by auto
with ‹b ≼ b'› ‹SE b' c› subsumptions_subsume show ‹∃b'. E' a' b' ∧ b ≼ b'›
by (blast intro: order_trans)
qed (auto simp: E'_def)
lemma run_subsumed:
assumes "run (s⇩0 ## xs)"
obtains ys where "G.run (s⇩0' ## ys)" "stream_all2 (≼) xs ys" "pred_stream (λx. x ∈ S) ys"
proof -
from ‹s⇩0 ≼ _› ‹s⇩0' ∈ S› have "equiv' s⇩0 s⇩0'"
unfolding equiv'_def by auto
with assms show ?thesis
by - (drule simulation_run, auto
dest: PB_invariant.invariant_run elim: stream_all2_weaken intro!: that simp: equiv'_def)
qed
context
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "reaches s⇩0 a ⟹ F a ⟹ a ≼ b ⟹ b ∈ S ⟹ F b"
begin
corollary final_unreachable:
"∄ s'. reaches s⇩0 s' ∧ F s'" if "∀ s' ∈ S. ¬ F s'"
using that ‹s⇩0 ≼ s⇩0'› ‹s⇩0' ∈ S› by (auto 4 3 dest: reachable_S_subsumed)
lemma buechi_run_lasso:
assumes "finite S" "run (s⇩0 ## xs)" "alw (ev (holds F)) (s⇩0 ## xs)"
obtains s where "G.reaches s⇩0' s" "G.reaches1 s s" "F s"
proof -
interpret Finite_Graph E' s⇩0'
by (standard, rule finite_subset[OF _ assms(1)])
(auto intro: PB_invariant.invariant_reaches ‹s⇩0' ∈ S›)
from run_subsumed[OF assms(2)] obtain ys where ys:
"G.run (s⇩0' ## ys)" "stream_all2 (≼) xs ys" "pred_stream (λx. x ∈ S) ys" .
moreover from ‹run _› have "pred_stream (reaches s⇩0) xs"
using run_reachable by blast
ultimately have "stream_all2 (λx y. x ≼ y ∧ reaches s⇩0 x ∧ y ∈ S) xs ys"
by (smt stream.pred_set stream.rel_mono_strong)
with assms(3) ‹s⇩0 ≼ _› ‹s⇩0' ∈ S› have "alw (ev (holds F)) (s⇩0' ## ys)"
by (elim alw_ev_lockstep) (erule stream.rel_intros[rotated], auto)
from buechi_run_lasso[OF ys(1) this] show ?thesis
using that .
qed
end
end
end
context Unreachability_Invariant1
begin
interpretation inv: Graph_Invariant
by standard (rule P_invariant)
context
fixes s⇩0 :: 'a
assumes "P s⇩0"
begin
interpretation E: Unreachability_Invariant
where S = "{s. I s}"
by standard (auto intro: ‹P s⇩0› inv.invariant_reaches mono S_E_subsumed subsumptions_subsume)
end
end
locale Unreachability_Invariant_Contract1 =
Unreachability_Invariant1 +
fixes f :: "'a ⇒ nat" and F :: "'a ⇒ bool"
assumes f_topo:
"I a ⟹ E a b ⟹ SE b c ⟹ (if F a then f a < f c else f a ≤ f c)"
assumes finite_invariant: "finite {s. I s}"
assumes F_mono[intro]: "P a ⟹ F a ⟹ a ≼ b ⟹ P b ⟹ F b"
begin
interpretation c: Contract E'
using f_topo
apply -
apply standard
apply (auto simp: E'_def)
oops
definition
"E1 ≡ λa c. ∃b. I a ∧ E a b ∧ SE b c"
interpretation c: Contract E1
using f_topo by - (standard, auto simp: E1_def)
lemma no_buechi_run:
assumes [intro, simp]: "P s⇩0" "I s⇩0'" "s⇩0 ≼ s⇩0'"
assumes "Graph_Defs.run E (s⇩0 ## xs)" "alw (ev (holds F)) (s⇩0 ## xs)"
shows False
proof -
interpret sim: Simulation E' E1 "λs s'. s' = s ∧ I s"
unfolding E'_def E1_def by standard auto
obtain s where
"G.reaches s⇩0' s" "G.reaches1 s s" "F s"
using finite_invariant assms by - (rule buechi_run_lasso[where F= F], rule assms, auto)
then have "c.E.reaches1 s s"
using E'_def G.reaches1_reaches_iff2 by - (frule sim.simulation_reaches1, auto)
then have "¬ F s"
by (rule c.no_accepting_cycle)
from this ‹F s› show ?thesis ..
qed
end
locale Reachability_Invariant_paired_pre_defs =
ord less_eq less for less_eq :: "'s ⇒ 's ⇒ bool" (infix "≼" 50) and less (infix "≺" 50) +
fixes E :: "('l × 's) ⇒ ('l × 's) ⇒ bool"
locale Reachability_Invariant_paired_defs =
Reachability_Invariant_paired_pre_defs where E = E for E :: "('l × 's) ⇒ ('l × 's) ⇒ bool" +
fixes M :: "'l ⇒ 's set"
and L :: "'l set"
begin
definition "covered ≡ λ (l, s). ∃ s' ∈ M l. s ≺ s'"
definition "RE = (λ(l, s) ab. s ∈ M l ∧ ¬ covered (l, s) ∧ E (l, s) ab)"
end
locale Unreachability_Invariant_paired_pre_defs =
Reachability_Invariant_paired_pre_defs _ _ E +
preorder less_eq less for E :: "('l × 's) ⇒ _" +
fixes P :: "('l × 's) ⇒ bool"
locale Unreachability_Invariant_paired_defs =
Unreachability_Invariant_paired_pre_defs where E = E +
Reachability_Invariant_paired_defs where E = E
for E :: "('l × 's) ⇒ _"
locale Unreachability_Invariant_paired_pre =
Unreachability_Invariant_paired_pre_defs +
assumes mono:
"s ≼ s' ⟹ E (l, s) (l', t) ⟹ P (l, s) ⟹ P (l, s') ⟹ ∃ t'. t ≼ t' ∧ E (l, s') (l', t')"
assumes P_invariant: "P (l, s) ⟹ E (l, s) (l', s') ⟹ P (l', s')"
locale Unreachability_Invariant_paired =
Unreachability_Invariant_paired_pre where E = E and P = P +
Unreachability_Invariant_paired_defs where M = M and L = L and E = E and P = P
for M :: "'l ⇒ 's set" and L :: "'l set" and E :: "'l × 's ⇒ _" and P :: "'l × 's ⇒ _" +
fixes l⇩0 :: 'l and s⇩0 :: 's
fixes SE :: "'l × 's ⇒ 'l × 's ⇒ bool"
assumes subsumption_edges_subsume: "SE (l, s) (l', s') ⟹ l' = l ∧ s ≼ s'"
assumes M_invariant: "l ∈ L ⟹ s ∈ M l ⟹ P (l, s)"
assumes start: "l⇩0 ∈ L" "∃s' ∈ M l⇩0. s⇩0 ≼ s'" "P (l⇩0, s⇩0)"
assumes closed:
"∀l ∈ L. ∀s ∈ M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s'' ∈ M l'. SE (l', s') (l', s''))"
begin
interpretation Graph_Defs E .
interpretation inv: Graph_Invariant E P
by standard (auto intro: P_invariant)
interpretation unreach1: Unreachability_Invariant1
"λ (l, s) (l', s'). l' = l ∧ s ≼ s'" "λ (l, s) (l', s'). l' = l ∧ s ≺ s'" E
"λ(l, s). l ∈ L ∧ s ∈ M l"
supply [intro] = order_trans less_trans less_imp_le
apply standard
using subsumption_edges_subsume closed
apply (all ‹(auto intro: M_invariant P_invariant dest: mono simp: less_le_not_le; fail)?›)
using closed by (metis (mono_tags, lifting) old.prod.case surj_pair)
interpretation Unreachability_Invariant
"λ (l, s) (l', s'). l' = l ∧ s ≼ s'" "λ (l, s) (l', s'). l' = l ∧ s ≺ s'" E "(l⇩0, s⇩0)"
"{(l, s) | l s. l ∈ L ∧ s ∈ M l}"
supply [intro] = order_trans less_trans less_imp_le
apply standard
apply (fastforce intro: inv.invariant_reaches[OF _ start(3)] M_invariant dest: mono)
subgoal for s t
using closed by (cases s; cases t) fastforce
subgoal
using subsumption_edges_subsume by auto
done
lemma E_L:
assumes "l ∈ L" "s ∈ M l" "E (l, s) (l', s')"
shows "l' ∈ L"
using assms closed by simp
context
fixes F
assumes F_mono: "⋀ a b. P a ⟹ F a ⟹ (λ(l, s) (l', s'). l' = l ∧ s ≼ s') a b ⟹ P b ⟹ F b"
begin
private definition
"s' ≡ SOME s. s ∈ M l⇩0 ∧ s⇩0 ≼ s"
private lemma s'_correct:
"s' ∈ M l⇩0 ∧ s⇩0 ≼ s'"
using start(2) unfolding s'_def by - (rule someI_ex, auto)
private lemma s'_1:
"(l⇩0, s') ∈ {(l, s) |l s. l ∈ L ∧ s ∈ M l}"
using s'_correct start by auto
private lemma s'_2:
"(case (l⇩0, s⇩0) of (l, s) ⇒ λ(l', s'). l' = l ∧ s ≼ s') (l⇩0, s')"
using s'_correct start by auto
theorem final_unreachable:
assumes "∀s'∈{(l, s) |l s. l ∈ L ∧ s ∈ M l}. ¬ F s'"
shows "∄s'. (l⇩0, s⇩0) →* s' ∧ F s'"
using inv.invariant_reaches start(3) M_invariant F_mono assms
by - (simp, rule final_unreachable[OF s'_2 s'_1, simplified], blast+)
lemma buechi_run_lasso:
assumes "finite {(l, s) |l s. l ∈ L ∧ s ∈ M l}"
assumes "run ((l⇩0, s⇩0) ## xs)" "alw (ev (holds F)) ((l⇩0, s⇩0) ## xs)"
obtains s⇩0' l s where
"G.reaches (l⇩0, s⇩0') (l, s)" "G.reaches1 (l, s) (l, s)" "F (l, s)" "s⇩0' ∈ M l⇩0" "s⇩0 ≼ s⇩0'"
using F_mono assms M_invariant inv.invariant_reaches start(3) s'_correct
by - (rule buechi_run_lasso[OF s'_2 s'_1, of F]; clarsimp; blast)
context
fixes f :: "'l × 's ⇒ nat"
assumes finite: "finite L" "∀ l ∈ L. finite (M l)"
assumes f_topo: "⋀l s l1 s1 l2 s2.
l ∈ L ⟹ s ∈ M l ⟹ l2 ∈ L ⟹ s2 ∈ M l2 ⟹ E (l, s) (l1, s1) ⟹ SE (l1, s1) (l2, s2) ⟹
if F (l, s) then f (l, s) < f (l2, s2) else f (l, s) ≤ f (l2, s2)"
begin
interpretation c: Contract2
where A = "λ(l, s) (l', s'). l ∈ L ∧ s ∈ M l ∧ E (l, s) (l', s')"
and B = SE
and G = "λ(l, s). l ∈ L ∧ s ∈ M l"
using f_topo by - (standard, auto)
lemma no_buechi_run:
assumes "Graph_Defs.run E ((l⇩0, s⇩0) ## xs)" "alw (ev (holds F)) ((l⇩0, s⇩0) ## xs)"
shows False
proof -
have finite: "finite {(l, s). l ∈ L ∧ s ∈ M l}" (is "finite ?S")
proof -
have "?S ⊆ L × ⋃ (M ` L)"
by auto
also from finite have "finite …"
by auto
finally show ?thesis .
qed
interpret sim: Simulation E' c.E "λ(l, s) (l', s'). l = l' ∧ s' = s ∧ l ∈ L ∧ s ∈ M l"
unfolding E'_def c.E_def by standard auto
obtain s⇩0' l s where
"s⇩0 ≼ s⇩0'" "s⇩0' ∈ M l⇩0" "G.reaches (l⇩0, s⇩0') (l, s)" "G.reaches1 (l, s) (l, s)" "F (l, s)"
using finite assms by - (rule buechi_run_lasso, auto)
then have "c.E.reaches1 (l, s) (l, s)"
using E'_def G.reaches1_reaches_iff2 by - (frule sim.simulation_reaches1, auto)
then have "¬ F (l, s)"
by (rule c.no_accepting_cycle)
from this ‹F (l, s)› show ?thesis ..
qed
end
end
end
subsection ‹Unused›
lemma (in Reachability_Compatible_Subsumption_Graph_Final) no_accepting_cycleI:
assumes "∄ x. G'.reachable x ∧ x →⇩G⇧+' x ∧ F x"
shows "∄ x. reachable x ∧ x →⇧+ x ∧ F x"
using cycle_G'_cycle assms F_mono by auto
locale Reachability_Compatible_Subsumption_Graph_Final2_pre =
Subsumption_Graph_Defs + preorder less_eq less +
fixes P :: "'a ⇒ bool" and G :: "'a ⇒ bool"
assumes mono:
"a ≼ b ⟹ E a a' ⟹ P a ⟹ P b ⟹ ∃b'. E b b' ∧ a' ≼ b'"
assumes P_invariant: "P a ⟹ E a b ⟹ P b"
assumes G_P[intro]: "G a ⟹ P a"
assumes subgraph: "∀ s s'. RE s s' ⟶ E s s'"
assumes G_finite: "finite {a. G a}"
and finitely_branching: "⋀a. G a ⟹ finite (Collect (E a))"
assumes G_start: "G s⇩0"
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "F a ⟹ a ≼ b ⟹ F b"
assumes G_anti_symmetric[rule_format]: "∀ a b. G a ∧ G b ∧ a ≼ b ∧ b ≼ a ⟶ a = b"
begin
abbreviation "E_mix ≡ λ x y. RE x y ∧ G x ∧ G y ∨ E x y ∧ G x ∧ ¬ G y ∨ ¬ G x ∧ x ≺ y ∧ G y"
sublocale G_mix: Graph_Start_Defs E_mix s⇩0 .
sublocale P_invariant: Graph_Invariant E P
by standard (auto intro: P_invariant)
sublocale G_invariant: Graph_Invariant E_mix P
by standard (auto simp: subgraph intro: P_invariant)
lemma mix_reachable_G[intro]:
"P x" if "G_mix.reachable x"
proof -
from G_start have "P s⇩0"
by auto
with that show ?thesis
by induction (auto simp: subgraph intro: P_invariant)
qed
lemma P_reachable[intro]:
"P a" if "reachable a"
using that G_start by (auto simp: reachable_def intro: P_invariant.invariant_reaches)
lemma mix_finite_reachable: "finite {a. G_mix.reachable a}"
proof -
have "G x ∨ (∃ a. G a ∧ E a x)" if "G_mix.reachable x" for x
using that G_start by induction auto
then have "{a. G_mix.reachable a} ⊆ Collect G ∪ {(a, b). E a b} `` Collect G"
by auto
also have "finite …"
using G_finite by (auto intro: finitely_branching)
finally show ?thesis .
qed
end
locale Reachability_Compatible_Subsumption_Graph_Final2 =
Reachability_Compatible_Subsumption_Graph_Final2_pre +
assumes liveness_compatible:
"∀a a' b. P a ∧ G a' ∧ a ≼ a' ∧ E a b
⟶ (∃b'. b ≼ b' ∧ a' →⇩G b' ∧ G b')
∨ (∃b' b''. b ≼ b' ∧ b' ≺ b'' ∧ E a' b' ∧ ¬ G b' ∧ G b'')"
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemma subsumption_step:
"(∃b'. b ≼ b' ∧ a' →⇩G b' ∧ G b') ∨ (∃b' b''. b ≼ b' ∧ b' ≺ b'' ∧ E a' b' ∧ ¬ G b' ∧ G b'')"
if "P a" "E a b" "G a'" "a ≼ a'"
using liveness_compatible that by auto
lemma subsumption_step':
"∃ b'. b ≼ b' ∧ G_mix.reaches1 a' b' ∧ G b'" if "P a" "E a b" "G a'" "a ≼ a'"
proof -
from subsumption_step[OF that] show ?thesis
proof (safe, goal_cases)
case (1 b')
then show ?case
using that(3) by auto
next
case (2 b' b'')
with ‹G a'› have "E_mix b' b''" "E_mix a' b'"
by auto
with ‹b ≼ b'› ‹b' ≺ b''› ‹G b''› show ?case
including graph_automation_aggressive using le_less_trans less_imp_le by blast
qed
qed
theorem reachability_complete':
"∃ s'. s ≼ s' ∧ G_mix.reachable s' ∧ G s'" if "a →* s" "G_mix.reachable a" "G a"
using that
proof (induction)
case base
then show ?case by auto
next
case (step s t)
then obtain s' where "s ≼ s'" "G_mix.reachable s'" "G s'"
by auto
from ‹G a› ‹a →* s› have "P s"
by (auto intro: P_invariant.invariant_reaches)
from subsumption_step[OF this ‹E s t› ‹G s'› ‹s ≼ s'›] show ?case
proof safe
fix b' :: ‹'a›
assume ‹t ≼ b'› and ‹s' →⇩G b'› and ‹G b'›
with ‹G s'› have "E_mix s' b'"
by auto
with ‹t ≼ b'› ‹G b'› ‹G_mix.reachable s'› show ‹∃s'. t ≼ s' ∧ G_mix.reachable s' ∧ G s'›
by auto
next
fix b' b'' :: ‹'a›
assume ‹t ≼ b'› and ‹b' ≺ b''› and ‹s' → b'› and ‹¬ G b'› and ‹G b''›
with ‹G s'› have "E_mix s' b'" "E_mix b' b''"
by auto
with ‹G b''› ‹t ≼ _› ‹_ ≺ b''› ‹G_mix.reachable s'› show
‹∃s'. t ≼ s' ∧ G_mix.reachable s' ∧ G s'›
apply (inst_existentials b'')
subgoal
using le_less_trans less_imp_le by auto
by auto
qed
qed
lemma steps_G_mix_steps:
"∃ ys ns. list_all2 (≼) xs (nths ys ns) ∧ G_mix.steps (b # ys)" if
"steps (a # xs)" "P a" "a ≼ b" "G b"
using that
proof (induction "a # xs" arbitrary: a b xs)
case (Single)
then show ?case by force
next
case (Cons x y xs)
from subsumption_step'[OF ‹P x› ‹E x y› _ ‹x ≼ b›] ‹G b› obtain b' where
"y ≼ b'" "G_mix.reaches1 b b'" "G b'"
by auto
with ‹P x› Cons.hyps(1) Cons.prems(3) obtain ys ns where
"list_all2 (≼) xs (nths ys ns)" "G_mix.steps (b' # ys)"
by atomize_elim
(blast intro: Cons.hyps(3)[OF _ ‹y ≼ b'›]
P_invariant graphI_aggressive G_invariant.invariant_reaches
)
from ‹G_mix.reaches1 b b'› this(2) obtain as where
"G_mix.steps (b # as @ b' # ys)"
by (fastforce intro: G_mix.graphI_aggressive1)
with ‹y ≼ b'› show ?case
apply (inst_existentials "as @ b' # ys" "{length as} ∪ {n + length as + 1 | n. n ∈ ns}")
subgoal
apply (subst nths_split, force)
apply (subst nths_nth, (simp; fail))
apply simp
apply (subst nths_shift, force)
subgoal premises prems
proof -
have
"{x - length as |x. x ∈ {Suc (n + length as) |n. n ∈ ns}} = {n + 1 | n. n ∈ ns}"
by force
with ‹list_all2 _ _ _› show ?thesis
by (simp add: nths_Cons)
qed
done
by assumption
qed
lemma cycle_G_mix_cycle'':
assumes "steps (s⇩0 # ws @ x # xs @ [x])"
shows "∃ x' xs' ys'. x ≼ x' ∧ G_mix.steps (s⇩0 # xs' @ x' # ys' @ [x'])"
proof -
let ?n = "card {x. G_mix.reachable x} + 1"
let ?xs = "x # concat (replicate ?n (xs @ [x]))"
from assms(1) have "steps (x # xs @ [x])"
by (auto intro: graphI_aggressive2)
with steps_replicate[of "x # xs @ [x]" ?n] have "steps ?xs"
by auto
have "steps (s⇩0 # ws @ ?xs)"
proof -
from assms have "steps (s⇩0 # ws @ [x])"
by (auto intro: graphI_aggressive2)
with ‹steps ?xs› show ?thesis
by (fastforce intro: graphI_aggressive1)
qed
from steps_G_mix_steps[OF this, of s⇩0] G_start obtain ys ns where ys:
"list_all2 (≼) (ws @ x # concat (replicate ?n (xs @ [x]))) (nths ys ns)"
"G_mix.steps (s⇩0 # ys)"
by auto
then obtain x' ys' ns' ws' where ys':
"G_mix.steps (x' # ys')" "G_mix.steps (s⇩0 # ws' @ [x'])"
"list_all2 (≼) (concat (replicate ?n (xs @ [x]))) (nths ys' ns')"
apply atomize_elim
apply simp
apply (subst (asm) list_all2_append1)
apply safe
apply (subst (asm) list_all2_Cons1)
apply safe
apply (drule nths_eq_appendD)
apply safe
apply (drule nths_eq_ConsD)
apply safe
subgoal for ys1 ys2 z ys3 ys4 ys5 ys6 ys7 i
apply (inst_existentials z ys7)
subgoal premises prems
using prems(1) by (auto intro: G_mix.graphI_aggressive2)
subgoal premises prems
proof -
from prems have "G_mix.steps ((s⇩0 # ys4 @ ys6 @ [z]) @ ys7)"
by auto
moreover then have "G_mix.steps (s⇩0 # ys4 @ ys6 @ [z])"
by (auto intro: G_mix.graphI_aggressive2)
ultimately show ?thesis
by (inst_existentials "ys4 @ ys6") auto
qed
by force
done
let ?ys = "filter ((≼) x) ys'"
have "length ?ys ≥ ?n"
using list_all2_replicate_elem_filter[OF ys'(3), of x]
using filter_nths_length[of "((≼) x)" ys' ns']
by auto
from ‹G_mix.steps (s⇩0 # ws' @ [x'])› have "G_mix.reachable x'"
by - (rule G_mix.reachable_reaches, auto)
have "set ?ys ⊆ set ys'"
by auto
also have "… ⊆ {x. G_mix.reachable x}"
using ‹G_mix.steps (x' # _)› ‹G_mix.reachable x'›
by clarsimp (rule G_mix.reachable_steps_elem[rotated], assumption, auto)
finally have "¬ distinct ?ys"
using distinct_card[of ?ys] ‹_ >= ?n›
by - (rule ccontr; drule distinct_length_le[OF mix_finite_reachable]; simp)
from not_distinct_decomp[OF this] obtain as y bs cs where "?ys = as @ [y] @ bs @ [y] @ cs"
by auto
then obtain as' bs' cs' where
"ys' = as' @ [y] @ bs' @ [y] @ cs'"
apply atomize_elim
apply simp
apply (drule filter_eq_appendD filter_eq_ConsD filter_eq_appendD[OF sym], clarify)+
apply clarsimp
subgoal for as1 as2 bs1 bs2 cs'
by (inst_existentials "as1 @ as2" "bs1 @ bs2") simp
done
have "G_mix.steps (y # bs' @ [y])"
proof -
from ‹G_mix.steps (x' # _)› ‹ys' = _› show ?thesis
by (force intro: G_mix.graphI_aggressive2)
qed
moreover have "G_mix.steps (s⇩0 # ws' @ x' # as' @ [y])"
proof -
from ‹G_mix.steps (x' # ys')› ‹ys' = _› have "G_mix.steps (x' # as' @ [y])"
by (force intro: G_mix.graphI_aggressive2)
with ‹G_mix.steps (s⇩0 # ws' @ [x'])› show ?thesis
by (fastforce intro: G_mix.graphI_aggressive1)
qed
moreover from ‹?ys = _› have "x ≼ y"
proof -
from ‹?ys = _› have "y ∈ set ?ys" by auto
then show ?thesis by auto
qed
ultimately show ?thesis
by (inst_existentials y "ws' @ x' # as'" bs'; fastforce intro: G_mix.graphI_aggressive1)
qed
lemma cycle_G_mix_cycle':
assumes "steps (s⇩0 # ws @ x # xs @ [x])"
shows "∃ y ys. x ≼ y ∧ G_mix.steps (y # ys @ [y]) ∧ G_mix.reachable y"
proof -
from cycle_G_mix_cycle''[OF assms] obtain x' xs' ys' where
"x ≼ x'" "G_mix.steps (s⇩0 # xs' @ x' # ys' @ [x'])"
by auto
then show ?thesis
apply (inst_existentials x' ys')
subgoal by assumption
subgoal by (auto intro: G_mix.graphI_aggressive2)
by (rule G_mix.reachable_reaches, auto)
qed
lemma cycle_G_mix_cycle:
assumes "reachable x" "x →⇧+ x"
shows "∃ y ys. x ≼ y ∧ G_mix.reachable y ∧ G_mix.reaches1 y y"
proof -
from assms(2) obtain xs where *: "steps (x # xs @ x # xs @ [x])"
by (fastforce intro: graphI_aggressive1)
from reachable_steps[of x] assms(1) obtain ws where "steps ws" "hd ws = s⇩0" "last ws = x"
by auto
with * obtain us where "steps (s⇩0 # (us @ xs) @ x # xs @ [x])"
by (cases ws; force intro: graphI_aggressive1)
from cycle_G_mix_cycle'[OF this] show ?thesis
by (auto simp: G_mix.steps_reaches1)
qed
theorem no_accepting_cycleI:
assumes "∄ x. G_mix.reachable x ∧ G_mix.reaches1 x x ∧ F x"
shows "∄ x. reachable x ∧ x →⇧+ x ∧ F x"
using cycle_G_mix_cycle assms F_mono by auto
end
end
locale Reachability_Compatible_Subsumption_Graph_Final'_pre =
Subsumption_Graph_Defs + preorder less_eq less +
fixes P :: "'a ⇒ bool" and G :: "'a ⇒ bool"
assumes mono:
"a ≼ b ⟹ E a a' ⟹ P a ⟹ P b ⟹ ∃b'. E b b' ∧ a' ≼ b'"
assumes P_invariant: "P a ⟹ E a b ⟹ P b"
assumes G_P[intro]: "G a ⟹ P a"
assumes subgraph: "∀ s s'. RE s s' ⟶ E s s'"
assumes G_finite: "finite {a. G a}"
assumes G_start: "G s⇩0"
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "F a ⟹ a ≼ b ⟹ F b"
assumes G_anti_symmetric[rule_format]: "∀ a b. G a ∧ G b ∧ a ≼ b ∧ b ≼ a ⟶ a = b"
begin
abbreviation "E_mix ≡ λ x y. RE x y ∧ G y ∨ x ≺ y ∧ G y"
sublocale G_mix: Graph_Start_Defs E_mix s⇩0 .
sublocale P_invariant: Graph_Invariant E P
by standard (auto intro: P_invariant)
sublocale G_invariant: Graph_Invariant E_mix G
by standard auto
lemma mix_reachable_G[intro]:
"G x" if "G_mix.reachable x"
using that G_start by induction auto
lemma P_reachable[intro]:
"P a" if "reachable a"
using that G_start by (auto simp: reachable_def intro: P_invariant.invariant_reaches)
lemma mix_finite_reachable: "finite {a. G_mix.reachable a}"
by (blast intro: finite_subset[OF _ G_finite])
end
locale Reachability_Compatible_Subsumption_Graph_Final'' =
Reachability_Compatible_Subsumption_Graph_Final'_pre +
assumes liveness_compatible:
"∀a a' b. P a ∧ G a' ∧ a ≼ a' ∧ E a b
⟶ (∃ a'' b'. a' ≼ a'' ∧ b ≼ b' ∧ a'' →⇩G b' ∧ G a'' ∧ G b')"
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemma subsumption_step:
"∃ a'' b'. a' ≼ a'' ∧ b ≼ b' ∧ a'' →⇩G b' ∧ G a'' ∧ G b'" if
"P a" "E a b" "G a'" "a ≼ a'"
using liveness_compatible that by auto
lemma G_mix_reaches:
assumes "G a" "G b" "a ≼ b"
shows "G_mix.reaches a b"
using assms by (cases "a ≺ b") (auto simp: G_anti_symmetric less_le_not_le)
lemma subsumption_step':
"∃ b'. b ≼ b' ∧ G_mix.reaches1 a' b'" if "P a" "E a b" "G a'" "a ≼ a'"
proof -
from subsumption_step[OF that] obtain a'' b' where
"a' ≼ a''" "b ≼ b'" "a'' →⇩G b'" "G a''" "G b'"
by atomize_elim
with ‹G a'› have "G_mix.reaches a' a''" "E_mix a'' b'"
by (auto intro: G_mix_reaches)
with ‹b ≼ b'› show ?thesis
unfolding G_mix.reaches1_reaches_iff2 by auto
qed
theorem reachability_complete':
"∃ s'. s ≼ s' ∧ G_mix.reachable s' ∧ G s'" if "a →* s" "G_mix.reachable a" "G a"
using that
proof (induction)
case base
then show ?case by auto
next
case (step s t)
then obtain s' where "s ≼ s'" "G_mix.reachable s'" "G s'"
by auto
from ‹G a› ‹a →* s› have "P s"
by (auto intro: P_invariant.invariant_reaches)
from subsumption_step[OF this ‹E s t› ‹G s'› ‹s ≼ s'›] obtain s'' t' where
"s' ≼ s''" "t ≼ t'" "s'' →⇩G t'" "G s''" "G t'" by atomize_elim
with ‹G_mix.reachable s'› show ?case
using G_mix_reaches by (inst_existentials t') blast+
qed
lemma steps_G_mix_steps:
"∃ ys ns. list_all2 (≼) xs (nths ys ns) ∧ G_mix.steps (b # ys)" if
"steps (a # xs)" "P a" "a ≼ b" "G b"
using that
proof (induction "a # xs" arbitrary: a b xs)
case (Single)
then show ?case by force
next
case (Cons x y xs)
from subsumption_step'[OF ‹P x› ‹E x y› _ ‹x ≼ b›] ‹G b› obtain b' where
"y ≼ b'" "G_mix.reaches1 b b'"
by auto
with ‹P x› Cons.hyps(1) Cons.prems(3) obtain ys ns where
"list_all2 (≼) xs (nths ys ns)" "G_mix.steps (b' # ys)"
by atomize_elim
(blast intro: Cons.hyps(3)[OF _ ‹y ≼ b'›]
P_invariant graphI_aggressive G_invariant.invariant_reaches
)
from ‹G_mix.reaches1 b b'› this(2) obtain as where
"G_mix.steps (b # as @ b' # ys)"
by (fastforce intro: G_mix.graphI_aggressive1)
with ‹y ≼ b'› show ?case
apply (inst_existentials "as @ b' # ys" "{length as} ∪ {n + length as + 1 | n. n ∈ ns}")
subgoal
apply (subst nths_split, force)
apply (subst nths_nth, (simp; fail))
apply simp
apply (subst nths_shift, force)
subgoal premises prems
proof -
have
"{x - length as |x. x ∈ {Suc (n + length as) |n. n ∈ ns}} = {n + 1 | n. n ∈ ns}"
by force
with ‹list_all2 _ _ _› show ?thesis
by (simp add: nths_Cons)
qed
done
by assumption
qed
lemma cycle_G_mix_cycle'':
assumes "steps (s⇩0 # ws @ x # xs @ [x])"
shows "∃ x' xs' ys'. x ≼ x' ∧ G_mix.steps (s⇩0 # xs' @ x' # ys' @ [x'])"
proof -
let ?n = "card {x. G_mix.reachable x} + 1"
let ?xs = "x # concat (replicate ?n (xs @ [x]))"
from assms(1) have "steps (x # xs @ [x])"
by (auto intro: graphI_aggressive2)
with steps_replicate[of "x # xs @ [x]" ?n] have "steps ?xs"
by auto
have "steps (s⇩0 # ws @ ?xs)"
proof -
from assms have "steps (s⇩0 # ws @ [x])"
by (auto intro: graphI_aggressive2)
with ‹steps ?xs› show ?thesis
by (fastforce intro: graphI_aggressive1)
qed
from steps_G_mix_steps[OF this, of s⇩0] obtain ys ns where ys:
"list_all2 (≼) (ws @ x # concat (replicate ?n (xs @ [x]))) (nths ys ns)"
"G_mix.steps (s⇩0 # ys)"
by auto
then obtain x' ys' ns' ws' where ys':
"G_mix.steps (x' # ys')" "G_mix.steps (s⇩0 # ws' @ [x'])"
"list_all2 (≼) (concat (replicate ?n (xs @ [x]))) (nths ys' ns')"
apply atomize_elim
apply simp
apply (subst (asm) list_all2_append1)
apply safe
apply (subst (asm) list_all2_Cons1)
apply safe
apply (drule nths_eq_appendD)
apply safe
apply (drule nths_eq_ConsD)
apply safe
subgoal for ys1 ys2 z ys3 ys4 ys5 ys6 ys7 i
apply (inst_existentials z ys7)
subgoal premises prems
using prems(1) by (auto intro: G_mix.graphI_aggressive2)
subgoal premises prems
proof -
from prems have "G_mix.steps ((s⇩0 # ys4 @ ys6 @ [z]) @ ys7)"
by auto
moreover then have "G_mix.steps (s⇩0 # ys4 @ ys6 @ [z])"
by (auto intro: G_mix.graphI_aggressive2)
ultimately show ?thesis
by (inst_existentials "ys4 @ ys6") auto
qed
by force
done
let ?ys = "filter ((≼) x) ys'"
have "length ?ys ≥ ?n"
using list_all2_replicate_elem_filter[OF ys'(3), of x]
using filter_nths_length[of "((≼) x)" ys' ns']
by auto
from ‹G_mix.steps (s⇩0 # ws' @ [x'])› have "G_mix.reachable x'"
by - (rule G_mix.reachable_reaches, auto)
have "set ?ys ⊆ set ys'"
by auto
also have "… ⊆ {x. G_mix.reachable x}"
using ‹G_mix.steps (x' # _)› ‹G_mix.reachable x'›
by clarsimp (rule G_mix.reachable_steps_elem[rotated], assumption, auto)
finally have "¬ distinct ?ys"
using distinct_card[of ?ys] ‹_ >= ?n›
by - (rule ccontr; drule distinct_length_le[OF mix_finite_reachable]; simp)
from not_distinct_decomp[OF this] obtain as y bs cs where "?ys = as @ [y] @ bs @ [y] @ cs"
by auto
then obtain as' bs' cs' where
"ys' = as' @ [y] @ bs' @ [y] @ cs'"
apply atomize_elim
apply simp
apply (drule filter_eq_appendD filter_eq_ConsD filter_eq_appendD[OF sym], clarify)+
apply clarsimp
subgoal for as1 as2 bs1 bs2 cs'
by (inst_existentials "as1 @ as2" "bs1 @ bs2") simp
done
have "G_mix.steps (y # bs' @ [y])"
proof -
from ‹G_mix.steps (x' # _)› ‹ys' = _› show ?thesis
by (force intro: G_mix.graphI_aggressive2)
qed
moreover have "G_mix.steps (s⇩0 # ws' @ x' # as' @ [y])"
proof -
from ‹G_mix.steps (x' # ys')› ‹ys' = _› have "G_mix.steps (x' # as' @ [y])"
by (force intro: G_mix.graphI_aggressive2)
with ‹G_mix.steps (s⇩0 # ws' @ [x'])› show ?thesis
by (fastforce intro: G_mix.graphI_aggressive1)
qed
moreover from ‹?ys = _› have "x ≼ y"
proof -
from ‹?ys = _› have "y ∈ set ?ys" by auto
then show ?thesis by auto
qed
ultimately show ?thesis
by (inst_existentials y "ws' @ x' # as'" bs'; fastforce intro: G_mix.graphI_aggressive1)
qed
lemma cycle_G_mix_cycle':
assumes "steps (s⇩0 # ws @ x # xs @ [x])"
shows "∃y ys. x ≼ y ∧ G_mix.steps (y # ys @ [y]) ∧ G_mix.reachable y"
proof -
from cycle_G_mix_cycle''[OF assms] obtain x' xs' ys' where
"x ≼ x'" "G_mix.steps (s⇩0 # xs' @ x' # ys' @ [x'])"
by auto
then show ?thesis
apply (inst_existentials x' ys')
subgoal by assumption
subgoal by (auto intro: G_mix.graphI_aggressive2)
by (rule G_mix.reachable_reaches, auto)
qed
lemma cycle_G_mix_cycle:
assumes "reachable x" "x →⇧+ x"
shows "∃y. x ≼ y ∧ G_mix.reachable y ∧ G_mix.reaches1 y y"
proof -
from assms(2) obtain xs where *: "steps (x # xs @ x # xs @ [x])"
by (fastforce intro: graphI_aggressive1)
from reachable_steps[of x] assms(1) obtain ws where "steps ws" "hd ws = s⇩0" "last ws = x"
by auto
with * obtain us where "steps (s⇩0 # (us @ xs) @ x # xs @ [x])"
by (cases ws; force intro: graphI_aggressive1)
from cycle_G_mix_cycle'[OF this] show ?thesis
by (auto simp: G_mix.steps_reaches1)
qed
end
end
locale Reachability_Compatible_Subsumption_Graph_Final' =
Reachability_Compatible_Subsumption_Graph_Final'_pre +
assumes liveness_compatible:
"∀ s. G s ⟶ (∀ s'. E s s' ⟶ RE s s' ∧ G s') ∨ (∃ t. s ≺ t ∧ G t)"
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemmas preorder_intros = order_trans less_trans less_imp_le
lemma reachable_has_surrogate:
"∃ t. G t ∧ s ≼ t ∧ (∀ s'. E t s' ⟶ RE t s' ∧ G s')" if "G s"
proof -
note [intro] = preorder_intros
from G_finite ‹G s› obtain x where
"∀s'. E x s' ⟶ RE x s' ∧ G s'" "G x" "((≺)⇧*⇧*) s x"
by atomize_elim (induction rule: rtranclp_ev_induct2, auto simp: liveness_compatible)
moreover from ‹((≺)⇧*⇧*) s x› have "s ≺ x ∨ s = x"
by induction auto
ultimately show ?thesis
by auto
qed
lemma subsumption_step:
"∃ a'' b'. a' ≼ a'' ∧ b ≼ b' ∧ a'' →⇩G b' ∧ G a'' ∧ G b'" if
"P a" "E a b" "G a'" "a ≼ a'"
proof -
note [intro] = preorder_intros
from mono[OF ‹a ≼ a'› ‹E a b›] ‹P a› ‹G a'› obtain b' where "E a' b'" "b ≼ b'"
by auto
from reachable_has_surrogate[OF ‹G a'›] obtain a''
where "a' ≼ a''" "G a''" and *: "∀ s'. E a'' s' ⟶ RE a'' s' ∧ G s'"
by auto
from mono[OF ‹a' ≼ a''› ‹E a' b'›] ‹G a'› ‹G a''› obtain b'' where
"E a'' b''" "b' ≼ b''"
by auto
with * ‹a' ≼ a''› ‹b ≼ b'› ‹G a''› show ?thesis
by auto
qed
end
sublocale Reachability_Compatible_Subsumption_Graph_Final''
using subsumption_step by - (standard, auto)
theorem no_accepting_cycleI:
assumes "∄ x. G_mix.reachable x ∧ G_mix.reaches1 x x ∧ F x"
shows "∄ x. reachable x ∧ x →⇧+ x ∧ F x"
using cycle_G_mix_cycle assms F_mono by auto
end
locale Reachability_Compatible_Subsumption_Graph_Final1 =
Reachability_Compatible_Subsumption_Graph_Final'_pre +
assumes reachable_has_surrogate:
"∀ s. G s ⟶ (∃ t. G t ∧ s ≼ t ∧ (∀ s'. E t s' ⟶ RE t s' ∧ G s'))"
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemmas preorder_intros = order_trans less_trans less_imp_le
lemma subsumption_step:
"∃ a'' b'. a' ≼ a'' ∧ b ≼ b' ∧ a'' →⇩G b' ∧ G a'' ∧ G b'" if
"P a" "E a b" "G a'" "a ≼ a'"
proof -
note [intro] = preorder_intros
from mono[OF ‹a ≼ a'› ‹E a b›] ‹P a› ‹G a'› obtain b' where "E a' b'" "b ≼ b'"
by auto
from reachable_has_surrogate ‹G a'› obtain a''
where "a' ≼ a''" "G a''" and *: "∀ s'. E a'' s' ⟶ RE a'' s' ∧ G s'"
by auto
from mono[OF ‹a' ≼ a''› ‹E a' b'›] ‹G a'› ‹G a''› obtain b'' where
"E a'' b''" "b' ≼ b''"
by auto
with * ‹a' ≼ a''› ‹b ≼ b'› ‹G a''› show ?thesis
by auto
qed
end
sublocale Reachability_Compatible_Subsumption_Graph_Final''
using subsumption_step by - (standard, auto)
theorem no_accepting_cycleI:
assumes "∄ x. G_mix.reachable x ∧ G_mix.reaches1 x x ∧ F x"
shows "∄ x. reachable x ∧ x →⇧+ x ∧ F x"
using cycle_G_mix_cycle assms F_mono by auto
end
subsection ‹Instantiating Reachability Compatible Subsumption Graphs›
locale Reachability_Invariant_paired =
Reachability_Invariant_paired_defs where M = M +
preorder: preorder less_eq less for M :: "'l ⇒ 's set" +
fixes l⇩0 :: 'l and s⇩0 :: 's
assumes E_T: "∀ l s l' s'. E (l, s) (l', s') ⟷ (∃ f. (l', f) ∈ T l ∧ s' = f s)"
assumes mono:
"s ≼ s' ⟹ E (l, s) (l', t) ⟹ E⇧*⇧* (l⇩0, s⇩0) (l, s) ⟹ E⇧*⇧* (l⇩0, s⇩0) (l, s')
⟹ ∃ t'. t ≼ t' ∧ E (l, s') (l', t')"
assumes finitely_branching: "finite (Collect (E (a, b)))"
assumes start:"l⇩0 ∈ L" "s⇩0 ∈ S" "s⇩0 ∈ M(l⇩0)"
assumes closed:
"∀ l ∈ L. ∀ (l', f) ∈ T l. l' ∈ L ∧ (∀ s ∈ M l. (∃ s' ∈ M l'. f s ≺ s') ∨ f s ∈ M l')"
assumes reachable:
"∀ l ∈ L. ∀ s ∈ M l. RE⇧*⇧* (l⇩0, s⇩0) (l, s)"
assumes finite:
"finite L" "∀ l ∈ L. finite (M l)"
begin
lemma invariant:
"((∃ s' ∈ M l. s ≺ s') ∨ s ∈ M l) ∧ l ∈ L" if "RE⇧*⇧* (l⇩0, s⇩0) (l, s)"
using that start closed by (induction rule: rtranclp_induct2) (auto 4 3 simp: RE_def)
interpretation Reachability_Compatible_Subsumption_Graph_View
"λ (l, s) (l', s'). l' = l ∧ s ≼ s'" "λ (l, s) (l', s'). l' = l ∧ s ≺ s'"
E "(l⇩0, s⇩0)" RE
"λ (l, s) (l', s'). l' = l ∧ s ≺ s'" covered
supply [intro] = order_trans less_trans less_imp_le
apply standard
apply (solves ‹auto simp: preorder.less_le_not_le›)
apply (solves ‹auto simp: preorder.less_le_not_le›)
apply (solves ‹auto simp: preorder.order.trans›)
apply clarsimp
apply (drule mono, assumption+, (simp add: Graph_Start_Defs.reachable_def; fail)+)
apply blast
apply (clarsimp simp: Graph_Start_Defs.reachable_def; safe)
subgoal for l s
apply (drule invariant)
using reachable unfolding covered_def RE_def by fastforce
subgoal for l s l' s'
apply (drule invariant)
unfolding RE_def covered_def using E_T by force
subgoal
using E_T by force
subgoal
unfolding RE_def using E_T by force
subgoal
unfolding Graph_Start_Defs.reachable_def
proof -
have 1: "finite {(l, s). l ∈ L ∧ s ∈ M l}"
proof -
let ?S = "{(l, s). l ∈ L ∧ s ∈ M l}"
have "?S ⊆ (⋃l∈L. ((λ s. (l, s)) ` M l))"
by auto
also have "finite …"
using finite by auto
finally show "finite ?S" .
qed
have 2: "finite (Collect (E (l, s)))" for l s
by (rule finitely_branching)
let ?S = "{a. RE⇧*⇧* (l⇩0, s⇩0) a}"
have "?S ⊆ {(l⇩0, s⇩0)} ∪ (⋃ ((λ a. {b. E a b}) ` {(l, s). l ∈ L ∧ s ∈ M l}))"
using invariant by (auto simp: RE_def elim: rtranclp.cases)
also have "finite …"
using 1 2 by auto
finally show "finite ?S" .
qed
done
context
assumes no_subsumption_cycle: "G'.reachable x ⟹ x →⇩G⇧+' x ⟹ x →⇩G⇧+ x"
fixes F :: "'l × 's ⇒ bool"
assumes F_mono[intro]: "F (l, a) ⟹ a ≼ b ⟹ F (l, b)"
begin
interpretation Liveness_Compatible_Subsumption_Graph
"λ (l, s) (l', s'). l' = l ∧ s ≼ s'" "λ (l, s) (l', s'). l' = l ∧ s ≺ s'"
E "(l⇩0, s⇩0)" RE F
by standard (auto intro: no_subsumption_cycle)
lemma
"∄ x. reachable x ∧ F x ∧ x →⇧+ x" if "∄ x. G.reachable x ∧ F x ∧ x →⇩G⇧+ x"
using cycle_iff that by auto
lemma no_reachable_cycleI:
"∄ x. reachable x ∧ F x ∧ x →⇧+ x" if "∄ x. G'.reachable x ∧ F x ∧ x →⇩G⇧+ x"
using that cycle_iff unfolding G_G'_reachable_iff[symmetric] by auto
text ‹
We can certify this by accepting a set of components and checking that:
▪ there are no cycles in the component graph (including subsumption edges)
▪ no non-trivial component contains a final state
▪ no component contains an internal subsumption edge
›
end
end
subsection ‹Certifying Cycle-Freeness with Graph Components›
context
fixes E1 E2 :: "'a ⇒ 'a ⇒ bool"
fixes S :: "'a set set"
fixes s⇩0 :: 'a and a⇩0 :: "'a set"
assumes start: "s⇩0 ∈ a⇩0" "a⇩0 ∈ S"
assumes closed:
"∀ a ∈ S. ∀ x ∈ a. ∀ y. E1 x y ⟶ (∃ b ∈ S. y ∈ b)"
"∀ a ∈ S. ∀ x ∈ a. ∀ y. E2 x y ⟶ (∃ b ∈ S. y ∈ b)"
assumes finite: "∀ a ∈ S. finite a"
begin
definition "E ≡ λ x y. E1 x y ∨ E2 x y"
definition "C ≡ λ a b. ∃ x ∈ a. ∃ y ∈ b. E x y ∧ b ∈ S"
interpretation E1: Graph_Start_Defs E1 s⇩0 .
interpretation E2: Graph_Start_Defs E2 s⇩0 .
interpretation E: Graph_Start_Defs E s⇩0 .
interpretation C: Graph_Start_Defs C a⇩0 .
lemma E_closed:
"∀ a ∈ S. ∀ x ∈ a. ∀ y. E x y ⟶ (∃ b ∈ S. y ∈ b)"
using closed unfolding E_def by auto
interpretation E_invariant: Graph_Invariant E "λ x. ∃ a ∈ S. x ∈ a"
using E_closed by - (standard, auto)
interpretation E1_invariant: Graph_Invariant E1 "λ x. ∃ a ∈ S. x ∈ a"
using closed by - (standard, auto)
interpretation E2_invariant: Graph_Invariant E2 "λ x. ∃ a ∈ S. x ∈ a"
using closed by - (standard, auto)
interpretation C_invariant: Graph_Invariant C "λ a. a ∈ S ∧ a ≠ {}"
unfolding C_def by standard auto
interpretation Simulation_Invariant E C "(∈)" "λ x. ∃ a ∈ S. x ∈ a" "λ a. a ∈ S ∧ a ≠ {}"
unfolding C_def by (standard; blast dest: E_invariant.invariant[rotated])+
interpretation Subgraph E E1
unfolding E_def by standard auto
context
assumes no_internal_E2: "∀ a ∈ S. ∀ x ∈ a. ∀ y ∈ a. ¬ E2 x y"
and no_component_cycle: "∀ a ∈ S. ∄ b. (C.reachable a ∧ C a b ∧ C.reaches b a ∧ a ≠ b)"
begin
lemma E_C_reaches1:
"C.reaches1 a b" if "E.reaches1 x y" "x ∈ a" "a ∈ S" "y ∈ b" "b ∈ S"
using that
proof (induction arbitrary: b)
case (base y)
then have "C a b"
unfolding C_def by auto
then show ?case
by auto
next
case (step y z c)
then obtain b where "y ∈ b" "b ∈ S"
by (meson E_invariant.invariant_reaches tranclp_into_rtranclp)
from step.IH[OF ‹x ∈ a› ‹a ∈ S› this] have "C.reaches1 a b" .
moreover from step.prems ‹E _ _› ‹y ∈ b› ‹b ∈ S› have "C b c"
unfolding C_def by auto
finally show ?case .
qed
lemma certify_no_E1_cycle:
assumes "E.reachable x" "E.reaches1 x x"
shows "E1.reaches1 x x"
proof (rule ccontr)
assume A: "¬ E1.reaches1 x x"
with ‹E.reaches1 x x› obtain y z where "E.reaches x y" "E2 y z" "E.reaches z x"
by (fastforce dest!: non_subgraph_cycle_decomp simp: E_def)
from start ‹E.reachable x› obtain a where [intro]: "C.reachable a" "x ∈ a" "a ∈ S"
unfolding E.reachable_def C.reachable_def by (auto dest: simulation_reaches)
with ‹E.reaches x y› obtain b where "C.reaches a b" "y ∈ b" "b ∈ S"
by (auto dest: simulation_reaches)
from ‹C.reaches a b› have "C.reachable b"
by (blast intro: C.reachable_reaches)
from ‹E.reaches z x› have ‹E.reaches1 z x ∨ z = x›
by (meson rtranclpD)
then show False
proof
assume "E.reaches1 z x"
from ‹y ∈ b› ‹b ∈ S› ‹E2 y z› obtain c where "C b c" ‹z ∈ c› ‹c ∈ S›
using A_B_step[of y z b] unfolding E_def by (auto dest: C_invariant.invariant[rotated])
with no_internal_E2 ‹y ∈ _› ‹E2 y z› have "b ≠ c"
by auto
with ‹E2 y z› ‹y ∈ b› ‹z ∈ c› ‹c ∈ S› have "C b c"
unfolding C_def E_def by auto
from ‹E.reaches1 z x› ‹z ∈ c› ‹c ∈ S› ‹x ∈ a› have "C.reaches1 c a"
by (auto intro: E_C_reaches1)
with ‹C.reaches a b› have "C.reaches1 c b"
by auto
then have "C.reaches c b"
by auto
with ‹C b c› ‹b ∈ S› ‹C.reachable b› ‹b ≠ c› no_component_cycle show False
by auto
next
assume [simp]: "z = x"
with ‹y ∈ b› ‹E2 y z› ‹a ∈ S› ‹x ∈ a› have "C b a"
unfolding C_def E_def by auto
with no_internal_E2 ‹y ∈ _› ‹E2 y z› have "b ≠ a"
by auto
with ‹C.reaches a b› ‹C b a› ‹b ∈ S› ‹C.reachable b› no_component_cycle show False
by auto
qed
qed
lemma certify_no_accepting_cycle:
assumes
"∀ a ∈ S. card a > 1 ⟶ (∀ x ∈ a. ¬ F x)"
"∀ a ∈ S. ∀ x. a = {x} ⟶ (¬ F x ∨ ¬ E1 x x)"
assumes "E.reachable x" "E1.reaches1 x x"
shows "¬ F x"
proof (rule ccontr, unfold not_not)
assume "F x"
from start ‹E.reachable x› obtain a where "x ∈ a" "a ∈ S" "C.reachable a"
unfolding E.reachable_def C.reachable_def by (auto dest: simulation_reaches)
consider "card a = 0" | "card a = 1" | "card a > 1"
by force
then show False
proof cases
assume "card a = 0"
with finite ‹x ∈ a› ‹a ∈ S› show False
by auto
next
assume "card a > 1"
with ‹x ∈ a› ‹a ∈ S› assms(1) ‹F x› show False
by auto
next
assume "card a = 1"
with finite ‹x ∈ a› ‹a ∈ S› have "a = {x}"
using card_1_singletonE by blast
with ‹a ∈ S› assms(2) ‹F x› have "¬ E1 x x"
by auto
from assms(4) show False
proof (cases rule: converse_tranclpE, assumption, goal_cases)
case 1
with ‹¬ E1 x x› show ?thesis
by auto
next
case (2 y)
interpret sim: Simulation E1 E "(=)"
by (rule Subgraph_Simulation)
from ‹E1.reaches1 y x› have "E.reaches1 y x"
by (auto dest: sim.simulation_reaches1)
from ‹E1 x y› ‹¬ E1 x x› ‹a = _› ‹x ∈ a› ‹a ∈ S› obtain b where "y ∈ b" "b ∈ S" "C a b"
by (meson C_def E_def closed(1))
with ‹a = _› ‹¬ E1 x x› ‹E1 x y› have "a ≠ b"
by auto
from ‹y ∈ b› ‹b ∈ S› ‹E.reaches1 y x› ‹x ∈ a› ‹a ∈ S› have "C.reaches1 b a"
by (auto intro: E_C_reaches1)
with ‹x ∈ a› ‹a ∈ S› ‹C a b› ‹C.reachable a› ‹a ≠ b› show ?thesis
including graph_automation_aggressive using no_component_cycle by auto
qed
qed
qed
end
end
end