# Theory AbsAlgo

theory AbsAlgo
imports Ta Exploration CollectionsV1
(*  Title:       Tree Automata
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section "Abstract Tree Automata Algorithms"
theory AbsAlgo
imports
Ta
Collections_Examples.Exploration
Collections.CollectionsV1
begin

no_notation fun_rel_syn (infixr "→" 60)

text_raw ‹\label{sec:absalgo}›
text ‹This theory defines tree automata algorithms on an abstract level,
that is using non-executable datatypes and constructs like sets,
set-collecting operations, etc.

These algorithms are then refined to executable algorithms in
Section~\ref{sec:taimpl}.
›

subsection ‹Word Problem›

text ‹
First, a recursive version of the @{const accs}-predicate is defined.
›

fun r_match :: "'a set list ⇒ 'a list ⇒ bool" where
"r_match [] [] ⟷ True" |
"r_match (A#AS) (a#as) ⟷ a∈A ∧ r_match AS as" |
"r_match _ _ ⟷ False"

― ‹@{const r_match} accepts two lists, if they have the same length and
the elements in the second list are contained in the respective
elements of the first list:›
lemma r_match_alt:
"r_match L l ⟷ length L = length l ∧ (∀i<length l. l!i ∈ L!i)"
apply (induct L l rule: r_match.induct)
apply auto
apply (case_tac i)
apply auto
done

― ‹Whether a rule matches the given state, label and list of sets of states›
fun r_matchc where
"r_matchc q l Qs (qr → lr qsr) ⟷ q=qr ∧ l=lr ∧ r_match Qs qsr"

― ‹recursive version of @{const accs}-predicate›
fun faccs :: "('Q,'L) ta_rule set ⇒ 'L tree ⇒ 'Q set" where
"faccs δ (NODE f ts) = (
let Qs = map (faccs δ) (ts) in
{q. ∃r∈δ. r_matchc q f Qs r }
)"

lemma faccs_correct_aux:
"q∈faccs δ n = accs δ n q" (is ?T1)
"(map (faccs δ) ts = map (λt. { q . accs δ t q}) ts)" (is ?T2)
proof -
have "(∀q. q∈faccs δ n = accs δ n q)
∧ (map (faccs δ) ts = map (λt. { q . accs δ t q}) ts)"
proof (induct rule: compat_tree_tree_list.induct)
case (NODE f ts)
thus ?case
apply (intro allI iffI)
apply simp
apply (erule bexE)
apply (case_tac x)
apply simp
apply (rule accs.intros)
apply assumption
apply (unfold r_match_alt)
apply simp
apply fastforce
apply simp
apply (erule accs.cases)
apply auto
apply (rule_tac x="qa → f qs" in bexI)
apply simp
apply (unfold r_match_alt)
apply auto
done
qed auto
thus ?T1 ?T2 by auto
qed

theorem faccs_correct1: "q∈faccs δ n ⟹ accs δ n q"
theorem faccs_correct2: "accs δ n q ⟹ q∈faccs δ n"

lemmas faccs_correct = faccs_correct1 faccs_correct2

lemma faccs_alt: "faccs δ t = {q. accs δ t q}" by (auto intro: faccs_correct)

subsection ‹Backward Reduction and Emptiness Check›
subsubsection "Auxiliary Definitions"

― ‹Step function, that maps a set of states to those states
that are reachable via one backward step.›
inductive_set bacc_step :: "('Q,'L) ta_rule set ⇒ 'Q set ⇒ 'Q set"
for δ Q
where
"⟦ r∈δ; set (rhsq r) ⊆ Q ⟧ ⟹ lhs r ∈ bacc_step δ Q"

― ‹If a set is closed under adding all states that are reachable from the set
by one backward step, then this set contains all backward accessible states.›
lemma b_accs_as_closed:
assumes A: "bacc_step δ Q ⊆ Q"
shows "b_accessible δ ⊆ Q"
proof (rule subsetI)
fix q
assume "q∈b_accessible δ"
thus "q∈Q"
proof (induct rule: b_accessible.induct)
fix q f qs
assume BC: "(q→f qs)∈δ"
"!!x. x∈set qs ⟹ x∈b_accessible δ"
"!!x. x∈set qs ⟹ x∈Q"
from bacc_step.intros[OF BC(1)] BC(3) have "q∈bacc_step δ Q" by auto
with A show "q∈Q" by blast
qed
qed

subsubsection "Algorithms"

text ‹
First, the basic workset algorithm is specified.
Then, it is refined to contain a counter for each rule,
that counts the number of undiscovered states on the RHS.
For both levels of abstraction, a version that computes the
backwards reduction, and a version that checks for emptiness is specified.

Additionally, a version of the algorithm that computes a witness
for non-emptiness is provided.

Levels of abstraction:
\begin{itemize}
\item[‹α›] On this level, the state consists of a set of
discovered states and a workset.
\item[‹α'›] On this level, the state consists of a set of
discovered states, a workset and a map from rules to number of
undiscovered rhs states. This map can be used to make the discovery of
rules that have to be considered more efficient.
\end{itemize}
›

text_raw ‹\paragraph {‹α› - Level:}›

― ‹A state contains the set of discovered states and a workset›
type_synonym ('Q,'L) br_state = "'Q set × 'Q set"

― ‹Set of states that are non-empty (accept a tree) after adding the
state $q$ to the set of discovered states›
definition br_dsq
:: "('Q,'L) ta_rule set ⇒ 'Q ⇒ ('Q,'L) br_state ⇒ 'Q set"
where
"br_dsq δ q == λ(Q,W). { lhs r | r. r∈δ ∧ set (rhsq r) ⊆ (Q-(W-{q})) }"

― ‹Description of a step: One state is removed from the workset, and all
new states that become non-empty due to this state are added to, both,
the workset and the set of discovered states›
inductive_set br_step
:: "('Q,'L) ta_rule set ⇒ (('Q,'L) br_state × ('Q,'L) br_state) set"
for δ where
"⟦
q∈W;
Q' = Q ∪ br_dsq δ q (Q,W);
W' = W - {q} ∪ (br_dsq δ q (Q,W) - Q)
⟧ ⟹ ((Q,W),(Q',W'))∈br_step δ"

― ‹Termination condition for backwards reduction: The workset is empty›
definition br_cond :: "('Q,'L) br_state set"
where "br_cond == {(Q,W). W≠{}}"

― ‹Termination condition for emptiness check:
The workset is empty or a non-empty initial state has been discovered›
definition bre_cond :: "'Q set ⇒ ('Q,'L) br_state set"
where "bre_cond Qi == {(Q,W). W≠{} ∧ (Qi∩Q={})}"

― ‹Set of all states that occur on the lhs of a constant-rule›
definition br_iq :: "('Q,'L) ta_rule set ⇒ 'Q set"
where "br_iq δ == { lhs r | r. r∈δ ∧ rhsq r = [] }"

― ‹Initial state for the iteration›
definition br_initial :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br_state"
where "br_initial δ == (br_iq δ, br_iq δ)"

― ‹Invariant for the iteration:
\begin{itemize}
\item States on the workset have been discovered
\item Only accessible states have been discovered
\item If a state is non-empty due to a rule whose
rhs-states have been discovered and processed
(i.e. are in $Q-W$), then the lhs state of the
rule has also been discovered.
\item The set of discovered states is finite
\end{itemize}›
definition br_invar :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br_state set"
where "br_invar δ == {(Q,W).
W⊆Q ∧
Q ⊆ b_accessible δ ∧
bacc_step δ (Q - W) ⊆ Q ∧
finite Q}"

