Theory Subsumption_Graphs
theory Subsumption_Graphs
imports
Timed_Automata.Graphs
Timed_Automata.More_List1
begin
section ‹Subsumption Graphs›
subsection ‹Preliminaries›
subsubsection ‹Transitive Closure›
context
fixes R :: "'a ⇒ 'a ⇒ bool"
assumes R_trans[intro]: "⋀ x y z. R x y ⟹ R y z ⟹ R x z"
begin
lemma rtranclp_transitive_compress1: "R a c" if "R a b" "R⇧*⇧* b c"
using that(2,1) by induction auto
lemma rtranclp_transitive_compress2: "R a c" if "R⇧*⇧* a b" "R b c"
using that by induction auto
end
lemma rtranclp_ev_induct[consumes 1, case_names irrefl trans step]:
fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
assumes reachable_finite: "finite {x. R⇧*⇧* a x}"
assumes R_irrefl: "⋀ x. ¬ R x x" and R_trans[intro]: "⋀ x y z. R x y ⟹ R y z ⟹ R x z"
assumes step: "⋀ x. R⇧*⇧* a x ⟹ P x ∨ (∃ y. R x y)"
shows "∃ x. P x ∧ R⇧*⇧* a x"
proof -
let ?S = "{y. R⇧*⇧* a y}"
from reachable_finite have "finite ?S"
by auto
then have "∃ x ∈ ?S. P x"
using step
proof (induction ?S arbitrary: a rule: finite_psubset_induct)
case psubset
let ?S = "{y. R⇧*⇧* a y}"
from psubset have "finite ?S" by auto
show ?case
proof (cases "?S = {}")
case True
then show ?thesis by auto
next
case False
then obtain y where "R⇧*⇧* a y"
by auto
from psubset(3)[OF this] show ?thesis
proof
assume "P y"
with ‹R⇧*⇧* a y› show ?thesis by auto
next
assume "∃ z. R y z"
then obtain z where "R y z" by safe
let ?T = "{y. R⇧*⇧* z y}"
from ‹R y z› ‹R⇧*⇧* a y› have "¬ R⇧*⇧* z a"
by (auto simp: R_irrefl dest!: rtranclp_transitive_compress2[of R, rotated])
then have "a ∉ ?T" by auto
moreover have "?T ⊆ ?S"
using ‹R⇧*⇧* a y› ‹R y z› by auto
ultimately have "?T ⊂ ?S"
by auto
have "P x ∨ Ex (R x)" if "R⇧*⇧* z x" for x
using that ‹R y z› ‹R⇧*⇧* a y› by (auto intro!: psubset.prems)
from psubset.hyps(2)[OF ‹?T ⊂ ?S› this] psubset.prems ‹R y z› ‹R⇧*⇧* a y› obtain w
where "R⇧*⇧* z w" "P w" by auto
with ‹R⇧*⇧* a y› ‹R y z› have "R⇧*⇧* a w" by auto
with ‹P w› show ?thesis by auto
qed
qed
qed
then show ?thesis by auto
qed
lemma rtranclp_ev_induct2[consumes 2, case_names irrefl trans step]:
fixes P Q :: "'a ⇒ bool"
assumes Q_finite: "finite {x. Q x}" and Q_witness: "Q a"
assumes R_irrefl: "⋀ x. ¬ R x x" and R_trans[intro]: "⋀ x y z. R x y ⟹ R y z ⟹ R x z"
assumes step: "⋀ x. Q x ⟹ P x ∨ (∃ y. R x y ∧ Q y)"
shows "∃ x. P x ∧ Q x ∧ R⇧*⇧* a x"
proof -
let ?R = "λ x y. R x y ∧ Q x ∧ Q y"
have [intro]: "R⇧*⇧* a x" if "?R⇧*⇧* a x" for x
using that by induction auto
have [intro]: "Q x" if "?R⇧*⇧* a x" for x
using that ‹Q a› by (auto elim: rtranclp.cases)
have "{x. ?R⇧*⇧* a x} ⊆ {x. Q x}" by auto
with ‹finite _› have "finite {x. ?R⇧*⇧* a x}" by - (rule finite_subset)
then have "∃x. P x ∧ ?R⇧*⇧* a x"
proof (induction rule: rtranclp_ev_induct)
case prems: (step x)
with step[of x] show ?case by auto
qed (auto simp: R_irrefl)
then show ?thesis by auto
qed
subsection ‹Definitions›
locale Subsumption_Graph_Pre_Defs =
ord less_eq less for less_eq :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50) and less (infix "≺" 50) +
fixes E :: "'a ⇒ 'a ⇒ bool"
begin
sublocale Graph_Defs E .
end
locale Subsumption_Graph_Pre_Nodes_Defs = Subsumption_Graph_Pre_Defs +
fixes V :: "'a ⇒ bool"
begin
sublocale Subgraph_Node_Defs_Notation .
end
locale Subsumption_Graph_Defs = Subsumption_Graph_Pre_Defs +
fixes s⇩0 :: 'a
fixes RE :: "'a ⇒ 'a ⇒ bool"
begin
sublocale Graph_Start_Defs E s⇩0 .
sublocale G: Graph_Start_Defs RE s⇩0 .
sublocale G': Graph_Start_Defs "λ x y. RE x y ∨ (x ≺ y ∧ G.reachable y)" s⇩0 .
abbreviation G'_E ("_ →⇩G⇩' _" [100, 100] 40) where
"G'_E x y ≡ RE x y ∨ (x ≺ y ∧ G.reachable y)"
notation RE ("_ →⇩G _" [100, 100] 40)
notation G.reaches ("_ →⇩G* _" [100, 100] 40)
notation G.reaches1 ("_ →⇩G⇧+ _" [100, 100] 40)
notation G'.reaches ("_ →⇩G*'' _" [100, 100] 40)
notation G'.reaches1 ("_ →⇩G⇧+'' _" [100, 100] 40)
end
locale Subsumption_Graph_Pre = Subsumption_Graph_Defs + preorder less_eq less +
assumes mono:
"a ≼ b ⟹ E a a' ⟹ reachable a ⟹ reachable b ⟹ ∃ b'. E b b' ∧ a' ≼ b'"
begin
lemmas preorder_intros = order_trans less_trans less_imp_le
end
locale Subsumption_Graph_Pre_Nodes = Subsumption_Graph_Pre_Nodes_Defs + preorder less_eq less +
assumes mono:
"a ≼ b ⟹ a → a' ⟹ V a ⟹ V b ⟹ ∃ b'. b → b' ∧ a' ≼ b'"
begin
lemmas preorder_intros = order_trans less_trans less_imp_le
end
text ‹
This is sufficient to show that if ‹→⇩G› cannot reach an accepting state,
then ‹→› cannot either.
›
locale Reachability_Compatible_Subsumption_Graph_Pre =
Subsumption_Graph_Defs + preorder less_eq less +
assumes mono:
"a ≼ b ⟹ E a a' ⟹ reachable a ∨ G.reachable a ⟹ reachable b ∨ G.reachable b
⟹ ∃ b'. E b b' ∧ a' ≼ b'"
assumes reachability_compatible:
"∀ s. G.reachable s ⟶ (∀ s'. E s s' ⟶ RE s s') ∨ (∃ t. s ≺ t ∧ G.reachable t)"
assumes finite_reachable: "finite {a. G.reachable a}"
locale Reachability_Compatible_Subsumption_Graph =
Subsumption_Graph_Defs + Subsumption_Graph_Pre +
assumes reachability_compatible:
"∀ s. G.reachable s ⟶ (∀ s'. E s s' ⟶ RE s s') ∨ (∃ t. s ≺ t ∧ G.reachable t)"
assumes subgraph: "∀ s s'. RE s s' ⟶ E s s'"
assumes finite_reachable: "finite {a. G.reachable a}"
locale Subsumption_Graph_View_Defs = Subsumption_Graph_Defs +
fixes SE :: "'a ⇒ 'a ⇒ bool"
and covered :: "'a ⇒ bool"
locale Reachability_Compatible_Subsumption_Graph_View =
Subsumption_Graph_View_Defs + Subsumption_Graph_Pre +
assumes reachability_compatible:
"∀ s. G.reachable s ⟶
(if covered s then (∃ t. SE s t ∧ G.reachable t) else (∀ s'. E s s' ⟶ RE s s'))"
assumes subsumption: "∀ s'. SE s s' ⟶ s ≺ s'"
assumes subgraph: "∀ s s'. RE s s' ⟶ E s s'"
assumes finite_reachable: "finite {a. G.reachable a}"
begin
sublocale Reachability_Compatible_Subsumption_Graph "(≼)" "(≺)" E s⇩0 RE
proof unfold_locales
have "(∀s'. E s s' ⟶ RE s s') ∨ (∃t. s ≺ t ∧ G.reachable t)" if "G.reachable s" for s
using that reachability_compatible subsumption by (cases "covered s"; fastforce)
then show "∀s. G.reachable s ⟶ (∀s'. E s s' ⟶ RE s s') ∨ (∃t. s ≺ t ∧ G.reachable t)"
by auto
qed (use subgraph in ‹auto intro: finite_reachable mono›)
end
locale Subsumption_Graph_Closure_View_Defs =
ord less_eq less for less_eq :: "'b ⇒ 'b ⇒ bool" (infix "≼" 50) and less (infix "≺" 50) +
fixes E :: "'a ⇒ 'a ⇒ bool"
and s⇩0 :: 'a
fixes RE :: "'a ⇒ 'a ⇒ bool"
fixes SE :: "'a ⇒ 'a ⇒ bool"
and covered :: "'a ⇒ bool"
fixes closure :: "'a ⇒ 'b"
fixes P :: "'a ⇒ bool"
fixes Q :: "'a ⇒ bool"
begin
sublocale Graph_Start_Defs E s⇩0 .
sublocale G: Graph_Start_Defs RE s⇩0 .
end
locale Reachability_Compatible_Subsumption_Graph_Closure_View =
Subsumption_Graph_Closure_View_Defs +
preorder less_eq less +
assumes mono:
"closure a ≼ closure b ⟹ E a a' ⟹ P a ⟹ P b ⟹ ∃ b'. E b b' ∧ closure a' ≼ closure b'"
assumes closure_eq:
"closure a = closure b ⟹ E a a' ⟹ P a ⟹ P b ⟹ ∃ b'. E b b' ∧ closure a' = closure b'"
assumes reachability_compatible:
"∀ s. Q s ⟶ (if covered s then (∃ t. SE s t ∧ G.reachable t) else (∀ s'. E s s' ⟶ RE s s'))"
assumes subsumption: "∀ s'. SE s s' ⟶ closure s ≺ closure s'"
assumes subgraph: "∀ s s'. RE s s' ⟶ E s s'"
assumes finite_closure: "finite (closure ` UNIV)"
assumes P_post: "a → b ⟹ P b"
assumes P_pre: "a → b ⟹ P a"
assumes P_s⇩0: "P s⇩0"
assumes Q_post: "RE a b ⟹ Q b"
assumes Q_s⇩0: "Q s⇩0"
begin
definition close where "close e a b = (∃ x y. e x y ∧ a = closure x ∧ b = closure y)"
lemma Simulation_close:
"Simulation A (close A) (λ a b. b = closure a)"
unfolding close_def by standard auto
sublocale view: Reachability_Compatible_Subsumption_Graph
"(≼)" "(≺)" "close E" "closure s⇩0" "close RE"
supply [simp] = close_def
supply [intro] = P_pre P_post Q_post
proof (standard, goal_cases)
case prems: (1 a b a')
then obtain x y where [simp]: "x → y" "a = closure x" "a' = closure y"
by auto
then have "P x" "P y"
by blast+
from prems(4) P_s⇩0 obtain x' where [simp]: "b = closure x'" "P x'"
unfolding Graph_Start_Defs.reachable_def by cases auto
from mono[OF ‹_ ≼ _›[simplified] ‹x → y› ‹P x› ‹P x'›] obtain b' where
"x' → b'" "closure y ≼ closure b'"
by auto
then show ?case
by auto
next
case 2
interpret Simulation RE "close RE" "λ a b. b = closure a"
by (rule Simulation_close)
{ fix x assume "Graph_Start_Defs.reachable (close RE) (closure s⇩0) x"
then obtain x' where [simp]: "x = closure x'" "Q x'" "P x'"
using Q_s⇩0 P_s⇩0 subgraph unfolding Graph_Start_Defs.reachable_def by cases auto
have "(∀s'. close E x s' ⟶ close RE x s')
∨ (∃t. x ≺ t ∧ Graph_Start_Defs.reachable (close RE) (closure s⇩0) t)"
proof (cases "covered x'")
case True
with reachability_compatible ‹Q x'› obtain t where "SE x' t" "G.reachable t"
by fastforce
then show ?thesis
using subsumption
by - (rule disjI2, auto dest: simulation_reaches simp: Graph_Start_Defs.reachable_def)
next
case False
with reachability_compatible ‹Q x'› have "∀s'. x' → s' ⟶ RE x' s'"
by auto
then show ?thesis
unfolding close_def using closure_eq[OF _ _ _ ‹P x'›] by - (rule disjI1, force)
qed
}
then show ?case
by (intro allI impI)
next
case 3
then show ?case
using subgraph by auto
next
case 4
have "{a. Graph_Start_Defs.reachable (close RE) (closure s⇩0) a} ⊆ closure ` UNIV"
by (smt (z3) Graph_Start_Defs.reachable_induct close_def full_SetCompr_eq mem_Collect_eq subsetI)
also have "finite …"
by (rule finite_closure)
finally show ?case .
qed
end
locale Reachability_Compatible_Subsumption_Graph_Final = Reachability_Compatible_Subsumption_Graph +
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "F a ⟹ a ≼ b ⟹ F b"
locale Liveness_Compatible_Subsumption_Graph = Reachability_Compatible_Subsumption_Graph_Final +
assumes no_subsumption_cycle:
"G'.reachable x ⟹ x →⇩G⇧+' x ⟹ x →⇩G⇧+ x"
subsection ‹Reachability›
context Subsumption_Graph_Defs
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemma G'_reachable_G_reachable[intro]:
"G.reachable a" if "G'.reachable a"
using that by (induction; blast)
lemma G_reachable_G'_reachable[intro]:
"G'.reachable a" if "G.reachable a"
using that by (induction; blast)
lemma G_G'_reachable_iff:
"G.reachable a ⟷ G'.reachable a"
by blast
end
end
context Reachability_Compatible_Subsumption_Graph_Pre
begin
lemmas preorder_intros = order_trans less_trans less_imp_le
lemma G'_finite_reachable: "finite {a. G'.reachable a}"
by (blast intro: finite_subset[OF _ finite_reachable])
lemma G_reachable_has_surrogate:
"∃ t. G.reachable t ∧ s ≼ t ∧ (∀ s'. E t s' ⟶ RE t s')" if "G.reachable s"
proof -
note [intro] = preorder_intros
from finite_reachable ‹G.reachable s› obtain x where
"∀s'. E x s' ⟶ RE x s'" "G.reachable x" "((≺)⇧*⇧*) s x"
apply atomize_elim
apply (induction rule: rtranclp_ev_induct2)
using reachability_compatible by auto
moreover from ‹((≺)⇧*⇧*) s x› have "s ≺ x ∨ s = x"
by induction auto
ultimately show ?thesis
by auto
qed
lemma reachable_has_surrogate:
"∃ t. G.reachable t ∧ s ≼ t ∧ (∀ s'. E t s' ⟶ RE t s')" if "reachable s"
using that
proof induction
case start
have "G.reachable s⇩0"
by auto
then show ?case
by (rule G_reachable_has_surrogate)
next
case (step a b)
then obtain t where *: "G.reachable t" "a ≼ t" "(∀s'. t → s' ⟶ t →⇩G s')"
by auto
from mono[OF ‹a ≼ t› ‹a → b›] ‹reachable a› ‹G.reachable t› obtain b' where
"t → b'" "b ≼ b'"
by auto
with G_reachable_has_surrogate[of b'] * show ?case
by (auto intro: preorder_intros G.reachable_step)
qed
context
fixes F :: "'a ⇒ bool"
assumes F_mono[intro]: "F a ⟹ a ≼ b ⟹ F b"
begin
corollary reachability_correct:
"∄ s'. reachable s' ∧ F s'" if "∄ s'. G.reachable s' ∧ F s'"
using that by (auto dest!: reachable_has_surrogate)
end
end
context Reachability_Compatible_Subsumption_Graph
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemma subgraph'[intro]:
"E s s'" if "RE s s'"
using that subgraph by blast
lemma G_reachability_sound[intro]:
"reachable a" if "G.reachable a"
using that by (induction; blast)
lemma G_steps_sound[intro]:
"steps xs" if "G.steps xs"
using that by (induction; blast)
lemma G_run_sound[intro]:
"run xs" if "G.run xs"
using that by (coinduction arbitrary: xs) (auto 4 3 elim: G.run.cases)
lemma G'_reachability_sound[intro]:
"reachable a" if "G'.reachable a"
using that by (induction; blast)
lemma G'_finite_reachable: "finite {a. G'.reachable a}"
by (blast intro: finite_subset[OF _ finite_reachable])
lemma G_steps_G'_steps[intro]:
"G'.steps as" if "G.steps as"
using that by induction auto
lemma reachable_has_surrogate:
"∃ t. G.reachable t ∧ s ≼ t ∧ (∀ s'. E t s' ⟶ RE t s')" if "G.reachable s"
proof -
note [intro] = preorder_intros
from finite_reachable ‹G.reachable s› obtain x where
"∀s'. E x s' ⟶ RE x s'" "G.reachable x" "((≺)⇧*⇧*) s x"
apply atomize_elim
apply (induction rule: rtranclp_ev_induct2)
using reachability_compatible by auto
moreover from ‹((≺)⇧*⇧*) s x› have "s ≺ x ∨ s = x"
by induction auto
ultimately show ?thesis
by auto
qed
lemma reachable_has_surrogate':
"∃ t. s ≼ t ∧ s →⇩G*' t ∧ (∀ s'. E t s' ⟶ RE t s')" if "G.reachable s"
proof -
note [intro] = preorder_intros
from ‹G.reachable s› have ‹G.reachable s› by auto
from finite_reachable this obtain x where
real_edges: "∀s'. E x s' ⟶ RE x s'" and "G.reachable x" "((≺)⇧*⇧*) s x"
apply atomize_elim
apply (induction rule: rtranclp_ev_induct2)
using reachability_compatible by auto
from ‹((≺)⇧*⇧*) s x› have "s ≺ x ∨ s = x"
by induction auto
then show ?thesis
proof
assume "s ≺ x"
with real_edges ‹G.reachable x› show ?thesis
by (inst_existentials "x") auto
next
assume "s = x"
with real_edges show ?thesis
by (inst_existentials "s") auto
qed
qed
lemma subsumption_step:
"∃ a'' b'. a' ≼ a'' ∧ b ≼ b' ∧ a'' →⇩G b' ∧ G.reachable a''" if
"reachable a" "E a b" "G.reachable a'" "a ≼ a'"
proof -
note [intro] = preorder_intros
from mono[OF ‹a ≼ a'› ‹E a b› ‹reachable a›] ‹G.reachable a'› obtain b' where "E a' b'" "b ≼ b'"
by auto
from reachable_has_surrogate[OF ‹G.reachable a'›] obtain a''
where "a' ≼ a''" "G.reachable a''" and *: "∀ s'. E a'' s' ⟶ RE a'' s'"
by auto
from mono[OF ‹a' ≼ a''› ‹E a' b'›] ‹G.reachable a'› ‹G.reachable a''› obtain b'' where
"E a'' b''" "b' ≼ b''"
by auto
with * ‹a' ≼ a''› ‹b ≼ b'› ‹G.reachable a''› show ?thesis
by auto
qed
lemma subsumption_step':
"∃ b'. b ≼ b' ∧ a' →⇩G⇧+' b'" if "reachable a" "a → b" "G'.reachable a'" "a ≼ a'"
proof -
note [intro] = preorder_intros
from mono[OF ‹a ≼ a'› ‹E a b› ‹reachable a›] ‹G'.reachable a'› obtain b' where
"b ≼ b'" "a' → b'"
by auto
from reachable_has_surrogate'[of a'] ‹G'.reachable a'› obtain a'' where *:
"a' ≼ a''" "a' →⇩G*' a''" "∀s'. a'' → s' ⟶ a'' →⇩G s'"
by auto
with ‹G'.reachable a'› have "G'.reachable a''"
by blast
with mono[OF ‹a' ≼ a''› ‹E a' b'›] ‹G'.reachable a'› obtain b'' where
"b' ≼ b''" "a'' → b''"
by auto
with * ‹b ≼ b'› ‹b' ≼ b''› ‹G'.reachable a''› show ?thesis
by (auto simp: G'.reaches1_reaches_iff2)
qed
theorem reachability_complete':
"∃ s'. s ≼ s' ∧ G.reachable s'" if "a →* s" "G.reachable a"
using that
proof (induction)
case base
then show ?case by auto
next
case (step s t)
then obtain s' where "s ≼ s'" "G.reachable s'"
by auto
with step(4) have "reachable a" "G.reachable s'"
by auto
with step(1) have "reachable s"
by auto
from subsumption_step[OF ‹reachable s› ‹E s t› ‹G.reachable s'› ‹s ≼ s'›] obtain s'' t' where
"s' ≼ s''" "t ≼ t'" "s'' →⇩G t'" "G.reachable s''"
by atomize_elim
with ‹G.reachable s'› show ?case
by auto
qed
theorem steps_complete':
"∃ ys. list_all2 (≼) xs ys ∧ G.steps (a # ys)" if
"steps (a # xs)" "G.reachable a"
using that
proof (induction "a # xs" arbitrary: a xs rule: steps_alt_induct)
case (Single x)
then show ?case by auto
oops
theorem steps_complete':
"∃ c ys. list_all2 (≼) xs ys ∧ G.steps (c # ys) ∧ b ≼ c" if
"steps (a # xs)" "reachable a" "a ≼ b" "G.reachable b"
oops
theorem run_complete':
"∃ ys. stream_all2 (≼) xs ys ∧ G.run (a ## ys)" if "run (a ## xs)" "G.reachable a"
proof -
define f where "f = (λ x b. SOME y. x ≼ y ∧ RE b y)"
define gen where "gen a xs = sscan f xs a" for a xs
have gen_ctr: "gen x xs = f (shd xs) x ## gen (f (shd xs) x) (stl xs)" for x xs
unfolding gen_def by (subst sscan.ctr) (rule HOL.refl)
from that have "G.run (gen a xs)"
proof (coinduction arbitrary: a xs)
case run
then show ?case
apply (cases xs)
apply auto
apply (subst gen_ctr)
apply simp
apply (subst gen_ctr)
apply simp
apply rule
oops
corollary reachability_complete:
"∃ s'. s ≼ s' ∧ G.reachable s'" if "reachable s"
using reachability_complete'[of s⇩0 s] that unfolding reachable_def by auto
corollary reachability_correct:
"(∃ s'. s ≼ s' ∧ reachable s') ⟷ (∃ s'. s ≼ s' ∧ G.reachable s')"
by (blast dest: reachability_complete intro: preorder_intros)
lemma steps_G'_steps:
"∃ ys ns. list_all2 (≼) xs (nths ys ns) ∧ G'.steps (b # ys)" if
"steps (a # xs)" "reachable a" "a ≼ b" "G'.reachable 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 ‹reachable x› ‹E x y› _ ‹x ≼ b›] ‹G'.reachable b› obtain b' where
"y ≼ b'" "b →⇩G⇧+' b'"
by auto
with ‹reachable x› Cons.hyps(1) Cons.prems(3) obtain ys ns where
"list_all2 (≼) xs (nths ys ns)" "G'.steps (b' # ys)"
by atomize_elim (blast intro: Cons.hyps(3)[OF _ ‹y ≼ b'›] intro: graphI_aggressive)
from ‹b →⇩G⇧+' b'› this(2) obtain as where
"G'.steps (b # as @ b' # ys)"
by (fastforce intro: G'.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'_cycle'':
assumes "steps (s⇩0 # ws @ x # xs @ [x])"
shows "∃ x' xs' ys'. x ≼ x' ∧ G'.steps (s⇩0 # xs' @ x' # ys' @ [x'])"
proof -
let ?n = "card {x. G'.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'_steps[OF this, of s⇩0] obtain ys ns where ys:
"list_all2 (≼) (ws @ x # concat (replicate ?n (xs @ [x]))) (nths ys ns)"
"G'.steps (s⇩0 # ys)"
by auto
then obtain x' ys' ns' ws' where ys':
"G'.steps (x' # ys')" "G'.steps (s⇩0 # ws' @ [x'])"
"list_all2 (≼) (concat (replicate ?n (xs @ [x]))) (nths ys' ns')"
apply atomize_elim
apply auto
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'.graphI_aggressive2)
subgoal premises prems
proof -
from prems have "G'.steps ((s⇩0 # ys4 @ ys6 @ [z]) @ ys7)"
by auto
moreover then have "G'.steps (s⇩0 # ys4 @ ys6 @ [z])"
by (auto intro: G'.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'.steps (s⇩0 # ws' @ [x'])› have "G'.reachable x'"
by - (rule G'.reachable_reaches, auto)
have "set ?ys ⊆ set ys'"
by auto
also have "… ⊆ {x. G'.reachable x}"
using ‹G'.steps (x' # _)› ‹G'.reachable x'›
by clarsimp (rule G'.reachable_steps_elem[rotated], assumption, auto)
finally have "¬ distinct ?ys"
using distinct_card[of ?ys] ‹_ >= ?n›
by - (rule ccontr; drule distinct_length_le[OF G'_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'.steps (y # bs' @ [y])"
proof -
from ‹G'.steps (x' # _)› ‹ys' = _› show ?thesis
by (force intro: G'.graphI_aggressive2)
qed
moreover have "G'.steps (s⇩0 # ws' @ x' # as' @ [y])"
proof -
from ‹G'.steps (x' # ys')› ‹ys' = _› have "G'.steps (x' # as' @ [y])"
by (force intro: G'.graphI_aggressive2)
with ‹G'.steps (s⇩0 # ws' @ [x'])› show ?thesis
by (fastforce intro: G'.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'.graphI_aggressive1)
qed
lemma cycle_G'_cycle':
assumes "steps (s⇩0 # ws @ x # xs @ [x])"
shows "∃ y ys. x ≼ y ∧ G'.steps (y # ys @ [y]) ∧ G'.reachable y"
proof -
from cycle_G'_cycle''[OF assms] obtain x' xs' ys' where
"x ≼ x'" "G'.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'.graphI_aggressive2)
by (rule G'.reachable_reaches, auto intro: G'.graphI_aggressive2)
qed
lemma cycle_G'_cycle:
assumes "reachable x" "x →⇧+ x"
shows "∃ y ys. x ≼ y ∧ G'.reachable y ∧ y →⇩G⇧+' 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'_cycle'[OF this] show ?thesis
by (auto intro: G'.graphI_aggressive2)
qed
corollary G'_reachability_complete:
"∃ s'. s ≼ s' ∧ G.reachable s'" if "G'.reachable s"
using reachability_complete that by auto
end
end
corollary (in Reachability_Compatible_Subsumption_Graph_Final) reachability_correct:
"(∃ s'. reachable s' ∧ F s') ⟷ (∃ s'. G.reachable s' ∧ F s')"
using reachability_complete by blast
subsection ‹Liveness›
theorem (in Liveness_Compatible_Subsumption_Graph) cycle_iff:
"(∃ x. x →⇧+ x ∧ reachable x ∧ F x) ⟷ (∃ x. x →⇩G⇧+ x ∧ G.reachable x ∧ F x)"
by (auto 4 4 intro: no_subsumption_cycle steps_reaches1 dest: cycle_G'_cycle G.graphD)
subsection ‹Appendix›
context Subsumption_Graph_Pre_Nodes
begin
text ‹Setup for automation›
context
includes graph_automation
begin
lemma steps_mono:
assumes "G'.steps (x # xs)" "x ≼ y" "V x" "V y"
shows "∃ ys. G'.steps (y # ys) ∧ list_all2 (≼) xs ys"
using assms including subgraph_automation
proof (induction "x # xs" arbitrary: x y xs)
case (Single x)
then show ?case by auto
next
case (Cons x y xs x')
from mono[OF ‹x ≼ x'›] ‹x → y› Cons.prems obtain y' where "x' → y'" "y ≼ y'"
by auto
with Cons.hyps(3)[OF ‹y ≼ y'›] ‹x → y› Cons.prems obtain ys where
"G'.steps (y' # ys)" "list_all2 (≼) xs ys"
by auto
with ‹x' → y'› ‹y ≼ y'› show ?case
by auto
qed
lemma steps_append_subsumption:
assumes "G'.steps (x # xs)" "G'.steps (y # ys)" "y ≼ last (x # xs)" "V x" "V y"
shows "∃ ys'. G'.steps (x # xs @ ys') ∧ list_all2 (≼) ys ys'"
proof -
from assms have "V (last (x # xs))"
by - (rule G'_steps_V_last, auto)
from steps_mono[OF ‹G'.steps (y # ys)› ‹y ≼ _› ‹V y› this] obtain ys' where
"G'.steps (last (x # xs) # ys')" "list_all2 (≼) ys ys'"
by auto
with G'.steps_append[OF ‹G'.steps (x # xs)› this(1)] show ?thesis
by auto
qed
lemma steps_replicate_subsumption:
assumes "x ≼ last (x # xs)" "G'.steps (x # xs)" "n > 0" "V x"
notes [intro] = preorder_intros
shows "∃ ys. G'.steps (x # ys) ∧ list_all2 (≼) (concat (replicate n xs)) ys"
using assms
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
show ?case
proof (cases n)
case 0
with Suc.prems show ?thesis
by (inst_existentials xs) (auto intro: list_all2_refl)
next
case prems: (Suc n')
with Suc ‹n = _› obtain ys where ys:
"list_all2 (≼) (concat (replicate n xs)) ys" "G'.steps (x # ys)"
by auto
with ‹n = _› have "list_all2 (≼) (concat (replicate n' xs) @ xs) ys"
by (metis append_Nil2 concat.simps(1,2) concat_append replicate_Suc replicate_append_same)
with ‹x ≼ _› have "x ≼ last (x # ys)"
by (cases xs; auto 4 3 dest: list_all2_last split: if_split_asm)
from steps_append_subsumption[OF ‹G'.steps (x # ys)› ‹G'.steps (x # xs)› this] ‹V x› obtain
ys' where "G'.steps (x # ys @ ys')" "list_all2 (≼) xs ys'"
by auto
with ys(1) ‹n = _› show ?thesis
apply (inst_existentials "ys @ ys'")
by auto
(metis
append_Nil2 concat.simps(1,2) concat_append list_all2_appendI replicate_Suc
replicate_append_same
)
qed
qed
context
assumes finite_V: "finite {x. V x}"
begin
lemma wf_less_on_reachable_set:
assumes antisym: "⋀ x y. x ≼ y ⟹ y ≼ x ⟹ x = y"
shows "wf {(x, y). y ≺ x ∧ V x ∧ V y}" (is "wf ?S")
proof (rule finite_acyclic_wf)
have "?S ⊆ {(x, y). V x ∧ V y}"
by auto
also have "finite …"
using finite_V by auto
finally show "finite ?S" .
next
interpret order by unfold_locales (rule antisym)
show "acyclicP (λx y. y ≺ x ∧ V x ∧ V y)"
by (rule acyclicI_order[where f = id]) auto
qed
text ‹
This shows that looking for cycles and pre-cycles is equivalent in monotone subsumption graphs.
›
lemma pre_cycle_cycle':
assumes A: "x ≼ x'" "G'.steps (x # xs @ [x'])" "V x"
shows "∃ x'' ys. x' ≼ x'' ∧ G'.steps (x'' # ys @ [x'']) ∧ V x''"
proof -
let ?n = "card {x. V x} + 1"
let ?xs = "concat (replicate ?n (xs @ [x']))"
from steps_replicate_subsumption[OF _ ‹G'.steps _›, of ?n] ‹V x› ‹x ≼ x'› obtain ys where
"G'.steps (x # ys)" "list_all2 (≼) ?xs ys"
by auto
let ?ys = "filter ((≼) x') ys"
have "length ?ys ≥ ?n"
using list_all2_replicate_elem_filter[OF ‹list_all2 (≼) ?xs ys›, of x']
by auto
have "set ?ys ⊆ set ys"
by auto
also have "… ⊆ {x. V x}"
using G'_steps_V_all[OF ‹G'.steps (x # ys)›] ‹V x› unfolding list_all_iff by auto
finally have "¬ distinct ?ys"
using distinct_card[of ?ys] ‹_ >= ?n›
by - (rule ccontr, drule distinct_length_le[OF finite_V], auto)
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'.steps (y # bs' @ [y])"
proof -
from ‹G'.steps (x # ys)› ‹ys = _› have "G'.steps (x # as' @ (y # bs' @ [y]) @ cs')"
by auto
then show ?thesis
by - ((simp; fail) | drule G'.stepsD)+
qed
moreover have "V y"
proof -
from ‹G'.steps (x # ys)› ‹ys = _› have "G'.steps ((x # as' @ [y]) @ (bs' @ y # cs'))"
by simp
then have "G'.steps (x # as' @ [y])"
by (blast dest: G'.stepsD)
with ‹V x› show ?thesis
by (auto dest: G'_steps_V_last)
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 auto
qed
lemma pre_cycle_cycle:
"(∃ x x'. V x ∧ x →⇧+ x' ∧ x ≼ x') ⟷ (∃ x. V x ∧ x →⇧+ x)"
including reaches_steps_iff by (force dest: pre_cycle_cycle')
lemma pre_cycle_cycle_reachable:
"(∃ x x'. a⇩0 →* x ∧ V x ∧ x →⇧+ x' ∧ x ≼ x') ⟷ (∃ x. a⇩0 →* x ∧ V x ∧ x →⇧+ x)"
proof -
interpret interp: Subsumption_Graph_Pre_Nodes _ _ E "λ x. a⇩0 →* x ∧ V x"
including graph_automation_aggressive
by standard (drule mono, auto 4 3 simp: Subgraph_Node_Defs.E'_def E'_def)
interpret start: Graph_Start_Defs E' a⇩0 .
have *: "start.reachable_subgraph.E' = interp.E'"
unfolding interp.E'_def start.reachable_subgraph.E'_def
unfolding start.reachable_def E'_def
by auto
have *: "start.reachable_subgraph.G'.reaches1 = interp.G'.reaches1"
unfolding tranclp_def * ..
have *: "interp.G'.reaches1 x y ⟷ x →⇧+ y" if "a⇩0 →* x" for x y
using start.reachable_reaches1_equiv[of x y] that unfolding * by (simp add: start.reachable_def)
from interp.pre_cycle_cycle finite_V show ?thesis
by (auto simp: *)
qed
end
end
end
context Subsumption_Graph_Pre
begin
text ‹Setup for automation›
context
includes graph_automation
begin
interpretation Subsumption_Graph_Pre_Nodes _ _ E reachable
apply standard
apply (drule mono)
apply (simp_all add: Subgraph_Node_Defs.E'_def)
apply force
by auto
lemma steps_mono:
assumes "steps (x # xs)" "x ≼ y" "reachable x" "reachable y"
shows "∃ ys. steps (y # ys) ∧ list_all2 (≼) xs ys"
using assms steps_mono by (simp add: reachable_steps_equiv)
lemma steps_append_subsumption:
assumes "steps (x # xs)" "steps (y # ys)" "y ≼ last (x # xs)" "reachable x" "reachable y"
shows "∃ ys'. steps (x # xs @ ys') ∧ list_all2 (≼) ys ys'"
using assms steps_append_subsumption by (simp add: reachable_steps_equiv)
lemma steps_replicate_subsumption:
assumes "x ≼ last (x # xs)" "steps (x # xs)" "n > 0" "reachable x"
notes [intro] = preorder_intros
shows "∃ ys. steps (x # ys) ∧ list_all2 (≼) (concat (replicate n xs)) ys"
using assms steps_replicate_subsumption by (simp add: reachable_steps_equiv)
context
assumes finite_reachable: "finite {x. reachable x}"
begin
lemma wf_less_on_reachable_set:
assumes antisym: "⋀ x y. x ≼ y ⟹ y ≼ x ⟹ x = y"
shows "wf {(x, y). y ≺ x ∧ reachable x ∧ reachable y}" (is "wf ?S")
proof (rule finite_acyclic_wf)
have "?S ⊆ {(x, y). reachable x ∧ reachable y}"
by auto
also have "finite …"
using finite_reachable by auto
finally show "finite ?S" .
next
interpret order by standard (rule antisym)
show "acyclicP (λx y. y ≺ x ∧ reachable x ∧ reachable y)"
by (rule acyclicI_order[where f = id]) auto
qed
text ‹
This shows that looking for cycles and pre-cycles is equivalent in monotone subsumption graphs.
›
lemma pre_cycle_cycle':
assumes A: "x ≼ x'" "steps (x # xs @ [x'])" "reachable x"
shows "∃ x'' ys. x' ≼ x'' ∧ steps (x'' # ys @ [x'']) ∧ reachable x''"
using assms pre_cycle_cycle'[OF finite_reachable] reachable_steps_equiv by meson
lemma pre_cycle_cycle:
"(∃ x x'. reachable x ∧ reaches x x' ∧ x ≼ x') ⟷ (∃ x. reachable x ∧ reaches x x)"
including reaches_steps_iff by (force dest: pre_cycle_cycle')
end
end
end
context Subsumption_Graph_Defs
begin
sublocale G'': Graph_Start_Defs "λ x y. ∃ z. G.reachable z ∧ x ≼ z ∧ RE z y" s⇩0 .
lemma G''_reachable_G'[intro]:
"G'.reachable x" if "G''.reachable x"
using that
unfolding G'.reachable_def G''.reachable_def G_G'_reachable_iff Graph_Start_Defs.reachable_def
proof (induction)
case base
then show ?case
by blast
next
case (step y z)
then obtain z' where
"RE⇧*⇧* s⇩0 z'" "y ≼ z'" "RE z' z"
by auto
from this(1) have "(λx y. RE x y ∨ x ≺ y ∧ RE⇧*⇧* s⇩0 y)⇧*⇧* s⇩0 z'"
by (induction; blast intro: rtranclp.intros(2))
with ‹RE z' z› show ?case
by (blast intro: rtranclp.intros(2))
qed
end
locale Reachability_Compatible_Subsumption_Graph_Total = Reachability_Compatible_Subsumption_Graph +
assumes total: "reachable a ⟹ reachable b ⟹ a ≼ b ∨ b ≼ a"
begin
sublocale G''_pre: Subsumption_Graph_Pre "(≼)" "(≺)" "λ x y. ∃ z. G.reachable z ∧ x ≼ z ∧ RE z y"
proof (standard, safe, goal_cases)
case prems: (1 a b a' z)
show ?case
proof (cases "b ≼ z")
case True
with prems show ?thesis
by auto
next
case False
with total[of b z] prems have "z ≼ b"
by auto
with subsumption_step[of z a' b] prems obtain a'' b' where
"b ≼ a''" "a' ≼ b'" "RE a'' b'" "G.reachable a''"
by auto
then show ?thesis
by (inst_existentials b' a'') auto
qed
qed
end
subsection ‹Old Material›
locale Reachability_Compatible_Subsumption_Graph' = Subsumption_Graph_Defs + order "(≼)" "(≺)" +
assumes reachability_compatible:
"∀ s. G.reachable s ⟶ (∀ s'. E s s' ⟶ RE s s') ∨ (∃ t. s ≺ t ∧ G.reachable t)"
assumes subgraph: "∀ s s'. RE s s' ⟶ E s s'"
assumes finite_reachable: "finite {a. G.reachable a}"
assumes mono:
"a ≼ b ⟹ E a a' ⟹ reachable a ⟹ G.reachable b ⟹ ∃ b'. E b b' ∧ a' ≼ b'"
begin
text ‹Setup for automation›
context
includes graph_automation
notes [intro] = order.trans
begin
lemma subgraph'[intro]:
"E s s'" if "RE s s'"
using that subgraph by blast
lemma G_reachability_sound[intro]:
"reachable a" if "G.reachable a"
using that unfolding reachable_def G.reachable_def by (induction; blast intro: rtranclp.intros(2))
lemma G_steps_sound[intro]:
"steps xs" if "G.steps xs"
using that by induction auto
lemma G_run_sound[intro]:
"run xs" if "G.run xs"
using that by (coinduction arbitrary: xs) (auto 4 3 elim: G.run.cases)
lemma reachable_has_surrogate:
"∃ t. G.reachable t ∧ s ≼ t ∧ (∀ s'. E t s' ⟶ RE t s')" if "G.reachable s"
using that
proof -
from finite_reachable ‹G.reachable s› obtain x where
"∀s'. E x s' ⟶ RE x s'" "G.reachable x" "((≺)⇧*⇧*) s x"
apply atomize_elim
apply (induction rule: rtranclp_ev_induct2)
using reachability_compatible by auto
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' ∧ RE a'' b' ∧ G.reachable a''" if
"reachable a" "E a b" "G.reachable a'" "a ≼ a'"
proof -
from mono[OF ‹a ≼ a'› ‹E a b› ‹reachable a› ‹G.reachable a'›] obtain b' where "E a' b'" "b ≼ b'"
by auto
from reachable_has_surrogate[OF ‹G.reachable a'›] obtain a''
where "a' ≼ a''" "G.reachable a''" and *: "∀ s'. E a'' s' ⟶ RE a'' s'"
by auto
from mono[OF ‹a' ≼ a''› ‹E a' b'›] ‹G.reachable a'› ‹G.reachable a''› obtain b'' where
"E a'' b''" "b' ≼ b''"
by auto
with * ‹a' ≼ a''› ‹b ≼ b'› ‹G.reachable a''› show ?thesis by auto
qed
theorem reachability_complete':
"∃ s'. s ≼ s' ∧ G.reachable s'" if "E⇧*⇧* a s" "G.reachable a"
using that
proof (induction)
case base
then show ?case by auto
next
case (step s t)
then obtain s' where "s ≼ s'" "G.reachable s'"
by auto
with step(4) have "reachable a" "G.reachable s'"
by auto
with step(1) have "reachable s"
by (auto simp: reachable_def)
from subsumption_step[OF ‹reachable s› ‹E s t› ‹G.reachable s'› ‹s ≼ s'›] obtain s'' t' where
"s' ≼ s''" "t ≼ t'" "s'' →⇩G t'" "G.reachable s''"
by atomize_elim
with ‹G.reachable s'› show ?case
by (auto simp: reachable_def)
qed
theorem steps_complete':
"∃ ys. list_all2 (≼) xs ys ∧ G.steps (a # ys)" if
"steps (a # xs)" "G.reachable a"
using that
proof (induction "a # xs" arbitrary: a xs rule: steps_alt_induct)
case (Single x)
then show ?case by auto
oops
theorem steps_complete':
"∃ c ys. list_all2 (≼) xs ys ∧ G.steps (c # ys) ∧ b ≼ c" if
"steps (a # xs)" "reachable a" "a ≼ b" "G.reachable b"
using that
proof (induction "a # xs" arbitrary: a b xs)
case (Single x)
then show ?case by auto
next
case (Cons x y xs)
from subsumption_step[OF ‹reachable x› ‹E _ _› ‹G.reachable b› ‹x ≼ b›] obtain b' y' where
"b ≼ b'" "y ≼ y'" "b' →⇩G y'" "G.reachable b'"
by atomize_elim
with Cons obtain y'' ys where "list_all2 (≼) xs ys" "G.steps (y'' # ys)" "y' ≼ y''"
oops
theorem run_complete':
"∃ ys. stream_all2 (≼) xs ys ∧ G.run (a ## ys)" if "run (a ## xs)" "G.reachable a"
proof -
define f where "f = (λ x b. SOME y. x ≼ y ∧ RE b y)"
define gen where "gen a xs = sscan f xs a" for a xs
have gen_ctr: "gen x xs = f (shd xs) x ## gen (f (shd xs) x) (stl xs)" for x xs
unfolding gen_def by (subst sscan.ctr) (rule HOL.refl)
from that have "G.run (gen a xs)"
proof (coinduction arbitrary: a xs)
case run
then show ?case
apply (cases xs)
apply auto
apply (subst gen_ctr)
apply simp
apply (subst gen_ctr)
apply simp
apply rule
oops
corollary reachability_complete:
"∃ s'. s ≼ s' ∧ G.reachable s'" if "reachable s"
using reachability_complete'[of s⇩0 s] that unfolding reachable_def by auto
corollary reachability_correct:
"(∃ s'. s ≼ s' ∧ reachable s') ⟷ (∃ s'. s ≼ s' ∧ G.reachable s')"
using reachability_complete by blast
lemma G'_reachability_sound[intro]:
"reachable a" if "G'.reachable a"
using that by induction auto
corollary G'_reachability_complete:
"∃ s'. s ≼ s' ∧ G.reachable s'" if "G'.reachable s"
using reachability_complete that by auto
end
end
end