Theory Lasso_Freeness_Certificates_Complete
section ‹ Certificates for the Absence of Lassos ›
theory Lasso_Freeness_Certificates_Complete
imports Main "HOL-Library.Countable" Graph_Library_Adaptor
begin
text ‹
This theory gives two valid ways of generating a certificate that proves that the given
graph does not contain an accepting lasso. It is not directly used by the \muntac\
formalization but summarizes the idea of how to get from certificates for unreachability
to certificates for the absence of B\"uechi properties.
›
locale Contract_Downward =
fixes E :: "'a :: countable ⇒ 'a ⇒ bool" and F :: "'a ⇒ bool"
fixes f :: "'a ⇒ nat"
assumes f_topo: "E a b ⟹ if F a then f a > f b else f a ≥ f b"
begin
lemma f_downward:
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" "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_downward order.trans)
lemma 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
sublocale Graph_Defs .
lemma run_f_mono:
assumes "run (x ## xs)" "c ≥ f x"
shows "pred_stream (λa. c ≥ f a) xs"
using assms
by (coinduction arbitrary: x xs) (metis f_downward order.trans run.cases stream.inject)
lemma no_Buechi_run:
assumes "run xs" "infs F xs"
shows False
proof -
let ?S = "f ` sset xs" let ?T = "f ` sset (sfilter F xs)"
obtain x ys where "xs = x ## ys"
by (cases xs)
let ?ub = "f x"
from ‹run xs› have "run ys" "f (shd ys) ≤ ?ub"
unfolding ‹xs = _› by (force elim: run.cases dest: f_downward)+
then have "pred_stream (λx. f x ≤ ?ub) ys"
by (coinduction arbitrary: ys) (fastforce elim: run.cases dest: f_downward intro: order.trans)
then have "finite ?S"
unfolding stream.pred_set ‹xs = _› finite_nat_set_iff_bounded_le by auto
from ‹run xs› ‹infs F xs› have "sdistinct (smap f (sfilter F xs))"
proof (coinduction arbitrary: xs)
case (sdistinct x xs ys)
obtain y xs' where [simp]: "xs = y ## xs'"
by (cases xs)
obtain as bs x' y' ys' where eqs:
"F x'" "F y'" "x = f x'" "y = f y'"
"ys = as @- x' ## bs @- y' ## ys'" "xs' = smap f (sfilter F ys')"
"list_all (Not o F) as" "list_all (Not o F) bs"
proof (atomize_elim, goal_cases)
case 1
from sdistinct have "ev (holds F) ys"
by auto
from ‹x ## xs = _› have "x ## y ## xs' = smap f (sfilter F ys)"
by simp
then obtain x' y' ys' where "x = f x'" "y = f y'" "sfilter F ys = x' ## y' ## ys'"
"xs' = smap f ys'"
apply atomize_elim
unfolding scons_eq_smap
apply (elim conjE)
apply (intro exI conjI)
apply assumption+
apply (subst stream.collapse)+
..
with ‹ev (holds F) ys› show ?case
apply -
apply (drule (1) sfilter_SCons_decomp)
apply (elim conjE exE)
apply (drule sfilter_SCons_decomp, metis alw.cases alw_shift sdistinct(3) stream.sel(2))
by force
qed
have "run (y' ## ys')"
using ‹run ys› unfolding ‹ys = _›
by (metis alw.cases alw_iff_sdrop alw_shift run_sdrop stream.sel(2))
from eqs ‹run ys› have "steps (as @ x' # bs @ [y'])"
by (simp add: run_decomp)
then have "steps (x' # bs @ [y'])"
using steps_appendD2 by blast
then have "E⇧+⇧+ x' y'"
using steps_reaches1 by blast
with ‹F x'› have "f x' > f y'"
using f_strict reaches1_reaches_iff1 reaches_f_mono by fastforce
moreover have "pred_stream (λa. f y' ≥ f a) ys'"
by (rule run_f_mono[where c = "f y'"]) (auto intro: ‹run (y' ## ys')›)
ultimately have "x ∉ f ` sset ys'"
unfolding stream.pred_set eqs by auto
from ‹infs F ys› have "infs F ys'"
unfolding eqs by auto
then have "sset (sfilter F ys') ⊆ sset ys'"
by (rule sset_sfilter)
with ‹x ∉ _› ‹f x' > f y'› have "x ∉ sset xs"
unfolding stream.pred_set eqs ‹xs = _› by auto
with ‹run (y' ## ys')› ‹infs F ys'› eqs ‹xs' = _› show ?case
by - (safe, rule exI[where x = "y'##ys'"], auto)
qed
then have "infinite ?T"
by - (drule sdistinct_infinite_sset, simp)
moreover have "?T ⊆ ?S"
by (rule image_mono sset_sfilter assms)+
ultimately show ?thesis
using ‹finite ?S› finite_subset by auto
qed
end
context
fixes E :: "'a :: countable ⇒ 'a ⇒ bool" and F :: "'a ⇒ bool"
begin
context
fixes f :: "'a ⇒ nat"
assumes f_topo: "E a b ⟹ if F a then f a < f b else f a ≤ f b"
begin
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" "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)
lemma 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
context
assumes no_accepting_cycle: "E⇧+⇧+ x x ⟹ ¬ F x"
begin
definition
"reach x ≡ card {y. F y ∧ E⇧*⇧* x y}"
context
assumes finite: "finite {y. E⇧*⇧* x y}"
begin
lemma reach_mono:
assumes "E x y"
shows "reach x ≥ reach y"
using assms unfolding reach_def by (intro card_mono finite_subset[OF _ finite]) auto
lemma reach_strict:
assumes "E x y" "F x"
shows "reach x > reach y"
proof -
have False
if "E x y"
and "F x"
and "{ya. F ya ∧ E⇧*⇧* y ya} = {y. F y ∧ E⇧*⇧* x y}"
proof -
from that have "E⇧*⇧* y x"
by auto
with ‹E x y› have "E⇧+⇧+ x x"
by auto
with ‹F x› no_accepting_cycle show False
by auto
qed
then show ?thesis
using assms unfolding reach_def
apply (intro psubset_card_mono finite_subset[OF _ finite])
apply force
by auto
qed
end
end
end
context Finite_Graph
begin
context
assumes no_accepting_cycle: "E⇧+⇧+ x x ⟹ ¬ F x"
begin
private definition
"f x ≡ scc_num (THE V. is_max_scc V ∧ x ∈ V)"
lemma f_topo:
assumes "E a b"
shows "if F a then f a < f b else f a ≤ f b"
proof -
from assms obtain A where A: "is_max_scc A" "a ∈ A"
by - (rule max_sccI, auto simp: vertices_def)
from assms obtain B where B: "is_max_scc B" "b ∈ B"
by - (rule max_sccI[where a = b], auto simp: vertices_def)
from A B have [simp]: "f a = scc_num A" "f b = scc_num B"
unfolding f_def using is_max_scc_disjoint
by (intro arg_cong[where f = scc_num] the_equality, auto)+
have "f a ≤ f b"
proof (cases "A = B")
case True
then show ?thesis
by simp
next
case False
with ‹E a b› ‹a ∈ A› ‹b ∈ B› have "edge A B"
unfolding edge_def by auto
then have "f a < f b"
using A B scc_num_topological by simp
then show ?thesis
by simp
qed
moreover have "f a ≠ f b" if "F a"
proof (rule ccontr)
assume "¬ f a ≠ f b"
with A B have "A = B"
using scc_num_inj unfolding inj_on_def by simp
with A ‹b ∈ B› have "E⇧*⇧* b a"
unfolding is_max_scc_def by auto
with ‹E a b› have "E⇧+⇧+ a a"
by auto
with ‹F a› no_accepting_cycle show False
by auto
qed
ultimately show ?thesis
by auto
qed
end
end
end