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
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)
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
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
by (simp add: ghole_pos_in_apply)
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)
lemma ground_ctxt_adapt_ground [intro]:
assumes "ground_ctxt C"
shows "ground_ctxt (adapt_vars_ctxt C)"
using assms by (induct C) auto
lemma adapt_vars_ctxt2 :
assumes "ground_ctxt C"
shows "adapt_vars_ctxt (adapt_vars_ctxt C) = adapt_vars_ctxt C" using assms
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]
by (simp add: gunions_def gencode_def)
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"
by (simp add: RR1_spec_def)
lemma relabel_RR2_spec [simp]:
"RR2_spec (relabel_reg A) T ⟷ RR2_spec A T"
by (simp add: RR2_spec_def)
lemma relabel_RRn_spec [simp]:
"RRn_spec n (relabel_reg A) T ⟷ RRn_spec n A T"
by (simp add: RRn_spec_def)
lemma trim_RR1_spec [simp]:
"RR1_spec (trim_reg A) T ⟷ RR1_spec A T"
by (simp add: RR1_spec_def ℒ_trim)
lemma trim_RR2_spec [simp]:
"RR2_spec (trim_reg A) T ⟷ RR2_spec A T"
by (simp add: RR2_spec_def ℒ_trim)
lemma trim_RRn_spec [simp]:
"RRn_spec n (trim_reg A) T ⟷ RRn_spec n A T"
by (simp add: RRn_spec_def ℒ_trim)
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
by (simp add: fimage_funion 𝒬_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)
apply (simp add: rule_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]
by (simp add: gterm.map_comp comp_def)
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
by (simp add: p)
qed (simp add: p)
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"
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 (collapse_automaton A))|⇧+|"
"length qs = length ts" "⋀i. i < length ts ⟹ qs ! i |∈| ta_der A (term_of_gterm (ts ! i))"
using GFun(2) by (auto simp: collapse_automaton_def)
obtain f' where f [simp]: "f = Some f'" using GFun(3) by (cases f) auto
define qs' where
"qs' = map (λi. if Option.is_none (gcollapse (ts ! i)) then None else Some (qs ! i)) [0..<length qs]"
have "Option.is_none (gcollapse (ts ! i)) ⟹ qs ! i |∈| Qn'" if "i < length qs" for i
using q(4)[of i] that
by (cases "ts ! i" rule: gcollapse.cases)
(auto simp: q(3) Qn'_def collapse_Qn_Qs_set_conv)
moreover have "¬ Option.is_none (gcollapse (ts ! i)) ⟹ qs ! i |∈| Qs'" if "i < length qs" for i
using q(4)[of i] that
by (cases "ts ! i" rule: gcollapse.cases)
(auto simp: q(3) Qs'_def collapse_Qn_Qs_set_conv)
ultimately have "f' (map the (filter (λq. ¬ Option.is_none q) qs')) → q' |∈| rules (collapse_automaton A)"
using q(1, 4) unfolding collapse_automaton_def Qn'_def[symmetric] Qs'_def[symmetric]
by (fastforce simp: qs'_def q(3) intro: exI[of _ qs] exI[of _ qs'] split: if_splits)
moreover have ***: "length (filter (λi.¬ Option.is_none (gcollapse (ts ! i))) [0..<length ts]) =
length (filter (λt. ¬ Option.is_none (gcollapse t)) ts)" for ts
by (subst length_map[of "(!) ts", symmetric] filter_map[unfolded comp_def, symmetric] map_nth)+
(rule refl)
note this[of ts]
moreover have "the (filter (λq. ¬ Option.is_none q) qs' ! i) |∈| ta_der (collapse_automaton A)
(term_of_gterm (the (filter (λt. ¬ Option.is_none t) (map gcollapse ts) ! i)))"
if "i < length [x←ts . ¬ Option.is_none (gcollapse x)]" for i
unfolding qs'_def using that q(3) GFun(1)[OF nth_mem q(4)]
proof (induct ts arbitrary: qs rule: List.rev_induct)
case (snoc t ts)
have x1 [simp]: "i < length xs ⟹ (xs @ ys) ! i = xs ! i" for xs ys i by (auto simp: nth_append)
have x2: "i = length xs ⟹ (xs @ ys) ! i = ys ! 0" for xs ys i by (auto simp: nth_append)
obtain q qs' where qs [simp]: "qs = qs' @ [q]" using snoc(3) by (cases "rev qs") auto
have [simp]:
"map (λx. if Option.is_none (gcollapse ((ts @ [t]) ! x)) then None else Some ((qs' @ [q]) ! x)) [0..<length ts] =
map (λx. if Option.is_none (gcollapse (ts ! x)) then None else Some (qs' ! x)) [0..<length ts]"
using snoc(3) by auto
show ?case
proof (cases "Option.is_none (gcollapse t)")
case True then show ?thesis using snoc(1)[of qs'] snoc(2,3)
snoc(4)[unfolded length_append list.size add_0 add_0_right add_Suc_right, OF less_SucI]
by (auto cong: if_cong)
next
case False note False' = this
show ?thesis
proof (cases "i = length [x←ts . ¬ Option.is_none (gcollapse x)]")
case True
then show ?thesis using snoc(3) snoc(4)[of "length ts"]
unfolding qs length_append list.size add_0 add_0_right add_Suc_right
upt_Suc_append[OF zero_le] filter_append map_append
by (subst (5 6) x2) (auto simp: comp_def *** False' Option.is_none_def[symmetric])
next
case False
then show ?thesis using snoc(1)[of qs'] snoc(2,3)
snoc(4)[unfolded length_append list.size add_0 add_0_right add_Suc_right, OF less_SucI]
unfolding qs length_append list.size add_0 add_0_right add_Suc_right
upt_Suc_append[OF zero_le] filter_append map_append
by (subst (5 6) x1) (auto simp: comp_def *** False')
qed
qed
qed auto
ultimately show ?case using q(2) by (auto simp: qs'_def comp_def q(3)
intro!: exI[of _ q'] exI[of _ "map the (filter (λq. ¬ Option.is_none q) qs')"])
qed
then have "the (gcollapse t) ∈ gta_lang Q (collapse_automaton A)"
by (metis q(1) gta_langI)
} ultimately show ?thesis by blast
qed
lemma ℒ_collapse_automaton':
assumes "𝒬⇩r A |⊆| ta_reachable (ta A)"
shows "ℒ (collapse_automaton_reg A) = the ` (gcollapse ` ℒ A - {None})"
using assms by (auto simp: collapse_automaton_reg_def ℒ_def collapse_automaton')
lemma collapse_automaton:
assumes "𝒬⇩r A |⊆| ta_reachable (ta A)" "RR1_spec A T"
shows "RR1_spec (collapse_automaton_reg A) (the ` (gcollapse ` ℒ A - {None}))"
using collapse_automaton'[OF assms(1)] assms(2)
by (simp add: collapse_automaton_reg_def ℒ_def RR1_spec_def)
subsection ‹Cylindrification›
definition pad_with_Nones where
"pad_with_Nones n m = (λ(f, g). case_option (replicate n None) id f @ case_option (replicate m None) id g)"
lemma gencode_append:
"gencode (ss @ ts) = map_gterm (pad_with_Nones (length ss) (length ts)) (gpair (gencode ss) (gencode ts))"
proof -
have [simp]: "p ∉ gposs (gunions (map gdomain ts)) ⟹ map (λt. gfun_at t p) ts = replicate (length ts) None"
for p ts by (intro nth_equalityI)
(fastforce simp: poss_gposs_mem_conv fun_at_def' image_def all_set_conv_all_nth)+
note [simp] = glabel_map_gterm_conv[of "λ(_ :: unit option). ()", unfolded comp_def gdomain_id]
show ?thesis by (auto intro!: arg_cong[of _ _ "λx. glabel x _"] simp del: gposs_gunions
simp: pad_with_Nones_def gencode_def gunions_append gpair_def map_gterm_glabel comp_def)
qed
lemma append_automaton:
assumes "RRn_spec n A T" "RRn_spec m B U"
shows "RRn_spec (n + m) (fmap_funs_reg (pad_with_Nones n m) (pair_automaton_reg A B)) {ts @ us |ts us. ts ∈ T ∧ us ∈ U}"
using assms pair_automaton[of A "gencode ` T" B "gencode ` U"]
unfolding RRn_spec_def
proof (intro conjI set_eqI iffI, goal_cases)
case (1 s)
then obtain ts us where "ts ∈ T" "us ∈ U" "s = gencode (ts @ us)"
by (fastforce simp: ℒ_def fmap_funs_reg_def RR1_spec_def RR2_spec_def gencode_append fmap_funs_gta_lang)
then show ?case by blast
qed (fastforce simp: RR1_spec_def RR2_spec_def fmap_funs_reg_def ℒ_def gencode_append fmap_funs_gta_lang)+
lemma cons_automaton:
assumes "RR1_spec A T" "RRn_spec m B U"
shows "RRn_spec (Suc m) (fmap_funs_reg (λ(f, g). pad_with_Nones 1 m (map_option (λf. [Some f]) f, g))
(pair_automaton_reg A B)) {t # us |t us. t ∈ T ∧ us ∈ U}"
proof -
have [simp]: "{ts @ us |ts us. ts ∈ (λt. [t]) ` T ∧ us ∈ U} = {t # us |t us. t ∈ T ∧ us ∈ U}"
by (auto intro: exI[of _ "[_]", OF exI])
show ?thesis using append_automaton[OF RR1_to_RRn_spec, OF assms]
by (auto simp: ℒ_def fmap_funs_reg_def pair_automaton_reg_def comp_def
fmap_funs_gta_lang map_pair_automaton_12 fmap_funs_ta_comp prod.case_distrib
gencode_append[of "[_]", unfolded gencode_singleton List.append.simps])
qed
subsection ‹Projection›
abbreviation "drop_none_rule m fs ≡ if list_all (Option.is_none) (drop m fs) then None else Some (drop m fs)"
lemma drop_automaton_reg:
assumes "𝒬⇩r A |⊆| ta_reachable (ta A)" "m < n" "RRn_spec n A T"
defines "f ≡ λfs. drop_none_rule m fs"
shows "RRn_spec (n - m) (collapse_automaton_reg (fmap_funs_reg f A)) (drop m ` T)"
proof -
have [simp]: "length ts = n - m ==> p ∈ gposs (gencode ts) ⟹ ∃f. ∃t∈set ts. Some f = gfun_at t p" for p ts
proof (cases p, goal_cases Empty PCons)
case Empty
obtain t where "t ∈ set ts" using assms(2) Empty(1) by (cases ts) auto
moreover then obtain f where "Some f = gfun_at t p" using Empty(3) by (cases t rule: gterm.exhaust) auto
ultimately show ?thesis by auto
next
case (PCons i p')
then have "p ≠ []" by auto
then show ?thesis using PCons(2)
by (auto 0 3 simp: gencode_def eq_commute[of "gfun_at _ _" "Some _"] elim!: gfun_at_possE)
qed
{ fix p ts y assume that: "gfun_at (gencode ts) p = Some y"
have "p ∈ gposs (gencode ts) ⟹ gfun_at (gencode ts) p = Some (map (λt. gfun_at t p) ts)"
by (auto simp: gencode_def)
moreover have "gfun_at (gencode ts) p = Some y ⟹ p ∈ gposs (gencode ts)"
using gfun_at_nongposs by force
ultimately have "y = map (λt. gfun_at t p) ts ∧ p ∈ gposs (gencode ts)" by (simp add: that)
} note [dest!] = this
have [simp]: "list_all f (replicate n x) ⟷ n = 0 ∨ f x" for f n x by (induct n) auto
have [dest]: "x ∈ set xs ⟹ list_all f xs ⟹ f x" for f x xs by (induct xs) auto
have *: "f (pad_with_Nones m' n' z) = snd z"
if "fst z = None ∨ fst z ≠ None ∧ length (the (fst z)) = m"
"snd z = None ∨ snd z ≠ None ∧ length (the (snd z)) = n - m ∧ (∃y. Some y ∈ set (the (snd z)))"
"m' = m" "n' = n - m" for z m' n'
using that by (auto simp: f_def pad_with_Nones_def split: option.splits prod.splits)
{ fix ts assume ts: "ts ∈ T" "length ts = n"
have "gencode (drop m ts) = the (gcollapse (map_gterm f (gencode ts)))"
"gcollapse (map_gterm f (gencode ts)) ≠ None"
proof (goal_cases)
case 1 show ?case
using ts assms(2)
apply (subst gsnd_gpair[of "gencode (take m ts)", symmetric])
apply (subst gencode_append[of "take m ts" "drop m ts", unfolded append_take_drop_id])
unfolding gsnd_def comp_def gterm.map_comp
apply (intro arg_cong[where f = "λx. the (gcollapse x)"] gterm.map_cong refl)
by (subst *) (auto simp: gpair_def set_gterm_gposs_conv image_def)
next
case 2
have [simp]: "gcollapse t = None ⟷ gfun_at t [] = Some None" for t
by (cases t rule: gcollapse.cases) auto
obtain t where "t ∈ set (drop m ts)" using ts(2) assms(2) by (cases "drop m ts") auto
moreover then have "¬ Option.is_none (gfun_at t [])" by (cases t rule: gterm.exhaust) auto
ultimately show ?case
by (auto simp: f_def gencode_def list_all_def drop_map)
qed
}
then show ?thesis using assms(3)
by (fastforce simp: ℒ_def collapse_automaton_reg_def fmap_funs_reg_def
RRn_spec_def fmap_funs_gta_lang gsnd_def gpair_def gterm.map_comp comp_def
glabel_map_gterm_conv[unfolded comp_def] assms(1) collapse_automaton')
qed
lemma gfst_collapse_simp:
"the (gcollapse (map_gterm fst t)) = gfst t"
by (simp add: gfst_def)
lemma gsnd_collapse_simp:
"the (gcollapse (map_gterm snd t)) = gsnd t"
by (simp add: gsnd_def)
definition proj_1_reg where
"proj_1_reg A = collapse_automaton_reg (fmap_funs_reg fst (trim_reg A))"
definition proj_2_reg where
"proj_2_reg A = collapse_automaton_reg (fmap_funs_reg snd (trim_reg A))"
lemmas proj_1_reg_simp = proj_1_reg_def collapse_automaton_reg_def fmap_funs_reg_def trim_reg_def
lemmas proj_2_reg_simp = proj_2_reg_def collapse_automaton_reg_def fmap_funs_reg_def trim_reg_def
lemma ℒ_proj_1_reg_collapse:
"ℒ (proj_1_reg 𝒜) = the ` (gcollapse ` map_gterm fst ` (ℒ 𝒜) - {None})"
proof -
have "𝒬⇩r (fmap_funs_reg fst (trim_reg 𝒜)) |⊆| ta_reachable (ta (fmap_funs_reg fst (trim_reg 𝒜)))"
by (auto simp: fmap_funs_reg_def)
note [simp] = ℒ_collapse_automaton'[OF this]
show ?thesis by (auto simp: proj_1_reg_def fmap_funs_ℒ ℒ_trim)
qed
lemma ℒ_proj_2_reg_collapse:
"ℒ (proj_2_reg 𝒜) = the ` (gcollapse ` map_gterm snd ` (ℒ 𝒜) - {None})"
proof -
have "𝒬⇩r (fmap_funs_reg snd (trim_reg 𝒜)) |⊆| ta_reachable (ta (fmap_funs_reg snd (trim_reg 𝒜)))"
by (auto simp: fmap_funs_reg_def)
note [simp] = ℒ_collapse_automaton'[OF this]
show ?thesis by (auto simp: proj_2_reg_def fmap_funs_ℒ ℒ_trim)
qed
lemma proj_1:
assumes "RR2_spec A R"
shows "RR1_spec (proj_1_reg A) (fst ` R)"
proof -
{fix s t assume ass: "(s, t) ∈ R"
from ass have s: "s = the (gcollapse (map_gterm fst (gpair s t)))"
by (auto simp: gfst_gpair gfst_collapse_simp)
then have "Some s = gcollapse (map_gterm fst (gpair s t))"
by (cases s; cases t) (auto simp: gpair_def)
then have "s ∈ ℒ (proj_1_reg A)" using assms ass s
by (auto simp: proj_1_reg_simp ℒ_def trim_ta_reach trim_gta_lang
image_def image_Collect RR2_spec_def fmap_funs_gta_lang
collapse_automaton'[of "fmap_funs_ta fst (trim_ta (fin A) (ta A))"])
force}
moreover
{fix s assume "s ∈ ℒ (proj_1_reg A)" then have "s ∈ fst ` R" using assms
by (auto simp: gfst_collapse_simp gfst_gpair rev_image_eqI RR2_spec_def trim_ta_reach trim_gta_lang
ℒ_def proj_1_reg_simp fmap_funs_gta_lang collapse_automaton'[of "fmap_funs_ta fst (trim_ta (fin A) (ta A))"])}
ultimately show ?thesis using assms unfolding RR2_spec_def RR1_spec_def ℒ_def proj_1_reg_simp
by auto
qed
lemma proj_2:
assumes "RR2_spec A R"
shows "RR1_spec (proj_2_reg A) (snd ` R)"
proof -
{fix s t assume ass: "(s, t) ∈ R"
then have s: "t = the (gcollapse (map_gterm snd (gpair s t)))"
by (auto simp: gsnd_gpair gsnd_collapse_simp)
then have "Some t = gcollapse (map_gterm snd (gpair s t))"
by (cases s; cases t) (auto simp: gpair_def)
then have "t ∈ ℒ (proj_2_reg A)" using assms ass s
by (auto simp: ℒ_def trim_ta_reach trim_gta_lang proj_2_reg_simp
image_def image_Collect RR2_spec_def fmap_funs_gta_lang
collapse_automaton'[of "fmap_funs_ta snd (trim_ta (fin A) (ta A))"])
fastforce}
moreover
{fix s assume "s ∈ ℒ (proj_2_reg A)" then have "s ∈ snd ` R" using assms
by (auto simp: ℒ_def gsnd_collapse_simp gsnd_gpair rev_image_eqI RR2_spec_def
trim_ta_reach trim_gta_lang proj_2_reg_simp
fmap_funs_gta_lang collapse_automaton'[of "fmap_funs_ta snd (trim_ta (fin A) (ta A))"])}
ultimately show ?thesis using assms unfolding RR2_spec_def RR1_spec_def
by auto
qed
lemma ℒ_proj:
assumes "RR2_spec A R"
shows "ℒ (proj_1_reg A) = gfst ` ℒ A" "ℒ (proj_2_reg A) = gsnd ` ℒ A"
proof -
have [simp]: "gfst ` {gpair t u |t u. (t, u) ∈ R} = fst ` R"
by (force simp: gfst_gpair image_def)
have [simp]: "gsnd ` {gpair t u |t u. (t, u) ∈ R} = snd ` R"
by (force simp: gsnd_gpair image_def)
show "ℒ (proj_1_reg A) = gfst ` ℒ A" "ℒ (proj_2_reg A) = gsnd ` ℒ A"
using proj_1[OF assms] proj_2[OF assms] assms gfst_gpair gsnd_gpair
by (auto simp: RR1_spec_def RR2_spec_def)
qed
lemmas proj_automaton_gta_lang = proj_1 proj_2
subsection ‹Permutation›
lemma gencode_permute:
assumes "set ps = {0..<length ts}"
shows "gencode (map ((!) ts) ps) = map_gterm (λxs. map ((!) xs) ps) (gencode ts)"
proof -
have *: "(!) ts ` set ps = set ts" using assms by (auto simp: image_def set_conv_nth)
show ?thesis using subsetD[OF equalityD1[OF assms]]
apply (intro eq_gterm_by_gposs_gfun_at)
unfolding gencode_def gposs_glabel gposs_map_gterm gposs_gunions gfun_at_map_gterm gfun_at_glabel
set_map * by auto
qed
lemma permute_automaton:
assumes "RRn_spec n A T" "set ps = {0..<n}"
shows "RRn_spec (length ps) (fmap_funs_reg (λxs. map ((!) xs) ps) A) ((λxs. map ((!) xs) ps) ` T)"
using assms by (auto simp: RRn_spec_def gencode_permute fmap_funs_reg_def ℒ_def fmap_funs_gta_lang image_def)
subsection ‹Intersection›
lemma intersect_automaton:
assumes "RRn_spec n A T" "RRn_spec n B U"
shows "RRn_spec n (reg_intersect A B) (T ∩ U)" using assms
by (simp add: RRn_spec_def ℒ_intersect)
(metis gdecode_gencode image_Int inj_on_def)
lemma union_automaton:
assumes "RRn_spec n A T" "RRn_spec n B U"
shows "RRn_spec n (reg_union A B) (T ∪ U)"
using assms by (auto simp: RRn_spec_def ℒ_union)
subsection ‹Difference›
lemma RR1_difference:
assumes "RR1_spec A T" "RR1_spec B U"
shows "RR1_spec (difference_reg A B) (T - U)"
using assms by (auto simp: RR1_spec_def ℒ_difference_reg)
lemma RR2_difference:
assumes "RR2_spec A T" "RR2_spec B U"
shows "RR2_spec (difference_reg A B) (T - U)"
using assms by (auto simp: RR2_spec_def ℒ_difference_reg)
lemma RRn_difference:
assumes "RRn_spec n A T" "RRn_spec n B U"
shows "RRn_spec n (difference_reg A B) (T - U)"
using assms by (auto simp: RRn_spec_def ℒ_difference_reg) (metis gdecode_gencode)+
subsection ‹All terms over a signature›
definition term_automaton :: "('f × nat) fset ⇒ (unit, 'f) ta" where
"term_automaton ℱ = TA ((λ (f, n). TA_rule f (replicate n ()) ()) |`| ℱ) {||}"
definition term_reg where
"term_reg ℱ = Reg {|()|} (term_automaton ℱ)"
lemma term_automaton:
"RR1_spec (term_reg ℱ) (𝒯⇩G (fset ℱ))"
unfolding RR1_spec_def gta_lang_def term_reg_def ℒ_def
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr t)
then have "() |∈| ta_der (term_automaton ℱ) (term_of_gterm t)"
by (auto simp: gta_der_def)
then show ?case
by (induct t) (auto simp: term_automaton_def split: if_splits)
next
case (rl t)
then have "() |∈| ta_der (term_automaton ℱ) (term_of_gterm t)"
proof (induct t rule: 𝒯⇩G.induct)
case (const a) then show ?case
by (auto simp: term_automaton_def image_iff intro: bexI[of _ "(a, 0)"])
next
case (ind f n ss) then show ?case
by (auto simp: term_automaton_def image_iff intro: bexI[of _ "(f, n)"])
qed
then show ?case
by (auto simp: gta_der_def)
qed
fun true_RRn :: "('f × nat) fset ⇒ nat ⇒ (nat, 'f option list) reg" where
"true_RRn ℱ 0 = Reg {|0|} (TA {|TA_rule [] [] 0|} {||})"
| "true_RRn ℱ (Suc 0) = relabel_reg (fmap_funs_reg (λf. [Some f]) (term_reg ℱ))"
| "true_RRn ℱ (Suc n) = relabel_reg
(trim_reg (fmap_funs_reg (pad_with_Nones 1 n) (pair_automaton_reg (true_RRn ℱ 1) (true_RRn ℱ n))))"
lemma true_RRn_spec:
"RRn_spec n (true_RRn ℱ n) {ts. length ts = n ∧ set ts ⊆ 𝒯⇩G (fset ℱ)}"
proof (induct ℱ n rule: true_RRn.induct)
case (1 ℱ) show ?case
by (simp cong: conj_cong add: true_RR0_spec)
next
case (2 ℱ)
moreover have "{ts. length ts = 1 ∧ set ts ⊆ 𝒯⇩G (fset ℱ)} = (λt. [t]) ` 𝒯⇩G (fset ℱ)"
apply (intro equalityI subsetI)
subgoal for ts by (cases ts) auto
by auto
ultimately show ?case
using RR1_to_RRn_spec[OF term_automaton, of ℱ] by auto
next
case (3 ℱ n)
have [simp]: "{ts @ us |ts us. length ts = n ∧ set ts ⊆ 𝒯⇩G (fset ℱ) ∧ length us = m ∧
set us ⊆ 𝒯⇩G (fset ℱ)} = {ss. length ss = n + m ∧ set ss ⊆ 𝒯⇩G (fset ℱ)}" for n m
by (auto 0 4 intro!: exI[of _ "take n _", OF exI[of _ "drop n _"], of _ xs xs for xs]
dest!: subsetD[OF set_take_subset] subsetD[OF set_drop_subset])
show ?case using append_automaton[OF 3]
by simp
qed
subsection ‹RR2 composition›
abbreviation "RR2_to_RRn A ≡ fmap_funs_reg (λ(f, g). [f, g]) A"
abbreviation "RRn_to_RR2 A ≡ fmap_funs_reg (λf. (f ! 0, f ! 1)) A"
definition rr2_compositon where
"rr2_compositon ℱ A B =
(let A' = RR2_to_RRn A in
let B' = RR2_to_RRn B in
let F = true_RRn ℱ 1 in
let CA = trim_reg (fmap_funs_reg (pad_with_Nones 2 1) (pair_automaton_reg A' F)) in
let CB = trim_reg (fmap_funs_reg (pad_with_Nones 1 2) (pair_automaton_reg F B')) in
let PI = trim_reg (fmap_funs_reg (λxs. map ((!) xs) [1, 0, 2]) (reg_intersect CA CB)) in
RRn_to_RR2 (collapse_automaton_reg (fmap_funs_reg (drop_none_rule 1) PI))
)"
lemma list_length1E:
assumes "length xs = Suc 0" obtains x where "xs = [x]" using assms
by (cases xs) auto
lemma rr2_compositon:
assumes "ℛ ⊆ 𝒯⇩G (fset ℱ) × 𝒯⇩G (fset ℱ)" "𝔏 ⊆ 𝒯⇩G (fset ℱ) × 𝒯⇩G (fset ℱ)"
and "RR2_spec A ℛ" and "RR2_spec B 𝔏"
shows "RR2_spec (rr2_compositon ℱ A B) (ℛ O 𝔏)"
proof -
let ?R = "(λ(t, u). [t, u]) ` ℛ" let ?L = "(λ(t, u). [t, u]) ` 𝔏"
let ?A = "RR2_to_RRn A" let ?B = "RR2_to_RRn B" let ?F = "true_RRn ℱ 1"
let ?CA = "trim_reg (fmap_funs_reg (pad_with_Nones 2 1) (pair_automaton_reg ?A ?F))"
let ?CB = "trim_reg (fmap_funs_reg (pad_with_Nones 1 2) (pair_automaton_reg ?F ?B))"
let ?PI = "trim_reg (fmap_funs_reg (λxs. map ((!) xs) [1, 0, 2]) (reg_intersect ?CA ?CB))"
let ?DR = "collapse_automaton_reg (fmap_funs_reg (drop_none_rule 1) ?PI)"
let ?Rs = "{ts @ us | ts us. ts ∈ ?R ∧ (∃t. us = [t] ∧ t ∈ 𝒯⇩G (fset ℱ))}"
let ?Ls = "{us @ ts | ts us. ts ∈ ?L ∧ (∃t. us = [t] ∧ t ∈ 𝒯⇩G (fset ℱ))}"
from RR2_to_RRn_spec assms(3, 4)
have rr2: "RRn_spec 2 ?A ?R" "RRn_spec 2 ?B ?L" by auto
have *: "{ts. length ts = 1 ∧ set ts ⊆ 𝒯⇩G (fset ℱ)} = {[t] | t. t ∈ 𝒯⇩G (fset ℱ)}"
by (auto elim!: list_length1E)
have F: "RRn_spec 1 ?F {[t] | t. t ∈ 𝒯⇩G (fset ℱ)}" using true_RRn_spec[of 1 ℱ] unfolding * .
have "RRn_spec 3 ?CA ?Rs" "RRn_spec 3 ?CB ?Ls"
using append_automaton[OF rr2(1) F] append_automaton[OF F rr2(2)]
by (auto simp: numeral_3_eq_3) (smt Collect_cong)
from permute_automaton[OF intersect_automaton[OF this], of "[1, 0, 2]"]
have "RRn_spec 3 ?PI ((λxs. map ((!) xs) [1, 0, 2]) ` (?Rs ∩ ?Ls))"
by (auto simp: atLeast0_lessThan_Suc insert_commute numeral_2_eq_2 numeral_3_eq_3)
from drop_automaton_reg[OF _ _ this, of 1]
have sp: "RRn_spec 2 ?DR (drop 1 ` (λxs. map ((!) xs) [1, 0, 2]) ` (?Rs ∩ ?Ls))"
by auto
{fix s assume "s ∈ (λ(t, u). [t, u]) ` (ℛ O 𝔏)"
then obtain t u v where comp: "s = [t, u]" "(t, v) ∈ ℛ" "(v, u) ∈ 𝔏"
by (auto simp: image_iff relcomp_unfold split!: prod.split)
then have "[t, v] ∈ ?R" "[v , u] ∈ ?L" "u ∈ 𝒯⇩G (fset ℱ)" "v ∈ 𝒯⇩G (fset ℱ)" "t ∈ 𝒯⇩G (fset ℱ)" using assms(1, 2)
by (auto simp: image_iff relcomp_unfold split!: prod.splits)
then have "[t, v, u] ∈ ?Rs" "[t, v, u] ∈ ?Ls"
apply (simp_all)
subgoal
apply (rule exI[of _ "[t, v]"], rule exI[of _ "[u]"])
apply simp
done
subgoal
apply (rule exI[of _ "[v, u]"], rule exI[of _ "[t]"])
apply simp
done
done
then have "s ∈ drop 1 ` (λxs. map ((!) xs) [1, 0, 2]) ` (?Rs ∩ ?Ls)" unfolding comp(1)
apply (simp add: image_def Bex_def)
apply (rule exI[of _ "[v, t, u]"]) apply simp
apply (rule exI[of _ "[t, v, u]"]) apply simp
done}
moreover have "drop 1 ` (λxs. map ((!) xs) [1, 0, 2]) ` (?Rs ∩ ?Ls) ⊆ (λ(t, u). [t, u]) ` (ℛ O 𝔏)"
by (auto simp: image_iff relcomp_unfold Bex_def split!: prod.splits)
ultimately have *: "drop 1 ` (λxs. map ((!) xs) [1, 0, 2]) ` (?Rs ∩ ?Ls) = (λ(t, u). [t, u]) ` (ℛ O 𝔏)"
by (simp add: subsetI subset_antisym)
have **: "(λf. (f ! 0, f ! 1)) ` (λ(t, u). [t, u]) ` (ℛ O 𝔏) = ℛ O 𝔏"
by (force simp: image_def relcomp_unfold split!: prod.splits)
show ?thesis using sp unfolding *
using RRn_to_RR2_spec[where ?T = "(λ(t, u). [t, u]) ` (ℛ O 𝔏)" and ?A = ?DR]
unfolding ** by (auto simp: rr2_compositon_def Let_def image_iff)
qed
end