theory RRn_Automata
imports Tree_Automata_Utils
begin
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))))"
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}"
by (auto simp: gpair_def elim: gfun_at_possE) (auto simp: fun_at_def' split: if_splits)
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)
lemma gpair_mctxt:
assumes "∀ i < length ss. gpair (ss ! i) (ts ! i) = us ! i"
and "length ss = length ts" "length ts = length us" "length us = num_holes C"
and "ground_mctxt C"
shows "gterm_of_term (fill_holes (map_mctxt (λf . (Some f, Some f)) C) (map term_of_gterm us)) =
gpair (gterm_of_term (fill_holes C (map term_of_gterm ss))) (gterm_of_term (fill_holes C (map term_of_gterm ts)))"
using assms
proof (induct C arbitrary: ss ts us)
case (MFun f zs)
show ?case using MFun(2-)
using MFun(1)[OF nth_mem, of i "partition_holes ss zs ! i" "partition_holes ts zs ! i" "partition_holes us zs ! i" for i]
using length_partition_holes_nth[of zs] partition_by_nth_nth[of "map num_holes zs" us]
using partition_by_nth_nth[of "map num_holes zs" ss] partition_by_nth_nth[of "map num_holes zs" ts]
by (auto simp add: gpair_context1 comp_def intro!: nth_equalityI)
qed (auto simp add: fill_holes_MHole)
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 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 gpair_poss_args_poss [simp]:
shows "p ∈ gposs (gpair s t) ⟷ p ∈ gposs s ∨ p ∈ gposs t"
by (auto simp: gpair_def)
lemma gpair_poss_args_poss2 [simp]:
shows "gposs (gpair s t) = gposs s ∪ gposs t"
by (auto simp: gpair_def)
lemma lhs_poss_to_gpair_poss:
assumes "p ∈ gposs s"
shows "p ∈ gposs (gpair s t)"
using assms by (auto simp: gpair_def)
lemma rhs_poss_to_gpair_poss:
assumes "p ∈ gposs t"
shows "p ∈ gposs (gpair s t)"
using assms by (auto simp: gpair_def)
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: gpair_def gunion_gsubt_at_poss intro!: eq_gterm_by_gposs_gfun_at)
(metis gfun_at_gsub_at gfun_at_nongposs gpos_append_gposs)+
lemma subst_at_gpair_nt_poss_Some_None [simp]:
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 by (auto simp: gpair_def intro!: eq_gterm_by_gposs_gfun_at)
(metis gfun_at_possE map_option_eq_Some pos_append_poss)
lemma subst_at_gpair_nt_poss_None_Some [simp]:
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 by (auto simp: gpair_def intro!: eq_gterm_by_gposs_gfun_at)
(metis gfun_at_possE map_option_eq_Some pos_append_poss)
lemma groot_gpair [simp]:
"groot (gpair s t) = (Some (groot s), Some (groot t))"
by (cases s; cases t) (auto simp add: gpair_code)
fun poss_ctxt where
"poss_ctxt □ = {[]}"
| "poss_ctxt (More f ss C ts) = {[]} ∪ {i # p| i p. i < length ss ∧ p ∈ poss (ss ! i)} ∪
(#) (length ss) ` (poss_ctxt C) ∪ {(length ss + (Suc i)) # p| i p. i < length ts ∧ p ∈ poss (ts ! i)}"
lemma ctxt_poss [simp]:
"poss C⟨u⟩ = poss_ctxt C ∪ (λ ps. hole_pos C @ ps) ` poss u"
proof (induct C)
case (More f ss C ts)
{fix i p assume ass: "i # p ∈ poss (More f ss C ts)⟨u⟩"
then have "i # p ∈ poss_ctxt (More f ss C ts) ∪ (@) (hole_pos (More f ss C ts)) ` poss u" using More(1)
by (cases "i < length ss"; cases "i = length ss") (auto simp add: nth_append_Cons)}
then show ?case using More
by (auto simp add: append_Cons_nth_left) (blast, blast, metis add_Suc_right nth_Cons_Suc nth_append_length_plus)
qed auto
lemma [simp]:
assumes "ground t"
shows "gposs (gterm_of_term t) = poss t"
by (metis assms gterm_of_term_inv poss_gposs_conv)
lemma [simp]:
assumes "p ∈ gposs t"
shows "ground_ctxt (ctxt_of_pos_term p (term_of_gterm t))"
using assms by (induct t arbitrary: p) (auto dest!: in_set_takeD in_set_dropD)
lemma [simp]:
assumes "p ∉ gposs s" and "p ∈ poss_ctxt C"
and "poss_ctxt C ∪ u = gposs s ∪ gposs t"
shows "p ∈ gposs t" using assms by auto
lemma poss_ctxt_of_ctxt_of_poss:
assumes "p ∈ poss t"
shows "poss_ctxt (ctxt_of_pos_term p t) = {q | q. q ∈ poss t ∧ ¬ p <⇩p q}"
using assms
proof (induct p arbitrary: t)
case (Cons a p)
then obtain f ts where t[simp]: "t = Fun f ts" and b_a: "a < length ts" and
ctxt: "ctxt_of_pos_term (a # p) t = More f (take a ts) (ctxt_of_pos_term p (ts ! a)) (drop (Suc a) ts)"
by (cases t) auto
have *:"{q | q. q ∈ poss t ∧ ¬ a # p <⇩p q} = {[]} ∪ {i # p | i p. i < a ∧ p ∈ poss (ts ! i)} ∪
{a # q | q. q ∈ poss (ts ! a) ∧ ¬ p <⇩p q} ∪ {(a + Suc i) # p | i p. i < length (drop (Suc a) ts) ∧ p ∈ poss (ts ! (a + (Suc i)))}"
using b_a by auto (smt add_Suc diff_add_inverse less_iff_Suc_add linorder_neqE_nat nat_add_left_cancel_less)
have "{i # p | i p. i < a ∧ p ∈ poss (ts ! i)} = {i # p| i p. i < a∧ p ∈ poss ((take a ts) ! i)}"
using ctxt by auto
moreover have "{(a + Suc i) # p | i p. i < length (drop (Suc a) ts) ∧ p ∈ poss (ts ! (a + (Suc i)))} =
{(a + Suc i) # p | i p. i < length (drop (Suc a) ts) ∧ p ∈ poss (ts ! (a + Suc i))}"
using ctxt by auto
moreover have "{a # q | q. q ∈ poss (ts ! a) ∧ ¬ p <⇩p q} = (#) a ` (poss_ctxt (ctxt_of_pos_term p (ts ! a)))"
using ctxt Cons(2) Cons(1)[of "ts ! a"] by (auto simp del: ctxt_of_pos_term.simps)
ultimately show ?case using b_a unfolding *[unfolded t] t ctxt_of_pos_term.simps poss_ctxt.simps
by auto
qed (auto simp add: less_pos_def)
lemma poss_ctxt_not_hole_smaller_or_parallel:
assumes "p ∈ poss_ctxt C" and "p ≠ hole_pos C"
shows "p <⇩p hole_pos C ∨ p ⊥ hole_pos C"
using assms by (induct p arbitrary: C, auto simp add: less_pos_def)
(metis (no_types, lifting) ctxt_of_pos_term_hole_pos hole_pos_poss mem_Collect_eq order_pos.order.not_eq_order_implies_strict parallel_pos poss_ctxt_of_ctxt_of_poss)
lemma poss_domains_ctxt:
assumes "p ∉ gposs s" and "p ∈ gposs t" and "hole_pos C = p"
and "gposs (gctxt_apply C u) = gposs s ∪ gposs t" and "ground_ctxt C"
shows "gposs (gctxt_apply C (gterm_to_None_Some v)) = gposs s ∪ gposs (gctxt_apply (ctxt_of_pos_term p (term_of_gterm t)) v)"
using assms by (auto simp: poss_ctxt_of_ctxt_of_poss)
(metis order_pos.less_imp_le order_pos.less_imp_not_less parallel_pos poss_ctxt_not_hole_smaller_or_parallel)
lemma poss_ctxt_not_hole_rpes_fun_at:
assumes "p ∈ poss_ctxt C" and "p ≠ hole_pos C"
shows "fun_at C⟨t⟩ p = fun_at C⟨u⟩ p"
using assms by (induct C arbitrary: p) (auto simp add: nth_append_Cons, blast)
lemma gsubt_at_ctxt_pos [simp]:
"gsubt_at (gterm_of_term C⟨term_of_gterm t⟩) (hole_pos C) = t"
by (induct C arbitrary: t) (auto simp: comp_def nth_append_Cons)
lemma gfun_at_ctxt_pos [simp]:
"gfun_at (gterm_of_term C⟨term_of_gterm t⟩) (hole_pos C) = gfun_at t []"
by (induct C arbitrary: t) (auto simp: comp_def nth_append_Cons)
lemma fun_at_ctxt_hole_pos [simp]:
shows "fun_at C⟨v⟩ (hole_pos C) = fun_at v []"
by (induct C) auto
lemma fun_at_gfun_at_conv:
assumes "p ∈ gposs t"
shows "fun_at (term_of_gterm t) p = gfun_at t p"
using assms by (induct t arbitrary: p) auto
lemma gfun_at_gpair_nt_poss [simp]:
assumes "p ∉ gposs s" and "p ∉ gposs t"
shows "gfun_at (gpair s t) p = None"
using assms by (auto simp: gpair_def)
lemma gfun_at_gpair_Some [simp]:
assumes "p ∈ gposs s ∨ p ∈ gposs t"
shows "gfun_at (gpair s t) p = Some (gfun_at s p, gfun_at t p)"
using assms by (cases "p ∈ gposs s"; cases "p ∈ gposs t") (auto simp add: gpair_def gfun_at_poss)
lemma fst_groot_None_not_poss:
assumes "p ∈ gposs s ∪ gposs t"
and "fst (the (gfun_at (gpair s t) p)) = None"
shows "p ∉ gposs s"
using assms gfun_at_poss by fastforce
lemma gpair_ctxt_decomposition:
assumes "p ∉ gposs s" and "hole_pos C = p"
and "gpair s t = gctxt_apply C (gterm_to_None_Some u)" and "ground_ctxt C"
shows "gpair s (gctxt_apply (ctxt_of_pos_term p (term_of_gterm t)) v) = gctxt_apply C (gterm_to_None_Some v)"
proof -
let ?t_of_g = "λ t. term_of_gterm t :: ('a, unit) term"
from assms(3) have sub: "gposs s ∪ gposs t = gposs (gctxt_apply C (gterm_to_None_Some u))"
by (metis gpair_poss_args_poss2)
have pos_C: "poss_ctxt C ⊆ gposs (gctxt_apply C (gterm_to_None_Some u))"
using assms(4) by auto
from sub assms(1, 2) have pos_t: "p ∈ gposs t"
by (metis UnE assms(4) ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv hole_pos_poss)
from poss_domains_ctxt[OF assms(1) pos_t assms(2) _ assms(4)]
have poss_eq: "gposs (gpair s (gctxt_apply (ctxt_of_pos_term p (?t_of_g t)) v)) = gposs (gctxt_apply C (gterm_to_None_Some v))"
by (metis assms(3) gpair_poss_args_poss2)
{fix q assume q: "q ∈ poss_ctxt C"
have "gfun_at (gpair s (gctxt_apply (ctxt_of_pos_term p (?t_of_g t)) v)) q = gfun_at (gctxt_apply C (gterm_to_None_Some v)) q"
proof (cases "q = hole_pos C")
case True
then show ?thesis using assms(1, 2, 4) pos_t
by auto (metis empty_pos_in_poss fun_at_ctxt_hole_pos gfun_at_possE hole_pos_ctxt_of_pos_term map_option_eq_Some)
next
case False
have q2: "q ∉ gposs s ⟶ q ∈ poss_ctxt (ctxt_of_pos_term p (?t_of_g t))" using sub pos_C q False assms(2)
by (metis (mono_tags, lifting) UnE ctxt_of_pos_term_hole_pos hole_pos_poss mem_Collect_eq pos_t poss_ctxt_of_ctxt_of_poss subsetD)
have t: "gfun_at (gctxt_apply C (gterm_to_None_Some v)) q = gfun_at (gctxt_apply C (gterm_to_None_Some u)) q"
using poss_ctxt_not_hole_rpes_fun_at[OF q False] by (simp add: assms(4))
have [simp]: "fun_at (ctxt_of_pos_term (hole_pos C) (?t_of_g t))⟨?t_of_g v⟩ q = fun_at (ctxt_of_pos_term (hole_pos C) (?t_of_g t))⟨?t_of_g u⟩ q"
using q False poss_ctxt_not_hole_rpes_fun_at
by (metis (mono_tags, lifting) UnE assms(1, 2) ctxt_poss fun_at_def' hole_pos_ctxt_of_pos_term imageE pos_t poss_append_poss q2)
show ?thesis using assms q False pos_t q2 unfolding t
apply (cases "q ∈ gposs s") apply (auto simp: poss_ctxt_not_hole_rpes_fun_at assms(4))
apply (metis (no_types, lifting) assms(4) ctxt_of_pos_term_hole_pos ctxt_supt_id fun_at_def' gfun_at_gpair_Some ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv hole_pos_ctxt_of_pos_term hole_pos_poss mem_Collect_eq poss_ctxt_not_hole_rpes_fun_at poss_ctxt_of_ctxt_of_poss)
apply (metis (no_types, lifting) assms(4) ctxt_supt_id gfun_at_gpair_Some gfun_at_nongposs gpair_poss_args_poss ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv hole_pos_ctxt_of_pos_term pos_C poss_ctxt_not_hole_rpes_fun_at subsetD)
done
qed}
then show ?thesis using poss_eq
by (intro eq_gterm_by_gposs_gfun_at, auto)
(smt UnE assms ctxt_poss ctxt_supt_id gfun_at_gsub_at ground_ctxt_apply ground_term_of_gterm gsubt_at_to_subt_at gterm_of_term_inv hole_pos_ctxt_of_pos_term hole_pos_poss imageE pos_t poss_eq subst_at_gpair_nt_poss_None_Some subt_at_hole_pos term_of_gterm_inv)
qed
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)
lemma ground_ctxt_arbirarty_Var_type:
assumes "ground_ctxt C"
shows "gterm_of_term C⟨term_of_gterm u⟩ = gctxt_apply (adapt_vars_ctxt C) u"
using assms by (metis adapt_vars_ctxt ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv' term_of_gterm_inv)
lemma ground_ctxt_hole_pos_adapt_vars [simp]:
assumes "ground_ctxt C"
shows "hole_pos (adapt_vars_ctxt C) = hole_pos C"
using assms by (induct C) auto
lemma gpair_ctxt_decomposition_2:
assumes "hole_pos C ∉ gposs s"
and "gpair s t = gterm_of_term C⟨term_of_gterm (gterm_to_None_Some u)⟩" and "ground_ctxt C"
shows "gpair s (gctxt_apply (ctxt_of_pos_term (hole_pos C) (term_of_gterm t)) v) = gterm_of_term C⟨term_of_gterm (gterm_to_None_Some v)⟩"
proof -
from gpair_ctxt_decomposition[of "hole_pos C" s "adapt_vars_ctxt C" t u v]
show ?thesis using assms ground_ctxt_arbirarty_Var_type
by (auto simp: ground_ctxt_arbirarty_Var_type assms(3) ground_ctxt_adapt_ground)
qed
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) (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) force
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_impl_code [code]:
"gencode_impl ts = (let tss = map (λt. case t of Some (GFun _ ts) ⇒ ts | _ ⇒ []) ts in
let len = max_list (map length tss) in
let tss' = map (λts. map Some ts @ replicate (len - length ts) None) tss in
GFun (map (λt. case t of Some (GFun f _) ⇒ Some f | _ ⇒ None) ts)
(map gencode_impl (transpose tss')))"
oops
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 ⟷ gta_lang A = T"
definition RR2_spec where
"RR2_spec A T ⟷ gta_lang A = {gpair t u |t u. (t, u) ∈ T}"
definition RRn_spec where
"RRn_spec n A R ⟷ gta_lang A = gencode ` R ∧ (∀ts ∈ R. length ts = n)"
lemma RR1_to_RRn_spec:
assumes "RR1_spec A T"
shows "RRn_spec 1 (fmap_funs_ta (λ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_gta_lang image_comp comp_def gencode_singleton)
qed
lemma RR2_to_RRn_spec:
assumes "RR2_spec A T"
shows "RRn_spec 2 (fmap_funs_ta (λ(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_gta_lang image_comp comp_def prod.case_distrib gencode_pair)
qed
lemma relabel_RR1_spec [simp]:
"finite (ta_states A) ⟹ RR1_spec (relabel_ta A) T ⟷ RR1_spec A T"
by (simp add: RR1_spec_def)
lemma relabel_RR2_spec [simp]:
"finite (ta_states A) ⟹ RR2_spec (relabel_ta A) T ⟷ RR2_spec A T"
by (simp add: RR2_spec_def)
lemma relabel_RRn_spec [simp]:
"finite (ta_states A) ⟹ RRn_spec n (relabel_ta A) T ⟷ RRn_spec n A T"
by (simp add: RRn_spec_def)
lemma trim_RR1_spec [simp]:
"RR1_spec (trim_ta A) T ⟷ RR1_spec A T"
by (simp add: RR1_spec_def gta_lang_def trim_ta_lang)
lemma trim_RR2_spec [simp]:
"RR2_spec (trim_ta A) T ⟷ RR2_spec A T"
by (simp add: RR2_spec_def gta_lang_def trim_ta_lang)
lemma trim_RRn_spec [simp]:
"RRn_spec n (trim_ta A) T ⟷ RRn_spec n A T"
by (simp add: RRn_spec_def gta_lang_def trim_ta_lang)
lemma swap_RR2_spec:
assumes "RR2_spec ta R"
shows "RR2_spec (fmap_funs_ta prod.swap ta) (prod.swap ` R)"
using assms
apply (simp add: RR2_spec_def fmap_funs_gta_lang)
by (smt Collect_cong setcompr_eq_image gpair_swap)
subsection ‹Nullary automata›
lemma false_RRn_spec:
"RRn_spec n (ta.make {} {} {}) {}"
by (auto simp: RRn_spec_def empty_ta_lang)
lemma true_RR0_spec:
"RRn_spec 0 (ta.make {q} {[] [] → q} {}) {[]}"
by (auto simp: RRn_spec_def const_ta_lang gencode_def gunions_def)
subsection ‹Pairing RR1 languages›
text ‹cf. @{const "gpair"}.›
definition pair_automaton :: "('p, 'f) ta ⇒ ('q, 'g) ta ⇒ ('p option × 'q option, 'f option × 'g option) ta" where
"pair_automaton A B = ta.make (Some ` ta_final A × Some ` ta_final B)
({(Some f, None) (map (λp. (Some p, None)) ps) → (Some p, None) |f ps p. f ps → p ∈ ta_rules A} ∪
{(None, Some g) (map (λq. (None, Some q)) qs) → (None, Some q) |g qs q. g qs → q ∈ ta_rules B} ∪
{(Some f, Some g) (zip_fill ps qs) → (Some p, Some q) |f ps p g qs q. f ps → p ∈ ta_rules A ∧ g qs → q ∈ ta_rules B})
({((Some p, q), (Some p', q)) |p q p'. (p, p') ∈ ta_eps A ∧ q ∈ {None} ∪ Some ` ta_states B} ∪
{((p, Some q), (p, Some q')) |p q q'. p ∈ {None} ∪ Some ` ta_states A ∧ (q, q') ∈ ta_eps B})"
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)"
by (simp add: pair_automaton_def) (force simp: fmap_funs_ta_def)
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)"
apply (auto simp: ta_rule.case_distrib fmap_states_ta_def fmap_funs_ta_def ta.make_def image_def split: ta_rule.splits)
apply (metis ta_rule.exhaust_sel ta_rule.simps(1))
apply (metis ta_rule.exhaust_sel ta_rule.sel(1) ta_rule.sel(2) ta_rule.sel(3))
done
lemma states_pair_automaton:
"ta_states (pair_automaton A B) ⊆ ({None} ∪ Some ` ta_states A) × ({None} ∪ Some ` ta_states B)"
unfolding ta_states_def pair_automaton_def ta_make_simps r_states_def
apply (intro Un_least UN_least; intro subrelI)
subgoal for r p q
apply (elim UnE insertE, (force+)[4])
subgoal by (intro SigmaI UnI2) force+
subgoal by (force simp: set_conv_nth nth_zip_fill split: if_splits)
done
by blast+
lemma finite_pair_automaton [simp]:
"finite (ta_states A) ⟹ finite (ta_states B) ⟹ finite (ta_states (pair_automaton A B))"
by (simp add: finite_subset[OF states_pair_automaton])
lemma swap_pair_automaton:
assumes "(p, q) ∈ ta_res (pair_automaton A B) (term_of_gterm t)"
shows "(q, p) ∈ ta_res (pair_automaton B A) (term_of_gterm (map_gterm prod.swap t))"
proof -
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 "ta_eps ?AB ⊆ ta_eps ?BA" "ta_final ?AB ⊆ ta_final ?BA" "ta_rules ?AB ⊆ ta_rules ?BA"
by (auto simp: fmap_states_ta_def fmap_funs_ta_def pair_automaton_def)
} note * = this
let ?BA = "?swp (?swp (pair_automaton B A))" and ?AB = "?swp (pair_automaton A B)"
have "ta_eps ?BA ⊆ ta_eps ?AB" "ta_final ?BA ⊆ ta_final ?AB" "ta_rules ?BA ⊆ ta_rules ?AB"
using *[of B A]
unfolding fmap_funs_ta_def fmap_states_ta_def ta.make_def[symmetric] ta_make_simps Let_def
by (fastforce intro!: image_mono simp: image_def)+
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)
then show ?thesis
using ta_res_fmap_states_ta[OF ta_res_fmap_funs_ta[OF assms], of prod.swap prod.swap]
by (simp add: gterm.map_comp comp_def)
qed
lemma to_ta_res_pair_automaton:
"p ∈ ta_res A (term_of_gterm t) ⟹
(Some p, None) ∈ ta_res (pair_automaton A B) (term_of_gterm (map_gterm (λf. (Some f, None)) t))"
"q ∈ ta_res B (term_of_gterm u) ⟹
(None, Some q) ∈ ta_res (pair_automaton A B) (term_of_gterm (map_gterm (λf. (None, Some f)) u))"
"p ∈ ta_res A (term_of_gterm t) ⟹ q ∈ ta_res B (term_of_gterm u) ⟹
(Some p, Some q) ∈ ta_res (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_res (pair_automaton A B) (term_of_gterm (map_gterm (λf. (Some f, None)) s))"
if "p ∈ ta_res A (term_of_gterm s)" for A B p s
by (intro subsetD[OF ta_res_mono', OF _ _ ta_res_fmap_states_ta[OF ta_res_fmap_funs_ta[OF that]],
unfolded map_term_of_gterm gterm.map_ident])
(auto simp add: pair_automaton_def fmap_states_ta_def fmap_funs_ta_def)
have 2: "q ∈ ta_res B (term_of_gterm t) ⟹
(None, Some q) ∈ ta_res ?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' ∈ ta_rules A" "(p', p) ∈ (ta_eps A)⇧*" "length ps = length ts"
"⋀i. i < length ts ⟹ ps ! i ∈ ta_res A (term_of_gterm (ts ! i))" using GFun(2) by auto
obtain q' qs where q': "g qs → q' ∈ ta_rules B" "(q', q) ∈ (ta_eps B)⇧*" "length qs = length us"
"⋀i. i < length us ⟹ qs ! i ∈ ta_res B (term_of_gterm (us ! i))" using GFun(3) by auto
have *: "Some p ∈ Some ` ta_states A" "Some q' ∈ Some ` ta_states B"
using p'(2,1) q'(1)
apply (-, cases p' p rule: rtrancl.cases)
by (auto simp: r_rhs_states) (auto simp: ta_states_def)
have [simp]: "((Some p', Some q'), (Some p, Some q)) ∈ (ta_eps ?AB)⇧*"
by (rule rtrancl_trans[OF rtrancl_map[OF _ p'(2), of "λp. (Some p, _)" "ta_eps ?AB"]
rtrancl_map[OF _ q'(2), of "λq. (_, Some q)" "ta_eps ?AB"]]) (auto simp: pair_automaton_def *)
have [simp]: "(Some f, Some g) zip_fill ps qs → (Some p', Some q') ∈ ta_rules ?AB"
using p'(1) q'(1) by (auto simp: pair_automaton_def)
show ?case using GFun(1)[OF nth_mem p'(4) q'(4)]
by (auto intro!: exI[of _ "Some p'", OF exI[of _ "Some q'", OF exI[of _ "zip_fill ps qs"]]]
simp: gpair_code nth_zip_fill less_max_iff_disj p'(3) q'(3) 1[OF p'(4)] 2[OF q'(4)])
qed
}
qed
lemma from_ta_res_pair_automaton:
"(None, None) ∉ ta_res (pair_automaton A B) (term_of_gterm s)"
"(Some p, None) ∈ ta_res (pair_automaton A B) (term_of_gterm s) ⟹
∃t. p ∈ ta_res A (term_of_gterm t) ∧ s = map_gterm (λf. (Some f, None)) t"
"(None, Some q) ∈ ta_res (pair_automaton A B) (term_of_gterm s) ⟹
∃u. q ∈ ta_res B (term_of_gterm u) ∧ s = map_gterm (λf. (None, Some f)) u"
"(Some p, Some q) ∈ ta_res (pair_automaton A B) (term_of_gterm s) ⟹
∃t u. p ∈ ta_res A (term_of_gterm t) ∧ q ∈ ta_res 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_res (pair_automaton A B) (term_of_gterm s)"
then have "∃t. p ∈ ta_res 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) ∈ ta_rules (pair_automaton A B)"
"((sp, nq), (Some p, None)) ∈ (ta_eps (pair_automaton A B))⇧*" "length rs = length ss"
"⋀i. i < length ss ⟹ rs ! i ∈ ta_res (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) ∈ (ta_eps A)⇧*"
using r(2)
proof (induct arbitrary: thesis rule: converse_rtrancl_induct2)
case (step sp' nq' sp'' nq'')
guess p'' using step(3) . note [simp] = this(1,2) and pq'' = this(3)
obtain p' where pq': "sp' = Some p'" "nq' = None"
"(p', p'') ∈ ta_eps A"
using step(1) by (auto simp: pair_automaton_def)
then show ?case using pq'' by (auto intro!: step(4)[of p'])
qed auto
obtain f ps where h: "h = (Some f, None)" "rs = map (λx. (Some x, None)) ps"
"f ps → p' ∈ ta_rules A"
using r(1) unfolding pq(1,2) by (auto simp: pair_automaton_def)
obtain ts where "⋀i. i < length ss ⟹
ps ! i ∈ ta_res 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 simp 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_res B (term_of_gterm u) ∧ s = map_gterm (λg. (None, Some g)) u"
if "(None, Some q) ∈ ta_res ?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
have *: "((p, q), (None, None)) ∈ (ta_eps ?AB)⇧* ⟹ p = None ∧ q = None" for p q
by (induct rule: converse_rtrancl_induct2) (auto simp: pair_automaton_def)
show ?case
apply (cases s)
by (auto dest!: *) (auto simp: pair_automaton_def)
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) ∈ ta_rules ?AB"
"((sp, sq), (Some p, Some q)) ∈ (ta_eps ?AB)⇧*" "length rs = length ss"
"⋀i. i < length ss ⟹ rs ! i ∈ ta_res ?AB (term_of_gterm (ss ! i))"
using GFun(2) by auto
obtain p' q' where pq: "sp = Some p'" "sq = Some q'" "(p', p) ∈ (ta_eps A)⇧*" "(q', q) ∈ (ta_eps B)⇧*"
using r(2)
proof (induct arbitrary: thesis rule: converse_rtrancl_induct2)
case (step sp' sq' sp'' sq'')
guess p'' q'' using step(3) . note [simp] = this(1,2) and pq'' = this(3,4)
obtain p' q' where pq': "sp' = Some p'" "sq' = Some q'"
"(p', p'') ∈ ta_eps A ∧ q' = q'' ∨ p' = p'' ∧ (q', q'') ∈ ta_eps B"
using step(1) by (auto simp: pair_automaton_def)
then show ?case using pq'' by (auto intro!: step(4)[of p' q'])
qed auto
obtain f g ps qs where h: "h = (Some f, Some g)" "rs = zip_fill ps qs"
"f ps → p' ∈ ta_rules A" "g qs → q' ∈ ta_rules B"
using r(1) unfolding pq(1,2) by (auto simp: pair_automaton_def)
have *: "∃t u. ps ! i ∈ ta_res A (term_of_gterm t) ∧ qs ! i ∈ ta_res 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_res A (term_of_gterm t)) ∧
(i < length qs ⟶ qs ! i ∈ ta_res 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_res A (term_of_gterm (ts i))) ∧
(i < length qs ⟶ qs ! i ∈ ta_res 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_res A (term_of_gterm (ts i))"
"⋀i. i < length qs ⟹ qs ! i ∈ ta_res 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 pair_automaton:
assumes "RR1_spec A T" "RR1_spec B U"
shows "RR2_spec (pair_automaton A B) (T × U)"
proof -
let ?AB = "pair_automaton A B"
{ fix t u assume t: "t ∈ T" and u: "u ∈ U"
obtain p where p: "p ∈ ta_final A" "p ∈ ta_res A (term_of_gterm t)" using t assms(1)
by (auto simp: RR1_spec_def gta_lang_def image_def gterm_of_term_inv' elim: ta_langE2)
obtain q where q: "q ∈ ta_final B" "q ∈ ta_res B (term_of_gterm u)" using u assms(2)
by (auto simp: RR1_spec_def gta_lang_def image_def gterm_of_term_inv' elim: ta_langE2)
have "gpair t u ∈ gta_lang (pair_automaton A B)" using p(1) q(1) to_ta_res_pair_automaton(3)[OF p(2) q(2)]
by (auto simp: gta_lang_def pair_automaton_def
intro!: image_eqI[where x = "term_of_gterm (gpair t u)"] ta_langI2[of _ "(Some p, Some q)"])
} moreover
{ fix s assume "s ∈ gta_lang (pair_automaton A B)"
from this[unfolded gta_lang_def]
obtain s' r where r: "s = gterm_of_term s'" "ground s'" "r ∈ ta_final ?AB" "r ∈ ta_res ?AB s'"
by (auto elim!: ta_langE2)
have s': "s' = term_of_gterm s" using r(1,2) by simp
obtain p q where pq: "r = (Some p, Some q)" "p ∈ ta_final A" "q ∈ ta_final B"
using r(3) by (auto simp: pair_automaton_def)
guess t u using from_ta_res_pair_automaton(4)[OF r(4)[unfolded pq(1) s']]
by (elim exE conjE) note * = this
then have "t ∈ gta_lang A" "u ∈ gta_lang B" using pq(2,3)
by (metis ground_term_of_gterm ta_langI2 ta_res_adapt_vars_ground term_of_gterm_in_ta_lang_conv)+
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 "gta_lang (pair_automaton A B) = case_prod gpair ` (gta_lang A × gta_lang B)"
using pair_automaton[of A _ B] by (auto simp: RR1_spec_def RR2_spec_def)
subsection ‹Collapsing›
text ‹cf. @{const "gcollapse"}.›
definition collapse_automaton :: "('q, 'f option) ta ⇒ ('q, 'f) ta" where
"collapse_automaton A = (
let Qn = {q' |qs q q'. None qs → q ∈ ta_rules A ∧ (q, q') ∈ (ta_eps A)⇧*} in
let Qs = {q' |f qs q q'. (Some f) qs → q ∈ ta_rules A ∧ (q, q') ∈ (ta_eps A)⇧*} in
ta.make (ta_final A) {
f (map the (filter (λq. ¬ Option.is_none q) qs')) → q |f qs qs' q.
(Some f) qs → q ∈ ta_rules A ∧ length qs = length qs' ∧
(∀i < length qs. qs ! i ∈ Qn ∧ qs' ! i = None ∨ qs ! i ∈ Qs ∧ qs' ! i = Some (qs ! i))
} (ta_eps A))"
lemma collapse_automaton':
assumes "ta_states A ⊆ ta_reachable A"
shows "gta_lang (collapse_automaton A) = the ` (gcollapse ` gta_lang A - {None})"
proof -
define Qn where "Qn = {q' |qs q q'. None qs → q ∈ ta_rules A ∧ (q, q') ∈ (ta_eps A)⇧*}"
define Qs where "Qs = {q' |f qs q q'. (Some f) qs → q ∈ ta_rules A ∧ (q, q') ∈ (ta_eps A)⇧*}"
{ fix t assume t: "t ∈ gta_lang (collapse_automaton A)"
then obtain q where q: "q ∈ ta_final A" "q ∈ ta_res (collapse_automaton A) (term_of_gterm t)"
by (auto simp: gta_lang_def image_def gterm_of_term_inv' collapse_automaton_def elim: ta_langE2)
obtain t' where "q ∈ ta_res A (term_of_gterm t')" "gcollapse t' ≠ None" "t = the (gcollapse t')"
using q(2)
proof (induct t arbitrary: q thesis)
case (GFun f ts)
obtain qs q' where q': "f qs → q' ∈ ta_rules (collapse_automaton A)"
"(q', q) ∈ (ta_eps (collapse_automaton A))⇧*" "length qs = length ts"
"⋀i. i < length ts ⟹ qs ! i ∈ ta_res (collapse_automaton A) (term_of_gterm (ts ! i))"
using GFun(3) by auto
have "∃t'. qs ! i ∈ ta_res A (term_of_gterm t') ∧ gcollapse t' ≠ None ∧ ts ! i = the (gcollapse t')"
if "i < length ts" for i using GFun(1)[OF nth_mem _ q'(4)] that by metis
then obtain ts' where ts':
"qs ! i ∈ ta_res A (term_of_gterm (ts' i)) ∧ gcollapse (ts' i) ≠ None ∧ ts ! i = the (gcollapse (ts' i))"
if "i < length ts" for i by metis
have "(q', q) ∈ (ta_eps A)⇧*" using q'(2) by (auto simp: collapse_automaton_def)
moreover obtain ps rs where ps: "(Some f) ps → q' ∈ ta_rules A" "length ps = length rs"
"⋀i. i < length ps ⟹ ps ! i ∈ Qn ∧ rs ! i = None ∨ ps ! i ∈ Qs ∧ rs ! i = Some (ps ! i)"
"qs = map the (filter (λq. ¬ Option.is_none q) rs)"
using q'(1) by (auto simp: collapse_automaton_def Qn_def Qs_def)
have *: "∃t'. qs ! i ∈ ta_res A (term_of_gterm t') ∧ gcollapse t' ≠ None ∧ ts ! i = the (gcollapse t')"
if "i < length ts" for i using GFun(1)[OF nth_mem _ q'(4)] that by metis
obtain ts' where "length ts' = length ps"
"⋀i. i < length ps ⟹ ps ! i ∈ ta_res A (term_of_gterm (ts' ! i))"
"ts = map the (filter (λq. ¬ Option.is_none q) (map gcollapse ts'))"
using ps(2,3,4) q'(3) ts' *
proof (induct ps arbitrary: rs qs ts ts' thesis)
case (Cons p ps)
obtain r rs' where rs [simp]: "rs = r # rs'" using Cons(3) by (cases rs) auto
show ?case using Cons(4)[of 0, unfolded list.size add_Suc_right, OF zero_less_Suc]
unfolding nth.simps nat.case mem_Collect_eq rs Qn_def Qs_def
proof (elim conjE disjE exE, goal_cases None Some)
case (None qs' q q'')
{ fix i assume i: "i < length qs'"
then have "qs' ! i ∈ ta_states A" using None(3) by (force simp: ta_states_def r_states_def)
then have "∃t. qs' ! i ∈ ta_res A (term_of_gterm t)"
using subsetD[OF assms, of "qs' ! i"] None(3)
by (auto simp: ta_reachable_def dest: ground_term_to_gtermD)
}
then obtain us where "⋀i. i < length qs' ⟹ qs' ! i ∈ ta_res A (term_of_gterm (us i))"
by metis
moreover obtain us' where "length us' = length ps"
"⋀i. i < length ps ⟹ ps ! i ∈ ta_res A (term_of_gterm (us' ! i))"
"ts = map the (filter (λt. ¬ Option.is_none t) (map gcollapse us'))"
using Cons(3,5,6,7,8) Cons(4)[of "Suc _"]
by (subst Cons(1)[of ts _ rs' qs ts']) (auto simp: None(1,2))
ultimately show ?case using None(3,4)
by (intro Cons(2)[of "GFun None (map us [0..<length qs']) # us'"])
(auto 0 4 simp: less_Suc_eq_0_disj None(2))
next
case (Some f qs' q p)
obtain q'' qs'' where [simp]: "qs = q'' # qs''" by (auto simp: Cons(5) Some(1))
obtain t'' ts'' where [simp]: "ts = t'' # ts''" using Cons(6) by (cases ts) auto
obtain t' where "qs ! 0 ∈ ta_res A (term_of_gterm t')" "gcollapse t' ≠ None"
"ts ! 0 = the (gcollapse t')" using Cons(8)[of 0] by auto
moreover obtain us' where "length us' = length ps"
"⋀i. i < length ps ⟹ ps ! i ∈ ta_res A (term_of_gterm (us' ! i))"
"ts'' = map the (filter (λt. ¬ Option.is_none t) (map gcollapse us'))"
using Cons(3,5,6) Cons(4,7,8)[of "Suc _"]
by (subst Cons(1)[of ts'' _ rs' qs'' "ts' ∘ Suc"]) (auto simp: Some(1))
ultimately show ?case using arg_cong[OF Cons(5), of hd]
by (intro Cons(2)[of "t' # us'"]) (auto simp: less_Suc_eq_0_disj Some(1,2))
qed
qed auto
ultimately show ?case using ps(1,2) by (intro GFun(2)[of "GFun (Some f) ts'"]) auto
qed
then have "t ∈ the ` (gcollapse ` gta_lang A - {None})" by (metis q(1) DiffI ground_term_of_gterm
gterm_of_term_inv gterm_of_term_inv' image_eqI singletonD ta_langI2 term_of_gterm_in_ta_lang_conv)
} moreover
{ fix t assume t: "t ∈ gta_lang A" "gcollapse t ≠ None"
obtain q where q: "q ∈ ta_final (collapse_automaton A)" "q ∈ ta_res A (term_of_gterm t)" using t(1)
by (auto simp: gta_lang_def image_def gterm_of_term_inv' collapse_automaton_def elim: ta_langE2)
have "q ∈ ta_res (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: "f qs → q' ∈ ta_rules A" "(q', q) ∈ (ta_eps (collapse_automaton A))⇧*"
"length qs = length ts" "⋀i. i<length ts ⟹ qs ! i ∈ ta_res 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)
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)
ultimately have "f' (map the (filter (λq. ¬ Option.is_none q) qs')) → q' ∈ ta_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_res (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 (collapse_automaton A)" by (metis q(1)
ground_term_of_gterm gterm_of_term_inv' term_of_gterm_in_ta_lang_conv term_of_gterm_inv ta_langI2)
} ultimately show ?thesis by blast
qed
lemma collapse_automaton:
assumes "ta_states A ⊆ ta_reachable A" "RR1_spec A T"
shows "RR1_spec (collapse_automaton A) (the ` (gcollapse ` gta_lang A - {None}))"
using collapse_automaton'[OF assms(1)] assms(2) by (simp add: 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: 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_ta (pad_with_Nones n m) (pair_automaton 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: 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 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_ta (λ(f, g). pad_with_Nones 1 m (map_option (λf. [Some f]) f, g))
(pair_automaton 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: 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›
lemma drop_automaton:
assumes "ta_states A ⊆ ta_reachable A" "m < n" "RRn_spec n A T"
defines "f ≡ λfs. if list_all (Option.is_none) (drop m fs) then None else Some (drop m fs)"
shows "RRn_spec (n - m) (collapse_automaton (fmap_funs_ta 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)"
by (auto simp: fun_at_def' split: if_splits)
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: 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
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_ta (λxs. map ((!) xs) ps) A) ((λxs. map ((!) xs) ps) ` T)"
using assms by (auto simp: RRn_spec_def gencode_permute 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 (intersect_ta A B) (T ∩ U)"
proof -
have *: "ta_lang A ⊆ (term_of_gterm ` UNIV :: (_, _) term set)" for A
by (auto dest: ta_lang_imp_ground simp: image_def ground_term_to_gtermD)
have "inj_on gterm_of_term (term_of_gterm ` UNIV)" by (simp add: inj_on_def)
note [simp] = inj_on_image_Int[OF this * *, of A B]
have "inj gencode" unfolding inj_def using gdecode_gencode by metis
note [simp] = image_Int[OF this, of T U]
show ?thesis using assms
by (simp add: gta_lang_def_sym RRn_spec_def intersect_ta[of A B] cong[OF gta_lang_def refl, of "intersect_ta _ _"])
qed
subsection ‹Union›
definition union_automaton :: "('p, 'f) ta ⇒ ('q, 'f) ta ⇒ ('p + 'q, 'f) ta" where
"union_automaton A B = ta.make (Inl ` ta_final A ∪ Inr ` ta_final B)
(map_ta_rule Inl id ` ta_rules A ∪ map_ta_rule Inr id ` ta_rules B)
(map_prod Inl Inl ` ta_eps A ∪ map_prod Inr Inr ` ta_eps B)"
lemma swap_union_automaton:
"fmap_states_ta (case_sum Inr Inl) (union_automaton B A) = union_automaton A B"
by (simp add: fmap_states_ta_def' union_automaton_def image_Un image_comp case_sum_o_inj
ta_rule.map_comp prod.map_comp comp_def id_def ac_simps)
lemma union_automaton':
"gta_lang (union_automaton A B) = gta_lang A ∪ gta_lang B"
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr t)
then obtain t' q where q: "t = gterm_of_term t'" "ground t'" "q ∈ ta_final (union_automaton A B)"
"q ∈ ta_res (union_automaton A B) t'" by (auto simp: gta_lang_def elim!: ta_langE2)
from q(1,2) have t': "t' = term_of_gterm t" by (auto dest!: ground_term_to_gtermD)
{ fix q A B assume "Inl q ∈ ta_res (union_automaton A B) (term_of_gterm t)"
then have "q ∈ ta_res A (adapt_vars (term_of_gterm t))"
proof (induct t arbitrary: q)
case (GFun f ts)
obtain sqs sq' where q: "f sqs → sq' ∈ ta_rules (union_automaton A B)"
"(sq', Inl q) ∈ (ta_eps (union_automaton A B))⇧*" "length sqs = length ts"
"⋀i. i < length ts ⟹ sqs ! i ∈ ta_res (union_automaton A B) (term_of_gterm (ts ! i))"
using GFun(2) by auto
obtain q' where q': "sq' = Inl q'" "(q', q) ∈ (ta_eps A)⇧*" using q(2)
proof (induct sq' arbitrary: thesis rule: converse_rtrancl_induct)
case (step sq sq')
obtain q' where "sq' = Inl q'" "(q', q) ∈ (ta_eps A)⇧*" using step(3) .
moreover then obtain q'' where "sq = Inl q''" "(q'', q') ∈ ta_eps A"
using step(1) by (auto simp: union_automaton_def)
ultimately show ?case by (auto intro!: step(4)[of q''])
qed auto
have [simp]: "map_ta_rule f g r = (case r of h qs → q ⇒ (g h) (map f qs) → f q)" for f g r
by (cases r) auto
obtain qs where "sqs = map Inl qs" "f qs → q' ∈ ta_rules A" using q(1) q'(1)
by (auto simp: union_automaton_def split: ta_rule.splits)
then show ?case using q(3,4) GFun(1)[OF nth_mem, of i "qs ! i" for i] q'(2)
by (auto intro!: exI[of _ q'] exI[of _ qs])
qed
} note * = this
note this[of _ A B] this[of _ B A, folded swap_union_automaton[of A B]]
ta_res_fmap_states_ta[of "Inr _" "union_automaton A B" "term_of_gterm t" "case_sum Inr Inl"]
then show ?case
proof (cases q)
case (Inl q')
then have "q' ∈ ta_final A" using q(3) by (auto simp: union_automaton_def)
then show ?thesis using q(2,4) *[of q' A B]
by (auto intro!: UnI1 image_eqI[of _ _ "adapt_vars t'"] ta_langI2[of _ q']
simp: gterm_of_term_inv'[symmetric] Inl gta_lang_def t')
next
case (Inr q')
then have "q' ∈ ta_final B" using q(3) by (auto simp: union_automaton_def)
then show ?thesis using q(2,4) *[of q' B A, folded swap_union_automaton[of A B]]
ta_res_fmap_states_ta[of "Inr q'" "union_automaton A B" "term_of_gterm t" "case_sum Inr Inl"]
by (auto intro!: UnI2 image_eqI[of _ _ "adapt_vars t'"] ta_langI2[of _ q']
simp: gterm_of_term_inv'[symmetric] gterm.map_ident t' Inr gta_lang_def)
qed
next
case (rl t)
have "ta_subset (fmap_states_ta Inl A) (union_automaton A B)"
"ta_subset (fmap_states_ta Inr B) (union_automaton A B)"
by (force simp: ta_subset_def union_automaton_def fmap_states_ta_def split: ta_rule.splits)+
note this[THEN ta_lang_mono, THEN image_mono[of _ _ gterm_of_term]]
then show ?case using rl
by (auto simp: fmap_ta(2)[of Inl A] fmap_ta(2)[of Inr B] gta_lang_def_sym)
qed
lemma union_automaton:
assumes "RRn_spec n A T" "RRn_spec n B U"
shows "RRn_spec n (union_automaton A B) (T ∪ U)"
using assms by (auto simp: RRn_spec_def union_automaton')
lemma ta_states_union_automaton:
"ta_states (union_automaton A B) = (Inl ` ta_states A) ∪ (Inr ` ta_states B)"
by (auto simp: ta_states_def union_automaton_def r_states_def ta_rule.map_sel)
subsection ‹All terms over a signature›
definition term_automaton :: "('f × nat) set ⇒ (unit, 'f) ta" where
"term_automaton ℱ = ta.make {()} {f (replicate n ()) → () |f n. (f, n) ∈ ℱ} {}"
lemma term_automaton:
"RR1_spec (term_automaton ℱ) {t. funas_gterm t ⊆ ℱ}"
unfolding RR1_spec_def gta_lang_def
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr t)
then have "() ∈ ta_res (term_automaton ℱ) (term_of_gterm t)"
by (auto elim: ta_langE2)
then show ?case
by (induct t) (fastforce simp: term_automaton_def set_conv_nth funas_gterm_def split: if_splits)
next
case (rl t)
then have "() ∈ ta_res (term_automaton ℱ) (term_of_gterm t)"
by (induct t) (auto simp: term_automaton_def UN_subset_iff funas_gterm_def intro!: exI[of _ "replicate (length _) ()"])
then show ?case
by (auto simp: term_automaton_def intro: ta_langI2 intro!: image_eqI[of _ _ "term_of_gterm t"])
qed
fun true_RRn :: "('f × nat) set ⇒ nat ⇒ (nat, 'f option list) ta" where
"true_RRn ℱ 0 = ta.make {0} {[] [] → 0} {}"
| "true_RRn ℱ (Suc 0) = relabel_ta (fmap_funs_ta (λf. [Some f]) (term_automaton ℱ))"
| "true_RRn ℱ (Suc n) = relabel_ta
(trim_ta (fmap_funs_ta (pad_with_Nones 1 n) (pair_automaton (true_RRn ℱ 1) (true_RRn ℱ n))))"
lemma true_RRn_spec:
assumes "finite ℱ"
shows "finite (ta_states (true_RRn ℱ n)) ∧ RRn_spec n (true_RRn ℱ n) {ts. length ts = n ∧ set ts ⊆ {t. funas_gterm t ⊆ ℱ}}"
using assms
proof (induct ℱ n rule: true_RRn.induct)
case (1 ℱ) show ?case by (simp cong: conj_cong add: true_RR0_spec ta_states_def r_states_def)
next
case (2 ℱ)
moreover have "{ts. length ts = 1 ∧ set ts ⊆ {t. funas_gterm t ⊆ ℱ}} = (λt. [t]) ` {t. funas_gterm t ⊆ ℱ}"
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 ⊆ {t. funas_gterm t ⊆ ℱ} ∧ length us = m ∧
set us ⊆ {t. funas_gterm t ⊆ ℱ}} = {ss. length ss = n + m ∧ set ss ⊆ {t. funas_gterm t ⊆ ℱ}}" 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(1,2)[THEN conjunct2]] 3(1,2)[THEN conjunct1] 3(3) by simp
qed
locale many_sorted_terms =
fixes sigF :: "('f × nat) ⇒ ('t list × 't) option" and sigV :: "'v ⇒ 't option"
assumes arity: "sigF (f, n) = Some (tys, tr) ⟹ length tys = n"
begin
definition ℱ where
"ℱ = { fn. sigF fn ≠ None }"
definition 𝒱 where
"𝒱 = { v. sigV v ≠ None }"
inductive 𝒯⇩α :: "'t ⇒ ('f, 'v) term ⇒ bool" where
var [intro]: "sigV x = Some α ⟹ 𝒯⇩α α (Var x)"
| funs [intro]: "sigF (f, length ts) = Some (tys, α) ⟹
(∀ i < length ts. 𝒯⇩α (tys ! i) (ts ! i)) ⟹ 𝒯⇩α α (Fun f ts)"
definition term_automaton :: "('t, 'f) ta" where
"term_automaton = ta.make {tr |f n tys tr. sigF (f, n) = Some (tys, tr)}
{f tys → tr |f n tys tr. sigF (f, n) = Some (tys, tr)} {}"
lemma ta_res_term_automaton:
"α ∈ ta_res term_automaton (term_of_gterm t) ⟷ 𝒯⇩α α (term_of_gterm t)"
proof (intro iffI, goal_cases lr rl)
case lr then show ?case
proof (induct t arbitrary: α)
case (GFun f ts)
obtain qs where "length qs = length ts" "sigF (f, length ts) = Some (qs, α)"
"⋀i. i < length ts ⟹ qs ! i ∈ ta_res term_automaton (term_of_gterm (ts ! i))"
using GFun(2) by (auto simp: term_automaton_def arity)
then show ?case using GFun(1)[OF nth_mem, of i "_ ! i" for i] by auto
qed
next
case rl then show ?case
proof (induct t arbitrary: α)
case (GFun f ts)
obtain qs where "sigF (f, length ts) = Some (qs, α)" "length qs = length ts"
"⋀i. i < length ts ⟹ 𝒯⇩α (qs ! i) (term_of_gterm (ts ! i))"
using GFun(2) by (auto elim!: 𝒯⇩α.cases simp: arity)
then show ?case using GFun(1)[OF nth_mem, of i "qs ! i" for i]
by (auto simp: term_automaton_def intro!: exI[of _ qs])
qed
qed
lemma term_automaton:
"RR1_spec term_automaton {t |α t. 𝒯⇩α α (term_of_gterm t)}"
unfolding RR1_spec_def gta_lang_def
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr t)
then obtain α where "α ∈ ta_res term_automaton (term_of_gterm t)"
by (auto elim: ta_langE2)
then show ?case by (auto simp: ta_res_term_automaton)
next
case (rl t)
then obtain α where "𝒯⇩α α (term_of_gterm t)" by auto
moreover then have "α ∈ ta_final term_automaton"
by (cases t) (auto simp: ta_res_term_automaton[symmetric] term_automaton_def elim!: 𝒯⇩α.cases)
ultimately show ?case by (auto simp: ta_res_term_automaton[symmetric] intro: ta_langI2
intro!: image_eqI[of _ _ "term_of_gterm t"])
qed
end
end