theory GTT
imports TR.Tree_Automata FOR.Lift_Root_Step
begin
type_synonym ('q, 'f) gtt = "('q, 'f) ta × ('q, 'f) ta"
abbreviation gtt_rules where
"gtt_rules 𝒢 ≡ rules (fst 𝒢) |∪| rules (snd 𝒢)"
abbreviation gtt_eps where
"gtt_eps 𝒢 ≡ eps (fst 𝒢) |∪| eps (snd 𝒢)"
definition gtt_states where
"gtt_states 𝒢 = 𝒬 (fst 𝒢) |∪| 𝒬 (snd 𝒢)"
abbreviation gtt_syms where
"gtt_syms 𝒢 ≡ ta_sig (fst 𝒢) |∪| ta_sig (snd 𝒢)"
definition gtt_interface where
"gtt_interface 𝒢 = 𝒬 (fst 𝒢) |∩| 𝒬 (snd 𝒢)"
inductive gtt_accept :: "('q, 'f) gtt ⇒ 'f gterm ⇒ 'f gterm ⇒ bool" for 𝒢 where
refl [intro]: "gtt_accept 𝒢 t t"
| join [intro]: "q |∈| gta_der (fst 𝒢) s ⟹ q |∈| gta_der (snd 𝒢) t ⟹ gtt_accept 𝒢 s t"
| ctxt [intro]: "length ss = length ts ⟹
∀i < length ss. gtt_accept 𝒢 (ss ! i) (ts ! i) ⟹
gtt_accept 𝒢 (GFun f ss) (GFun f ts)"
hide_fact (open) refl
inductive gtt_accept' :: "('q, 'f) gtt ⇒ 'f gterm ⇒ 'f gterm ⇒ bool"
for 𝒢 where
mctxt [intro]: "length ss = length ts ⟹ num_gholes C = length ss ⟹
∀i < length ts. ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i) ⟹
gtt_accept' 𝒢 (fill_gholes C ss) (fill_gholes C ts)"
text ‹language accepted by a GTT›
abbreviation gtt_lang :: "('q, 'f) gtt ⇒ 'f gterm rel" where
"gtt_lang 𝒢 ≡ {(s, t). gtt_accept 𝒢 s t}"
abbreviation gtt_lang_terms :: "('q, 'f) gtt ⇒ ('f, 'q) term rel" where
"gtt_lang_terms 𝒢 ≡ {(s, t). gtt_accept 𝒢 (gterm_of_term s) (gterm_of_term t) ∧ ground s ∧ ground t}"
lemma term_of_gterm_gtt_lang_gtt_lang_terms_conv:
"map_both term_of_gterm ` gtt_lang 𝒢 = gtt_lang_terms 𝒢"
by auto (metis CollectI case_prodI gterm_of_term_inv map_prod_imageI)
text ‹*anchored* language accepted by a GTT›
definition agtt_lang :: "('q, 'f) gtt ⇒ 'f gterm rel" where
"agtt_lang 𝒢 = {(t, u) |t u q. q |∈| gta_der (fst 𝒢) t ∧ q |∈| gta_der (snd 𝒢) u}"
lemma converse_agtt_lang:
"(agtt_lang 𝒢)¯ = agtt_lang (prod.swap 𝒢)"
by (auto simp: agtt_lang_def)
lemma agtt_lang_swap:
"agtt_lang (prod.swap 𝒢) = prod.swap ` agtt_lang 𝒢"
by (auto simp: agtt_lang_def)
lemma gtt_accept'_refl [simp]:
"gtt_accept' 𝒢 t t"
proof -
have "gtt_accept' 𝒢 (fill_gholes (gmctxt_of_gterm t) [])
(fill_gholes (gmctxt_of_gterm t) [])" by fastforce
thus ?thesis by simp
qed
lemma gtt_accept'_join [simp]:
assumes "q |∈| gta_der (fst 𝒢) s" "q |∈| gta_der (snd 𝒢) t"
shows "gtt_accept' 𝒢 s t"
proof -
have "gtt_accept' 𝒢 (fill_gholes GMHole [s]) (fill_gholes GMHole [t])"
using assms by (intro gtt_accept'.intros) auto
thus ?thesis by simp
qed
lemma gtt_cont_extrct:
assumes "gtt_accept' 𝒢 s t"
shows "∃C ss ts. s =⇩G⇩f (C, ss) ∧ t =⇩G⇩f (C, ts) ∧
(∀i < length ts. ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧
q |∈| gta_der (snd 𝒢) (ts ! i))"
using assms by (auto elim!: gtt_accept'.cases) (metis eq_gfill.intros)
lemma gtt_accept'E [elim]:
assumes "gtt_accept' 𝒢 s t"
obtains C ss ts where "s = fill_gholes C ss" "t = fill_gholes C ts"
"num_gholes C = length ss" "num_gholes C = length ts"
"∀ i < length ts. ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
using gtt_cont_extrct[OF assms] eqgfE
by blast
lemma gtt_accept'_closed:
assumes "length ss = length ts" "∀ i < length ts. gtt_accept' 𝒢 (ss ! i) (ts ! i)"
shows " gtt_accept' 𝒢 (GFun f ss) (GFun f ts)"
proof -
let ?Prop = "λ (C, ss',ts') i. ss ! i =⇩G⇩f (C, ss') ∧ ts ! i =⇩G⇩f (C, ts') ∧
(∀j < length ts'. ∃q. q |∈| gta_der (fst 𝒢) (ss' ! j) ∧
q |∈| gta_der (snd 𝒢) (ts' ! j)) ∧
gtt_accept' 𝒢 (fill_gholes C ss') (fill_gholes C ts')"
from assms gtt_cont_extrct[of 𝒢 "ss ! i" "ts ! i" for i]
have "∀ i < length ts. ∃ C ss' ts'. ?Prop (C, ss', ts') i" for i
by auto (metis eqgfE(1))
then obtain xs where inv: "length ts = length xs" "∀ i < length xs. ?Prop (xs ! i) i"
using Ex_list_of_length_P[of "length ts" ?Prop]
by fastforce
define Ds where "Ds ≡ map fst xs" define sss where "sss ≡ map (fst ∘ snd) xs"
define tss where "tss ≡ map (snd ∘ snd) xs" note unf = Ds_def sss_def tss_def
let ?C = "GMFun f (replicate (length Ds) GMHole)"
have len: "length ts = length Ds" "length Ds = length sss" "length sss = length tss"
using inv(1) by (auto simp: unf comp_def)
then have eq: "∀ i < length tss. ss ! i =⇩G⇩f (Ds ! i, sss ! i)" "∀ i < length tss. ts ! i =⇩G⇩f (Ds ! i, tss ! i)"
using len inv by (auto simp: unf)
then have len_inn: "∀ i < length tss. length (sss ! i) = length (tss ! i)"
using len by auto (metis eqgfE(2))
have mem: "∀ i < length (concat tss). ∃ q. q |∈| gta_der (fst 𝒢) (concat sss ! i) ∧ q |∈| gta_der (snd 𝒢) (concat tss ! i)"
using len len_inn inv by (intro concat_nth_nthI) (auto simp: unf comp_def case_prod_unfold)
have *: "fill_gholes ?C ss = GFun f ss" "fill_gholes ?C ts = GFun f ts"
using len assms(1) by (auto simp del: fill_gholes.simps)
have s: "GFun f ss =⇩G⇩f (fill_gholes_gmctxt ?C Ds, concat sss)"
using assms(1) eq len_inn len inv(1) unfolding *[symmetric]
by (intro fill_gholes_gmctxt_sound) (auto simp add: assms(1))
have t: "GFun f ts =⇩G⇩f (fill_gholes_gmctxt ?C Ds, concat tss)"
using assms(1) eq len_inn len inv(1) unfolding *[symmetric]
by (intro fill_gholes_gmctxt_sound) (auto simp add: assms(1))
show ?thesis unfolding eqgfE[OF s] eqgfE[OF t]
using mem len inv(1) len_inn eq eqgfE(2)[OF s] eqgfE(2)[OF t]
by (intro gtt_accept'.mctxt[of "concat sss" "concat tss" "fill_gholes_gmctxt ?C Ds" 𝒢])
(auto simp del: fill_gholes_gmctxt.simps fill_gholes.simps)
qed
lemma gtt_accept_equiv:
"gtt_accept 𝒢 s t ⟷ gtt_accept' 𝒢 s t"
proof (rule iffI)
assume "gtt_accept 𝒢 s t"
then show "gtt_accept' 𝒢 s t"
proof (induction rule: gtt_accept.induct)
case (ctxt ss ts f)
then show ?case using gtt_accept'_closed[OF ctxt(1), of 𝒢]
by auto
qed auto
next
assume "gtt_accept' 𝒢 s t"
then show "gtt_accept 𝒢 s t"
proof (induction rule: gtt_accept'.induct)
case (mctxt ss ts C) thus ?case
proof (induction C arbitrary: ss ts)
case GMHole
then obtain s' t' where "ss = [s']" "ts = [t']" by (cases ss; cases ts) fastforce+
thus ?case using GMHole(3) by auto
next
case (GMFun f Cs)
moreover { fix i
assume asm: "i < length Cs"
hence lengths_eq: "length (partition_gholes ss Cs ! i) = length (partition_gholes ts Cs ! i)"
by (metis calculation(2, 3) length_map length_partition_by_nth num_gholes.simps(2))
have num_holes_length: "num_gholes (Cs ! i) = length (partition_gholes ss Cs ! i)"
using asm GMFun(3) by (simp add: length_partition_by_nth)
have join: "∀j<length (partition_gholes ts Cs ! i).
∃q. q |∈| gta_der (fst 𝒢) ((partition_gholes ss Cs ! i) ! j) ∧
q |∈| gta_der (snd 𝒢) ((partition_gholes ts Cs ! i) ! j)"
using GMFun(2,3,4)
by (simp add: asm length_partition_by_nth partition_by_nth_nth(1) partition_by_nth_nth(2))
have "gtt_accept 𝒢 (fill_gholes (Cs ! i) (partition_gholes ss Cs ! i))
(fill_gholes (Cs ! i) (partition_gholes ts Cs ! i))"
using asm GMFun(1)[OF _ lengths_eq num_holes_length join] by auto
}
ultimately show ?case using length_upt[of 0 "length Cs"] unfolding fill_gholes.simps
by (intro gtt_accept.intros(3)) auto
qed
qed
qed
lemma accept'_closed_ctxt:
assumes "length ss = length ts"
and "∀i < length ts. gtt_accept' 𝒢 (ss ! i) (ts ! i)"
and "num_gholes C = length ss"
shows "gtt_accept' 𝒢 (fill_gholes C ss) (fill_gholes C ts)" using assms
proof (induction C arbitrary: ss ts)
case GMHole
then show ?case
by (cases ss; cases ts) auto
next
case (GMFun f Cs)
let ?sss = "(partition_gholes ss Cs)"
let ?tss = "(partition_gholes ts Cs)"
obtain Css Cts where Css_Cts:"fill_gholes (GMFun f Cs) ss = GFun f Css"
"fill_gholes (GMFun f Cs) ts = GFun f Cts" "length Cts = length Css"
by simp
{fix i
assume loc_asm: "i < length Cs"
hence "length (?sss ! i) = length (?tss ! i)" using assms(1) GMFun
by (simp add: length_partition_by_nth)
moreover have "num_gholes (Cs ! i) = length (?sss ! i)" using assms(2) loc_asm GMFun
by (simp add: length_partition_by_nth)
moreover have "∀j < length (?tss ! i). gtt_accept' 𝒢 ((?sss ! i) ! j) ((?tss ! i) ! j)"
using loc_asm GMFun assms(3)
by (simp add: calculation(1, 2) partition_by_nth_nth(1, 2))
ultimately have "gtt_accept' 𝒢 (fill_gholes (Cs ! i) (?sss ! i)) (fill_gholes (Cs ! i) (?tss ! i))"
using GMFun(1) loc_asm by force
hence "gtt_accept 𝒢 (fill_gholes (Cs!i) (?sss!i)) (fill_gholes (Cs ! i) (?tss ! i))"
using gtt_accept_equiv by blast}
hence "∀i < length Cts. gtt_accept 𝒢 (Css ! i) (Cts ! i)" using Css_Cts by fastforce
hence "gtt_accept 𝒢 (GFun f Css) (GFun f Cts)" using Css_Cts(3) by auto
then show ?case using gtt_accept_equiv Css_Cts by metis
qed
lemma gtt_lang_from_agtt_lang:
"gtt_lang 𝒢 = lift_root_step UNIV PAny EParallel (agtt_lang 𝒢)"
by (auto simp: lift_root_step.simps gtt_accept_equiv agtt_lang_def elim!: gtt_accept'E gmctxtex_onpE)
text ‹Inverse of GTTs.›
lemma gtt_accept_swap [simp]:
"gtt_accept (prod.swap 𝒢) s t ⟷ gtt_accept 𝒢 t s"
unfolding gtt_accept_equiv
by (intro iffI; elim gtt_accept'.cases; metis gtt_accept'.intros fst_swap snd_swap)
lemma gtt_lang_swap:
"(gtt_lang (A, B))¯ = gtt_lang (B, A)"
using gtt_accept_swap[of "(A, B)"] by auto
lemma gmctxtex_onp_gtt_accpet:
"gmctxtex_onp (λC. True) (agtt_lang 𝒢)= gtt_lang 𝒢"
using gtt_lang_from_agtt_lang[ unfolded lift_root_step.simps, of 𝒢]
unfolding agtt_lang_def
by force
lemma gtt_lang_signature_closed:
"signature_closed UNIV (gtt_lang 𝒢)"
unfolding gmctxtex_onp_gtt_accpet[symmetric]
by (intro gmctxtex_onp_sig_closed) simp
abbreviation mctxt_of_terms where
"mctxt_of_terms s t ≡ (mctxt_of_term s) ⊓ (mctxt_of_term t)"
abbreviation residuals where
"residuals s t ≡ inf_mctxt_args (mctxt_of_term s) (mctxt_of_term t)"
lemma term_mctxt [simp]:
"term_of_mctxt (MFun f (map mctxt_of_term ts)) = Fun f ts"
by (metis term_of_mctxt_mctxt_of_term_id mctxt_of_term.simps(2))
lemma map_zip_fun:
assumes "length xs = length ys"
shows "map (λ(x,y). f x y) (zip (map g xs) (map g ys)) =
map (λ(x,y). f (g x) (g y)) (zip xs ys)"
by (simp add: map_nth_eq_conv)
lemma terms_to_common_residuals:
fixes s t :: "('f, 'v) term"
shows "s = fill_holes (mctxt_of_terms s t) (map term_of_mctxt (residuals s t)) ∧
t = fill_holes (mctxt_of_terms s t) (map term_of_mctxt (residuals t s))"
proof (induction s arbitrary: t)
case (Var x) thus ?case
proof (induction t)
case (Var y)
have "num_holes (MVar y ⊓ MVar x) = num_holes (MVar x ⊓ MVar y)" by simp
define n_holes where "n_holes = (λ (x::'v) y. num_holes (MVar x ⊓ MVar y))"
have "(n_holes y x = n_holes x y ∧ Var y = Var x) ∨
(n_holes y x = n_holes x y ∧ y ≠ x)" using n_holes_def by simp
thus ?case by fastforce
next
case (Fun f ts)
have "Fun f ts = term_of_mctxt (MFun f (map mctxt_of_term ts))"
by (metis mctxt_of_term.simps(2) term_of_mctxt_mctxt_of_term_id)
hence "Fun f ts = fill_holes (mctxt_of_terms (Var x) (Fun f ts))
(map term_of_mctxt (residuals (Fun f ts) (Var x)))"
using term_mctxt[of f ts] by fastforce
thus ?case by auto
qed
next
case (Fun g ss) thus ?case
proof (induction t arbitrary: g ss)
case (Var y)
have "Fun g ss = fill_holes (mctxt_of_terms (Var y) (Fun g ss))
(map term_of_mctxt (residuals (Fun g ss) (Var y)))"
using term_mctxt[of g ss] by fastforce
thus ?case using term_mctxt[of g ss] by fastforce
next
case (Fun f ts) thus ?case
proof (cases "f = g ∧ length ts = length ss")
case True
hence "mctxt_of_terms (Fun g ss) (Fun f ts) =
MFun f (map (λ(s',t'). mctxt_of_terms s' t') (zip ss ts))"
using True by (simp add: zip_nth_conv)
let ?Cs = "map (λ(s',t'). mctxt_of_terms s' t') (zip ss ts)" and
?ts = "residuals (Fun g ss) (Fun f ts)" and
?ts' = "map (λ(s',t'). inf_mctxt_args s' t') (zip (map mctxt_of_term ss) (map mctxt_of_term ts))" and
?ts'' = "map (λ(s',t'). residuals s' t') (zip ss ts)" and
?ss = "residuals (Fun f ts) (Fun g ss)" and
?ss' = "map (λ(t',s'). inf_mctxt_args t' s') (zip (map mctxt_of_term ts) (map mctxt_of_term ss))" and
?ss'' = "map (λ(t',s'). residuals t' s') (zip ts ss)"
{ fix s' t' :: "('f, 'v) Term.term" and ss' ts'
assume "s' ∈ set ss'" "t' ∈ set ts'"
hence "length (residuals s' t') = num_holes (mctxt_of_terms s' t')"
"length (residuals s' t') = num_holes (mctxt_of_terms t' s')"
using num_holes_inf_mctxt by (metis, metis inf_mctxt_comm)
} note residuals_num_holes = this
have "i < length (map num_holes ?Cs) ⟹
length (?ts'' ! i) = (map num_holes ?Cs) ! i" for i
using residuals_num_holes(1)[of _ ss _ ts] True by force
hence "partition_by ?ts (map num_holes ?Cs) = ?ts'"
using partition_by_concat_id[of ?ts' "map num_holes ?Cs"] True by simp
hence part1: "map (λ(s', t'). residuals s' t') (zip ss ts) = partition_holes ?ts ?Cs"
using True map_zip_fun by metis
have "i < length (map num_holes ?Cs) ⟹
length (?ss'' ! i) = (map num_holes ?Cs) ! i" for i
using residuals_num_holes(2)[of _ ts _ ss] True by force
hence "partition_by ?ss (map num_holes ?Cs) = ?ss'"
using partition_by_concat_id[of ?ss' "map num_holes ?Cs"] True by simp
hence part2: "map (λ(t', s'). residuals t' s') (zip ts ss) = partition_holes ?ss ?Cs"
using True map_zip_fun by metis
have push_map_inside: "(map term_of_mctxt) ∘ (λ(x, y). residuals x y) =
(λ(x, y). map term_of_mctxt (residuals x y))" by auto
{ fix i
assume "i < length ss"
hence ith_in_set: "ss ! i ∈ set ss" using True by simp+
hence IH': "ss ! i = fill_holes (mctxt_of_terms (ss ! i) (ts ! i))
(map term_of_mctxt (residuals (ss ! i) (ts ! i)))"
"ts ! i = fill_holes (mctxt_of_terms (ss ! i) (ts ! i))
(map term_of_mctxt (residuals (ts ! i) (ss ! i)))"
using Fun(2)[of "ss ! i" "ts ! i"] True by (meson set_zip_leftD)+
have "ss ! i = fill_holes (map (λ(x, y). mctxt_of_terms x y) (zip ss ts) ! i)
(map (λ(x, y). map term_of_mctxt (residuals x y)) (zip ss ts) ! i)"
"ts ! i = fill_holes (map (λ(x, y). mctxt_of_terms x y) (zip ss ts) ! i)
(map (λ(x, y). map term_of_mctxt (residuals x y)) (zip ts ss) ! i)"
using IH' True nth_map[of i "zip ss ts"] ‹i < length ss› by force+
} note inner = this
have "Fun g ss = fill_holes (mctxt_of_terms (Fun g ss) (Fun f ts))
(map term_of_mctxt (residuals (Fun g ss) (Fun f ts)))"
using True part1[symmetric]
by (simp add: map_map_partition_by[symmetric] map_zip_fun push_map_inside)
(smt inner(1) atLeastLessThan_iff map_eq_conv map_nth set_upt)
moreover have "Fun f ts = fill_holes (mctxt_of_terms (Fun g ss) (Fun f ts))
(map term_of_mctxt (residuals (Fun f ts) (Fun g ss)))"
using True part2[symmetric]
by (simp add: map_map_partition_by[symmetric] map_zip_fun push_map_inside)
(smt inner(2) atLeastLessThan_iff map_eq_conv map_nth set_upt)
ultimately show ?thesis using True by blast
next
case False
thus ?thesis using term_mctxt[of f ts] term_mctxt[of g ss] by fastforce
qed
qed
qed
lemma gtt_accept_exI:
assumes "gtt_accept 𝒢 s t"
shows "∃ u. u |∈| ta_der' (fst 𝒢) (term_of_gterm s) ∧ u |∈| ta_der' (snd 𝒢) (term_of_gterm t)" using assms
proof (induction)
case (refl t)
then show ?case using ta_der'_refl by blast
next
case (join q s t)
then show ?case
by (metis gta_der_def ta_der_to_ta_der')
next
case (ctxt ss ts f)
then have inner: "∃ us. length us = length ss ∧
(∀i < length ss. (us ! i) |∈| ta_der' (fst 𝒢) (term_of_gterm (ss ! i)) ∧
(us ! i) |∈| ta_der' (snd 𝒢) (term_of_gterm (ts ! i)))"
using Ex_list_of_length_P[of "length ss" "λ u i. u |∈| ta_der' (fst 𝒢) (term_of_gterm (ss ! i)) ∧
u |∈| ta_der' (snd 𝒢) (term_of_gterm (ts ! i))"]
by auto
then obtain us where "length us = length ss ∧ (∀i < length ss.
(us ! i) |∈| ta_der' (fst 𝒢) (term_of_gterm (ss ! i)) ∧ (us ! i) |∈| ta_der' (snd 𝒢) (term_of_gterm (ts ! i)))"
by blast
then have "Fun f us |∈| ta_der' (fst 𝒢) (Fun f (map term_of_gterm ss)) ∧
Fun f us |∈| ta_der' (snd 𝒢) (Fun f (map term_of_gterm ts))" using ctxt(1) by fastforce
then show ?case by (metis term_of_gterm.simps)
qed
lemma agtt_lang_mono:
assumes "rules (fst 𝒢) |⊆| rules (fst 𝒢')" "eps (fst 𝒢) |⊆| eps (fst 𝒢')"
"rules (snd 𝒢) |⊆| rules (snd 𝒢')" "eps (snd 𝒢) |⊆| eps (snd 𝒢')"
shows "agtt_lang 𝒢 ⊆ agtt_lang 𝒢'"
using fsubsetD[OF ta_der_mono[OF assms(1, 2)]] ta_der_mono[OF assms(3, 4)]
by (auto simp: agtt_lang_def gta_der_def dest!: fsubsetD[OF ta_der_mono[OF assms(1, 2)]] fsubsetD[OF ta_der_mono[OF assms(3, 4)]])
lemma gtt_accept_mono:
assumes "rules (fst 𝒢) |⊆| rules (fst 𝒢')" "eps (fst 𝒢) |⊆| eps (fst 𝒢')"
"rules (snd 𝒢) |⊆| rules (snd 𝒢')" "eps (snd 𝒢) |⊆| eps (snd 𝒢')"
"gtt_accept 𝒢 s t"
shows "gtt_accept 𝒢' s t"
using ta_der_mono[OF assms(1, 2)] ta_der_mono[OF assms(3, 4)]
using assms(5) unfolding gtt_accept_equiv
by (auto simp: gta_der_def elim!: gtt_accept'.cases intro!: mctxt) (meson fin_mono)
definition fmap_states_gtt where
"fmap_states_gtt f ≡ map_both (fmap_states_ta f)"
lemma ground_map_vars_term_simp:
"ground t ⟹ map_term f g t = map_term f (λ_. undefined) t"
by (induct t) auto
lemma ground_map_vars_mctxt_simp:
"ground_mctxt C ⟹ map_vars_mctxt f C = map_vars_mctxt (λ_. undefined) C"
by (induct C) auto
lemma states_fmap_states_gtt [simp]:
"gtt_states (fmap_states_gtt f 𝒢) = f |`| gtt_states 𝒢"
by (simp add: fimage_funion gtt_states_def fmap_states_gtt_def)
lemma agtt_lang_fmap_states_gtt:
assumes "finj_on f (gtt_states 𝒢)"
shows "agtt_lang (fmap_states_gtt f 𝒢) = agtt_lang 𝒢" (is "?Ls = ?Rs")
proof -
from assms have inj: "finj_on f (𝒬 (fst 𝒢) |∪| 𝒬 (snd 𝒢))" "finj_on f (𝒬 (fst 𝒢))" "finj_on f (𝒬 (snd 𝒢))"
by (auto simp: gtt_states_def finj_on_fUn)
then have "?Ls ⊆ ?Rs" using ta_der_fmap_states_inv_superset[OF _ inj(1)]
by (auto simp: agtt_lang_def gta_der_def fmap_states_gtt_def)
moreover have "?Rs ⊆ ?Ls"
by (auto simp: agtt_lang_def gta_der_def fmap_states_gtt_def elim!: ta_der_to_fmap_states_der)
ultimately show ?thesis by blast
qed
lemma agtt_lang_Inl_Inr_states_agtt:
"agtt_lang (fmap_states_gtt Inl 𝒢) = agtt_lang 𝒢"
"agtt_lang (fmap_states_gtt Inr 𝒢) = agtt_lang 𝒢"
by (auto simp: finj_Inl_Inr intro!: agtt_lang_fmap_states_gtt)
lemma gtt_lang_fmap_states_gtt:
assumes "finj_on f (gtt_states 𝒢)"
shows "gtt_lang (fmap_states_gtt f 𝒢) = gtt_lang 𝒢" (is "?Ls = ?Rs")
unfolding fmap_states_gtt_def
proof (intro set_eqI iffI, goal_cases lr rl)
case (lr x)
obtain C ss ts where x: "x = (fill_gholes C ss, fill_gholes C ts)"
"length ss = num_gholes C" "length ts = num_gholes C"
"⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fmap_states_ta f (fst 𝒢)) (ss ! i) ∧
q |∈| gta_der (fmap_states_ta f (snd 𝒢)) (ts ! i)"
using lr by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
{ fix i assume i: "i < num_gholes C"
obtain q where q: "q |∈| gta_der (fmap_states_ta f (fst 𝒢)) (ss ! i)"
"q |∈| gta_der (fmap_states_ta f (snd 𝒢)) (ts ! i)" using x(4)[OF i] by blast
then have "the_finv_into (gtt_states 𝒢) f q |∈| gta_der (fst 𝒢) (ss ! i) ∧
the_finv_into (gtt_states 𝒢) f q |∈| gta_der (snd 𝒢) (ts ! i)"
using assms by (simp add: gta_der_def gtt_states_def ta_der_fmap_states_inv_superset)
then have "∃ p. p |∈| gta_der (fst 𝒢) (ss ! i) ∧ p |∈| gta_der (snd 𝒢) (ts ! i)"
using assms by blast}
then have "gtt_accept' 𝒢 (fill_gholes C ss) (fill_gholes C ts)"
using x(2,3) by (auto simp: adapt_vars_def map_vars_term_fill_holes)
then show ?case using x
by (simp add: gtt_accept_equiv)
next
case (rl x)
obtain C ss ts where x: "x = (fill_gholes C ss, fill_gholes C ts)"
"length ss = num_gholes C" "length ts = num_gholes C"
"⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
using rl by (auto 0 0 simp: gtt_accept_equiv image_def elim!: gtt_accept'.cases)
from x(4) obtain qs where qs: "qs i |∈| gta_der (fst 𝒢) (ss ! i) ∧ qs i |∈| gta_der (snd 𝒢) (ts ! i)"
if "i < num_gholes C" for i by metis
have "gtt_accept' (fmap_states_gtt f 𝒢) (fst x) (snd x)"
using gtt_accept'.intros[of ss ts C "fmap_states_gtt f 𝒢"] x
using ta_der_fmap_states_ta[OF conjunct1[OF qs, unfolded gta_der_def], where h = f]
using ta_der_fmap_states_ta[OF conjunct2[OF qs, unfolded gta_der_def], where h = f]
by (metis fmap_states_gtt_def fst_map_prod gta_der_def map_vars_term_term_of_gterm prod.sel(1, 2) snd_map_prod)
then show ?case using x by (auto simp: gtt_accept_equiv fmap_states_gtt_def)
qed
definition gtt_only_reach where
"gtt_only_reach = map_both ta_only_reach"
lemma gtt_only_reach_lang:
"gtt_lang (gtt_only_reach 𝒢) = gtt_lang 𝒢"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR s t)
then obtain C ss ts qs where
s: "s = fill_gholes C ss" "length ss = num_gholes C" and
t: "t = fill_gholes C ts" "length ts = num_gholes C" and
q: "⋀i. i < num_gholes C ⟹ ∃ q. q |∈| gta_der (fst (gtt_only_reach 𝒢)) (ss ! i) ∧
q |∈| gta_der (snd (gtt_only_reach 𝒢)) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "∃ q . q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)" if "i < num_gholes C" for i
using q[of i] that
by (auto simp: gta_der_def gtt_only_reach_def simp flip: ta_der_gterm_only_reach)
then show ?case using s t by (auto simp: gtt_accept_equiv)
next
case (RL s t)
then obtain C ss ts qs where
s: "s = fill_gholes C ss" "length ss = num_gholes C" and
t: "t = fill_gholes C ts" "length ts = num_gholes C" and
q: "⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "∃ q. q |∈| gta_der (fst (gtt_only_reach 𝒢)) (ss ! i) ∧ q |∈| gta_der (snd (gtt_only_reach 𝒢)) (ts ! i)"
if "i < num_gholes C" for i
using q[of i] that s t
by (auto simp add: gta_der_def gtt_only_reach_def simp flip: ta_der_gterm_only_reach)
then show ?case using s t by (auto simp: gtt_accept_equiv)
qed
lemma gtt_only_reach_syms:
"gtt_syms (gtt_only_reach 𝒢) |⊆| gtt_syms 𝒢"
by (auto simp: gtt_only_reach_def ta_restrict_def ta_sig_def)
definition gtt_only_prod where
"gtt_only_prod 𝒢 = (let iface = gtt_interface 𝒢 in
map_both (ta_only_prod iface) 𝒢)"
lemma gtt_only_prod_lang:
"gtt_lang (gtt_only_prod 𝒢) = gtt_lang 𝒢"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR s t)
then obtain C ss ts qs where
s: "s = fill_gholes C ss" "length ss = num_gholes C" and
t: "t = fill_gholes C ts" "length ts = num_gholes C" and
q: "⋀i. i < num_gholes C ⟹ ∃ q. q |∈| gta_der (fst (gtt_only_prod 𝒢)) (ss ! i) ∧
q |∈| gta_der (snd (gtt_only_prod 𝒢)) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)" if "i < num_gholes C" for i using q[OF that]
by (auto simp: gta_der_def gtt_only_prod_def Let_def intro: ta_der_ta_only_prod_ta_der)
then show ?case using s t by (auto simp: gtt_accept_equiv)
next
case (RL s t)
then obtain C ss ts qs where
s: "s = fill_gholes C ss" "length ss = num_gholes C" and
t: "t = fill_gholes C ts" "length ts = num_gholes C" and
q: "⋀i. i < num_gholes C ⟹ ∃q. q |∈| gta_der (fst 𝒢) (ss ! i) ∧ q |∈| gta_der (snd 𝒢) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
{fix i assume i: "i < num_gholes C"
guess q using q[OF i] by (elim exE conjE) note q = this
have "q |∈| gtt_interface 𝒢" using q
by (simp add: gta_der_def gtt_interface_def)
then have "q |∈| gta_der (fst (gtt_only_prod 𝒢)) (ss ! i)" "q |∈| gta_der (snd (gtt_only_prod 𝒢)) (ts ! i)"
using q
by (auto simp: gta_der_def gtt_only_prod_def Let_def gtt_interface_def ta_der_only_prod ta_productive_setI)
then have "∃q. q |∈| gta_der (fst (gtt_only_prod 𝒢)) (ss ! i) ∧ q |∈| gta_der (snd (gtt_only_prod 𝒢)) (ts ! i)"
by auto}
then show ?case using s t by (auto simp: gtt_accept_equiv)
qed
lemma gtt_only_prod_syms:
"gtt_syms (gtt_only_prod 𝒢) |⊆| gtt_syms 𝒢"
by (auto simp: gtt_only_prod_def ta_restrict_def ta_sig_def Let_def)
definition trim_gtt where
"trim_gtt = gtt_only_prod ∘ gtt_only_reach"
lemma trim_gtt_lang:
"gtt_lang (trim_gtt G) = gtt_lang G"
unfolding trim_gtt_def comp_def gtt_only_prod_lang gtt_only_reach_lang ..
lemma trim_gtt_prod_syms:
"gtt_syms (trim_gtt G) |⊆| gtt_syms G"
unfolding trim_gtt_def using fsubset_trans[OF gtt_only_prod_syms gtt_only_reach_syms] by simp
subsection ‹root-cleanliness›
text ‹A GTT is root-clean if none of its interface states can occur in a non-root positions
in the accepting derivations corresponding to its anchored GTT relation.›
definition ta_nr_states :: "('q, 'f) ta ⇒ 'q fset" where
"ta_nr_states A = |⋃| ((fset_of_list ∘ r_lhs_states) |`| (rules A))"
definition gtt_nr_states where
"gtt_nr_states G = ta_nr_states (fst G) |∪| ta_nr_states (snd G)"
definition gtt_root_clean where
"gtt_root_clean G ⟷ gtt_nr_states G |∩| gtt_interface G = {||}"
subsection ‹Relabeling›
definition relabel_gtt :: "('q :: linorder, 'f) gtt ⇒ (nat, 'f) gtt" where
"relabel_gtt G = fmap_states_gtt (map_fset_to_nat (gtt_states G)) G"
lemma relabel_agtt_lang [simp]:
"agtt_lang (relabel_gtt G) = agtt_lang G"
by (simp add: agtt_lang_fmap_states_gtt map_fset_to_nat_inj relabel_gtt_def)
lemma agtt_lang_sig:
"fset (gtt_syms G) ⊆ ℱ ⟹ agtt_lang G ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
by (auto simp: agtt_lang_def gta_der_def 𝒯⇩G_equivalent_def)
(metis ffunas_gterm.rep_eq less_eq_fset.rep_eq subset_iff ta_der_gterm_sig)+
end