# Theory Regular_Tree_Relations.RRn_Automata

```theory RRn_Automata
imports Tree_Automata_Complement Ground_Ctxt
begin
section ‹Regular relations›

subsection ‹Encoding pairs of terms›

text ‹The encoding of two terms \$s\$ and \$t\$ is given by its tree domain, which is the union of the
domains of \$s\$ and \$t\$, and the labels, which arise from looking up each position in \$s\$ and \$t\$,
respectively.›

definition gpair :: "'f gterm ⇒ 'g gterm ⇒ ('f option × 'g option) gterm" where
"gpair s t = glabel (λp. (gfun_at s p, gfun_at t p)) (gunion (gdomain s) (gdomain t))"

text ‹We provide an efficient implementation of gpair.›

definition zip_fill :: "'a list ⇒ 'b list ⇒ ('a option × 'b option) list" where
"zip_fill xs ys = zip (map Some xs @ replicate (length ys - length xs) None)
(map Some ys @ replicate (length xs - length ys) None)"

lemma zip_fill_code [code]:
"zip_fill xs [] = map (λx. (Some x, None)) xs"
"zip_fill [] ys = map (λy. (None, Some y)) ys"
"zip_fill (x # xs) (y # ys) = (Some x, Some y) # zip_fill xs ys"
subgoal by (induct xs) (auto simp: zip_fill_def)
subgoal by (induct ys) (auto simp: zip_fill_def)
subgoal by (auto simp: zip_fill_def)
done

lemma length_zip_fill [simp]:
"length (zip_fill xs ys) = max (length xs) (length ys)"
by (auto simp: zip_fill_def)

lemma nth_zip_fill:
assumes "i < max (length xs) (length ys)"
shows "zip_fill xs ys ! i = (if i < length xs then Some (xs ! i) else None, if i < length ys then Some (ys ! i) else None)"
using assms by (auto simp: zip_fill_def nth_append)

fun gpair_impl :: "'f gterm option ⇒ 'g gterm option ⇒ ('f option × 'g option) gterm" where
"gpair_impl (Some s) (Some t) = gpair s t"
| "gpair_impl (Some s) None     = map_gterm (λf. (Some f, None)) s"
| "gpair_impl None     (Some t) = map_gterm (λf. (None, Some f)) t"
| "gpair_impl None     None     = GFun (None, None) []"

declare gpair_impl.simps(2-4)[code]

lemma gpair_impl_code [simp, code]:
"gpair_impl (Some s) (Some t) =
(case s of GFun f ss ⇒ case t of GFun g ts ⇒
GFun (Some f, Some g) (map (λ(s, t). gpair_impl s t) (zip_fill ss ts)))"
proof (induct "gdomain s" "gdomain t" arbitrary: s t rule: gunion.induct)
case (1 f ss g ts)
obtain f' ss' where [simp]: "s = GFun f' ss'" by (cases s)
obtain g' ts' where [simp]: "t = GFun g' ts'" by (cases t)
show ?case using 1(2,3) 1(1)[of i "ss' ! i" "ts' ! i" for i]
by (auto simp: gpair_def comp_def nth_zip_fill intro: glabel_map_gterm_conv[unfolded comp_def]
intro!: nth_equalityI)
qed

lemma gpair_code [code]:
"gpair s t = gpair_impl (Some s) (Some t)"
by simp

(* export_code gpair in Haskell *)

declare gpair_impl.simps(1)[simp del]

text ‹We can easily prove some basic properties. I believe that proving them by induction with a
definition along the lines of @{const gpair_impl} would be very cumbersome.›

lemma gpair_swap:
"map_gterm prod.swap (gpair s t) = gpair t s"
by (intro eq_gterm_by_gposs_gfun_at) (auto simp: gpair_def)

lemma gpair_assoc:
defines "f ≡ λ(f, gh). (f, gh ⤜ fst, gh ⤜ snd)"
defines "g ≡ λ(fg, h). (fg ⤜ fst, fg ⤜ snd, h)"
shows "map_gterm f (gpair s (gpair t u)) = map_gterm g (gpair (gpair s t) u)"
by (intro eq_gterm_by_gposs_gfun_at) (auto simp: gpair_def f_def g_def)

subsection ‹Decoding of pairs›

fun gcollapse :: "'f option gterm ⇒ 'f gterm option" where
"gcollapse (GFun None _) = None"
| "gcollapse (GFun (Some f) ts) = Some (GFun f (map the (filter (λt. ¬ Option.is_none t) (map gcollapse ts))))"

lemma gcollapse_groot_None [simp]:
"groot_sym t = None ⟹ gcollapse t = None"
"fst (groot t) = None ⟹ gcollapse t = None"
by (cases t, simp)+

definition gfst :: "('f option × 'g option) gterm ⇒ 'f gterm" where
"gfst = the ∘ gcollapse ∘ map_gterm fst"

definition gsnd :: "('f option × 'g option) gterm ⇒ 'g gterm" where
"gsnd = the ∘ gcollapse ∘ map_gterm snd"

lemma filter_less_upt:
"[i←[i..<m] . i < n] = [i..<min n m]"
proof (cases "i ≤ m")
case True then show ?thesis
proof (induct rule: inc_induct)
case (step n) then show ?case by (auto simp: upt_rec[of n])
qed simp
qed simp

lemma gcollapse_aux:
assumes "gposs s = {p. p ∈ gposs t ∧ gfun_at t p ≠ Some None}"
shows "gposs (the (gcollapse t)) = gposs s"
"⋀p. p ∈ gposs s ⟹ gfun_at (the (gcollapse t)) p = (gfun_at t p ⤜ id)"
proof (goal_cases)
define s' t' where "s' ≡ gdomain s" and "t' ≡ gdomain t"
have *: "gposs (the (gcollapse t)) = gposs s ∧
(∀p. p ∈ gposs s ⟶ gfun_at (the (gcollapse t)) p = (gfun_at t p ⤜ id))"
using assms s'_def t'_def
proof (induct s' t' arbitrary: s t rule: gunion.induct)
case (1 f' ss' g' ts')
obtain f ss where s [simp]: "s = GFun f ss" by (cases s)
obtain g ts where t [simp]: "t = GFun (Some g) ts"
using arg_cong[OF 1(2), of "λP. [] ∈ P"] by (cases t) auto
have *: "i < length ts ⟹ ¬ Option.is_none (gcollapse (ts ! i)) ⟷ i < length ss" for i
using arg_cong[OF 1(2), of "λP. [i] ∈ P"] by (cases "ts ! i") auto
have l: "length ss ≤ length ts"
using arg_cong[OF 1(2), of "λP. [length ss-1] ∈ P"] by auto
have [simp]: "[t←map gcollapse ts . ¬ Option.is_none t] = take (length ss) (map gcollapse ts)"
by (subst (2) map_nth[symmetric]) (auto simp add: * filter_map comp_def filter_less_upt
cong: filter_cong[OF refl, of "[0..<length ts]", unfolded set_upt atLeastLessThan_iff]
intro!: nth_equalityI)
have [simp]: "i < length ss ⟹ gposs (ss ! i) = gposs (the (gcollapse (ts ! i)))" for i
using conjunct1[OF 1(1), of i "ss ! i" "ts ! i"] l arg_cong[OF 1(2), of "λP. {p. i # p ∈ P}"]
1(3,4) by simp
show ?case
proof (intro conjI allI, goal_cases A B)
case A show ?case using l by (auto simp: comp_def split: if_splits)
next
case (B p) show ?case
proof (cases p)
case (Cons i q) then show ?thesis using arg_cong[OF 1(2), of "λP. {p. i # p ∈ P}"]
spec[OF conjunct2[OF 1(1)], of i "ss ! i" "ts ! i" q] 1(3,4) by auto
qed auto
qed
qed
{ case 1 then show ?case using * by blast
next
case 2 then show ?case using * by blast }
qed

lemma gfst_gpair:
"gfst (gpair s t) = s"
proof -
have *: "gposs s = {p ∈ gposs (map_gterm fst (gpair s t)). gfun_at (map_gterm fst (gpair s t)) p ≠ Some None}"
using gfun_at_nongposs
by (fastforce simp: gpair_def elim: gfun_at_possE)
show ?thesis unfolding gfst_def comp_def using gcollapse_aux[OF *]
by (auto intro!: eq_gterm_by_gposs_gfun_at simp: gpair_def)
qed

lemma gsnd_gpair:
"gsnd (gpair s t) = t"
using gfst_gpair[of t s] gpair_swap[of t s, symmetric]
by (simp add: gfst_def gsnd_def gpair_def gterm.map_comp comp_def)

lemma gpair_impl_None_Inv:
"map_gterm (the ∘ snd) (gpair_impl None (Some t)) = t"
by (simp add: gterm.map_ident gterm.map_comp comp_def)

subsection ‹Contexts to gpair›

lemma gpair_context1:
assumes "length ts = length us"
shows "gpair (GFun f ts) (GFun f us) = GFun (Some f, Some f) (map (case_prod gpair) (zip ts us))"
using assms unfolding gpair_code by (auto intro!: nth_equalityI simp: zip_fill_def)

lemma gpair_context2:
assumes "⋀ i. i < length ts ⟹ ts ! i = gpair (ss ! i) (us ! i)"
and "length ss = length ts" and "length us = length ts"
shows "GFun (Some f, Some h) ts = gpair (GFun f ss) (GFun h us)"
using assms unfolding gpair_code gpair_impl_code
by (auto simp: zip_fill_def intro!: nth_equalityI)

lemma map_funs_term_some_gpair:
shows "gpair t t = map_gterm (λf. (Some f, Some f)) t"
proof (induct t)
case (GFun f ts)
then show ?case by (auto intro!: gpair_context2[symmetric])
qed

lemma gpair_inject [simp]:
"gpair s t = gpair s' t' ⟷ s = s' ∧ t = t'"
by (metis gfst_gpair gsnd_gpair)

abbreviation gterm_to_None_Some :: "'f gterm ⇒ ('f option × 'f option) gterm" where
"gterm_to_None_Some t ≡ map_gterm (λf. (None, Some f)) t"
abbreviation "gterm_to_Some_None t ≡ map_gterm (λf. (Some f, None)) t"

lemma inj_gterm_to_None_Some: "inj gterm_to_None_Some"
by (meson Pair_inject gterm.inj_map inj_onI option.inject)

lemma zip_fill1:
assumes "length ss < length ts"
shows "zip_fill ss ts = zip (map Some ss) (map Some (take (length ss) ts)) @
map (λ x. (None, Some x)) (drop (length ss) ts)"
using assms by (auto simp: zip_fill_def list_eq_iff_nth_eq nth_append simp add: min.absorb2)

lemma zip_fill2:
assumes "length ts < length ss"
shows "zip_fill ss ts = zip (map Some (take (length ts) ss)) (map Some ts) @
map (λ x. (Some x, None)) (drop (length ts) ss)"
using assms by (auto simp: zip_fill_def list_eq_iff_nth_eq nth_append simp add: min.absorb2)

(* GPair position lemmas *)

(* MOVE me*)
lemma not_gposs_append [simp]:
assumes "p ∉ gposs t"
shows "p @ q ∈ gposs t = False" using assms poss_gposs_conv
using poss_append_poss by blast

(*end Move *)

lemma gfun_at_gpair:
"gfun_at (gpair s t) p = (if p ∈ gposs s then (if p ∈ gposs t
then Some (gfun_at s p, gfun_at t p)
else Some (gfun_at s p, None)) else
(if p ∈ gposs t then Some (None, gfun_at t p) else None))"
using gfun_at_glabel by (auto simp: gpair_def)

lemma gposs_of_gpair [simp]:
shows "gposs (gpair s t) = gposs s ∪ gposs t"
by (auto simp: gpair_def)

lemma poss_to_gpair_poss:
"p ∈ gposs s ⟹ p ∈ gposs (gpair s t)"
"p ∈ gposs t ⟹ p ∈ gposs (gpair s t)"
by auto

lemma gsubt_at_gpair_poss:
assumes "p ∈ gposs s" and "p ∈ gposs t"
shows "gsubt_at (gpair s t) p = gpair (gsubt_at s p) (gsubt_at t p)" using assms
by (auto simp: gunion_gsubt_at_poss gfun_at_gpair intro!: eq_gterm_by_gposs_gfun_at)

lemma subst_at_gpair_nt_poss_Some_None:
assumes "p ∈ gposs s" and "p ∉ gposs t"
shows "gsubt_at (gpair s t) p = gterm_to_Some_None (gsubt_at s p)" using assms gfun_at_poss
by (force simp: gunion_gsubt_at_poss gfun_at_gpair intro!: eq_gterm_by_gposs_gfun_at)

lemma subst_at_gpair_nt_poss_None_Some:
assumes "p ∈ gposs t" and "p ∉ gposs s"
shows "gsubt_at (gpair s t) p = gterm_to_None_Some (gsubt_at t p)" using assms gfun_at_poss
by (force simp: gunion_gsubt_at_poss gfun_at_gpair intro!: eq_gterm_by_gposs_gfun_at)

lemma gpair_ctxt_decomposition:
fixes C defines "p ≡ ghole_pos C"
assumes "p ∉ gposs s" and "gpair s t = C⟨gterm_to_None_Some u⟩⇩G"
shows "gpair s (gctxt_at_pos t p)⟨v⟩⇩G = C⟨gterm_to_None_Some v⟩⇩G"
using assms(2-)
proof -
note p[simp] = assms(1)
have pt: "p ∈ gposs t" and pc: "p ∈ gposs C⟨gterm_to_None_Some v⟩⇩G"
and pu: "p ∈ gposs C⟨gterm_to_None_Some u⟩⇩G"
using arg_cong[OF assms(3), of gposs] assms(2) ghole_pos_in_apply
by auto
have *: "gctxt_at_pos (gpair s (gctxt_at_pos t (ghole_pos C))⟨v⟩⇩G) (ghole_pos C) = gctxt_at_pos (gpair s t) (ghole_pos C)"
using assms(2) pt
by (intro eq_gctxt_at_pos)
(auto simp: gposs_gctxt_at_pos gunion_gsubt_at_poss gfun_at_gpair gfun_at_gctxt_at_pos_not_after)
have "gsubt_at (gpair s (gctxt_at_pos t p)⟨v⟩⇩G) p = gsubt_at C⟨gterm_to_None_Some v⟩⇩G p"
using pt assms(2) subst_at_gpair_nt_poss_None_Some[OF _ assms(2), of "(gctxt_at_pos t p)⟨v⟩⇩G"]
using ghole_pos_gctxt_at_pos
then show ?thesis using assms(2) ghole_pos_gctxt_at_pos
using gsubst_at_gctxt_at_eq_gtermD[OF assms(3) pu]
by (intro gsubst_at_gctxt_at_eq_gtermI[OF _ pc])
(auto simp: ghole_pos_in_apply * gposs_gctxt_at_pos[OF pt, unfolded p])
qed

lemma groot_gpair [simp]:
"fst (groot (gpair s t)) = (Some (fst (groot s)), Some (fst (groot t)))"
by (cases s; cases t) (auto simp add: gpair_code)

assumes "ground_ctxt C"
using assms by (induct C) auto

assumes "ground_ctxt C"
by (induct C) (auto simp: adapt_vars2)

subsection ‹Encoding of lists of terms›

definition gencode :: "'f gterm list ⇒ 'f option list gterm" where
"gencode ts = glabel (λp. map (λt. gfun_at t p) ts) (gunions (map gdomain ts))"

definition gdecode_nth :: "'f option list gterm ⇒ nat ⇒ 'f gterm" where
"gdecode_nth t i = the (gcollapse (map_gterm (λf. f ! i) t))"

lemma gdecode_nth_gencode:
assumes "i < length ts"
shows "gdecode_nth (gencode ts) i = ts ! i"
proof -
have *: "gposs (ts ! i) = {p ∈ gposs (map_gterm (λf. f ! i) (gencode ts)).
gfun_at (map_gterm (λf. f ! i) (gencode ts)) p ≠ Some None}"
using assms
by (auto simp: gencode_def elim: gfun_at_possE dest: gfun_at_poss_gpossD) (force simp: fun_at_def' split: if_splits)
show ?thesis unfolding gdecode_nth_def comp_def using assms gcollapse_aux[OF *]
by (auto intro!: eq_gterm_by_gposs_gfun_at simp: gencode_def)
(metis (no_types) gposs_map_gterm length_map list.set_map map_nth_eq_conv nth_mem)
qed

definition gdecode :: "'f option list gterm ⇒ 'f gterm list" where
"gdecode t = (case t of GFun f ts ⇒ map (λi. gdecode_nth t i) [0..<length f])"

lemma gdecode_gencode:
"gdecode (gencode ts) = ts"
proof (cases "gencode ts")
case (GFun f ts')
have "length f = length ts" using arg_cong[OF GFun, of "λt. gfun_at t []"]
by (auto simp: gencode_def)
then show ?thesis using gdecode_nth_gencode[of _ ts]
by (auto intro!: nth_equalityI simp: gdecode_def GFun)
qed

definition gencode_impl :: "'f gterm option list ⇒ 'f option list gterm" where
"gencode_impl ts = glabel (λp. map (λt. t ⤜ (λt. gfun_at t p)) ts) (gunions (map (case_option (GFun () []) gdomain) ts))"

lemma gencode_code [code]:
"gencode ts = gencode_impl (map Some ts)"
by (auto simp: gencode_def gencode_impl_def comp_def)

lemma gencode_singleton:
"gencode [t] = map_gterm (λf. [Some f]) t"
using glabel_map_gterm_conv[unfolded comp_def, of "λt. [t]" t]

lemma gencode_pair:
"gencode [t, u] = map_gterm (λ(f, g). [f, g]) (gpair t u)"
by (simp add: gunions_def gencode_def gpair_def map_gterm_glabel comp_def)

subsection ‹RRn relations›

definition RR1_spec where
"RR1_spec A T ⟷ ℒ A = T"

definition RR2_spec where
"RR2_spec A T ⟷ ℒ A = {gpair t u |t u. (t, u) ∈ T}"

definition RRn_spec where
"RRn_spec n A R ⟷ ℒ A = gencode ` R ∧ (∀ts ∈ R. length ts = n)"

