Theory Timed_Automata.Graphs
chapter ‹Graphs›
theory Graphs
imports
More_List Stream_More
"HOL-Library.Rewrite"
begin
section ‹Basic Definitions and Theorems›
locale Graph_Defs =
fixes E :: "'a ⇒ 'a ⇒ bool"
begin
inductive steps where
Single: "steps [x]" |
Cons: "steps (x # y # xs)" if "E x y" "steps (y # xs)"
lemmas [intro] = steps.intros
lemma steps_append:
"steps (xs @ tl ys)" if "steps xs" "steps ys" "last xs = hd ys"
using that by induction (auto 4 4 elim: steps.cases)
lemma steps_append':
"steps xs" if "steps as" "steps bs" "last as = hd bs" "as @ tl bs = xs"
using steps_append that by blast
coinductive run where
"run (x ## y ## xs)" if "E x y" "run (y ## xs)"
lemmas [intro] = run.intros
lemma steps_appendD1:
"steps xs" if "steps (xs @ ys)" "xs ≠ []"
using that proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case
by - (cases xs; auto elim: steps.cases)
qed
lemma steps_appendD2:
"steps ys" if "steps (xs @ ys)" "ys ≠ []"
using that by (induction xs) (auto elim: steps.cases)
lemma steps_appendD3:
"steps (xs @ [x]) ∧ E x y" if "steps (xs @ [x, y])"
using that proof (induction xs)
case Nil
then show ?case by (auto elim!: steps.cases)
next
case prems: (Cons a xs)
then show ?case by (cases xs) (auto elim: steps.cases)
qed
lemma steps_ConsD:
"steps xs" if "steps (x # xs)" "xs ≠ []"
using that by (auto elim: steps.cases)
lemmas stepsD = steps_ConsD steps_appendD1 steps_appendD2
lemma steps_alt_induct[consumes 1, case_names Single Snoc]:
assumes
"steps x" "(⋀x. P [x])"
"⋀y x xs. E y x ⟹ steps (xs @ [y]) ⟹ P (xs @ [y]) ⟹ P (xs @ [y,x])"
shows "P x"
using assms(1)
proof (induction rule: rev_induct)
case Nil
then show ?case by (auto elim: steps.cases)
next
case prems: (snoc x xs)
then show ?case by (cases xs rule: rev_cases) (auto intro: assms(2,3) dest!: steps_appendD3)
qed
lemma steps_appendI:
"steps (xs @ [x, y])" if "steps (xs @ [x])" "E x y"
using that
proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case by (cases xs; auto elim: steps.cases)
qed
lemma steps_append_single:
assumes
"steps xs" "E (last xs) x" "xs ≠ []"
shows "steps (xs @ [x])"
using assms(3,1,2) by (induction xs rule: list_nonempty_induct) (auto 4 4 elim: steps.cases)
lemma extend_run:
assumes
"steps xs" "E (last xs) x" "run (x ## ys)" "xs ≠ []"
shows "run (xs @- x ## ys)"
using assms(4,1-3) by (induction xs rule: list_nonempty_induct) (auto 4 3 elim: steps.cases)
lemma run_cycle:
assumes "steps xs" "E (last xs) (hd xs)" "xs ≠ []"
shows "run (cycle xs)"
using assms proof (coinduction arbitrary: xs)
case run
then show ?case
apply (rewrite at ‹cycle xs› stream.collapse[symmetric])
apply (rewrite at ‹stl (cycle xs)› stream.collapse[symmetric])
apply clarsimp
apply (erule steps.cases)
subgoal for x
apply (rule conjI)
apply (simp; fail)
apply (rule disjI1)
apply (inst_existentials xs)
apply (simp, metis cycle_Cons[of x "[]", simplified])
by auto
subgoal for x y xs'
apply (rule conjI)
apply (simp; fail)
apply (rule disjI1)
apply (inst_existentials "y # xs' @ [x]")
using steps_append_single[of "y # xs'" x]
apply (auto elim: steps.cases split: if_split_asm simp: cycle_Cons)
done
done
qed
lemma run_stl:
"run (stl xs)" if "run xs"
using that by (auto elim: run.cases)
lemma run_sdrop:
"run (sdrop n xs)" if "run xs"
using that by (induction n arbitrary: xs) (auto intro: run_stl)
lemma run_reachable':
assumes "run (x ## xs)" "E⇧*⇧* x⇩0 x"
shows "pred_stream (λ x. E⇧*⇧* x⇩0 x) xs"
using assms by (coinduction arbitrary: x xs) (auto 4 3 elim: run.cases)
lemma run_reachable:
assumes "run (x⇩0 ## xs)"
shows "pred_stream (λ x. E⇧*⇧* x⇩0 x) xs"
by (rule run_reachable'[OF assms]) blast
lemma run_decomp:
assumes "run (xs @- ys)" "xs ≠ []"
shows "steps xs ∧ run ys ∧ E (last xs) (shd ys)"
using assms(2,1) proof (induction xs rule: list_nonempty_induct)
case (single x)
then show ?case by (auto elim: run.cases)
next
case (cons x xs)
then show ?case by (cases xs; auto 4 4 elim: run.cases)
qed
lemma steps_decomp:
assumes "steps (xs @ ys)" "xs ≠ []" "ys ≠ []"
shows "steps xs ∧ steps ys ∧ E (last xs) (hd ys)"
using assms(2,1,3) proof (induction xs rule: list_nonempty_induct)
case (single x)
then show ?case by (auto elim: steps.cases)
next
case (cons x xs)
then show ?case by (cases xs; auto 4 4 elim: steps.cases)
qed
lemma steps_rotate:
assumes "steps (x # xs @ y # ys @ [x])"
shows "steps (y # ys @ x # xs @ [y])"
proof -
from steps_decomp[of "x # xs" "y # ys @ [x]"] assms have
"steps (x # xs)" "steps (y # ys @ [x])" "E (last (x # xs)) y"
by auto
then have "steps ((x # xs) @ [y])" by (blast intro: steps_append_single)
from steps_append[OF ‹steps (y # ys @ [x])› this] show ?thesis by auto
qed
lemma run_shift_coinduct[case_names run_shift, consumes 1]:
assumes "R w"
and "⋀ w. R w ⟹ ∃ u v x y. w = u @- x ## y ## v ∧ steps (u @ [x]) ∧ E x y ∧ R (y ## v)"
shows "run w"
using assms(2)[OF ‹R w›] proof (coinduction arbitrary: w)
case (run w)
then obtain u v x y where "w = u @- x ## y ## v" "steps (u @ [x])" "E x y" "R (y ## v)"
by auto
then show ?case
apply -
apply (drule assms(2))
apply (cases u)
apply force
subgoal for z zs
apply (cases zs)
subgoal
apply simp
apply safe
apply (force elim: steps.cases)
subgoal for u' v' x' y'
by (inst_existentials "x # u'") (cases u'; auto)
done
subgoal for a as
apply simp
apply safe
apply (force elim: steps.cases)
subgoal for u' v' x' y'
apply (inst_existentials "a # as @ x # u'")
using steps_append[of "a # as @ [x, y]" "u' @ [x']"]
apply simp
apply (drule steps_appendI[of "a # as" x, rotated])
by (cases u'; force elim: steps.cases)+
done
done
done
qed
lemma run_flat_coinduct[case_names run_shift, consumes 1]:
assumes "R xss"
and
"⋀ xs ys xss.
R (xs ## ys ## xss) ⟹ xs ≠ [] ∧ steps xs ∧ E (last xs) (hd ys) ∧ R (ys ## xss)"
shows "run (flat xss)"
proof -
obtain xs ys xss' where "xss = xs ## ys ## xss'" by (metis stream.collapse)
with assms(2)[OF assms(1)[unfolded this]] show ?thesis
proof (coinduction arbitrary: xs ys xss' xss rule: run_shift_coinduct)
case (run_shift xs ys xss' xss)
from run_shift show ?case
apply (cases xss')
apply clarify
apply (drule assms(2))
apply (inst_existentials "butlast xs" "tl ys @- flat xss'" "last xs" "hd ys")
apply (cases ys)
apply (simp; fail)
subgoal premises prems for x1 x2 z zs
proof (cases "xs = []")
case True
with prems show ?thesis
by auto
next
case False
then have "xs = butlast xs @ [last xs]" by auto
then have "butlast xs @- last xs ## tail = xs @- tail" for tail
by (metis shift.simps(1,2) shift_append)
with prems show ?thesis by simp
qed
apply (simp; fail)
apply assumption
subgoal for ws wss
by (inst_existentials ys ws wss) (cases ys, auto)
done
qed
qed
lemma steps_non_empty[simp]:
"¬ steps []"
by (auto elim: steps.cases)
lemma steps_non_empty'[simp]:
"xs ≠ []" if "steps xs"
using that by auto
lemma steps_replicate:
"steps (hd xs # concat (replicate n (tl xs)))" if "last xs = hd xs" "steps xs" "n > 0"
using that
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 (cases xs; auto)
next
case prems: (Suc nat)
from Suc.prems have [simp]: "hd xs # tl xs @ ys = xs @ ys" for ys
by (cases xs; auto)
from Suc.prems have **: "tl xs @ ys = tl (xs @ ys)" for ys
by (cases xs; auto)
from prems Suc show ?thesis
by (fastforce intro: steps_append')
qed
qed
notation E (‹_ → _› [100, 100] 40)
abbreviation reaches (‹_ →* _› [100, 100] 40) where "reaches x y ≡ E⇧*⇧* x y"
abbreviation reaches1 (‹_ →⇧+ _› [100, 100] 40) where "reaches1 x y ≡ E⇧+⇧+ x y"
lemma steps_reaches:
"hd xs →* last xs" if "steps xs"
using that by (induction xs) auto
lemma steps_reaches':
"x →* y" if "steps xs" "hd xs = x" "last xs = y"
using that steps_reaches by auto
lemma reaches_steps:
"∃ xs. hd xs = x ∧ last xs = y ∧ steps xs" if "x →* y"
using that
apply (induction)
apply force
apply clarsimp
subgoal for z xs
by (inst_existentials "xs @ [z]", (cases xs; simp), auto intro: steps_append_single)
done
lemma reaches_steps_iff:
"x →* y ⟷ (∃ xs. hd xs = x ∧ last xs = y ∧ steps xs)"
using steps_reaches reaches_steps by fast
lemma steps_reaches1:
"x →⇧+ y" if "steps (x # xs @ [y])"
by (metis list.sel(1,3) rtranclp_into_tranclp2 snoc_eq_iff_butlast steps.cases steps_reaches that)
lemma stepsI:
"steps (x # xs)" if "x → hd xs" "steps xs"
using that by (cases xs) auto
lemma reaches1_steps:
"∃ xs. steps (x # xs @ [y])" if "x →⇧+ y"
proof -
from that obtain z where "x → z" "z →* y"
by atomize_elim (simp add: tranclpD)
from reaches_steps[OF this(2)] obtain xs where *: "hd xs = z" "last xs = y" "steps xs"
by auto
then obtain xs' where [simp]: "xs = xs' @ [y]"
by atomize_elim (auto 4 3 intro: append_butlast_last_id[symmetric])
with ‹x → z› * show ?thesis
by (auto intro: stepsI)
qed
lemma reaches1_steps_iff:
"x →⇧+ y ⟷ (∃ xs. steps (x # xs @ [y]))"
using steps_reaches1 reaches1_steps by fast
lemma reaches_steps_iff2:
"x →* y ⟷ (x = y ∨ (∃vs. steps (x # vs @ [y])))"
by (simp add: Nitpick.rtranclp_unfold reaches1_steps_iff)
lemma reaches1_reaches_iff1:
"x →⇧+ y ⟷ (∃ z. x → z ∧ z →* y)"
by (auto dest: tranclpD)
lemma reaches1_reaches_iff2:
"x →⇧+ y ⟷ (∃ z. x →* z ∧ z → y)"
apply safe
apply (metis Nitpick.rtranclp_unfold tranclp.cases)
by auto
lemma
"x →⇧+ z" if "x →* y" "y →⇧+ z"
using that by auto
lemma
"x →⇧+ z" if "x →⇧+ y" "y →* z"
using that by auto
lemma steps_append2:
"steps (xs @ x # ys)" if "steps (xs @ [x])" "steps (x # ys)"
using that by (auto dest: steps_append)
lemma reaches1_steps_append:
assumes "a →⇧+ b" "steps xs" "hd xs = b"
shows "∃ ys. steps (a # ys @ xs)"
using assms by (fastforce intro: steps_append' dest: reaches1_steps)
lemma steps_last_step:
"∃ a. a → last xs" if "steps xs" "length xs > 1"
using that by induction auto
lemma steps_remove_cycleE:
assumes "steps (a # xs @ [b])"
obtains ys where "steps (a # ys @ [b])" "distinct ys" "a ∉ set ys" "b ∉ set ys" "set ys ⊆ set xs"
using assms
proof (induction "length xs" arbitrary: xs rule: less_induct)
case less
note prems = less.prems(2) and intro = less.prems(1) and IH = less.hyps
consider
"distinct xs" "a ∉ set xs" "b ∉ set xs" | "a ∈ set xs" | "b ∈ set xs" | "¬ distinct xs"
by auto
then consider (goal) ?case
| (a) as bs where "xs = as @ a # bs" | (b) as bs where "xs = as @ b # bs"
| (between) x as bs cs where "xs = as @ x # bs @ x # cs"
using prems by (cases; fastforce dest: not_distinct_decomp simp: split_list intro: intro)
then show ?case
proof cases
case a
with prems show ?thesis
by - (rule IH[where xs = bs], auto 4 3 intro: intro dest: stepsD)
next
case b
with prems have "steps (a # as @ b # [] @ (bs @ [b]))"
by simp
then have "steps (a # as @ [b])"
by (metis Cons_eq_appendI Graph_Defs.steps_appendD1 append_eq_appendI neq_Nil_conv)
with b show ?thesis
by - (rule IH[where xs = as], auto 4 3 dest: stepsD intro: intro)
next
case between
with prems have "steps (a # as @ x # cs @ [b])"
by simp (metis
stepsI append_Cons list.distinct(1) list.sel(1) list.sel(3) steps_append steps_decomp)
with between show ?thesis
by - (rule IH[where xs = "as @ x # cs"], auto 4 3 intro: intro dest: stepsD)
qed
qed
lemma reaches1_stepsE:
assumes "a →⇧+ b"
obtains xs where "steps (a # xs @ [b])" "distinct xs" "a ∉ set xs" "b ∉ set xs"
proof -
from assms obtain xs where "steps (a # xs @ [b])"
by (auto dest: reaches1_steps)
then show ?thesis
by - (erule steps_remove_cycleE, rule that)
qed
lemma reaches_stepsE:
assumes "a →* b"
obtains "a = b" | xs where "steps (a # xs @ [b])" "distinct xs" "a ∉ set xs" "b ∉ set xs"
proof -
from assms consider "a = b" | xs where "a →⇧+ b"
by (meson rtranclpD)
then show ?thesis
by cases ((erule reaches1_stepsE)?; rule that; assumption)+
qed
definition sink where
"sink a ≡ ∄b. a → b"
lemma sink_or_cycle:
assumes "finite {b. reaches a b}"
obtains b where "reaches a b" "sink b" | b where "reaches a b" "reaches1 b b"
proof -
let ?S = "{b. reaches1 a b}"
have "?S ⊆ {b. reaches a b}"
by auto
then have "finite ?S"
using assms by (rule finite_subset)
then show ?thesis
using that
proof (induction ?S arbitrary: a rule: finite_psubset_induct)
case psubset
consider (empty) "Collect (reaches1 a) = {}" | b where "reaches1 a b"
by auto
then show ?case
proof cases
case empty
then have "sink a"
unfolding sink_def by auto
with psubset.prems show ?thesis
by auto
next
case 2
show ?thesis
proof (cases "reaches b a")
case True
with ‹reaches1 a b› have "reaches1 a a"
by auto
with psubset.prems show ?thesis
by auto
next
case False
show ?thesis
proof (cases "reaches1 b b")
case True
with ‹reaches1 a b› psubset.prems show ?thesis
by (auto intro: tranclp_into_rtranclp)
next
case False
with ‹¬ reaches b a› ‹reaches1 a b› have "Collect (reaches1 b) ⊂ Collect (reaches1 a)"
by (intro psubsetI) auto
then show ?thesis
using ‹reaches1 a b› psubset.prems
by - (erule psubset.hyps; meson tranclp_into_rtranclp tranclp_rtranclp_tranclp)
qed
qed
qed
qed
qed
text ‹
A directed graph where every node has at least one ingoing edge, contains a directed cycle.
›
lemma directed_graph_indegree_ge_1_cycle':
assumes "finite S" "S ≠ {}" "∀ y ∈ S. ∃ x ∈ S. E x y"
shows "∃ x ∈ S. ∃ y. E x y ∧ E⇧*⇧* y x"
using assms
proof (induction arbitrary: E rule: finite_ne_induct)
case (singleton x)
then show ?case by auto
next
case (insert x S E)
from insert.prems obtain y where "y ∈ insert x S" "E y x"
by auto
show ?case
proof (cases "y = x")
case True
with ‹E y x› show ?thesis by auto
next
case False
with ‹y ∈ _› have "y ∈ S" by auto
define E' where "E' a b ≡ E a b ∨ (a = y ∧ E x b)" for a b
have E'_E: "∃ c. E a c ∧ E⇧*⇧* c b" if "E' a b" for a b
using that ‹E y x› unfolding E'_def by auto
have [intro]: "E⇧*⇧* a b" if "E' a b" for a b
using that ‹E y x› unfolding E'_def by auto
have [intro]: "E⇧*⇧* a b" if "E'⇧*⇧* a b" for a b
using that by (induction; blast intro: rtranclp_trans)
have "∀y∈S. ∃x∈S. E' x y"
proof (rule ballI)
fix b assume "b ∈ S"
with insert.prems obtain a where "a ∈ insert x S" "E a b"
by auto
show "∃a∈S. E' a b"
proof (cases "a = x")
case True
with ‹E a b› have "E' y b" unfolding E'_def by simp
with ‹y ∈ S› show ?thesis ..
next
case False
with ‹a ∈ _› ‹E a b› show ?thesis unfolding E'_def by auto
qed
qed
from insert.IH[OF this] obtain x y where "x ∈ S" "E' x y" "E'⇧*⇧* y x" by safe
then show ?thesis by (blast intro: rtranclp_trans dest: E'_E)
qed
qed
lemma directed_graph_indegree_ge_1_cycle:
assumes "finite S" "S ≠ {}" "∀ y ∈ S. ∃ x ∈ S. E x y"
shows "∃ x ∈ S. ∃ y. x →⇧+ x"
using directed_graph_indegree_ge_1_cycle'[OF assms] reaches1_reaches_iff1 by blast
text ‹Vertices of a graph›
definition "vertices = {x. ∃y. E x y ∨ E y x}"
lemma reaches1_verts:
assumes "x →⇧+ y"
shows "x ∈ vertices" and "y ∈ vertices"
using assms reaches1_reaches_iff2 reaches1_reaches_iff1 vertices_def by blast+
lemmas graphI =
steps.intros
steps_append_single
steps_reaches'
stepsI
end
section ‹Graphs with a Start Node›
locale Graph_Start_Defs = Graph_Defs +
fixes s⇩0 :: 'a
begin
definition reachable where
"reachable = E⇧*⇧* s⇩0"
lemma start_reachable[intro!, simp]:
"reachable s⇩0"
unfolding reachable_def by auto
lemma reachable_step:
"reachable b" if "reachable a" "E a b"
using that unfolding reachable_def by auto
lemma reachable_reaches:
"reachable b" if "reachable a" "a →* b"
using that(2,1) by induction (auto intro: reachable_step)
lemma reachable_steps_append:
assumes "reachable a" "steps xs" "hd xs = a" "last xs = b"
shows "reachable b"
using assms by (auto intro: graphI reachable_reaches)
lemmas steps_reachable = reachable_steps_append[of s⇩0, simplified]
lemma reachable_steps_elem:
"reachable y" if "reachable x" "steps xs" "y ∈ set xs" "hd xs = x"
proof -
from ‹y ∈ set xs› obtain as bs where [simp]: "xs = as @ y # bs"
by (auto simp: in_set_conv_decomp)
show ?thesis
proof (cases "as = []")
case True
with that show ?thesis
by simp
next
case False
from ‹steps xs› have "steps (as @ [y])"
by (auto intro: stepsD)
with ‹as ≠ []› ‹hd xs = x› ‹reachable x› show ?thesis
by (auto 4 3 intro: reachable_reaches graphI)
qed
qed
lemma reachable_steps:
"∃ xs. steps xs ∧ hd xs = s⇩0 ∧ last xs = x" if "reachable x"
using that unfolding reachable_def
proof induction
case base
then show ?case by (inst_existentials "[s⇩0]"; force)
next
case (step y z)
from step.IH obtain xs where "steps xs" "s⇩0 = hd xs" "y = last xs" by clarsimp
with step.hyps show ?case
apply (inst_existentials "xs @ [z]")
apply (force intro: graphI)
by (cases xs; auto)+
qed
lemma reachable_cycle_iff:
"reachable x ∧ x →⇧+ x ⟷ (∃ ws xs. steps (s⇩0 # ws @ [x] @ xs @ [x]))"
proof (safe, goal_cases)
case (2 ws)
then show ?case
by (auto intro: steps_reachable stepsD)
next
case (3 ws xs)
then show ?case
by (auto intro: stepsD steps_reaches1)
next
case prems: 1
from ‹reachable x› prems(2) have "s⇩0 →⇧+ x"
unfolding reachable_def by auto
with ‹x →⇧+ x› show ?case
by (fastforce intro: steps_append' dest: reaches1_steps)
qed
lemma reachable_induct[consumes 1, case_names start step, induct pred: reachable]:
assumes "reachable x"
and "P s⇩0"
and "⋀ a b. reachable a ⟹ P a ⟹ a → b ⟹ P b"
shows "P x"
using assms(1) unfolding reachable_def
by induction (auto intro: assms(2-)[unfolded reachable_def])
lemmas graphI_aggressive =
tranclp_into_rtranclp
rtranclp.rtrancl_into_rtrancl
tranclp.trancl_into_trancl
rtranclp_into_tranclp2
lemmas graphI_aggressive1 =
graphI_aggressive
steps_append'
lemmas graphI_aggressive2 =
graphI_aggressive
stepsD
steps_reaches1
steps_reachable
lemmas graphD =
reaches1_steps
lemmas graphD_aggressive =
tranclpD
lemmas graph_startI =
reachable_reaches
start_reachable
end
section ‹Subgraphs›
subsection ‹Edge-induced Subgraphs›
locale Subgraph_Defs = G: Graph_Defs +
fixes E' :: "'a ⇒ 'a ⇒ bool"
begin
sublocale G': Graph_Defs E' .
end
locale Subgraph_Start_Defs = G: Graph_Start_Defs +
fixes E' :: "'a ⇒ 'a ⇒ bool"
begin
sublocale G': Graph_Start_Defs E' s⇩0 .
end
locale Subgraph = Subgraph_Defs +
assumes subgraph[intro]: "E' a b ⟹ E a b"
begin
lemma non_subgraph_cycle_decomp:
"∃ c d. G.reaches a c ∧ E c d ∧ ¬ E' c d ∧ G.reaches d b" if
"G.reaches1 a b" "¬ G'.reaches1 a b" for a b
using that
proof induction
case (base y)
then show ?case
by auto
next
case (step y z)
show ?case
proof (cases "E' y z")
case True
with step have "¬ G'.reaches1 a y"
by (auto intro: tranclp.trancl_into_trancl)
with step obtain c d where
"G.reaches a c" "E c d" "¬ E' c d" "G.reaches d y"
by auto
with ‹E' y z› show ?thesis
by (blast intro: rtranclp.rtrancl_into_rtrancl)
next
case False
with step show ?thesis
by (intro exI conjI) auto
qed
qed
lemma reaches:
"G.reaches a b" if "G'.reaches a b"
using that by induction (auto intro: rtranclp.intros(2))
lemma reaches1:
"G.reaches1 a b" if "G'.reaches1 a b"
using that by induction (auto intro: tranclp.intros(2))
end
locale Subgraph_Start = Subgraph_Start_Defs + Subgraph
begin
lemma reachable_subgraph[intro]: "G.reachable b" if ‹G.reachable a› ‹G'.reaches a b› for a b
using that by (auto intro: G.graph_startI mono_rtranclp[rule_format, of E'])
lemma reachable:
"G.reachable x" if "G'.reachable x"
using that by (fastforce simp: G.reachable_def G'.reachable_def)
end
subsection ‹Node-induced Subgraphs›
locale Subgraph_Node_Defs = Graph_Defs +
fixes V :: "'a ⇒ bool"
begin
definition E' where "E' x y ≡ E x y ∧ V x ∧ V y"
sublocale Subgraph E E' by standard (auto simp: E'_def)
lemma subgraph':
"E' x y" if "E x y" "V x" "V y"
using that unfolding E'_def by auto
lemma E'_V1:
"V x" if "E' x y"
using that unfolding E'_def by auto
lemma E'_V2:
"V y" if "E' x y"
using that unfolding E'_def by auto
lemma G'_reaches_V:
"V y" if "G'.reaches x y" "V x"
using that by (cases) (auto intro: E'_V2)
lemma G'_steps_V_all:
"list_all V xs" if "G'.steps xs" "V (hd xs)"
using that by induction (auto intro: E'_V2)
lemma G'_steps_V_last:
"V (last xs)" if "G'.steps xs" "V (hd xs)"
using that by induction (auto dest: E'_V2)
lemmas subgraphI = E'_V1 E'_V2 G'_reaches_V
lemmas subgraphD = E'_V1 E'_V2 G'_reaches_V
end
locale Subgraph_Node_Defs_Notation = Subgraph_Node_Defs
begin
no_notation E (‹_ → _› [100, 100] 40)
notation E' (‹_ → _› [100, 100] 40)
no_notation reaches (‹_ →* _› [100, 100] 40)
notation G'.reaches (‹_ →* _› [100, 100] 40)
no_notation reaches1 (‹_ →⇧+ _› [100, 100] 40)
notation G'.reaches1 (‹_ →⇧+ _› [100, 100] 40)
end
subsection ‹The Reachable Subgraph›
context Graph_Start_Defs
begin
interpretation Subgraph_Node_Defs_Notation E reachable .
sublocale reachable_subgraph: Subgraph_Node_Defs E reachable .
lemma reachable_supgraph:
"x → y" if "E x y" "reachable x"
using that unfolding E'_def by (auto intro: graph_startI)
lemma reachable_reaches_equiv: "reaches x y ⟷ x →* y" if "reachable x" for x y
apply standard
subgoal premises prems
using prems ‹reachable x›
by induction (auto dest: reachable_supgraph intro: graph_startI graphI_aggressive)
subgoal premises prems
using prems ‹reachable x›
by induction (auto dest: subgraph)
done
lemma reachable_reaches1_equiv: "reaches1 x y ⟷ x →⇧+ y" if "reachable x" for x y
apply standard
subgoal premises prems
using prems ‹reachable x›
by induction (auto dest: reachable_supgraph intro: graph_startI graphI_aggressive)
subgoal premises prems
using prems ‹reachable x›
by induction (auto dest: subgraph)
done
lemma reachable_steps_equiv:
"steps (x # xs) ⟷ G'.steps (x # xs)" if "reachable x"
apply standard
subgoal premises prems
using prems ‹reachable x›
by (induction "x # xs" arbitrary: x xs) (auto dest: reachable_supgraph intro: graph_startI)
subgoal premises prems
using prems by induction auto
done
end
section ‹Bundles›
bundle graph_automation
begin
lemmas [intro] = Graph_Defs.graphI Graph_Start_Defs.graph_startI
lemmas [dest] = Graph_Start_Defs.graphD
end
bundle reaches_steps_iff =
Graph_Defs.reaches1_steps_iff [iff]
Graph_Defs.reaches_steps_iff [iff]
bundle graph_automation_aggressive
begin
unbundle graph_automation
lemmas [intro] = Graph_Start_Defs.graphI_aggressive
lemmas [dest] = Graph_Start_Defs.graphD_aggressive
end
bundle subgraph_automation
begin
unbundle graph_automation
lemmas [intro] = Subgraph_Node_Defs.subgraphI
lemmas [dest] = Subgraph_Node_Defs.subgraphD
end
section ‹Directed Acyclic Graphs›
locale DAG = Graph_Defs +
assumes acyclic: "¬ E⇧+⇧+ x x"
begin
lemma topological_numbering:
fixes S assumes "finite S"
shows "∃f :: _ ⇒ nat. inj_on f S ∧ (∀x ∈ S. ∀y ∈ S. E x y ⟶ f x < f y)"
using assms
proof (induction rule: finite_psubset_induct)
case (psubset A)
show ?case
proof (cases "A = {}")
case True
then show ?thesis
by simp
next
case False
then obtain x where x: "x ∈ A" "∀y ∈ A. ¬E y x"
using directed_graph_indegree_ge_1_cycle[OF ‹finite A›] acyclic by auto
let ?A = "A - {x}"
from ‹x ∈ A› have "?A ⊂ A"
by auto
from psubset.IH(1)[OF this] obtain f :: "_ ⇒ nat" where f:
"inj_on f ?A" "∀x∈?A. ∀y∈?A. x → y ⟶ f x < f y"
by blast
let ?f = "λy. if x ≠ y then f y + 1 else 0"
from ‹x ∈ A› have "A = insert x ?A"
by auto
from ‹inj_on f ?A› have "inj_on ?f A"
by (auto simp: inj_on_def)
moreover from f(2) x(2) have "∀x∈A. ∀y∈A. x → y ⟶ ?f x < ?f y"
by auto
ultimately show ?thesis
by blast
qed
qed
end
section ‹Finite Graphs›
locale Finite_Graph = Graph_Defs +
assumes finite_graph: "finite vertices"
locale Finite_DAG = Finite_Graph + DAG
begin
lemma finite_reachable:
"finite {y. x →* y}" (is "finite ?S")
proof -
have "?S ⊆ insert x vertices"
by (metis insertCI mem_Collect_eq reaches1_verts(2) rtranclpD subsetI)
also from finite_graph have "finite …" ..
finally show ?thesis .
qed
end
section ‹Graph Invariants›
locale Graph_Invariant = Graph_Defs +
fixes P :: "'a ⇒ bool"
assumes invariant: "P a ⟹ a → b ⟹ P b"
begin
lemma invariant_steps:
"list_all P as" if "steps (a # as)" "P a"
using that by (induction "a # as" arbitrary: as a) (auto intro: invariant)
lemma invariant_reaches:
"P b" if "a →* b" "P a"
using that by (induction; blast intro: invariant)
lemma invariant_run:
assumes run: "run (x ## xs)" and P: "P x"
shows "pred_stream P (x ## xs)"
using run P by (coinduction arbitrary: x xs) (auto 4 3 elim: invariant run.cases)
text ‹Every graph invariant induces a subgraph.›
sublocale Subgraph_Node_Defs where E = E and V = P .
lemma subgraph':
assumes "x → y" "P x"
shows "E' x y"
using assms by (intro subgraph') (auto intro: invariant)
lemma invariant_steps_iff:
"G'.steps (v # vs) ⟷ steps (v # vs)" if "P v"
apply (rule iffI)
subgoal
using G'.steps_alt_induct steps_appendI by blast
subgoal premises prems
using prems ‹P v› by (induction "v # vs" arbitrary: v vs) (auto intro: subgraph' invariant)
done
lemma invariant_reaches_iff:
"G'.reaches u v ⟷ reaches u v" if "P u"
using that by (simp add: reaches_steps_iff2 G'.reaches_steps_iff2 invariant_steps_iff)
lemma invariant_reaches1_iff:
"G'.reaches1 u v ⟷ reaches1 u v" if "P u"
using that by (simp add: reaches1_steps_iff G'.reaches1_steps_iff invariant_steps_iff)
end
locale Graph_Invariants = Graph_Defs +
fixes P Q :: "'a ⇒ bool"
assumes invariant: "P a ⟹ a → b ⟹ Q b" and Q_P: "Q a ⟹ P a"
begin
sublocale Pre: Graph_Invariant E P
by standard (blast intro: invariant Q_P)
sublocale Post: Graph_Invariant E Q
by standard (blast intro: invariant Q_P)
lemma invariant_steps:
"list_all Q as" if "steps (a # as)" "P a"
using that by (induction "a # as" arbitrary: as a) (auto intro: invariant Q_P)
lemma invariant_run:
assumes run: "run (x ## xs)" and P: "P x"
shows "pred_stream Q xs"
using run P by (coinduction arbitrary: x xs) (auto 4 4 elim: invariant run.cases intro: Q_P)
lemma invariant_reaches1:
"Q b" if "a →⇧+ b" "P a"
using that by (induction; blast intro: invariant Q_P)
end
locale Graph_Invariant_Start = Graph_Start_Defs + Graph_Invariant +
assumes P_s⇩0: "P s⇩0"
begin
lemma invariant_steps:
"list_all P as" if "steps (s⇩0 # as)"
using that P_s⇩0 by (rule invariant_steps)
lemma invariant_reaches:
"P b" if "s⇩0 →* b"
using invariant_reaches[OF that P_s⇩0] .
lemmas invariant_run = invariant_run[OF _ P_s⇩0]
end
locale Graph_Invariant_Strong = Graph_Defs +
fixes P :: "'a ⇒ bool"
assumes invariant: "a → b ⟹ P b"
begin
sublocale inv: Graph_Invariant by standard (rule invariant)
lemma P_invariant_steps:
"list_all P as" if "steps (a # as)"
using that by (induction "a # as" arbitrary: as a) (auto intro: invariant)
lemma steps_last_invariant:
"P (last xs)" if "steps (x # xs)" "xs ≠ []"
using steps_last_step[of "x # xs"] that by (auto intro: invariant)
lemmas invariant_reaches = inv.invariant_reaches
lemma invariant_reaches1:
"P b" if "a →⇧+ b"
using that by (induction; blast intro: invariant)
end
section ‹Simulations and Bisimulations›
locale Simulation_Defs =
fixes A :: "'a ⇒ 'a ⇒ bool" and B :: "'b ⇒ 'b ⇒ bool"
and sim :: "'a ⇒ 'b ⇒ bool" (infixr ‹∼› 60)
begin
sublocale A: Graph_Defs A .
sublocale B: Graph_Defs B .
end
locale Simulation = Simulation_Defs +
assumes A_B_step: "⋀ a b a'. A a b ⟹ a ∼ a' ⟹ (∃ b'. B a' b' ∧ b ∼ b')"
begin
lemma simulation_reaches:
"∃ b'. B⇧*⇧* b b' ∧ a' ∼ b'" if "A⇧*⇧* a a'" "a ∼ b"
using that by (induction rule: rtranclp_induct) (auto intro: rtranclp.intros(2) dest: A_B_step)
lemma simulation_reaches1:
"∃ b'. B⇧+⇧+ b b' ∧ a' ∼ b'" if "A⇧+⇧+ a a'" "a ∼ b"
using that by (induction rule: tranclp_induct) (auto 4 3 intro: tranclp.intros(2) dest: A_B_step)
lemma simulation_steps:
"∃ bs. B.steps (b # bs) ∧ list_all2 (λ a b. a ∼ b) as bs" if "A.steps (a # as)" "a ∼ b"
using that
apply (induction "a # as" arbitrary: a b as)
apply force
apply (frule A_B_step, auto)
done
lemma simulation_run:
"∃ ys. B.run (y ## ys) ∧ stream_all2 (∼) xs ys" if "A.run (x ## xs)" "x ∼ y"
proof -
let ?ys = "sscan (λ a' b. SOME b'. B b b' ∧ a' ∼ b') xs y"
have "B.run (y ## ?ys)"
using that by (coinduction arbitrary: x y xs) (force dest!: someI_ex A_B_step elim: A.run.cases)
moreover have "stream_all2 (∼) xs ?ys"
using that by (coinduction arbitrary: x y xs) (force dest!: someI_ex A_B_step elim: A.run.cases)
ultimately show ?thesis by blast
qed
end
lemma (in Subgraph) Subgraph_Simulation:
"Simulation E' E (=)"
by standard auto
locale Simulation_Invariant = Simulation_Defs +
fixes PA :: "'a ⇒ bool" and PB :: "'b ⇒ bool"
assumes A_B_step: "⋀ a b a'. A a b ⟹ PA a ⟹ PB a' ⟹ a ∼ a' ⟹ (∃ b'. B a' b' ∧ b ∼ b')"
assumes A_invariant[intro]: "⋀ a b. PA a ⟹ A a b ⟹ PA b"
assumes B_invariant[intro]: "⋀ a b. PB a ⟹ B a b ⟹ PB b"
begin
definition "equiv' ≡ λ a b. a ∼ b ∧ PA a ∧ PB b"
sublocale Simulation A B equiv' by standard (auto dest: A_B_step simp: equiv'_def)
sublocale PA_invariant: Graph_Invariant A PA by standard blast
sublocale PB_invariant: Graph_Invariant B PB by standard blast
lemma simulation_reaches:
"∃ b'. B⇧*⇧* b b' ∧ a' ∼ b' ∧ PA a' ∧ PB b'" if "A⇧*⇧* a a'" "a ∼ b" "PA a" "PB b"
using simulation_reaches[of a a' b] that unfolding equiv'_def by simp
lemma simulation_steps:
"∃ bs. B.steps (b # bs) ∧ list_all2 (λ a b. a ∼ b ∧ PA a ∧ PB b) as bs"
if "A.steps (a # as)" "a ∼ b" "PA a" "PB b"
using simulation_steps[of a as b] that unfolding equiv'_def by simp
lemma simulation_steps':
"∃ bs. B.steps (b # bs) ∧ list_all2 (λ a b. a ∼ b) as bs ∧ list_all PA as ∧ list_all PB bs"
if "A.steps (a # as)" "a ∼ b" "PA a" "PB b"
using simulation_steps[OF that]
by (force dest: list_all2_set1 list_all2_set2 simp: list_all_iff elim: list_all2_mono)
context
fixes f
assumes eq: "a ∼ b ⟹ b = f a"
begin
lemma simulation_steps'_map:
"∃ bs.
B.steps (b # bs) ∧ bs = map f as
∧ list_all2 (λ a b. a ∼ b) as bs
∧ list_all PA as ∧ list_all PB bs"
if "A.steps (a # as)" "a ∼ b" "PA a" "PB b"
proof -
from simulation_steps'[OF that] obtain bs where guessed:
"B.steps (b # bs)"
"list_all2 (∼) as bs"
"list_all PA as"
"list_all PB bs"
by safe
from this(2) have "bs = map f as"
by (induction; simp add: eq)
with guessed show ?thesis
by auto
qed
end
end
locale Simulation_Invariants = Simulation_Defs +
fixes PA QA :: "'a ⇒ bool" and PB QB :: "'b ⇒ bool"
assumes A_B_step: "⋀ a b a'. A a b ⟹ PA a ⟹ PB a' ⟹ a ∼ a' ⟹ (∃ b'. B a' b' ∧ b ∼ b')"
assumes A_invariant[intro]: "⋀ a b. PA a ⟹ A a b ⟹ QA b"
assumes B_invariant[intro]: "⋀ a b. PB a ⟹ B a b ⟹ QB b"
assumes PA_QA[intro]: "⋀ a. QA a ⟹ PA a" and PB_QB[intro]: "⋀ a. QB a ⟹ PB a"
begin
sublocale Pre: Simulation_Invariant A B "(∼)" PA PB
by standard (auto intro: A_B_step)
sublocale Post: Simulation_Invariant A B "(∼)" QA QB
by standard (auto intro: A_B_step)
sublocale A_invs: Graph_Invariants A PA QA
by standard auto
sublocale B_invs: Graph_Invariants B PB QB
by standard auto
lemma simulation_reaches1:
"∃ b2. B.reaches1 b1 b2 ∧ a2 ∼ b2 ∧ QB b2" if "A.reaches1 a1 a2" "a1 ∼ b1" "PA a1" "PB b1"
using that
by - (drule Pre.simulation_reaches1, auto intro: B_invs.invariant_reaches1 simp: Pre.equiv'_def)
lemma reaches1_unique:
assumes unique: "⋀ b2. a ∼ b2 ⟹ QB b2 ⟹ b2 = b"
and that: "A.reaches1 a a" "a ∼ b" "PA a" "PB b"
shows "B.reaches1 b b"
using that by (auto dest: unique simulation_reaches1)
end
locale Bisimulation = Simulation_Defs +
assumes A_B_step: "⋀ a b a'. A a b ⟹ a ∼ a' ⟹ (∃ b'. B a' b' ∧ b ∼ b')"
assumes B_A_step: "⋀ a a' b'. B a' b' ⟹ a ∼ a' ⟹ (∃ b. A a b ∧ b ∼ b')"
begin
sublocale A_B: Simulation A B "(∼)" by standard (rule A_B_step)
sublocale B_A: Simulation B A "λ x y. y ∼ x" by standard (rule B_A_step)
lemma A_B_reaches:
"∃ b'. B⇧*⇧* b b' ∧ a' ∼ b'" if "A⇧*⇧* a a'" "a ∼ b"
using A_B.simulation_reaches[OF that] .
lemma B_A_reaches:
"∃ b'. A⇧*⇧* b b' ∧ b' ∼ a'" if "B⇧*⇧* a a'" "b ∼ a"
using B_A.simulation_reaches[OF that] .
end
locale Bisimulation_Invariant = Simulation_Defs +
fixes PA :: "'a ⇒ bool" and PB :: "'b ⇒ bool"
assumes A_B_step: "⋀ a b a'. A a b ⟹ a ∼ a' ⟹ PA a ⟹ PB a' ⟹ (∃ b'. B a' b' ∧ b ∼ b')"
assumes B_A_step: "⋀ a a' b'. B a' b' ⟹ a ∼ a' ⟹ PA a ⟹ PB a' ⟹ (∃ b. A a b ∧ b ∼ b')"
assumes A_invariant[intro]: "⋀ a b. PA a ⟹ A a b ⟹ PA b"
assumes B_invariant[intro]: "⋀ a b. PB a ⟹ B a b ⟹ PB b"
begin
sublocale PA_invariant: Graph_Invariant A PA by standard blast
sublocale PB_invariant: Graph_Invariant B PB by standard blast
lemmas B_steps_invariant[intro] = PB_invariant.invariant_reaches
definition "equiv' ≡ λ a b. a ∼ b ∧ PA a ∧ PB b"
sublocale bisim: Bisimulation A B equiv'
by standard (clarsimp simp add: equiv'_def, frule A_B_step B_A_step, assumption; auto)+
sublocale A_B: Simulation_Invariant A B "(∼)" PA PB
by (standard; blast intro: A_B_step B_A_step)
sublocale B_A: Simulation_Invariant B A "λ x y. y ∼ x" PB PA
by (standard; blast intro: A_B_step B_A_step)
context
fixes f
assumes eq: "a ∼ b ⟷ b = f a"
and inj: "∀ a b. PB (f a) ∧ PA b ∧ f a = f b ⟶ a = b"
begin
lemma list_all2_inj_map_eq:
"as = bs" if "list_all2 (λa b. a = f b) (map f as) bs" "list_all PB (map f as)" "list_all PA bs"
using that inj
by (induction "map f as" bs arbitrary: as rule: list_all2_induct) (auto simp: inj_on_def)
lemma steps_map_equiv:
"A.steps (a # as) ⟷ B.steps (b # map f as)" if "a ∼ b" "PA a" "PB b"
using A_B.simulation_steps'_map[of f a as b] B_A.simulation_steps'[of b "map f as" a] that eq
by (auto dest: list_all2_inj_map_eq)
lemma steps_map:
"∃ as. bs = map f as" if "B.steps (f a # bs)" "PA a" "PB (f a)"
proof -
have "a ∼ f a" unfolding eq ..
from B_A.simulation_steps'[OF that(1) this ‹PB _› ‹PA _›] obtain as where
"A.steps (a # as)"
"list_all2 (λa b. b ∼ a) bs as"
"list_all PB bs"
"list_all PA as"
by safe
from this(2) show ?thesis
unfolding eq by (inst_existentials as, induction rule: list_all2_induct, auto)
qed
lemma reaches_equiv:
"A.reaches a a' ⟷ B.reaches (f a) (f a')" if "PA a" "PB (f a)"
apply safe
apply (drule A_B.simulation_reaches[of a a' "f a"]; simp add: eq that)
apply (drule B_A.simulation_reaches)
defer
apply (rule that | clarsimp simp: eq | metis inj)+
done
end
lemma equiv'_D:
"a ∼ b" if "A_B.equiv' a b"
using that unfolding A_B.equiv'_def by auto
lemma equiv'_rotate_1:
"B_A.equiv' b a" if "A_B.equiv' a b"
using that by (auto simp: B_A.equiv'_def A_B.equiv'_def)
lemma equiv'_rotate_2:
"A_B.equiv' a b" if "B_A.equiv' b a"
using that by (auto simp: B_A.equiv'_def A_B.equiv'_def)
lemma stream_all2_equiv'_D:
"stream_all2 (∼) xs ys" if "stream_all2 A_B.equiv' xs ys"
using stream_all2_weaken[OF that equiv'_D] by fast
lemma stream_all2_equiv'_D2:
"stream_all2 B_A.equiv' ys xs ⟹ stream_all2 ((∼)¯¯) ys xs"
by (coinduction arbitrary: xs ys) (auto simp: B_A.equiv'_def)
lemma stream_all2_rotate_1:
"stream_all2 B_A.equiv' ys xs ⟹ stream_all2 A_B.equiv' xs ys"
by (coinduction arbitrary: xs ys) (auto simp: B_A.equiv'_def A_B.equiv'_def)
lemma stream_all2_rotate_2:
"stream_all2 A_B.equiv' xs ys ⟹ stream_all2 B_A.equiv' ys xs"
by (coinduction arbitrary: xs ys) (auto simp: B_A.equiv'_def A_B.equiv'_def)
end
locale Bisimulation_Invariants = Simulation_Defs +
fixes PA QA :: "'a ⇒ bool" and PB QB :: "'b ⇒ bool"
assumes A_B_step: "⋀ a b a'. A a b ⟹ a ∼ a' ⟹ PA a ⟹ PB a' ⟹ (∃ b'. B a' b' ∧ b ∼ b')"
assumes B_A_step: "⋀ a a' b'. B a' b' ⟹ a ∼ a' ⟹ PA a ⟹ PB a' ⟹ (∃ b. A a b ∧ b ∼ b')"
assumes A_invariant[intro]: "⋀ a b. PA a ⟹ A a b ⟹ QA b"
assumes B_invariant[intro]: "⋀ a b. PB a ⟹ B a b ⟹ QB b"
assumes PA_QA[intro]: "⋀ a. QA a ⟹ PA a" and PB_QB[intro]: "⋀ a. QB a ⟹ PB a"
begin
sublocale PA_invariant: Graph_Invariant A PA by standard blast
sublocale PB_invariant: Graph_Invariant B PB by standard blast
sublocale QA_invariant: Graph_Invariant A QA by standard blast
sublocale QB_invariant: Graph_Invariant B QB by standard blast
sublocale Pre_Bisim: Bisimulation_Invariant A B "(∼)" PA PB
by standard (auto intro: A_B_step B_A_step)
sublocale Post_Bisim: Bisimulation_Invariant A B "(∼)" QA QB
by standard (auto intro: A_B_step B_A_step)
sublocale A_B: Simulation_Invariants A B "(∼)" PA QA PB QB
by standard (blast intro: A_B_step)+
sublocale B_A: Simulation_Invariants B A "λ x y. y ∼ x" PB QB PA QA
by standard (blast intro: B_A_step)+
context
fixes f
assumes eq[simp]: "a ∼ b ⟷ b = f a"
and inj: "∀ a b. QB (f a) ∧ QA b ∧ f a = f b ⟶ a = b"
begin
lemmas list_all2_inj_map_eq = Post_Bisim.list_all2_inj_map_eq[OF eq inj]
lemmas steps_map_equiv' = Post_Bisim.steps_map_equiv[OF eq inj]
lemma list_all2_inj_map_eq':
"as = bs" if "list_all2 (λa b. a = f b) (map f as) bs" "list_all QB (map f as)" "list_all QA bs"
using that by (rule list_all2_inj_map_eq)
lemma steps_map_equiv:
"A.steps (a # as) ⟷ B.steps (b # map f as)" if "a ∼ b" "PA a" "PB b"
proof
assume "A.steps (a # as)"
then show "B.steps (b # map f as)"
proof cases
case Single
then show ?thesis by auto
next
case prems: (Cons a' xs)
from A_B_step[OF ‹A a a'› ‹a ∼ b› ‹PA a› ‹PB b›] obtain b' where "B b b'" "a' ∼ b'"
by auto
with steps_map_equiv'[OF ‹a' ∼ b'›, of xs] prems that show ?thesis
by auto
qed
next
assume "B.steps (b # map f as)"
then show "A.steps (a # as)"
proof cases
case Single
then show ?thesis by auto
next
case prems: (Cons b' xs)
from B_A_step[OF ‹B b b'› ‹a ∼ b› ‹PA a› ‹PB b›] obtain a' where "A a a'" "a' ∼ b'"
by auto
with that prems have "QA a'" "QB b'"
by auto
with ‹A a a'› ‹a' ∼ b'› steps_map_equiv'[OF ‹a' ∼ b'›, of "tl as"] prems that show ?thesis
apply clarsimp
subgoal for z zs
using inj[rule_format, of z a'] by auto
done
qed
qed
lemma steps_map:
"∃ as. bs = map f as" if "B.steps (f a # bs)" "PA a" "PB (f a)"
using that proof cases
case Single
then show ?thesis by simp
next
case prems: (Cons b' xs)
from B_A_step[OF ‹B _ b'› _ ‹PA a› ‹PB (f a)›] obtain a' where "A a a'" "a' ∼ b'"
by auto
with that prems have "QA a'" "QB b'"
by auto
with Post_Bisim.steps_map[OF eq inj, of a' xs] prems ‹a' ∼ b'› obtain ys where "xs = map f ys"
by auto
with ‹bs = _› ‹a' ∼ b'› show ?thesis
by (inst_existentials "a' # ys") auto
qed
text ‹
@{thm Post_Bisim.reaches_equiv} cannot be lifted directly:
injectivity cannot be applied for the reflexive case.
›
lemma reaches1_equiv:
"A.reaches1 a a' ⟷ B.reaches1 (f a) (f a')" if "PA a" "PB (f a)"
proof safe
assume "A.reaches1 a a'"
then obtain a'' where prems: "A a a''" "A.reaches a'' a'"
including graph_automation_aggressive by blast
from A_B_step[OF ‹A a _› _ that] obtain b where "B (f a) b" "a'' ∼ b"
by auto
with that prems have "QA a''" "QB b"
by auto
with Post_Bisim.reaches_equiv[OF eq inj, of a'' a'] prems ‹B (f a) b› ‹a'' ∼ b›
show "B.reaches1 (f a) (f a')"
by auto
next
assume "B.reaches1 (f a) (f a')"
then obtain b where prems: "B (f a) b" "B.reaches b (f a')"
including graph_automation_aggressive by blast
from B_A_step[OF ‹B _ b› _ ‹PA a› ‹PB (f a)›] obtain a'' where "A a a''" "a'' ∼ b"
by auto
with that prems have "QA a''" "QB b"
by auto
with Post_Bisim.reaches_equiv[OF eq inj, of a'' a'] prems ‹A a a''› ‹a'' ∼ b›
show "A.reaches1 a a'"
by auto
qed
end
end
lemma Bisimulation_Invariant_composition:
assumes
"Bisimulation_Invariant A B sim1 PA PB"
"Bisimulation_Invariant B C sim2 PB PC"
shows
"Bisimulation_Invariant A C (λ a c. ∃ b. PB b ∧ sim1 a b ∧ sim2 b c) PA PC"
proof -
interpret A: Bisimulation_Invariant A B sim1 PA PB
by (rule assms(1))
interpret B: Bisimulation_Invariant B C sim2 PB PC
by (rule assms(2))
show ?thesis
by (standard; (blast dest: A.A_B_step B.A_B_step | blast dest: A.B_A_step B.B_A_step))
qed
lemma Bisimulation_Invariant_filter:
assumes
"Bisimulation_Invariant A B sim PA PB"
"⋀ a b. sim a b ⟹ PA a ⟹ PB b ⟹ FA a ⟷ FB b"
"⋀ a b. A a b ∧ FA b ⟷ A' a b"
"⋀ a b. B a b ∧ FB b ⟷ B' a b"
shows
"Bisimulation_Invariant A' B' sim PA PB"
proof -
interpret Bisimulation_Invariant A B sim PA PB
by (rule assms(1))
have unfold:
"A' = (λ a b. A a b ∧ FA b)" "B' = (λ a b. B a b ∧ FB b)"
using assms(3,4) by auto
show ?thesis
unfolding unfold
apply standard
using assms(2) apply (blast dest: A_B_step)
using assms(2) apply (blast dest: B_A_step)
by blast+
qed
lemma Bisimulation_Invariants_filter:
assumes
"Bisimulation_Invariants A B sim PA QA PB QB"
"⋀ a b. QA a ⟹ QB b ⟹ FA a ⟷ FB b"
"⋀ a b. A a b ∧ FA b ⟷ A' a b"
"⋀ a b. B a b ∧ FB b ⟷ B' a b"
shows
"Bisimulation_Invariants A' B' sim PA QA PB QB"
proof -
interpret Bisimulation_Invariants A B sim PA QA PB QB
by (rule assms(1))
have unfold:
"A' = (λ a b. A a b ∧ FA b)" "B' = (λ a b. B a b ∧ FB b)"
using assms(3,4) by auto
show ?thesis
unfolding unfold
apply standard
using assms(2) apply (blast dest: A_B_step)
using assms(2) apply (blast dest: B_A_step)
by blast+
qed
lemma Bisimulation_Invariants_composition:
assumes
"Bisimulation_Invariants A B sim1 PA QA PB QB"
"Bisimulation_Invariants B C sim2 PB QB PC QC"
shows
"Bisimulation_Invariants A C (λ a c. ∃ b. PB b ∧ sim1 a b ∧ sim2 b c) PA QA PC QC"
proof -
interpret A: Bisimulation_Invariants A B sim1 PA QA PB QB
by (rule assms(1))
interpret B: Bisimulation_Invariants B C sim2 PB QB PC QC
by (rule assms(2))
show ?thesis
by (standard, blast dest: A.A_B_step B.A_B_step) (blast dest: A.B_A_step B.B_A_step)+
qed
lemma Bisimulation_Invariant_Invariants_composition:
assumes
"Bisimulation_Invariant A B sim1 PA PB"
"Bisimulation_Invariants B C sim2 PB QB PC QC"
shows
"Bisimulation_Invariants A C (λ a c. ∃ b. PB b ∧ sim1 a b ∧ sim2 b c) PA PA PC QC"
proof -
interpret Bisimulation_Invariant A B sim1 PA PB
by (rule assms(1))
interpret B: Bisimulation_Invariants B C sim2 PB QB PC QC
by (rule assms(2))
interpret A: Bisimulation_Invariants A B sim1 PA PA PB QB
by (standard; blast intro: A_B_step B_A_step)+
show ?thesis
by (standard; (blast dest: A.A_B_step B.A_B_step | blast dest: A.B_A_step B.B_A_step))
qed
lemma Bisimulation_Invariant_Bisimulation_Invariants:
assumes "Bisimulation_Invariant A B sim PA PB"
shows "Bisimulation_Invariants A B sim PA PA PB PB"
proof -
interpret Bisimulation_Invariant A B sim PA PB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step B_A_step)
qed
lemma Bisimulation_Invariant_strengthen_post:
assumes
"Bisimulation_Invariant A B sim PA PB"
"⋀ a b. PA' a ⟹ PA b ⟹ A a b ⟹ PA' b"
"⋀ a. PA' a ⟹ PA a"
shows "Bisimulation_Invariant A B sim PA' PB"
proof -
interpret Bisimulation_Invariant A B sim PA PB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step B_A_step assms)
qed
lemma Bisimulation_Invariant_strengthen_post':
assumes
"Bisimulation_Invariant A B sim PA PB"
"⋀ a b. PB' a ⟹ PB b ⟹ B a b ⟹ PB' b"
"⋀ a. PB' a ⟹ PB a"
shows "Bisimulation_Invariant A B sim PA PB'"
proof -
interpret Bisimulation_Invariant A B sim PA PB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step B_A_step assms)
qed
lemma Simulation_Invariant_strengthen_post:
assumes
"Simulation_Invariant A B sim PA PB"
"⋀ a b. PA a ⟹ PA b ⟹ A a b ⟹ PA' b"
"⋀ a. PA' a ⟹ PA a"
shows "Simulation_Invariant A B sim PA' PB"
proof -
interpret Simulation_Invariant A B sim PA PB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step assms)
qed
lemma Simulation_Invariant_strengthen_post':
assumes
"Simulation_Invariant A B sim PA PB"
"⋀ a b. PB a ⟹ PB b ⟹ B a b ⟹ PB' b"
"⋀ a. PB' a ⟹ PB a"
shows "Simulation_Invariant A B sim PA PB'"
proof -
interpret Simulation_Invariant A B sim PA PB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step assms)
qed
lemma Simulation_Invariants_strengthen_post:
assumes
"Simulation_Invariants A B sim PA QA PB QB"
"⋀ a b. PA a ⟹ QA b ⟹ A a b ⟹ QA' b"
"⋀ a. QA' a ⟹ QA a"
shows "Simulation_Invariants A B sim PA QA' PB QB"
proof -
interpret Simulation_Invariants A B sim PA QA PB QB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step assms)
qed
lemma Simulation_Invariants_strengthen_post':
assumes
"Simulation_Invariants A B sim PA QA PB QB"
"⋀ a b. PB a ⟹ QB b ⟹ B a b ⟹ QB' b"
"⋀ a. QB' a ⟹ QB a"
shows "Simulation_Invariants A B sim PA QA PB QB'"
proof -
interpret Simulation_Invariants A B sim PA QA PB QB
by (rule assms)
show ?thesis
by (standard; blast intro: A_B_step assms)
qed
lemma Bisimulation_Invariant_sim_replace:
assumes "Bisimulation_Invariant A B sim PA PB"
and "⋀ a b. PA a ⟹ PB b ⟹ sim a b ⟷ sim' a b"
shows "Bisimulation_Invariant A B sim' PA PB"
proof -
interpret Bisimulation_Invariant A B sim PA PB
by (rule assms(1))
show ?thesis
apply standard
using assms(2) apply (blast dest: A_B_step)
using assms(2) apply (blast dest: B_A_step)
by blast+
qed
end