# Theory Ta_impl

theory Ta_impl
imports AbsAlgo
(*  Title:       Tree Automata
Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section "Executable Implementation of Tree Automata"
theory Ta_impl
imports
Main
Collections.CollectionsV1
Ta AbsAlgo
"HOL-Library.Code_Target_Numeral"
begin

text_raw ‹\label{sec:taimpl}›

text ‹
In this theory, an effcient executable implementation of non-deterministic
tree automata and basic algorithms is defined.

The algorithms use red-black trees to represent sets of states or rules
where appropriate.
›

subsection "Prelude"

― ‹Make rules hashable›
instantiation ta_rule :: (hashable,hashable) hashable
begin
fun hashcode_of_ta_rule
:: "('Q1::hashable,'Q2::hashable) ta_rule ⇒ hashcode"
where
"hashcode_of_ta_rule (q → f qs) = hashcode q + hashcode f + hashcode qs"

definition [simp]: "hashcode = hashcode_of_ta_rule"

definition "def_hashmap_size::(('a,'b) ta_rule itself ⇒ nat) == (λ_. 32)"

instance
end

― ‹Make wrapped states hashable›
instantiation ustate_wrapper :: (hashable,hashable) hashable
begin
definition "hashcode x == (case x of USW1 a ⇒ 2 * hashcode a | USW2 b ⇒ 2 * hashcode b + 1)"
definition "def_hashmap_size = (λ_ :: (('a,'b) ustate_wrapper) itself. def_hashmap_size TYPE('a) + def_hashmap_size TYPE('b))"

instance using def_hashmap_size[where ?'a="'a"] def_hashmap_size[where ?'a="'b"]
by(intro_classes)(simp_all add: bounded_hashcode_bounds def_hashmap_size_ustate_wrapper_def split: ustate_wrapper.split)

end

subsubsection ‹Ad-Hoc instantiations of generic Algorithms›
setup Locale_Code.open_block
interpretation hll_idx: build_index_loc hm_ops ls_ops ls_ops by unfold_locales
interpretation ll_set_xy: g_set_xy_loc ls_ops ls_ops
by unfold_locales

interpretation lh_set_xx: g_set_xx_loc ls_ops hs_ops
by unfold_locales
interpretation lll_iflt_cp: inj_image_filter_cp_loc ls_ops ls_ops ls_ops
by unfold_locales
interpretation hhh_cart: cart_loc hs_ops hs_ops hs_ops by unfold_locales
interpretation hh_set_xy: g_set_xy_loc hs_ops hs_ops
by unfold_locales

interpretation llh_set_xyy: g_set_xyy_loc ls_ops ls_ops hs_ops
by unfold_locales

interpretation hh_map_to_nat: map_to_nat_loc hs_ops hm_ops by unfold_locales
interpretation hh_set_xy: g_set_xy_loc hs_ops hs_ops by unfold_locales
interpretation lh_set_xy: g_set_xy_loc ls_ops hs_ops by unfold_locales
interpretation hh_set_xx: g_set_xx_loc hs_ops hs_ops by unfold_locales
interpretation hs_to_fifo: set_to_list_loc hs_ops fifo_ops by unfold_locales

setup Locale_Code.close_block

subsection "Generating Indices of Rules"
text ‹
Rule indices are pieces of extra information that may be attached to a
tree automaton.
There are three possible rule indices
\begin{description}
\item[f]   index of rules by function symbol
\item[s]   index of rules by lhs
\item[sf]  index of rules
\end{description}
›

definition build_rule_index
:: "(('q,'l) ta_rule ⇒ 'i::hashable) ⇒ ('q,'l) ta_rule ls
⇒ ('i,('q,'l) ta_rule ls) hm"
where "build_rule_index == hll_idx.idx_build"

definition "build_rule_index_f δ == build_rule_index (λr. rhsl r) δ"
definition "build_rule_index_s δ == build_rule_index (λr. lhs r) δ"
definition "build_rule_index_sf δ == build_rule_index (λr. (lhs r, rhsl r)) δ"

lemma build_rule_index_f_correct[simp]:
assumes I[simp, intro!]: "ls_invar δ"
shows "hll_idx.is_index rhsl (ls_α δ) (build_rule_index_f δ)"
apply (unfold build_rule_index_f_def build_rule_index_def)
done

lemma build_rule_index_s_correct[simp]:
assumes I[simp, intro!]: "ls_invar δ"
shows
"hll_idx.is_index lhs (ls_α δ) (build_rule_index_s δ)"
by (unfold build_rule_index_s_def build_rule_index_def)

lemma build_rule_index_sf_correct[simp]:
assumes I[simp, intro!]: "ls_invar δ"
shows
"hll_idx.is_index (λr. (lhs r, rhsl r)) (ls_α δ) (build_rule_index_sf δ)"
by (unfold build_rule_index_sf_def build_rule_index_def)

subsection "Tree Automaton with Optional Indices"

text ‹
A tree automaton contains a hashset of initial states, a list-set of rules and
several (optional) rule indices.
›

― ‹Initial states›
hta_Qi :: "'q hs"
― ‹Rules›
hta_δ :: "('q,'l) ta_rule ls"
― ‹Rules by function symbol›
hta_idx_f :: "('l,('q,'l) ta_rule ls) hm option"
― ‹Rules by lhs state›
hta_idx_s :: "('q,('q,'l) ta_rule ls) hm option"
― ‹Rules by lhs state and function symbol›
hta_idx_sf :: "('q×'l,('q,'l) ta_rule ls) hm option"

― ‹Abstraction of a concrete tree automaton to an abstract one›
definition hta_α
where "hta_α H = ⦇ ta_initial = hs_α (hta_Qi H), ta_rules = ls_α (hta_δ H) ⦈"

― ‹Builds the f-index if not present›
definition "hta_ensure_idx_f H ==
case hta_idx_f H of
None ⇒ H⦇ hta_idx_f := Some (build_rule_index_f (hta_δ H)) ⦈ |
Some _ ⇒ H
"

― ‹Builds the s-index if not present›
definition "hta_ensure_idx_s H ==
case hta_idx_s H of
None ⇒ H⦇ hta_idx_s := Some (build_rule_index_s (hta_δ H)) ⦈ |
Some _ ⇒ H
"

― ‹Builds the sf-index if not present›
definition "hta_ensure_idx_sf H ==
case hta_idx_sf H of
None ⇒ H⦇ hta_idx_sf := Some (build_rule_index_sf (hta_δ H)) ⦈ |
Some _ ⇒ H
"

lemma hta_ensure_idx_f_correct_α[simp]:
"hta_α (hta_ensure_idx_f H) = hta_α H"
by (simp add: hta_ensure_idx_f_def hta_α_def split: option.split)
lemma hta_ensure_idx_s_correct_α[simp]:
"hta_α (hta_ensure_idx_s H) = hta_α H"
by (simp add: hta_ensure_idx_s_def hta_α_def split: option.split)
lemma hta_ensure_idx_sf_correct_α[simp]:
"hta_α (hta_ensure_idx_sf H) = hta_α H"
by (simp add: hta_ensure_idx_sf_def hta_α_def split: option.split)

lemma hta_ensure_idx_other[simp]:
"hta_Qi (hta_ensure_idx_f H) = hta_Qi H"
"hta_δ (hta_ensure_idx_f H) = hta_δ H"

"hta_Qi (hta_ensure_idx_s H) = hta_Qi H"
"hta_δ (hta_ensure_idx_s H) = hta_δ H"

"hta_Qi (hta_ensure_idx_sf H) = hta_Qi H"
"hta_δ (hta_ensure_idx_sf H) = hta_δ H"
by (auto
split: option.split)

― ‹Check whether the f-index is present›
definition "hta_has_idx_f H == hta_idx_f H ≠ None"
― ‹Check whether the s-index is present›
definition "hta_has_idx_s H == hta_idx_s H ≠ None"
― ‹Check whether the sf-index is present›
definition "hta_has_idx_sf H == hta_idx_sf H ≠ None"

lemma hta_idx_f_pres
[simp, intro!]: "hta_has_idx_f (hta_ensure_idx_f H)" and
[simp, intro]: "hta_has_idx_s H ⟹ hta_has_idx_s (hta_ensure_idx_f H)" and
[simp, intro]: "hta_has_idx_sf H ⟹ hta_has_idx_sf (hta_ensure_idx_f H)"
by (simp_all
hta_ensure_idx_f_def
split: option.split)

lemma hta_idx_s_pres
[simp, intro!]: "hta_has_idx_s (hta_ensure_idx_s H)" and
[simp, intro]: "hta_has_idx_f H ⟹ hta_has_idx_f (hta_ensure_idx_s H)" and
[simp, intro]: "hta_has_idx_sf H ⟹ hta_has_idx_sf (hta_ensure_idx_s H)"
by (simp_all
hta_ensure_idx_s_def
split: option.split)

lemma hta_idx_sf_pres
[simp, intro!]: "hta_has_idx_sf (hta_ensure_idx_sf H)" and
[simp, intro]: "hta_has_idx_f H ⟹ hta_has_idx_f (hta_ensure_idx_sf H)" and
[simp, intro]: "hta_has_idx_s H ⟹ hta_has_idx_s (hta_ensure_idx_sf H)"
by (simp_all
hta_ensure_idx_sf_def
split: option.split)

text ‹
The lookup functions are only defined if the required index is present.
This enforces generation of the index before applying lookup functions.
›
― ‹Lookup rules by function symbol›
definition "hta_lookup_f f H == hll_idx.lookup f (the (hta_idx_f H))"
― ‹Lookup rules by lhs-state›
definition "hta_lookup_s q H == hll_idx.lookup q (the (hta_idx_s H))"
― ‹Lookup rules by function symbol and lhs-state›
definition "hta_lookup_sf q f H == hll_idx.lookup (q,f) (the (hta_idx_sf H))"

― ‹This locale defines the invariants of a tree automaton›
locale hashedTa =
fixes H :: "('Q::hashable,'L::hashable) hashedTa"

― ‹The involved sets satisfy their invariants›
assumes invar[simp, intro!]:
"hs_invar (hta_Qi H)"
"ls_invar (hta_δ H)"

― ‹The indices are correct, if present›
assumes index_correct:
"hta_idx_f H = Some idx_f
⟹ hll_idx.is_index rhsl (ls_α (hta_δ H)) idx_f"
"hta_idx_s H = Some idx_s
⟹ hll_idx.is_index lhs (ls_α (hta_δ H)) idx_s"
"hta_idx_sf H = Some idx_sf
⟹ hll_idx.is_index (λr. (lhs r, rhsl r)) (ls_α (hta_δ H)) idx_sf"

begin
― ‹Inside this locale, some shorthand notations for the sets of
rules and initial states are used›
abbreviation "δ == hta_δ H"
abbreviation "Qi == hta_Qi H"

― ‹The lookup-xxx operations are correct›
lemma hta_lookup_f_correct:
"hta_has_idx_f H ⟹ ls_α (hta_lookup_f f H) = {r∈ls_α δ . rhsl r = f}"
"hta_has_idx_f H ⟹ ls_invar (hta_lookup_f f H)"
apply (cases "hta_has_idx_f H")
apply (unfold hta_has_idx_f_def hta_lookup_f_def)
apply (auto
index_def)
done

lemma hta_lookup_s_correct:
"hta_has_idx_s H ⟹ ls_α (hta_lookup_s q H) = {r∈ls_α δ . lhs r = q}"
"hta_has_idx_s H ⟹ ls_invar (hta_lookup_s q H)"
apply (cases "hta_has_idx_s H")
apply (unfold hta_has_idx_s_def hta_lookup_s_def)
apply (auto
index_def)
done

lemma hta_lookup_sf_correct:
"hta_has_idx_sf H
⟹ ls_α (hta_lookup_sf q f H) = {r∈ls_α δ . lhs r = q ∧ rhsl r = f}"
"hta_has_idx_sf H ⟹ ls_invar (hta_lookup_sf q f H)"
apply (cases "hta_has_idx_sf H")
apply (unfold hta_has_idx_sf_def hta_lookup_sf_def)
apply (auto
index_def)
done

― ‹The ensure-index operations preserve the invariants›
lemma hta_ensure_idx_f_correct[simp, intro!]: "hashedTa (hta_ensure_idx_f H)"
apply (unfold_locales)
apply (auto)
apply (auto
index_correct
split: option.split_asm)
done

lemma hta_ensure_idx_s_correct[simp, intro!]: "hashedTa (hta_ensure_idx_s H)"
apply (unfold_locales)
apply (auto)
apply (auto
index_correct
split: option.split_asm)
done

lemma hta_ensure_idx_sf_correct[simp, intro!]: "hashedTa (hta_ensure_idx_sf H)"
apply (unfold_locales)
apply (auto)
apply (auto
index_correct
split: option.split_asm)
done

text ‹The abstract tree automaton satisfies the invariants for an abstract
tree automaton›
lemma hta_α_is_ta[simp, intro!]: "tree_automaton (hta_α H)"
apply unfold_locales
apply (unfold hta_α_def)
apply auto
done

end

― ‹Add some lemmas to simpset -- also outside the locale›
lemmas [simp, intro] =
hashedTa.hta_ensure_idx_f_correct
hashedTa.hta_ensure_idx_s_correct
hashedTa.hta_ensure_idx_sf_correct

― ‹Build a tree automaton from a set of initial states and a set of rules›
definition "init_hta Qi δ ==
⦇ hta_Qi= Qi,
hta_δ = δ,
hta_idx_f = None,
hta_idx_s = None,
hta_idx_sf = None
⦈"

― ‹Building a tree automaton from a valid tree automaton yields again a
valid tree automaton. This operation has the only effect of removing
the indices.›
lemma (in hashedTa) init_hta_is_hta:
"hashedTa (init_hta (hta_Qi H) (hta_δ H))"
apply (unfold_locales)
apply (unfold init_hta_def)
apply (auto)
done

subsection "Algorithm for the Word Problem"

lemma r_match_by_laz: "r_match L l = list_all_zip (λQ q. q∈Q) L l"
by (unfold r_match_alt list_all_zip_alt)
auto

text "Executable function that computes the set of accepting states for
a given tree"
fun faccs' where
"faccs' H (NODE f ts) = (
let Qs = List.map (faccs' H) ts in
ll_set_xy.g_image_filter (λr. case r of (q → f' qs) ⇒
if list_all_zip (λQ q. ls_memb q Q) Qs qs then Some (lhs r) else None
)
(hta_lookup_f f H)
)"

― ‹Executable algorithm to decide the word-problem. The first version
depends on the f-index to be present, the second version computes the
index if not present.›
definition "hta_mem' t H == ¬lh_set_xx.g_disjoint (faccs' H t) (hta_Qi H)"
definition "hta_mem t H == hta_mem' t (hta_ensure_idx_f H)"

context hashedTa
begin

lemma faccs'_invar:
assumes HI[simp, intro!]: "hta_has_idx_f H"
shows "ls_invar (faccs' H t)" (is ?T1)
"list_all ls_invar (List.map (faccs' H) ts)" (is ?T2)
proof -
have "?T1 ∧ ?T2"
apply (induct rule: compat_tree_tree_list.induct)
apply (auto simp add: ll_set_xy.image_filter_correct hta_lookup_f_correct)
done
thus ?T1 ?T2 by auto
qed

declare faccs'_invar(1)[simp, intro]

lemma faccs'_correct:
assumes HI[simp, intro!]: "hta_has_idx_f H"
shows
"ls_α (faccs' H t) = faccs (ls_α (hta_δ H)) t" (is ?T1)
"List.map ls_α (List.map (faccs' H) ts)
= List.map (faccs (ls_α (hta_δ H))) ts" (is ?T2)
proof -
have "?T1 ∧ ?T2"
proof (induct rule: compat_tree_tree_list.induct)
case (NODE f ts)
let ?δ = "(ls_α (hta_δ H))"
have "faccs ?δ (NODE f ts) = (
let Qs = List.map (faccs ?δ) ts in
{q. ∃r∈?δ. r_matchc q f Qs r })"
by (rule faccs.simps)
also note NODE.hyps[symmetric]
finally have
1: "faccs ?δ (NODE f ts)
= ( let Qs = List.map ls_α (List.map (faccs' H) ts) in
{q. ∃r∈?δ. r_matchc q f Qs r })" .
{
fix Qsc:: "'Q ls list"
assume QI: "list_all ls_invar Qsc"
let ?Qs = "List.map ls_α Qsc"
have "{ q. ∃r∈?δ. r_matchc q f ?Qs r }
= { q. ∃qs. (q → f qs)∈?δ ∧ r_match ?Qs qs }"
apply (safe)
apply (case_tac r)
apply auto [1]
apply force
done
also have "… = lhs  { r∈{r∈?δ. rhsl r = f}.
case r of (q → f' qs) ⇒ r_match ?Qs qs}"
apply auto
apply force
apply (case_tac xa)
apply auto
done
finally have
1: "{ q. ∃r∈?δ. r_matchc q f ?Qs r }
= lhs  { r∈{r∈?δ. rhsl r = f}.
case r of (q → f' qs) ⇒ r_match ?Qs qs}"
by auto
from QI have
[simp]: "!!qs. list_all_zip (λQ q. q∈ls_α Q) Qsc qs
⟷ list_all_zip (λQ q. ls_memb q Q) Qsc qs"
apply (induct Qsc)
apply (case_tac qs)
apply auto [2]
apply (case_tac qs)
apply (auto simp add: ls.correct) [2]
done
have 2: "!!qs. r_match ?Qs qs = list_all_zip (λa b. ls_memb b a) Qsc qs"
apply (unfold r_match_by_laz)
done
from 1 have
"{ q. ∃r∈?δ. r_matchc q f ?Qs r }
= lhs  { r∈{r∈?δ. rhsl r = f}.
case r of (q → f' qs) ⇒
list_all_zip (λa b. ls_memb b a) Qsc qs}"
by (simp only: 2)
also have
"… = lhs  { r∈ls_α (hta_lookup_f f H).
case r of (q → f' qs) ⇒
list_all_zip (λa b. ls_memb b a) Qsc qs}"
also have
"… = ls_α ( ll_set_xy.g_image_filter
( λr. case r of (q → f' qs) ⇒
(if (list_all_zip (λQ q. ls_memb q Q) Qsc qs) then Some (lhs r) else None))
(hta_lookup_f f H)
)"
apply (auto split: ta_rule.split)
apply (rule_tac x=xa in exI)
apply auto
apply (case_tac a)
apply (rule_tac x=a in exI)
apply auto
done
finally have
"{ q. ∃r∈?δ. r_matchc q f ?Qs r }
= ls_α ( ll_set_xy.g_image_filter
(λr. case r of (q → f' qs) ⇒
(if (list_all_zip (λQ q. ls_memb q Q) Qsc qs) then Some (lhs r) else None))
(hta_lookup_f f H))" .
} note 2=this

from
1
2[ where Qsc2 = "(List.map (faccs' H) ts)",
simplified faccs'_invar[OF HI]]
show ?case by simp
qed simp_all
thus ?T1 ?T2 by auto
qed

― ‹Correctness of the algorithms for the word problem›
lemma hta_mem'_correct:
"hta_has_idx_f H ⟹ hta_mem' t H ⟷ t∈ta_lang (hta_α H)"
apply (unfold ta_lang_def hta_α_def hta_mem'_def)
apply (auto simp add: lh_set_xx.disjoint_correct faccs'_correct faccs_alt)
done

theorem hta_mem_correct: "hta_mem t H ⟷ t∈ta_lang (hta_α H)"
using hashedTa.hta_mem'_correct[OF hta_ensure_idx_f_correct, simplified]
apply (unfold hta_mem_def)
apply simp
done

end

subsection "Product Automaton and Intersection"

subsubsection "Brute Force Product Automaton"
text ‹
In this section, an algorithm that computes the product
automaton without reduction is implemented. While the runtime is always
quadratic, this algorithm is very simple and the constant factors are
smaller than that of the version with integrated reduction.
Moreover, lazy languages like Haskell seem to profit from this algorithm.
›

definition δ_prod_h
:: "('q1::hashable,'l::hashable) ta_rule ls
⇒ ('q2::hashable,'l) ta_rule ls ⇒ ('q1×'q2,'l) ta_rule ls"
where "δ_prod_h δ1 δ2 ==
lll_iflt_cp.inj_image_filter_cp (λ(r1,r2). r_prod r1 r2)
(λ(r1,r2). rhsl r1 = rhsl r2
∧ length (rhsq r1) = length (rhsq r2))
δ1 δ2"

lemma r_prod_inj:
"⟦ rhsl r1 = rhsl r2; length (rhsq r1) = length (rhsq r2);
rhsl r1' = rhsl r2'; length (rhsq r1') = length (rhsq r2');
r_prod r1 r2 = r_prod r1' r2' ⟧ ⟹ r1=r1' ∧ r2=r2'"
apply (cases r1, cases r2, cases r1', cases r2')
apply (auto dest: zip_inj)
done

lemma δ_prod_h_correct:
assumes INV[simp]: "ls_invar δ1" "ls_invar δ2"
shows
"ls_α (δ_prod_h δ1 δ2) = δ_prod (ls_α δ1) (ls_α δ2)"
"ls_invar (δ_prod_h δ1 δ2)"
apply (unfold δ_prod_def δ_prod_h_def)
apply (subst lll_iflt_cp.inj_image_filter_cp_correct)
apply simp_all [2]
using r_prod_inj
apply (auto intro!: inj_onI) []
apply auto []
apply (case_tac xa, case_tac y, simp, blast)
apply force
apply simp
done

definition "hta_prodWR H1 H2 ==
init_hta (hhh_cart.cart (hta_Qi H1) (hta_Qi H2)) (δ_prod_h (hta_δ H1) (hta_δ H2))"

lemma hta_prodWR_correct_aux:
assumes A: "hashedTa H1" "hashedTa H2"
shows
"hta_α (hta_prodWR H1 H2) = ta_prod (hta_α H1) (hta_α H2)" (is ?T1)
"hashedTa (hta_prodWR H1 H2)" (is ?T2)
proof -
interpret a1: hashedTa H1 + a2: hashedTa H2 using A .
show ?T1 ?T2
apply (unfold hta_prodWR_def init_hta_def hta_α_def ta_prod_def)
apply (unfold_locales)
done
qed

lemma hta_prodWR_correct:
assumes TA: "hashedTa H1" "hashedTa H2"
shows
"ta_lang (hta_α (hta_prodWR H1 H2))
= ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
"hashedTa (hta_prodWR H1 H2)"
by (simp_all add: hta_prodWR_correct_aux[OF TA] ta_prod_correct_aux1)

subsubsection "Product Automaton with Forward-Reduction"
text ‹
A more elaborated algorithm combines forward-reduction and the product
construction, i.e. product rules are only created ,,by need''.
›

― ‹State of the product-automaton DFS-algorithm›
type_synonym ('q1,'q2,'l) pa_state
= "('q1×'q2) hs × ('q1×'q2) list × ('q1×'q2,'l) ta_rule ls"

― ‹Abstraction mapping to algorithm specified in
Section~\ref{sec:absalgo}.›
definition pa_α
:: "('q1::hashable,'q2::hashable,'l::hashable) pa_state
⇒ ('q1,'q2,'l) frp_state"
where "pa_α S == let (Q,W,δd)=S in (hs_α Q,W,ls_α δd)"

definition pa_cond
:: "('q1::hashable,'q2::hashable,'l::hashable) pa_state ⇒ bool"
where "pa_cond S == let (Q,W,δd) = S in W≠[]"

― ‹Adds all successor states to the set of discovered states and to the
worklist›
fun pa_upd_rule
:: "('q1×'q2) hs ⇒ ('q1×'q2) list
⇒ (('q1::hashable)×('q2::hashable)) list
⇒ (('q1×'q2) hs × ('q1×'q2) list)"
where
"pa_upd_rule Q W [] = (Q,W)" |
"pa_upd_rule Q W (qp#qs) = (
if ¬ hs_memb qp Q then
pa_upd_rule (hs_ins qp Q) (qp#W) qs
else pa_upd_rule Q W qs
)"

definition pa_step
:: "('q1::hashable,'l::hashable) hashedTa
⇒ ('q2::hashable,'l) hashedTa
⇒ ('q1,'q2,'l) pa_state ⇒ ('q1,'q2,'l) pa_state"
where "pa_step H1 H2 S == let
(Q,W,δd)=S;
(q1,q2)=hd W
in
ls_iteratei (hta_lookup_s q1 H1) (λ_. True) (λr1 res.
ls_iteratei (hta_lookup_sf q2 (rhsl r1) H2) (λ_. True) (λr2 res.
if (length (rhsq r1) = length (rhsq r2)) then
let
rp=r_prod r1 r2;
(Q,W,δd) = res;
(Q',W') = pa_upd_rule Q W (rhsq rp)
in
(Q',W',ls_ins_dj rp δd)
else
res
) res
) (Q,tl W,δd)
"

definition pa_initial
:: "('q1::hashable,'l::hashable) hashedTa
⇒ ('q2::hashable,'l) hashedTa
⇒ ('q1,'q2,'l) pa_state"
where "pa_initial H1 H2 ==
let Qip = hhh_cart.cart (hta_Qi H1) (hta_Qi H2) in (
Qip,
hs_to_list Qip,
ls_empty ()
)"

"('q1::hashable,'q2::hashable,'l::hashable) pa_state set"
where "pa_invar_add == { (Q,W,δd). hs_invar Q ∧ ls_invar δd }"

definition "pa_invar H1 H2 ==
pa_invar_add ∩ {s. (pa_α s) ∈ frp_invar (hta_α H1) (hta_α H2)}"

definition "pa_det_algo H1 H2
== ⦇ dwa_cond=pa_cond,
dwa_step = pa_step H1 H2,
dwa_initial = pa_initial H1 H2,
dwa_invar = pa_invar H1 H2 ⦈"

lemma pa_upd_rule_correct:
assumes INV[simp, intro!]: "hs_invar Q"
assumes FMT: "pa_upd_rule Q W qs = (Q',W')"
shows
"hs_invar Q'" (is ?T1)
"hs_α Q' = hs_α Q ∪ set qs" (is ?T2)
"∃Wn. distinct Wn ∧ set Wn = set qs - hs_α Q ∧ W'=Wn@W" (is ?T3)
proof -
from INV FMT have "?T1 ∧ ?T2 ∧ ?T3"
proof (induct qs arbitrary: Q W Q' W')
case Nil thus ?case by simp
next
case (Cons q qs Q W Q' W')
show ?case
proof (cases "q∈hs_α Q")
case True
obtain Qh Wh where RF: "pa_upd_rule Q W qs = (Qh,Wh)" by force
with True Cons.prems have [simp]: "Q'=Qh" "W'=Wh"
from Cons.hyps[OF Cons.prems(1) RF] have
"hs_invar Qh"
"hs_α Qh = hs_α Q ∪ set qs"
"(∃Wn. distinct Wn ∧ set Wn = set qs - hs_α Q ∧ Wh = Wn @ W)"
by auto
thus ?thesis using True by auto
next
case False
with Cons.prems have RF: "pa_upd_rule (hs_ins q Q) (q#W) qs = (Q',W')"

from Cons.hyps[OF _ RF] Cons.prems(1) have
"hs_invar Q'"
"hs_α Q' = insert q (hs_α Q) ∪ set (qs)"
"∃Wn. distinct Wn
∧ set Wn = set qs - insert q (hs_α Q)
∧ W' = Wn @ q # W"
thus ?thesis using False by auto
qed
qed
thus ?T1 ?T2 ?T3 by auto
qed

lemma pa_step_correct:
assumes TA: "hashedTa H1" "hashedTa H2"
assumes idx[simp]: "hta_has_idx_s H1" "hta_has_idx_sf H2"
assumes INV: "(Q,W,δd)∈pa_invar H1 H2"
assumes COND: "pa_cond (Q,W,δd)"
shows
"(pa_step H1 H2 (Q,W,δd))∈pa_invar_add" (is ?T1)
"(pa_α (Q,W,δd), pa_α (pa_step H1 H2 (Q,W,δd)))
∈ frp_step (ls_α (hta_δ H1)) (ls_α (hta_δ H2))" (is ?T2)
proof -
interpret h1: hashedTa H1 by fact
interpret h2: hashedTa H2 by fact

from COND obtain q1 q2 Wtl where
[simp]: "W=(q1,q2)#Wtl"
by (cases W) (auto simp add: pa_cond_def)

from INV have [simp]: "hs_invar Q" "ls_invar δd"

define inv where "inv = (λδp (Q', W', δd').
hs_invar Q'
∧ ls_invar δd'
∧ (∃Wn. distinct Wn
∧ set Wn = (f_succ δp  {(q1,q2)}) - hs_α Q
∧ W'=Wn@Wtl
∧ hs_α Q'=hs_α Q ∪ (f_succ δp  {(q1,q2)}))
∧ (ls_α δd' = ls_α δd ∪ {r∈δp. lhs r = (q1,q2) }))"

have G: "inv (δ_prod (ls_α (hta_δ H1)) (ls_α (hta_δ H2)))
(pa_step H1 H2 (Q,W,δd))"
apply (unfold pa_step_def)
apply simp
apply (rule_tac
I="λit1 res. inv (δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))) res"
in ls.iterate_rule_P)
― ‹Invar›
― ‹Initial›
apply (fastforce simp add: inv_def δ_prod_def h1.hta_lookup_s_correct
f_succ_alt)
― ‹Step›
apply (rule_tac
I="λit2 res. inv ( δ_prod (ls_α (hta_δ H1) - it) (ls_α (hta_δ H2))
∪ δ_prod {x} (ls_α (hta_δ H2) - it2))
res"
in ls.iterate_rule_P)
― ‹Invar›
― ‹Init›
apply (case_tac σ)
apply (simp add: inv_def h1.hta_lookup_s_correct h2.hta_lookup_sf_correct)
apply (force simp add: f_succ_alt elim: δ_prodE intro: δ_prodI) [1]
― ‹Step›
defer ― ‹Requires considerably more work: Deferred to Isar proof below›
― ‹Final›
apply (auto) [1]
apply (subgoal_tac
"ls_α (hta_δ H1) - (it - {x}) = (ls_α (hta_δ H1) - it) ∪ {x}")
apply (subst Un_commute)
apply simp
apply blast
― ‹Final›
apply force
proof goal_cases
case prems: (1 r1 it1 resxh r2 it2 resh)
― ‹Resolve lookup-operations›
hence G':
"it1 ⊆ {r ∈ ls_α (hta_δ H1). lhs r = q1}"
"it2 ⊆ {r ∈ ls_α (hta_δ H2). lhs r = q2 ∧ rhsl r = rhsl r1}"

― ‹Basic reasoning setup›
from prems(1,4) G' have
[simp]: "ls_α (hta_δ H2) - (it2 - {r2}) = (ls_α (hta_δ H2) - it2) ∪ {r2}"
by auto
obtain Qh Wh δdh Q' W' δd' where [simp]: "resh=(Qh,Wh,δdh)"
by (cases resh) fastforce
from prems(6) have INVAH[simp]: "hs_invar Qh" "ls_invar δdh"

― ‹The involved rules have the same label, and their lhs is determined›
from prems(1,4) G' obtain l qs1 qs2 where
RULE_FMT: "r1 = (q1 → l qs1)" "r2=(q2 → l qs2)"
apply (cases r1, cases r2)
apply force
done

{
― ‹If the rhs have different lengths, the algorithm ignores the rule:›
assume LEN: "length (rhsq r1) ≠ length (rhsq r2)"

hence [simp]: "δ_prod_sng2 {r1} r2 = {}"
by (auto simp add: δ_prod_sng2_def split: ta_rule.split)

have ?case using prems
} moreover {
― ‹If the rhs have the same length, the rule is inserted›
assume LEN: "length (rhsq r1) = length (rhsq r2)"
hence [simp]: "length qs1 = length qs2" by (simp add: RULE_FMT)

hence [simp]: "δ_prod_sng2 {r1} r2 = {(q1,q2) → l (zip qs1 qs2)}"
using prems(1,4) G'
by (auto simp add: δ_prod_sng2_def RULE_FMT)

― ‹Obtain invariant of previous state›
from prems(6)[unfolded inv_def, simplified] obtain Wn where INVH:
"distinct Wn"
"set Wn = f_succ (δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))
∪ δ_prod {r1} (ls_α (hta_δ H2) - it2))
 {(q1, q2)} - hs_α Q"
"Wh = Wn @ Wtl"
"hs_α Qh = hs_α Q
∪ f_succ (δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))
∪ δ_prod {r1} (ls_α (hta_δ H2) - it2))
 {(q1, q2)}"
"ls_α δdh = ls_α δd
∪ {r. ( r ∈ δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))
∨ r ∈ δ_prod {r1} (ls_α (hta_δ H2) - it2)
) ∧ lhs r = (q1, q2)
}"
by blast

― ‹Required to justify disjoint insert›
have RPD: "r_prod r1 r2 ∉ ls_α δdh"
proof -
have LSDD:
"ls_α δd = {r ∈ δ_prod (ls_α (hta_δ H1)) (ls_α (hta_δ H2)).
lhs r ∈ hs_α Q - set W}"
by (auto simp add: pa_α_def hta_α_def)
have "r_prod r1 r2 ∉ ls_α δd"
proof
assume "r_prod r1 r2 ∈ ls_α δd"
with LSDD have "lhs (r_prod r1 r2) ∉ set W" by auto
moreover from prems(1,4) G' have "lhs (r_prod r1 r2) = (q1,q2)"
by (cases r1, cases r2) auto
ultimately show False by simp
qed
moreover from prems(6) have "ls_α δdh =
ls_α δd ∪
{r. ( r ∈ δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))
∨ r ∈ δ_prod {r1} (ls_α (hta_δ H2) - it2)
) ∧ lhs r = (q1, q2)}" (is "_= _ ∪ ?s")
moreover have "r_prod r1 r2 ∉ ?s" using prems(1,4) G'(2) LEN
apply (cases r1, cases r2)
done
ultimately show ?thesis by blast
qed

― ‹Correctness of result of @{text pa_upd_rule}›
obtain Q' W' where
PAUF: "(pa_upd_rule Qh Wh (rhsq (r_prod r1 r2))) = (Q',W')"
by force
from pa_upd_rule_correct[OF INVAH(1) PAUF] obtain Wnn where UC:
"hs_invar Q'"
"hs_α Q' = hs_α Qh ∪ set (rhsq (r_prod r1 r2))"
"distinct Wnn"
"set Wnn = set (rhsq (r_prod r1 r2)) - hs_α Qh"
"W' = Wnn @ Wh"
by blast

― ‹Put it all together›
have ?case
apply (simp add: LEN Let_def ls.ins_dj_correct[OF INVAH(2) RPD]
PAUF inv_def UC(1))
apply (intro conjI)
apply (rule_tac x="Wnn@Wn" in exI)
apply (auto simp add: f_succ_alt δ_prod_insert RULE_FMT UC INVH
δ_prod_sng2_def δ_prod_sng1_def)
done
} ultimately show ?case by blast
qed
from G show ?T1
by (cases "pa_step H1 H2 (Q,W,δd)")
from G show ?T2
by (cases "pa_step H1 H2 (Q,W,δd)")
(auto simp add: inv_def pa_α_def Let_def intro: frp_step.intros)

qed

― ‹The product-automaton algorithm is a precise implementation of its
specification›
lemma pa_pref_frp:
assumes TA: "hashedTa H1" "hashedTa H2"
assumes idx[simp]: "hta_has_idx_s H1" "hta_has_idx_sf H2"

shows "wa_precise_refine (det_wa_wa (pa_det_algo H1 H2))
(frp_algo (hta_α H1) (hta_α H2))
pa_α"
proof -
interpret h1: hashedTa H1 by fact
interpret h2: hashedTa H2 by fact

show ?thesis
apply (unfold_locales)
apply (auto simp add: det_wa_wa_def pa_det_algo_def pa_α_def
pa_cond_def frp_algo_def frp_cond_def) [1]
apply (auto simp add: det_wa_wa_def pa_det_algo_def pa_cond_def
hta_α_def frp_algo_def frp_cond_def
intro!: pa_step_correct(2)[OF TA]) [1]
apply (auto simp add: det_wa_wa_def pa_det_algo_def pa_α_def
hta_α_def pa_cond_def frp_algo_def frp_cond_def
pa_invar_def pa_step_def pa_initial_def
hs.correct ls.correct Let_def hhh_cart.cart_correct
intro: frp_initial.intros
) [3]
done
qed

― ‹The product automaton algorithm is a correct while-algorithm›
lemma pa_while_algo:
assumes TA: "hashedTa H1" "hashedTa H2"
assumes idx[simp]: "hta_has_idx_s H1" "hta_has_idx_sf H2"

shows "while_algo (det_wa_wa (pa_det_algo H1 H2))"
proof -
interpret h1: hashedTa H1 by fact
interpret h2: hashedTa H2 by fact

interpret ref: wa_precise_refine "(det_wa_wa (pa_det_algo H1 H2))"
"(frp_algo (hta_α H1) (hta_α H2))"
"pa_α"
using pa_pref_frp[OF TA idx] .
show ?thesis
apply (rule ref.wa_intro)
apply (simp add: det_wa_wa_def pa_det_algo_def pa_invar_def frp_algo_def)

apply (auto simp add: det_wa_wa_def pa_det_algo_def) [1]
apply (rule pa_step_correct(1)[OF TA idx])
apply (auto simp add: pa_invar_def frp_algo_def) [2]

apply (simp add: det_wa_wa_def pa_det_algo_def pa_initial_def
done
qed

― ‹By definition, the product automaton algorithm is deterministic›
lemmas pa_det_while_algo = det_while_algo_intro[OF pa_while_algo]

― ‹Transferred correctness lemma›
lemmas pa_inv_final =
wa_precise_refine.transfer_correctness[OF pa_pref_frp frp_inv_final]

― ‹The next two definitions specify the product-automata algorithm. The first
version requires the s-index of the first and the sf-index of the second
automaton to be present, while the second version computes the required
indices, if necessary›
definition "hta_prod' H1 H2 ==
let (Q,W,δd) = while pa_cond (pa_step H1 H2) (pa_initial H1 H2) in
init_hta (hhh_cart.cart (hta_Qi H1) (hta_Qi H2)) δd
"

definition "hta_prod H1 H2 ==
hta_prod' (hta_ensure_idx_s H1) (hta_ensure_idx_sf H2)"

lemma hta_prod'_correct_aux:
assumes TA: "hashedTa H1" "hashedTa H2"
assumes idx: "hta_has_idx_s H1" "hta_has_idx_sf H2"
shows "hta_α (hta_prod' H1 H2)
= ta_fwd_reduce (ta_prod (hta_α H1) (hta_α H2))" (is ?T1)
"hashedTa (hta_prod' H1 H2)" (is ?T2)
proof -
interpret h1: hashedTa H1 by fact
interpret h2: hashedTa H2 by fact

interpret dwa: det_while_algo "pa_det_algo H1 H2"
using pa_det_while_algo[OF TA idx] .

have LC: "while pa_cond (pa_step H1 H2) (pa_initial H1 H2) = dwa.loop"
by (unfold dwa.loop_def)

from dwa.while_proof'[OF pa_inv_final[OF TA idx]]
show ?T1
apply (unfold dwa.loop_def)
apply (simp add: hta_prod'_def init_hta_def hta_α_def pa_det_algo_def)
apply (cases "(while pa_cond (pa_step H1 H2) (pa_initial H1 H2))")
apply (simp add: pa_α_def hhh_cart.cart_correct hta_α_def)
done

show ?T2
apply (rule dwa.while_proof)
apply (case_tac s)
apply unfold_locales
done
qed

theorem hta_prod'_correct:
assumes TA: "hashedTa H1" "hashedTa H2"
assumes HI: "hta_has_idx_s H1" "hta_has_idx_sf H2"
shows
"ta_lang (hta_α (hta_prod' H1 H2))
= ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"

"hashedTa (hta_prod' H1 H2)"
by (simp_all add: hta_prod'_correct_aux[OF TA HI] ta_prod_correct_aux1)

lemma hta_prod_correct_aux:
assumes TA[simp]: "hashedTa H1" "hashedTa H2"
shows
"hta_α (hta_prod H1 H2) = ta_fwd_reduce (ta_prod (hta_α H1) (hta_α H2))"
"hashedTa (hta_prod H1 H2)"
by (unfold hta_prod_def)

theorem hta_prod_correct:
assumes TA: "hashedTa H1" "hashedTa H2"
shows
"ta_lang (hta_α (hta_prod H1 H2))
= ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
"hashedTa (hta_prod H1 H2)"
by (simp_all add: hta_prod_correct_aux[OF TA] ta_prod_correct_aux1)

subsection "Remap States"

― ‹Mapping the states of an automaton›
definition hta_remap
:: "('q::hashable ⇒ 'qn::hashable) ⇒ ('q,'l::hashable) hashedTa
⇒ ('qn,'l) hashedTa"
where "hta_remap f H ==
init_hta (hh_set_xy.g_image f (hta_Qi H))
(ll_set_xy.g_image (remap_rule f) (hta_δ H))"

lemma (in hashedTa) hta_remap_correct:
shows "hta_α (hta_remap f H) = ta_remap f (hta_α H)"
"hashedTa (hta_remap f H)"
apply (auto
hh_set_xy.image_correct ll_set_xy.image_correct ta_remap_def)
apply (unfold_locales)
apply (auto simp add: hh_set_xy.image_correct ll_set_xy.image_correct)
done

subsubsection "Reindex Automaton"
text ‹
In this section, an algorithm for re-indexing the states of the automaton to
an initial segment of the naturals is implemented. The language of the
automaton is not changed by the reindexing operation.
›

― ‹Set of states of a rule›
fun rule_states_l where
"rule_states_l (q → f qs) = ls_ins q (ls.from_list qs)"

lemma rule_states_l_correct[simp]:
"ls_α (rule_states_l r) = rule_states r"
"ls_invar (rule_states_l r)"
by (cases r, simp add: ls.correct)+

definition "hta_δ_states H
== (llh_set_xyy.g_Union_image id (ll_set_xy.g_image_filter
(λr. Some (rule_states_l r)) (hta_δ H)))"

definition "hta_states H ==
hs_union (hta_Qi H) (hta_δ_states H)"

lemma (in hashedTa) hta_δ_states_correct:
"hs_α (hta_δ_states H) = δ_states (ta_rules (hta_α H))"
"hs_invar (hta_δ_states H)"
proof (simp_all add: hta_α_def hta_δ_states_def, goal_cases)
case 1
have
[simp]: "ls_α (ll_set_xy.g_image_filter (λx. Some (rule_states_l x)) δ)
= rule_states_l  ls_α δ"
show ?case
apply (subst
llh_set_xyy.Union_image_correct[
of "(ll_set_xy.g_image_filter (λx. Some (rule_states_l x)) δ)",
simplified])
done
(*next
case goal2 thus ?case
apply (rule llh.Union_image_correct)
done*)
qed

lemma (in hashedTa) hta_states_correct:
"hs_α (hta_states H) = ta_rstates (hta_α H)"
"hs_invar (hta_states H)"
by (simp_all
hta_α_def)

definition "reindex_map H ==
λq. the (hm_lookup q (hh_map_to_nat.map_to_nat (hta_states H)))"

definition hta_reindex
:: "('Q::hashable,'L::hashable) hashedTa ⇒ (nat,'L) hashedTa" where
"hta_reindex H == hta_remap (reindex_map H) H"

declare hta_reindex_def [code del]

― ‹This version is more efficient, as the map is only computed once›
lemma [code]: "hta_reindex H = (
let mp = (hh_map_to_nat.map_to_nat (hta_states H)) in
hta_remap (λq. the (hm_lookup q mp)) H)
"
by (simp add: Let_def hta_reindex_def reindex_map_def)

lemma (in hashedTa) reindex_map_correct:
"inj_on (reindex_map H) (ta_rstates (hta_α H))"
proof -
have [simp]:
"reindex_map H = the ∘ hm_α (hh_map_to_nat.map_to_nat (hta_states H))"
by (rule ext)
hh_map_to_nat.map_to_nat_correct(4)
hta_states_correct)

show ?thesis
apply (rule inj_on_map_the)
done
qed

theorem (in hashedTa) hta_reindex_correct:
"ta_lang (hta_α (hta_reindex H)) = ta_lang (hta_α H)"
"hashedTa (hta_reindex H)"
apply (unfold hta_reindex_def)
apply (simp_all
reindex_map_correct)
done

subsection "Union"

text "Computes the union of two automata"
definition hta_union
:: "('q1::hashable,'l::hashable) hashedTa
⇒ ('q2::hashable,'l) hashedTa
⇒ (('q1,'q2) ustate_wrapper,'l) hashedTa"
where "hta_union H1 H2 ==
init_hta (hs_union (hh_set_xy.g_image USW1 (hta_Qi H1))
(hh_set_xy.g_image USW2 (hta_Qi H2)))
(ls_union_dj (ll_set_xy.g_image (remap_rule USW1) (hta_δ H1))
(ll_set_xy.g_image (remap_rule USW2) (hta_δ H2)))"

lemma hta_union_correct':
assumes TA: "hashedTa H1" "hashedTa H2"
shows "hta_α (hta_union H1 H2)
= ta_union_wrap (hta_α H1) (hta_α H2)" (is ?T1)
"hashedTa (hta_union H1 H2)" (is ?T2)
proof -
interpret a1: hashedTa H1 + a2: hashedTa H2 using TA .
show ?T1 ?T2
apply (auto
hs.correct ls.correct
ll_set_xy.image_correct hh_set_xy.image_correct
ta_remap_def ta_union_def ta_union_wrap_def)
apply (unfold_locales)
apply (auto
done
qed

theorem hta_union_correct:
assumes TA: "hashedTa H1" "hashedTa H2"
shows
"ta_lang (hta_α (hta_union H1 H2))
= ta_lang (hta_α H1) ∪ ta_lang (hta_α H2)" (is ?T1)
"hashedTa (hta_union H1 H2)" (is ?T2)
proof -
interpret a1: hashedTa H1 + a2: hashedTa H2 using TA .
show ?T1 ?T2
by (simp_all add: hta_union_correct'[OF TA] ta_union_wrap_correct)
qed

subsection "Operators to Construct Tree Automata"
text ‹
This section defines operators that add initial states and rules to a tree
automaton, and thus incrementally construct a tree automaton from the empty
automaton.
›

― ‹The empty automaton›
definition hta_empty :: "unit ⇒ ('q::hashable,'l::hashable) hashedTa"
where "hta_empty u == init_hta (hs_empty ()) (ls_empty ())"
lemma hta_empty_correct [simp, intro!]:
shows "(hta_α (hta_empty ())) = ta_empty"
"hashedTa (hta_empty ())"
apply (auto
simp add: init_hta_def hta_empty_def hta_α_def δ_states_def ta_empty_def
hs.correct ls.correct)
apply (unfold_locales)
apply (auto simp add: hs.correct ls.correct)
done

― ‹Add an initial state to the automaton›
:: "'q ⇒ ('q::hashable,'l::hashable) hashedTa ⇒ ('q,'l) hashedTa"
where "hta_add_qi qi H == init_hta (hs_ins qi (hta_Qi H)) (hta_δ H)"

= ⦇ ta_initial = insert qi (ta_initial (hta_α H)),
ta_rules = ta_rules (hta_α H)
⦈"
apply (auto
hs.correct)
apply (unfold_locales)
done

― ‹Add a rule to the automaton›
:: "('q,'l) ta_rule ⇒ ('q::hashable,'l::hashable) hashedTa
⇒ ('q,'l) hashedTa"
where "hta_add_rule r H == init_hta (hta_Qi H) (ls_ins r (hta_δ H))"

= ⦇ ta_initial = ta_initial (hta_α H),
ta_rules = insert r (ta_rules (hta_α H))
⦈"
apply (auto
δ_states_def ls.correct)
apply (unfold_locales)
done

― ‹Reduces an automaton to the given set of states›
definition "hta_reduce H Q ==
init_hta (hs_inter Q (hta_Qi H))
(ll_set_xy.g_image_filter
(λr. if hs_memb (lhs r) Q ∧ list_all (λq. hs_memb q Q) (rhsq r) then Some r else None)
(hta_δ H))
"

theorem (in hashedTa) hta_reduce_correct:
assumes INV[simp]: "hs_invar Q"
shows
"hta_α (hta_reduce H Q) = ta_reduce (hta_α H) (hs_α Q)" (is ?T1)
"hashedTa (hta_reduce H Q)" (is ?T2)
apply (auto
hta_reduce_def ta_reduce_def hta_α_def init_hta_def
hs.correct ls.correct
(*hs_correct ls_correct *)
list_all_iff
reduce_rules_def rule_states_simp
ll_set_xy.image_filter_correct
split:
ta_rule.split_asm
) [1]
apply (unfold_locales)
apply (unfold hta_reduce_def init_hta_def)
apply (auto simp add: hs.correct ls.correct)
done

subsection "Backwards Reduction and Emptiness Check"

text ‹
The algorithm uses a map from states to the set of rules that contain
the state on their rhs.
›

― ‹Add an entry to the index›
definition "rqrm_add q r res ==
case hm_lookup q res of
None ⇒ hm_update q (ls_ins r (ls_empty ())) res |
Some s ⇒ hm_update q (ls_ins r s) res
"

― ‹Lookup the set of rules with given state on rhs›
definition "rqrm_lookup rqrm q == case hm_lookup q rqrm of
None ⇒ ls_empty () |
Some s ⇒ s
"

― ‹Build the index from a set of rules›
definition build_rqrm
:: "('q::hashable,'l::hashable) ta_rule ls
⇒ ('q,('q,'l) ta_rule ls) hm"
where
"build_rqrm δ ==
ls_iteratei δ (λ_. True)
(λr res.
foldl (λres q. rqrm_add q r res) res (rhsq r)
)
(hm_empty ())
"

― ‹Whether the index satisfies the map and set invariants›
definition "rqrm_invar rqrm ==
hm_invar rqrm ∧ (∀q. ls_invar (rqrm_lookup rqrm q))"
― ‹Whether the index really maps a state to the set of rules with this
state on their rhs›
definition "rqrm_prop δ rqrm ==
∀q. ls_α (rqrm_lookup rqrm q) = {r∈δ. q∈set (rhsq r)}"

lemma rqrm_α_lookup_update[simp]:
"rqrm_invar rqrm ⟹
ls_α (rqrm_lookup (rqrm_add q r rqrm) q')
= ( if q=q' then
insert r (ls_α (rqrm_lookup rqrm q'))
else
ls_α (rqrm_lookup rqrm q')
)"
by (simp
ls.correct
split: option.split_asm option.split)

lemma rqrm_propD:
"rqrm_prop δ rqrm ⟹ ls_α (rqrm_lookup rqrm q) = {r∈δ. q∈set (rhsq r)}"

lemma build_rqrm_correct:
fixes δ
assumes [simp]: "ls_invar δ"
shows "rqrm_invar (build_rqrm δ)" (is ?T1) and
"rqrm_prop (ls_α δ) (build_rqrm δ)" (is ?T2)
proof -
have "rqrm_invar (build_rqrm δ) ∧
(∀q. ls_α (rqrm_lookup (build_rqrm δ) q) = {r∈ls_α δ. q∈set (rhsq r)})"
apply (unfold build_rqrm_def)
apply (rule_tac
I="λit res. (rqrm_invar res)
∧ (∀q. ls_α (rqrm_lookup res q)
= {r∈ls_α δ - it. q∈set (rhsq r)})"
in ls.iterate_rule_P)
― ‹Invar›
apply simp
― ‹Initial›
apply (simp add: hm_correct ls_correct rqrm_lookup_def rqrm_invar_def)
― ‹Step›
apply (rule_tac
I="λres itl itr.
(rqrm_invar res)
∧ (∀q. ls_α (rqrm_lookup res q)
= {r∈ls_α δ - it. q∈set (rhsq r)}
∪ {r. r=x ∧ q∈set itl})"
in Misc.foldl_rule_P)
― ‹Initial›
apply simp
― ‹Step›
apply (intro conjI)
apply (simp
ls_correct
split: option.split option.split_asm)
apply simp
apply (simp
split: option.split option.split_asm)
apply (auto) [1]
― ‹Final›
apply auto [1]
― ‹Final›
apply simp
done
thus ?T1 ?T2 by (simp_all add: rqrm_prop_def)
qed

― ‹A state of the basic algorithm contains a set of discovered states,
a worklist and a map from rules to the number of distinct states on
its RHS that have not yet been discovered or are still on the worklist›
type_synonym ('Q,'L) brc_state
= "'Q hs × 'Q list × (('Q,'L) ta_rule, nat) hm"

― ‹Abstraction to @{text α'}-level:›
definition brc_α
:: "('Q::hashable,'L::hashable) brc_state ⇒ ('Q,'L) br'_state"
where "brc_α == λ(Q,W,rcm). (hs_α Q, set W, hm_α rcm)"

definition brc_invar_add :: "('Q::hashable,'L::hashable) brc_state set"
where
hs_invar Q ∧
distinct W ∧
hm_invar rcm
⌦‹∧ set W ⊆ hs_α Q›}
"

definition "brc_invar δ == brc_invar_add ∩ {s. brc_α s ∈ br'_invar δ}"

definition brc_cond :: "('q::hashable,'l::hashable) brc_state ⇒ bool"
where "brc_cond == λ(Q,W,rcm). W≠[]"

definition brc_inner_step
:: "('q,'l) ta_rule ⇒ ('q::hashable,'l::hashable) brc_state
⇒ ('q,'l) brc_state"
where
"brc_inner_step r == λ(Q,W,rcm).
let c=the (hm_lookup r rcm);
rcm' = hm_update r (c-(1::nat)) rcm;
Q' = (if c ≤ 1 then hs_ins (lhs r) Q else Q);
W' = (if c ≤ 1 ∧ ¬ hs_memb (lhs r) Q then lhs r # W else W) in
(Q',W',rcm')"

definition brc_step
:: "('q,('q,'l) ta_rule ls) hm
⇒ ('q::hashable,'l::hashable) brc_state
⇒ ('q,'l) brc_state"
where
"brc_step rqrm == λ(Q,W,rcm).
ls_iteratei (rqrm_lookup rqrm (hd W)) (λ_. True) brc_inner_step
(Q,tl W, rcm)"

― ‹Initial concrete state›
definition brc_iq :: "('q,'l) ta_rule ls ⇒ 'q::hashable hs"
where "brc_iq δ == lh_set_xy.g_image_filter (λr.
if rhsq r = [] then Some (lhs r) else None) δ"

definition brc_rcm_init
:: "('q::hashable,'l::hashable) ta_rule ls
⇒ (('q,'l) ta_rule,nat) hm"
where "brc_rcm_init δ ==
ls_iteratei δ (λ_. True)
(λr res. hm_update r ((length (remdups (rhsq r)))) res)
(hm_empty ())"

definition brc_initial
:: "('q::hashable,'l::hashable) ta_rule ls ⇒ ('q,'l) brc_state"
where "brc_initial δ ==
let iq=brc_iq δ in
(iq, hs_to_list (iq), brc_rcm_init δ)"

definition "brc_det_algo rqrm δ == ⦇
dwa_cond = brc_cond,
dwa_step = brc_step rqrm,
dwa_initial = brc_initial δ,
dwa_invar = brc_invar (ls_α δ)
⦈"

― ‹Additional facts needed from the abstract level›
lemma brc_inv_imp_WssQ: "brc_α (Q,W,rcm)∈br'_invar δ ⟹ set W ⊆ hs_α Q"
by (auto simp add: brc_α_def br'_invar_def br'_α_def br_invar_def)

lemma brc_iq_correct:
assumes [simp]: "ls_invar δ"
shows "hs_invar (brc_iq δ)"
"hs_α (brc_iq δ) = br_iq (ls_α δ)"
by (auto simp add: brc_iq_def br_iq_def lh_set_xy.image_filter_correct)

lemma brc_rcm_init_correct:
assumes INV[simp]: "ls_invar δ"
shows "r∈ls_α δ
⟹ hm_α (brc_rcm_init δ) r = Some ((card (set (rhsq r))))"
(is "_ ⟹ ?T1 r") and
"hm_invar (brc_rcm_init δ)" (is ?T2)
proof -
have G: "(∀r∈ls_α δ. ?T1 r) ∧ ?T2"
apply (unfold brc_rcm_init_def)
apply (rule_tac
I="λit res. hm_invar res
∧ (∀r∈ls_α δ - it. hm_α res r = Some ((card (set (rhsq r)))))"
in ls.iterate_rule_P)
― ‹Invar›
apply simp
― ‹Init›
apply (auto simp add: hm_correct) [1]
― ‹Step›
apply (rule conjI)

apply (simp only: hm_correct hs_correct INV)
apply (rule ballI)
apply (case_tac "r=x")
apply (auto
intro!: arg_cong[where f=card]) [1]
apply simp
― ‹Final›
apply simp
done
from G show ?T2 by auto
fix r
assume "r∈ls_α δ"
thus "?T1 r" using G by auto
qed

lemma brc_inner_step_br'_desc:
"⟦ (Q,W,rcm)∈brc_invar δ ⟧ ⟹ brc_α (brc_inner_step r (Q,W,rcm)) = (
if the (hm_α rcm r) ≤ 1 then
insert (lhs r) (hs_α Q)
else hs_α Q,
if the (hm_α rcm r) ≤ 1 ∧ (lhs r) ∉ hs_α Q then
insert (lhs r) (set W)
else (set W),
((hm_α rcm)(r ↦ the (hm_α rcm r) - 1))
)"
by (simp
hs_correct hm_correct)

lemma brc_step_invar:
assumes RQRM: "rqrm_invar rqrm"
shows "⟦ Σ∈brc_invar_add; brc_α Σ∈br'_invar δ; brc_cond Σ ⟧
apply (cases Σ)
apply (rule_tac I="λit (Q,W,rcm). (Q,W,rcm)∈brc_invar_add ∧ set W ⊆ hs_α Q"
in ls.iterate_rule_P)
apply (case_tac b)
dest!: brc_inv_imp_WssQ) [1]
apply (case_tac σ)
Let_def hs_correct hm_correct) [1]
apply (case_tac σ)
apply simp
done

lemma brc_step_abs:
assumes RQRM: "rqrm_invar rqrm" "rqrm_prop δ rqrm"
assumes A: "Σ∈brc_invar δ" "brc_cond Σ"
shows "(brc_α Σ, brc_α (brc_step rqrm Σ)) ∈ br'_step δ"
proof -
obtain Q W rcm where [simp]: "Σ=(Q,W,rcm)" by (cases Σ) auto
from A show ?thesis
apply (rule
br'_inner_step_proof[OF ls.v1_iteratei_impl,
∧ set W ⊆ hs_α Q" and
q="hd W"])
apply (case_tac W)
dest!: brc_inv_imp_WssQ) [2]
prefer 6
apply (case_tac Σ)
apply (auto
Let_def hm_correct hs_correct) [1]
apply (auto
br'_inner_step_def Let_def hm_correct hs_correct) [1]
apply (case_tac W)
apply (simp_all add: brc_α_def brc_cond_def brc_invar_def) [2]
apply (case_tac W)
apply (simp_all add: brc_α_def brc_cond_def brc_invar_def
done
qed

lemma brc_initial_invar: "ls_invar δ ⟹ (brc_initial δ)∈brc_invar_add"
by (simp
brc_rcm_init_correct hs_correct)

lemma brc_cond_abs: "brc_cond Σ ⟷ (brc_α Σ)∈br'_cond"
apply (cases Σ)
apply (simp add: brc_cond_def br'_cond_def brc_α_def)
done

lemma brc_initial_abs:
"ls_invar δ ⟹ brc_α (brc_initial δ) ∈ br'_initial (ls_α δ)"
by (auto
simp add: brc_initial_def Let_def brc_α_def brc_iq_correct
brc_rcm_init_correct hs_correct
intro: br'_initial.intros)

lemma brc_pref_br':
assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
assumes INV[simp]: "ls_invar δ"
shows "wa_precise_refine (det_wa_wa (brc_det_algo rqrm δ))
(br'_algo (ls_α δ))
brc_α"
apply (unfold_locales)
apply (simp_all add: brc_det_algo_def br'_algo_def det_wa_wa_def)
apply (auto simp add: brc_step_abs[OF RQRM]) [1]
apply (auto simp add: brc_invar_def) [1]
done

lemma brc_while_algo:
assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
assumes INV[simp]: "ls_invar δ"
shows "while_algo (det_wa_wa (brc_det_algo rqrm δ))"
proof -
from brc_pref_br'[OF RQRM INV] interpret
ref: wa_precise_refine "(det_wa_wa (brc_det_algo rqrm δ))"
"(br'_algo (ls_α δ))"
brc_α .
show ?thesis
apply (rule ref.wa_intro)
apply (simp_all add: det_wa_wa_def brc_det_algo_def br'_algo_def)
apply (auto simp add: brc_step_invar) [1]
done
qed

lemmas brc_det_while_algo =
det_while_algo_intro[OF brc_while_algo]

lemma fst_brc_α: "fst (brc_α s) = hs_α (fst s)"
by (cases s) (simp add: brc_α_def)

lemmas brc_invar_final =
wa_precise_refine.transfer_correctness[OF
brc_pref_br' br'_invar_final, unfolded fst_brc_α]

definition "hta_bwd_reduce H ==
let rqrm = build_rqrm (hta_δ H) in
hta_reduce
H
(fst (while brc_cond (brc_step rqrm) (brc_initial (hta_δ H))))
"

theorem (in hashedTa) hta_bwd_reduce_correct:
shows "hta_α (hta_bwd_reduce H)
= ta_reduce (hta_α H) (b_accessible (ls_α (hta_δ H)))" (is ?T1)
"hashedTa (hta_bwd_reduce H)" (is ?T2)
proof -
interpret det_while_algo "(brc_det_algo (build_rqrm δ) δ)"
by (rule brc_det_while_algo)

have LC: "(while brc_cond (brc_step (build_rqrm δ)) (brc_initial δ)) = loop"
by (unfold loop_def)

from while_proof'[OF brc_invar_final] have
G1: "hs_α (fst loop) = b_accessible (ls_α δ)"
have G2: "loop ∈ brc_invar (ls_α δ)"
by (rule while_proof)
hence [simp]: "hs_invar (fst loop)"
by (cases loop)

show ?T1 ?T2
by (simp_all add: hta_bwd_reduce_def LC hta_reduce_correct G1)

qed

subsubsection ‹Emptiness Check with Witness Computation›

definition brec_construct_witness
:: "('q::hashable,'l::hashable tree) hm ⇒ ('q,'l) ta_rule ⇒ 'l tree"
where "brec_construct_witness Qm r ==
NODE (rhsl r) (List.map (λq. the (hm_lookup q Qm)) (rhsq r))"

lemma brec_construct_witness_correct:
"⟦hm_invar Qm⟧ ⟹
brec_construct_witness Qm r = construct_witness (hm_α Qm) r"
by (auto

type_synonym ('Q,'L) brec_state
= "(('Q,'L tree) hm
× 'Q fifo
× (('Q,'L) ta_rule, nat) hm
× 'Q option)"

― ‹Abstractions›
definition brec_α
:: "('Q::hashable,'L::hashable) brec_state ⇒ ('Q,'L) brw_state"
where "brec_α == λ(Q,W,rcm,f). (hm_α Q, set (fifo_α W), (hm_α rcm))"

definition brec_inner_step
:: "'q hs ⇒ ('q,'l) ta_rule
⇒ ('q::hashable,'l::hashable) brec_state
⇒ ('q,'l) brec_state"
where "brec_inner_step Qi r == λ(Q,W,rcm,qwit).
let c=the (hm_lookup r rcm);
cond = c ≤ 1 ∧ hm_lookup (lhs r) Q = None;
rcm' = hm_update r (c-(1::nat)) rcm;
Q' = ( if cond then
hm_update (lhs r) (brec_construct_witness Q r) Q
else Q);
W' = (if cond then fifo_enqueue (lhs r) W else W);
qwit' = (if c ≤ 1 ∧ hs_memb (lhs r) Qi then Some (lhs r) else qwit)
in
(Q',W',rcm',qwit')"

definition brec_step
:: "('q,('q,'l) ta_rule ls) hm ⇒ 'q hs
⇒ ('q::hashable,'l::hashable) brec_state
⇒ ('q,'l) brec_state"
where "brec_step rqrm Qi == λ(Q,W,rcm,qwit).
let (q,W')=fifo_dequeue W in
ls_iteratei (rqrm_lookup rqrm q) (λ_. True)
(brec_inner_step Qi) (Q,W',rcm,qwit)
"

definition brec_iqm
:: "('q::hashable,'l::hashable) ta_rule ls ⇒ ('q,'l tree) hm"
where "brec_iqm δ ==
ls_iteratei δ (λ_. True) (λr m. if rhsq r = [] then
hm_update (lhs r) (NODE (rhsl r) []) m
else m)
(hm_empty ())"

definition brec_initial
:: "'q hs ⇒ ('q::hashable,'l::hashable) ta_rule ls
⇒ ('q,'l) brec_state"
where "brec_initial Qi δ ==
let iq=brc_iq δ in
( brec_iqm δ,
hs_to_fifo.g_set_to_listr iq,
brc_rcm_init δ,
hh_set_xx.g_disjoint_witness iq Qi)"

definition brec_cond
:: "('q,'l) brec_state ⇒ bool"
where "brec_cond == λ(Q,W,rcm,qwit). ¬ fifo_isEmpty W ∧ qwit = None"

:: "'Q set ⇒ ('Q::hashable,'L::hashable) brec_state set"
where
hm_invar Q ∧
distinct (fifo_α W) ∧
hm_invar rcm ∧
( case qwit of
None ⇒ Qi ∩ dom (hm_α Q) = {} |
Some q ⇒ q∈Qi ∩ dom (hm_α Q))}
"

definition "brec_invar Qi δ == brec_invar_add Qi ∩ {s. brec_α s ∈ brw_invar δ}"

definition "brec_invar_inner Qi ==
brec_invar_add Qi ∩ {(Q,W,_,_). set (fifo_α W) ⊆ dom (hm_α Q)}"

lemma brec_invar_cons:
"Σ∈brec_invar Qi δ ⟹ Σ∈brec_invar_inner Qi"
apply (cases Σ)
apply (simp add: brec_invar_def brw_invar_def br'_invar_def br_invar_def
brec_α_def brw_α_def br'_α_def brec_invar_inner_def)
done

lemma brec_brw_invar_cons:
"brec_α Σ ∈ brw_invar Qi ⟹ set (fifo_α (fst (snd Σ))) ⊆ dom (hm_α (fst Σ))"
apply (cases Σ)
apply (simp add: brec_invar_def brw_invar_def br'_invar_def br_invar_def
brec_α_def brw_α_def br'_α_def)
done

definition "brec_det_algo rqrm Qi δ == ⦇
dwa_cond=brec_cond,
dwa_step=brec_step rqrm Qi,
dwa_initial=brec_initial Qi δ,
dwa_invar=brec_invar (hs_α Qi) (ls_α δ)
⦈"

lemma brec_iqm_correct':
assumes INV[simp]: "ls_invar δ"
shows
"dom (hm_α (brec_iqm δ)) = {lhs r | r. r∈ls_α δ ∧ rhsq r = []}" (is ?T1)
"witness_prop (ls_α δ) (hm_α (brec_iqm δ))" (is ?T2)
"hm_invar (brec_iqm δ)" (is ?T3)
proof -
have "?T1 ∧ ?T2 ∧ ?T3"
apply (unfold brec_iqm_def)
apply (rule_tac
I="λit m. hm_invar m
∧ dom (hm_α m) = {lhs r | r. r∈ls_α δ - it ∧ rhsq r = []}
∧ witness_prop (ls_α δ) (hm_α m)"
in ls.iterate_rule_P)
apply simp
apply (auto simp add: hm_correct witness_prop_def) [1]
apply (auto simp add: hm_correct witness_prop_def) [1]
apply (case_tac x)
apply (auto intro: accs.intros) [1]
apply simp
done
thus ?T1 ?T2 ?T3 by auto
qed

lemma brec_iqm_correct:
assumes INV[simp]: "ls_invar δ"
shows "hm_α (brec_iqm δ) ∈ brw_iq (ls_α δ)"
proof -
have "(∀q t. hm_α (brec_iqm δ) q = Some t
⟶ (∃r∈ls_α δ. rhsq r = [] ∧ q = lhs r ∧ t = NODE (rhsl r) []))
∧ (∀r∈ls_α δ. rhsq r = [] ⟶ hm_α (brec_iqm δ) (lhs r) ≠ None)"
apply (unfold brec_iqm_def)
apply (rule_tac I="λit m. (
(hm_invar m) ∧
(∀q t. hm_α m q = Some t
⟶ (∃r∈ls_α δ. rhsq r = [] ∧ q = lhs r ∧ t = NODE (rhsl r) [])) ∧
(∀r∈ls_α δ-it. rhsq r = [] ⟶ hm_α m (lhs r) ≠ None)
)"
in ls.iterate_rule_P)
apply simp
apply (auto simp add: hm_correct) [1]
apply (auto simp add: hm_correct) [1]
done
thus ?thesis by (blast intro: brw_iq.intros)
qed

lemma brec_inner_step_brw_desc:
"⟦ Σ∈brec_invar_inner (hs_α Qi) ⟧
⟹ (brec_α Σ, brec_α (brec_inner_step Qi r Σ)) ∈ brw_inner_step r"
apply (cases Σ)
apply (rule brw_inner_step.intros)
apply (simp only: )
apply (simp only: brec_α_def split_conv)
apply (simp only: brec_inner_step_def brec_α_def Let_def split_conv)
apply (auto
brec_inner_step_def
Let_def hs_correct hm_correct fifo_correct
brec_construct_witness_correct)
done

lemma brec_step_invar:
assumes RQRM: "rqrm_invar rqrm" "rqrm_prop δ rqrm"
assumes [simp]: "hs_invar Qi"
shows "⟦ Σ∈brec_invar_add (hs_α Qi); brec_α Σ ∈ brw_invar δ;  brec_cond Σ ⟧
⟹ (brec_step rqrm Qi Σ)∈brec_invar_add (hs_α Qi)"
apply (frule brec_brw_invar_cons)
apply (cases Σ)
apply (case_tac "fifo_α b")
apply (simp
)
apply (rule_tac s=b in fifo.removelE)
apply simp
apply simp
apply simp

apply (rule_tac
∧ set (fifo_α W) ⊆ dom (hm_α Q)"
in ls.iterate_rule_P)
apply simp
apply (simp
)
apply (simp
fifo_correct)
apply (case_tac σ)
apply (auto
hm_correct fifo_correct split: option.split_asm) [1]
apply (case_tac σ)
apply simp
done

lemma brec_step_abs:
assumes RQRM: "rqrm_invar rqrm" "rqrm_prop δ rqrm"
assumes INV[simp]: "hs_invar Qi"
assumes A': "Σ∈brec_invar (hs_α Qi) δ"
assumes COND: "brec_cond Σ"
shows "(brec_α Σ, brec_α (brec_step rqrm Qi Σ)) ∈ brw_step δ"
proof -
from A' have A: "(brec_α Σ)∈brw_invar δ" "Σ∈brec_invar_add (hs_α Qi)"

obtain Q W rcm qwit where [simp]: "Σ=(Q,W,rcm,qwit)" by (cases Σ) blast
from A COND show ?thesis
apply (case_tac "fifo_α W")
apply (simp
)
apply (rule_tac s=W in fifo.removelE)
apply simp
apply simp
apply simp

apply (rule brw_inner_step_proof[
OF ls.v1_iteratei_impl,
where cinvar="λit Σ. Σ∈brec_invar_inner (hs_α Qi)" and
q="hd (fifo_α W)"])
apply assumption
apply (frule brec_brw_invar_cons)
apply (simp_all
brec_invar_inner_def) [1]
prefer 6
apply (case_tac Σ)
apply (auto
hs_correct fifo_correct brec_invar_inner_def
split: option.split_asm) [1]
apply (blast intro: brec_inner_step_brw_desc)
apply (simp
apply (simp_all
add: brec_α_def brec_cond_def brec_invar_def fifo_correct) [1]
apply (simp_all
done
qed

lemma brec_invar_initial:
"⟦ls_invar δ; hs_invar Qi⟧ ⟹ (brec_initial Qi δ) ∈ brec_invar_add (hs_α Qi)"
apply (auto
brec_iqm_correct' hs_correct hs.isEmpty_correct Let_def
brc_rcm_init_correct br_iq_def
hh_set_xx.disjoint_witness_correct
hs_to_fifo.g_set_to_listr_correct
split: option.split)
hh_set_xx.disjoint_witness_None br_iq_def) [1]

apply (drule hh_set_xx.disjoint_witness_correct[simplified])
apply simp

apply (drule hh_set_xx.disjoint_witness_correct[simplified])
done

lemma brec_cond_abs:
"⟦Σ∈brec_invar Qi δ⟧ ⟹ brec_cond Σ ⟷ (brec_α Σ)∈brw_cond Qi"
apply (cases Σ)
apply (auto
simp add: brec_cond_def brw_cond_def brec_α_def brec_invar_def
split: option.split_asm)
done

lemma brec_initial_abs:
"⟦ ls_invar δ; hs_invar Qi ⟧
⟹ brec_α (brec_initial Qi δ) ∈ brw_initial (ls_α δ)"
by (auto simp add: brec_initial_def Let_def brec_α_def
brc_iq_correct brc_rcm_init_correct brec_iqm_correct
br_iq_def fifo_correct hs_to_fifo.g_set_to_listr_correct
intro: brw_initial.intros[unfolded br_iq_def])

lemma brec_pref_brw:
assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
assumes INV[simp]: "ls_invar δ" "hs_invar Qi"
shows "wa_precise_refine (det_wa_wa (brec_det_algo rqrm Qi δ))
(brw_algo (hs_α Qi) (ls_α δ))
brec_α"
apply (unfold_locales)
apply (simp_all add: det_wa_wa_def brec_det_algo_def brw_algo_def)
apply (auto simp add: brec_cond_abs brec_step_abs brec_initial_abs)
done

lemma brec_while_algo:
assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
assumes INV[simp]: "ls_invar δ" "hs_invar Qi"
shows "while_algo (det_wa_wa (brec_det_algo rqrm Qi δ))"
proof -
interpret ref:
wa_precise_refine "(det_wa_wa (brec_det_algo rqrm Qi δ))"
"(brw_algo (hs_α Qi) (ls_α δ))"
"brec_α"
using brec_pref_brw[OF RQRM INV] .

show ?thesis
apply (rule ref.wa_intro)
apply (simp_all add: det_wa_wa_def brec_det_algo_def brw_algo_def)
apply (auto simp add: brec_step_invar[OF RQRM INV(2)]) [1]
done
qed

lemma fst_brec_α: "fst (brec_α Σ) = hm_α (fst Σ)"
by (cases Σ) (simp add: brec_α_def)

lemmas brec_invar_final =
wa_precise_refine.transfer_correctness[
OF brec_pref_brw brw_invar_final,
unfolded fst_brec_α]

lemmas brec_det_algo = det_while_algo_intro[OF brec_while_algo]

definition "hta_is_empty_witness H ==
let rqrm = build_rqrm (hta_δ H);
(Q,_,_,qwit) = (while brec_cond (brec_step rqrm (hta_Qi H))
(brec_initial (hta_Qi H) (hta_δ H)))
in
case qwit of
None ⇒ None |
Some q ⇒ (hm_lookup q Q)
"

theorem (in hashedTa) hta_is_empty_witness_correct:
shows [rule_format]: "hta_is_empty_witness H = Some t
⟶ t∈ta_lang (hta_α H)" (is ?T1)
"hta_is_empty_witness H = None ⟶ ta_lang (hta_α H) = {}" (is ?T2)
proof -

interpret det_while_algo "(brec_det_algo (build_rqrm δ) Qi δ)"
by (rule brec_det_algo)

have LC:
"(while brec_cond (brec_step (build_rqrm δ) Qi) (brec_initial Qi δ)) = loop"
by (unfold loop_def)

from while_proof'[OF brec_invar_final] have X:
"hs_α Qi ∩ dom (hm_α (fst loop)) = {}
⟷ (hs_α Qi ∩ b_accessible (ls_α δ) = {})"
"witness_prop (ls_α δ) (hm_α (fst loop))"

obtain Q W rcm qwit where
[simp]: "loop = (Q,W,rcm,qwit)"
by (case_tac "loop") blast

from loop_invar have I: "loop ∈ brec_invar (hs_α Qi) (ls_α δ)"
hence INVARS[simp]: "hm_invar Q" "hm_invar rcm"

{
assume C: "hta_is_empty_witness H = Some t"
then obtain q where
[simp]: "qwit=Some q" and
LUQ: "hm_lookup q Q = Some t"
by (unfold hta_is_empty_witness_def)
from LUQ have QqF: "hm_α Q q = Some t" by (simp add: hm_correct)
from I have QMEM: "q∈hs_α Qi"
moreover from witness_propD[OF X(2)] QqF have "accs (ls_α δ) t q" by simp
ultimately have "t∈ta_lang (hta_α H)"
by (auto simp add: ta_lang_def hta_α_def)
} moreover {
assume C: "hta_is_empty_witness H = None"
hence DJ: "hs_α Qi ∩ dom (hm_α Q) = {}" using I
by (auto simp add: hta_is_empty_witness_def LC brec_invar_def
split: option.split_asm)
with X have "hs_α Qi ∩ b_accessible (ls_α δ) = {}"
with empty_if_no_b_accessible[of "hta_α H"] have "ta_lang (hta_α H) = {}"
} ultimately show ?T1 ?T2 by auto
qed

subsection ‹Interface for Natural Number States and Symbols›
text_raw ‹\label{sec:htai_intf}›
text ‹
The library-interface is statically instantiated to use natural numbers
as both, states and symbols.

This interface is easier to use from ML and OCaml, because there is no
›

type_synonym htai = "(nat,nat) hashedTa"

definition htai_mem :: "_ ⇒ htai ⇒ bool"
where "htai_mem == hta_mem"
definition htai_prod :: "htai ⇒ htai ⇒ htai"
where "htai_prod H1 H2 == hta_reindex (hta_prod H1 H2)"
definition htai_prodWR :: "htai ⇒ htai ⇒ htai"
where "htai_prodWR H1 H2 == hta_reindex (hta_prodWR H1 H2)"
definition htai_union :: "htai ⇒ htai ⇒ htai"
where "htai_union H1 H2 == hta_reindex (hta_union H1 H2)"
definition htai_empty :: "unit ⇒ htai"
where "htai_empty == hta_empty"
definition htai_add_qi :: "_ ⇒ htai ⇒ htai"
definition htai_add_rule :: "_ ⇒ htai ⇒ htai"
definition htai_bwd_reduce :: "htai ⇒ htai"
where "htai_bwd_reduce == hta_bwd_reduce"
definition htai_is_empty_witness :: "htai ⇒ _"
where "htai_is_empty_witness == hta_is_empty_witness"
definition htai_ensure_idx_f :: "htai ⇒ htai"
where "htai_ensure_idx_f == hta_ensure_idx_f"
definition htai_ensure_idx_s :: "htai ⇒ htai"
where "htai_ensure_idx_s == hta_ensure_idx_s"
definition htai_ensure_idx_sf :: "htai ⇒ htai"
where "htai_ensure_idx_sf == hta_ensure_idx_sf"

definition htaip_prod :: "htai ⇒ htai ⇒ (nat * nat,nat) hashedTa"
where "htaip_prod == hta_prod"
definition htaip_prodWR :: "htai ⇒ htai ⇒ (nat * nat,nat) hashedTa"
where "htaip_prodWR == hta_prodWR"
definition htaip_reindex :: "(nat * nat,nat) hashedTa ⇒ htai"
where "htaip_reindex == hta_reindex"

locale htai = hashedTa +
constrains H :: htai
begin
lemmas htai_mem_correct = hta_mem_correct[folded htai_mem_def]

lemma htai_empty_correct[simp]:
"hta_α (htai_empty ()) = ta_empty"
"hashedTa (htai_empty ())"
by (auto simp add: htai_empty_def hta_empty_correct)

lemmas htai_bwd_reduce_correct =
hta_bwd_reduce_correct[folded htai_bwd_reduce_def]
lemmas htai_is_empty_witness_correct =
hta_is_empty_witness_correct[folded htai_is_empty_witness_def]

lemmas htai_ensure_idx_f_correct =
hta_ensure_idx_f_correct[folded htai_ensure_idx_f_def]
lemmas htai_ensure_idx_s_correct =
hta_ensure_idx_s_correct[folded htai_ensure_idx_s_def]
lemmas htai_ensure_idx_sf_correct =
hta_ensure_idx_sf_correct[folded htai_ensure_idx_sf_def]

end

lemma htai_prod_correct:
assumes [simp]: "hashedTa H1" "hashedTa H2"
shows
"ta_lang (hta_α (htai_prod H1 H2)) = ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
"hashedTa (htai_prod H1 H2)"
apply (unfold htai_prod_def)
apply (auto simp add: hta_prod_correct hashedTa.hta_reindex_correct)
done

lemma htai_prodWR_correct:
assumes [simp]: "hashedTa H1" "hashedTa H2"
shows
"ta_lang (hta_α (htai_prodWR H1 H2))
= ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
"hashedTa (htai_prodWR H1 H2)"
apply (unfold htai_prodWR_def)
apply (auto simp add: hta_prodWR_correct hashedTa.hta_reindex_correct)
done

lemma htai_union_correct:
assumes [simp]: "hashedTa H1" "hashedTa H2"
shows
"ta_lang (hta_α (htai_union H1 H2))
= ta_lang (hta_α H1) ∪ ta_lang (hta_α H2)"
"hashedTa (htai_union H1 H2)"
apply (unfold htai_union_def)
apply (auto simp add: hta_union_correct hashedTa.hta_reindex_correct)
done

subsection ‹Interface Documentation› text_raw‹\label{sec:intf_doc}›
text ‹
This section contains a documentation of the executable tree-automata
interface. The documentation contains a description of each function along
with the relevant correctness lemmas.
›

text ‹
ML/OCaml users should note, that there is an interface that has the fixed type
Int for both states and function symbols. This interface is simpler to use
from ML/OCaml than the generic one, as it requires no overhead to emulate
Isabelle/HOL type-classes.

{\em hta}, but have the same semantics otherwise
(cf Section~\ref{sec:htai_intf}).
›

subsubsection ‹Building a Tree Automaton›
text_raw ‹
\newcommand{\fundesc}[2]{{\bf Function: #1}\\#2}

›

text ‹
\fundesc{@{const [show_types] hta_empty}}{
Returns a tree automaton with no states and no rules.
}

\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hta_empty_correct}:] @{thm hta_empty_correct[no_vars]}
\item[@{thm [source] ta_empty_lang}:] @{thm ta_empty_lang[no_vars]}
\end{description}
›

text ‹
Adds an initial state to the given automaton.
}
\paragraph{Relevant Lemmas}
\begin{description}
\end{description}
›

text ‹
Adds a rule to the given automaton.
}
\paragraph{Relevant Lemmas}
\begin{description}
\end{description}
›

subsubsection ‹Basic Operations›

text ‹
The tree automata of this library may have some optional indices, that
accelerate computation. The tree-automata operations will compute the
indices if necessary, but due to the pure nature of the Isabelle-language,
the computed index cannot be stored for the next usage. Hence, before using a
bulk of tree-automaton operations on the same tree-automata, the relevant
indexes should be pre-computed.
›

text ‹
\fundesc{
@{const [show_types] hta_ensure_idx_f}\\
@{const [show_types] hta_ensure_idx_s}\\
@{const [show_types] hta_ensure_idx_sf}
}{
Computes an index for a tree automaton, if it is not yet present.
}
›

text ‹
\fundesc{@{const [show_types] hta_mem}, @{const [show_types] hta_mem'}}{
Check whether a tree is accepted by the tree automaton.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hashedTa.hta_mem_correct}:]
@{thm hashedTa.hta_mem_correct[no_vars]}
\item[@{thm [source] hashedTa.hta_mem'_correct}:]
@{thm hashedTa.hta_mem'_correct[no_vars]}
\end{description}
›

text ‹
\fundesc{@{const [show_types] hta_prod}, @{const [show_types] hta_prod'}}{
Compute the product automaton. The computed automaton is in
forward-reduced form.
The language of the product automaton is the intersection of
the languages of the two argument automata.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hta_prod_correct_aux}:]
@{thm hta_prod_correct_aux[no_vars]}
\item[@{thm [source] hta_prod_correct}:]
@{thm hta_prod_correct[no_vars]}
\item[@{thm [source] hta_prod'_correct_aux}:]
@{thm hta_prod'_correct_aux[no_vars]}
\item[@{thm [source] hta_prod'_correct}:]
@{thm hta_prod'_correct[no_vars]}
\end{description}
›

text ‹
\fundesc{@{const [show_types] hta_prodWR}}{
Compute the product automaton by brute-force algorithm.
The resulting automaton is not reduced.
The language of the product automaton is the intersection of
the languages of the two argument automata.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hta_prodWR_correct_aux}:]
@{thm hta_prodWR_correct_aux[no_vars]}
\item[@{thm [source] hta_prodWR_correct}:]
@{thm hta_prodWR_correct[no_vars]}
\end{description}
›

text ‹
\fundesc{@{const [show_types] hta_union}}{
Compute the union of two tree automata.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hta_union_correct'}:] @{thm hta_union_correct'[no_vars]}
\item[@{thm [source] hta_union_correct}:] @{thm hta_union_correct[no_vars]}
\end{description}
›

text ‹
\fundesc{@{const [show_types] hta_reduce}}{
Reduce the automaton to the given set of states. All initial states outside
this set will be removed. Moreover, all rules that contain states outside
this set are removed, too.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hashedTa.hta_reduce_correct}:]
@{thm hashedTa.hta_reduce_correct[no_vars]}
\end{description}
›

text ‹
\fundesc{@{const [show_types] hta_bwd_reduce}}{
Compute the backwards-reduced version of a tree automata.
States from that no tree can be produced are removed.
Backwards reduction does not change the language of the automaton.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hashedTa.hta_bwd_reduce_correct}:]
@{thm hashedTa.hta_bwd_reduce_correct[no_vars]}
\item[@{thm [source] ta_reduce_b_acc}:] @{thm ta_reduce_b_acc[no_vars]}
\end{description}
›

text ‹
\fundesc{@{const [show_types] hta_is_empty_witness}}{
Check whether the language of the automaton is empty.
If the language is not empty, a tree of the language is returned.

The following property is not (yet) formally proven, but should hold:
If a tree is returned, the language contains no tree with a smaller depth
than the returned one.
}
\paragraph{Relevant Lemmas}
\begin{description}
\item[@{thm [source] hashedTa.hta_is_empty_witness_correct}:]
@{thm hashedTa.hta_is_empty_witness_correct[no_vars]}
\end{description}
›

subsection ‹Code Generation›

(* TODO/FIXME: There seems to be no way to reference the project-directory,
in order to control the placement of the generated code files.
The code-generation in this file only dumps the generated code to standard output.
Hence it is safe to include this file from other projects.

Actual code generation is done in Ta_impl_codegen.thy
*)

export_code
hta_mem hta_mem' hta_prod hta_prod' hta_prodWR hta_union
hta_reduce hta_bwd_reduce hta_is_empty_witness
hta_ensure_idx_f hta_ensure_idx_s hta_ensure_idx_sf

htai_mem htai_prod htai_prodWR htai_union
htai_bwd_reduce htai_is_empty_witness
htai_ensure_idx_f htai_ensure_idx_s htai_ensure_idx_sf

(*ls_size hs_size rs_size*)
in SML
module_name Ta

export_code
hta_mem hta_mem' hta_prod hta_prod' hta_prodWR hta_union
hta_reduce hta_bwd_reduce hta_is_empty_witness
hta_ensure_idx_f hta_ensure_idx_s hta_ensure_idx_sf

htai_mem htai_prod htai_prodWR htai_union
htai_bwd_reduce htai_is_empty_witness
htai_ensure_idx_f htai_ensure_idx_s htai_ensure_idx_sf

(*ls_size hs_size rs_size*)
module_name Ta
(string_classes)

export_code
hta_mem hta_mem' hta_prod hta_prod' hta_prodWR hta_union
hta_reduce hta_bwd_reduce hta_is_empty_witness
hta_ensure_idx_f hta_ensure_idx_s hta_ensure_idx_sf

htai_mem htai_prod htai_prodWR htai_union
htai_bwd_reduce htai_is_empty_witness
htai_ensure_idx_f htai_ensure_idx_s htai_ensure_idx_sf

(*ls_size hs_size rs_size*)
in OCaml
module_name Ta

(* If this statement fails with an error from ML, this indicates a problem
with the code-generator. The most frequent problem in this context is, that
the code generator generates code that violates the ML value-restriction.
*)

ML ‹
@{code hta_mem};
@{code hta_mem'};
@{code hta_prod};
@{code hta_prod'};
@{code hta_prodWR};
@{code hta_union};
@{code hta_empty};
@{code hta_reduce};
@{code hta_bwd_reduce};
@{code hta_is_empty_witness};
@{code hta_ensure_idx_f};
@{code hta_ensure_idx_s};
@{code hta_ensure_idx_sf};
@{code htai_mem};
@{code htai_prod};
@{code htai_prodWR};
@{code htai_union};
@{code htai_empty};
`