lemma RR1_to_RRn_spec:
assumes "RR1_spec A T"
shows "RRn_spec 1 (fmap_funs_reg (λf. [Some f]) A) ((λt. [t]) ` T)"
proof -
have [simp]: "inj_on (λf. [Some f]) X" for X by (auto simp: inj_on_def)
show ?thesis using assms
by (auto simp: RR1_spec_def RRn_spec_def fmap_funs_ℒ image_comp comp_def gencode_singleton)
qed

lemma RR2_to_RRn_spec:
assumes "RR2_spec A T"
shows "RRn_spec 2 (fmap_funs_reg (λ(f, g). [f, g]) A) ((λ(t, u). [t, u]) ` T)"
proof -
have [simp]: "inj_on (λ(f, g). [f, g]) X" for X by (auto simp: inj_on_def)
show ?thesis using assms
by (auto simp: RR2_spec_def RRn_spec_def fmap_funs_ℒ image_comp comp_def prod.case_distrib gencode_pair)
qed

lemma RRn_to_RR2_spec:
assumes "RRn_spec 2 A T"
shows "RR2_spec (fmap_funs_reg (λ f. (f ! 0 ,  f ! 1)) A) ((λ f. (f ! 0, f ! 1)) ` T)" (is "RR2_spec ?A ?T")
proof -
{fix xs assume "xs ∈ T" then have "length xs = 2" using assms by (auto simp: RRn_spec_def)
then obtain t u where *: "xs = [t, u]"
by (metis (no_types, lifting) One_nat_def Suc_1 length_0_conv length_Suc_conv)
have **: "(λf. (f ! 0, f ! Suc 0)) ∘ (λ(f, g). [f, g]) = id" by auto
have "map_gterm (λf. (f ! 0, f ! Suc 0)) (gencode xs) = gpair t u"
unfolding * gencode_pair gterm.map_comp ** gterm.map_id ..
then have "∃ t u. xs = [t, u] ∧ map_gterm (λf. (f ! 0, f ! Suc 0)) (gencode xs) = gpair t u"
using * by blast}
then show ?thesis using assms
by (force simp: RR2_spec_def RRn_spec_def fmap_funs_ℒ image_comp comp_def prod.case_distrib gencode_pair image_iff Bex_def)
qed

