# Theory Digraph_Basic

section ‹Relations interpreted as Directed Graphs›
theory Digraph_Basic
imports
"Automatic_Refinement.Misc"
"Automatic_Refinement.Refine_Util"
"HOL-Library.Omega_Words_Fun"
begin

text ‹
This theory contains some basic graph theory on directed graphs which are
modeled as a relation between nodes.

The theory here is very fundamental, and
also used by non-directly graph-related applications like the theory of
tail-recursion in the Refinement Framework. Thus, we decided to put it
in the basic theories of the refinement framework.
›

text ‹Directed graphs are modeled as a relation on nodes›
type_synonym 'v digraph = "('v×'v) set"

locale digraph = fixes E :: "'v digraph"

subsection ‹Paths›
text ‹Path are modeled as list of nodes, the last node of a path is not included
into the list. This formalization allows for nice concatenation and splitting
of paths.›
inductive path :: "'v digraph ⇒ 'v ⇒ 'v list ⇒ 'v ⇒ bool" for E where
path0: "path E u [] u"
| path_prepend: "⟦ (u,v)∈E; path E v l w ⟧ ⟹ path E u (u#l) w"

lemma path1: "(u,v)∈E ⟹ path E u [u] v"
by (auto intro: path.intros)

lemma path_empty_conv[simp]:
"path E u [] v ⟷ u=v"
by (auto intro: path0 elim: path.cases)

inductive_cases path_uncons: "path E u (u'#l) w"
inductive_simps path_cons_conv: "path E u (u'#l) w"

lemma path_no_edges[simp]: "path {} u p v ⟷ (u=v ∧ p=[])"
by (cases p) (auto simp: path_cons_conv)

lemma path_conc:
assumes P1: "path E u la v"
assumes P2: "path E v lb w"
shows "path E u (la@lb) w"
using P1 P2 apply induct
by (auto intro: path.intros)

lemma path_append:
"⟦ path E u l v; (v,w)∈E ⟧ ⟹ path E u (l@[v]) w"
using path_conc[OF _ path1] .

lemma path_unconc:
assumes "path E u (la@lb) w"
obtains v where "path E u la v" and "path E v lb w"
using assms
thm path.induct
apply (induct u "la@lb" w arbitrary: la lb rule: path.induct)
apply (auto intro: path.intros elim!: list_Cons_eq_append_cases)
done

lemma path_conc_conv:
"path E u (la@lb) w ⟷ (∃v. path E u la v ∧ path E v lb w)"
by (auto intro: path_conc elim: path_unconc)

lemma (in -) path_append_conv: "path E u (p@[v]) w ⟷ (path E u p v ∧ (v,w)∈E)"

lemmas path_simps = path_empty_conv path_cons_conv path_conc_conv

lemmas path_trans[trans] = path_prepend path_conc path_append
lemma path_from_edges: "⟦(u,v)∈E; (v,w)∈E⟧ ⟹ path E u [u] v"
by (auto simp: path_simps)

lemma path_edge_cases[case_names no_use split]:
assumes "path (insert (u,v) E) w p x"
obtains
"path E w p x"
| p1 p2 where "path E w p1 u" "path (insert (u,v) E) v p2 x"
using assms
apply induction
apply simp
apply (clarsimp)
apply (metis path_simps path_cons_conv)
done

lemma path_edge_rev_cases[case_names no_use split]:
assumes "path (insert (u,v) E) w p x"
obtains
"path E w p x"
| p1 p2 where "path (insert (u,v) E) w p1 u" "path E v p2 x"
using assms
apply (induction p arbitrary: x rule: rev_induct)
apply simp
apply (clarsimp simp: path_cons_conv path_conc_conv)
apply (metis path_simps path_append_conv)
done

lemma path_mono:
assumes S: "E⊆E'"
assumes P: "path E u p v"
shows "path E' u p v"
using P
apply induction
apply simp
using S
apply (auto simp: path_cons_conv)
done

lemma path_is_rtrancl:
assumes "path E u l v"
shows "(u,v)∈E⇧*"
using assms
by induct auto

lemma rtrancl_is_path:
assumes "(u,v)∈E⇧*"
obtains l where "path E u l v"
using assms
by induct (auto intro: path0 path_append)

lemma path_is_trancl:
assumes "path E u l v"
and "l≠[]"
shows "(u,v)∈E⇧+"
using assms
apply induct
apply auto []
apply (case_tac l)
apply auto
done

lemma trancl_is_path:
assumes "(u,v)∈E⇧+"
obtains l where "l≠[]" and "path E u l v"
using assms
by induct (auto intro: path0 path_append)

lemma path_nth_conv: "path E u p v ⟷ (let p'=p@[v] in
u=p'!0 ∧
(∀i<length p' - 1. (p'!i,p'!Suc i)∈E))"
apply (induct p arbitrary: v rule: rev_induct)
apply (auto simp: path_conc_conv path_cons_conv nth_append)
done

lemma path_mapI:
assumes "path E u p v"
shows "path (pairself f  E) (f u) (map f p) (f v)"
using assms
apply induction
apply (simp)
apply (force simp: path_cons_conv)
done

lemma path_restrict:
assumes "path E u p v"
shows "path (E ∩ set p × insert v (set (tl p))) u p v"
using assms
proof induction
print_cases
case (path_prepend u v p w)
from path_prepend.IH have "path (E ∩ set (u#p) × insert w (set p)) v p w"
apply (rule path_mono[rotated])
by (cases p) auto
thus ?case using ‹(u,v)∈E›
by (cases p) (auto simp add: path_cons_conv)
qed auto

lemma path_restrict_closed:
assumes CLOSED: "ED ⊆ D"
assumes I: "v∈D" and P: "path E v p v'"
shows "path (E∩D×D) v p v'"
using P CLOSED I
by induction (auto simp: path_cons_conv)

lemma path_set_induct:
assumes "path E u p v" and "u∈I" and "EI ⊆ I"
shows "set p ⊆ I"
using assms
by (induction rule: path.induct) auto

lemma path_nodes_reachable: "path E u p v ⟹ insert v (set p) ⊆ E⇧*{u}"
apply (auto simp: in_set_conv_decomp path_cons_conv path_conc_conv)
apply (auto dest!: path_is_rtrancl)
done

lemma path_nodes_edges: "path E u p v ⟹ set p ⊆ fstE"
by (induction rule: path.induct) auto

lemma path_tl_nodes_edges:
assumes "path E u p v"
shows "set (tl p) ⊆ fstE ∩ sndE"
proof -
from path_nodes_edges[OF assms] have "set (tl p) ⊆ fstE"
by (cases p) auto

moreover have "set (tl p) ⊆ sndE"
using assms
apply (cases)
apply simp
apply simp
apply (erule path_set_induct[where I = "sndE"])
apply auto
done
ultimately show ?thesis
by auto
qed

lemma path_loop_shift:
assumes P: "path E u p u"
assumes S: "v∈set p"
obtains p' where "set p' = set p" "path E v p' v"
proof -
from S obtain p1 p2 where [simp]: "p = p1@v#p2" by (auto simp: in_set_conv_decomp)
from P obtain v' where A: "path E u p1 v" "(v, v') ∈ E" "path E v' p2 u"
by (auto simp: path_simps)
hence "path E v (v#p2@p1) v" by (auto simp: path_simps)
thus ?thesis using that[of "v#p2@p1"] by auto
qed

lemma path_hd:
assumes "p ≠ []" "path E v p w"
shows "hd p = v"
using assms
by (auto simp: path_cons_conv neq_Nil_conv)

lemma path_last_is_edge:
assumes "path E x p y"
and "p ≠ []"
shows "(last p, y) ∈ E"
using assms
by (auto simp: neq_Nil_rev_conv path_simps)

lemma path_member_reach_end:
assumes P: "path E x p y"
and v: "v ∈ set p"
shows "(v,y) ∈ E⇧+"
using assms
by (auto intro!: path_is_trancl simp: in_set_conv_decomp path_simps)

lemma path_tl_induct[consumes 2, case_names single step]:
assumes P: "path E x p y"
and NE: "x ≠ y"
and S: "⋀u. (x,u) ∈ E ⟹ P x u"
and ST: "⋀u v. ⟦(x,u) ∈ E⇧+; (u,v) ∈ E; P x u⟧ ⟹ P x v"
shows "P x y ∧ (∀ v ∈ set (tl p). P x v)"
proof -
from P NE have "p ≠ []" by auto
thus ?thesis using P
proof (induction p arbitrary: y rule: rev_nonempty_induct)
case (single u) hence "(x,y) ∈ E" by (simp add: path_cons_conv)
with S show ?case by simp
next
case (snoc u us) hence "path E x us u" by (simp add: path_append_conv)
with snoc path_is_trancl have
"P x u" "(x,u) ∈ E⇧+" "∀v ∈ set (tl us). P x v"
by simp_all
moreover with snoc have "∀v ∈ set (tl (us@[u])). P x v" by simp
moreover from snoc have "(u,y) ∈ E" by (simp add: path_append_conv)
ultimately show ?case by (auto intro: ST)
qed
qed

lemma path_restrict_tl:
"⟦ u∉R; path (E ∩ UNIV × -R) u p v ⟧ ⟹ path (rel_restrict E R) u p v"
apply (induction p arbitrary: u)
apply (auto simp: path_simps rel_restrict_def)
done

lemma path1_restr_conv: "path (E∩UNIV × -R) u (x#xs) v
⟷ (∃w. w∉R ∧ x=u ∧ (u,w)∈E ∧ path (rel_restrict E R) w xs v)"
proof -
have 1: "rel_restrict E R ⊆ E ∩ UNIV × - R" by (auto simp: rel_restrict_def)

show ?thesis
by (auto simp: path_simps intro: path_restrict_tl path_mono[OF 1])
qed

lemma dropWhileNot_path:
assumes "p ≠ []"
and "path E w p x"
and "v ∈ set p"
and "dropWhile ((≠) v) p = c"
shows "path E v c x"
using assms
proof (induction arbitrary: w c rule: list_nonempty_induct)
case (single p) thus ?case by (auto simp add: path_simps)
next
case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
show ?case
proof (cases "p=v")
case True with cons show ?thesis by simp
next
case False with cons have "c = dropWhile ((≠) v) ps" by simp
moreover from cons.prems obtain y where "path E y ps x"
using path_uncons by metis
moreover from cons.prems False have "v ∈ set ps" by simp
ultimately show ?thesis using cons.IH by metis
qed
qed

lemma takeWhileNot_path:
assumes "p ≠ []"
and "path E w p x"
and "v ∈ set p"
and "takeWhile ((≠) v) p = c"
shows "path E w c v"
using assms
proof (induction arbitrary: w c rule: list_nonempty_induct)
case (single p) thus ?case by (auto simp add: path_simps)
next
case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
show ?case
proof (cases "p=v")
case True with cons show ?thesis by simp
next
case False with cons obtain c' where
"c' = takeWhile ((≠) v) ps" and
[simp]: "c = p#c'"
by simp_all
moreover from cons.prems obtain y where
"path E y ps x" and "(w,y) ∈ E"
using path_uncons by metis+
moreover from cons.prems False have "v ∈ set ps" by simp
ultimately have "path E y c' v" using cons.IH by metis
with ‹(w,y) ∈ E› show ?thesis by (auto simp add: path_cons_conv)
qed
qed

subsection ‹Infinite Paths›
definition ipath :: "'q digraph ⇒ 'q word ⇒ bool"
― ‹Predicate for an infinite path in a digraph›
where "ipath E r ≡ ∀i. (r i, r (Suc i))∈E"

lemma ipath_conc_conv:
"ipath E (u ⌢ v) ⟷ (∃a. path E a u (v 0) ∧ ipath E v)"
apply (auto simp: conc_def ipath_def path_nth_conv nth_append)
by (metis Suc_diff_Suc diff_Suc_Suc not_less_eq)

