Theory Automata
section ‹Automata›
theory Automata
imports Digraph
begin
text ‹
In this theory, we define Generalized Buchi Automata and Buchi Automata
based on directed graphs
›
hide_const (open) prod
subsection "Generalized Buchi Graphs"
text ‹
A generalized Buchi graph is a graph where each node belongs to a set of
acceptance classes. An infinite run on this graph is accepted, iff
it visits nodes from each acceptance class infinitely often.
The standard encoding of acceptance classes is as a set of sets of nodes,
each inner set representing one acceptance class.
›
record 'Q gb_graph_rec = "'Q graph_rec" +
gbg_F :: "'Q set set"
locale gb_graph =
graph G
for G :: "('Q,'more) gb_graph_rec_scheme" +
assumes finite_F[simp, intro!]: "finite (gbg_F G)"
assumes F_ss: "gbg_F G ⊆ Pow V"
begin
abbreviation "F ≡ gbg_F G"
lemma is_gb_graph: "gb_graph G" by unfold_locales
definition
is_acc :: "'Q word ⇒ bool" where "is_acc r ≡ (∀A∈F. ∃⇩∞i. r i ∈ A)"
definition "is_acc_run r ≡ is_run r ∧ is_acc r"
lemma "is_acc_run r ≡ is_run r ∧ (∀A∈F. ∃⇩∞i. r i ∈ A)"
unfolding is_acc_run_def is_acc_def .
lemma acc_run_run: "is_acc_run r ⟹ is_run r"
unfolding is_acc_run_def by simp
lemmas acc_run_reachable = run_reachable[OF acc_run_run]
lemma acc_eq_limit:
assumes FIN: "finite (range r)"
shows "is_acc r ⟷ (∀A∈F. limit r ∩ A ≠ {})"
proof
assume "∀A∈F. limit r ∩ A ≠ {}"
thus "is_acc r"
unfolding is_acc_def
by (metis limit_inter_INF)
next
from FIN have FIN': "⋀A. finite (A ∩ range r)"
by simp
assume "is_acc r"
hence AUX: "∀A∈F. ∃⇩∞i. r i ∈ (A ∩ range r)"
unfolding is_acc_def by auto
have "∀A∈F. limit r ∩ (A ∩ range r) ≠ {}"
apply (rule ballI)
apply (drule bspec[OF AUX])
apply (subst (asm) fin_ex_inf_eq_limit[OF FIN'])
.
thus "∀A∈F. limit r ∩ A ≠ {}"
by auto
qed
lemma is_acc_run_limit_alt:
assumes "finite (E⇧* `` V0)"
shows "is_acc_run r ⟷ is_run r ∧ (∀A∈F. limit r ∩ A ≠ {})"
using assms acc_eq_limit[symmetric] unfolding is_acc_run_def
by (auto dest: run_reachable finite_subset)
lemma is_acc_suffix[simp]: "is_acc (suffix i r) ⟷ is_acc r"
unfolding is_acc_def suffix_def
apply (clarsimp simp: INFM_nat)
apply (rule iffI)
apply (metis trans_less_add2)
by (metis add_lessD1 less_imp_add_positive nat_add_left_cancel_less)
lemma finite_V_Fe:
assumes "finite V" "A ∈ F"
shows "finite A"
using assms by (metis Pow_iff infinite_super rev_subsetD F_ss)
end
definition "gb_rename_ecnv ecnv f G ≡ ⦇
gbg_F = { f`A | A. A∈gbg_F G }, … = ecnv G
⦈"
abbreviation "gb_rename_ext ecnv f ≡ fr_rename_ext (gb_rename_ecnv ecnv f) f"
locale gb_rename_precond =
gb_graph G +
g_rename_precond G f "gb_rename_ecnv ecnv f"
for G :: "('u,'more) gb_graph_rec_scheme"
and f :: "'u ⇒ 'v" and ecnv
begin
lemma G'_gb_fields: "gbg_F G' = { f`A | A. A∈F }"
unfolding gb_rename_ecnv_def fr_rename_ext_def
by simp
sublocale G': gb_graph G'
apply unfold_locales
apply (simp_all add: G'_fields G'_gb_fields)
using F_ss
by auto
lemma acc_sim1: "is_acc r ⟹ G'.is_acc (f o r)"
unfolding is_acc_def G'.is_acc_def G'_gb_fields
by (fastforce intro: imageI simp: INFM_nat)
lemma acc_sim2:
assumes "G'.is_acc r" shows "is_acc (fi o r)"
proof -
from assms have 1: "⋀A m. A ∈ gbg_F G ⟹ ∃i>m. r i ∈ f`A"
unfolding G'.is_acc_def G'_gb_fields
by (auto simp: INFM_nat)
{ fix A m
assume 2: "A ∈ gbg_F G"
from 1[OF this, of m] have "∃i>m. fi (r i) ∈ A"
using F_ss
apply clarsimp
by (metis Pow_iff 2 fi_f in_mono)
} thus ?thesis
unfolding is_acc_def
by (auto simp: INFM_nat)
qed
lemma acc_run_sim1: "is_acc_run r ⟹ G'.is_acc_run (f o r)"
using acc_sim1 run_sim1 unfolding G'.is_acc_run_def is_acc_run_def
by auto
lemma acc_run_sim2: "G'.is_acc_run r ⟹ is_acc_run (fi o r)"
using acc_sim2 run_sim2 unfolding G'.is_acc_run_def is_acc_run_def
by auto
end
subsection "Generalized Buchi Automata"
text ‹
A GBA is obtained from a GBG by adding a labeling function, that associates
each state with a set of labels. A word is accepted if there is an
accepting run that can be labeld with this word.
›
record ('Q,'L) gba_rec = "'Q gb_graph_rec" +
gba_L :: "'Q ⇒ 'L ⇒ bool"
locale gba =
gb_graph G
for G :: "('Q,'L,'more) gba_rec_scheme" +
assumes L_ss: "gba_L G q l ⟹ q ∈ V"
begin
abbreviation "L ≡ gba_L G"
lemma is_gba: "gba G" by unfold_locales
definition "accept w ≡ ∃r. is_acc_run r ∧ (∀i. L (r i) (w i))"
lemma acceptI[intro?]: "⟦is_acc_run r; ⋀i. L (r i) (w i)⟧ ⟹ accept w"
by (auto simp: accept_def)
definition "lang ≡ Collect (accept)"
lemma langI[intro?]: "accept w ⟹ w∈lang" by (auto simp: lang_def)
end
definition "gba_rename_ecnv ecnv f G ≡ ⦇
gba_L = λq l.
if q∈f`g_V G then
gba_L G (the_inv_into (g_V G) f q) l
else
False,
… = ecnv G
⦈"
abbreviation "gba_rename_ext ecnv f ≡ gb_rename_ext (gba_rename_ecnv ecnv f) f"
locale gba_rename_precond =
gb_rename_precond G f "gba_rename_ecnv ecnv f" + gba G
for G :: "('u,'L,'more) gba_rec_scheme"
and f :: "'u ⇒ 'v" and ecnv
begin
lemma G'_gba_fields: "gba_L G' = (λq l.
if q∈f`V then L (fi q) l else False)"
unfolding gb_rename_ecnv_def gba_rename_ecnv_def fr_rename_ext_def fi_def
by simp
sublocale G': gba G'
apply unfold_locales
apply (auto simp add: G'_gba_fields G'_fields split: if_split_asm)
done
lemma L_sim1: "⟦range r ⊆ V; L (r i) l⟧ ⟹ G'.L (f (r i)) l"
by (auto simp: G'_gba_fields fi_def[symmetric] fi_f
dest: inj_onD[OF INJ]
dest!: rev_subsetD[OF rangeI[of _ i]])
lemma L_sim2: "⟦ range r ⊆ f`V; G'.L (r i) l ⟧ ⟹ L (fi (r i)) l"
by (auto
simp: G'_gba_fields fi_def[symmetric] f_fi
dest!: rev_subsetD[OF rangeI[of _ i]])
lemma accept_eq[simp]: "G'.accept = accept"
apply (rule ext)
unfolding accept_def G'.accept_def
proof safe
fix w r
assume R: "G'.is_acc_run r"
assume L: "∀i. G'.L (r i) (w i)"
from R have RAN: "range r ⊆ f`V"
using G'.run_reachable[OF G'.acc_run_run[OF R]] G'.reachable_V
unfolding G'_fields
by simp
from L show "∃r. is_acc_run r ∧ (∀i. L (r i) (w i))"
using acc_run_sim2[OF R] L_sim2[OF RAN]
by auto
next
fix w r
assume R: "is_acc_run r"
assume L: "∀i. L (r i) (w i)"
from R have RAN: "range r ⊆ V"
using run_reachable[OF acc_run_run[OF R]] reachable_V by simp
from L show "∃r.
G'.is_acc_run r
∧ (∀i. G'.L (r i) (w i))"
using acc_run_sim1[OF R] L_sim1[OF RAN]
by auto
qed
lemma lang_eq[simp]: "G'.lang = lang"
unfolding G'.lang_def lang_def by simp
lemma finite_G'_V:
assumes "finite V"
shows "finite G'.V"
using assms by (auto simp add: G'_gba_fields G'_fields split: if_split_asm)
end
abbreviation "gba_rename ≡ gba_rename_ext (λ_. ())"
lemma gba_rename_correct:
fixes G :: "('v,'l,'m) gba_rec_scheme"
assumes "gba G"
assumes INJ: "inj_on f (g_V G)"
defines "G' ≡ gba_rename f G"
shows "gba G'"
and "finite (g_V G) ⟹ finite (g_V G')"
and "gba.accept G' = gba.accept G"
and "gba.lang G' = gba.lang G"
unfolding G'_def
proof -
let ?G' = "gba_rename f G"
interpret gba G by fact
from INJ interpret gba_rename_precond G f "λ_. ()"
by unfold_locales simp_all
show "gba ?G'" by (rule G'.is_gba)
show "finite (g_V G) ⟹ finite (g_V ?G')" by (fact finite_G'_V)
show "G'.accept = accept" by simp
show "G'.lang = lang" by simp
qed
subsection "Buchi Graphs"
text ‹A Buchi graph has exactly one acceptance class›
record 'Q b_graph_rec = "'Q graph_rec" +
bg_F :: "'Q set"
locale b_graph =
graph G
for G :: "('Q,'more) b_graph_rec_scheme"
+
assumes F_ss: "bg_F G ⊆ V"
begin
abbreviation F where "F ≡ bg_F G"
lemma is_b_graph: "b_graph G" by unfold_locales
definition "to_gbg_ext m
≡ ⦇ g_V = V,
g_E=E,
g_V0=V0,
gbg_F = if F=UNIV then {} else {F},
… = m ⦈"
abbreviation "to_gbg ≡ to_gbg_ext ()"
sublocale gbg: gb_graph "to_gbg_ext m"
apply unfold_locales
using V0_ss E_ss F_ss
apply (auto simp: to_gbg_ext_def split: if_split_asm)
done
definition is_acc :: "'Q word ⇒ bool" where "is_acc r ≡ (∃⇩∞i. r i ∈ F)"
definition is_acc_run where "is_acc_run r ≡ is_run r ∧ is_acc r"
lemma to_gbg_alt:
"gbg.V T m = V"
"gbg.E T m = E"
"gbg.V0 T m = V0"
"gbg.F T m = (if F=UNIV then {} else {F})"
"gbg.is_run T m = is_run"
"gbg.is_acc T m = is_acc"
"gbg.is_acc_run T m = is_acc_run"
unfolding is_run_def[abs_def] gbg.is_run_def[abs_def]
is_acc_def[abs_def] gbg.is_acc_def[abs_def]
is_acc_run_def[abs_def] gbg.is_acc_run_def[abs_def]
by (auto simp: to_gbg_ext_def)
end
subsection "Buchi Automata"
text ‹Buchi automata are labeled Buchi graphs›
record ('Q,'L) ba_rec = "'Q b_graph_rec" +
ba_L :: "'Q ⇒ 'L ⇒ bool"
locale ba =
bg?: b_graph G
for G :: "('Q,'L,'more) ba_rec_scheme"
+
assumes L_ss: "ba_L G q l ⟹ q ∈ V"
begin
abbreviation L where "L == ba_L G"
lemma is_ba: "ba G" by unfold_locales
abbreviation "to_gba_ext m ≡ to_gbg_ext ⦇ gba_L = L, …=m ⦈"
abbreviation "to_gba ≡ to_gba_ext ()"
sublocale gba: gba "to_gba_ext m"
apply unfold_locales
unfolding to_gbg_ext_def
using L_ss apply auto []
done
lemma ba_acc_simps[simp]: "gba.L T m = L"
by (simp add: to_gbg_ext_def)
definition "accept w ≡ (∃r. is_acc_run r ∧ (∀i. L (r i) (w i)))"
definition "lang ≡ Collect accept"
lemma to_gba_alt_accept:
"gba.accept T m = accept"
apply (intro ext)
unfolding accept_def gba.accept_def
apply (simp_all add: to_gbg_alt)
done
lemma to_gba_alt_lang:
"gba.lang T m = lang"
unfolding lang_def gba.lang_def
apply (simp_all add: to_gba_alt_accept)
done
lemmas to_gba_alt = to_gbg_alt to_gba_alt_accept to_gba_alt_lang
end
subsection "Indexed acceptance classes"
record 'Q igb_graph_rec = "'Q graph_rec" +
igbg_num_acc :: nat
igbg_acc :: "'Q ⇒ nat set"
locale igb_graph =
graph G
for G :: "('Q,'more) igb_graph_rec_scheme"
+
assumes acc_bound: "⋃(range (igbg_acc G)) ⊆ {0..<(igbg_num_acc G)}"
assumes acc_ss: "igbg_acc G q ≠ {} ⟹ q∈V"
begin
abbreviation num_acc where "num_acc ≡ igbg_num_acc G"
abbreviation acc where "acc ≡ igbg_acc G"
lemma is_igb_graph: "igb_graph G" by unfold_locales
lemma acc_boundI[simp, intro]: "x∈acc q ⟹ x<num_acc"
using acc_bound by fastforce
definition "accn i ≡ {q . i∈acc q}"
definition "F ≡ { accn i | i. i<num_acc }"
definition "to_gbg_ext m
≡ ⦇ g_V = V, g_E = E, g_V0 = V0, gbg_F = F, …=m ⦈"
sublocale gbg: gb_graph "to_gbg_ext m"
apply unfold_locales
using V0_ss E_ss acc_ss
apply (auto simp: to_gbg_ext_def F_def accn_def)
done
lemma to_gbg_alt1:
"gbg.E T m = E"
"gbg.V0 T m = V0"
"gbg.F T m = F"
by (simp_all add: to_gbg_ext_def)
lemma F_fin[simp,intro!]: "finite F"
unfolding F_def
by auto
definition is_acc :: "'Q word ⇒ bool"
where "is_acc r ≡ (∀n<num_acc. ∃⇩∞i. n ∈ acc (r i))"
definition "is_acc_run r ≡ is_run r ∧ is_acc r"
lemma is_run_gbg:
"gbg.is_run T m = is_run"
unfolding is_run_def[abs_def] is_acc_run_def[abs_def]
gbg.is_run_def[abs_def] gbg.is_acc_run_def[abs_def]
by (simp_all add: to_gbg_ext_def)
lemma is_acc_gbg:
"gbg.is_acc T m = is_acc"
apply (intro ext)
unfolding gbg.is_acc_def is_acc_def
apply (simp add: to_gbg_alt1 is_run_gbg)
unfolding F_def accn_def
apply (blast intro: INFM_mono)
done
lemma is_acc_run_gbg:
"gbg.is_acc_run T m = is_acc_run"
apply (intro ext)
unfolding gbg.is_acc_run_def is_acc_run_def
by (simp_all add: to_gbg_alt1 is_run_gbg is_acc_gbg)
lemmas to_gbg_alt = to_gbg_alt1 is_run_gbg is_acc_gbg is_acc_run_gbg
lemma acc_limit_alt:
assumes FIN: "finite (range r)"
shows "is_acc r ⟷ (∀n<num_acc. limit r ∩ accn n ≠ {})"
proof
assume "∀n<num_acc. limit r ∩ accn n ≠ {}"
thus "is_acc r"
unfolding is_acc_def accn_def
by (auto dest!: limit_inter_INF)
next
from FIN have FIN': "⋀A. finite (A ∩ range r)" by simp
assume "is_acc r"
hence "∀n<num_acc. limit r ∩ (accn n ∩ range r) ≠ {}"
unfolding is_acc_def accn_def
by (auto simp: fin_ex_inf_eq_limit[OF FIN', symmetric])
thus "∀n<num_acc. limit r ∩ accn n ≠ {}" by auto
qed
lemma acc_limit_alt':
"finite (range r) ⟹ is_acc r ⟷ (⋃(acc ` limit r) = {0..<num_acc})"
unfolding acc_limit_alt
by (auto simp: accn_def)
end
record ('Q,'L) igba_rec = "'Q igb_graph_rec" +
igba_L :: "'Q ⇒ 'L ⇒ bool"
locale igba =
igbg?: igb_graph G
for G :: "('Q,'L,'more) igba_rec_scheme"
+
assumes L_ss: "igba_L G q l ⟹ q ∈ V"
begin
abbreviation L where "L ≡ igba_L G"
lemma is_igba: "igba G" by unfold_locales
abbreviation "to_gba_ext m ≡ to_gbg_ext ⦇ gba_L = igba_L G, …=m ⦈"
sublocale gba: gba "to_gba_ext m"
apply unfold_locales
unfolding to_gbg_ext_def
using L_ss
apply auto
done
lemma to_gba_alt_L:
"gba.L T m = L"
by (auto simp: to_gbg_ext_def)
definition "accept w ≡ ∃r. is_acc_run r ∧ (∀i. L (r i) (w i))"
definition "lang ≡ Collect accept"
lemma accept_gba_alt: "gba.accept T m = accept"
apply (intro ext)
unfolding accept_def gba.accept_def
apply (simp add: to_gbg_alt to_gba_alt_L)
done
lemma lang_gba_alt: "gba.lang T m = lang"
unfolding lang_def gba.lang_def
apply (simp add: accept_gba_alt)
done
lemmas to_gba_alt = to_gbg_alt to_gba_alt_L accept_gba_alt lang_gba_alt
end
subsubsection ‹Indexing Conversion›
definition F_to_idx :: "'Q set set ⇒ (nat × ('Q ⇒ nat set)) nres" where
"F_to_idx F ≡ do {
Flist ← SPEC (λFlist. distinct Flist ∧ set Flist = F);
let num_acc = length Flist;
let acc = (λv. {i . i<num_acc ∧ v∈Flist!i});
RETURN (num_acc,acc)
}"
lemma F_to_idx_correct:
shows "F_to_idx F ≤ SPEC (λ(num_acc,acc). F = { {q. i∈acc q} | i. i<num_acc }
∧ ⋃(range acc) ⊆ {0..<num_acc})"
unfolding F_to_idx_def
apply (refine_rcg refine_vcg)
apply (clarsimp dest!: sym[where t=F])
apply (intro equalityI subsetI)
apply (auto simp: in_set_conv_nth) [2]
apply auto []
done
definition "mk_acc_impl Flist ≡ do {
let acc = Map.empty;
(_,acc) ← nfoldli Flist (λ_. True) (λA (i,acc). do {
acc ← FOREACHi (λit acc'.
acc' = (λv.
if v∈A-it then
Some (insert i (the_default {} (acc v)))
else
acc v
)
)
A (λv acc. RETURN (acc(v↦insert i (the_default {} (acc v))))) acc;
RETURN (Suc i,acc)
}) (0,acc);
RETURN (λx. the_default {} (acc x))
}"
lemma mk_acc_impl_correct:
assumes F: "(Flist',Flist)∈Id"
assumes FIN: "∀A∈set Flist. finite A"
shows "mk_acc_impl Flist' ≤ ⇓Id (RETURN (λv. {i . i<length Flist ∧ v∈Flist!i}))"
using F apply simp
unfolding mk_acc_impl_def
apply (refine_rcg
nfoldli_rule[where
I="λl1 l2 (i,res). i=length l1
∧ the_default {} o res = (λv. {j . j<i ∧ v∈Flist!j})"
]
refine_vcg
)
using FIN apply (simp_all)
apply (rule ext) apply auto []
apply (rule ext) apply (auto split: if_split_asm simp: nth_append nth_Cons') []
apply (rule ext) apply (auto split: if_split_asm simp: nth_append nth_Cons'
fun_comp_eq_conv) []
apply (rule ext) apply (auto simp: fun_comp_eq_conv) []
done
definition F_to_idx_impl :: "'Q set set ⇒ (nat × ('Q ⇒ nat set)) nres" where
"F_to_idx_impl F ≡ do {
Flist ← SPEC (λFlist. distinct Flist ∧ set Flist = F);
let num_acc = length Flist;
acc ← mk_acc_impl Flist;
RETURN (num_acc,acc)
}"
lemma F_to_idx_refine:
assumes FIN: "∀A∈F. finite A"
shows "F_to_idx_impl F ≤ ⇓Id (F_to_idx F)"
using assms
unfolding F_to_idx_impl_def F_to_idx_def
apply (refine_rcg bind_Let_refine2[OF mk_acc_impl_correct])
apply auto
done
definition gbg_to_idx_ext
:: "_ ⇒ ('a, 'more) gb_graph_rec_scheme ⇒ ('a, 'more') igb_graph_rec_scheme nres"
where "gbg_to_idx_ext ecnv A = do {
(num_acc,acc) ← F_to_idx_impl (gbg_F A);
RETURN ⦇
g_V = g_V A,
g_E = g_E A,
g_V0=g_V0 A,
igbg_num_acc = num_acc,
igbg_acc = acc,
… = ecnv A
⦈
}"
lemma (in gb_graph) gbg_to_idx_ext_correct:
assumes [simp, intro]: "⋀ A. A ∈ F ⟹ finite A"
shows "gbg_to_idx_ext ecnv G ≤ SPEC (λG'.
igb_graph.is_acc_run G' = is_acc_run
∧ g_V G' = V
∧ g_E G' = E
∧ g_V0 G' = V0
∧ igb_graph_rec.more G' = ecnv G
∧ igb_graph G'
)"
proof -
note F_to_idx_refine[of F]
also note F_to_idx_correct
finally have R: "F_to_idx_impl F
≤ SPEC (λ(num_acc, acc). F = {{q. i ∈ acc q} |i. i < num_acc}
∧ ⋃(range acc) ⊆ {0..<num_acc})" by simp
have eq_conjI: "⋀a b c. (b⟷c) ⟹ (a&b ⟷ a&c)" by simp
{
fix acc :: "'Q ⇒ nat set" and num_acc r
have "(∀A. (∃i. A = {q. i ∈ acc q} ∧ i < num_acc) ⟶ (limit r ∩ A ≠ {}))
⟷ (∀i<num_acc. ∃q∈limit r. i∈acc q)"
by blast
} note aux1=this
{
fix acc :: "'Q ⇒ nat set" and num_acc i
assume FE: "F = {{q. i ∈ acc q} |i. i < num_acc}"
assume INR: "(⋃x. acc x) ⊆ {0..<num_acc}"
have "finite {q. i ∈ acc q}"
proof (cases "i<num_acc")
case True thus ?thesis using FE by auto
next
case False hence "{q. i ∈ acc q} = {}" using INR by force
thus ?thesis by simp
qed
} note aux2=this
{
fix acc :: "'Q ⇒ nat set" and num_acc q
assume FE: "F = {{q. i ∈ acc q} |i. i < num_acc}"
and INR: "(⋃x. acc x) ⊆ {0..<num_acc}"
and "acc q ≠ {}"
then obtain i where "i∈acc q" by auto
moreover with INR have "i<num_acc" by force
ultimately have "q∈⋃F" by (auto simp: FE)
with F_ss have "q∈V" by auto
} note aux3=this
show ?thesis
unfolding gbg_to_idx_ext_def
apply (refine_rcg order_trans[OF R] refine_vcg)
proof clarsimp_all
fix acc and num_acc :: nat
assume FE[simp]: "F = {{q. i ∈ acc q} |i. i < num_acc}"
and BOUND: "(⋃x. acc x) ⊆ {0..<num_acc}"
let ?G' = "⦇
g_V = V,
g_E = E,
g_V0 = V0,
igbg_num_acc = num_acc,
igbg_acc = acc,
… = ecnv G⦈"
interpret G': igb_graph ?G'
apply unfold_locales
using V0_ss E_ss
apply (auto simp add: aux2 aux3 BOUND)
done
show "igb_graph ?G'" by unfold_locales
show "G'.is_acc_run = is_acc_run"
unfolding G'.is_acc_run_def[abs_def] is_acc_run_def[abs_def]
G'.is_run_def[abs_def] is_run_def[abs_def]
G'.is_acc_def[abs_def] is_acc_def[abs_def]
apply (clarsimp intro!: ext eq_conjI)
apply auto []
apply (metis (lifting, no_types) INFM_mono mem_Collect_eq)
done
qed
qed
abbreviation gbg_to_idx :: "('q,_) gb_graph_rec_scheme ⇒ 'q igb_graph_rec nres"
where "gbg_to_idx ≡ gbg_to_idx_ext (λ_. ())"
definition ti_Lcnv where "ti_Lcnv ecnv A ≡ ⦇ igba_L = gba_L A, …=ecnv A ⦈"
abbreviation "gba_to_idx_ext ecnv ≡ gbg_to_idx_ext (ti_Lcnv ecnv)"
abbreviation "gba_to_idx ≡ gba_to_idx_ext (λ_. ())"
lemma (in gba) gba_to_idx_ext_correct:
assumes [simp, intro]: "⋀ A. A ∈ F ⟹ finite A"
shows "gba_to_idx_ext ecnv G ≤
SPEC (λG'.
igba.accept G' = accept
∧ g_V G' = V
∧ g_E G' = E
∧ g_V0 G' = V0
∧ igba_rec.more G' = ecnv G
∧ igba G')"
apply (rule order_trans[OF gbg_to_idx_ext_correct])
apply (rule, assumption)
apply (rule SPEC_rule)
apply (elim conjE, intro conjI)
proof -
fix G'
assume
ARUN: "igb_graph.is_acc_run G' = is_acc_run"
and MORE: "igb_graph_rec.more G' = ti_Lcnv ecnv G"
and LOC: "igb_graph G'"
and FIELDS: "g_V G' = V" "g_E G' = E" "g_V0 G' = V0"
from LOC interpret igb: igb_graph G' .
interpret igb: igba G'
apply unfold_locales
using MORE FIELDS L_ss
unfolding ti_Lcnv_def
apply (cases G')
apply simp
done
show "igba.accept G' = accept" and "igba_rec.more G' = ecnv G"
using ARUN MORE
unfolding accept_def[abs_def] igb.accept_def[abs_def] ti_Lcnv_def
apply (cases G', (auto) []) +
done
show "igba G'" by unfold_locales
qed
corollary (in gba) gba_to_idx_ext_lang_correct:
assumes [simp, intro]: "⋀ A. A ∈ F ⟹ finite A"
shows "gba_to_idx_ext ecnv G ≤
SPEC (λG'. igba.lang G' = lang ∧ igba_rec.more G' = ecnv G ∧ igba G')"
apply (rule order_trans[OF gba_to_idx_ext_correct])
apply (rule, assumption)
apply (rule SPEC_rule)
unfolding lang_def[abs_def]
apply (subst igba.lang_def)
apply auto
done
subsubsection ‹Degeneralization›
context igb_graph
begin
definition degeneralize_ext :: "_ ⇒ ('Q × nat, _) b_graph_rec_scheme" where
"degeneralize_ext ecnv ≡
if num_acc = 0 then ⦇
g_V = V × {0},
g_E = {((q,0),(q',0)) | q q'. (q,q')∈E},
g_V0 = V0×{0},
bg_F = V × {0},
… = ecnv G
⦈
else ⦇
g_V = V × {0..<num_acc},
g_E = { ((q,i),(q',i')) | i i' q q'.
i<num_acc
∧ (q,q')∈E
∧ i' = (if i∈acc q then (i+1) mod num_acc else i) },
g_V0 = V0 × {0},
bg_F = {(q,0)| q. 0∈acc q},
… = ecnv G
⦈"
abbreviation degeneralize where "degeneralize ≡ degeneralize_ext (λ_. ())"
lemma degen_more[simp]: "b_graph_rec.more (degeneralize_ext ecnv) = ecnv G"
unfolding degeneralize_ext_def
by auto
lemma degen_invar: "b_graph (degeneralize_ext ecnv)"
proof
let ?G' = "degeneralize_ext ecnv"
show "g_V0 ?G' ⊆ g_V ?G'"
unfolding degeneralize_ext_def
using V0_ss
by auto
show "g_E ?G' ⊆ g_V ?G' × g_V ?G'"
unfolding degeneralize_ext_def
using E_ss
by auto
show "bg_F ?G' ⊆ g_V ?G'"
unfolding degeneralize_ext_def
using acc_ss
by auto
qed
sublocale degen: b_graph "degeneralize_ext m" using degen_invar .
lemma degen_finite_reachable:
assumes [simp, intro]: "finite (E⇧* `` V0)"
shows "finite ((g_E (degeneralize_ext ecnv))⇧* `` g_V0 (degeneralize_ext ecnv))"
proof -
let ?G' = "degeneralize_ext ecnv"
have "((g_E ?G')⇧* `` g_V0 ?G')
⊆ E⇧*``V0 × {0..num_acc}"
proof -
{
fix q n q' n'
assume "((q,n),(q',n'))∈(g_E ?G')⇧*"
and 0: "(q,n)∈g_V0 ?G'"
hence G1: "(q,q')∈E⇧* ∧ n'≤num_acc"
apply (induction rule: rtrancl_induct2)
by (auto simp: degeneralize_ext_def split: if_split_asm)
from 0 have G2: "q∈V0 ∧ n≤num_acc"
by (auto simp: degeneralize_ext_def split: if_split_asm)
note G1 G2
} thus ?thesis by fastforce
qed
also have "finite …" by auto
finally (finite_subset) show "finite ((g_E ?G')⇧* `` g_V0 ?G')" .
qed
lemma degen_is_run_sound:
"degen.is_run T m r ⟹ is_run (fst o r)"
unfolding degen.is_run_def is_run_def
unfolding degeneralize_ext_def
apply (clarsimp split: if_split_asm simp: ipath_def)
apply (metis fst_conv)+
done
lemma degen_path_sound:
assumes "path (degen.E T m) u p v"
shows "path E (fst u) (map fst p) (fst v)"
using assms
by induction (auto simp: degeneralize_ext_def path_simps split: if_split_asm)
lemma degen_V0_sound:
assumes "u ∈ degen.V0 T m"
shows "fst u ∈ V0"
using assms
by (auto simp: degeneralize_ext_def path_simps split: if_split_asm)
lemma degen_visit_acc:
assumes "path (degen.E T m) (q,n) p (q',n')"
assumes "n≠n'"
shows "∃qa. (qa,n)∈set p ∧ n∈acc qa"
using assms
proof (induction _ "(q,n)" p "(q',n')" arbitrary: q rule: path.induct)
case (path_prepend qnh p)
then obtain qh nh where [simp]: "qnh=(qh,nh)" by (cases qnh)
from ‹((q,n),qnh) ∈ degen.E T m›
have "nh=n ∨ (nh=(n+1) mod num_acc ∧ n∈acc q)"
by (auto simp: degeneralize_ext_def split: if_split_asm)
thus ?case proof
assume [simp]: "nh=n"
from path_prepend obtain qa where "(qa, n) ∈ set p" and "n ∈ acc qa"
by auto
thus ?case by auto
next
assume "(nh=(n+1) mod num_acc ∧ n∈acc q)" thus ?case by auto
qed
qed simp
lemma degen_run_complete0:
assumes [simp]: "num_acc = 0"
assumes R: "is_run r"
shows "degen.is_run T m (λi. (r i,0))"
using R
unfolding degen.is_run_def is_run_def
unfolding ipath_def degeneralize_ext_def
by auto
lemma degen_acc_run_complete0:
assumes [simp]: "num_acc = 0"
assumes R: "is_acc_run r"
shows "degen.is_acc_run T m (λi. (r i,0))"
using R
unfolding degen.is_acc_run_def is_acc_run_def is_acc_def degen.is_acc_def
apply (simp add: degen_run_complete0)
unfolding degeneralize_ext_def
using run_reachable[of r] reachable_V
by (auto simp: INFM_nat)
lemma degen_run_complete:
assumes [simp]: "num_acc ≠ 0"
assumes R: "is_run r"
shows "∃r'. degen.is_run T m r' ∧ r = fst o r'"
using R
unfolding degen.is_run_def is_run_def ipath_def
apply (elim conjE)
proof -
assume R0: "r 0 ∈ V0" and RS: "∀i. (r i, r (Suc i)) ∈ E"
define r' where "r' = rec_nat
(r 0,0)
(λi (q,n). (r (Suc i), if n ∈ acc q then (n+1) mod num_acc else n))"
have [simp]:
"r' 0 = (r 0,0)"
"⋀i. r' (Suc i) = (
let
(q,n)=r' i
in
(r (Suc i), if n ∈ acc q then (n+1) mod num_acc else n)
)"
unfolding r'_def
by auto
have R0': "r' 0 ∈ degen.V0 T m" using R0
unfolding degeneralize_ext_def by auto
have MAP: "r = fst o r'"
proof (rule ext)
fix i
show "r i = (fst o r') i"
by (cases i) (auto simp: split: prod.split)
qed
have [simp]: "0<num_acc" by (cases num_acc) auto
have SND_LESS: "⋀i. snd (r' i) < num_acc"
proof -
fix i show "snd (r' i) < num_acc" by (induction i) (auto split: prod.split)
qed
have RS': "∀i. (r' i, r' (Suc i)) ∈ degen.E T m"
proof
fix i
obtain n where [simp]: "r' i = (r i,n)"
apply (cases i)
apply (force)
apply (force split: prod.split)
done
from SND_LESS[of i] have [simp]: "n<num_acc" by simp
show "(r' i, r' (Suc i)) ∈ degen.E T m" using RS
by (auto simp: degeneralize_ext_def)
qed
from R0' RS' MAP show
"∃r'. (r' 0 ∈ degen.V0 T m
∧ (∀i. (r' i, r' (Suc i)) ∈ degen.E T m))
∧ r = fst ∘ r'" by blast
qed
lemma degen_run_bound:
assumes [simp]: "num_acc ≠ 0"
assumes R: "degen.is_run T m r"
shows "snd (r i) < num_acc"
apply (induction i)
using R
unfolding degen.is_run_def is_run_def
unfolding degeneralize_ext_def ipath_def
apply -
apply auto []
apply clarsimp
by (metis snd_conv)
lemma degen_acc_run_complete_aux1:
assumes NN0[simp]: "num_acc ≠ 0"
assumes R: "degen.is_run T m r"
assumes EXJ: "∃j≥i. n ∈ acc (fst (r j))"
assumes RI: "r i = (q,n)"
shows "∃j≥i. ∃q'. r j = (q',n) ∧ n ∈ acc q'"
proof -
define j where "j = (LEAST j. j≥i ∧ n ∈ acc (fst (r j)))"
from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
from EXJ have
"j≥i"
"n ∈ acc (fst (r j))"
"∀k≥i. n ∈ acc (fst (r k)) ⟶ j≤k"
using LeastI_ex[OF EXJ]
unfolding j_def
apply (auto) [2]
apply (metis (lifting) Least_le)
done
hence "∀k≥i. k<j ⟶ n ∉ acc (fst (r k))" by auto
have "∀k. k≥i ∧ k≤j ⟶ (snd (r k) = n)"
proof (clarify)
fix k
assume "i≤k" "k≤j"
thus "snd (r k) = n"
proof (induction k rule: less_induct)
case (less k)
show ?case proof (cases "k=i")
case True thus ?thesis using RI by simp
next
case False with less.prems have "k - 1 < k" "i ≤ k - 1" "k - 1≤j"
by auto
from less.IH[OF this] have "snd (r (k - 1)) = n" .
moreover from R have
"(r (k - 1), r k) ∈ degen.E T m"
unfolding degen.is_run_def is_run_def ipath_def
by clarsimp (metis One_nat_def Suc_diff_1 ‹k - 1 < k›
less_nat_zero_code neq0_conv)
moreover have "n ∉ acc (fst (r (k - 1)))"
using ‹∀k≥i. k < j ⟶ n ∉ acc (fst (r k))› ‹i ≤ k - 1› ‹k - 1 < k›
dual_order.strict_trans1 less.prems(2)
by blast
ultimately show ?thesis
by (auto simp: degeneralize_ext_def)
qed
qed
qed
thus ?thesis
by (metis ‹i ≤ j› ‹n ∈ local.acc (fst (r j))›
order_refl surjective_pairing)
qed
lemma degen_acc_run_complete_aux1':
assumes NN0[simp]: "num_acc ≠ 0"
assumes R: "degen.is_run T m r"
assumes ACC: "∀n<num_acc. ∃⇩∞i. n ∈ acc (fst (r i))"
assumes RI: "r i = (q,n)"
shows "∃j≥i. ∃q'. r j = (q',n) ∧ n ∈ acc q'"
proof -
from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
with ACC have EXJ: "∃j≥i. n ∈ acc (fst (r j))"
unfolding INFM_nat_le by blast
from degen_acc_run_complete_aux1[OF NN0 R EXJ RI] show ?thesis .
qed
lemma degen_acc_run_complete_aux2:
assumes NN0[simp]: "num_acc ≠ 0"
assumes R: "degen.is_run T m r"
assumes ACC: "∀n<num_acc. ∃⇩∞i. n ∈ acc (fst (r i))"
assumes RI: "r i = (q,n)" and OFS: "ofs<num_acc"
shows "∃j≥i. ∃q'.
r j = (q',(n + ofs) mod num_acc) ∧ (n + ofs) mod num_acc ∈ acc q'"
using RI OFS
proof (induction ofs arbitrary: q n i)
case 0
from degen_run_bound[OF NN0 R, of i] ‹r i = (q, n)›
have NLE: "n<num_acc"
by simp
with degen_acc_run_complete_aux1'[OF NN0 R ACC ‹r i = (q, n)›] show ?case
by auto
next
case (Suc ofs)
from Suc.IH[OF Suc.prems(1)] Suc.prems(2)
obtain j q' where "j≥i" and RJ: "r j = (q',(n+ofs) mod num_acc)"
and A: "(n+ofs) mod num_acc ∈ acc q'"
by auto
from R have "(r j, r (Suc j)) ∈ degen.E T m"
by (auto simp: degen.is_run_def is_run_def ipath_def)
with RJ A obtain q2 where RSJ: "r (Suc j) = (q2,(n+Suc ofs) mod num_acc)"
by (auto simp: degeneralize_ext_def mod_simps)
have aux: "⋀j'. i≤j ⟹ Suc j ≤ j' ⟹ i≤j'" by auto
from degen_acc_run_complete_aux1'[OF NN0 R ACC RSJ] ‹j≥i›
show ?case
by (auto dest: aux)
qed
lemma degen_acc_run_complete:
assumes AR: "is_acc_run r"
obtains r'
where "degen.is_acc_run T m r'" and "r = fst o r'"
proof (cases "num_acc = 0")
case True
with AR degen_acc_run_complete0
show ?thesis by (auto intro!: that[of "(λi. (r i, 0))"])
next
case False
assume NN0[simp]: "num_acc ≠ 0"
from AR have R: "is_run r" and ACC: "∀n<num_acc. ∃⇩∞i. n ∈ acc (r i)"
unfolding is_acc_run_def is_acc_def by auto
from degen_run_complete[OF NN0 R] obtain r' where
R': "degen.is_run T m r'"
and [simp]: "r = fst ∘ r'"
by auto
from ACC have ACC': "∀n<num_acc. ∃⇩∞i. n ∈ acc (fst (r' i))" by simp
have "∀i. ∃j>i. r' j ∈ degen.F T m"
proof
fix i
obtain q n where RI: "r' (Suc i) = (q,n)" by (cases "r' (Suc i)")
have "(n + (num_acc - n mod num_acc)) mod num_acc = 0"
apply (rule dvd_imp_mod_0)
apply (metis (mono_tags, lifting) NN0 add_diff_inverse mod_0_imp_dvd
mod_add_left_eq mod_less_divisor mod_self nat_diff_split not_gr_zero zero_less_diff)
done
then obtain ofs where
OFS_LESS: "ofs<num_acc"
and [simp]: "(n + ofs) mod num_acc = 0"
by (metis NN0 Nat.add_0_right diff_less neq0_conv)
with degen_acc_run_complete_aux2[OF NN0 R' ACC' RI OFS_LESS]
obtain j q' where
"j>i" "r' j = (q',0)" and "0∈acc q'"
by (auto simp: less_eq_Suc_le)
thus "∃j>i. r' j ∈ degen.F T m"
by (auto simp: degeneralize_ext_def)
qed
hence "∃⇩∞i. r' i ∈ degen.F T m" by (auto simp: INFM_nat)
have "degen.is_acc_run T m r'"
unfolding degen.is_acc_run_def degen.is_acc_def
by rule fact+
thus ?thesis by (auto intro: that)
qed
lemma degen_run_find_change:
assumes NN0[simp]: "num_acc ≠ 0"
assumes R: "degen.is_run T m r"
assumes A: "i≤j" "r i = (q,n)" "r j = (q',n')" "n≠n'"
obtains k qk where "i≤k" "k<j" "r k = (qk,n)" "n ∈ acc qk"
proof -
from degen_run_bound[OF NN0 R] A have "n<num_acc" "n'<num_acc"
by (metis snd_conv)+
define k where "k = (LEAST k. i<k ∧ snd (r k) ≠ n)"
have "i<k" "snd (r k) ≠ n"
by (metis (lifting, mono_tags) LeastI_ex A k_def leD less_linear snd_conv)+
from Least_le[where P="λk. i<k ∧ snd (r k) ≠ n", folded k_def]
have LEK_EQN: "∀k'. i≤k' ∧ k'<k ⟶ snd (r k') = n"
using ‹r i = (q,n)›
by clarsimp (metis le_neq_implies_less not_le snd_conv)
hence SND_RKMO: "snd (r (k - 1)) = n" using ‹i<k› by auto
moreover from R have "(r (k - 1), r k) ∈ degen.E T m"
unfolding degen.is_run_def ipath_def using ‹i<k›
by clarsimp (metis Suc_pred gr_implies_not0 neq0_conv)
moreover note ‹snd (r k) ≠ n›
ultimately have "n ∈ acc (fst (r (k - 1)))"
by (auto simp: degeneralize_ext_def split: if_split_asm)
moreover have "k - 1 < j" using A LEK_EQN
apply (rule_tac ccontr)
apply clarsimp
by (metis One_nat_def ‹snd (r (k - 1)) = n› less_Suc_eq
less_imp_diff_less not_less_eq snd_conv)
ultimately show thesis
apply -
apply (rule that[of "k - 1" "fst (r (k - 1))"])
using ‹i<k› SND_RKMO by auto
qed
lemma degen_run_find_acc_aux:
assumes NN0[simp]: "num_acc ≠ 0"
assumes AR: "degen.is_acc_run T m r"
assumes A: "r i = (q,0)" "0 ∈ acc q" "n<num_acc"
shows "∃j qj. i≤j ∧ r j = (qj,n) ∧ n ∈ acc qj"
proof -
from AR have R: "degen.is_run T m r"
and ACC: "∃⇩∞i. r i ∈ degen.F T m"
unfolding degen.is_acc_run_def degen.is_acc_def by auto
from ACC have ACC': "∀i. ∃j>i. r j ∈ degen.F T m"
by (auto simp: INFM_nat)
show ?thesis using ‹n<num_acc›
proof (induction n)
case 0 thus ?case using A by auto
next
case (Suc n)
then obtain j qj where "i≤j" "r j = (qj,n)" "n∈acc qj" by auto
moreover from R have "(r j, r (Suc j)) ∈ degen.E T m"
unfolding degen.is_run_def ipath_def
by auto
ultimately obtain qsj where RSJ: "r (Suc j) = (qsj,Suc n)"
unfolding degeneralize_ext_def using ‹Suc n<num_acc› by auto
from ACC' obtain k q0 where "Suc j ≤ k" "r k = (q0, 0)"
unfolding degeneralize_ext_def apply auto
by (metis less_imp_le_nat)
from degen_run_find_change[OF NN0 R ‹Suc j ≤ k› RSJ ‹r k = (q0, 0)›]
obtain l ql where
"Suc j ≤ l" "l < k" "r l = (ql, Suc n)" "Suc n ∈ acc ql"
by blast
thus ?case using ‹i ≤ j›
by (intro exI[where x=l] exI[where x=ql]) auto
qed
qed
lemma degen_acc_run_sound:
assumes A: "degen.is_acc_run T m r"
shows "is_acc_run (fst o r)"
proof -
from A have R: "degen.is_run T m r"
and ACC: "∃⇩∞i. r i ∈ degen.F T m"
unfolding degen.is_acc_run_def degen.is_acc_def by auto
from degen_is_run_sound[OF R] have R': "is_run (fst o r)" .
show ?thesis
proof (cases "num_acc = 0")
case NN0[simp]: False
from ACC have ACC': "∀i. ∃j>i. r j ∈ degen.F T m"
by (auto simp: INFM_nat)
have "∀n<num_acc. ∀i. ∃j>i. n ∈ acc (fst (r j))"
proof (intro allI impI)
fix n i
obtain j qj where "j>i" and RJ: "r j = (qj,0)" and ACCJ: "0 ∈ acc (qj)"
using ACC' unfolding degeneralize_ext_def by fastforce
assume NLESS: "n<num_acc"
show "∃j>i. n ∈ acc (fst (r j))"
proof (cases n)
case 0 thus ?thesis using ‹j>i› RJ ACCJ by auto
next
case [simp]: (Suc n')
from degen_run_find_acc_aux[OF NN0 A RJ ACCJ NLESS] obtain k qk where
"j≤k" "r k = (qk,n)" "n ∈ acc qk" by auto
thus ?thesis
by (metis ‹i < j› dual_order.strict_trans1 fst_conv)
qed
qed
hence "∀n<num_acc. ∃⇩∞i. n ∈ acc (fst (r i))"
by (auto simp: INFM_nat)
with R' show ?thesis
unfolding is_acc_run_def is_acc_def by auto
next
case [simp]: True
with R' show ?thesis
unfolding is_acc_run_def is_acc_def
by auto
qed
qed
lemma degen_acc_run_iff:
"is_acc_run r ⟷ (∃r'. fst o r' = r ∧ degen.is_acc_run T m r')"
using degen_acc_run_complete degen_acc_run_sound
by blast
end
subsection "System Automata"
text ‹
System automata are (finite) rooted graphs with a labeling function. They are
used to describe the model (system) to be checked.
›
record ('Q,'L) sa_rec = "'Q graph_rec" +
sa_L :: "'Q ⇒ 'L"
locale sa =
g?: graph G
for G :: "('Q, 'L, 'more) sa_rec_scheme"
begin
abbreviation L where "L ≡ sa_L G"
definition "accept w ≡ ∃r. is_run r ∧ w = L o r"
lemma acceptI[intro?]: "⟦is_run r; w = L o r⟧ ⟹ accept w" by (auto simp: accept_def)
definition "lang ≡ Collect accept"
lemma langI[intro?]: "accept w ⟹ w∈lang" by (auto simp: lang_def)
end
subsubsection "Product Construction"
text ‹
In this section we formalize the product construction between a GBA and a system
automaton. The result is a GBG and a projection function, such that projected
runs of the GBG correspond to words accepted by the GBA and the system.
›
locale igba_sys_prod_precond = igba: igba G + sa: sa S for
G :: "('q,'l,'moreG) igba_rec_scheme"
and S :: "('s,'l,'moreS) sa_rec_scheme"
begin
definition "prod ≡ ⦇
g_V = igba.V × sa.V,
g_E = { ((q,s),(q',s')).
igba.L q (sa.L s) ∧ (q,q') ∈ igba.E ∧ (s,s') ∈ sa.E },
g_V0 = igba.V0 × sa.V0,
igbg_num_acc = igba.num_acc,
igbg_acc = (λ(q,s). if s∈sa.V then igba.acc q else {} ) ⦈"
lemma prod_invar: "igb_graph prod"
apply unfold_locales
using igba.V0_ss sa.V0_ss
apply (auto simp: prod_def) []
using igba.E_ss sa.E_ss
apply (auto simp: prod_def) []
using igba.acc_bound
apply (auto simp: prod_def split: if_split_asm) []
using igba.acc_ss
apply (fastforce simp: prod_def split: if_split_asm) []
done
sublocale prod: igb_graph prod using prod_invar .
lemma prod_finite_reachable:
assumes "finite (igba.E⇧* `` igba.V0)" "finite (sa.E⇧* `` sa.V0)"
shows "finite ((g_E prod)⇧* `` g_V0 prod)"
proof -
{
fix q s q' s'
assume "((q,s),(q',s')) ∈ (g_E prod)⇧*"
hence "(q,q') ∈ (igba.E)⇧* ∧ (s,s') ∈ (sa.E)⇧*"
apply (induction rule: rtrancl_induct2)
apply (auto simp: prod_def)
done
} note gsp_reach=this
have [simp]: "⋀q s. (q,s) ∈ g_V0 prod ⟷ q ∈ igba.V0 ∧ s ∈ sa.V0"
by (auto simp: prod_def)
have reachSS:
"((g_E prod)⇧* `` g_V0 prod)
⊆ ((igba.E)⇧* `` igba.V0) × (sa.E⇧* `` sa.V0)"
by (auto dest: gsp_reach)
show ?thesis
apply (rule finite_subset[OF reachSS])
using assms
by simp
qed
lemma prod_fields:
"prod.V = igba.V × sa.V"
"prod.E = { ((q,s),(q',s')).
igba.L q (sa.L s) ∧ (q,q') ∈ igba.E ∧ (s,s') ∈ sa.E }"
"prod.V0 = igba.V0 × sa.V0"
"prod.num_acc = igba.num_acc"
"prod.acc = (λ(q,s). if s∈sa.V then igba.acc q else {} )"
unfolding prod_def
apply simp_all
done
lemma prod_run: "prod.is_run r ⟷
igba.is_run (fst o r)
∧ sa.is_run (snd o r)
∧ (∀i. igba.L (fst (r i)) (sa.L (snd (r i))))" (is "?L=?R")
apply rule
unfolding igba.is_run_def sa.is_run_def prod.is_run_def
unfolding prod_def ipath_def
apply (auto split: prod.split_asm intro: in_prod_fst_sndI)
apply (metis surjective_pairing)
apply (metis surjective_pairing)
apply (metis fst_conv snd_conv)
apply (metis fst_conv snd_conv)
apply (metis fst_conv snd_conv)
done
lemma prod_acc:
assumes A: "range (snd o r) ⊆ sa.V"
shows "prod.is_acc r ⟷ igba.is_acc (fst o r)"
proof -
{
fix i
from A have "prod.acc (r i) = igba.acc (fst (r i))"
unfolding prod_fields
apply safe
apply (clarsimp_all split: if_split_asm)
by (metis UNIV_I comp_apply imageI snd_conv subsetD)
} note [simp] = this
show ?thesis
unfolding prod.is_acc_def igba.is_acc_def
by (simp add: prod_fields(4))
qed
lemma gsp_correct1:
assumes A: "prod.is_acc_run r"
shows "sa.is_run (snd o r) ∧ (sa.L o snd o r ∈ igba.lang)"
proof -
from A have PR: "prod.is_run r" and PA: "prod.is_acc r"
unfolding prod.is_acc_run_def by auto
have PRR: "range r ⊆ prod.V" using prod.run_reachable prod.reachable_V PR by auto
have RSR: "range (snd o r) ⊆ sa.V" using PRR unfolding prod_fields by auto
show ?thesis
using PR PA
unfolding igba.is_acc_run_def
igba.lang_def igba.accept_def[abs_def]
apply (auto simp: prod_run prod_acc[OF RSR])
done
qed
lemma gsp_correct2:
assumes A: "sa.is_run r" "sa.L o r ∈ igba.lang"
shows "∃r'. r = snd o r' ∧ prod.is_acc_run r'"
proof -
have [simp]: "⋀r r'. fst o (λi. (r i, r' i)) = r"
"⋀r r'. snd o (λi. (r i, r' i)) = r'"
by auto
from A show ?thesis
unfolding prod.is_acc_run_def
igba.lang_def igba.accept_def[abs_def] igba.is_acc_run_def
apply (clarsimp simp: prod_run)
apply (rename_tac ra)
apply (rule_tac x="λi. (ra i, r i)" in exI)
apply clarsimp
apply (subst prod_acc)
using order_trans[OF sa.run_reachable sa.reachable_V]
apply auto []
apply auto []
done
qed
end
end