lemma relabel_RR1_spec [simp]:
"RR1_spec (relabel_reg A) T ⟷ RR1_spec A T"

lemma relabel_RR2_spec [simp]:
"RR2_spec (relabel_reg A) T ⟷ RR2_spec A T"

lemma relabel_RRn_spec [simp]:
"RRn_spec n (relabel_reg A) T ⟷ RRn_spec n A T"

lemma trim_RR1_spec [simp]:
"RR1_spec (trim_reg A) T ⟷ RR1_spec A T"

lemma trim_RR2_spec [simp]:
"RR2_spec (trim_reg A) T ⟷ RR2_spec A T"

lemma trim_RRn_spec [simp]:
"RRn_spec n (trim_reg A) T ⟷ RRn_spec n A T"

lemma swap_RR2_spec:
assumes "RR2_spec A R"
shows "RR2_spec (fmap_funs_reg prod.swap A) (prod.swap ` R)" using assms
by (force simp add: RR2_spec_def fmap_funs_ℒ gpair_swap image_iff)

subsection ‹Nullary automata›

lemma false_RRn_spec:
"RRn_spec n empty_reg {}"
by (auto simp: RRn_spec_def ℒ_epmty)

lemma true_RR0_spec:
"RRn_spec 0 (Reg {|q|} (TA {|[] [] → q|} {||})) {[]}"
by (auto simp: RRn_spec_def ℒ_def const_ta_lang gencode_def gunions_def)

subsection ‹Pairing RR1 languages›

text ‹cf. @{const "gpair"}.›

abbreviation "lift_Some_None s ≡ (Some s, None)"
abbreviation "lift_None_Some s ≡ (None, Some s)"
abbreviation "pair_eps A B ≡ (λ (p, q). ((Some (fst p), q), (Some (snd p), q))) |`| (eps A |×| finsert None (Some |`| 𝒬 B))"
abbreviation "pair_rule ≡ (λ (ra, rb). TA_rule (Some (r_root ra), Some (r_root rb)) (zip_fill (r_lhs_states ra) (r_lhs_states rb)) (Some (r_rhs ra), Some (r_rhs rb)))"

lemma lift_Some_None_pord_swap [simp]:
"prod.swap ∘ lift_Some_None = lift_None_Some"
"prod.swap ∘ lift_None_Some = lift_Some_None"
by auto

lemma eps_to_pair_eps_Some_None:
"(p, q) |∈| eps 𝒜 ⟹ (lift_Some_None p, lift_Some_None q) |∈| pair_eps 𝒜 ℬ"
by force

definition pair_automaton :: "('p, 'f) ta ⇒ ('q, 'g) ta ⇒ ('p option × 'q option, 'f option × 'g option) ta" where
"pair_automaton A B = TA
(map_ta_rule lift_Some_None lift_Some_None |`| rules A |∪|
map_ta_rule lift_None_Some lift_None_Some |`| rules B |∪|
pair_rule |`| (rules A |×| rules B))
(pair_eps A B |∪| map_both prod.swap |`| (pair_eps B A))"

definition pair_automaton_reg where
"pair_automaton_reg R L = Reg (Some |`| fin R |×| Some |`| fin L) (pair_automaton (ta R) (ta L))"

lemma pair_automaton_eps_simps:
"(lift_Some_None p, p') |∈| eps (pair_automaton A B) ⟷ (lift_Some_None p, p') |∈| pair_eps A B"
"(q , lift_Some_None q') |∈| eps (pair_automaton A B) ⟷ (q , lift_Some_None q') |∈| pair_eps A B"
by (auto simp: pair_automaton_def eps_to_pair_eps_Some_None)

lemma pair_automaton_eps_Some_SomeD:
"((Some p, Some p'), r) |∈| eps (pair_automaton A B) ⟹ fst r ≠ None ∧ snd r ≠ None ∧ (Some p = fst r ∨ Some p' = snd r) ∧
(Some p ≠ fst r ⟶ (p, the (fst r)) |∈| (eps A)) ∧ (Some p' ≠ snd r ⟶ (p', the (snd r)) |∈| (eps B))"
by (auto simp: pair_automaton_def)

lemma pair_automaton_eps_Some_SomeD2:
"(r, (Some p, Some p')) |∈| eps (pair_automaton A B) ⟹ fst r ≠ None ∧ snd r ≠ None ∧ (fst r = Some p ∨ snd r = Some p') ∧
(fst r ≠ Some p ⟶ (the (fst r), p) |∈| (eps A)) ∧ (snd r ≠ Some p' ⟶ (the (snd r), p') |∈| (eps B))"
by (auto simp: pair_automaton_def)

