theory GTT
imports TA.Tree_Automata Tree_Automata_Utils Basic_Utils Lift_Root_Step
begin
abbreviation map_both where
"map_both f ≡ map_prod f f"
lemma trancl_map_prod_mono:
"map_both f ` R⇧+ ⊆ (map_both f ` R)⇧+"
proof -
have "(f x, f y) ∈ (map_both f ` R)⇧+" if "(x, y) ∈ R⇧+" for x y using that
by (induct) (auto intro: trancl_into_trancl)
then show ?thesis by auto
qed
lemma trancl_map_both_Restr:
assumes "inj_on f X"
shows "(map_both f ` Restr R X)⇧+ = map_both f ` (Restr R X)⇧+"
proof -
have [simp]:
"map_prod (inv_into X f ∘ f) (inv_into X f ∘ f) ` Restr R X = Restr R X"
using inv_into_f_f[OF assms]
apply (intro equalityI subrelI)
apply (auto simp: comp_def map_prod_def image_def)
apply (metis (no_types, lifting) IntI SigmaI case_prod_conv)
done
have [simp]:
"map_prod (f ∘ inv_into X f) (f ∘ inv_into X f) ` (map_both f ` Restr R X)⇧+ = (map_both f ` Restr R X)⇧+"
using f_inv_into_f[of _ f X] subsetD[OF trancl_mono_set[OF image_mono[of "Restr R X" "X × X" "map_both f"]]]
by (intro equalityI subrelI) (auto simp: map_prod_surj_on trancl_full_on comp_def rev_image_eqI)
show ?thesis using assms trancl_map_prod_mono[of f "Restr R X"]
image_mono[OF trancl_map_prod_mono[of "inv_into X f" "map_both f ` Restr R X"], of "map_both f"]
by (intro equalityI) (simp_all add: image_comp map_prod.comp)
qed
lemmas trancl_map_both = trancl_map_both_Restr[of _ UNIV, unfolded UNIV_Times_UNIV Int_UNIV_right]
lemma map_both_relcomp:
"inj_on f (snd ` A ∪ fst ` B) ⟹ map_both f ` A O map_both f ` B = map_both f ` (A O B)"
by (force simp: inj_on_def intro: rev_image_eqI)
lemma ground_set_map_adapt_vars_dist:
assumes "A ⊆ Collect ground × Collect ground"
and "B ⊆ Collect ground × Collect ground"
shows "(map_both adapt_vars ` A) O (map_both adapt_vars ` B) = map_both adapt_vars ` (A O B)" (is "?L = ?R")
proof
show "?L ⊆ ?R" apply (rule) using assms adapt_vars_inj by blast
next
show "?R ⊆ ?L" apply (rule) using assms adapt_vars_inj by blast
qed
type_synonym ('q, 'f) gtt = "('q, 'f) ta × ('q, 'f) ta"
abbreviation gtt_rules where
"gtt_rules 𝒢 ≡ ta_rules (fst 𝒢) ∪ ta_rules (snd 𝒢)"
abbreviation gtt_eps where
"gtt_eps 𝒢 ≡ ta_eps (fst 𝒢) ∪ ta_eps (snd 𝒢)"
definition gtt_states where
"gtt_states 𝒢 = ta_states (fst 𝒢) ∪ ta_states (snd 𝒢)"
abbreviation gtt_syms where
"gtt_syms 𝒢 ≡ ta_syms (fst 𝒢) ∪ ta_syms (snd 𝒢)"
definition gtt_interface where
"gtt_interface G = ta_states ((fst G)⦇ta_final := {}⦈) ∩ ta_states ((snd G)⦇ta_final := {}⦈)"
inductive gtt_accept :: "('q, 'f) gtt ⇒ ('f, 'q) term ⇒ ('f, 'q) term ⇒ bool" for 𝒢 where
refl [intro]: "gtt_accept 𝒢 t t"
| join [intro]: "q ∈ ta_res (fst 𝒢) s ⟹ q ∈ ta_res (snd 𝒢) t ⟹ gtt_accept 𝒢 s t"
| ctxt [intro]: "length ss = length ts ⟹
∀i < length ss. gtt_accept 𝒢 (ss ! i) (ts ! i) ⟹
gtt_accept 𝒢 (Fun f ss) (Fun f ts)"
hide_fact (open) refl
inductive gtt_accept' :: "('q, 'f) gtt ⇒ ('f, 'q) term ⇒ ('f, 'q) term ⇒ bool"
for 𝒢 where
mctxt [intro]: "length ss = length ts ⟹ num_holes C = length ss ⟹
∀i < length ts. ∃q. q ∈ ta_res (fst 𝒢) (ss ! i) ∧ q ∈ ta_res (snd 𝒢) (ts ! i) ⟹
gtt_accept' 𝒢 (fill_holes C ss) (fill_holes C ts)"
text ‹language accepted by a GTT›
abbreviation gtt_lang :: "('q, 'f) gtt ⇒ ('f, 'q) term rel" where
"gtt_lang 𝒢 ≡ Restr {(s, t). gtt_accept 𝒢 s t} {t. ground t}"
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_res (fst 𝒢) t ∧ q ∈ gta_res (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_lang_from_agtt_lang:
"gtt_lang G = map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang G)"
proof -
{ fix s t assume st: "gtt_accept G s t" "ground s" "ground t"
then have *: "(gterm_of_term s, gterm_of_term t) ∈ {aps_step a |a. a ∈ annotated_parallel_closure UNIV (agtt_lang G)}"
proof (induct s t)
case (refl t) then show ?case
by (auto intro: exI[of "λa. _ a ∧ a ∈ _", OF conjI, OF _ empty_aps])
next
case (join q s t) then show ?case
by (auto simp: agtt_lang_def gta_res_def intro!: exI[of "λa. _ a ∧ a ∈ _", OF conjI, OF _ aps_root_step])
next
case (ctxt ss ts f)
have "∃a. a ∈ annotated_parallel_closure UNIV (agtt_lang G) ∧
aps_step a = (gterm_of_term (ss ! i), gterm_of_term (ts ! i))" if "i < length ss" for i
using ctxt that by (auto 0 3)
then obtain as where "as i ∈ annotated_parallel_closure UNIV (agtt_lang G)"
"aps_step (as i) = (gterm_of_term (ss ! i), gterm_of_term (ts ! i))" if "i < length ss" for i
by metis
then show ?case using ctxt(1) by (auto intro!: nth_equalityI
exI[of "λa. _ a ∧ a ∈ _", OF conjI, OF _ aps_non_root_step[of f _ _ "map as [0..<length ss]"]])
qed
have "(s, t) ∈ map_both term_of_gterm ` {aps_step a |a. a ∈ annotated_parallel_closure UNIV (agtt_lang G)}"
using st(2,3) by (auto intro!: image_eqI[OF _ *]) }
moreover
{ fix s t p assume "p ∈ annotated_parallel_closure UNIV (agtt_lang G)" "(s, t) = aps_step p"
then have "gtt_accept G (term_of_gterm s) (term_of_gterm t)"
by (induct p arbitrary: s t) (auto simp: agtt_lang_def gta_res_def) }
ultimately show ?thesis by (auto simp: lift_root_step_def)
qed
lemma gtt_accept'_refl [simp]:
"gtt_accept' 𝒢 t t"
proof -
have "gtt_accept' 𝒢 (fill_holes (mctxt_of_term t) [])
(fill_holes (mctxt_of_term t) [])" by fastforce
thus ?thesis by simp
qed
lemma gtt_accept'_join[simp]:
assumes "q ∈ ta_res (fst 𝒢) s" "q ∈ ta_res (snd 𝒢) t"
shows "gtt_accept' 𝒢 s t"
proof -
have "gtt_accept' 𝒢 (fill_holes MHole [s]) (fill_holes MHole [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 = fill_holes C ss) ∧ (t = fill_holes C ts) ∧
(length ss = length ts) ∧ (num_holes C = length ss ) ∧
(∀i < length ts. ∃q. q ∈ ta_res (fst 𝒢) (ss ! i) ∧
q ∈ ta_res (snd 𝒢) (ts ! i))"
using assms by (auto elim!: gtt_accept'.cases)
lemma gtt_accept_equiv:
"gtt_accept 𝒢 s t ⟷ gtt_accept' 𝒢 s t"
proof (rule iffI)
assume "gtt_accept 𝒢 s t"
thus "gtt_accept' 𝒢 s t"
proof (induction rule: gtt_accept.induct)
case (ctxt ss ts f)
let ?Prop = "λx i. ∃C ss' ts'. x = (C, (ss', ts')) ∧ length ss' = length ts' ∧
(num_holes C = length ss') ∧
(ss ! i = fill_holes C ss') ∧ (ts ! i = fill_holes C ts') ∧
(∀j < length ts'. ∃q. q ∈ ta_res (fst 𝒢) (ss' ! j) ∧
q ∈ ta_res (snd 𝒢) (ts' ! j)) ∧
gtt_accept' 𝒢 (fill_holes C ss') (fill_holes C ts')"
{ fix i
assume "i < length ss"
hence "gtt_accept' 𝒢 (ss ! i) (ts ! i)" using ctxt(2) by blast
hence "∃x C ss' ts'. x = (C, (ss', ts')) ∧ length ss' = length ts' ∧
(num_holes C = length ss') ∧
(ss ! i = fill_holes C ss') ∧ (ts ! i = fill_holes C ts') ∧
(∀j < length ts'. ∃q. q ∈ ta_res (fst 𝒢) (ss' ! j) ∧
q ∈ ta_res (snd 𝒢) (ts' ! j)) ∧
gtt_accept' 𝒢 (fill_holes C ss') (fill_holes C ts')"
by (auto elim!: gtt_accept'.cases)
} note inner = this
then obtain xs where xs: "length xs = length ss ∧ (∀i<length ss. ?Prop (xs ! i) i)"
using construct_exI'[of "length ss" ?Prop] by blast
hence ss_i_ts_i:
"∀i<length xs. ss ! i = fill_holes ((map fst xs) ! i) ((map (fst ∘ snd) xs) ! i) ∧
ts ! i = fill_holes ((map fst xs) ! i) ((map (snd ∘ snd) xs) ! i) ∧
num_holes ((map fst xs) ! i) = length ((map (fst ∘ snd) xs) ! i) ∧
num_holes ((map fst xs) ! i) = length ((map (snd ∘ snd) xs) ! i)"
by (smt comp_apply fst_conv length_map map_nth nth_map snd_conv)
define ss' ts' where ss': "ss' = concat (map (fst ∘ snd) xs)" and
ts': "ts' = concat (map (snd ∘ snd) xs)"
hence lengths_eq: "length ss' = length ts'" using ss_i_ts_i
by (metis (no_types, lifting) eq_length_concat_nth length_map)
have map_eq: "map (num_holes ∘ fst) xs = map (length ∘ (fst ∘ snd)) xs"
using ss_i_ts_i by (metis (no_types, lifting) List.map.compositionality map_eq_conv')
hence num_holes: "num_holes (MFun f (map fst xs)) = length ss'"
using ss' ts' by (auto simp: length_concat nth_map[of _ xs] map_eq)
have "∀i<length xs. ∀j < length ((map (snd ∘ snd) xs) ! i).
∃q. q ∈ ta_res (fst 𝒢) (((map (fst ∘ snd) xs) ! i) ! j) ∧
q ∈ ta_res (snd 𝒢) (((map (snd ∘ snd) xs) ! i) ! j)"
using xs by (smt comp_apply fst_conv length_map map_nth nth_map snd_conv)
hence join_state: "∀j < length ts'. ∃q. q ∈ ta_res (fst 𝒢) (ss' ! j) ∧
q ∈ ta_res (snd 𝒢) (ts' ! j)"
using ss_i_ts_i
unfolding ss' ts' by (smt length_map nth_concat_two_lists ss_i_ts_i)
have "i < length (map (num_holes ∘ fst) xs) ⟹
length (map (fst ∘ snd) xs ! i) = map (num_holes ∘ fst) xs ! i" for i
using ss_i_ts_i by fastforce
hence f_ss: "Fun f ss = fill_holes (MFun f (map fst xs)) ss'"
using xs ss_i_ts_i partition_by_concat_id[of "map (fst ∘ snd) xs" "map (num_holes ∘ fst) xs"]
unfolding ss' by simp (smt atLeastLessThan_iff map_eq_conv map_nth set_upt ss_i_ts_i)
have "i < length (map (num_holes ∘ fst) xs) ⟹
length (map (snd ∘ snd) xs ! i) = map (num_holes ∘ fst) xs ! i" for i
using ss_i_ts_i by fastforce
hence f_ts: "Fun f ts = fill_holes (MFun f (map fst xs)) ts'"
using xs ss_i_ts_i partition_by_concat_id[of "map (snd ∘ snd) xs" "map (num_holes ∘ fst) xs"]
unfolding ss' ts' ‹length ss = length ts›
by simp (smt atLeastLessThan_iff map_eq_conv map_nth set_upt ss_i_ts_i)
show ?case using join_state lengths_eq num_holes unfolding f_ss f_ts
by (intro gtt_accept'.intros) auto
qed auto
next
assume "gtt_accept' 𝒢 s t"
thus "gtt_accept 𝒢 s t"
proof (induction rule: gtt_accept'.induct)
case (mctxt ss ts C) thus ?case
proof (induction C arbitrary: ss ts)
case MHole
then obtain s' t' where "ss = [s']" "ts = [t']" by (cases ss; cases ts) fastforce+
thus ?case using MHole(3) by auto
next
case (MFun f Cs)
moreover { fix i
assume asm: "i < length Cs"
hence lengths_eq: "length (partition_holes ss Cs ! i) = length (partition_holes ts Cs ! i)"
using MFun(2,3) by auto
have num_holes_length: "num_holes (Cs ! i) = length (partition_holes ss Cs ! i)"
using asm MFun(3) by auto
have join: "∀j<length (partition_holes ts Cs ! i).
∃q. q ∈ ta_res (fst 𝒢) ((partition_holes ss Cs ! i) ! j) ∧
q ∈ ta_res (snd 𝒢) ((partition_holes ts Cs ! i) ! j)"
using MFun(2,3,4)
by (smt asm length_map lengths_eq nth_map num_holes.simps(3) num_holes_length
partition_by_nth_nth)
have "gtt_accept 𝒢 (fill_holes (Cs ! i) (partition_holes ss Cs ! i))
(fill_holes (Cs ! i) (partition_holes ts Cs ! i))"
using asm MFun(1)[OF _ lengths_eq num_holes_length join] by auto
}
ultimately show ?case using length_upt[of 0 "length Cs"] unfolding fill_holes.simps
by (intro gtt_accept.intros(3)) auto
qed auto
qed
qed
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 accept'_closed_ctxt:
assumes "length ss = length ts"
and "∀i < length ts. gtt_accept' 𝒢 (ss ! i) (ts ! i)"
and "num_holes C = length ss"
shows "gtt_accept' 𝒢 (fill_holes C ss) (fill_holes C ts)"
using assms
proof (induction C arbitrary: ss ts)
case (MVar x)
then show ?case by auto
next
case MHole
then show ?case
by (metis One_nat_def fill_holes_MHole lessI num_holes.simps(2))
next
case (MFun f Cs)
let ?sss = "(partition_holes ss Cs)"
let ?tss = "(partition_holes ts Cs)"
obtain Css Cts where Css_Cts:"fill_holes (MFun f Cs) ss = Fun f Css"
"fill_holes (MFun f Cs) ts = Fun 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) MFun by simp
moreover have "num_holes (Cs ! i) = length (?sss ! i)" using assms(2) loc_asm MFun by force
moreover have "∀j < length (?tss ! i). gtt_accept' 𝒢 ((?sss ! i) ! j) ((?tss ! i) ! j)"
using loc_asm MFun assms(3) by (metis calculation(1) calculation(2) length_map nth_map
num_holes.simps(3) partition_by_nth_nth(1) partition_by_nth_nth(2))
ultimately have "gtt_accept' 𝒢 (fill_holes (Cs ! i) (?sss ! i)) (fill_holes (Cs ! i) (?tss ! i))"
using MFun(1) loc_asm by force
hence "gtt_accept 𝒢 (fill_holes (Cs!i) (?sss!i)) (fill_holes (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 𝒢 (Fun f Css) (Fun f Cts)" using Css_Cts(3) by auto
then show ?case using gtt_accept_equiv Css_Cts by metis
qed
lemma ta_res'_id:
"t ∈ ta_res' 𝒜 t"
by (induction t) auto
lemma ta_res_res'_inclusion:
fixes q 𝒜 l
shows "(q ∈ ta_res 𝒜 l) ⟶ Var q ∈ ta_res' 𝒜 l"
by (induction "𝒜" "l" rule: ta_res.induct) fastforce+
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 mctxt_of_term.simps(2) term_of_mctxt_mctxt_of_term_id)
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" "ground s" "ground t"
shows "∃u. u ∈ ta_res' (fst 𝒢) s ∧ u ∈ ta_res' (snd 𝒢) t"
using assms
proof (induction)
case (refl t)
thus ?case using ta_res'_id by blast
next
case (join q s t)
thus ?case using ta_res_res'_inclusion by fast
next
case (ctxt ss ts f)
{ fix i
assume asm: "i < length ss"
hence "ground (ts ! i)" "ground (ss ! i)" using ctxt by auto
hence "gtt_accept 𝒢 (ss ! i) (ts ! i)"
"∃u⇩i. u⇩i ∈ ta_res' (fst 𝒢) (ss ! i) ∧ u⇩i ∈ ta_res' (snd 𝒢) (ts ! i)"
using asm ctxt(1,2) by blast+
hence "∃us. (us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i)"
using asm by (metis nth_list_update_eq)
}
hence inner: "∀i < length ss.
∃us. (us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i)"
by auto
have "∃us. length us = length ss ∧ (∀i < length ss.
(us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i))"
using construct_exI[OF inner] by auto
then obtain us where "length us = length ss ∧ (∀i < length ss.
(us ! i) ∈ ta_res' (fst 𝒢) (ss ! i) ∧ (us ! i) ∈ ta_res' (snd 𝒢) (ts ! i))"
by blast
hence "Fun f us ∈ ta_res' (fst 𝒢) (Fun f ss) ∧
Fun f us ∈ ta_res' (snd 𝒢) (Fun f ts)" using ctxt(1) by fastforce
thus ?case by blast
qed
lemma ta_res_stable:
assumes "q ∈ ta_res 𝒜 t" "ta_rules 𝒜 ⊆ ta_rules 𝒜'" "ta_eps 𝒜 ⊆ ta_eps 𝒜'"
shows "q ∈ ta_res 𝒜' t"
by (metis assms subsetD[OF ta_res_mono'])
lemma gtt_accept_mono:
assumes "ta_eps (fst 𝒢) ⊆ ta_eps (fst 𝒢')" "ta_rules (fst 𝒢) ⊆ ta_rules (fst 𝒢')"
"ta_eps (snd 𝒢) ⊆ ta_eps (snd 𝒢')" "ta_rules (snd 𝒢) ⊆ ta_rules (snd 𝒢')"
"gtt_accept 𝒢 s t"
shows "gtt_accept 𝒢' s t"
using assms(5) unfolding gtt_accept_equiv
by (elim gtt_accept'.cases) (metis gtt_accept'.intros assms(1-4) subsetD[OF ta_res_mono'])
lemma agtt_lang_mono:
assumes "ta_eps (fst 𝒢) ⊆ ta_eps (fst 𝒢')" "ta_rules (fst 𝒢) ⊆ ta_rules (fst 𝒢')"
"ta_eps (snd 𝒢) ⊆ ta_eps (snd 𝒢')" "ta_rules (snd 𝒢) ⊆ ta_rules (snd 𝒢')"
shows "agtt_lang 𝒢 ⊆ agtt_lang 𝒢'"
by (auto simp: agtt_lang_def gta_res_def dest: subsetD[OF ta_res_mono'[OF assms(1,2)]] subsetD[OF ta_res_mono'[OF assms(3,4)]])
lemma ta_res_ta_final_ignored:
assumes "q ∈ ta_res (ta.make Q⇩f Δ ℰ) t"
shows "q ∈ ta_res (ta.make Q⇩f' Δ ℰ) t"
using assms(1) unfolding ta.make_def
proof (induction "⦇ta_final = Q⇩f, ta_rules = Δ, ta_eps = ℰ⦈" t arbitrary: q rule: ta_res.induct)
case (2 f ts)
obtain q' qs where accepted_Δ: "f qs → q' ∈ Δ" "(q', q) ∈ ℰ⇧*" "length qs = length ts"
"∀i<length ts. qs ! i ∈ ta_res ⦇ta_final = Q⇩f, ta_rules = Δ, ta_eps = ℰ⦈ (ts ! i)"
using 2(2) by auto
moreover have "∀i<length ts. qs ! i ∈ ta_res ⦇ta_final = Q⇩f', ta_rules = Δ, ta_eps = ℰ⦈ (ts ! i)"
using 2(1) accepted_Δ(4) by auto
ultimately show ?case using accepted_Δ(1-3) by auto
qed simp
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: image_Un gtt_states_def fmap_states_gtt_def)
lemma agtt_lang_fmap_states_gtt:
assumes "inj_on f (gtt_states 𝒢)"
shows "agtt_lang (fmap_states_gtt f 𝒢) = agtt_lang 𝒢"
unfolding agtt_lang_def gta_res_def fst_map_prod snd_map_prod fmap_states_gtt_def
proof ((intro equalityI subsetI CollectI; elim CollectE exE conjE), goal_cases LR RL)
case (LR x t u q) note [simp] = LR(1)
show ?case using assms
ta_res_fmap_states_inv[of _ _ "term_of_gterm _", unfolded adapt_vars_term_of_gterm, OF _ _ LR(2)]
ta_res_fmap_states_inv[of _ _ "term_of_gterm _", unfolded adapt_vars_term_of_gterm, OF _ _ LR(3)]
apply (auto simp: gtt_states_def)
by (smt ground_term_of_gterm inj_onD inj_on_Un subsetCE sup_ge1 sup_ge2 ta_res_states)
next
case (RL x t u q) note [simp] = RL(1)
show ?case using assms
RL(2,3)[THEN ta_res_fmap_states_ta, of f, unfolded map_vars_term_term_of_gterm] by auto
qed
lemma gtt_lang_fmap_states_gtt:
assumes "inj_on f (gtt_states 𝒢)"
shows "gtt_lang (fmap_states_gtt f 𝒢) = map_both adapt_vars ` gtt_lang 𝒢"
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_holes C ss, fill_holes C ts)"
"length ss = num_holes C" "length ts = num_holes C"
"⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fmap_states_ta f (fst 𝒢)) (ss ! i) ∧
q ∈ ta_res (fmap_states_ta f (snd 𝒢)) (ts ! i)"
"ground (fill_holes C ss)" "ground (fill_holes C ts)"
using lr by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
{ fix i assume i: "i < num_holes C"
obtain q where q: "q ∈ ta_res (fmap_states_ta f (fst 𝒢)) (ss ! i)"
"q ∈ ta_res (fmap_states_ta f (snd 𝒢)) (ts ! i)" using x(4)[OF i] by blast
have g: "ground (ss ! i)" "ground (ts ! i)" using x(2,3,5,6) by (auto simp: ground_fill_holes i)
then have "∃p. p ∈ ta_res (fst 𝒢) (adapt_vars (ss ! i)) ∧ p ∈ ta_res (snd 𝒢) (adapt_vars (ts ! i))"
using assms[unfolded inj_on_Un gtt_states_def] x(2,3,5,6) q
ta_res_fmap_states_inv[of f "fst 𝒢" "ss ! i" q] ta_res_fmap_states_inv[of f "snd 𝒢" "ts ! i" q]
inj_onD[OF assms[unfolded gtt_states_def] _ UnI1[OF subsetD[OF ta_res_states]] UnI2[OF subsetD[OF ta_res_states]],
of _ _ "adapt_vars (ss ! i)" "adapt_vars (ts ! i)"]
by (auto) }
then have "gtt_accept' 𝒢 (adapt_vars (fill_holes C ss)) (adapt_vars (fill_holes C ts))"
using x(2,3) by (auto simp: adapt_vars_def map_vars_term_fill_holes)
then show ?case using x(1,5,6) by (auto 0 0 simp: image_def prod.map_comp gtt_accept_equiv
intro!: bexI[of _ "map_prod adapt_vars adapt_vars x"])
next
case (rl x)
obtain C ss ts where x: "x = (adapt_vars (fill_holes C ss), adapt_vars (fill_holes C ts))"
"length ss = num_holes C" "length ts = num_holes C"
"⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst 𝒢) (ss ! i) ∧ q ∈ ta_res (snd 𝒢) (ts ! i)"
"ground (fill_holes C ss)" "ground (fill_holes C ts)"
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 ∈ ta_res (fst 𝒢) (ss ! i) ∧ qs i ∈ ta_res (snd 𝒢) (ts ! i)"
if "i < num_holes C" for i by metis
have "gtt_accept' (fmap_states_gtt f 𝒢) (fst x) (snd x)"
using gtt_accept'.intros[of "map (map_vars_term f) ss" "map (map_vars_term f) ts"
"map_vars_mctxt f C" "fmap_states_gtt f 𝒢"] x(2,3,5,6)
ta_res_fmap_states_ta[OF conjunct1[OF qs], where h = f]
ta_res_fmap_states_ta[OF conjunct2[OF qs], where h = f]
by (auto simp: map_vars_term_fill_holes x(1) adapt_vars_def ground_fill_holes fmap_states_gtt_def
ground_map_vars_term_simp[of _ _ f] ground_map_vars_mctxt_simp[of _ f]
cong: map_cong)
then show ?case using x(1,2,3,5,6) 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 G) = gtt_lang G"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR s t)
then obtain C ss ts qs where
s: "s = fill_holes C ss" "length ss = num_holes C" "ground s" and
t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst (gtt_only_reach G)) (ss ! i) ∧
q ∈ ta_res (snd (gtt_only_reach G)) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)" if "i < num_holes C" for i
using q[of i] subsetD[OF ta_res_mono[OF ta_restrict_subset]] that by (fastforce simp: gtt_only_reach_def)
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_holes C ss" "length ss = num_holes C" "ground s" and
t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "∃q. q ∈ ta_res (fst (gtt_only_reach G)) (ss ! i) ∧ q ∈ ta_res (snd (gtt_only_reach G)) (ts ! i)"
if "i < num_holes C" for i
using q[of i] ta_res_only_reach[OF refl, of "ss ! i" "fst G", THEN conjunct2]
ta_res_only_reach[OF refl, of "ts ! i" "snd G", THEN conjunct2] that s t
by (simp add: ground_fill_holes all_set_conv_all_nth)
(auto simp: ground_vars_term_empty set_conv_nth gtt_only_reach_def)
then show ?case using s t by (auto simp: gtt_accept_equiv)
qed
lemma gtt_only_reach_syms:
"gtt_syms (gtt_only_reach G) ⊆ gtt_syms G"
by (auto simp: gtt_only_reach_def ta_restrict_def)
(metis (mono_tags, lifting) image_iff mem_Collect_eq select_convs(2) ta_syms_def)+
definition gtt_only_prod where
"gtt_only_prod G =
(let iface = gtt_interface G in
map_both ta_only_prod ((fst G)⦇ta_final := iface⦈, (snd G)⦇ta_final := iface⦈))"
lemma gtt_only_prod_lang:
"gtt_lang (gtt_only_prod G) = gtt_lang G"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR s t)
then obtain C ss ts qs where
s: "s = fill_holes C ss" "length ss = num_holes C" "ground s" and
t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst (gtt_only_prod G)) (ss ! i) ∧
q ∈ ta_res (snd (gtt_only_prod G)) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)" if "i < num_holes C" for i
using q[of i] subsetD[OF ta_res_mono'[of "fst (gtt_only_prod G)" "fst G"]]
subsetD[OF ta_res_mono'[of "snd (gtt_only_prod G)" "snd G"]] that
ta_restrict_subset[of "_⦇ ta_final := _ ⦈"]
by (fastforce simp: gtt_only_prod_def Let_def ta_subset_def)
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_holes C ss" "length ss = num_holes C" "ground s" and
t: "t = fill_holes C ts" "length ts = num_holes C" "ground t" and
q: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)"
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
let ?iface = "ta_states (fst G⦇ta_final := {}⦈) ∩ ta_states (snd G⦇ta_final := {}⦈)"
{ fix i assume i: "i < num_holes C"
guess q using q[OF i] by (elim exE conjE) note q = this
have g: "ground (ss ! i)" "ground (ts ! i)" using s t i by (auto simp: ground_fill_holes)
have "q ∈ ?iface" using q g
subset_trans[OF ta_res_mono'[of A "A⦇ta_final := {}⦈" for A] ta_res_states[of _ "_⦇ta_final := {} ⦈"], THEN subsetD]
by fastforce
have "q ∈ ta_res (fst (gtt_only_prod G)) (ss ! i)" "q ∈ ta_res (snd (gtt_only_prod G)) (ts ! i)"
using q g by (auto simp: gtt_only_prod_def Let_def gtt_interface_def intro!: ta_productive_final
ta_res_only_prod subsetD[OF ta_res_mono'[of A "A⦇ta_final := ?iface⦈" for A]]
subset_trans[OF ta_res_mono'[of A "A⦇ta_final := {}⦈" for A] ta_res_states[of _ "_⦇ta_final := {} ⦈"], THEN subsetD])
then have "∃q. q ∈ ta_res (fst (gtt_only_prod G)) (ss ! i) ∧ q ∈ ta_res (snd (gtt_only_prod G)) (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 G) ⊆ gtt_syms G"
by (auto simp: gtt_only_prod_def ta_restrict_def)
(smt fst_conv snd_conv image_iff mem_Collect_eq select_convs(2) ta_syms_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 subset_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 set" where
"ta_nr_states A = ⋃{set qs |f qs q. f qs → q ∈ ta_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_set_to_nat (gtt_states G)) G"
lemma relabel_agtt_lang [simp]:
"finite (gtt_states G) ⟹ agtt_lang (relabel_gtt G) = agtt_lang G"
by (simp add: agtt_lang_fmap_states_gtt map_set_to_nat_inj relabel_gtt_def)
lemma finite_relabel_gtt [simp]:
"finite (gtt_states A) ⟹ finite (gtt_states (relabel_gtt A))"
by (simp add: relabel_gtt_def gtt_states_def fmap_states_gtt_def)
lemma agtt_lang_sig:
"gtt_syms G ⊆ ℱ ⟹ agtt_lang G ⊆ {t. funas_gterm t ⊆ ℱ} × {t. funas_gterm t ⊆ ℱ}"
by (auto simp: agtt_lang_def gta_res_def dest: subset_trans[OF ta_syms_res, of _ _ "term_of_gterm _" ℱ, unfolded funas_term_of_gterm_conv])
end