lemma ipath_iter_conv:
assumes "p≠[]"
shows "ipath E (p⇧ω) ⟷ (path E (hd p) p (hd p))"
proof (cases p)
case Nil thus ?thesis using assms by simp
next
case (Cons u p') hence PLEN: "length p > 0" by simp
show ?thesis proof
assume "ipath E (iter (p))"
hence "∀i. (iter (p) i, iter (p) (Suc i)) ∈ E"
unfolding ipath_def by simp
hence "(∀i<length p. (p!i,(p@[hd p])!Suc i)∈E)"
apply safe
apply (drule_tac x=i in spec)
apply simp
apply (case_tac "Suc i = length p")
done
thus "path E (hd p) p (hd p)"
by (auto simp: path_nth_conv Cons nth_append nth_Cons')
next
assume "path E (hd p) p (hd p)"
thus "ipath E (iter p)"
apply (auto simp: path_nth_conv ipath_def assms Let_def)
apply (drule_tac x="i mod length p" in spec)
apply (auto simp: nth_append assms split: if_split_asm)
apply (metis less_not_refl mod_Suc)
by (metis PLEN diff_self_eq_0 mod_Suc nth_Cons_0 mod_less_divisor)
qed
qed

lemma ipath_to_rtrancl:
assumes R: "ipath E r"
assumes I: "i1≤i2"
shows "(r i1,r i2)∈E⇧*"
using I
proof (induction i2)
case (Suc i2)
show ?case proof (cases "i1=Suc i2")
assume "i1≠Suc i2"
with Suc have "(r i1,r i2)∈E⇧*" by auto
also from R have "(r i2,r (Suc i2))∈E" unfolding ipath_def by auto
finally show ?thesis .
qed simp
qed simp

lemma ipath_to_trancl:
assumes R: "ipath E r"
assumes I: "i1<i2"
shows "(r i1,r i2)∈E⇧+"
proof -
from R have "(r i1,r (Suc i1))∈E"
by (auto simp: ipath_def)
also have "(r (Suc i1),r i2)∈E⇧*"
using ipath_to_rtrancl[OF R,of "Suc i1" i2] I by auto
finally (rtrancl_into_trancl2) show ?thesis .
qed

lemma run_limit_two_connectedI:
assumes A: "ipath E r"
assumes B: "a ∈ limit r" "b∈limit r"
shows "(a,b)∈E⇧+"
proof -
from B have "{a,b} ⊆ limit r" by simp
with A show ?thesis
by (metis ipath_to_trancl two_in_limit_iff)
qed

lemma ipath_subpath:
assumes P: "ipath E r"
assumes LE: "l≤u"
shows "path E (r l) (map r [l..<u]) (r u)"
using LE
proof (induction "u-l" arbitrary: u l)
case (Suc n)
note IH=Suc.hyps(1)
from ‹Suc n = u-l› ‹l≤u› obtain u' where [simp]: "u=Suc u'"
and A: "n=u'-l" "l ≤ u'"
by (cases u) auto

note IH[OF A]
also from P have "(r u',r u)∈E"
by (auto simp: ipath_def)
finally show ?case using ‹l ≤ u'› by (simp add: upt_Suc_append)
qed auto

lemma ipath_restrict_eq: "ipath (E ∩ (E⇧*{r 0} × E⇧*{r 0})) r ⟷ ipath E r"
unfolding ipath_def
by (auto simp: relpow_fun_conv rtrancl_power)
lemma ipath_restrict: "ipath E r ⟹ ipath (E ∩ (E⇧*{r 0} × E⇧*{r 0})) r"

lemma ipathI[intro?]: "⟦⋀i. (r i, r (Suc i)) ∈ E⟧ ⟹ ipath E r"
unfolding ipath_def by auto

lemma ipathD: "ipath E r ⟹ (r i, r (Suc i)) ∈ E"
unfolding ipath_def by auto

lemma ipath_in_Domain: "ipath E r ⟹ r i ∈ Domain E"
unfolding ipath_def by auto

lemma ipath_in_Range: "⟦ipath E r; i≠0⟧ ⟹ r i ∈ Range E"
unfolding ipath_def by (cases i) auto

lemma ipath_suffix: "ipath E r ⟹ ipath E (suffix i r)"
unfolding suffix_def ipath_def by auto

subsection ‹Strongly Connected Components›

text ‹A strongly connected component is a maximal mutually connected set
of nodes›
definition is_scc :: "'q digraph ⇒ 'q set ⇒ bool"
where "is_scc E U ⟷ U×U⊆E⇧* ∧ (∀V. V⊃U ⟶ ¬ (V×V⊆E⇧*))"

lemma scc_non_empty[simp]: "¬is_scc E {}" unfolding is_scc_def by auto

lemma scc_non_empty'[simp]: "is_scc E U ⟹ U≠{}" unfolding is_scc_def by auto

lemma is_scc_closed:
assumes SCC: "is_scc E U"
assumes MEM: "x∈U"
assumes P: "(x,y)∈E⇧*" "(y,x)∈E⇧*"
shows "y∈U"
proof -
from SCC MEM P have "insert y U × insert y U ⊆ E⇧*"
unfolding is_scc_def
apply clarsimp
apply rule
apply clarsimp_all
apply (erule disjE1)
apply clarsimp
apply (metis in_mono mem_Sigma_iff rtrancl_trans)
apply auto []
apply (erule disjE1)
apply clarsimp
apply (metis in_mono mem_Sigma_iff rtrancl_trans)
apply auto []
done
with SCC show ?thesis unfolding is_scc_def by blast
qed

lemma is_scc_connected:
assumes SCC: "is_scc E U"
assumes MEM: "x∈U" "y∈U"
shows "(x,y)∈E⇧*"
using assms unfolding is_scc_def by auto

text ‹In the following, we play around with alternative characterizations, and
prove them all equivalent .›

text ‹A common characterization is to define an equivalence relation
,,mutually connected'' on nodes, and characterize the SCCs as its
equivalence classes:›

definition mconn :: "('a×'a) set ⇒ ('a × 'a) set"
― ‹Mutually connected relation on nodes›
where "mconn E = E⇧* ∩ (E¯)⇧*"

lemma mconn_pointwise:
"mconn E = {(u,v). (u,v)∈E⇧* ∧ (v,u)∈E⇧*}"
by (auto simp add: mconn_def rtrancl_converse)

text ‹‹mconn› is an equivalence relation:›
lemma mconn_refl[simp]: "Id⊆mconn E"

lemma mconn_sym: "mconn E = (mconn E)¯"

lemma mconn_trans: "mconn E O mconn E = mconn E"

lemma mconn_refl': "refl (mconn E)"
by (auto intro: refl_onI simp: mconn_pointwise)

lemma mconn_sym': "sym (mconn E)"
by (auto intro: symI simp: mconn_pointwise)

lemma mconn_trans': "trans (mconn E)"
by (metis mconn_def trans_Int trans_rtrancl)

lemma mconn_equiv: "equiv UNIV (mconn E)"
using mconn_refl' mconn_sym' mconn_trans'
by (rule equivI)

lemma is_scc_mconn_eqclasses: "is_scc E U ⟷ U ∈ UNIV // mconn E"
― ‹The strongly connected components are the equivalence classes of the
mutually-connected relation on nodes›
proof
assume A: "is_scc E U"
then obtain x where "x∈U" unfolding is_scc_def by auto
hence "U = mconn E  {x}" using A
unfolding mconn_pointwise is_scc_def
apply clarsimp
apply rule
apply auto []
apply clarsimp
by (metis A is_scc_closed)
thus "U ∈ UNIV // mconn E"
by (auto simp: quotient_def)
next
assume "U ∈ UNIV // mconn E"
thus "is_scc E U"
by (auto simp: is_scc_def mconn_pointwise quotient_def)
qed

(* For presentation in the paper *)
lemma "is_scc E U ⟷ U ∈ UNIV // (E⇧* ∩ (E¯)⇧*)"
unfolding is_scc_mconn_eqclasses mconn_def by simp

text ‹We can also restrict the notion of "reachability" to nodes
inside the SCC
›

lemma find_outside_node:
assumes "(u,v)∈E⇧*"
assumes "(u,v)∉(E∩U×U)⇧*"
assumes "u∈U" "v∈U"
shows "∃u'. u'∉U ∧ (u,u')∈E⇧* ∧ (u',v)∈E⇧*"
using assms
apply (induction)
apply auto []
apply clarsimp
by (metis IntI mem_Sigma_iff rtrancl.simps)

lemma is_scc_restrict1:
assumes SCC: "is_scc E U"
shows "U×U⊆(E∩U×U)⇧*"
using assms
unfolding is_scc_def
apply clarsimp
apply (rule ccontr)
apply (drule (2) find_outside_node[rotated])
apply auto []
by (metis is_scc_closed[OF SCC] mem_Sigma_iff rtrancl_trans subsetD)

lemma is_scc_restrict2:
assumes SCC: "is_scc E U"
assumes "V⊃U"
shows "¬ (V×V⊆(E∩V×V)⇧*)"
using assms
unfolding is_scc_def
apply clarsimp
using rtrancl_mono[of "E ∩ V × V" "E"]
apply clarsimp
apply blast
done

lemma is_scc_restrict3:
assumes SCC: "is_scc E U"
shows "((E⇧*((E⇧*U) - U)) ∩ U = {})"
apply auto
by (metis assms is_scc_closed is_scc_connected rtrancl_trans)

lemma is_scc_alt_restrict_path:
"is_scc E U ⟷ U≠{} ∧
(U×U ⊆ (E∩U×U)⇧*) ∧ ((E⇧*((E⇧*U) - U)) ∩ U = {})"
apply rule
apply (intro conjI)
apply simp
apply (blast dest: is_scc_restrict1)
apply (blast dest: is_scc_restrict3)

unfolding is_scc_def
apply rule
apply clarsimp
apply (metis (full_types) Int_lower1 in_mono mem_Sigma_iff rtrancl_mono_mp)
apply blast
done

lemma is_scc_pointwise:
"is_scc E U ⟷
U≠{}
∧ (∀u∈U. ∀v∈U. (u,v)∈(E∩U×U)⇧*)
∧ (∀u∈U. ∀v. (v∉U ∧ (u,v)∈E⇧*) ⟶ (∀u'∈U. (v,u')∉E⇧*))"
― ‹Alternative, pointwise characterization›
unfolding is_scc_alt_restrict_path
by blast

lemma is_scc_unique:
assumes SCC: "is_scc E scc" "is_scc E scc'"
and v: "v ∈ scc" "v ∈ scc'"
shows "scc = scc'"
proof -
from SCC have "scc = scc' ∨ scc ∩ scc' = {}"
using quotient_disj[OF mconn_equiv]
with v show ?thesis by auto
qed

lemma is_scc_ex1:
"∃!scc. is_scc E scc ∧ v ∈ scc"
proof (rule ex1I, rule conjI)
let ?scc = "mconn E  {v}"
have "?scc ∈ UNIV // mconn E" by (auto intro: quotientI)
thus "is_scc E ?scc" by (simp add: is_scc_mconn_eqclasses)
moreover show "v ∈ ?scc" by (blast intro: refl_onD[OF mconn_refl'])
ultimately show "⋀scc. is_scc E scc ∧ v ∈ scc ⟹ scc = ?scc"
by (metis is_scc_unique)
qed

lemma is_scc_ex:
"∃scc. is_scc E scc ∧ v ∈ scc"
by (metis is_scc_ex1)

lemma is_scc_connected':
"⟦is_scc E scc; x ∈ scc; y ∈ scc⟧ ⟹ (x,y)∈(Restr E scc)⇧*"
unfolding is_scc_pointwise
by blast

definition scc_of :: "('v×'v) set ⇒ 'v ⇒ 'v set"
where
"scc_of E v = (THE scc. is_scc E scc ∧ v ∈ scc)"

lemma scc_of_is_scc[simp]:
"is_scc E (scc_of E v)"
using is_scc_ex1[of E v]
by (auto dest!: theI' simp: scc_of_def)

lemma node_in_scc_of_node[simp]:
"v ∈ scc_of E v"
using is_scc_ex1[of E v]
by (auto dest!: theI' simp: scc_of_def)

lemma scc_of_unique:
assumes "w ∈ scc_of E v"
shows "scc_of E v = scc_of E w"
proof -
have "is_scc E (scc_of E v)" by simp
moreover note assms
moreover have "is_scc E (scc_of E w)" by simp
moreover have "w ∈ scc_of E w" by simp
ultimately show ?thesis using is_scc_unique by metis
qed

end


# Theory Digraph

section ‹Directed Graphs›
(* Author: Peter Lammich *)
theory Digraph
imports
CAVA_Base.CAVA_Base
Digraph_Basic
begin

subsection "Directed Graphs with Explicit Node Set and Set of Initial Nodes"

record 'v graph_rec =
g_V :: "'v set"
g_E :: "'v digraph"
g_V0 :: "'v set"

definition graph_restrict :: "('v, 'more) graph_rec_scheme ⇒ 'v set ⇒ ('v, 'more) graph_rec_scheme"
where "graph_restrict G R ≡
⦇
g_V = g_V G,
g_E = rel_restrict (g_E G) R,
g_V0 = g_V0 G - R,
… = graph_rec.more G
⦈"

lemma graph_restrict_simps[simp]:
"g_V (graph_restrict G R) = g_V G"
"g_E (graph_restrict G R) = rel_restrict (g_E G) R"
"g_V0 (graph_restrict G R) = g_V0 G - R"
"graph_rec.more (graph_restrict G R) = graph_rec.more G"
unfolding graph_restrict_def by auto

lemma graph_restrict_trivial[simp]: "graph_restrict G {} = G" by simp

locale graph_defs =
fixes G :: "('v, 'more) graph_rec_scheme"
begin

abbreviation "V ≡ g_V G"
abbreviation "E ≡ g_E G"
abbreviation "V0 ≡ g_V0 G"

abbreviation "reachable ≡ E⇧*  V0"
abbreviation "succ v ≡ E  {v}"

lemma finite_V0: "finite reachable ⟹ finite V0" by (auto intro: finite_subset)

definition is_run
― ‹Infinite run, i.e., a rooted infinite path›
where "is_run r ≡ r 0 ∈ V0 ∧ ipath E r"

lemma run_ipath: "is_run r ⟹ ipath E r" unfolding is_run_def by auto
lemma run_V0: "is_run r ⟹ r 0 ∈ V0" unfolding is_run_def by auto

lemma run_reachable: "is_run r ⟹ range r ⊆ reachable"
unfolding is_run_def using ipath_to_rtrancl by blast

end

locale graph =
graph_defs G
for G :: "('v, 'more) graph_rec_scheme"
+
assumes V0_ss: "V0 ⊆ V"
assumes E_ss: "E ⊆ V × V"
begin

lemma reachable_V: "reachable ⊆ V" using V0_ss E_ss by (auto elim: rtrancl_induct)

lemma finite_E: "finite V ⟹ finite E" using finite_subset E_ss by auto

end

(* TODO: finite reachability is handled using loose assumptions, while finitely branching
graphs are captured using a locale. it may be advantageous to unify this. *)
locale fb_graph =
graph G
for G :: "('v, 'more) graph_rec_scheme"
+
assumes finite_V0[simp, intro!]: "finite V0"
assumes finitely_branching[simp, intro]: "v ∈ reachable ⟹ finite (succ v)"
begin

lemma fb_graph_subset:
assumes "g_V G' = V"
assumes "g_E G' ⊆ E"
assumes "finite (g_V0 G')"
assumes "g_V0 G' ⊆ reachable"
shows "fb_graph G'"
proof
show "g_V0 G' ⊆ g_V G'" using reachable_V assms(1, 4) by simp
show "g_E G' ⊆ g_V G' × g_V G'" using E_ss assms(1, 2) by simp
show "finite (g_V0 G')" using assms(3) by this
next
fix v
assume 1: "v ∈ (g_E G')⇧*  g_V0 G'"
obtain u where 2: "u ∈ g_V0 G'" "(u, v) ∈ (g_E G')⇧*" using 1 by rule
have 3: "u ∈ reachable" "(u, v) ∈ E⇧*" using rtrancl_mono assms(2, 4) 2 by auto
have 4: "v ∈ reachable" using rtrancl_image_advance_rtrancl 3 by metis
have 5: "finite (E  {v})" using 4 by rule
have 6: "g_E G'  {v} ⊆ E  {v}" using assms(2) by auto
show "finite (g_E G'  {v})" using finite_subset 5 6 by auto
qed

lemma fb_graph_restrict: "fb_graph (graph_restrict G R)"
by (rule fb_graph_subset, auto simp: rel_restrict_sub)

end

lemma (in graph) fb_graphI_fr:
assumes "finite reachable"
shows "fb_graph G"
proof
from assms show "finite V0" by (rule finite_subset[rotated]) auto
fix v
assume "v ∈ reachable"
hence "succ v ⊆ reachable" by (metis Image_singleton_iff rtrancl_image_advance subsetI)
thus "finite (succ v)" using assms by (rule finite_subset)
qed

abbreviation "rename_E f E ≡ (λ(u,v). (f u, f v))E"

definition "fr_rename_ext ecnv f G ≡ ⦇
g_V = f(g_V G),
g_E = rename_E f (g_E G),
g_V0 = (fg_V0 G),
… = ecnv G
⦈"

locale g_rename_precond =
graph G
for G :: "('u,'more) graph_rec_scheme"
+
fixes f :: "'u ⇒ 'v"
fixes ecnv :: "('u, 'more) graph_rec_scheme ⇒ 'more'"
assumes INJ: "inj_on f V"
begin

abbreviation "G' ≡ fr_rename_ext ecnv f G"

lemma G'_fields:
"g_V G' = fV"
"g_V0 G' = fV0"
"g_E G' = rename_E f E"
unfolding fr_rename_ext_def by simp_all

definition "fi ≡ the_inv_into V f"

lemma
fi_f: "x∈V ⟹ fi (f x) = x" and
f_fi: "y∈fV ⟹ f (fi y) = y" and
fi_f_eq: "⟦f x = y; x∈V⟧ ⟹ fi y = x"
unfolding fi_def
by (auto
simp: the_inv_into_f_f f_the_inv_into_f the_inv_into_f_eq INJ)

lemma E'_to_E: "(u,v) ∈ g_E G' ⟹ (fi u, fi v)∈E"
using E_ss
by (auto simp: fi_f G'_fields)

lemma V0'_to_V0: "v∈g_V0 G' ⟹ fi v ∈ V0"
using V0_ss
by (auto simp: fi_f G'_fields)

lemma rtrancl_E'_sim:
assumes "(f u,v')∈(g_E G')⇧*"
assumes "u∈V"
shows "∃v. v' = f v ∧ v∈V ∧ (u,v)∈E⇧*"
using assms
proof (induction "f u" v' arbitrary: u)
case (rtrancl_into_rtrancl v' w' u)
then obtain v w where "v' = f v" "w' = f w" "(v,w)∈E"
by (auto simp: G'_fields)
hence "v∈V" "w∈V" using E_ss by auto
from rtrancl_into_rtrancl obtain vv where "v' = f vv" "vv∈V" "(u,vv)∈E⇧*"
by blast
from ‹v' = f v› ‹v∈V› ‹v' = f vv› ‹vv∈V› have [simp]: "vv = v"

note ‹(u,vv)∈E⇧*›[simplified]
also note ‹(v,w)∈E›
finally show ?case using ‹w' = f w› ‹w∈V› by blast
qed auto

lemma rtrancl_E'_to_E: assumes "(u,v)∈(g_E G')⇧*" shows "(fi u, fi v)∈E⇧*"
using assms apply induction
by (fastforce intro: E'_to_E rtrancl_into_rtrancl)+

lemma G'_invar: "graph G'"
apply unfold_locales
proof -
show "g_V0 G' ⊆ g_V G'"
using V0_ss by (auto simp: G'_fields) []

show "g_E G' ⊆ g_V G' × g_V G'"
using E_ss by (auto simp: G'_fields) []
qed

sublocale G': graph G' using G'_invar .

lemma G'_finite_reachable:
assumes "finite ((g_E G)⇧*  g_V0 G)"
shows "finite ((g_E G')⇧*  g_V0 G')"
proof -
have "(g_E G')⇧*  g_V0 G' ⊆ f  (E⇧*V0)"
apply (clarsimp_all simp: G'_fields(2))
apply (drule rtrancl_E'_sim)
using V0_ss apply auto []
apply auto
done
thus ?thesis using finite_subset assms by blast
qed

lemma V'_to_V: "v ∈ G'.V ⟹ fi v ∈ V"
by (auto simp: fi_f G'_fields)

lemma ipath_sim1: "ipath E r ⟹ ipath G'.E (f o r)"
unfolding ipath_def by (auto simp: G'_fields)

lemma ipath_sim2: "ipath G'.E r ⟹ ipath E (fi o r)"
unfolding ipath_def
apply (clarsimp simp: G'_fields)
apply (drule_tac x=i in spec)
using E_ss
by (auto simp: fi_f)

lemma run_sim1: "is_run r ⟹ G'.is_run (f o r)"
unfolding is_run_def G'.is_run_def
apply (intro conjI)
apply (auto simp: G'_fields) []
apply (auto simp: ipath_sim1)
done

lemma run_sim2: "G'.is_run r ⟹ is_run (fi o r)"
unfolding is_run_def G'.is_run_def
by (auto simp: ipath_sim2 V0'_to_V0)

end

end


# Theory Automata

section ‹Automata›
(* Author: Peter Lammich *)
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"

(* For presentation in paper *)
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)

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 = { fA | 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' = { fA | A. A∈F }"
unfolding gb_rename_ecnv_def fr_rename_ext_def
by simp

sublocale G': gb_graph G'
apply unfold_locales
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 ∈ fA"
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∈fg_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∈fV 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 ⊆ fV; 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 ⊆ fV"
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"

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
done

lemma to_gba_alt_lang:
"gba.lang T m = lang"
unfolding lang_def gba.lang_def
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"

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]

lemma is_acc_gbg:
"gbg.is_acc T m = is_acc"
apply (intro ext)
unfolding gbg.is_acc_def is_acc_def
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
done

lemma lang_gba_alt: "gba.lang T m = lang"
unfolding lang_def gba.lang_def
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
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"
(*and ACC: "limit r ∩ bg_F (degeneralize_ext ecnv) ≠ {}"*)
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
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


# Theory Lasso

section ‹Lassos›
(* Author: Peter Lammich *)
theory Lasso
imports Automata
begin

record 'v lasso =
lasso_reach :: "'v list"
lasso_va :: "'v"
lasso_cysfx :: "'v list"

definition "lasso_v0 L ≡ case lasso_reach L of [] ⇒ lasso_va L | (v0#_) ⇒ v0"
definition lasso_cycle where "lasso_cycle L = lasso_va L # lasso_cysfx L"

definition "lasso_of_prpl prpl ≡ case prpl of (pr,pl) ⇒ ⦇
lasso_reach = pr,
lasso_va = hd pl,
lasso_cysfx = tl pl ⦈"

definition "prpl_of_lasso L ≡ (lasso_reach L, lasso_va L # lasso_cysfx L)"

lemma prpl_of_lasso_simps[simp]:
"fst (prpl_of_lasso L) = lasso_reach L"
"snd (prpl_of_lasso L) = lasso_va L # lasso_cysfx L"
unfolding prpl_of_lasso_def by auto

lemma lasso_of_prpl_simps[simp]:
"lasso_reach (lasso_of_prpl prpl) = fst prpl"
"snd prpl ≠ [] ⟹ lasso_cycle (lasso_of_prpl prpl) = snd prpl"
unfolding lasso_of_prpl_def lasso_cycle_def by (auto split: prod.split)

definition run_of_lasso :: "'q lasso ⇒ 'q word"
― ‹Run described by a lasso›
where "run_of_lasso L ≡ lasso_reach L ⌢ (lasso_cycle L)⇧ω"

lemma run_of_lasso_of_prpl:
"pl ≠ [] ⟹ run_of_lasso (lasso_of_prpl (pr, pl)) = pr ⌢ pl⇧ω"
unfolding run_of_lasso_def lasso_of_prpl_def lasso_cycle_def
by auto

definition "map_lasso f L ≡ ⦇
lasso_reach = map f (lasso_reach L),
lasso_va = f (lasso_va L),
lasso_cysfx = map f (lasso_cysfx L)
⦈"

lemma map_lasso_simps[simp]:
"lasso_reach (map_lasso f L) = map f (lasso_reach L)"
"lasso_va (map_lasso f L) = f (lasso_va L)"
"lasso_cysfx (map_lasso f L) = map f (lasso_cysfx L)"
"lasso_v0 (map_lasso f L) = f (lasso_v0 L)"
"lasso_cycle (map_lasso f L) = map f (lasso_cycle L)"
unfolding map_lasso_def lasso_v0_def lasso_cycle_def
by (auto split: list.split)

lemma map_lasso_run[simp]:
shows "run_of_lasso (map_lasso f L) = f o (run_of_lasso L)"
by (auto simp add: map_lasso_def run_of_lasso_def conc_def iter_def
lasso_cycle_def lasso_v0_def fun_eq_iff not_less nth_Cons'
nz_le_conv_less)

context graph begin
definition is_lasso_pre :: "'v lasso ⇒ bool"
where "is_lasso_pre L ≡
lasso_v0 L ∈ V0
∧ path E (lasso_v0 L) (lasso_reach L) (lasso_va L)
∧ path E (lasso_va L) (lasso_cycle L) (lasso_va L)"

definition "is_lasso_prpl_pre prpl ≡ case prpl of (pr, pl) ⇒ ∃v0 va.
v0∈V0
∧ pl ≠ []
∧ path E v0 pr va
∧ path E va pl va"

lemma is_lasso_pre_prpl_of_lasso[simp]:
"is_lasso_prpl_pre (prpl_of_lasso L) ⟷ is_lasso_pre L"
unfolding is_lasso_pre_def prpl_of_lasso_def is_lasso_prpl_pre_def
unfolding lasso_v0_def lasso_cycle_def
by (auto simp: path_simps split: list.split)

lemma is_lasso_prpl_pre_conv:
"is_lasso_prpl_pre prpl
⟷ (snd prpl≠[] ∧ is_lasso_pre (lasso_of_prpl prpl))"
unfolding is_lasso_pre_def lasso_of_prpl_def is_lasso_prpl_pre_def
unfolding lasso_v0_def lasso_cycle_def
apply (cases prpl)
apply (rename_tac a b)
apply (case_tac b)
apply (auto simp: path_simps split: list.splits)
done

lemma is_lasso_pre_empty[simp]: "V0 = {} ⟹ ¬is_lasso_pre L"
unfolding is_lasso_pre_def by auto

lemma run_of_lasso_pre:
assumes "is_lasso_pre L"
shows "is_run (run_of_lasso L)"
and "run_of_lasso L 0 ∈ V0"
using assms
unfolding is_lasso_pre_def is_run_def run_of_lasso_def
lasso_cycle_def lasso_v0_def
by (auto simp: ipath_conc_conv ipath_iter_conv path_cons_conv conc_fst
split: list.splits)

end

context gb_graph begin
definition is_lasso
:: "'Q lasso ⇒ bool"
― ‹Predicate that defines a lasso›
where "is_lasso L ≡
is_lasso_pre L
∧ (∀A∈F. (set (lasso_cycle L)) ∩ A ≠ {})"

definition "is_lasso_prpl prpl ≡
is_lasso_prpl_pre prpl
∧ (∀A∈F. set (snd prpl) ∩ A ≠ {})"

lemma is_lasso_prpl_of_lasso[simp]:
"is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
unfolding is_lasso_def is_lasso_prpl_def
unfolding lasso_v0_def lasso_cycle_def
by auto

lemma is_lasso_prpl_conv:
"is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
apply safe
apply simp_all
done

lemma is_lasso_empty[simp]: "V0 = {} ⟹ ¬is_lasso L"
unfolding is_lasso_def by auto

lemma lasso_accepted:
assumes L: "is_lasso L"
shows "is_acc_run (run_of_lasso L)"
proof -
obtain "pr" va pls where
[simp]: "L = ⦇lasso_reach = pr,lasso_va = va,lasso_cysfx = pls⦈"
by (cases L)

from L have "is_run (run_of_lasso L)"
unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
moreover from L have "(∀A∈F. set (va#pls) ∩ A ≠ {})"
by (auto simp: is_lasso_def lasso_cycle_def)
moreover from L have "(run_of_lasso L) 0 ∈ V0"
unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
ultimately show "is_acc_run (run_of_lasso L)"
unfolding is_acc_run_def is_acc_def run_of_lasso_def
lasso_cycle_def lasso_v0_def
by (fastforce intro: limit_inter_INF)
qed

lemma lasso_prpl_acc_run:
"is_lasso_prpl (pr, pl) ⟹ is_acc_run (pr ⌢ iter pl)"
apply (clarsimp simp: is_lasso_prpl_conv)
apply (drule lasso_accepted)
done

end

context gb_graph
begin
lemma accepted_lasso:
assumes [simp, intro]: "finite (E⇧*  V0)"
assumes A: "is_acc_run r"
shows "∃L. is_lasso L"
proof -
from A have
RUN: "is_run r"
and ACC: "∀A∈F. limit r ∩ A ≠ {}"
by (auto simp: is_acc_run_limit_alt)
from RUN have [simp]: "r 0 ∈ V0" and RUN': "ipath E r"

txt ‹Choose a node that is visited infinitely often›
from RUN have RAN_REACH: "range r ⊆ E⇧*V0"
by (auto simp: is_run_def dest: ipath_to_rtrancl)
hence "finite (range r)" by (auto intro: finite_subset)
then obtain u where "u∈limit r" using limit_nonempty by blast
hence U_REACH: "u∈E⇧*V0" using RAN_REACH limit_in_range by force
then obtain v0 "pr" where PR: "v0∈V0" "path E v0 pr u"
by (auto intro: rtrancl_is_path)
moreover
txt ‹Build a path from ‹u› to ‹u›, that contains nodes from
each acceptance set›
have "∃pl. pl≠[] ∧ path E u pl u ∧ (∀A∈F. set pl ∩ A ≠ {})"
using finite_F ACC
proof (induction rule: finite_induct)
case empty
from run_limit_two_connectedI[OF RUN' ‹u∈limit r› ‹u∈limit r›]
obtain p where [simp]: "p≠[]" and P: "path E u p u"
by (rule trancl_is_path)
thus ?case by blast
next
case (insert A F)
from insert.IH insert.prems obtain pl where
[simp]: "pl≠[]"
and P: "path E u pl u"
and ACC: "(∀A'∈F. set pl ∩ A' ≠ {})"
by auto
from insert.prems obtain v where VACC: "v∈A" "v∈limit r" by auto
from run_limit_two_connectedI[OF RUN' ‹u∈limit r› ‹v∈limit r›]
obtain p1 where [simp]: "p1≠[]"
and P1: "path E u p1 v"
by (rule trancl_is_path)

from run_limit_two_connectedI[OF RUN' ‹v∈limit r› ‹u∈limit r›]
obtain p2 where [simp]: "p2≠[]"
and P2: "path E v p2 u"
by (rule trancl_is_path)

note P also note P1 also (path_conc) note P2 finally (path_conc)
have "path E u (pl@p1@p2) u" by simp
moreover from P2 have "v∈set (p1@p2)"
by (cases p2) (auto simp: path_cons_conv)
with ACC VACC have "(∀A'∈insert A F. set (pl@p1@p2) ∩ A' ≠ {})" by auto
moreover have "pl@p1@p2 ≠ []" by auto
ultimately show ?case by (intro exI conjI)
qed
then obtain pl where "pl ≠ []" "path E u pl u" "(∀A∈F. set pl ∩ A ≠ {})"
by blast
then obtain pls where "path E u (u#pls) u" "∀A∈F. set (u#pls) ∩ A ≠ {}"
by (cases pl) (auto simp add: path_simps)
ultimately show ?thesis
apply -
apply (rule
exI[where x="⦇lasso_reach = pr,lasso_va = u,lasso_cysfx = pls⦈"])
unfolding is_lasso_def lasso_v0_def lasso_cycle_def is_lasso_pre_def
apply (cases "pr")
done
qed
end

context b_graph
begin
definition is_lasso where "is_lasso L ≡
is_lasso_pre L
∧ (set (lasso_cycle L)) ∩ F ≠ {}"

definition is_lasso_prpl where "is_lasso_prpl L ≡
is_lasso_prpl_pre L
∧ (set (snd L)) ∩ F ≠ {}"

lemma is_lasso_pre_ext[simp]:
"gbg.is_lasso_pre T m = is_lasso_pre"
unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
unfolding to_gbg_ext_def
by auto

lemma is_lasso_gbg:
"gbg.is_lasso T m = is_lasso"
unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
apply simp
apply (auto simp: to_gbg_ext_def lasso_cycle_def)
done

lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]

lemma is_lasso_prpl_of_lasso[simp]:
"is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
unfolding is_lasso_def is_lasso_prpl_def
unfolding lasso_v0_def lasso_cycle_def
by auto

lemma is_lasso_prpl_conv:
"is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
apply safe
apply auto
done

lemma lasso_prpl_acc_run:
"is_lasso_prpl (pr, pl) ⟹ is_acc_run (pr ⌢ iter pl)"
apply (clarsimp simp: is_lasso_prpl_conv)
apply (drule lasso_accepted)
done

end

context igb_graph begin
definition "is_lasso L ≡
is_lasso_pre L
∧ (∀i<num_acc. ∃q∈set (lasso_cycle L). i∈acc q)"

definition "is_lasso_prpl L ≡
is_lasso_prpl_pre L
∧ (∀i<num_acc. ∃q∈set (snd L). i∈acc q)"

lemma is_lasso_prpl_of_lasso[simp]:
"is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
unfolding is_lasso_def is_lasso_prpl_def
unfolding lasso_v0_def lasso_cycle_def
by auto

lemma is_lasso_prpl_conv:
"is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
apply safe
apply auto
done

lemma is_lasso_pre_ext[simp]:
"gbg.is_lasso_pre T m = is_lasso_pre"
unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
unfolding to_gbg_ext_def
by auto

lemma is_lasso_gbg: "gbg.is_lasso T m = is_lasso"
unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
apply simp
apply (intro ext)
apply (fo_rule arg_cong | intro ext)+
apply (auto simp: F_def accn_def intro!: ext)
done

lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]

lemma lasso_prpl_acc_run:
"is_lasso_prpl (pr, pl) ⟹ is_acc_run (pr ⌢ iter pl)"
apply (clarsimp simp: is_lasso_prpl_conv)
apply (drule lasso_accepted)
done

lemma degen_lasso_sound:
assumes A: "degen.is_lasso T m L"
shows "is_lasso (map_lasso fst L)"
proof -

from A have
V0: "lasso_v0 L ∈ degen.V0 T m" and
REACH: "path (degen.E T m)
(lasso_v0 L) (lasso_reach L) (lasso_va L)" and
LOOP: "path (degen.E T m)
(lasso_va L) (lasso_cycle L) (lasso_va L)" and
ACC: "(set (lasso_cycle L)) ∩ degen.F T m ≠ {}"
unfolding degen.is_lasso_def degen.is_lasso_pre_def by auto

{
fix i
assume "i<num_acc"
hence "∃q∈set (lasso_cycle L). i ∈ local.acc (fst q) ∧ snd q = i"
proof (induction i)
case 0
thus ?case using ACC unfolding degeneralize_ext_def by fastforce
next
case (Suc i)
then obtain q where "(q,i)∈set (lasso_cycle L)" and "i∈acc q" by auto
with LOOP obtain pl' where SPL: "set (lasso_cycle L) = set pl'"
and PS: "path (degen.E T m) (q,i) pl' (q,i)"
by (blast elim: path_loop_shift)
from SPL have "pl'≠[]" by (auto simp: lasso_cycle_def)
then obtain pl'' where [simp]: "pl'=(q,i)#pl''"
using PS by (cases pl') (auto simp: path_simps)
then obtain q2 pl''' where
[simp]: "pl'' = (q2,(i + 1) mod num_acc)#pl'''"
using PS ‹i∈acc q› ‹Suc i < num_acc›
apply (cases pl'')
apply (auto
simp: path_simps degeneralize_ext_def
split: if_split_asm)
done
from PS have
"path (degen.E T m) (q2,Suc i) pl'' (q,i)"
using ‹Suc i < num_acc›
by (auto simp: path_simps)
from degen_visit_acc[OF this] obtain qa
where "(qa,Suc i)∈set pl''" "Suc i ∈ acc qa"
by auto
thus ?case
by (rule_tac bexI[where x="(qa,Suc i)"]) (auto simp: SPL)
qed
} note aux=this

from degen_V0_sound[OF V0]
degen_path_sound[OF REACH]
degen_path_sound[OF LOOP] aux
show ?thesis
unfolding is_lasso_def is_lasso_pre_def
by auto
qed

end

definition lasso_rel_ext_internal_def: "⋀Re R. lasso_rel_ext Re R ≡ {
(⦇ lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', …=m' ⦈,
⦇ lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, …=m ⦈) |
r' r va' va cysfx' cysfx m' m.
(r',r) ∈ ⟨R⟩list_rel
∧ (va',va)∈R
∧ (cysfx', cysfx) ∈ ⟨R⟩list_rel
∧ (m',m) ∈ Re
}"

lemma lasso_rel_ext_def: "⋀ Re R. ⟨Re,R⟩lasso_rel_ext = {
(⦇ lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', …=m' ⦈,
⦇ lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, …=m ⦈) |
r' r va' va cysfx' cysfx m' m.
(r',r) ∈ ⟨R⟩list_rel
∧ (va',va)∈R
∧ (cysfx', cysfx) ∈ ⟨R⟩list_rel
∧ (m',m) ∈ Re
}"
unfolding lasso_rel_ext_internal_def relAPP_def by auto

lemma lasso_rel_ext_sv[relator_props]:
"⋀ Re R. ⟦ single_valued Re; single_valued R ⟧ ⟹ single_valued (⟨Re,R⟩lasso_rel_ext)"
unfolding lasso_rel_ext_def
apply (rule single_valuedI)
apply safe
apply (blast dest: single_valuedD list_rel_sv[THEN single_valuedD])+
done

lemma lasso_rel_ext_id[relator_props]:
"⋀Re R. ⟦ Re=Id; R=Id ⟧ ⟹ ⟨Re,R⟩lasso_rel_ext = Id"
unfolding lasso_rel_ext_def
apply simp
apply safe
by (metis lasso.surjective)

consts i_lasso_ext :: "interface ⇒ interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of lasso_rel_ext i_lasso_ext]

find_consts "(_,_) lasso_scheme"
term lasso_reach_update

lemma lasso_param[param, autoref_rules]:
"⋀Re R. (lasso_reach, lasso_reach) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
"⋀Re R. (lasso_va, lasso_va) ∈ ⟨Re,R⟩lasso_rel_ext → R"
"⋀Re R. (lasso_cysfx, lasso_cysfx) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
"⋀Re R. (lasso_ext, lasso_ext)
∈ ⟨R⟩list_rel → R → ⟨R⟩list_rel → Re → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso_reach_update, lasso_reach_update)
∈ (⟨R⟩list_rel → ⟨R⟩list_rel) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso_va_update, lasso_va_update)
∈ (R→R) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso_cysfx_update, lasso_cysfx_update)
∈ (⟨R⟩list_rel → ⟨R⟩list_rel) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
"⋀Re R. (lasso.more_update, lasso.more_update)
∈ (Re→Re) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
unfolding lasso_rel_ext_def
by (auto dest: fun_relD)

lemma lasso_param2[param, autoref_rules]:
"⋀Re R. (lasso_v0, lasso_v0) ∈ ⟨Re,R⟩lasso_rel_ext → R"
"⋀Re R. (lasso_cycle, lasso_cycle) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
"⋀Re R. (map_lasso, map_lasso)
∈ (R→R') → ⟨Re,R⟩lasso_rel_ext → ⟨unit_rel,R'⟩lasso_rel_ext"
unfolding lasso_v0_def[abs_def] lasso_cycle_def[abs_def] map_lasso_def[abs_def]
by parametricity+

lemma lasso_of_prpl_param: "⟦(l',l)∈⟨R⟩list_rel ×⇩r ⟨R⟩list_rel; snd l ≠ []⟧
⟹ (lasso_of_prpl l', lasso_of_prpl l) ∈ ⟨unit_rel,R⟩lasso_rel_ext"
unfolding lasso_of_prpl_def
apply (cases l, cases l', clarsimp)
apply (case_tac b, simp, case_tac ba, clarsimp_all)
apply parametricity
done

context begin interpretation autoref_syn .

lemma lasso_of_prpl_autoref[autoref_rules]:
assumes "SIDE_PRECOND (snd l ≠ [])"
assumes "(l',l)∈⟨R⟩list_rel ×⇩r ⟨R⟩list_rel"
shows "(lasso_of_prpl l',
(OP lasso_of_prpl
::: ⟨R⟩list_rel ×⇩r ⟨R⟩list_rel → ⟨unit_rel,R⟩lasso_rel_ext)$l) ∈ ⟨unit_rel,R⟩lasso_rel_ext" using assms apply (simp add: lasso_of_prpl_param) done end subsection ‹Implementing runs by lassos› definition lasso_run_rel_def_internal: "lasso_run_rel R ≡ br run_of_lasso (λ_. True) O (nat_rel → R)" lemma lasso_run_rel_def: "⟨R⟩lasso_run_rel = br run_of_lasso (λ_. True) O (nat_rel → R)" unfolding lasso_run_rel_def_internal relAPP_def by simp lemma lasso_run_rel_sv[relator_props]: "single_valued R ⟹ single_valued (⟨R⟩lasso_run_rel)" unfolding lasso_run_rel_def by tagged_solver consts i_run :: "interface ⇒ interface" lemmas [autoref_rel_intf] = REL_INTFI[of lasso_run_rel i_run] definition [simp]: "op_map_run ≡ (o)" lemma [autoref_op_pat]: "(o) ≡ op_map_run" by simp lemma map_lasso_run_refine[autoref_rules]: shows "(map_lasso,op_map_run) ∈ (R→R') → ⟨R⟩lasso_run_rel → ⟨R'⟩lasso_run_rel" unfolding lasso_run_rel_def op_map_run_def proof (intro fun_relI) fix f f' l r assume [param]: "(f,f')∈R→R'" and "(l, r) ∈ br run_of_lasso (λ_. True) O (nat_rel → R)" then obtain r' where [param]: "(r',r)∈nat_rel → R" and [simp]: "r' = run_of_lasso l" by (auto simp: br_def) have "(map_lasso f l, f o r') ∈ br run_of_lasso (λ_. True)" by (simp add: br_def) also have "(f o r', f' o r) ∈ nat_rel → R'" by parametricity finally (relcompI) show "(map_lasso f l, f' o r) ∈ br run_of_lasso (λ_. True) O (nat_rel → R')" . qed end  # Theory Simulation section ‹Simulation› theory Simulation imports Automata begin lemma finite_ImageI: assumes "finite A" assumes "⋀a. a∈A ⟹ finite (R{a})" shows "finite (RA)" proof - note [[simproc add: finite_Collect]] have "RA = ⋃{R{a} | a. a:A}" by auto also have "finite (⋃{R{a} | a. a:A})" apply (rule finite_Union) apply (simp add: assms) apply (clarsimp simp: assms) done finally show ?thesis . qed section ‹Simulation› subsection ‹Functional Relations› definition "the_br_α R ≡ λ x. SOME y. (x, y) ∈ R" abbreviation (input) "the_br_invar R ≡ λ x. x ∈ Domain R" lemma the_br[simp]: assumes "single_valued R" shows "br (the_br_α R) (the_br_invar R) = R" unfolding build_rel_def the_br_α_def apply auto apply (metis someI_ex) apply (metis assms someI_ex single_valuedD) done lemma the_br_br[simp]: "I x ⟹ the_br_α (br α I) x = α x" "the_br_invar (br α I) = I" unfolding the_br_α_def build_rel_def[abs_def] by auto subsection ‹Relation between Runs› definition run_rel :: "('a × 'b) set ⇒ ('a word × 'b word) set" where "run_rel R ≡ {(ra, rb). ∀ i. (ra i, rb i) ∈ R}" lemma run_rel_converse[simp]: "(ra, rb) ∈ run_rel (R¯) ⟷ (rb, ra) ∈ run_rel R" unfolding run_rel_def by auto lemma run_rel_single_valued: "single_valued R ⟹ (ra, rb) ∈ run_rel R ⟷ ((∀i. the_br_invar R (ra i)) ∧ rb = the_br_α R o ra)" unfolding run_rel_def the_br_α_def apply (auto intro!: ext) apply (metis single_valuedD someI_ex) apply (metis DomainE someI_ex) done subsection ‹Simulation› locale simulation = a: graph A + b: graph B for R :: "('a × 'b) set" and A :: "('a, _) graph_rec_scheme" and B :: "('b, _) graph_rec_scheme" + assumes nodes_sim: "a ∈ a.V ⟹ (a, b) ∈ R ⟹ b ∈ b.V" assumes init_sim: "a0 ∈ a.V0 ⟹ ∃ b0. b0 ∈ b.V0 ∧ (a0, b0) ∈ R" assumes step_sim: "(a, a') ∈ a.E ⟹ (a, b) ∈ R ⟹ ∃ b'. (b, b') ∈ b.E ∧ (a', b') ∈ R" begin lemma simulation_this: "simulation R A B" by unfold_locales lemma run_sim: assumes arun: "a.is_run ra" obtains rb where "b.is_run rb" "(ra, rb) ∈ run_rel R" proof - from arun have ainit: "ra 0 ∈ a.V0" and astep: "∀i. (ra i, ra (Suc i)) ∈ a.E" using a.run_V0 a.run_ipath ipathD by blast+ from init_sim obtain rb0 where rel0: "(ra 0, rb0) ∈ R" and binit: "rb0 ∈ b.V0" by (auto intro: ainit) define rb where "rb = rec_nat rb0 (λi rbi. SOME rbsi. (rbi, rbsi) ∈ b.E ∧ (ra (Suc i), rbsi) ∈ R)" have [simp]: "rb 0 = rb0" "⋀i. rb (Suc i) = (SOME rbsi. (rb i, rbsi) ∈ b.E ∧ (ra (Suc i), rbsi) ∈ R)" unfolding rb_def by auto { fix i have "(rb i, rb (Suc i)) ∈ b.E ∧ (ra (Suc i), rb (Suc i)) ∈ R" proof (induction i) case 0 from step_sim astep rel0 obtain rb1 where "(rb 0, rb1) ∈ b.E" and "(ra 1, rb1) ∈ R" by fastforce thus ?case by (auto intro!: someI) next case (Suc i) with step_sim astep obtain rbss where "(rb (Suc i), rbss) ∈ b.E" and "(ra (Suc (Suc i)), rbss) ∈ R" by fastforce thus ?case by (auto intro!: someI) qed } note aux=this from aux binit have "b.is_run rb" unfolding b.is_run_def ipath_def by simp moreover from aux rel0 have "(ra, rb) ∈ run_rel R" unfolding run_rel_def apply safe apply (case_tac i) by auto ultimately show ?thesis by rule qed lemma stuck_sim: assumes "(a, b) ∈ R" assumes "b ∉ Domain b.E" shows "a ∉ Domain a.E" using assms by (auto dest: step_sim) lemma run_Domain: "a.is_run r ⟹ r i ∈ Domain R" by (erule run_sim) (auto simp: run_rel_def) lemma br_run_sim: assumes "R = br α I" assumes "a.is_run r" shows "b.is_run (α o r)" using assms apply - apply (erule run_sim) apply (auto simp: run_rel_def build_rel_def a.is_run_def b.is_run_def ipath_def) done lemma is_reachable_sim: "a ∈ a.E⇧*  a.V0 ⟹ ∃ b. (a, b) ∈ R ∧ b ∈ b.E⇧*  b.V0" apply safe apply (erule rtrancl_induct) apply (metis ImageI init_sim rtrancl.rtrancl_refl) apply (metis rtrancl_image_advance step_sim) done lemma reachable_sim: "a.E⇧*  a.V0 ⊆ R¯  b.E⇧*  b.V0" using is_reachable_sim by blast lemma reachable_finite_sim: assumes "finite (b.E⇧*  b.V0)" assumes "⋀b. b ∈ b.E⇧*  b.V0 ⟹ finite (R¯  {b})" shows "finite (a.E⇧*  a.V0)" apply (rule finite_subset[OF reachable_sim]) apply (rule finite_ImageI) apply fact+ done end lemma simulation_trans[trans]: assumes "simulation R1 A B" assumes "simulation R2 B C" shows "simulation (R1 O R2) A C" proof - interpret s1: simulation R1 A B by fact interpret s2: simulation R2 B C by fact show ?thesis apply unfold_locales using s1.nodes_sim s2.nodes_sim apply blast using s1.init_sim s2.init_sim apply blast using s1.step_sim s2.step_sim apply blast done qed lemma (in graph) simulation_refl[simp]: "simulation Id G G" by unfold_locales auto locale lsimulation = a: sa A + b: sa B + simulation R A B for R :: "('a × 'b) set" and A :: "('a, 'l, _) sa_rec_scheme" and B :: "('b, 'l, _) sa_rec_scheme" + assumes labeling_consistent: "(a, b) ∈ R ⟹ a.L a = b.L b" begin lemma lsimulation_this: "lsimulation R A B" by unfold_locales lemma run_rel_consistent: "(ra, rb) ∈ run_rel R ⟹ a.L o ra = b.L o rb" using labeling_consistent unfolding run_rel_def by auto lemma accept_sim: "a.accept w ⟹ b.accept w" unfolding a.accept_def b.accept_def apply clarsimp apply (erule run_sim) apply (auto simp: run_rel_consistent) done end lemma lsimulation_trans[trans]: assumes "lsimulation R1 A B" assumes "lsimulation R2 B C" shows "lsimulation (R1 O R2) A C" proof - interpret s1: lsimulation R1 A B by fact interpret s2: lsimulation R2 B C by fact interpret simulation "R1 O R2" A C using simulation_trans s1.simulation_this s2.simulation_this by this show ?thesis apply unfold_locales using s1.labeling_consistent s2.labeling_consistent by auto qed lemma (in sa) lsimulation_refl[simp]: "lsimulation Id G G" by unfold_locales auto subsection ‹Bisimulation› locale bisimulation = a: graph A + b: graph B + s1: simulation "R" A B + s2: simulation "R¯" B A for R :: "('a × 'b) set" and A :: "('a, _) graph_rec_scheme" and B :: "('b, _) graph_rec_scheme" begin lemma bisimulation_this: "bisimulation R A B" by unfold_locales lemma converse: "bisimulation (R¯) B A" proof - interpret simulation "(R¯)¯" A B by simp unfold_locales show ?thesis by unfold_locales qed lemma br_run_conv: assumes "R = br α I" shows "b.is_run rb ⟷ (∃ra. rb=α o ra ∧ a.is_run ra)" using assms apply safe apply (erule s2.run_sim, auto intro!: ext simp: run_rel_def build_rel_def) [] apply (erule s1.br_run_sim, assumption) done lemma bri_run_conv: assumes "R = (br γ I)¯" shows "a.is_run ra ⟷ (∃rb. ra=γ o rb ∧ b.is_run rb)" using assms apply safe apply (erule s1.run_sim, auto simp: run_rel_def build_rel_def intro!: ext) [] apply (erule s2.run_sim, auto simp: run_rel_def build_rel_def) by (metis (no_types, hide_lams) fun_comp_eq_conv) lemma inj_map_run_eq: assumes "inj α" assumes E: "α o r1 = α o r2" shows "r1 = r2" proof (rule ext) fix i from E have "α (r1 i) = α (r2 i)" by (simp add: comp_def) metis with ‹inj α› show "r1 i = r2 i" by (auto dest: injD) qed lemma br_inj_run_conv: assumes INJ: "inj α" assumes [simp]: "R = br α I" shows "b.is_run (α o ra) ⟷ a.is_run ra" apply (subst br_run_conv[OF assms(2)]) apply (auto dest: inj_map_run_eq[OF INJ]) done lemma single_valued_run_conv: assumes "single_valued R" shows "b.is_run rb ⟷ (∃ra. rb=the_br_α R o ra ∧ a.is_run ra)" using assms apply safe apply (erule s2.run_sim) apply (auto simp add: run_rel_single_valued) apply (erule s1.run_sim) apply (auto simp add: run_rel_single_valued) done lemma stuck_bisim: assumes A: "(a, b) ∈ R" shows "a ∈ Domain a.E ⟷ b ∈ Domain b.E" using s1.stuck_sim[OF A] using s2.stuck_sim[OF A[THEN converseI[of _ _ R]]] by blast end lemma bisimulation_trans[trans]: assumes "bisimulation R1 A B" assumes "bisimulation R2 B C" shows "bisimulation (R1 O R2) A C" proof - interpret s1: bisimulation R1 A B by fact interpret s2: bisimulation R2 B C by fact interpret t1: simulation "(R1 O R2)" A C using simulation_trans s1.s1.simulation_this s2.s1.simulation_this by this interpret t2: simulation "(R1 O R2)¯" C A using simulation_trans s2.s2.simulation_this s1.s2.simulation_this unfolding converse_relcomp by this show ?thesis by unfold_locales qed lemma (in graph) bisimulation_refl[simp]: "bisimulation Id G G" by unfold_locales auto locale lbisimulation = a: sa A + b: sa B + s1: lsimulation "R" A B + s2: lsimulation "R¯" B A + bisimulation R A B for R :: "('a × 'b) set" and A :: "('a, 'l, _) sa_rec_scheme" and B :: "('b, 'l, _) sa_rec_scheme" begin lemma lbisimulation_this: "lbisimulation R A B" by unfold_locales lemma accept_bisim: "a.accept = b.accept" apply (rule ext) using s1.accept_sim s2.accept_sim by blast end lemma lbisimulation_trans[trans]: assumes "lbisimulation R1 A B" assumes "lbisimulation R2 B C" shows "lbisimulation (R1 O R2) A C" proof - interpret s1: lbisimulation R1 A B by fact interpret s2: lbisimulation R2 B C by fact from lsimulation_trans[OF s1.s1.lsimulation_this s2.s1.lsimulation_this] interpret t1: lsimulation "(R1 O R2)" A C . from lsimulation_trans[OF s2.s2.lsimulation_this s1.s2.lsimulation_this, folded converse_relcomp] interpret t2: lsimulation "(R1 O R2)¯" C A . show ?thesis by unfold_locales qed lemma (in sa) lbisimulation_refl[simp]: "lbisimulation Id G G" by unfold_locales auto end  # Theory Step_Conv theory Step_Conv imports Main begin (* Different ways of representing transitions, and functions to convert between them: rel :: ('a × 'b) set pred :: 'a ⇒ 'b ⇒ bool succ :: 'a ⇒ 'b set *) definition "rel_of_pred s ≡ {(a,b). s a b}" definition "rel_of_succ s ≡ {(a,b). b∈s a}" definition "pred_of_rel s ≡ λa b. (a,b)∈s" definition "pred_of_succ s ≡ λa b. b∈s a" definition "succ_of_rel s ≡ λa. {b. (a,b)∈s}" definition "succ_of_pred s ≡ λa. {b. s a b}" lemma rps_expand[simp]: "(a,b)∈rel_of_pred p ⟷ p a b" "(a,b)∈rel_of_succ s ⟷ b ∈ s a" "pred_of_rel r a b ⟷ (a,b)∈r" "pred_of_succ s a b ⟷ b ∈ s a" "b∈succ_of_rel r a ⟷ (a,b)∈r" "b∈succ_of_pred p a ⟷ p a b" unfolding rel_of_pred_def pred_of_rel_def unfolding rel_of_succ_def succ_of_rel_def unfolding pred_of_succ_def succ_of_pred_def by auto lemma rps_conv[simp]: "rel_of_pred (pred_of_rel r) = r" "rel_of_pred (pred_of_succ s) = rel_of_succ s" "rel_of_succ (succ_of_rel r) = r" "rel_of_succ (succ_of_pred p) = rel_of_pred p" "pred_of_rel (rel_of_pred p) = p" "pred_of_rel (rel_of_succ s) = pred_of_succ s" "pred_of_succ (succ_of_pred p) = p" "pred_of_succ (succ_of_rel r) = pred_of_rel r" "succ_of_rel (rel_of_succ s) = s" "succ_of_rel (rel_of_pred p) = succ_of_pred p" "succ_of_pred (pred_of_succ s) = s" "succ_of_pred (pred_of_rel r) = succ_of_rel r" unfolding rel_of_pred_def pred_of_rel_def unfolding rel_of_succ_def succ_of_rel_def unfolding pred_of_succ_def succ_of_pred_def by auto (* Lifting transitions from option monad to option×option *) definition m2r_rel :: "('a × 'a option) set ⇒ 'a option rel" where "m2r_rel r ≡ {(Some a,b)|a b. (a,b)∈r}" definition m2r_pred :: "('a ⇒ 'a option ⇒ bool) ⇒ 'a option ⇒ 'a option ⇒ bool" where "m2r_pred p ≡ λNone ⇒ λ_. False | Some a ⇒ p a" definition m2r_succ :: "('a ⇒ 'a option set) ⇒ 'a option ⇒ 'a option set" where "m2r_succ s ≡ λNone ⇒ {} | Some a ⇒ s a" lemma m2r_expand[simp]: "(a,b)∈m2r_rel r ⟷ (∃a'. a=Some a' ∧ (a',b)∈r)" "m2r_pred p a b ⟷ (∃a'. a=Some a' ∧ p a' b)" "b∈m2r_succ s a ⟷ (∃a'. a=Some a' ∧ b ∈ s a')" unfolding m2r_rel_def m2r_succ_def m2r_pred_def by (auto split: option.splits) lemma m2r_conv[simp]: "m2r_rel (rel_of_succ s) = rel_of_succ (m2r_succ s)" "m2r_rel (rel_of_pred p) = rel_of_pred (m2r_pred p)" "m2r_pred (pred_of_succ s) = pred_of_succ (m2r_succ s)" "m2r_pred (pred_of_rel r) = pred_of_rel (m2r_rel r)" "m2r_succ (succ_of_pred p) = succ_of_pred (m2r_pred p)" "m2r_succ (succ_of_rel r) = succ_of_rel (m2r_rel r)" unfolding rel_of_pred_def pred_of_rel_def unfolding rel_of_succ_def succ_of_rel_def unfolding pred_of_succ_def succ_of_pred_def unfolding m2r_rel_def m2r_succ_def m2r_pred_def by (auto split: option.splits) definition "rel_of_enex enex ≡ let (en, ex) = enex in {(s, ex a s) |s a. a ∈ en s}" definition "pred_of_enex enex ≡ λs s'. let (en,ex) = enex in ∃a∈en s. s'=ex a s" definition "succ_of_enex enex ≡ λs. let (en,ex) = enex in {s'. ∃a∈en s. s'=ex a s}" lemma x_of_enex_expand[simp]: "(s, s') ∈ rel_of_enex (en, ex) ⟷ (∃ a ∈ en s. s' = ex a s)" "pred_of_enex (en,ex) s s' ⟷ (∃a∈en s. s'=ex a s)" "s'∈succ_of_enex (en,ex) s ⟷ (∃a∈en s. s'=ex a s)" unfolding rel_of_enex_def pred_of_enex_def succ_of_enex_def by auto lemma x_of_enex_conv[simp]: "rel_of_pred (pred_of_enex enex) = rel_of_enex enex" "rel_of_succ (succ_of_enex enex) = rel_of_enex enex" "pred_of_rel (rel_of_enex enex) = pred_of_enex enex" "pred_of_succ (succ_of_enex enex) = pred_of_enex enex" "succ_of_rel (rel_of_enex enex) = succ_of_enex enex" "succ_of_pred (pred_of_enex enex) = succ_of_enex enex" unfolding rel_of_enex_def pred_of_enex_def succ_of_enex_def unfolding rel_of_pred_def rel_of_succ_def unfolding pred_of_rel_def pred_of_succ_def unfolding succ_of_rel_def succ_of_pred_def by auto end  # Theory Stuttering_Extension theory Stuttering_Extension imports Simulation Step_Conv begin definition stutter_extend_edges :: "'v set ⇒ 'v digraph ⇒ 'v digraph" where "stutter_extend_edges V E ≡ E ∪ {(v, v) |v. v ∈ V ∧ v ∉ Domain E}" lemma stutter_extend_edgesI_edge: assumes "(u, v) ∈ E" shows "(u, v) ∈ stutter_extend_edges V E" using assms unfolding stutter_extend_edges_def by auto lemma stutter_extend_edgesI_stutter: assumes "v ∈ V" "v ∉ Domain E" shows "(v, v) ∈ stutter_extend_edges V E" using assms unfolding stutter_extend_edges_def by auto lemma stutter_extend_edgesE: assumes "(u, v) ∈ stutter_extend_edges V E" obtains (edge) "(u, v) ∈ E" | (stutter) "u ∈ V" "u ∉ Domain E" "u = v" using assms unfolding stutter_extend_edges_def by auto lemma stutter_extend_wf: "E ⊆ V × V ⟹ stutter_extend_edges V E ⊆ V × V" unfolding stutter_extend_edges_def by auto lemma stutter_extend_edges_rtrancl[simp]: "(stutter_extend_edges V E)⇧* = E⇧*" unfolding stutter_extend_edges_def by (auto intro: in_rtrancl_UnI elim: rtrancl_induct) lemma stutter_extend_domain: "V ⊆ Domain (stutter_extend_edges V E)" unfolding stutter_extend_edges_def by auto definition stutter_extend :: "('v, _) graph_rec_scheme ⇒ ('v, _) graph_rec_scheme" where "stutter_extend G ≡ ⦇ g_V = g_V G, g_E = stutter_extend_edges (g_V G) (g_E G), g_V0 = g_V0 G, … = graph_rec.more G ⦈" lemma stutter_extend_simps[simp]: "g_V (stutter_extend G) = g_V G" "g_E (stutter_extend G) = stutter_extend_edges (g_V G) (g_E G)" "g_V0 (stutter_extend G) = g_V0 G" unfolding stutter_extend_def by auto lemma stutter_extend_simps_sa[simp]: "sa_L (stutter_extend G) = sa_L G" unfolding stutter_extend_def by (metis graph_rec.select_convs(4) sa_rec.select_convs(1) sa_rec.surjective) lemma (in graph) stutter_extend_graph: "graph (stutter_extend G)" using V0_ss E_ss by (unfold_locales, auto intro!: stutter_extend_wf) lemma (in sa) stutter_extend_sa: "sa (stutter_extend G)" proof - interpret graph "stutter_extend G" using stutter_extend_graph by this show ?thesis by unfold_locales qed lemma (in bisimulation) stutter_extend: "bisimulation R (stutter_extend A) (stutter_extend B)" proof - interpret ea: graph "stutter_extend A" by (rule a.stutter_extend_graph) interpret eb: graph "stutter_extend B" by (rule b.stutter_extend_graph) show ?thesis proof fix a b assume "a ∈ g_V (stutter_extend A)" "(a, b) ∈ R" thus "b ∈ g_V (stutter_extend B)" using s1.nodes_sim by simp next fix a assume "a ∈ g_V0 (stutter_extend A)" thus "∃ b. b ∈ g_V0 (stutter_extend B) ∧ (a, b) ∈ R" using s1.init_sim by simp next fix a a' b assume "(a, a') ∈ g_E (stutter_extend A)" "(a, b) ∈ R" thus "∃ b'. (b, b') ∈ g_E (stutter_extend B) ∧ (a', b') ∈ R" apply simp using s1.nodes_sim s1.step_sim s2.stuck_sim by (blast intro: stutter_extend_edgesI_edge stutter_extend_edgesI_stutter elim: stutter_extend_edgesE) next fix b a assume "b ∈ g_V (stutter_extend B)" "(b, a) ∈ R¯" thus "a ∈ g_V (stutter_extend A)" using s2.nodes_sim by simp next fix b assume "b ∈ g_V0 (stutter_extend B)" thus "∃ a. a ∈ g_V0 (stutter_extend A) ∧ (b, a) ∈ R¯" using s2.init_sim by simp next fix b b' a assume "(b, b') ∈ g_E (stutter_extend B)" "(b, a) ∈ R¯" thus "∃ a'. (a, a') ∈ g_E (stutter_extend A) ∧ (b', a') ∈ R¯" apply simp using s2.nodes_sim s2.step_sim s1.stuck_sim by (blast intro: stutter_extend_edgesI_edge stutter_extend_edgesI_stutter elim: stutter_extend_edgesE) qed qed lemma (in lbisimulation) lstutter_extend: "lbisimulation R (stutter_extend A) (stutter_extend B)" proof - interpret se: bisimulation R "stutter_extend A" "stutter_extend B" by (rule stutter_extend) show ?thesis by (unfold_locales, auto simp: s1.labeling_consistent) qed definition stutter_extend_en :: "('s⇒'a set) ⇒ ('s ⇒ 'a option set)" where "stutter_extend_en en ≡ λs. let as = en s in if as={} then {None} else Someas" definition stutter_extend_ex :: "('a ⇒ 's ⇒ 's) ⇒ ('a option ⇒ 's ⇒ 's)" where "stutter_extend_ex ex ≡ λNone ⇒ id | Some a ⇒ ex a" abbreviation stutter_extend_enex :: "('s⇒'a set) × ('a ⇒ 's ⇒ 's) ⇒ ('s ⇒ 'a option set) × ('a option ⇒ 's ⇒ 's)" where "stutter_extend_enex ≡ map_prod stutter_extend_en stutter_extend_ex" lemma stutter_extend_pred_of_enex_conv: "stutter_extend_edges UNIV (rel_of_enex enex) = rel_of_enex (stutter_extend_enex enex)" unfolding rel_of_enex_def stutter_extend_edges_def apply (auto simp: stutter_extend_en_def stutter_extend_ex_def split: prod.splits) apply force apply blast done lemma stutter_extend_en_Some_eq[simp]: "Some a ∈ stutter_extend_en en gc ⟷ a ∈ en gc" "stutter_extend_ex ex (Some a) gc = ex a gc" unfolding stutter_extend_en_def stutter_extend_ex_def by auto lemma stutter_extend_ex_None_eq[simp]: "stutter_extend_ex ex None = id" unfolding stutter_extend_ex_def by auto end  # Theory Digraph_Impl section ‹Implementing Graphs› (* Author: Peter Lammich *) theory Digraph_Impl imports Digraph begin subsection ‹Directed Graphs by Successor Function› type_synonym 'a slg = "'a ⇒ 'a list" definition slg_rel :: "('a×'b) set ⇒ ('a slg × 'b digraph) set" where slg_rel_def_internal: "slg_rel R ≡ (R → ⟨R⟩list_set_rel) O br (λsuccs. {(u,v). v∈succs u}) (λ_. True)" lemma slg_rel_def: "⟨R⟩slg_rel = (R → ⟨R⟩list_set_rel) O br (λsuccs. {(u,v). v∈succs u}) (λ_. True)" unfolding slg_rel_def_internal relAPP_def by simp lemma slg_rel_sv[relator_props]: "⟦single_valued R; Range R = UNIV⟧ ⟹ single_valued (⟨R⟩slg_rel)" unfolding slg_rel_def by (tagged_solver) consts i_slg :: "interface ⇒ interface" lemmas [autoref_rel_intf] = REL_INTFI[of slg_rel i_slg] definition [simp]: "op_slg_succs E v ≡ E{v}" lemma [autoref_itype]: "op_slg_succs ::⇩i ⟨I⟩⇩ii_slg →⇩i I →⇩i ⟨I⟩⇩ii_set" by simp context begin interpretation autoref_syn . lemma [autoref_op_pat]: "E{v} ≡ op_slg_succs$E$v" by simp end lemma refine_slg_succs[autoref_rules_raw]: "(λsuccs v. succs v,op_slg_succs)∈⟨R⟩slg_rel→R→⟨R⟩list_set_rel" apply (intro fun_relI) apply (auto simp add: slg_rel_def br_def dest: fun_relD) done definition "E_of_succ succ ≡ { (u,v). v∈succ u }" definition "succ_of_E E ≡ (λu. {v . (u,v)∈E})" lemma E_of_succ_of_E[simp]: "E_of_succ (succ_of_E E) = E" unfolding E_of_succ_def succ_of_E_def by auto lemma succ_of_E_of_succ[simp]: "succ_of_E (E_of_succ E) = E" unfolding E_of_succ_def succ_of_E_def by auto context begin interpretation autoref_syn . lemma [autoref_itype]: "E_of_succ ::⇩i (I →⇩i ⟨I⟩⇩ii_set) →⇩i ⟨I⟩⇩ii_slg" by simp lemma [autoref_itype]: "succ_of_E ::⇩i ⟨I⟩⇩ii_slg →⇩i I →⇩i ⟨I⟩⇩ii_set" by simp end lemma E_of_succ_refine[autoref_rules]: "(λx. x, E_of_succ) ∈ (R → ⟨R⟩list_set_rel) → ⟨R⟩slg_rel" "(λx. x, succ_of_E) ∈ ⟨R⟩slg_rel → (R → ⟨R⟩list_set_rel)" unfolding E_of_succ_def[abs_def] succ_of_E_def[abs_def] slg_rel_def br_def apply auto [] apply clarsimp apply (blast dest: fun_relD) done subsubsection ‹Restricting Edges› definition op_graph_restrict :: "'v set ⇒ 'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set" where [simp]: "op_graph_restrict Vl Vr E ≡ E ∩ Vl × Vr" definition op_graph_restrict_left :: "'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set" where [simp]: "op_graph_restrict_left Vl E ≡ E ∩ Vl × UNIV" definition op_graph_restrict_right :: "'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set" where [simp]: "op_graph_restrict_right Vr E ≡ E ∩ UNIV × Vr" lemma [autoref_op_pat]: "E ∩ (Vl × Vr) ≡ op_graph_restrict Vl Vr E" "E ∩ (Vl × UNIV) ≡ op_graph_restrict_left Vl E" "E ∩ (UNIV × Vr) ≡ op_graph_restrict_right Vr E" by simp_all lemma graph_restrict_aimpl: "op_graph_restrict Vl Vr E = E_of_succ (λv. if v∈Vl then {x ∈ E{v}. x∈Vr} else {})" by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm) lemma graph_restrict_left_aimpl: "op_graph_restrict_left Vl E = E_of_succ (λv. if v∈Vl then E{v} else {})" by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm) lemma graph_restrict_right_aimpl: "op_graph_restrict_right Vr E = E_of_succ (λv. {x ∈ E{v}. x∈Vr})" by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm) schematic_goal graph_restrict_impl_aux: fixes Rsl Rsr notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set] assumes [autoref_rules]: "(meml, (∈)) ∈ R → ⟨R⟩Rsl → bool_rel" assumes [autoref_rules]: "(memr, (∈)) ∈ R → ⟨R⟩Rsr → bool_rel" shows "(?c, op_graph_restrict) ∈ ⟨R⟩Rsl → ⟨R⟩Rsr → ⟨R⟩slg_rel → ⟨R⟩slg_rel" unfolding graph_restrict_aimpl[abs_def] apply (autoref (keep_goal)) done schematic_goal graph_restrict_left_impl_aux: fixes Rsl Rsr notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set] assumes [autoref_rules]: "(meml, (∈)) ∈ R → ⟨R⟩Rsl → bool_rel" shows "(?c, op_graph_restrict_left) ∈ ⟨R⟩Rsl → ⟨R⟩slg_rel → ⟨R⟩slg_rel" unfolding graph_restrict_left_aimpl[abs_def] apply (autoref (keep_goal, trace)) done schematic_goal graph_restrict_right_impl_aux: fixes Rsl Rsr notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set] assumes [autoref_rules]: "(memr, (∈)) ∈ R → ⟨R⟩Rsr → bool_rel" shows "(?c, op_graph_restrict_right) ∈ ⟨R⟩Rsr → ⟨R⟩slg_rel → ⟨R⟩slg_rel" unfolding graph_restrict_right_aimpl[abs_def] apply (autoref (keep_goal, trace)) done concrete_definition graph_restrict_impl uses graph_restrict_impl_aux concrete_definition graph_restrict_left_impl uses graph_restrict_left_impl_aux concrete_definition graph_restrict_right_impl uses graph_restrict_right_impl_aux context begin interpretation autoref_syn . lemma [autoref_itype]: "op_graph_restrict ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_slg" "op_graph_restrict_right ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_slg" "op_graph_restrict_left ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_slg" by auto end lemmas [autoref_rules_raw] = graph_restrict_impl.refine[OF GEN_OP_D GEN_OP_D] graph_restrict_left_impl.refine[OF GEN_OP_D] graph_restrict_right_impl.refine[OF GEN_OP_D] schematic_goal "(?c::?'c, λ(E::nat digraph) x. E{x}) ∈ ?R" apply (autoref (keep_goal)) done lemma graph_minus_aimpl: fixes E1 E2 :: "'a rel" shows "E1-E2 = E_of_succ (λx. E1{x} - E2{x})" by (auto simp: E_of_succ_def) schematic_goal graph_minus_impl_aux: fixes R :: "('vi×'v) set" assumes [autoref_rules]: "(eq,(=))∈R→R→bool_rel" shows "(?c, (-)) ∈ ⟨R⟩slg_rel → ⟨R⟩slg_rel → ⟨R⟩slg_rel" apply (subst graph_minus_aimpl[abs_def]) apply (autoref (keep_goal,trace)) done lemmas [autoref_rules] = graph_minus_impl_aux[OF GEN_OP_D] lemma graph_minus_set_aimpl: fixes E1 E2 :: "'a rel" shows "E1-E2 = E_of_succ (λu. {v∈E1{u}. (u,v)∉E2})" by (auto simp: E_of_succ_def) schematic_goal graph_minus_set_impl_aux: fixes R :: "('vi×'v) set" assumes [autoref_rules]: "(eq,(=))∈R→R→bool_rel" assumes [autoref_rules]: "(mem,(∈)) ∈ R ×⇩r R → ⟨R ×⇩r R⟩Rs → bool_rel" shows "(?c, (-)) ∈ ⟨R⟩slg_rel → ⟨R×⇩rR⟩Rs → ⟨R⟩slg_rel" apply (subst graph_minus_set_aimpl[abs_def]) apply (autoref (keep_goal,trace)) done lemmas [autoref_rules (overloaded)] = graph_minus_set_impl_aux[OF GEN_OP_D GEN_OP_D] subsection ‹Rooted Graphs› subsubsection ‹Operation Identification Setup› consts i_g_ext :: "interface ⇒ interface ⇒ interface" abbreviation "i_frg ≡ ⟨i_unit⟩⇩ii_g_ext" context begin interpretation autoref_syn . lemma g_type[autoref_itype]: "g_V ::⇩i ⟨Ie,I⟩⇩ii_g_ext →⇩i ⟨I⟩⇩ii_set" "g_E ::⇩i ⟨Ie,I⟩⇩ii_g_ext →⇩i ⟨I⟩⇩ii_slg" "g_V0 ::⇩i ⟨Ie,I⟩⇩ii_g_ext →⇩i ⟨I⟩⇩ii_set" "graph_rec_ext ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_set →⇩i iE →⇩i ⟨Ie,I⟩⇩ii_g_ext" by simp_all end subsubsection ‹Generic Implementation› record ('vi,'ei,'v0i) gen_g_impl = gi_V :: 'vi gi_E :: 'ei gi_V0 :: 'v0i definition gen_g_impl_rel_ext_internal_def: "⋀ Rm Rv Re Rv0. gen_g_impl_rel_ext Rm Rv Re Rv0 ≡ { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m) | Vi Ei V0i mi V E V0 m. (Vi,V)∈Rv ∧ (Ei,E)∈Re ∧ (V0i,V0)∈Rv0 ∧ (mi,m)∈Rm }" lemma gen_g_impl_rel_ext_def: "⋀Rm Rv Re Rv0. ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext ≡ { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m) | Vi Ei V0i mi V E V0 m. (Vi,V)∈Rv ∧ (Ei,E)∈Re ∧ (V0i,V0)∈Rv0 ∧ (mi,m)∈Rm }" unfolding gen_g_impl_rel_ext_internal_def relAPP_def by simp lemma gen_g_impl_rel_sv[relator_props]: "⋀Rm Rv Re Rv0. ⟦single_valued Rv; single_valued Re; single_valued Rv0; single_valued Rm ⟧ ⟹ single_valued (⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext)" unfolding gen_g_impl_rel_ext_def apply (auto intro!: single_valuedI dest: single_valuedD slg_rel_sv list_set_rel_sv) done lemma gen_g_refine: "⋀Rm Rv Re Rv0. (gi_V,g_V) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Rv" "⋀Rm Rv Re Rv0. (gi_E,g_E) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Re" "⋀Rm Rv Re Rv0. (gi_V0,g_V0) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Rv0" "⋀Rm Rv Re Rv0. (gen_g_impl_ext, graph_rec_ext) ∈ Rv → Re → Rv0 → Rm → ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext" unfolding gen_g_impl_rel_ext_def by auto subsubsection ‹Implementation with list-set for Nodes› type_synonym ('v,'m) frgv_impl_scheme = "('v list, 'v ⇒ 'v list, 'v list, 'm) gen_g_impl_scheme" definition frgv_impl_rel_ext_internal_def: "frgv_impl_rel_ext Rm Rv ≡ ⟨Rm,⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext" lemma frgv_impl_rel_ext_def: "⟨Rm,Rv⟩frgv_impl_rel_ext ≡ ⟨Rm,⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext" unfolding frgv_impl_rel_ext_internal_def relAPP_def by simp lemma [autoref_rel_intf]: "REL_INTF frgv_impl_rel_ext i_g_ext" by (rule REL_INTFI) lemma [relator_props, simp]: "⟦single_valued Rv; Range Rv = UNIV; single_valued Rm⟧ ⟹ single_valued (⟨Rm,Rv⟩frgv_impl_rel_ext)" unfolding frgv_impl_rel_ext_def by tagged_solver lemmas [param, autoref_rules] = gen_g_refine[where Rv = "⟨Rv⟩list_set_rel" and Re = "⟨Rv⟩slg_rel" and ?Rv0.0 = "⟨Rv⟩list_set_rel" for Rv, folded frgv_impl_rel_ext_def] subsubsection ‹Implementation with Cfun for Nodes› text ‹This implementation allows for the universal node set.› type_synonym ('v,'m) g_impl_scheme = "('v ⇒ bool, 'v ⇒ 'v list, 'v list, 'm) gen_g_impl_scheme" definition g_impl_rel_ext_internal_def: "g_impl_rel_ext Rm Rv ≡ ⟨Rm,⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext" lemma g_impl_rel_ext_def: "⟨Rm,Rv⟩g_impl_rel_ext ≡ ⟨Rm,⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext" unfolding g_impl_rel_ext_internal_def relAPP_def by simp lemma [autoref_rel_intf]: "REL_INTF g_impl_rel_ext i_g_ext" by (rule REL_INTFI) lemma [relator_props, simp]: "⟦single_valued Rv; Range Rv = UNIV; single_valued Rm⟧ ⟹ single_valued (⟨Rm,Rv⟩g_impl_rel_ext)" unfolding g_impl_rel_ext_def by tagged_solver lemmas [param, autoref_rules] = gen_g_refine[where Rv = "⟨Rv⟩fun_set_rel" and Re = "⟨Rv⟩slg_rel" and ?Rv0.0 = "⟨Rv⟩list_set_rel" for Rv, folded g_impl_rel_ext_def] lemma [autoref_rules]: "(gi_V_update, g_V_update) ∈ (⟨Rv⟩fun_set_rel → ⟨Rv⟩fun_set_rel) → ⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext" unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def by (auto, metis (full_types) tagged_fun_relD_both) lemma [autoref_rules]: "(gi_E_update, g_E_update) ∈ (⟨Rv⟩slg_rel → ⟨Rv⟩slg_rel) → ⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext" unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def by (auto, metis (full_types) tagged_fun_relD_both) lemma [autoref_rules]: "(gi_V0_update, g_V0_update) ∈ (⟨Rv⟩list_set_rel → ⟨Rv⟩list_set_rel) → ⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext" unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def by (auto, metis (full_types) tagged_fun_relD_both) (* HACK: The homgeneity rule heuristics erronously creates a homogeneity rule that equalizes Rv and Rv0, out of the frv-implementation, which happens to be the first. This declaration counters the undesired effects caused by this. *) lemma [autoref_hom]: "CONSTRAINT graph_rec_ext (⟨Rv⟩Rvs → ⟨Rv⟩Res → ⟨Rv⟩Rv0s → Rm → ⟨Rm,Rv⟩Rg)" by simp schematic_goal "(?c::?'c, λG x. g_E G  {x})∈?R" apply (autoref (keep_goal)) done schematic_goal "(?c,λV0 E. ⦇ g_V = UNIV, g_E = E, g_V0 = V0 ⦈ ) ∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → ⟨unit_rel,R⟩g_impl_rel_ext" apply (autoref (keep_goal)) done schematic_goal "(?c,λV V0 E. ⦇ g_V = V, g_E = E, g_V0 = V0 ⦈ ) ∈⟨R⟩list_set_rel → ⟨R⟩list_set_rel → ⟨R⟩slg_rel → ⟨unit_rel,R⟩frgv_impl_rel_ext" apply (autoref (keep_goal)) done subsubsection ‹Renaming› definition "the_inv_into_map V f x = (if x ∈ fV then Some (the_inv_into V f x) else None)" lemma the_inv_into_map_None[simp]: "the_inv_into_map V f x = None ⟷ x ∉ fV" unfolding the_inv_into_map_def by auto lemma the_inv_into_map_Some': "the_inv_into_map V f x = Some y ⟷ x ∈ fV ∧ y=the_inv_into V f x" unfolding the_inv_into_map_def by auto lemma the_inv_into_map_Some[simp]: "inj_on f V ⟹ the_inv_into_map V f x = Some y ⟷ y∈V ∧ x=f y" by (auto simp: the_inv_into_map_Some' the_inv_into_f_f) definition "the_inv_into_map_impl V f = FOREACH V (λx m. RETURN (m(f x ↦ x))) Map.empty" lemma the_inv_into_map_impl_correct: assumes [simp]: "finite V" assumes INJ: "inj_on f V" shows "the_inv_into_map_impl V f ≤ SPEC (λr. r = the_inv_into_map V f)" unfolding the_inv_into_map_impl_def apply (refine_rcg FOREACH_rule[where I="λit m. m=the_inv_into_map (V - it) f"] refine_vcg ) apply (vc_solve simp: the_inv_into_map_def[abs_def] it_step_insert_iff intro!: ext) apply (intro allI impI conjI) apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) [] apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) [] apply safe [] apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], (auto) [2])+ apply simp done schematic_goal the_inv_into_map_code_aux: fixes Rv' :: "('vti × 'vt) set" assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc" assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) (def_size)" assumes [autoref_rules]: "(Vi,V)∈⟨Rv⟩list_set_rel" assumes [autoref_rules]: "(fi,f)∈Rv→Rv'" shows "(RETURN ?c, the_inv_into_map_impl V f) ∈ ⟨⟨Rv',Rv⟩ahm_rel bhc⟩nres_rel" unfolding the_inv_into_map_impl_def[abs_def] apply (autoref_monadic (plain)) done concrete_definition the_inv_into_map_code uses the_inv_into_map_code_aux export_code the_inv_into_map_code checking SML thm the_inv_into_map_code.refine context begin interpretation autoref_syn . lemma autoref_the_inv_into_map[autoref_rules]: fixes Rv' :: "('vti × 'vt) set" assumes "SIDE_GEN_ALGO (is_bounded_hashcode Rv' eq bhc)" assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vti) def_size)" assumes INJ: "SIDE_PRECOND (inj_on f V)" assumes V: "(Vi,V)∈⟨Rv⟩list_set_rel" assumes F: "(fi,f)∈Rv→Rv'" shows "(the_inv_into_map_code eq bhc def_size Vi fi, (OP the_inv_into_map ::: ⟨Rv⟩list_set_rel → (Rv→Rv') → ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc)$V\$f) ∈ ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc"
proof simp

from V have FIN: "finite V" using list_set_rel_range by auto

note the_inv_into_map_code.refine[
OF assms(1-2,4-5)[unfolded autoref_tag_defs], THEN nres_relD
]
also note the_inv_into_map_impl_correct[OF FIN INJ[unfolded autoref_tag_defs]]
finally show "(the_inv_into_map_code eq bhc def_size Vi fi, the_inv_into_map V f)
∈ ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc"
qed

end

schematic_goal "(?c::?'c, do {
let s = {1,2,3::nat};
⌦‹ASSERT (inj_on Suc s);›
RETURN (the_inv_into_map s Suc) }) ∈ ?R"
apply (autoref (keep_goal))
done

definition "fr_rename_ext_aimpl ecnv f G ≡ do {
ASSERT (inj_on f (g_V G));
ASSERT (inj_on f (g_V0 G));
let fi_map = the_inv_into_map (g_V G) f;
e ← ecnv fi_map G;
RETURN ⦇
g_V = f(g_V G),
g_E = (E_of_succ (λv. case fi_map v of
Some u ⇒ f  (succ_of_E (g_E G) u) | None ⇒ {})),
g_V0 = (fg_V0 G),
… = e
⦈
}"

context g_rename_precond begin

definition "fi_map x = (if x ∈ fV then Some (fi x) else None)"
lemma fi_map_alt: "fi_map = the_inv_into_map V f"
apply (rule ext)
unfolding fi_map_def the_inv_into_map_def fi_def
by simp

lemma fi_map_Some: "(fi_map u = Some v) ⟷ u∈fV ∧ fi u = v"
unfolding fi_map_def by (auto split: if_split_asm)

lemma fi_map_None: "(fi_map u = None) ⟷ u∉fV"
unfolding fi_map_def by (auto split: if_split_asm)

lemma rename_E_aimpl_alt: "rename_E f E = E_of_succ (λv. case fi_map v of
Some u ⇒ f  (succ_of_E E u) | None ⇒ {})"
unfolding E_of_succ_def succ_of_E_def
using E_ss
by (force
simp: fi_f f_fi fi_map_Some fi_map_None
split: if_split_asm option.splits)

lemma frv_rename_ext_aimpl_alt:
assumes ECNV: "ecnv' fi_map G ≤ SPEC (λr. r = ecnv G)"
shows "fr_rename_ext_aimpl ecnv' f G
≤ SPEC (λr. r = fr_rename_ext ecnv f G)"
proof -
(*have [simp]: "⦇ g_E =
E_of_succ
(λv. case the_inv_into_map V f v of None ⇒ {}
| Some u ⇒ f  succ_of_E (g_E G) u),
g_V0 = f  g_V0 G, … = ecnv Gv⦈
= frv_G (frv_rename_ext ecnv f Gv)"
unfolding frv_rename_ext_def
by (auto simp: rename_E_aimpl_alt fi_map_alt)

have [simp]: "⦇frv_V = f  V, frv_G = frv_G Gv'⦈ = Gv'"
unfolding frv_rename_ext_def
by simp*)

show ?thesis
unfolding fr_rename_ext_def fr_rename_ext_aimpl_def
apply (refine_rcg
order_trans[OF ECNV[unfolded fi_map_alt]]
refine_vcg)
using subset_inj_on[OF _ V0_ss]
apply (auto intro: INJ simp: rename_E_aimpl_alt fi_map_alt)
done
qed
end

term frv_rename_ext_aimpl
schematic_goal fr_rename_ext_impl_aux:
fixes Re and Rv' :: "('vti × 'vt) set"
assumes [autoref_rules]: "(eq, (=)) ∈ Rv' → Rv' → bool_rel"
assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) def_size"
shows "(?c,fr_rename_ext_aimpl) ∈
((⟨Rv',Rv⟩ahm_rel bhc) → ⟨Re,Rv⟩frgv_impl_rel_ext → ⟨Re'⟩nres_rel) →
(Rv→Rv') →
⟨Re,Rv⟩frgv_impl_rel_ext →
⟨⟨Re',Rv'⟩frgv_impl_rel_ext⟩nres_rel"
unfolding fr_rename_ext_aimpl_def[abs_def]
apply (autoref (keep_goal))
done

concrete_definition fr_rename_ext_impl uses fr_rename_ext_impl_aux

thm fr_rename_ext_impl.refine[OF GEN_OP_D SIDE_GEN_ALGO_D SIDE_GEN_ALGO_D]

subsection ‹Graphs from Lists›

definition succ_of_list :: "(nat×nat) list ⇒ nat ⇒ nat set"
where
"succ_of_list l ≡ let
m = fold (λ(u,v) g.
case g u of
None ⇒ g(u↦{v})
| Some s ⇒ g(u↦insert v s)
) l Map.empty
in
(λu. case m u of None ⇒ {} | Some s ⇒ s)"

lemma succ_of_list_correct_aux:
"(succ_of_list l, set l) ∈ br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"
proof -

term the_default

{ fix m
have "fold (λ(u,v) g.
case g u of
None ⇒ g(u↦{v})
| Some s ⇒ g(u↦insert v s)
) l m
= (λu. let s=set l  {u} in
if s={} then m u else Some (the_default {} (m u) ∪ s))"
apply (induction l arbitrary: m)
apply (auto
split: option.split if_split
simp: Let_def Image_def
intro!: ext)
done
} note aux=this

show ?thesis
unfolding succ_of_list_def aux
by (auto simp: br_def Let_def split: option.splits if_split_asm)
qed

schematic_goal succ_of_list_impl:
notes [autoref_tyrel] =
ty_REL[where 'a="nat⇀nat set" and R="⟨nat_rel,R⟩iam_map_rel" for R]
ty_REL[where 'a="nat set" and R="⟨nat_rel⟩list_set_rel"]

shows "(?f::?'c,succ_of_list) ∈ ?R"
unfolding succ_of_list_def[abs_def]
apply (autoref (keep_goal))
done

concrete_definition succ_of_list_impl uses succ_of_list_impl
export_code succ_of_list_impl in SML

lemma succ_of_list_impl_correct: "(succ_of_list_impl,set) ∈ Id → ⟨Id⟩slg_rel"
apply rule
unfolding slg_rel_def
apply rule
apply (rule succ_of_list_impl.refine[THEN fun_relD])
apply simp
apply (rule succ_of_list_correct_aux)
done

end



# Theory Automata_Impl

section ‹Implementing Automata›
(* Author: Peter Lammich *)
theory Automata_Impl
imports Digraph_Impl Automata
begin

subsection ‹Indexed Generalized Buchi Graphs›

consts
i_igbg_eext :: "interface ⇒ interface ⇒ interface"

abbreviation "i_igbg Ie Iv ≡ ⟨⟨Ie,Iv⟩⇩ii_igbg_eext,Iv⟩⇩ii_g_ext"

context begin interpretation autoref_syn .

lemma igbg_type[autoref_itype]:
"igbg_num_acc ::⇩i i_igbg Ie Iv →⇩i i_nat"
"igbg_acc ::⇩i i_igbg Ie Iv →⇩i Iv →⇩i ⟨i_nat⟩⇩ii_set"
"igb_graph_rec_ext
::⇩i i_nat →⇩i (Iv →⇩i ⟨i_nat⟩⇩ii_set) →⇩i Ie →⇩i ⟨Ie,Iv⟩⇩ii_igbg_eext"
by simp_all
end

record ('vi,'ei,'v0i,'acci) gen_igbg_impl = "('vi,'ei,'v0i) gen_g_impl" +
igbgi_num_acc :: nat
igbgi_acc :: 'acci

definition gen_igbg_impl_rel_eext_def_internal:
"gen_igbg_impl_rel_eext Rm Racc ≡ { (
⦇ igbgi_num_acc = num_acci, igbgi_acc = acci, …=mi ⦈,
⦇ igbg_num_acc = num_acc, igbg_acc = acc, …=m ⦈)
| num_acci acci mi num_acc acc m.
(num_acci,num_acc)∈nat_rel
∧ (acci,acc)∈Racc
∧ (mi,m)∈Rm
}"

lemma gen_igbg_impl_rel_eext_def:
"⟨Rm,Racc⟩gen_igbg_impl_rel_eext = { (
⦇ igbgi_num_acc = num_acci, igbgi_acc = acci, …=mi ⦈,
⦇ igbg_num_acc = num_acc, igbg_acc = acc, …=m ⦈)
| num_acci acci mi num_acc acc m.
(num_acci,num_acc)∈nat_rel
∧ (acci,acc)∈Racc
∧ (mi,m)∈Rm
}"
unfolding gen_igbg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_igbg_impl_rel_sv[relator_props]:
"⟦single_valued Racc; single_valued Rm⟧
⟹ single_valued (⟨Rm,Racc⟩gen_igbg_impl_rel_eext)"
unfolding gen_igbg_impl_rel_eext_def
apply (rule single_valuedI)
apply (clarsimp)
apply (intro conjI)
apply (rule single_valuedD[rotated], assumption+)
apply (rule single_valuedD[rotated], assumption+)
done

abbreviation gen_igbg_impl_rel_ext
:: "_ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ (_×(_,_)igb_graph_rec_scheme) set"
where "gen_igbg_impl_rel_ext Rm Racc
≡ ⟨⟨Rm,Racc⟩gen_igbg_impl_rel_eext⟩gen_g_impl_rel_ext "

lemma gen_igbg_refine:
fixes Rv Re Rv0 Racc
assumes "TERM (Rv,Re,Rv0)"
assumes "TERM (Racc)"
shows
"(igbgi_num_acc,igbg_num_acc)
∈ ⟨Rv,Re,Rv0⟩gen_igbg_impl_rel_ext Rm Racc → nat_rel"
"(igbgi_acc,igbg_acc)
∈ ⟨Rv,Re,Rv0⟩gen_igbg_impl_rel_ext Rm Racc → Racc"
"(gen_igbg_impl_ext, igb_graph_rec_ext)
∈ nat_rel → Racc → Rm → ⟨Rm,Racc⟩gen_igbg_impl_rel_eext"
unfolding gen_igbg_impl_rel_eext_def gen_g_impl_rel_ext_def
by auto

subsubsection ‹Implementation with bit-set›

definition igbg_impl_rel_eext_internal_def:
"igbg_impl_rel_eext Rm Rv ≡ ⟨Rm, Rv → ⟨nat_rel⟩bs_set_rel⟩gen_igbg_impl_rel_eext"

lemma igbg_impl_rel_eext_def:
"⟨Rm,Rv⟩igbg_impl_rel_eext ≡ ⟨Rm, Rv → ⟨nat_rel⟩bs_set_rel⟩gen_igbg_impl_rel_eext"
unfolding igbg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of igbg_impl_rel_eext i_igbg_eext]

lemma [relator_props, simp]:
"⟦Range Rv = UNIV; single_valued Rm⟧
⟹ single_valued (⟨Rm,Rv⟩igbg_impl_rel_eext)"
unfolding igbg_impl_rel_eext_def by tagged_solver

lemma g_tag: "TERM (⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel)" .
lemma frgv_tag: "TERM (⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel)" .
lemma igbg_bs_tag: "TERM (Rv → ⟨nat_rel⟩bs_set_rel)" .

abbreviation "igbgv_impl_rel_ext Rm Rv
≡ ⟨⟨Rm, Rv⟩igbg_impl_rel_eext, Rv⟩frgv_impl_rel_ext"

abbreviation "igbg_impl_rel_ext Rm Rv
≡ ⟨⟨Rm, Rv⟩igbg_impl_rel_eext, Rv⟩g_impl_rel_ext"

type_synonym ('v,'m) igbgv_impl_scheme =
"('v, ⦇ igbgi_num_acc::nat, igbgi_acc::'v⇒integer, …::'m  ⦈)
frgv_impl_scheme"
type_synonym ('v,'m) igbg_impl_scheme =
"('v, ⦇ igbgi_num_acc::nat, igbgi_acc::'v⇒integer, …::'m  ⦈)
g_impl_scheme"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_igbg_refine[
OF frgv_tag[of Rv] igbg_bs_tag[of Rv],
folded frgv_impl_rel_ext_def igbg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_igbg_refine[
OF g_tag[of Rv] igbg_bs_tag[of Rv],
folded g_impl_rel_ext_def igbg_impl_rel_eext_def]
end

schematic_goal "(?c::?'c,
λG x. if igbg_num_acc G = 0 ∧ 1∈igbg_acc G x then (g_E G  {x}) else {}
)∈?R"
apply (autoref (keep_goal))
done

schematic_goal "(?c,
λV0 E num_acc acc.
⦇ g_V = UNIV, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc ⦈
)∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → nat_rel → (R → ⟨nat_rel⟩bs_set_rel)
→ igbg_impl_rel_ext unit_rel R"
apply (autoref (keep_goal))
done

schematic_goal "(?c,
λV0 E num_acc acc.
⦇ g_V = {}, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc ⦈
)∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → nat_rel → (R → ⟨nat_rel⟩bs_set_rel)
→ igbgv_impl_rel_ext unit_rel R"
apply (autoref (keep_goal))
done

subsection ‹Indexed Generalized Buchi Automata›

consts
i_igba_eext :: "interface ⇒ interface ⇒ interface ⇒ interface"

abbreviation "i_igba Ie Iv Il
≡ ⟨⟨⟨Ie,Iv,Il⟩⇩ii_igba_eext,Iv⟩⇩ii_igbg_eext,Iv⟩⇩ii_g_ext"
context begin interpretation autoref_syn .

lemma igba_type[autoref_itype]:
"igba_L ::⇩i i_igba Ie Iv Il →⇩i (Iv →⇩i Il →⇩i i_bool)"
"igba_rec_ext ::⇩i (Iv →⇩i Il →⇩i i_bool) →⇩i Ie →⇩i ⟨Ie,Iv,Il⟩⇩ii_igba_eext"
by simp_all
end

record ('vi,'ei,'v0i,'acci,'Li) gen_igba_impl =
"('vi,'ei,'v0i,'acci)gen_igbg_impl" +
igbai_L :: "'Li"

definition gen_igba_impl_rel_eext_def_internal:
"gen_igba_impl_rel_eext Rm Rl  ≡ { (
⦇ igbai_L = Li, …=mi ⦈,
⦇ igba_L = L, …=m ⦈)
| Li mi L m.
(Li,L)∈Rl
∧ (mi,m)∈Rm
}"

lemma gen_igba_impl_rel_eext_def:
"⟨Rm,Rl⟩gen_igba_impl_rel_eext = { (
⦇ igbai_L = Li, …=mi ⦈,
⦇ igba_L = L, …=m ⦈)
| Li mi L m.
(Li,L)∈Rl
∧ (mi,m)∈Rm
}"
unfolding gen_igba_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_igba_impl_rel_sv[relator_props]:
"⟦single_valued Rl; single_valued Rm⟧
⟹ single_valued (⟨Rm,Rl⟩gen_igba_impl_rel_eext)"
unfolding gen_igba_impl_rel_eext_def
apply (rule single_valuedI)
apply (clarsimp)
apply (intro conjI)
apply (rule single_valuedD[rotated], assumption+)
apply (rule single_valuedD[rotated], assumption+)
done

abbreviation gen_igba_impl_rel_ext
:: "_ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ (_ × ('a,'b,'c) igba_rec_scheme) set"
where "gen_igba_impl_rel_ext Rm Rl
≡ gen_igbg_impl_rel_ext (⟨Rm,Rl⟩gen_igba_impl_rel_eext)"

lemma gen_igba_refine:
fixes Rv Re Rv0 Racc Rl
assumes "TERM (Rv,Re,Rv0)"
assumes "TERM (Racc)"
assumes "TERM (Rl)"
shows
"(igbai_L,igba_L)
∈ ⟨Rv,Re,Rv0⟩gen_igba_impl_rel_ext Rm Rl Racc → Rl"
"(gen_igba_impl_ext, igba_rec_ext)
∈ Rl → Rm → ⟨Rm,Rl⟩gen_igba_impl_rel_eext"
unfolding gen_igba_impl_rel_eext_def gen_igbg_impl_rel_eext_def
gen_g_impl_rel_ext_def
by auto

subsubsection ‹Implementation as function›
definition igba_impl_rel_eext_internal_def:
"igba_impl_rel_eext Rm Rv Rl ≡ ⟨Rm, Rv → Rl → bool_rel⟩gen_igba_impl_rel_eext"

lemma igba_impl_rel_eext_def:
"⟨Rm,Rv,Rl⟩igba_impl_rel_eext ≡ ⟨Rm, Rv → Rl → bool_rel⟩gen_igba_impl_rel_eext"
unfolding igba_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of igba_impl_rel_eext i_igba_eext]

lemma [relator_props, simp]:
"⟦Range Rv = UNIV; single_valued Rm; Range Rl = UNIV⟧
⟹ single_valued (⟨Rm,Rv,Rl⟩igba_impl_rel_eext)"
unfolding igba_impl_rel_eext_def by tagged_solver

lemma igba_f_tag: "TERM (Rv → Rl → bool_rel)" .

abbreviation "igbav_impl_rel_ext Rm Rv Rl
≡ igbgv_impl_rel_ext (⟨Rm, Rv, Rl⟩igba_impl_rel_eext) Rv"

abbreviation "igba_impl_rel_ext Rm Rv Rl
≡ igbg_impl_rel_ext (⟨Rm, Rv, Rl⟩igba_impl_rel_eext) Rv"

type_synonym ('v,'l,'m) igbav_impl_scheme =
"('v, ⦇ igbai_L :: 'v ⇒ 'l ⇒ bool , …::'m  ⦈)
igbgv_impl_scheme"

type_synonym ('v,'l,'m) igba_impl_scheme =
"('v, ⦇ igbai_L :: 'v ⇒ 'l ⇒ bool , …::'m  ⦈)
igbg_impl_scheme"

context
fixes Rv :: "('vi×'v) set"
fixes Rl :: "('Li×'l) set"
begin
lemmas [autoref_rules] = gen_igba_refine[
OF frgv_tag[of Rv] igbg_bs_tag[of Rv] igba_f_tag[of Rv Rl],
folded frgv_impl_rel_ext_def igbg_impl_rel_eext_def igba_impl_rel_eext_def]

lemmas [autoref_rules] = gen_igba_refine[
OF g_tag[of Rv] igbg_bs_tag[of Rv] igba_f_tag[of Rv Rl],
folded g_impl_rel_ext_def igbg_impl_rel_eext_def igba_impl_rel_eext_def]
end

thm autoref_itype

schematic_goal
"(?c::?'c, λG x l. if igba_L G x l then (g_E G  {x}) else {} )∈?R"
apply (autoref (keep_goal))
done

schematic_goal
notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
shows "(?c::?'c, λE (V0::'a set) num_acc acc L.
⦇ g_V = UNIV, g_E = E, g_V0 = V0,
igbg_num_acc = num_acc, igbg_acc = acc, igba_L = L ⦈
)∈?R"
apply (autoref (keep_goal))
done

schematic_goal
notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
shows "(?c::?'c, λE (V0::'a set) num_acc acc L.
⦇ g_V = V0, g_E = E, g_V0 = V0,
igbg_num_acc = num_acc, igbg_acc = acc, igba_L = L ⦈
)∈?R"
apply (autoref (keep_goal))
done

subsection ‹Generalized Buchi Graphs›

consts
i_gbg_eext :: "interface ⇒ interface ⇒ interface"

abbreviation "i_gbg Ie Iv ≡ ⟨⟨Ie,Iv⟩⇩ii_gbg_eext,Iv⟩⇩ii_g_ext"

context begin interpretation autoref_syn .

lemma gbg_type[autoref_itype]:
"gbg_F ::⇩i i_gbg Ie Iv →⇩i ⟨⟨Iv⟩⇩ii_set⟩⇩ii_set"
"gb_graph_rec_ext ::⇩i ⟨⟨Iv⟩⇩ii_set⟩⇩ii_set →⇩i Ie →⇩i ⟨Ie,Iv⟩⇩ii_gbg_eext"
by simp_all
end

record ('vi,'ei,'v0i,'fi) gen_gbg_impl = "('vi,'ei,'v0i) gen_g_impl" +
gbgi_F :: 'fi

definition gen_gbg_impl_rel_eext_def_internal:
"gen_gbg_impl_rel_eext Rm Rf ≡ { (
⦇ gbgi_F = Fi, …=mi ⦈,
⦇ gbg_F = F, …=m ⦈)
| Fi mi F m.
(Fi,F)∈Rf
∧ (mi,m)∈Rm
}"

lemma gen_gbg_impl_rel_eext_def:
"⟨Rm,Rf⟩gen_gbg_impl_rel_eext = { (
⦇ gbgi_F = Fi, …=mi ⦈,
⦇ gbg_F = F, …=m ⦈)
| Fi mi F m.
(Fi,F)∈Rf
∧ (mi,m)∈Rm
}"
unfolding gen_gbg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_gbg_impl_rel_sv[relator_props]:
"⟦single_valued Rm; single_valued Rf⟧
⟹ single_valued (⟨Rm,Rf⟩gen_gbg_impl_rel_eext)"
unfolding gen_gbg_impl_rel_eext_def
apply (rule single_valuedI)
apply (clarsimp)
apply (intro conjI)
apply (rule single_valuedD[rotated], assumption+)
apply (rule single_valuedD[rotated], assumption+)
done

abbreviation gen_gbg_impl_rel_ext
:: "_ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ (_ × ('q,_) gb_graph_rec_scheme) set"
where "gen_gbg_impl_rel_ext Rm Rf
≡ ⟨⟨Rm,Rf⟩gen_gbg_impl_rel_eext⟩gen_g_impl_rel_ext"

lemma gen_gbg_refine:
fixes Rv Re Rv0 Rf
assumes "TERM (Rv,Re,Rv0)"
assumes "TERM (Rf)"
shows
"(gbgi_F,gbg_F)
∈ ⟨Rv,Re,Rv0⟩gen_gbg_impl_rel_ext Rm Rf → Rf"
"(gen_gbg_impl_ext, gb_graph_rec_ext)
∈ Rf → Rm → ⟨Rm,Rf⟩gen_gbg_impl_rel_eext"
unfolding gen_gbg_impl_rel_eext_def gen_g_impl_rel_ext_def
by auto

subsubsection ‹Implementation with list of lists›

definition gbg_impl_rel_eext_internal_def:
"gbg_impl_rel_eext Rm Rv
≡ ⟨Rm, ⟨⟨Rv⟩list_set_rel⟩list_set_rel⟩gen_gbg_impl_rel_eext"

lemma gbg_impl_rel_eext_def:
"⟨Rm,Rv⟩gbg_impl_rel_eext
≡ ⟨Rm, ⟨⟨Rv⟩list_set_rel⟩list_set_rel⟩gen_gbg_impl_rel_eext"
unfolding gbg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of gbg_impl_rel_eext i_gbg_eext]

lemma [relator_props, simp]:
"⟦single_valued Rm; single_valued Rv⟧
⟹ single_valued (⟨Rm,Rv⟩gbg_impl_rel_eext)"
unfolding gbg_impl_rel_eext_def by tagged_solver

lemma gbg_ls_tag: "TERM (⟨⟨Rv⟩list_set_rel⟩list_set_rel)" .

abbreviation "gbgv_impl_rel_ext Rm Rv
≡ ⟨⟨Rm, Rv⟩gbg_impl_rel_eext, Rv⟩frgv_impl_rel_ext"

abbreviation "gbg_impl_rel_ext Rm Rv
≡ ⟨⟨Rm, Rv⟩gbg_impl_rel_eext, Rv⟩g_impl_rel_ext"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_gbg_refine[
OF frgv_tag[of Rv] gbg_ls_tag[of Rv],
folded frgv_impl_rel_ext_def gbg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_gbg_refine[
OF g_tag[of Rv] gbg_ls_tag[of Rv],
folded g_impl_rel_ext_def gbg_impl_rel_eext_def]
end

schematic_goal "(?c::?'c,
λG x. if gbg_F G = {} then (g_E G  {x}) else {}
)∈?R"
apply (autoref (keep_goal))
done

schematic_goal
notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
shows "(?c::?'c, λE (V0::'a set) F.
⦇ g_V = {}, g_E = E, g_V0 = V0, gbg_F = F ⦈)∈?R"
apply (autoref (keep_goal))
done

schematic_goal
notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
shows "(?c::?'c, λE (V0::'a set) F.
⦇ g_V = UNIV, g_E = E, g_V0 = V0, gbg_F = insert {} F ⦈)∈?R"
apply (autoref (keep_goal))
done

schematic_goal "(?c::?'c, it_to_sorted_list (λ_ _. True) {1,2::nat} )∈?R"
apply (autoref (keep_goal))
done

subsection ‹GBAs›

consts
i_gba_eext :: "interface ⇒ interface ⇒ interface ⇒ interface"

abbreviation "i_gba Ie Iv Il
≡ ⟨⟨⟨Ie,Iv,Il⟩⇩ii_gba_eext,Iv⟩⇩ii_gbg_eext,Iv⟩⇩ii_g_ext"
context begin interpretation autoref_syn .

lemma gba_type[autoref_itype]:
"gba_L ::⇩i i_gba Ie Iv Il →⇩i (Iv →⇩i Il →⇩i i_bool)"
"gba_rec_ext ::⇩i (Iv →⇩i Il →⇩i i_bool) →⇩i Ie →⇩i ⟨Ie,Iv,Il⟩⇩ii_gba_eext"
by simp_all
end

record ('vi,'ei,'v0i,'acci,'Li) gen_gba_impl =
"('vi,'ei,'v0i,'acci)gen_gbg_impl" +
gbai_L :: "'Li"

definition gen_gba_impl_rel_eext_def_internal:
"gen_gba_impl_rel_eext Rm Rl  ≡ { (
⦇ gbai_L = Li, …=mi ⦈,
⦇ gba_L = L, …=m ⦈)
| Li mi L m.
(Li,L)∈Rl
∧ (mi,m)∈Rm
}"

lemma gen_gba_impl_rel_eext_def:
"⟨Rm,Rl⟩gen_gba_impl_rel_eext = { (
⦇ gbai_L = Li, …=mi ⦈,
⦇ gba_L = L, …=m ⦈)
| Li mi L m.
(Li,L)∈Rl
∧ (mi,m)∈Rm
}"
unfolding gen_gba_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_gba_impl_rel_sv[relator_props]:
"⟦single_valued Rl; single_valued Rm⟧
⟹ single_valued (⟨Rm,Rl⟩gen_gba_impl_rel_eext)"
unfolding gen_gba_impl_rel_eext_def
apply (rule single_valuedI)
apply (clarsimp)
apply (intro conjI)
apply (rule single_valuedD[rotated], assumption+)
apply (rule single_valuedD[rotated], assumption+)
done

abbreviation gen_gba_impl_rel_ext
:: "_ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ (_ × ('a,'b,'c) gba_rec_scheme) set"
where "gen_gba_impl_rel_ext Rm Rl
≡ gen_gbg_impl_rel_ext (⟨Rm,Rl⟩gen_gba_impl_rel_eext)"

lemma gen_gba_refine:
fixes Rv Re Rv0 Racc Rl
assumes "TERM (Rv,Re,Rv0)"
assumes "TERM (Racc)"
assumes "TERM (Rl)"
shows
"(gbai_L,gba_L)
∈ ⟨Rv,Re,Rv0⟩gen_gba_impl_rel_ext Rm Rl Racc → Rl"
"(gen_gba_impl_ext, gba_rec_ext)
∈ Rl → Rm → ⟨Rm,Rl⟩gen_gba_impl_rel_eext"
unfolding gen_gba_impl_rel_eext_def gen_gbg_impl_rel_eext_def
gen_g_impl_rel_ext_def
by auto

subsubsection ‹Implementation as function›
definition gba_impl_rel_eext_internal_def:
"gba_impl_rel_eext Rm Rv Rl ≡ ⟨Rm, Rv → Rl → bool_rel⟩gen_gba_impl_rel_eext"

lemma gba_impl_rel_eext_def:
"⟨Rm,Rv,Rl⟩gba_impl_rel_eext ≡ ⟨Rm, Rv → Rl → bool_rel⟩gen_gba_impl_rel_eext"
unfolding gba_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of gba_impl_rel_eext i_gba_eext]

lemma [relator_props, simp]:
"⟦Range Rv = UNIV; single_valued Rm; Range Rl = UNIV⟧
⟹ single_valued (⟨Rm,Rv,Rl⟩gba_impl_rel_eext)"
unfolding gba_impl_rel_eext_def by tagged_solver

lemma gba_f_tag: "TERM (Rv → Rl → bool_rel)" .

abbreviation "gbav_impl_rel_ext Rm Rv Rl
≡ gbgv_impl_rel_ext (⟨Rm, Rv, Rl⟩gba_impl_rel_eext) Rv"

abbreviation "gba_impl_rel_ext Rm Rv Rl
≡ gbg_impl_rel_ext (⟨Rm, Rv, Rl⟩gba_impl_rel_eext) Rv"

context
fixes Rv :: "('vi×'v) set"
fixes Rl :: "('Li×'l) set"
begin
lemmas [autoref_rules] = gen_gba_refine[
OF frgv_tag[of Rv] gbg_ls_tag[of Rv] gba_f_tag[of Rv Rl],
folded frgv_impl_rel_ext_def gbg_impl_rel_eext_def gba_impl_rel_eext_def]

lemmas [autoref_rules] = gen_gba_refine[
OF g_tag[of Rv] gbg_ls_tag[of Rv] gba_f_tag[of Rv Rl],
folded g_impl_rel_ext_def gbg_impl_rel_eext_def gba_impl_rel_eext_def]
end

thm autoref_itype

schematic_goal
"(?c::?'c, λG x l. if gba_L G x l then (g_E G  {x}) else {} )∈?R"
apply (autoref (keep_goal))
done

schematic_goal
notes [autoref_tyrel] =