lemma pair_eps_Some_None:
fixes p q q'
defines "l ≡ (p, q)" and "r ≡ lift_Some_None q'"
assumes "(l, r) |∈| (eps (pair_automaton A B))|⇧+|"
shows "q = None ∧ p ≠ None ∧ (the p, q') |∈| (eps A)|⇧+|" using assms(3, 1, 2)
proof (induct arbitrary: q' q rule: ftrancl_induct)
case (Step b)
then show ?case unfolding pair_automaton_eps_simps
by (auto simp: pair_automaton_eps_simps)
(meson not_ftrancl_into)
qed (auto simp: pair_automaton_def)

lemma pair_eps_Some_Some:
fixes p q
defines "l ≡ (Some p, Some q)"
assumes "(l, r) |∈| (eps (pair_automaton A B))|⇧+|"
shows "fst r ≠ None ∧ snd r ≠ None ∧
(fst l ≠ fst r ⟶ (p, the (fst r)) |∈| (eps A)|⇧+|) ∧
(snd l ≠ snd r ⟶ (q, the (snd r)) |∈| (eps B)|⇧+|)"
using assms(2, 1)
proof (induct arbitrary: p q rule: ftrancl_induct)
case (Step b c)
then obtain r r' where *: "b = (Some r, Some r')" by (cases b) auto
show ?case using Step(2)
using pair_automaton_eps_Some_SomeD[OF  Step(3)[unfolded *]]
by (auto simp: *) (meson not_ftrancl_into)+
qed (auto simp: pair_automaton_def)

lemma pair_eps_Some_Some2:
fixes p q
defines "r ≡ (Some p, Some q)"
assumes "(l, r) |∈| (eps (pair_automaton A B))|⇧+|"
shows "fst l ≠ None ∧ snd l ≠ None ∧
(fst l ≠ fst r ⟶ (the (fst l), p) |∈| (eps A)|⇧+|) ∧
(snd l ≠ snd r ⟶ (the (snd l), q) |∈| (eps B)|⇧+|)"
using assms(2, 1)
proof (induct arbitrary: p q rule: ftrancl_induct)
case (Step b c)
from pair_automaton_eps_Some_SomeD2[OF Step(3)]
obtain r r' where *: "c = (Some r, Some r')" by (cases c) auto
from Step(2)[OF this] show ?case
using pair_automaton_eps_Some_SomeD[OF  Step(3)[unfolded *]]
by (auto simp: *) (meson not_ftrancl_into)+
qed (auto simp: pair_automaton_def)

lemma map_pair_automaton:
"pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) =
fmap_funs_ta (λ(a, b). (map_option f a, map_option g b)) (pair_automaton A B)" (is "?Ls = ?Rs")
proof -
let ?ls = "pair_rule ∘ map_prod (map_ta_rule id f) (map_ta_rule id g)"
let ?rs = "map_ta_rule id (λ(a, b). (map_option f a, map_option g b)) ∘ pair_rule"
have *: "(λ(a, b). (map_option f a, map_option g b)) ∘ lift_Some_None = lift_Some_None ∘ f"
"(λ(a, b). (map_option f a, map_option g b)) ∘ lift_None_Some = lift_None_Some ∘ g"
by (auto simp: comp_def)
have "?ls x = ?rs x" for x
by (cases x) (auto simp: ta_rule.map_sel)
then have [simp]: "?ls = ?rs" by blast
then have "rules ?Ls = rules ?Rs"
unfolding pair_automaton_def fmap_funs_ta_def
by (simp add: fimage_funion map_ta_rule_comp * map_prod_ftimes)
moreover have "eps ?Ls = eps ?Rs"
unfolding pair_automaton_def fmap_funs_ta_def
ultimately show ?thesis
by (intro TA_equalityI) simp
qed

lemmas map_pair_automaton_12 =
map_pair_automaton[of _ _ id, unfolded fmap_funs_ta_id option.map_id]
map_pair_automaton[of id _ _, unfolded fmap_funs_ta_id option.map_id]

lemma fmap_states_funs_ta_commute:
"fmap_states_ta f (fmap_funs_ta g A) = fmap_funs_ta g (fmap_states_ta f A)"
proof -
have [simp]: "map_ta_rule f id (map_ta_rule id g r) = map_ta_rule id g (map_ta_rule f id r)" for r
by (cases r) auto
show ?thesis
by (auto simp: ta_rule.case_distrib fmap_states_ta_def fmap_funs_ta_def fimage_iff fBex_def split: ta_rule.splits)
qed

lemma states_pair_automaton:
"𝒬 (pair_automaton A B) |⊆| (finsert None (Some |`| 𝒬 A) |×| (finsert None (Some |`| 𝒬 B)))"
unfolding pair_automaton_def
apply (intro 𝒬_subseteq_I)
apply (auto simp: ta_rule.map_sel in_fset_conv_nth nth_zip_fill rule_statesD eps_statesD)
done

lemma swap_pair_automaton:
assumes "(p, q) |∈| ta_der (pair_automaton A B) (term_of_gterm t)"
shows "(q, p) |∈| ta_der (pair_automaton B A) (term_of_gterm (map_gterm prod.swap t))"
proof -
let ?m = "map_ta_rule prod.swap prod.swap"
have [simp]: "map prod.swap (zip_fill xs ys) = zip_fill ys xs" for xs ys
by (auto simp: zip_fill_def zip_nth_conv comp_def intro!: nth_equalityI)
let ?swp = "λX. fmap_states_ta prod.swap (fmap_funs_ta prod.swap X)"
{ fix A B
let ?AB = "?swp (pair_automaton A B)" and ?BA = "pair_automaton B A"
have "eps ?AB |⊆| eps ?BA" "rules ?AB |⊆| rules ?BA"
by (auto simp: fmap_states_ta_def fmap_funs_ta_def pair_automaton_def
fimage_funion comp_def prod.map_comp ta_rule.map_comp)
} note * = this
let ?BA = "?swp (?swp (pair_automaton B A))" and ?AB = "?swp (pair_automaton A B)"
have **: "r |∈| rules (pair_automaton B A) ⟹ ?m r |∈| ?m |`| rules (pair_automaton B A)" for r
by blast
have "r |∈| rules ?BA ⟹ r |∈| rules ?AB" "e |∈| eps ?BA ⟹ e |∈| eps ?AB" for r e
using *[of B A] map_ta_rule_prod_swap_id
unfolding fmap_funs_ta_def fmap_states_ta_def ta.sel
by (auto simp: map_ta_rule_comp image_iff ta_rule.map_id0 intro!: bexI[of _ "?m r"])
then have "eps ?BA |⊆| eps ?AB" "rules ?BA |⊆| rules ?AB"
by blast+
then have "fmap_states_ta prod.swap (fmap_funs_ta prod.swap (pair_automaton A B)) = pair_automaton B A"
using *[of A B] by (simp add: fmap_states_funs_ta_commute fmap_funs_ta_comp fmap_states_ta_comp TA_equalityI)
then show ?thesis
using ta_der_fmap_states_ta[OF ta_der_fmap_funs_ta[OF assms], of prod.swap prod.swap]
qed