definition "br_algo δ == ⦇
wa_cond = br_cond,
wa_step = br_step δ,
wa_initial = {br_initial δ},
wa_invar = br_invar δ
⦈"

definition "bre_algo Qi δ == ⦇
wa_cond = bre_cond Qi,
wa_step = br_step δ,
wa_initial = {br_initial δ},
wa_invar = br_invar δ
⦈"

― ‹Termination: Either a new state is added, or the workset decreases.›
definition "br_termrel δ ==
({(Q',Q). Q ⊂ Q' ∧ Q' ⊆ b_accessible δ}) <*lex*> finite_psubset"

lemma bre_cond_imp_br_cond[intro, simp]: "bre_cond Qi ⊆ br_cond"
by (auto simp add: br_cond_def bre_cond_def)

lemma br_termrel_wf[simp, intro!]: "finite δ ⟹ wf (br_termrel δ)"
apply (unfold br_termrel_def)
done

― ‹Only accessible states are discovered›
lemma br_dsq_ss:
assumes A: "(Q,W)∈br_invar δ" "W ≠ {}" "q∈W"
shows "br_dsq δ q (Q,W) ⊆ b_accessible δ"
proof (rule subsetI)
fix q'
assume B: "q'∈br_dsq δ q (Q,W)"
then obtain r where
R: "q' = lhs r" "r∈δ" and
S: "set (rhsq r) ⊆ (Q-(W-{q}))"
by (unfold br_dsq_def) auto
note S
also have "(Q-(W-{q})) ⊆ b_accessible δ" using A(1,3)
finally show "q'∈b_accessible δ" using R
by (cases r)
(auto intro: b_accessible.intros)
qed

lemma br_step_in_termrel:
assumes A: "Σ∈br_cond" "Σ∈br_invar δ" "(Σ,Σ')∈br_step δ"
shows "(Σ', Σ)∈br_termrel δ"
proof -
obtain Q W Q' W' where
[simp]: "Σ=(Q,W)" "Σ'=(Q',W')"
by (cases Σ, cases Σ', auto)
obtain q where
QIW: "q∈W" and
ASSFMT[simp]: "Q' = Q ∪ br_dsq δ q (Q, W)"
"W' = W - {q} ∪ (br_dsq δ q (Q, W) - Q)"
by (auto intro: br_step.cases[OF A(3)[simplified]])

from A(2) have [simp]: "finite Q"
from A(2)[unfolded br_invar_def] have [simp]: "finite W"
from A(1) have WNE: "W≠{}" by (unfold br_cond_def) auto

note DSQSS = br_dsq_ss[OF A(2)[simplified] WNE QIW]
{
assume "br_dsq δ q (Q,W) - Q = {}"
hence ?thesis using QIW
} moreover {
assume "br_dsq δ q (Q,W) - Q ≠ {}"
hence "Q ⊂ Q'" by auto
moreover from DSQSS A(2)[unfolded br_invar_def] have
"Q' ⊆ b_accessible δ"
by auto
ultimately have ?thesis
} ultimately show ?thesis by blast
qed

lemma br_invar_initial[simp]: "finite δ ⟹ (br_initial δ)∈br_invar δ"
apply (auto simp add: br_initial_def br_invar_def br_iq_def)

apply (case_tac r)
apply (fastforce intro: b_accessible.intros)
apply (fastforce elim!: bacc_step.cases)
done

lemma br_invar_step:
assumes [simp]: "finite δ"
assumes A: "Σ∈br_cond" "Σ∈br_invar δ" "(Σ,Σ')∈br_step δ"
shows "Σ'∈br_invar δ"
proof -
obtain Q W Q' W' where SF[simp]: "Σ=(Q,W)" "Σ'=(Q',W')"
by (cases Σ, cases Σ', auto)
obtain q where
QIW: "q∈W" and
ASSFMT[simp]: "Q' = Q ∪ br_dsq δ q (Q, W)"
"W' = W - {q} ∪ (br_dsq δ q (Q, W) - Q)"
by (auto intro: br_step.cases[OF A(3)[simplified]])

from A(1) have WNE: "W≠{}" by (unfold br_cond_def) auto

have DSQSS: "br_dsq δ q (Q,W) ⊆ b_accessible δ"
using br_dsq_ss[OF A(2)[simplified] WNE QIW] .

show ?thesis
apply (simp add: br_invar_def del: ASSFMT)
proof (intro conjI)
from A(2) have "W ⊆ Q" by (simp add: br_invar_def)
thus "W' ⊆ Q'" by auto
next
from A(2) have "Q ⊆ b_accessible δ" by (simp add: br_invar_def)
with DSQSS show "Q' ⊆ b_accessible δ" by auto
next
show "bacc_step δ (Q' - W') ⊆ Q'"
apply (rule subsetI)
apply (erule bacc_step.cases)
done
next
show "finite Q'" using A(2) by (simp add: br_invar_def br_dsq_def)
qed
qed

lemma br_invar_final:
"∀Σ. Σ∈wa_invar (br_algo δ) ∧ Σ∉wa_cond (br_algo δ)
⟶ fst Σ = b_accessible δ"
apply (simp add: br_invar_def br_cond_def br_algo_def)
apply (auto intro: rev_subsetD[OF _ b_accs_as_closed])
done
(*  shows "⟦(Q,W)∈br_invar δ; (Q,W)∉br_cond⟧ ⟹ Q = b_accessible δ"
apply (auto intro: rev_subsetD[OF _ b_accs_as_closed])
done*)

theorem br_while_algo:
assumes FIN[simp]: "finite δ"
shows "while_algo (br_algo δ)"
apply (unfold_locales)
apply (simp_all add: br_algo_def br_invar_step br_invar_initial
br_step_in_termrel)
apply (rule_tac r="br_termrel δ" in wf_subset)
apply (auto intro: br_step_in_termrel)
done

lemma bre_invar_final:
"∀Σ. Σ∈wa_invar (bre_algo Qi δ) ∧ Σ∉wa_cond (bre_algo Qi δ)
⟶ ((Qi∩fst Σ={}) ⟷ (Qi ∩ b_accessible δ = {}))"
apply (simp add: br_invar_def bre_cond_def bre_algo_def)
apply safe
apply (auto dest!: b_accs_as_closed)
done

theorem bre_while_algo:
assumes FIN[simp]: "finite δ"
shows "while_algo (bre_algo Qi δ)"
apply (unfold_locales)
apply (unfold bre_algo_def)
apply (auto simp add: br_invar_initial br_step_in_termrel
intro: br_invar_step
dest: rev_subsetD[OF _ bre_cond_imp_br_cond])
apply (rule_tac r="br_termrel δ" in wf_subset)
apply (auto intro: br_step_in_termrel
dest: rev_subsetD[OF _ bre_cond_imp_br_cond])
done

text_raw ‹\paragraph{‹α'› - Level}›
text ‹
For each rule, the algorithm now maintains a counter that counts the number
of undiscovered states on the rules RHS. Whenever a new state is discovered,
this counter is decremented for all rules where the state occurs on the RHS.
The LHS states of rules where the counter falls to 0 are added to the
worklist. The idea is that decrementing the counter is more efficient than
checking whether all states on the rule's RHS have been discovered.

A similar algorithm is sketched in \cite{tata2007}(Exercise~1.18).
›
type_synonym ('Q,'L) br'_state = "'Q set × 'Q set × (('Q,'L) ta_rule ⇀ nat)"

― ‹Abstraction to @{text α}-level›
definition br'_α :: "('Q,'L) br'_state ⇒ ('Q,'L) br_state"
where "br'_α = (λ(Q,W,rcm). (Q,W))"

definition br'_invar_add :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state set"
(∀r∈δ. rcm r = Some (card (set (rhsq r) - (Q - W)))) ∧
{lhs r | r. r∈δ ∧ the (rcm r) = 0} ⊆ Q
}"

definition br'_invar :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state set"
where "br'_invar δ == br'_invar_add δ ∩ {Σ. br'_α Σ ∈ br_invar δ}"

inductive_set br'_step
:: "('Q,'L) ta_rule set ⇒ (('Q,'L) br'_state × ('Q,'L) br'_state) set"
for δ where
"⟦ q∈W;
Q' = Q ∪ { lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 };
W' = (W-{q})
∪ ({ lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 }
- Q);
!!r. r∈δ ⟹ rcm' r = ( if q ∈ set (rhsq r) then
Some (the (rcm r) - 1)
else rcm r
)
⟧ ⟹ ((Q,W,rcm),(Q',W',rcm')) ∈ br'_step δ"

definition br'_cond :: "('Q,'L) br'_state set"
where "br'_cond == {(Q,W,rcm). W≠{}}"
definition bre'_cond :: "'Q set ⇒ ('Q,'L) br'_state set"
where "bre'_cond Qi == {(Q,W,rcm). W≠{} ∧ (Qi∩Q={})}"

inductive_set br'_initial :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state set"
for δ where
"⟦ !!r. r∈δ ⟹ rcm r = Some (card (set (rhsq r))) ⟧
⟹ (br_iq δ, br_iq δ, rcm)∈br'_initial δ"

definition "br'_algo δ == ⦇
wa_cond=br'_cond,
wa_step = br'_step δ,
wa_initial = br'_initial δ,
wa_invar = br'_invar δ
⦈"

definition "bre'_algo Qi δ == ⦇
wa_cond=bre'_cond Qi,
wa_step = br'_step δ,
wa_initial = br'_initial δ,
wa_invar = br'_invar δ
⦈"

lemma br'_step_invar:
assumes finite[simp]: "finite δ"
assumes INV: "Σ∈br'_invar_add δ" "br'_α Σ ∈ br_invar δ"
assumes STEP: "(Σ,Σ') ∈ br'_step δ"
proof -
obtain Q W rcm where [simp]: "Σ=(Q,W,rcm)"
by (cases Σ) auto
obtain Q' W' rcm' where [simp]: "Σ'=(Q',W',rcm')"
by (cases Σ') auto

from STEP obtain q where
STEPF:
"q∈W"
"Q' = Q ∪ { lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 }"
"W' = (W-{q})
∪ ({ lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 }
- Q)"
"!!r. r∈δ ⟹ rcm' r = ( if q ∈ set (rhsq r) then
Some (the (rcm r) - 1)
else rcm r
)"
by (auto elim: br'_step.cases)

from INV[unfolded br'_invar_def br_invar_def br'_invar_add_def br'_α_def,
simplified]
have INV:
"(∀r∈δ. rcm r = Some (card (set (rhsq r) - (Q - W))))"
"{lhs r |r. r ∈ δ ∧ the (rcm r) = 0} ⊆ Q"
"W ⊆ Q"
"Q ⊆ b_accessible δ"
"bacc_step δ (Q - W) ⊆ Q"
"finite Q"
by auto

{
fix r
assume A: "r∈δ"
with INV(1) have RCMR: "rcm r = Some (card (set (rhsq r) - (Q - W)))"
by auto

have "rcm' r = Some (card (set (rhsq r) - (Q' - W')))"
proof (cases "q∈set (rhsq r)")
case False
with A STEPF(4) have "rcm' r = rcm r" by auto
moreover from STEPF INV(3) False have
"set (rhsq r) - (Q-W) = set (rhsq r) - (Q'-W')"
by auto
ultimately show ?thesis
next
case True
with A STEPF(4) RCMR have
"rcm' r = Some ((card (set (rhsq r) - (Q - W))) - 1)"
by simp
moreover from STEPF INV(3) True have
"set (rhsq r) - (Q-W) = insert q (set (rhsq r) - (Q'-W'))"
"q∉(set (rhsq r) - (Q'-W'))"
by auto
ultimately show ?thesis
qed
} moreover {
fix r
assume A: "r∈δ" "the (rcm' r) = 0"
have "lhs r ∈ Q'" proof (cases "q∈set (rhsq r)")
case True
with A(1) STEPF(4) have "rcm' r = Some (the (rcm r) - 1)" by auto
with A(2) have "the (rcm r) - 1 = 0" by auto
hence "the (rcm r) ≤ 1" by auto
with STEPF(2) A(1) True show ?thesis by auto
next
case False
with A(1) STEPF(4) have "rcm' r = rcm r" by auto
with A(2) have "the (rcm r) = 0" by auto
with A(1) INV(2) have "lhs r ∈ Q" by auto
with STEPF(2) show ?thesis by auto
qed
} ultimately show ?thesis
qed

lemma br'_invar_initial:
apply safe
apply (erule br'_initial.cases)
done

lemma br'_rcm_aux':
"⟦ (Q,W,rcm)∈br'_invar δ; q∈W ⟧
⟹ {r ∈ δ. q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}
= {r∈δ. q∈set (rhsq r) ∧ set (rhsq r) ⊆ (Q - (W-{q}))}"
proof (intro subsetI equalityI, goal_cases)
case prems: (1 r)
hence  B: "r∈δ" "q∈set (rhsq r)" "the (rcm r) ≤ Suc 0" by auto
from B(1,3) prems(1)[unfolded br'_invar_def br'_invar_add_def] have
CARD: "card (set (rhsq r) - (Q - W)) ≤ Suc 0"
by auto
from prems(1)[unfolded br'_invar_def br_invar_def br'_α_def] have WSQ: "W⊆Q"
by auto
have "set (rhsq r) - (Q - W) = {q}"
proof -
from B(2) prems(2) have R1: "q∈set (rhsq r) - (Q - W)" by auto
moreover
{
fix x
assume A: "x≠q" "x∈set (rhsq r) - (Q - W)"
with R1 have "{x,q} ⊆ set (rhsq r) - (Q - W)" by auto
hence "card {x,q} ≤ card (set (rhsq r) - (Q - W))"
with CARD A(1) have False by auto
}
ultimately show ?thesis by auto
qed
with prems(2) WSQ have "set (rhsq r) ⊆ Q - (W - {q})" by auto
thus ?case using B(1,2) by auto
next
case prems: (2 r)
hence B: "r∈δ" "q∈set (rhsq r)" "set (rhsq r) ⊆ Q - (W - {q})" by auto
br'_α_def br_invar_def]
have
IC: "W⊆Q" "the (rcm r) = card (set (rhsq r) - (Q - W))"
by auto
have "set (rhsq r) - (Q - W) ⊆ {q}" using B(2,3) IC(1) by auto
from card_mono[OF _ this] have "the (rcm r) ≤ Suc 0" by (simp add: IC(2))
with B(1,2) show ?case by auto
qed

lemma br'_rcm_aux:
assumes A: "(Q,W,rcm)∈br'_invar δ" "q∈W"
shows "{lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}
= {lhs r | r. r∈δ ∧ q∈set (rhsq r) ∧ set (rhsq r) ⊆ (Q - (W-{q}))}"
proof -
have "{lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}
= lhs  {r ∈ δ. q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}"
by auto
also from br'_rcm_aux'[OF A] have
"… = lhs  {r ∈ δ. q ∈ set (rhsq r) ∧ set (rhsq r) ⊆ Q - (W - {q})}"
by simp
also have
"… = {lhs r | r. r∈δ ∧ q∈set (rhsq r) ∧ set (rhsq r) ⊆ (Q - (W-{q}))}"
by auto
finally show ?thesis .
qed

lemma br'_invar_QcD:
"(Q,W,rcm) ∈ br'_invar δ ⟹ {lhs r | r. r∈δ ∧ set (rhsq r) ⊆ (Q-W)} ⊆ Q"
proof (safe)
fix r
assume A: "(Q,W,rcm)∈br'_invar δ" "r∈δ" "set (rhsq r) ⊆ Q - W"
from A(1)[unfolded br'_invar_def br'_invar_add_def br'_α_def br_invar_def,
simplified]
have
IC: "W ⊆ Q"
"finite Q"
"(∀r∈δ. rcm r = Some (card (set (rhsq r) - (Q - W))))"
"{lhs r |r. r ∈ δ ∧ the (rcm r) = 0} ⊆ Q" by auto
from IC(3) A(2,3) have "the (rcm r) = 0" by auto
with IC(4) A(2) show "lhs r ∈ Q" by auto
qed

lemma br'_rcm_aux2:
"⟦ (Q,W,rcm)∈br'_invar δ; q∈W ⟧
⟹ Q ∪ br_dsq δ q (Q,W)
= Q ∪ {lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}"
apply (simp only: br'_rcm_aux)
apply (unfold br_dsq_def)
apply simp
apply (frule br'_invar_QcD)
apply auto
done

lemma br'_rcm_aux3:
"⟦ (Q,W,rcm)∈br'_invar δ; q∈W ⟧
⟹ br_dsq δ q (Q,W) - Q
= {lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0} - Q"
apply (simp only: br'_rcm_aux)
apply (unfold br_dsq_def)
apply simp
apply (frule br'_invar_QcD)
apply auto
done

lemma br'_step_abs:
"⟦
Σ∈br'_invar δ;
(Σ,Σ') ∈ br'_step δ
⟧ ⟹ (br'_α Σ, br'_α Σ')∈br_step δ"
apply (cases Σ, cases Σ', simp)
apply (erule br'_step.cases)
apply (rule_tac q=q in br_step.intros)
apply simp
apply (simp only: br'_rcm_aux2)
apply (simp only: br'_rcm_aux3)
done

lemma br'_initial_abs: "br'_α(br'_initial δ) = {br_initial δ}"
apply (force simp add: br_initial_def br'_α_def
elim: br'_initial.cases
intro: br'_initial.intros)
done

lemma br'_cond_abs: "Σ∈br'_cond ⟷ (br'_α Σ) ∈ br_cond"
by (cases Σ)
(simp add: br'_cond_def br_cond_def br'_α_def image_Collect
br'_algo_def br_algo_def)

lemma bre'_cond_abs: "Σ∈bre'_cond Qi ⟷ (br'_α Σ)∈bre_cond Qi"
by (cases Σ) (simp add: bre'_cond_def bre_cond_def br'_α_def image_Collect
bre'_algo_def bre_algo_def)

lemma br'_invar_abs: "br'_αbr'_invar δ ⊆ br_invar δ"

theorem br'_pref_br: "wa_precise_refine (br'_algo δ) (br_algo δ) br'_α"
apply unfold_locales
apply (simp_all add: br'_cond_abs br'_step_abs br'_invar_abs br'_initial_abs)
done

interpretation br'_pref: wa_precise_refine "br'_algo δ" "br_algo δ" "br'_α"
using br'_pref_br .

theorem br'_while_algo:
"finite δ ⟹ while_algo (br'_algo δ)"
apply (rule br'_pref.wa_intro)
apply (erule (3) br'_step_invar)
done

lemma fst_br'_α: "fst (br'_α s) = fst s" by (cases s) (simp add: br'_α_def)

lemmas br'_invar_final =
br'_pref.transfer_correctness[OF br_invar_final, unfolded fst_br'_α]

theorem bre'_pref_br: "wa_precise_refine (bre'_algo Qi δ) (bre_algo Qi δ) br'_α"
apply unfold_locales
apply (simp_all add: bre'_cond_abs br'_step_abs br'_invar_abs br'_initial_abs)
done

interpretation bre'_pref:
wa_precise_refine "bre'_algo Qi δ" "bre_algo Qi δ" "br'_α"
using bre'_pref_br .

theorem bre'_while_algo:
"finite δ ⟹ while_algo (bre'_algo Qi δ)"
apply (rule bre'_pref.wa_intro)
apply (erule (3) br'_step_invar)
done

lemmas bre'_invar_final =
bre'_pref.transfer_correctness[OF bre_invar_final, unfolded fst_br'_α]

text_raw ‹\paragraph{Implementing a Step}›
text ‹
In this paragraph, it is shown how to implement a step of the br'-algorithm
by iteration over the rules that have the discovered state on their RHS.
›

definition br'_inner_step
:: "('Q,'L) ta_rule ⇒ ('Q,'L) br'_state ⇒ ('Q,'L) br'_state"
where
"br'_inner_step == λr (Q,W,rcm). let c=the (rcm r) in (
if c≤1 then insert (lhs r) Q else Q,
if c≤1 ∧ (lhs r) ∉ Q then insert (lhs r) W else W,
rcm ( r ↦ (c-(1::nat)))
)
"

definition br'_inner_invar
:: "('Q,'L) ta_rule set ⇒ 'Q ⇒ ('Q,'L) br'_state
⇒ ('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state ⇒ bool"
where
"br'_inner_invar rules q == λ(Q,W,rcm) it (Q',W',rcm').
Q' = Q ∪ { lhs r | r. r∈rules-it ∧ the (rcm r) ≤ 1 } ∧
W' = (W-{q}) ∪ ({ lhs r | r. r∈rules-it ∧ the (rcm r) ≤ 1 } - Q) ∧
(∀r. rcm' r = (if r∈rules-it then Some (the (rcm r) - 1) else rcm r))
"

lemma br'_inner_invar_imp_final:
"⟦ q∈W; br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) {} Σ' ⟧
⟹ ((Q,W,rcm),Σ') ∈ br'_step δ"
apply (unfold br'_inner_invar_def)
apply auto
apply (rule br'_step.intros)
apply assumption
apply auto
done

lemma br'_inner_invar_step:
"⟦ q∈W; br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) it Σ';
r∈it; it⊆{r∈δ. q∈set (rhsq r)}
⟧ ⟹ br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm)
(it-{r}) (br'_inner_step r Σ')
"
apply (cases Σ', simp)
apply (unfold br'_inner_invar_def br'_inner_step_def Let_def)
apply auto
done

lemma br'_inner_invar_initial:
"⟦ q∈W ⟧ ⟹ br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm)
{r∈δ. q∈set (rhsq r)} (Q,W-{q},rcm)"
apply auto
done

lemma br'_inner_step_proof:
fixes αs :: "'Σ ⇒ ('Q,'L) br'_state"
fixes cstep :: "('Q,'L) ta_rule ⇒ 'Σ ⇒ 'Σ"
fixes Σh :: "'Σ"
fixes cinvar :: "('Q,'L) ta_rule set ⇒ 'Σ ⇒ bool"

assumes iterable_set: "set_iteratei α invar iteratei"
assumes invar_initial: "cinvar {r∈δ. q∈set (rhsq r)} Σh"
assumes invar_step:
"!!it r Σ. ⟦ r∈it; it ⊆ {r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧
⟹ cinvar (it-{r}) (cstep r Σ)"
assumes step_desc:
"!!it r Σ. ⟦ r∈it; it⊆{r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧
⟹ αs (cstep r Σ) = br'_inner_step r (αs Σ)"
assumes it_set_desc: "invar it_set" "α it_set = {r∈δ. q∈set (rhsq r)}"

assumes QIW[simp]: "q∈W"

assumes Σ_desc[simp]: "αs Σ = (Q,W,rcm)"
assumes Σh_desc[simp]: "αs Σh = (Q,W-{q},rcm)"

shows "(αs Σ, αs (iteratei it_set (λ_. True) cstep Σh))∈br'_step δ"
proof -
interpret set_iteratei α invar iteratei by fact

show ?thesis
apply (rule_tac
I="λit Σ. cinvar it Σ
∧ br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm)
it (αs Σ)"
in iterate_rule_P)
apply (simp_all
step_desc br'_inner_invar_step)
apply (rule br'_inner_invar_imp_final)
apply (rule QIW)
apply simp
done
qed

text_raw ‹\paragraph{Computing Witnesses}›
text ‹
The algorithm is now refined further, such that it stores, for each discovered
state, a witness for non-emptiness, i.e. a tree that is accepted with the
discovered state.
›

― ‹A map from states to trees has the witness-property, if it maps states to
trees that are accepted with that state:›
definition "witness_prop δ m == ∀q t. m q = Some t ⟶ accs δ t q"

― ‹Construct a witness for the LHS of a rule, provided that the map contains
witnesses for all states on the RHS:›
definition construct_witness
:: "('Q ⇀ 'L tree) ⇒ ('Q,'L) ta_rule ⇒ 'L tree"
where
"construct_witness Q r == NODE (rhsl r) (List.map (λq. the (Q q)) (rhsq r))"

lemma witness_propD: "⟦witness_prop δ m; m q = Some t⟧ ⟹ accs δ t q"

lemma construct_witness_correct:
"⟦ witness_prop δ Q; r∈δ; set (rhsq r) ⊆ dom Q ⟧
⟹ accs δ (construct_witness Q r) (lhs r)"
apply (unfold construct_witness_def witness_prop_def)
apply (cases r)
apply simp
apply (erule accs.intros)
apply (auto dest: nth_mem)
done

lemma construct_witness_eq:
"⟦ Q | set (rhsq r) = Q' | set (rhsq r) ⟧ ⟹
construct_witness Q r = construct_witness Q' r"
apply (unfold construct_witness_def)
apply auto
apply (subgoal_tac "Q x = Q' x")
apply (simp)
apply (drule_tac x=x in fun_cong)
apply auto
done

text ‹
The set of discovered states is refined by a map from discovered states to
their witnesses:
›
type_synonym ('Q,'L) brw_state = "('Q⇀'L tree) × 'Q set × (('Q,'L) ta_rule ⇀ nat)"

definition brw_α :: "('Q,'L) brw_state ⇒ ('Q,'L) br'_state"
where "brw_α = (λ(Q,W,rcm). (dom Q,W,rcm))"

definition brw_invar_add :: "('Q,'L) ta_rule set ⇒ ('Q,'L) brw_state set"
where "brw_invar_add δ == {(Q,W,rcm). witness_prop δ Q}"

definition "brw_invar δ == brw_invar_add δ ∩ {s. brw_α s ∈ br'_invar δ}"

(* TODO:
This step description does not allow full flexibility, because
we may want to construct new witnesses from other witnesses constructed
in the same step!

However, if we say t = construct_witness Q' r, may we run into cyclicity
problems, where a cycle of witnesses
may witness itself?. Hmm? As these cyclic witnesses would have to
be infinite, they cannot exist?

But, if we use a BFS search strategy, the current step description will
compute minimal depth witnesses.
The argumentation is, that:
Initially, all witnesses of depth 1 (definitely minimal) are discovered
A witness of depth n has children of length < n
The states that are initially on the workset are all those with
witnesses of depth 1. Thus,
after they have been processed, all states with witnesses of depth 2 have
been discovered. This argument can be iterated inductively.
*)
inductive_set brw_step
:: "('Q,'L) ta_rule set ⇒ (('Q,'L) brw_state × ('Q,'L) brw_state) set"
for δ where
"⟦
q∈W;
dsqr = { r∈δ. q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 };
dom Q' = dom Q ∪ lhsdsqr;
!!q t. Q' q = Some t ⟹ Q q = Some t
∨ (∃r∈dsqr. q=lhs r ∧ t=construct_witness Q r);
W' = (W-{q}) ∪ (lhsdsqr - dom Q);
!!r. r∈δ ⟹ rcm' r = ( if q ∈ set (rhsq r) then
Some (the (rcm r) - 1)
else rcm r
)
⟧ ⟹ ((Q,W,rcm),(Q',W',rcm')) ∈ brw_step δ"

definition brw_cond :: "'Q set ⇒ ('Q,'L) brw_state set"
where "brw_cond Qi == {(Q,W,rcm). W≠{} ∧ (Qi∩dom Q={})}"

inductive_set brw_iq :: "('Q,'L) ta_rule set ⇒ ('Q ⇀ 'L tree) set"
for δ where
"⟦
∀q t. Q q = Some t ⟶ (∃r∈δ. rhsq r = [] ∧ q = lhs r
∧ t = NODE (rhsl r) []);
∀r∈δ. rhsq r = [] ⟶ Q (lhs r) ≠ None
⟧ ⟹ Q ∈ brw_iq δ"

inductive_set brw_initial :: "('Q,'L) ta_rule set ⇒ ('Q,'L) brw_state set"
for δ where
"⟦ !!r. r∈δ ⟹ rcm r = Some (card (set (rhsq r))); Q∈brw_iq δ ⟧
⟹ (Q, br_iq δ, rcm)∈brw_initial δ"

definition "brw_algo Qi δ == ⦇
wa_cond=brw_cond Qi,
wa_step = brw_step δ,
wa_initial = brw_initial δ,
wa_invar = brw_invar δ
⦈"

lemma brw_cond_abs: "Σ∈brw_cond Qi ⟷ (brw_α Σ)∈bre'_cond Qi"
apply (cases Σ)
apply (simp add: brw_cond_def bre'_cond_def brw_α_def)
done

lemma brw_initial_abs: "Σ∈brw_initial δ ⟹ brw_α Σ ∈ br'_initial δ"
apply (cases Σ, simp)
apply (erule brw_initial.cases)
apply (erule brw_iq.cases)
apply (subgoal_tac "dom Qa = br_iq δ")
apply simp
apply (rule br'_initial.intros)
apply auto [1]
done

lemma brw_invar_initial: "brw_initial δ ⊆ brw_invar_add δ"
apply safe
apply (erule brw_initial.cases)
apply (erule brw_iq.cases)
apply auto
proof goal_cases
case prems: (1 q t rcm Q)
from prems(3)[rule_format, OF prems(1)] obtain r where
[simp]: "r∈δ" "rhsq r = []" "q=lhs r" "t=NODE (rhsl r) []"
by blast
have RF[simplified]: "r=((lhs r) → (rhsl r) (rhsq r))" by (cases r) simp
show ?case
apply (simp)
apply (rule accs.intros)
apply (subst RF[symmetric])
apply auto
done
qed

lemma brw_step_abs:
"⟦ (Σ,Σ')∈brw_step δ ⟧ ⟹ (brw_α Σ, brw_α Σ')∈br'_step δ"
apply (cases Σ, cases Σ', simp)
apply (erule brw_step.cases)
apply hypsubst
apply (rule br'_step.intros)
apply assumption
apply auto
done

lemma brw_step_invar:
assumes FIN[simp]: "finite δ"
assumes INV: "Σ∈brw_invar_add δ" and BR'INV: "brw_α Σ ∈ br'_invar δ"
assumes STEP: "(Σ,Σ') ∈ brw_step δ"
proof -
obtain Q W rcm Q' W' rcm' where
[simp]: "Σ=(Q,W,rcm)" "Σ'=(Q',W',rcm')"
by (cases Σ, cases Σ') force

from INV have WP: "witness_prop δ Q"

obtain qw dsqr where SPROPS:
"dsqr = {r ∈ δ. qw ∈ set (rhsq r) ∧ the (rcm r) ≤ 1}"
"qw∈W"
"dom Q' = dom Q ∪ lhs  dsqr"
"!!q t. Q' q = Some t ⟹ Q q = Some t
∨ (∃r∈dsqr. q=lhs r ∧ t=construct_witness Q r)"
by (auto intro: brw_step.cases[OF STEP[simplified]])
from br'_rcm_aux'[OF BR'INV[unfolded brw_α_def, simplified] SPROPS(2)] have
DSQR_ALT: "dsqr = {r ∈ δ. qw ∈ set (rhsq r)
∧ set (rhsq r) ⊆ dom Q - (W - {qw})}"
have "witness_prop δ Q'"
proof (unfold witness_prop_def, safe)
fix q t
assume A: "Q' q = Some t"

from SPROPS(4)[OF A] have
"Q q = Some t ∨ (∃r∈dsqr. q = lhs r ∧ t = construct_witness Q r)" .
moreover {
assume C: "Q q = Some t"
from witness_propD[OF WP, OF C] have "accs δ t q" .
} moreover {
fix r
assume "r∈dsqr" and [simp]: "q=lhs r" "t=construct_witness Q r"
from ‹r∈dsqr› have 1: "r∈δ" "set (rhsq r) ⊆ dom Q"
from construct_witness_correct[OF WP 1] have "accs δ t q" by simp
} ultimately show "accs δ t q" by blast
qed
qed

theorem brw_pref_bre': "wa_precise_refine (brw_algo Qi δ) (bre'_algo Qi δ) brw_α"
apply (unfold_locales)
apply (auto simp add: brw_cond_abs brw_step_abs brw_initial_abs brw_invar_def)
done

interpretation brw_pref:
wa_precise_refine "brw_algo Qi δ" "bre'_algo Qi δ" "brw_α"
using brw_pref_bre' .

theorem brw_while_algo: "finite δ ⟹ while_algo (brw_algo Qi δ)"
apply (rule brw_pref.wa_intro)
apply (auto intro: brw_step_invar simp add: brw_invar_initial)
done

lemma fst_brw_α: "fst (brw_α s) = dom (fst s)"
by (cases s) (simp add: brw_α_def)

theorem brw_invar_final:
"∀sc. sc ∈ wa_invar (brw_algo Qi δ) ∧ sc ∉ wa_cond (brw_algo Qi δ)
⟶ (Qi ∩ dom (fst sc) = {}) = (Qi ∩ b_accessible δ = {})
∧ (witness_prop δ (fst sc))"
apply (intro conjI allI impI)
using brw_pref.transfer_correctness[OF bre'_invar_final, unfolded fst_brw_α]
apply blast
done

text_raw ‹\paragraph{Implementing a Step}›
inductive_set brw_inner_step
:: "('Q,'L) ta_rule ⇒ (('Q,'L) brw_state × ('Q,'L) brw_state) set"
for r where
"⟦  c = the (rcm r); Σ = (Q,W,rcm); Σ'=(Q',W',rcm');
if c≤1 ∧ (lhs r) ∉ dom Q then
Q' = Q(lhs r ↦ construct_witness Q r)
else Q' = Q;
if c≤1 ∧ (lhs r) ∉ dom Q then
W' = insert (lhs r) W
else W' = W;
rcm' = rcm ( r ↦ (c-(1::nat)))
⟧ ⟹ (Σ,Σ')∈brw_inner_step r"

definition brw_inner_invar
:: "('Q,'L) ta_rule set ⇒ 'Q ⇒ ('Q,'L) brw_state ⇒ ('Q,'L) ta_rule set
⇒ ('Q,'L) brw_state ⇒ bool"
where
"brw_inner_invar rules q == λ(Q,W,rcm) it (Q',W',rcm').
(br'_inner_invar rules q (brw_α (Q,W,rcm)) it (brw_α (Q',W',rcm')) ∧
(Q'|dom Q = Q) ∧
(let dsqr = { r∈rules - it. the (rcm r) ≤ 1 } in
(∀q t. Q' q = Some t ⟶ (Q q = Some t
∨ (Q q = None ∧ (∃r∈dsqr. q=lhs r ∧ t=construct_witness Q r))
)
)))
"

lemma brw_inner_step_abs:
"(Σ,Σ')∈brw_inner_step r ⟹ br'_inner_step r (brw_α Σ) = brw_α Σ'"
apply (erule brw_inner_step.cases)
apply (unfold br'_inner_step_def brw_α_def Let_def)
apply auto
done

lemma brw_inner_invar_imp_final:
"⟦ q∈W; brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) {} Σ' ⟧
⟹ ((Q,W,rcm),Σ') ∈ brw_step δ"
apply (unfold brw_inner_invar_def br'_inner_invar_def brw_α_def)
apply (rule brw_step.intros)
apply assumption
apply (rule refl)
apply auto
done

lemma brw_inner_invar_step:
assumes INVI: "(Q,W,rcm)∈brw_invar δ"
assumes A: "q∈W" "r∈it" "it⊆{r∈δ. q∈set (rhsq r)}"
assumes INVH: "brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) it Σh"
assumes STEP: "(Σh,Σ')∈brw_inner_step r"
shows "brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) (it-{r}) Σ'"
proof -
from INVI have BR'_INV: "(dom Q,W,rcm)∈br'_invar δ"

obtain c Qh Wh rcmh Q' W' rcm' where
SIGMAF[simp]: "Σh=(Qh,Wh,rcmh)" "Σ'=(Q',W',rcm')" and
CF[simp]: "c = the (rcmh r)" and
SF: "if c≤1 ∧ (lhs r) ∉ dom Qh then
Q' = Qh(lhs r ↦ (construct_witness Qh r))
else Q' = Qh"

"if c≤1 ∧ (lhs r) ∉ dom Qh then
W' = insert (lhs r) Wh
else W' = Wh"

"rcm' = rcmh ( r ↦ (c-(1::nat)))"
by (blast intro: brw_inner_step.cases[OF STEP])
let ?rules = "{r∈δ. q∈set (rhsq r)}"
let ?dsqr = "λit. { r∈?rules - it. the (rcm r) ≤ 1 }"
from INVH have INVHF:
"br'_inner_invar ?rules q (dom Q, W-{q}, rcm) (it) (dom Qh,Wh,rcmh)"
"Qh|dom Q = Q"
"(∀q t. Qh q = Some t ⟶ (Q q = Some t
∨ (Q q = None ∧ (∃r∈?dsqr it. q=lhs r ∧ t=construct_witness Q r))
)
)"
by (auto simp add: brw_inner_invar_def Let_def brw_α_def)
from INVHF(1)[unfolded br'_inner_invar_def] have INV'HF:
"dom Qh = dom Q ∪ lhs?dsqr it"
"(∀r. rcmh r = (if r ∈ ?rules - it then
Some (the (rcm r) - 1)
else rcm r))"
by auto
from brw_inner_step_abs[OF STEP]
br'_inner_invar_step[OF A(1) INVHF(1) A(2,3)] have
G1: "br'_inner_invar ?rules q (dom Q, W-{q}, rcm) (it-{r}) (dom Q',W',rcm')"
moreover have
"(∀q t. Q' q = Some t ⟶ (Q q = Some t
∨ ( Q q = None
∧ (∃r∈?dsqr (it-{r}). q=lhs r ∧ t=construct_witness Q r)
)
)
)" (is ?G1)

"Q'|dom Q = Q" (is ?G2)
proof -
{
assume C: "¬ c≤1 ∨ lhs r ∈ dom Qh"
with SF have "Q'=Qh" by auto
with INVHF(2,3) have ?G1 ?G2 by auto
} moreover {
assume C: "c≤1" "lhs r∉ dom Qh"
with SF have Q'F: "Q'=Qh(lhs r ↦ (construct_witness Qh r))" by auto
from C(2) INVHF(2) INV'HF(1) have G2: ?G2 by (auto simp add: Q'F)
from C(1) INV'HF A have
RI: "r∈?dsqr (it-{r})" and
DSS: "dom Q ⊆ dom Qh"
by (auto)
from br'_rcm_aux'[OF BR'_INV A(1)] RI have
RDQ: "set (rhsq r) ⊆ dom Q"
by auto
with INVHF(2) have "Qh | set (rhsq r) = Q | set (rhsq r)"
by (blast intro: restrict_map_subset_eq)
hence [simp]: "construct_witness Qh r = construct_witness Q r"
by (blast dest: construct_witness_eq)

from DSS C(2) have [simp]: "Q (lhs r) = None" "Qh (lhs r) = None" by auto
have G1: ?G1
proof (intro allI impI, goal_cases)
case prems: (1 q t)
{
assume [simp]: "q=lhs r"
from prems Q'F have [simp]: "t = (construct_witness Qh r)" by simp
from RI have ?case by auto
} moreover {
assume "q≠lhs r"
with Q'F prems have "Qh q = Some t" by auto
with INVHF(3) have ?case by auto
} ultimately show ?case by blast
qed
note G1 G2
} ultimately show ?G1 ?G2 by blast+
qed
ultimately show ?thesis
by (unfold brw_inner_invar_def Let_def brw_α_def) auto
qed

lemma brw_inner_invar_initial:
"⟦q∈W⟧ ⟹ brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm)
{r∈δ. q∈set (rhsq r)} (Q,W-{q},rcm)"
by (simp add: brw_inner_invar_def br'_inner_invar_initial brw_α_def)

theorem brw_inner_step_proof:
fixes αs :: "'Σ ⇒ ('Q,'L) brw_state"
fixes cstep :: "('Q,'L) ta_rule ⇒ 'Σ ⇒ 'Σ"
fixes Σh :: "'Σ"
fixes cinvar :: "('Q,'L) ta_rule set ⇒ 'Σ ⇒ bool"

assumes set_iterate: "set_iteratei α invar iteratei"
assumes invar_start: "(αs Σ)∈brw_invar δ"
assumes invar_initial: "cinvar {r∈δ. q∈set (rhsq r)} Σh"
assumes invar_step:
"!!it r Σ. ⟦ r∈it; it ⊆ {r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧
⟹ cinvar (it-{r}) (cstep r Σ)"
assumes step_desc:
"!!it r Σ. ⟦ r∈it; it⊆{r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧
⟹ (αs Σ, αs (cstep r Σ)) ∈ brw_inner_step r"
assumes it_set_desc: "invar it_set" "α it_set = {r∈δ. q∈set (rhsq r)}"

assumes QIW[simp]: "q∈W"

assumes Σ_desc[simp]: "αs Σ = (Q,W,rcm)"
assumes Σh_desc[simp]: "αs Σh = (Q,W-{q},rcm)"

shows "(αs Σ, αs (iteratei it_set (λ_. True) cstep Σh))∈brw_step δ"
proof -
interpret set_iteratei α invar iteratei by fact

show ?thesis
apply (rule_tac
I="λit Σ. cinvar it Σ ∧ brw_inner_invar {r∈δ. q∈set (rhsq r)} q
(Q,W-{q},rcm) it (αs Σ)"
in iterate_rule_P)
apply (auto
simp add: it_set_desc invar_initial brw_inner_invar_initial invar_step
step_desc brw_inner_invar_step[OF invar_start[simplified]]
brw_inner_invar_imp_final[OF QIW])
done
qed

subsection ‹Product Automaton›

text ‹
The forward-reduced product automaton can be described as a state-space
exploration problem.

In this section, the DFS-algorithm for state-space exploration
(cf. Theory~@{theory Collections_Examples.Exploration} in the Isabelle Collections Framework) is refined to compute the product automaton.
›

type_synonym ('Q1,'Q2,'L) frp_state =
"('Q1×'Q2) set × ('Q1×'Q2) list × (('Q1×'Q2),'L) ta_rule set"

definition frp_α :: "('Q1,'Q2,'L) frp_state ⇒ ('Q1×'Q2) dfs_state"
where "frp_α S == let (Q,W,δ)=S in (Q, W)"

{ (Q,W,δd). δd = { r. r∈δ_prod δ1 δ2 ∧ lhs r ∈ Q - set W} }"

definition frp_invar
:: "('Q1, 'L) tree_automaton_rec ⇒ ('Q2, 'L) tree_automaton_rec
⇒ ('Q1,'Q2,'L) frp_state set"
where "frp_invar T1 T2 ==
∩ { s. frp_α s ∈ dfs_invar (ta_initial T1 × ta_initial T2)
(f_succ (δ_prod (ta_rules T1) (ta_rules T2))) }"

inductive_set frp_step
:: "('Q1,'L) ta_rule set ⇒ ('Q2,'L) ta_rule set
⇒ (('Q1,'Q2,'L) frp_state × ('Q1,'Q2,'L) frp_state) set"
for δ1 δ2 where
"⟦ W=(q1,q2)#Wtl;
distinct Wn;
set Wn = f_succ (δ_prod δ1 δ2)  {(q1,q2)} - Q;
W'=Wn@Wtl;
Q'=Q ∪ f_succ (δ_prod δ1 δ2)  {(q1,q2)};
δd'=δd ∪ {r∈δ_prod δ1 δ2. lhs r = (q1,q2) }
⟧ ⟹ ((Q,W,δd),(Q',W',δd'))∈frp_step δ1 δ2"

inductive_set frp_initial :: "'Q1 set ⇒ 'Q2 set ⇒ ('Q1,'Q2,'L) frp_state set"
for Q10 Q20 where
"⟦ distinct W; set W = Q10×Q20 ⟧ ⟹ (Q10×Q20,W,{}) ∈ frp_initial Q10 Q20"

definition frp_cond :: "('Q1,'Q2,'L) frp_state set" where
"frp_cond == {(Q,W,δd). W≠[]}"

definition "frp_algo T1 T2 == ⦇
wa_cond = frp_cond,
wa_step = frp_step (ta_rules T1) (ta_rules T2),
wa_initial = frp_initial (ta_initial T1) (ta_initial T2),
wa_invar = frp_invar T1 T2
⦈"

― ‹The algorithm refines the DFS-algorithm›
theorem frp_pref_dfs:
"wa_precise_refine (frp_algo T1 T2)
(dfs_algo (ta_initial T1 × ta_initial T2)
(f_succ (δ_prod (ta_rules T1) (ta_rules T2))))
frp_α"
apply unfold_locales
apply (auto simp add: frp_algo_def frp_α_def frp_cond_def dfs_algo_def
dfs_cond_def frp_invar_def
elim!: frp_step.cases frp_initial.cases
intro: dfs_step.intros dfs_initial.intros
)
done

interpretation frp_ref: wa_precise_refine "(frp_algo T1 T2)"
"(dfs_algo (ta_initial T1 × ta_initial T2)
(f_succ (δ_prod (ta_rules T1) (ta_rules T2))))"
"frp_α" using frp_pref_dfs .

― ‹The algorithm is a well-defined while-algorithm›
theorem frp_while_algo:
assumes TA: "tree_automaton T1"
"tree_automaton T2"
shows "while_algo (frp_algo T1 T2)"
proof -
interpret t1: tree_automaton T1 by fact
interpret t2: tree_automaton T2 by fact

have finite: "finite ((f_succ (δ_prod (ta_rules T1) (ta_rules T2)))⇧*
 (ta_initial T1 × ta_initial T2))"
proof -
have "((f_succ (δ_prod (ta_rules T1) (ta_rules T2)))⇧*
 (ta_initial T1 × ta_initial T2))
⊆ ((ta_initial T1 × ta_initial T2)
∪ δ_states (δ_prod (ta_rules T1) (ta_rules T2)))"
apply rule
apply (drule f_accessible_subset[unfolded f_accessible_def])
apply auto
done
moreover have "finite …"
by auto
ultimately show ?thesis by (simp add: finite_subset)
qed

show ?thesis
apply (rule frp_ref.wa_intro)
apply (rule dfs_while_algo[OF finite])
apply (simp add: frp_algo_def dfs_algo_def frp_invar_def)
apply (auto simp add: dfs_algo_def frp_algo_def frp_α_def
elim!: frp_step.cases) [1]
elim!: frp_initial.cases)
done
qed

(* unused
"⟦lhs r ∈ (f_succ δ)⇧*  Q0; r∈δ⟧ ⟹ set (rhsq r) ⊆ (f_succ δ)⇧*  Q0"
by (case_tac r) (auto dest: rtrancl_into_rtrancl intro: f_succ.intros)
*)

― ‹If the algorithm terminates, the forward reduced product automaton
can be constructed from the result›
theorem frp_inv_final:
"∀s. s∈wa_invar (frp_algo T1 T2) ∧ s∉wa_cond (frp_algo T1 T2)
⟶ (case s of (Q,W,δd) ⇒
⦇ ta_initial = ta_initial T1 × ta_initial T2,
ta_rules = δd
⦈ = ta_fwd_reduce (ta_prod T1 T2))"
apply (intro allI impI)
apply (case_tac s)
apply simp
apply (simp add: ta_reduce_def ta_prod_def frp_algo_def)
proof -
fix Q W δd
assume A: "(Q,W,δd)∈frp_invar T1 T2 ∧ (Q,W,δd)∉frp_cond"

from frp_ref.transfer_correctness[OF dfs_invar_final,
unfolded frp_algo_def, simplified,
rule_format, OF A]
have [simp]: "Q = f_accessible (δ_prod (ta_rules T1) (ta_rules T2))
(ta_initial T1 × ta_initial T2)"
by (simp add: f_accessible_def dfs_α_def frp_α_def)

from A show "δd = reduce_rules
(δ_prod (ta_rules T1) (ta_rules T2))
(f_accessible (δ_prod (ta_rules T1) (ta_rules T2))
(ta_initial T1 × ta_initial T2))"
apply (auto simp add: reduce_rules_def f_accessible_def frp_invar_def
`