lemma to_ta_der_pair_automaton:
"p |∈| ta_der A (term_of_gterm t) ⟹
(Some p, None) |∈| ta_der (pair_automaton A B) (term_of_gterm (map_gterm (λf. (Some f, None)) t))"
"q |∈| ta_der B (term_of_gterm u) ⟹
(None, Some q) |∈| ta_der (pair_automaton A B) (term_of_gterm (map_gterm (λf. (None, Some f)) u))"
"p |∈| ta_der A (term_of_gterm t) ⟹ q |∈| ta_der B (term_of_gterm u) ⟹
(Some p, Some q) |∈| ta_der (pair_automaton A B) (term_of_gterm (gpair t u))"
proof (goal_cases sn ns ss)
let ?AB = "pair_automaton A B"
have 1: "(Some p, None) |∈| ta_der (pair_automaton A B) (term_of_gterm (map_gterm (λf. (Some f, None)) s))"
if "p |∈| ta_der A (term_of_gterm s)" for A B p s
proof (rule fsubsetD[OF ta_der_mono])
show "rules (fmap_states_ta lift_Some_None (fmap_funs_ta lift_Some_None A)) |⊆|
rules (pair_automaton A B)"
by (auto simp: fmap_states_ta_def fmap_funs_ta_def comp_def ta_rule.map_comp
pair_automaton_def)
next
show "eps (fmap_states_ta lift_Some_None (fmap_funs_ta lift_Some_None A)) |⊆|
eps (pair_automaton A B)"
by (rule fsubsetI)
(auto simp: fmap_states_ta_def fmap_funs_ta_def pair_automaton_def comp_def fimage.rep_eq
dest: eps_to_pair_eps_Some_None)
next
show "lift_Some_None p |∈| ta_der
(fmap_states_ta lift_Some_None (fmap_funs_ta lift_Some_None A))
(term_of_gterm (gterm_to_Some_None s))"
using ta_der_fmap_states_ta[OF ta_der_fmap_funs_ta[OF that], of lift_Some_None]
using ta_der_fmap_funs_ta ta_der_to_fmap_states_der that by fastforce
qed
have 2: "q |∈| ta_der B (term_of_gterm t) ⟹
(None, Some q) |∈| ta_der ?AB (term_of_gterm (map_gterm (λg. (None, Some g)) t))"
for q t using swap_pair_automaton[OF 1[of q B t A]] by (simp add: gterm.map_comp comp_def)
{
case sn then show ?case by (rule 1)
next
case ns then show ?case by (rule 2)
next
case ss then show ?case
proof (induct t arbitrary: p q u)
case (GFun f ts)
obtain g us where u [simp]: "u = GFun g us" by (cases u)
obtain p' ps where p': "f ps → p' |∈| rules A" "p' = p ∨ (p', p) |∈| (eps A)|⇧+|" "length ps = length ts"
"⋀i. i < length ts ⟹ ps ! i |∈| ta_der A (term_of_gterm (ts ! i))" using GFun(2) by auto
obtain q' qs where q': "g qs → q' |∈| rules B" "q' = q ∨ (q', q) |∈| (eps B)|⇧+|" "length qs = length us"
"⋀i. i < length us ⟹ qs ! i |∈| ta_der B (term_of_gterm (us ! i))" using GFun(3) by auto
have *: "Some p |∈| Some |`| 𝒬 A" "Some q' |∈| Some |`| 𝒬 B"
using p'(2,1) q'(1)
by (auto simp: rule_statesD eps_trancl_statesD)
have eps: "p' = p ∧ q' = q ∨ ((Some p', Some q'), (Some p, Some q)) |∈| (eps ?AB)|⇧+|"
proof (cases "p' = p")
case True note p = this then show ?thesis
proof (cases "q' = q")
case False
then have "(q', q) |∈| (eps B)|⇧+|" using q'(2) by auto
hence "((Some p', Some q'), Some p', Some q) |∈| (eps (pair_automaton A B))|⇧+|"
proof (rule ftrancl_map[rotated])
fix x y
assume "(x, y) |∈| eps B"
thus "((Some p', Some x), Some p', Some y) |∈| eps (pair_automaton A B)"
using p'(1)[THEN rule_statesD(1), simplified]
apply (simp add: pair_automaton_def image_iff fSigma.rep_eq)
by fastforce
qed
thus ?thesis
next
case False note p = this
then have *: "(p', p) |∈| (eps A)|⇧+|" using p'(2) by auto
then have eps: "((Some p', Some q'), Some p, Some q') |∈| (eps (pair_automaton A B))|⇧+|"
proof (rule ftrancl_map[rotated])
fix x y
assume "(x, y) |∈| eps A"
then show "((Some x, Some q'), Some y, Some q') |∈| eps (pair_automaton A B)"
using q'(1)[THEN rule_statesD(1), simplified]
apply (simp add: pair_automaton_def image_iff fSigma.rep_eq)
by fastforce
qed
then show ?thesis
proof (cases "q' = q")
case True then show ?thesis using eps
by simp
next
case False
then have "(q', q) |∈| (eps B)|⇧+|" using q'(2) by auto
then have "((Some p, Some q'), Some p, Some q) |∈| (eps (pair_automaton A B))|⇧+|"
apply (rule ftrancl_map[rotated])
using *[THEN eps_trancl_statesD]
apply (simp add: p pair_automaton_def image_iff fSigma.rep_eq)
by fastforce

then show ?thesis using eps
by (meson ftrancl_trans)
qed
qed
have "(Some f, Some g) zip_fill ps qs → (Some p', Some q') |∈| rules ?AB"
using p'(1) q'(1) by (force simp: pair_automaton_def)
then show ?case using GFun(1)[OF nth_mem p'(4) q'(4)] p'(1 - 3)  q'(1 - 3) eps
using 1[OF p'(4), of _ B] 2[OF q'(4)]
by (auto simp: gpair_code nth_zip_fill less_max_iff_disj
intro!: exI[of _ "zip_fill ps qs"] exI[of _ "Some p'"] exI[of _ "Some q'"])
qed
}
qed

lemma from_ta_der_pair_automaton:
"(None, None) |∉| ta_der (pair_automaton A B) (term_of_gterm s)"
"(Some p, None) |∈| ta_der (pair_automaton A B) (term_of_gterm s) ⟹
∃t. p |∈| ta_der A (term_of_gterm t) ∧ s = map_gterm (λf. (Some f, None)) t"
"(None, Some q) |∈| ta_der (pair_automaton A B) (term_of_gterm s) ⟹
∃u. q |∈| ta_der B (term_of_gterm u) ∧ s = map_gterm (λf. (None, Some f)) u"
"(Some p, Some q) |∈| ta_der (pair_automaton A B) (term_of_gterm s) ⟹
∃t u. p |∈| ta_der A (term_of_gterm t) ∧ q |∈| ta_der B (term_of_gterm u) ∧ s = gpair t u"
proof (goal_cases nn sn ns ss)
let ?AB = "pair_automaton A B"
{ fix p s A B assume "(Some p, None) |∈| ta_der (pair_automaton A B) (term_of_gterm s)"
then have "∃t. p |∈| ta_der A (term_of_gterm t) ∧ s = map_gterm (λf. (Some f, None)) t"
proof (induct s arbitrary: p)
case (GFun h ss)
obtain rs sp nq where r: "h rs → (sp, nq) |∈| rules (pair_automaton A B)"
"sp = Some p ∧ nq = None ∨ ((sp, nq), (Some p, None)) |∈| (eps (pair_automaton A B))|⇧+|" "length rs = length ss"
"⋀i. i < length ss ⟹ rs ! i |∈| ta_der (pair_automaton A B) (term_of_gterm (ss ! i))"
using GFun(2) by auto
obtain p' where pq: "sp = Some p'" "nq = None" "p' = p ∨ (p', p) |∈| (eps A)|⇧+|"
using r(2) pair_eps_Some_None[of sp nq p A B]
by (cases sp) auto
obtain f ps where h: "h = lift_Some_None f" "rs = map lift_Some_None ps"
"f ps → p' |∈| rules A"
using r(1) unfolding pq(1, 2) by (auto simp: pair_automaton_def map_ta_rule_cases)
obtain ts where "⋀i. i < length ss ⟹
ps ! i |∈| ta_der A (term_of_gterm (ts i)) ∧ ss ! i = map_gterm (λf. (Some f, None)) (ts i)"
using GFun(1)[OF nth_mem, of i "ps ! i" for i] r(4)[unfolded h(2)] r(3)[unfolded h(2) length_map]
by auto metis
then show ?case using h(3) pq(3) r(3)[unfolded h(2) length_map]
by (intro exI[of _ "GFun f (map ts [0..<length ss])"]) (auto simp: h(1) intro!: nth_equalityI)
qed
} note 1 = this
have 2: "∃u. q |∈| ta_der B (term_of_gterm u) ∧ s = map_gterm (λg. (None, Some g)) u"
if "(None, Some q) |∈| ta_der ?AB (term_of_gterm s)" for q s
using 1[OF swap_pair_automaton, OF that]
by (auto simp: gterm.map_comp comp_def gterm.map_ident
dest!: arg_cong[of "map_gterm prod.swap _" _ "map_gterm prod.swap", unfolded gterm.map_comp])
{
case nn
then show ?case
by (intro ta_der_not_reach) (auto simp: pair_automaton_def map_ta_rule_cases)
next
case sn then show ?case by (rule 1)
next
case ns then show ?case by (rule 2)
next
case ss then show ?case
proof (induct s arbitrary: p q)
case (GFun h ss)
obtain rs sp sq where r: "h rs → (sp, sq) |∈| rules ?AB"
"sp = Some p ∧ sq = Some q ∨ ((sp, sq), (Some p, Some q)) |∈| (eps ?AB)|⇧+|" "length rs = length ss"
"⋀i. i < length ss ⟹ rs ! i |∈| ta_der ?AB (term_of_gterm (ss ! i))"
using GFun(2) by auto
from r(2) have "sp ≠ None" "sq ≠ None" using pair_eps_Some_Some2[of "(sp, sq)" p q]
by auto
then obtain p' q' where pq: "sp = Some p'" "sq = Some q'"
"p' = p ∨ (p', p) |∈| (eps A)|⇧+|" "q' = q ∨ (q', q) |∈| (eps B)|⇧+|"
using r(2) pair_eps_Some_Some[where ?r = "(Some p, Some q)" and ?A = A and ?B = B]
using pair_eps_Some_Some2[of "(sp, sq)" p q]
by (cases sp; cases sq) auto
obtain f g ps qs where h: "h = (Some f, Some g)" "rs = zip_fill ps qs"
"f ps → p' |∈| rules A" "g qs → q' |∈| rules B"
using r(1) unfolding pq(1,2) by (auto simp: pair_automaton_def map_ta_rule_cases)
have *: "∃t u. ps ! i |∈| ta_der A (term_of_gterm t) ∧ qs ! i |∈| ta_der B (term_of_gterm u) ∧ ss ! i = gpair t u"
if "i < length ps" "i < length qs" for i
using GFun(1)[OF nth_mem, of i "ps ! i" "qs ! i"] r(4)[unfolded pq(1,2) h(2), of i] that
r(3)[symmetric] by (auto simp: nth_zip_fill h(2))
{ fix i assume "i < length ss"
then have "∃t u. (i < length ps ⟶ ps ! i |∈| ta_der A (term_of_gterm t)) ∧
(i < length qs ⟶ qs ! i |∈| ta_der B (term_of_gterm u)) ∧
ss ! i = gpair_impl (if i < length ps then Some t else None) (if i < length qs then Some u else None)"
using *[of i] 1[of "ps ! i" A B "ss ! i"] 2[of "qs ! i" "ss ! i"] r(4)[of i] r(3)[symmetric]
by (cases "i < length ps"; cases "i < length qs")
(auto simp add: h(2) nth_zip_fill less_max_iff_disj gpair_code split: gterm.splits) }
then obtain ts us where "⋀i. i < length ss ⟹
(i < length ps ⟶ ps ! i |∈| ta_der A (term_of_gterm (ts i))) ∧
(i < length qs ⟶ qs ! i |∈| ta_der B (term_of_gterm (us i))) ∧
ss ! i = gpair_impl (if i < length ps then Some (ts i) else None) (if i < length qs then Some (us i) else None)"
by metis
moreover then have "⋀i. i < length ps ⟹ ps ! i |∈| ta_der A (term_of_gterm (ts i))"
"⋀i. i < length qs ⟹ qs ! i |∈| ta_der B (term_of_gterm (us i))"
using r(3)[unfolded h(2)] by auto
ultimately show ?case using h(3,4) pq(3,4) r(3)[symmetric]
by (intro exI[of _ "GFun f (map ts [0..<length ps])"] exI[of _ "GFun g (map us [0..<length qs])"])
(auto simp: gpair_code h(1,2) less_max_iff_disj nth_zip_fill intro!: nth_equalityI split: prod.splits gterm.splits)
qed
}
qed

lemma diagonal_automaton:
assumes "RR1_spec A R"
shows "RR2_spec (fmap_funs_reg (λf. (Some f, Some f)) A) {(s, s) | s. s ∈ R}" using assms
by (auto simp: RR2_spec_def RR1_spec_def fmap_funs_reg_def fmap_funs_gta_lang map_funs_term_some_gpair ℒ_def)

lemma pair_automaton:
assumes "RR1_spec A T" "RR1_spec B U"
shows "RR2_spec (pair_automaton_reg A B) (T × U)"
proof -
let ?AB = "pair_automaton (ta A) (ta B)"
{ fix t u assume t: "t ∈ T" and u: "u ∈ U"
obtain p where p: "p |∈| fin A" "p |∈| ta_der (ta A) (term_of_gterm t)" using t assms(1)
by (auto simp: RR1_spec_def gta_lang_def ℒ_def gta_der_def)
obtain q where q: "q |∈| fin B" "q |∈| ta_der (ta B) (term_of_gterm u)" using u assms(2)
by (auto simp: RR1_spec_def gta_lang_def ℒ_def gta_der_def)
have "gpair t u ∈ ℒ (pair_automaton_reg A B)" using p(1) q(1) to_ta_der_pair_automaton(3)[OF p(2) q(2)]
by (auto simp: pair_automaton_reg_def ℒ_def)
} moreover
{ fix s assume "s ∈ ℒ (pair_automaton_reg A B)"
from this[unfolded gta_lang_def ℒ_def]
obtain r where r: "r |∈| fin (pair_automaton_reg A B)" "r |∈| gta_der ?AB s"
by (auto simp: pair_automaton_reg_def)
obtain p q where pq: "r = (Some p, Some q)" "p |∈| fin A" "q |∈| fin B"
using r(1) by (auto simp: pair_automaton_reg_def)
from from_ta_der_pair_automaton(4)[OF r(2)[unfolded pq(1) gta_der_def]]
obtain t u where "p |∈| ta_der (ta A) (term_of_gterm t)" "q |∈| ta_der (ta B) (term_of_gterm u)" "s = gpair t u"
by (elim exE conjE) note * = this
then have "t ∈ ℒ A" "u ∈ ℒ B" using pq(2,3)
by (auto simp: ℒ_def)
then have "∃t u. s = gpair t u ∧ t ∈ T ∧ u ∈ U" using assms
by (auto simp: RR1_spec_def *(3) intro!: exI[of _ t, OF exI[of _ u]])
} ultimately show ?thesis by (auto simp: RR2_spec_def)
qed

lemma pair_automaton':
shows "ℒ (pair_automaton_reg A B) = case_prod gpair ` (ℒ A × ℒ B)"
using pair_automaton[of A _ B] by (auto simp: RR1_spec_def RR2_spec_def)

subsection ‹Collapsing›

text ‹cf. @{const "gcollapse"}.›

fun collapse_state_list where
"collapse_state_list Qn Qs [] = [[]]"
| "collapse_state_list Qn Qs (q # qs) = (let rec = collapse_state_list Qn Qs qs in
(if q |∈| Qn ∧ q |∈| Qs then map (Cons None) rec @ map (Cons (Some q)) rec
else if q |∈| Qn then map (Cons None) rec
else if q |∈| Qs then map (Cons (Some q)) rec
else [[]]))"

lemma collapse_state_list_inner_length:
assumes "qss = collapse_state_list Qn Qs qs"
and "∀ i < length qs. qs ! i |∈| Qn ∨ qs ! i |∈| Qs"
and "i < length qss"
shows "length (qss ! i) = length qs" using assms
proof (induct qs arbitrary: qss i)
case (Cons q qs)
have "∀i<length qs. qs ! i |∈| Qn ∨ qs ! i |∈| Qs" using Cons(3) by auto
then show ?case using Cons(1)[of "collapse_state_list Qn Qs qs"] Cons(2-)
by (auto simp: Let_def nth_append)
qed auto

lemma collapse_fset_inv_constr:
assumes "∀ i < length qs'. qs ! i |∈| Qn ∧ qs' ! i = None ∨
qs ! i |∈| Qs ∧ qs' ! i = Some (qs ! i)"
and "length qs = length qs'"
shows "qs' |∈| fset_of_list (collapse_state_list Qn Qs qs)" using assms
proof (induct qs arbitrary: qs')
case (Cons q qs)
have "(tl qs') |∈| fset_of_list (collapse_state_list Qn Qs qs)" using Cons(2-)
by (intro Cons(1)[of "tl qs'"]) (cases qs', auto)
then show ?case using Cons(2-)
by (cases qs') (auto simp: Let_def image_def)
qed auto

lemma collapse_fset_inv_constr2:
assumes "∀ i < length qs. qs ! i |∈| Qn ∨ qs ! i |∈| Qs"
and "qs' |∈| fset_of_list (collapse_state_list Qn Qs qs)" and "i < length qs'"
shows "qs ! i |∈| Qn ∧ qs' ! i = None ∨ qs ! i |∈| Qs ∧ qs' ! i = Some (qs ! i)"
using assms
proof (induct qs arbitrary: qs' i)
case (Cons a qs)
have "i ≠ 0 ⟹ qs ! (i - 1) |∈| Qn ∧ tl qs' ! (i - 1) = None ∨ qs ! (i - 1) |∈| Qs ∧ tl qs' ! (i - 1) = Some (qs ! (i - 1))"
using Cons(2-)
by (intro Cons(1)[of "tl qs'" "i - 1"]) (auto simp: Let_def split: if_splits)
then show ?case using Cons(2-)
by (cases i) (auto simp: Let_def split: if_splits)
qed auto

definition collapse_rule where
"collapse_rule A Qn Qs =
|⋃| ((λ r. fset_of_list (map (λ qs. TA_rule (r_root r) qs (Some (r_rhs r))) (collapse_state_list Qn Qs (r_lhs_states r)))) |`|
ffilter (λ r. (∀ i < length (r_lhs_states r). r_lhs_states r ! i |∈| Qn ∨ r_lhs_states r ! i |∈| Qs))
(ffilter (λ r. r_root r ≠ None) (rules A)))"

definition collapse_rule_fset where
"collapse_rule_fset A Qn Qs = (λ r. TA_rule (the (r_root r)) (map the (filter (λq. ¬ Option.is_none q) (r_lhs_states r))) (the (r_rhs r))) |`|
collapse_rule A Qn Qs"

lemma collapse_rule_set_conv:
"fset (collapse_rule_fset A Qn Qs) = {TA_rule f (map the (filter (λq. ¬ Option.is_none q) qs')) q | f qs qs' q.
TA_rule (Some f) qs q |∈| rules A ∧ length qs = length qs' ∧
(∀i < length qs. qs ! i |∈| Qn ∧ qs' ! i = None ∨ qs ! i |∈| Qs ∧ (qs' ! i) = Some (qs ! i))} " (is "?Ls = ?Rs")
proof
{fix f qs' q qs assume ass: "TA_rule (Some f) qs q |∈| rules A"
"length qs = length qs'"
"∀i < length qs. qs ! i |∈| Qn ∧ qs' ! i = None ∨ qs ! i |∈| Qs ∧ (qs' ! i) = Some (qs ! i)"
then have "TA_rule (Some f) qs' (Some q) |∈| collapse_rule A Qn Qs"
using collapse_fset_inv_constr[of qs' qs Qn Qs] unfolding collapse_rule_def
by (auto simp: fset_of_list.rep_eq fimage_iff intro!: bexI[of _ "TA_rule (Some f) qs q"])
then have "TA_rule f (map the (filter (λq. ¬ Option.is_none q) qs')) q ∈ ?Ls"
unfolding collapse_rule_fset_def
by (auto simp: image_iff Bex_def intro!: exI[of _"TA_rule (Some f) qs' (Some q)"])}
then show "?Rs ⊆ ?Ls" by blast
next
{fix f qs q assume ass: "TA_rule f qs q ∈ ?Ls"
then obtain ps qs' where w: "TA_rule (Some f) ps q |∈| rules A"
"∀ i < length ps. ps ! i |∈| Qn ∨ ps ! i |∈| Qs"
"qs' |∈| fset_of_list (collapse_state_list Qn Qs ps)"
"qs = map the (filter (λq. ¬ Option.is_none q) qs')"
unfolding collapse_rule_fset_def collapse_rule_def
by (auto simp: ffUnion.rep_eq fset_of_list.rep_eq) (metis ta_rule.collapse)
then have "∀ i < length qs'. ps ! i |∈| Qn ∧ qs' ! i = None ∨ ps ! i |∈| Qs ∧ qs' ! i = Some (ps ! i)"
using collapse_fset_inv_constr2
by metis
moreover have "length ps = length qs'"
using collapse_state_list_inner_length[of _ Qn Qs ps]
using w(2, 3) calculation(1)
by (auto simp: in_fset_conv_nth)
ultimately have "TA_rule f qs q ∈ ?Rs"
using w(1) unfolding w(4)
by auto fastforce}
then show "?Ls ⊆ ?Rs"
by (intro subsetI) (metis (no_types, lifting) ta_rule.collapse)
qed

lemma collapse_rule_fmember [simp]:
"TA_rule f qs q |∈| (collapse_rule_fset A Qn Qs) ⟷ (∃ qs' ps.
qs = map the (filter (λq. ¬ Option.is_none q) qs') ∧ TA_rule (Some f) ps q |∈| rules A ∧ length ps = length qs' ∧
(∀i < length ps. ps ! i |∈| Qn ∧ qs' ! i = None ∨ ps ! i |∈| Qs ∧ (qs' ! i) = Some (ps ! i)))"
unfolding collapse_rule_set_conv
by auto

definition "Qn A ≡ (let S = (r_rhs |`| ffilter (λ r. r_root r = None) (rules A)) in (eps A)|⇧+| |``| S |∪| S)"
definition "Qs A ≡ (let S = (r_rhs |`| ffilter (λ r. r_root r ≠ None) (rules A)) in (eps A)|⇧+| |``| S |∪| S)"

lemma Qn_member_iff [simp]:
"q |∈| Qn A ⟷ (∃ ps p. TA_rule None ps p |∈| rules A ∧ (p = q ∨ (p, q) |∈| (eps A)|⇧+|))" (is "?Ls ⟷ ?Rs")
proof -
{assume ass: "q |∈| Qn A" then obtain r where
"r_rhs r = q ∨ (r_rhs r, q) |∈| (eps A)|⇧+|" "r |∈| rules A" "r_root r = None"
by (force simp: Qn_def Image_def image_def Let_def fImage.rep_eq)
then have "?Ls ⟹ ?Rs"  by (cases r) auto}
moreover have "?Rs ⟹ ?Ls" by (force simp: Qn_def Image_def image_def Let_def fImage.rep_eq)
ultimately show ?thesis by blast
qed

lemma Qs_member_iff [simp]:
"q |∈| Qs A ⟷ (∃ f ps p. TA_rule (Some f) ps p |∈| rules A ∧ (p = q ∨ (p, q) |∈| (eps A)|⇧+|))"  (is "?Ls ⟷ ?Rs")
proof -
{assume ass: "q |∈| Qs A" then obtain f r where
"r_rhs r = q ∨ (r_rhs r, q) |∈| (eps A)|⇧+|" "r |∈| rules A" "r_root r = Some f"
by (force simp: Qs_def Image_def image_def Let_def fImage.rep_eq)
then have "?Ls ⟹ ?Rs"  by (cases r) auto}
moreover have "?Rs ⟹ ?Ls" by (force simp: Qs_def Image_def image_def Let_def fImage.rep_eq)
ultimately show ?thesis by blast
qed

lemma collapse_Qn_Qs_set_conv:
"fset (Qn A) = {q' |qs q q'. TA_rule None qs q |∈| rules A ∧ (q = q' ∨ (q, q') |∈| (eps A)|⇧+|)}" (is "?Ls1 = ?Rs1")
"fset (Qs A) = {q' |f qs q q'. TA_rule (Some f) qs q |∈| rules A ∧ (q = q' ∨ (q, q') |∈| (eps A)|⇧+|)}"  (is "?Ls2 = ?Rs2")
by auto force+

definition collapse_automaton :: "('q, 'f option) ta ⇒ ('q, 'f) ta" where
"collapse_automaton A = TA (collapse_rule_fset A (Qn A) (Qs A)) (eps A)"

definition collapse_automaton_reg where
"collapse_automaton_reg R = Reg (fin R) (collapse_automaton (ta R))"

lemma ta_states_collapse_automaton:
"𝒬 (collapse_automaton A) |⊆| 𝒬 A"
apply (intro 𝒬_subseteq_I)
apply (auto simp: collapse_automaton_def collapse_Qn_Qs_set_conv collapse_rule_set_conv
fset_of_list.rep_eq in_set_conv_nth rule_statesD eps_statesD[unfolded])
apply (metis Option.is_none_def fnth_mem option.sel rule_statesD(3) ta_rule.sel(2))
done

lemma last_nthI:
assumes "i < length ts" "¬ i < length ts - Suc 0"
shows "ts ! i = last ts" using assms
by (induct ts arbitrary: i)
(auto, metis last_conv_nth length_0_conv less_antisym nth_Cons')

lemma collapse_automaton':
assumes "𝒬 A |⊆| ta_reachable A" (* cf. ta_trim *)
shows "gta_lang Q (collapse_automaton A) = the ` (gcollapse ` gta_lang Q A - {None})"
proof -
define Qn' where "Qn' = Qn A"
define Qs' where "Qs' = Qs A"
{fix t assume t: "t ∈ gta_lang Q (collapse_automaton A)"
then obtain q where q: "q |∈| Q" "q |∈| ta_der (collapse_automaton A) (term_of_gterm t)" by auto
have "∃ t'. q |∈| ta_der A (term_of_gterm t') ∧ gcollapse t' ≠ None ∧ t = the (gcollapse t')" using q(2)
proof (induct rule: ta_der_gterm_induct)
case (GFun f ts ps p q)
from GFun(1 - 3) obtain qs rs where ps: "TA_rule (Some f) qs p |∈| rules A" "length qs = length rs"
"⋀i. i < length qs ⟹ qs ! i |∈| Qn' ∧ rs ! i = None ∨ qs ! i |∈| Qs' ∧ rs ! i = Some (qs ! i)"
"ps = map the (filter (λq. ¬ Option.is_none q) rs)"
by (auto simp: collapse_automaton_def Qn'_def Qs'_def)
obtain ts' where ts':
"ps ! i |∈| ta_der A (term_of_gterm (ts' i))" "gcollapse (ts' i) ≠ None" "ts ! i = the (gcollapse (ts' i))"
if "i < length ts" for i using GFun(5) by metis
from ps(2, 3, 4) have rs: "i < length qs ⟹ rs ! i = None ∨ rs ! i = Some (qs ! i)" for i
by auto
{fix i assume "i < length qs" "rs ! i = None"
then have "∃ t'. groot_sym t' = None ∧ qs ! i |∈| ta_der A (term_of_gterm t')"
using ps(1, 2) ps(3)[of i]
by (auto simp: ta_der_trancl_eps Qn'_def groot_sym_groot_conv elim!: ta_reachable_rule_gtermE[OF assms])
(force dest: ta_der_trancl_eps)+}
note None = this
{fix i assume i: "i < length qs" "rs ! i = Some (qs ! i)"
have "map Some ps = filter (λq. ¬ Option.is_none q) rs" using ps(4)
by (induct rs arbitrary: ps) (auto simp add: Option.is_none_def)
from filter_rev_nth_idx[OF _ _ this, of i]
have *: "rs ! i = map Some ps ! filter_rev_nth (λq. ¬ Option.is_none q) rs i"
"filter_rev_nth (λq. ¬ Option.is_none q) rs i < length ps"
using ps(2, 4) i by auto
then have "the (rs ! i) = ps ! filter_rev_nth (λq. ¬ Option.is_none q) rs i"
"filter_rev_nth (λq. ¬ Option.is_none q) rs i < length ps"
by auto} note Some = this
let ?P = "λ t i. qs ! i |∈| ta_der A (term_of_gterm t) ∧
(rs ! i = None ⟶ groot_sym t = None) ∧
(rs ! i = Some (qs ! i) ⟶ t = ts' (filter_rev_nth (λq. ¬ Option.is_none q) rs i))"
{fix i assume i: "i < length qs"
then have "∃ t. ?P t i" using Some[OF i] None[OF i] ts' ps(2, 4) GFun(2) rs[OF i]
by (cases "rs ! i") auto}
then obtain ts'' where ts'': "length ts'' = length qs"
"i < length qs ⟹ qs ! i |∈| ta_der A (term_of_gterm (ts'' ! i))"
"i < length qs ⟹ rs ! i = None ⟹ groot_sym (ts'' ! i) = None"
"i < length qs ⟹ rs ! i = Some (qs ! i) ⟹ ts'' ! i = ts' (filter_rev_nth (λq. ¬ Option.is_none q) rs i)"
for i using that Ex_list_of_length_P[of "length qs" ?P] by auto
from  ts''(1, 3, 4) Some ps(2, 4) GFun(2) rs ts'(2-)
have "map Some ts = (filter (λq. ¬ Option.is_none q) (map gcollapse ts''))"
proof (induct ts'' arbitrary: qs rs ps ts rule: rev_induct)
case (snoc a us)
from snoc(2, 7) obtain r rs' where [simp]: "rs = rs' @ [r]"
by (metis append_butlast_last_id append_is_Nil_conv length_0_conv not_Cons_self2)
have l: "length us = length (butlast qs)" "length (butlast qs) = length (butlast rs)"
using snoc(2, 7) by auto
have *: "i < length (butlast qs) ⟹ butlast rs ! i = None ⟹ groot_sym (us ! i) = None" for i
using snoc(3)[of i] snoc(2, 7)
by (auto simp:nth_append l(1) nth_butlast split!: if_splits)
have **: "i < length (butlast qs) ⟹ butlast rs ! i = None ∨ butlast rs ! i = Some (butlast qs ! i)" for i
using snoc(10)[of i] snoc(2, 7) l by (auto simp: nth_append nth_butlast)
have "i < length (butlast qs) ⟹ butlast rs ! i = Some (butlast qs ! i) ⟹
us ! i = ts' (filter_rev_nth (λq. ¬ Option.is_none q) (butlast rs) i)" for i
using snoc(4)[of i] snoc(2, 7) l
by (auto simp: nth_append nth_butlast filter_rev_nth_def take_butlast)
note IH = snoc(1)[OF l(1) * this _ _ l(2) _ _ **]
show ?case
proof (cases "r = None")
case True
then have "map Some ts = filter (λq. ¬ Option.is_none q) (map gcollapse us)"
using snoc(2, 5-)
by (intro IH[of ps ts]) (auto simp: nth_append nth_butlast filter_rev_nth_butlast)
then show ?thesis using True snoc(2, 7) snoc(3)[of "length (butlast rs)"]
by (auto simp: nth_append l(1) last_nthI split!: if_splits)
next
case False
then obtain t' ss where *: "ts = ss @ [t']" using snoc(2, 7, 8, 9)
by (cases ts) (auto, metis append_butlast_last_id list.distinct(1))
let ?i = "filter_rev_nth (λq. ¬ Option.is_none q) rs (length us)"
have "map Some (butlast ts) = filter (λq. ¬ Option.is_none q) (map gcollapse us)"
using False snoc(2, 5-) l filter_rev_nth_idx
by (intro IH[of "butlast ps" "butlast ts"])
(fastforce simp: nth_butlast filter_rev_nth_butlast)+
moreover have "a = ts' ?i" "?i < length ps"
using False snoc(2, 9) l snoc(4, 6, 10)[of "length us"]
by (auto simp: nth_append)
moreover have "filter_rev_nth (λq. ¬ Option.is_none q) (rs' @ [r]) (length rs') = length ss"
using l snoc(2, 7, 8, 9) False unfolding *
by (auto simp: filter_rev_nth_def)
ultimately show ?thesis using l snoc(2, 7, 9) snoc(11-)[of ?i]
by (auto simp: nth_append *)
qed
qed simp
then have "ts = map the (filter (λt. ¬ Option.is_none t) (map gcollapse ts''))"
by (metis comp_the_Some list.map_id map_map)
then show ?case using ps(1, 2) ts''(1, 2) GFun(3)
by (auto simp: collapse_automaton_def intro!: exI[of _ "GFun (Some f) ts''"] exI[of _ qs] exI[of _ p])
qed
then have "t ∈ the ` (gcollapse ` gta_lang Q A - {None})"
by (meson Diff_iff gta_langI imageI q(1) singletonD)
} moreover
{ fix t assume t: "t ∈ gta_lang Q A" "gcollapse t ≠ None"
obtain q where q: "q |∈| Q" "q |∈| ta_der A (term_of_gterm t)" using t(1) by auto
have "q |∈| ta_der (collapse_automaton A) (term_of_gterm (the (gcollapse t)))" using q(2) t(2)
proof (induct t arbitrary: q)
case (GFun f ts)
obtain qs q' where q: "TA_rule f qs q' |∈| rules A" "q' = q ∨ (q', q) |∈| (eps ```