theory TA_Clousure_Const
imports TR.Tree_Automata GR.Ground_mctxt
begin
lemma sum_list_length1:
assumes "sum_list ts = (1 :: nat)"
shows "∃ i < length ts. ts ! i = 1 ∧ (∀ j < length ts. i ≠ j ⟶ ts ! j = 0)" using assms
proof (induct ts)
case (Cons a ts) then show ?case
by (cases a, auto simp: nth_Cons')
qed auto
lemma vars_term_list_fill_holes [simp]:
assumes "ground_mctxt C" and "num_holes C = length xs"
shows "vars_term_list (fill_holes C (map Var xs)) = xs"
using split_vars_ground_vars[OF assms] split_vars_vars_term_list
by (metis snd_conv)
lemma ground_vars_term_list [simp]:
"ground t ⟹ vars_term_list t = []"
by (induct t) (auto simp: vars_term_list.simps)
lemma ground_ctxt_vars_term_list [simp]:
"ground_ctxt C ⟹ vars_term_list C⟨t⟩ = vars_term_list t"
proof (induct C)
case (More f ts C us)
have [simp]: "concat (map vars_term_list ts) = []" "concat (map vars_term_list us) = []"
using More(2) by auto
show ?case using More(1, 2)
by (auto simp: vars_term_list.simps)
qed (auto)
locale derivation_split =
fixes A :: "('q, 'f) ta" and Δ⇩A :: "('q, 'f) ta_rule fset" and Δ⇩B and Δ⇩ℰ⇩A and Δ⇩ℰ⇩B and Δ⇩ℰ⇩A⇩B
assumes rule_split: "rules A = Δ⇩A |∪| Δ⇩B"
and eps_split: "eps A = Δ⇩ℰ⇩A |∪| Δ⇩ℰ⇩A⇩B |∪| Δ⇩ℰ⇩B"
and st_split: "(rule_states Δ⇩A |∪| eps_states Δ⇩ℰ⇩A) |∩| (eps_states Δ⇩ℰ⇩B |∪| rule_states Δ⇩B) = {||}"
and eps_AB_trans: "Δ⇩ℰ⇩A⇩B |⊆| (rule_states Δ⇩A |∪| eps_states Δ⇩ℰ⇩A) |×| (rule_states Δ⇩B |∪| eps_states Δ⇩ℰ⇩B)"
begin
"𝒜 ≡ TA Δ_A Δ_ℰ_A"">abbreviation "𝒜 ≡ TA Δ⇩A Δ⇩ℰ⇩A"
"𝒞 ≡ TA {||} Δ_ℰ_A_B"">abbreviation "𝒞 ≡ TA {||} Δ⇩ℰ⇩A⇩B"
"ℬ ≡ TA Δ_B Δ_ℰ_B"">abbreviation "ℬ ≡ TA Δ⇩B Δ⇩ℰ⇩B"
"𝒬_A ≡ 𝒬 𝒜"">abbreviation "𝒬⇩A ≡ 𝒬 𝒜"
"𝒬_B ≡ 𝒬 ℬ"">abbreviation "𝒬⇩B ≡ 𝒬 ℬ"
lemma states_split [simp]:
"𝒬 A = 𝒬 𝒜 |∪| 𝒬 ℬ"
using fsubsetD[OF eps_AB_trans] st_split
by (auto simp add: 𝒬_def rule_split eps_split elim!: eps_statesE)
lemma state_sets_disjoint: "𝒬⇩A |∩| 𝒬⇩B = {||}"
using st_split by (auto simp add: 𝒬_def inf_sup_aci(5))
lemma rule_statesD:
"r |∈| Δ⇩A ⟹ r_rhs r |∈| 𝒬⇩A" "r |∈| Δ⇩B ⟹ r_rhs r |∈| 𝒬⇩B"
"r |∈| Δ⇩A ⟹ p |∈| fset_of_list (r_lhs_states r) ⟹ p |∈| 𝒬⇩A"
"r |∈| Δ⇩B ⟹ p |∈| fset_of_list (r_lhs_states r) ⟹ p |∈| 𝒬⇩B"
"TA_rule f qs q |∈| Δ⇩A ⟹ q |∈| 𝒬⇩A" "TA_rule f qs q |∈| Δ⇩B ⟹ q |∈| 𝒬⇩B"
"TA_rule f qs q |∈| Δ⇩A ⟹ p |∈| fset_of_list qs ⟹ p |∈| 𝒬⇩A"
"TA_rule f qs q |∈| Δ⇩B ⟹ p |∈| fset_of_list qs ⟹ p |∈| 𝒬⇩B"
using state_sets_disjoint
by (auto simp: rule_statesD)
lemma trancl_AB[simp]: "Δ⇩ℰ⇩A⇩B|⇧+| = Δ⇩ℰ⇩A⇩B"
using state_sets_disjoint st_split eps_AB_trans
by (intro frelcomp_empty_ftrancl_simp) auto
lemma eps_dest_all:
"(p, q) |∈| Δ⇩ℰ⇩A ⟹ p |∈| 𝒬⇩A" "(p, q) |∈| Δ⇩ℰ⇩A ⟹ q |∈| 𝒬⇩A"
"(p, q) |∈| Δ⇩ℰ⇩A|⇧+| ⟹ p |∈| 𝒬⇩A" "(p, q) |∈| Δ⇩ℰ⇩A|⇧+| ⟹ q |∈| 𝒬⇩A"
"(p, q) |∈| Δ⇩ℰ⇩B ⟹ p |∈| 𝒬⇩B" "(p, q) |∈| Δ⇩ℰ⇩B ⟹ q |∈| 𝒬⇩B"
"(p, q) |∈| Δ⇩ℰ⇩B|⇧+| ⟹ p |∈| 𝒬⇩B" "(p, q) |∈| Δ⇩ℰ⇩B|⇧+| ⟹ q |∈| 𝒬⇩B"
"(p, q) |∈| Δ⇩ℰ⇩A⇩B ⟹ p |∈| 𝒬⇩A" "(p, q) |∈| Δ⇩ℰ⇩A⇩B ⟹ q |∈| 𝒬⇩B"
using state_sets_disjoint eps_AB_trans
by (auto simp: eps_dest_all) (auto simp: 𝒬_def)
lemma eps_B_comp_empty: "Δ⇩ℰ⇩B |O| (Δ⇩ℰ⇩A |∪| Δ⇩ℰ⇩A⇩B) = {||}"
using state_sets_disjoint st_split eps_AB_trans
by auto
lemma eps_AB_A_comp_empty: "Δ⇩ℰ⇩A⇩B |O| Δ⇩ℰ⇩A = {||}"
using state_sets_disjoint st_split eps_AB_trans
by auto
lemma transcl_eps_simp:
"(eps A)|⇧+| = Δ⇩ℰ⇩A|⇧+| |∪| Δ⇩ℰ⇩B|⇧+| |∪| Δ⇩ℰ⇩A⇩B |∪| Δ⇩ℰ⇩A|⇧+| |O| Δ⇩ℰ⇩A⇩B |∪| Δ⇩ℰ⇩A⇩B |O| Δ⇩ℰ⇩B|⇧+| |∪| Δ⇩ℰ⇩A|⇧+| |O| Δ⇩ℰ⇩A⇩B |O| Δ⇩ℰ⇩B|⇧+|"
proof -
have [dest]: "(x, y) |∈| Δ⇩ℰ⇩A|⇧+| ⟹ (y, z) |∈| Δ⇩ℰ⇩B|⇧+| ⟹ False" for x y z
using eps_dest_all(4, 7) state_sets_disjoint by fastforce
then show ?thesis
unfolding eps_split using state_sets_disjoint
by (auto simp: in_ftrancl_UnI ftrancl_Un2_separatorE[OF eps_B_comp_empty]
ftrancl_Un2_separatorE[OF eps_AB_A_comp_empty])
qed
lemma rule_eps_A_state:
assumes "TA_rule f qs q |∈| rules A" and "q = p ∨ (q, p) |∈| (eps A)|⇧+|" and "p |∈| 𝒬⇩A"
shows "TA_rule f qs q |∈| Δ⇩A" "q = p ∨ (q, p) |∈| Δ⇩ℰ⇩A|⇧+|" using assms
using state_sets_disjoint
unfolding transcl_eps_simp rule_split
by (auto elim!: rule_statesD eps_dest_all dest: eps_dest_all)
lemma rule_eps_B_state:
assumes "TA_rule f qs q |∈| rules A" and "q = p ∨ (q, p) |∈| (eps A)|⇧+|" and "q |∈| 𝒬⇩B"
shows "TA_rule f qs q |∈| Δ⇩B" "q = p ∨ (q, p) |∈| Δ⇩ℰ⇩B|⇧+|" using assms
using state_sets_disjoint
unfolding transcl_eps_simp rule_split
by (auto dest: rule_statesD eps_dest_all)
lemma eps_from_A_to_B_E:
assumes "(p, r) |∈| (eps A)|⇧+|" and "p |∈| 𝒬⇩A" "r |∈| 𝒬⇩B"
obtains q r' where "p = q ∨ (p, q) |∈| Δ⇩ℰ⇩A|⇧+|" "(q, r') |∈| Δ⇩ℰ⇩A⇩B" "r' = r ∨ (r', r) |∈| Δ⇩ℰ⇩B|⇧+|"
using assms state_sets_disjoint
unfolding transcl_eps_simp rule_split
by (auto elim!: rule_statesD eps_dest_all)
declare fsubsetI[rule del]
lemma ta_der_monos:
"ta_der 𝒜 t |⊆| ta_der A t" "ta_der ℬ t |⊆| ta_der A t" "ta_der 𝒞 t |⊆| ta_der A t"
by (auto simp: sup.coboundedI1 rule_split eps_split intro!: ta_der_mono)
declare fsubsetI[intro!]
lemma ta_der_from_Δ⇩A:
assumes "q |∈| ta_der A (term_of_gterm t)" and "q |∈| 𝒬⇩A"
shows "q |∈| ta_der 𝒜 (term_of_gterm t)" using assms
proof (induct rule: ta_der_gterm_induct)
case (GFun f ts ps p q)
have "i < length ts ⟹ ps ! i |∈| 𝒬⇩A" for i using GFun
by (metis fnth_mem local.rule_statesD(7) rule_eps_A_state(1))
then show ?case using GFun(2, 5) rule_eps_A_state[OF GFun(1, 3, 6)]
by (auto simp: transcl_eps_simp)
qed
lemma ta_der_state:
assumes "q |∈| ta_der A (term_of_gterm s)"
shows "q |∈| 𝒬⇩A ∨ q |∈| 𝒬⇩B"
using gterm_ta_der_states[OF assms]
by auto
lemma ta_der'_states_𝒜:
assumes "t |∈| ta_der' 𝒜 (term_of_gterm s)"
shows "fvars_term t |⊆| 𝒬⇩A" using assms
proof (induct s arbitrary: t)
case (GFun f ts)
then show ?case
by (cases t) (force simp: in_fset_conv_nth dest: rule_statesD eps_dest_all)+
qed
lemma ta_der_states_ℬ:
assumes "q |∈| ta_der ℬ t" and "is_Fun t"
shows "fvars_term t |⊆| 𝒬⇩B ∧ q |∈| 𝒬⇩B" using assms
proof (induct rule: ta_der_induct)
case (Fun f ts ps p q)
{fix i assume ass: "i < length ts" "is_Var (ts ! i)"
then obtain x where [simp]: "ts ! i = Var x" by auto
have "the_Var (ts ! i) = ps ! i ∨ (the_Var (ts ! i), ps ! i) |∈| Δ⇩ℰ⇩B|⇧+|"
using Fun(4)[OF ass(1)] ass(2)
by auto
then have "x |∈| 𝒬⇩B" using Fun(1, 2) ass
by (auto elim: rule_statesD dest: eps_dest_all)
then have "fvars_term (ts ! i) |⊆| 𝒬⇩B" by auto}
then show ?case using Fun
by (auto simp: in_fset_conv_nth elim: rule_statesD eps_dest_all, blast+)
qed auto
lemma 𝒞_num_variable_stable:
assumes "u |∈| ta_der' 𝒞 t"
shows "length (vars_term_list t) = length (vars_term_list u)" using assms
proof (induct t arbitrary: u)
case (Fun f ts)
show ?case using Fun(2) Fun(1)[OF nth_mem, of i "args u ! i" for i]
by (cases u) (auto simp: vars_term_list.simps intro: eq_length_concat_nth)
qed (auto simp: ta_der'.simps vars_term_list.simps)
lemma 𝒞_ta_der_Δ⇩ℰ⇩A⇩B:
assumes "fvars_term t |⊆| 𝒬⇩A" "u |∈| ta_der' 𝒞 t" "q |∈| ta_der ℬ u" "q |∈| 𝒬⇩B"
shows "fset_of_list (zip (vars_term_list t) (vars_term_list u)) |⊆| Δ⇩ℰ⇩A⇩B" using assms
proof (induct t arbitrary: u q)
case (Var x) then show ?case
using state_sets_disjoint
by (cases u) (auto simp: ta_der'.simps vars_term_list.simps eps_dest_all)
next
case (Fun f ts)
from Fun(3) obtain ss where [simp]: "u = Fun f ss" by (cases u) auto
{fix i assume i: "i < length ts"
then have "fvars_term (ts ! i) |⊆| 𝒬⇩A" using Fun(2)
by auto (meson ffUnionI fimage_eqI fnth_mem fsubsetD)
from Fun(1)[OF nth_mem[OF i] this, of "ss ! i"] i have
"fset_of_list (zip (vars_term_list (ts ! i)) (vars_term_list (ss ! i))) |⊆| Δ⇩ℰ⇩A⇩B"
"length (vars_term_list (ts ! i)) = length (vars_term_list (ss ! i))"
using Fun(2-) ta_der_states_ℬ[OF Fun(4)]
using 𝒞_num_variable_stable[of "ss ! i" "ts ! i"]
by (fastforce simp: ta_der'.simps rule_statesD)+}
note IH = this
have un_index: "i < length (concat (map vars_term_list ts)) ⟹
concat_index_split (0, i) (map vars_term_list ss) = concat_index_split (0, i) (map vars_term_list ts)" for i
using IH(2) 𝒞_num_variable_stable[OF Fun(3)] Fun(3)
by (auto simp: vars_term_list.simps intro!: concat_index_split_unique)
{fix i assume ass: "i < length (concat (map vars_term_list ts))"
then have ls: "i < length (concat (map vars_term_list ss))" using Fun(3)
using IH(2) by (metis Fun.prems(2) 𝒞_num_variable_stable ‹u = Fun f ss› vars_term_list.simps(2))
obtain m n where [simp]: "concat_index_split (0, i) (map vars_term_list ts) = (m, n)" by fastforce
have "(concat (map vars_term_list ts) ! i, concat (map vars_term_list ss) ! i) |∈| Δ⇩ℰ⇩A⇩B"
using ass ls un_index IH[of m] concat_index_split_sound_fst_arg[OF ls]
using concat_index_split_sound concat_index_split_sound_fst_arg[OF ass]
using concat_index_split_sound_snd_arg[OF ls]
by (auto simp: concat_index_split_sound simp flip: fsubseteq_fset_conv_nth)}
then show ?case by (auto simp: vars_term_list.simps in_fset_conv_nth split: prod.splits)
qed
lemma ta_der_split:
assumes "q |∈| ta_der A (term_of_gterm s)" and "q |∈| 𝒬⇩B"
shows "∃ t u. t |∈| ta_der' 𝒜 (term_of_gterm s) ∧ u |∈| ta_der' 𝒞 t ∧ q |∈| ta_der ℬ u"
(is "∃t u . ?P s q t u") using assms
proof (induct s arbitrary: q)
case (GFun f ts)
from GFun(2) obtain qs q' where r: "TA_rule f qs q' |∈| rules A" "length qs = length ts" and
eps: "q' = q ∨ (q', q) |∈| (eps A)|⇧+|" and reach: "∀ i < length ts. qs ! i |∈| ta_der A (term_of_gterm (ts ! i))"
by auto
show ?case proof (cases "q' |∈| 𝒬⇩A")
case True then obtain p r where eps_sp: "q' = p ∨ (q', p) |∈| Δ⇩ℰ⇩A|⇧+|"
"(p, r) |∈| Δ⇩ℰ⇩A⇩B" "r = q ∨ (r, q) |∈| Δ⇩ℰ⇩B|⇧+|"
using eps GFun(3) state_sets_disjoint
by (auto elim!: eps_from_A_to_B_E)
then have "p |∈| ta_der A (term_of_gterm (GFun f ts))" using reach r eps
by (auto simp: transcl_eps_simp)
from this ta_der_from_Δ⇩A[OF this] True eps_sp show ?thesis
by (rule_tac x = "Var p" in exI, rule_tac x = "Var r" in exI)
(auto dest: eps_dest_all)
next
case False then have "i < length qs ⟹ qs ! i |∈| 𝒬⇩B" for i using rule_eps_B_state r rule_statesD
by (auto simp: rule_split)
then obtain h where IH:
"∀ i < length ts. fst (h i) |∈| ta_der' 𝒜 (term_of_gterm (ts ! i))"
"∀ i < length ts. snd (h i) |∈| ta_der' 𝒞 (fst (h i)) ∧ qs ! i |∈| ta_der ℬ (snd (h i))"
using GFun(1)[OF nth_mem, of i "qs ! i" for i] r(2) reach
using choice_nat[of "length ts" "λ t i. ?P (ts ! i) (qs ! i) (fst t) (snd t)"]
by auto blast
then show ?thesis using r(2) False rule_eps_B_state[OF r(1) eps]
by (rule_tac x = "Fun f (map (fst ∘ h) [0 ..< length ts])" in exI,
rule_tac x = "Fun f (map (snd ∘ h) [0 ..< length ts])" in exI)
(auto, metis funion_iff r(1) rule_split rule_statesD(1, 2) ta_rule.sel(3))
qed
qed
lemma ta_der_from_Δ⇩B:
assumes "t |∈| ta_der' 𝒜 (term_of_gterm s)" and "q |∈| ta_der ℬ t" and "q |∈| 𝒬⇩B"
shows "q |∈| ta_der ℬ (term_of_gterm s)"
proof (cases "is_Fun t")
case True show ?thesis
using state_sets_disjoint ta_der'_states_𝒜[OF assms(1)] assms(3)
using ta_der_states_ℬ[OF assms(2) True] ta_der_to_ta_der'
using ta_der'_empty_step_fvars[OF assms(1)] assms(2)
by force
next
case False then show ?thesis using state_sets_disjoint ta_der'_states_𝒜[OF assms(1)] assms(2,3)
by (cases t) (auto dest: eps_dest_all)
qed
lemma ta_der_to_mcxtx:
assumes "q |∈| ta_der A (term_of_gterm s)" and "q |∈| 𝒬⇩B"
shows "∃ C ss qs qs'. length qs' = length qs ∧ length qs = length ss ∧ num_holes C = length ss ∧
(∀ i < length ss. qs ! i |∈| ta_der 𝒜 (term_of_gterm (ss ! i))) ∧
(∀ i < length ss. (qs ! i, qs' ! i) |∈| Δ⇩ℰ⇩A⇩B) ∧
q |∈| ta_der ℬ (fill_holes C (map Var qs')) ∧
ground_mctxt C ∧ funas_mctxt C ⊆ fset (ta_sig ℬ) ∧
fill_holes C (map term_of_gterm ss) = term_of_gterm s"
(is "∃C ss qs qs'. ?P s q C ss qs qs'")
using ta_der_split[OF assms]
proof -
from ta_der_split[OF assms] obtain t u where
wit: "t |∈| ta_der' 𝒜 (term_of_gterm s)" "u |∈| ta_der' 𝒞 t" "q |∈| ta_der ℬ u" by auto
have poss [simp]:"i < length (varposs_list t) ⟹ varposs_list t ! i ∈ gposs s" for i
by (metis nth_mem ta_der'_poss[OF wit(1)] poss_gposs_conv subset_eq varposs_eq_varposs_list
varposs_imp_poss varposs_list_var_terms_length)
from wit(1) have vars: "fvars_term t |⊆| 𝒬⇩A" using ta_der'_states_𝒜 by blast
show ?thesis using wit 𝒞_ta_der_Δ⇩ℰ⇩A⇩B[OF vars wit(2,3) assms(2)]
apply (rule_tac x = "fst (split_vars t)" in exI,
rule_tac x = "map (gsubt_at s) (varposs_list t)" in exI,
rule_tac x = "snd (split_vars t)" in exI,
rule_tac x = "snd (split_vars u)" in exI)
apply (auto simp: split_vars_num_holes split_vars_vars_term_list 𝒞_num_variable_stable term_of_gterm_gsubt
varposs_list_var_terms_length varposs_eq_varposs_list set_zip split_vars_fill_holes comp_def
simp flip: fsubseteq_fset_conv_nth varposs_list_to_var_term_list ta_der'_eps_eq_split_vars[OF wit(2)]
intro!: ta_der'_varposs_to_ta_der)
subgoal using ta_der_term_sig[of q "TA Δ⇩B Δ⇩ℰ⇩B" u]
by (simp add: ffunas_term.rep_eq in_mono less_eq_fset.rep_eq)
apply (auto simp: term_of_gterm_gsubt ta_der'_fill_holes[OF wit(1)] ta_der'_eps_eq_split_vars[OF wit(2)])
by (metis (no_types, lifting) map_eq_conv' poss ta_der'_fill_holes term_of_gterm_gsubt)
qed
lemma ta_der_to_gmcxtx:
assumes "q |∈| ta_der A (term_of_gterm s)" and "q |∈| 𝒬⇩B"
shows "∃ C ss qs qs'. length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss ∧
(∀ i < length ss. qs ! i |∈| ta_der 𝒜 (term_of_gterm (ss ! i))) ∧
(∀ i < length ss. (qs ! i, qs' ! i) |∈| Δ⇩ℰ⇩A⇩B) ∧
q |∈| ta_der ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs')) ∧ funas_gmctxt C ⊆ fset (ta_sig ℬ) ∧
fill_gholes C ss = s"
using ta_der_to_mcxtx[OF assms]
by (metis funas_gmctxt_of_mctxt gmctxt_of_mctxt_inv ground_gmctxt_of_gterm_of_term num_gholes_gmctxt_of_mctxt term_of_gterm_inv)
end
lemma ta_der'_rule_empty:
assumes "Var q |∈| ta_der' (TA {||} Δ⇩ε) t"
obtains p where "t = Var p" "p = q ∨ (p, q) |∈| Δ⇩ε|⇧+|"
using assms by (cases t) auto
"ta_relfcl_rules ℱ q ≡ (λ (f, n). TA_rule f (replicate n q) q) |`| ℱ"">definition "ta_relfcl_rules ℱ q ≡ (λ (f, n). TA_rule f (replicate n q) q) |`| ℱ"
definition gen_reflcl_automaton :: "('f × nat) fset ⇒ ('q, 'f) ta ⇒ 'q ⇒ ('q, 'f) ta" where
"gen_reflcl_automaton ℱ 𝒜 q = TA (rules 𝒜 |∪| ta_relfcl_rules ℱ q) (eps 𝒜)"
lemma ta_reflcl_funas [simp]:
"(λ r. (r_root r, length (r_lhs_states r))) |`| (ta_relfcl_rules ℱ q) = ℱ"
by (auto simp: fimage_iff fBex_def ta_relfcl_rules_def)
lemma rule_states_refl [simp]:
"ℱ ≠ {||} ⟹ rule_states (ta_relfcl_rules ℱ q) = {|q|}"
"ℱ = {||} ⟹ rule_states (ta_relfcl_rules ℱ q) = {||}"
using in_fset_idx
by (auto simp: rule_states_def image_iff fBex_def ta_relfcl_rules_def) force+
lemma reflcl_st_reachable_if:
assumes "q |∈| ta_der (TA (ta_relfcl_rules ℱ q) {||}) s"
shows "ffunas_term s |⊆| ℱ ∧ fvars_term s |⊆| {|q|}" using assms
proof (induct s)
case (Fun f ts)
show ?case using Fun(1)[OF nth_mem] Fun(2-)
by (auto simp: ta_relfcl_rules_def) (metis fin_mono fsingleton_iff in_fset_idx)+
qed auto
lemma reflcl_st_reachable_only_if:
assumes "ffunas_term t |⊆| ℱ" and "fvars_term t |⊆| {|q|}"
shows "q |∈| ta_der (TA (ta_relfcl_rules ℱ q) {||}) t" using assms
proof (induct t)
case (Fun f ts)
then show ?case
by (auto simp: ta_relfcl_rules_def rev_fimage_eqI intro!: exI[of _ "replicate (length ts) q"])
(smt ffUnionI fnth_mem fsubsetD fsubsetI nth_mem rev_fimage_eqI)
qed auto
lemma reflcl_st_reachable_only_if':
assumes "funas_term t ⊆ fset ℱ" and "vars_term t ⊆ {q}"
shows "q |∈| ta_der (TA (ta_relfcl_rules ℱ q) {||}) t"
using assms
by (intro reflcl_st_reachable_only_if)
(simp add: fvars_term.rep_eq ffunas_term.rep_eq less_eq_fset.rep_eq)+
lemma reflcl_st_gen_reflc:
assumes "ffunas_term t |⊆| ℱ" and "fvars_term t |⊆| {|q|}"
shows "q |∈| ta_der (gen_reflcl_automaton ℱ 𝒜 q) t"
using ta_der_el_mono[OF _ _ reflcl_st_reachable_only_if[OF assms]]
by (auto simp: gen_reflcl_automaton_def)
lemma gen_reflcl_lang:
assumes "q |∉| 𝒬 𝒜"
shows "gta_lang (finsert q Q) (gen_reflcl_automaton ℱ 𝒜 q) = gta_lang Q 𝒜 ∪ 𝒯⇩G (fset ℱ)"
(is "?Ls = ?Rs1 ∪ ?Rs2")
proof -
let ?A = "gen_reflcl_automaton ℱ 𝒜 q"
interpret sq: derivation_split ?A "rules 𝒜" "ta_relfcl_rules ℱ q" "eps 𝒜" "{||}" "{||}"
using assms in_fset_idx
by (auto simp: ta_relfcl_rules_def derivation_split_def gen_reflcl_automaton_def
rule_states_def eps_states_def 𝒬_def fBall_def) fastforce+
show ?thesis proof
{fix t assume "t ∈ ?Ls"
from gta_langE[OF this] obtain p where fin: "p |∈| finsert q Q" and reach: "p |∈| ta_der ?A (term_of_gterm t)" .
then have st: "p |∈| sq.𝒬⇩A ∨ p |∈| sq.𝒬⇩B" using sq.ta_der_state by blast
then have "t ∈ ?Rs1 ∪ ?Rs2"
proof (cases "p |∈| sq.𝒬⇩A")
case True
have "p ≠ q" using True assms by auto
then have "t ∈ ?Rs1" using True fin sq.ta_der_from_Δ⇩A[OF reach True]
by (auto simp: gen_reflcl_automaton_def intro: gta_langI)
then show ?thesis by blast
next
case False
then have b: "p |∈| sq.𝒬⇩B" using st sq.state_sets_disjoint by auto
then have [simp]: "p = q" using assms in_fset_idx
by (auto simp: fBall_def 𝒬_def eps_states_def rule_states_def ta_relfcl_rules_def) force
have "p |∈| ta_der sq.ℬ (term_of_gterm t)"
using sq.ta_der_split[OF reach b] sq.ta_der_from_Δ⇩B[of _ t p] b
using ta_der'_empty by blast
then show ?thesis using reflcl_st_reachable_if[of q ℱ "term_of_gterm t"]
by (auto simp: funas_term_of_gterm_conv 𝒯⇩G_equivalent_def
ffunas_gterm.rep_eq ffunas_term_of_gterm_conv in_mono less_eq_fset.rep_eq)
qed}
then show "?Ls ⊆ ?Rs1 ∪ ?Rs2" by blast
next
{fix s assume "s ∈ ?Rs2"
then have "ffunas_gterm s |⊆| ℱ" unfolding 𝒯⇩G_equivalent_def
by (simp add: ffunas_gterm.rep_eq less_eq_fset.rep_eq)
from reflcl_st_gen_reflc[of "term_of_gterm s" ℱ q 𝒜] this
have "q |∈| ta_der ?A (term_of_gterm s)"
by (simp add: ffunas_term_of_gterm_conv)
then have "s ∈ ?Ls" by (auto simp add: gen_reflcl_automaton_def intro!: gta_langI)}
moreover have "?Rs1 ⊆ ?Ls"
by (intro gta_lang_mono) (auto simp add: ta_der_mono gen_reflcl_automaton_def)
ultimately show "?Rs1 ∪ ?Rs2 ⊆ ?Ls" by blast
qed
qed
"reflcl_automaton ℱ 𝒜 = (let ℬ = fmap_states_ta Some 𝒜 in">definition "reflcl_automaton ℱ 𝒜 = (let ℬ = fmap_states_ta Some 𝒜 in
gen_reflcl_automaton ℱ ℬ None)"
lemma ta_states_gen_reflcl_automaton [simp]:
"ℱ ≠ {||} ⟹ 𝒬 (gen_reflcl_automaton ℱ ℬ q) = 𝒬 ℬ |∪| {|q|}"
"ℱ = {||} ⟹ 𝒬 (gen_reflcl_automaton ℱ ℬ q) = 𝒬 ℬ"
by (simp add: gen_reflcl_automaton_def 𝒬_def)+
lemma fmap_states_Some_pres_gta [simp]:
"gta_lang (Some |`| Q) (fmap_states_ta Some 𝒜) = gta_lang Q 𝒜 "
by (intro fmap_states_ta_lang2) (simp add: finj_Some)
lemma reflcl_lang:
"gta_lang (finsert None (Some |`| Q)) (reflcl_automaton ℱ 𝒜) = gta_lang Q 𝒜 ∪ 𝒯⇩G (fset ℱ)"
proof -
have st: "None |∉| 𝒬 (fmap_states_ta Some 𝒜)" by auto
have "gta_lang Q 𝒜 = gta_lang (Some |`| Q) (fmap_states_ta Some 𝒜)" by simp
then show ?thesis
unfolding reflcl_automaton_def Let_def gen_reflcl_lang[OF st, of "Some |`| Q" ℱ]
by simp
qed
"reflcl_reg ℱ 𝒜 = Reg (finsert None (Some |`| fin 𝒜)) (reflcl_automaton ℱ (ta 𝒜))"">definition "reflcl_reg ℱ 𝒜 = Reg (finsert None (Some |`| fin 𝒜)) (reflcl_automaton ℱ (ta 𝒜))"
lemma ℒ_reflcl_reg:
"ℒ (reflcl_reg ℱ 𝒜) = ℒ 𝒜 ∪ 𝒯⇩G (fset ℱ)"
by (simp add: ℒ_def reflcl_lang reflcl_reg_def )
definition gen_parallel_closure_automaton :: "'q fset ⇒ ('f × nat) fset ⇒ ('q, 'f) ta ⇒ 'q ⇒ ('q, 'f) ta" where
"gen_parallel_closure_automaton Q ℱ 𝒜 q =
TA (rules 𝒜 |∪| ta_relfcl_rules ℱ q) (eps 𝒜 |∪| (λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜))"
lemma gen_parallel_closure_automaton_mono:
"ta_der 𝒜 t |⊆| ta_der (gen_parallel_closure_automaton Q ℱ 𝒜 q) t"
by (intro ta_der_mono) (auto simp: gen_parallel_closure_automaton_def)
lemma reflcl_parallel_closure_mono:
"ta_der (gen_reflcl_automaton ℱ 𝒜 q) t |⊆| ta_der (gen_parallel_closure_automaton Q ℱ 𝒜 q) t"
by (intro ta_der_mono) (auto simp: gen_reflcl_automaton_def gen_parallel_closure_automaton_def)
lemma parcl_st_reachable_only_if:
assumes "ffunas_term t |⊆| ℱ" and "fvars_term t |⊆| {|q|}"
shows "q |∈| ta_der (gen_parallel_closure_automaton Q ℱ 𝒜 q) t"
using reflcl_st_gen_reflc[OF assms] reflcl_parallel_closure_mono[of ℱ _ q t]
by blast
lemma parcl_st_reachable_only_if':
assumes "funas_term t ⊆ fset ℱ" and "vars_term t ⊆ {q}"
shows "q |∈| ta_der (gen_parallel_closure_automaton Q ℱ 𝒜 q) t"
using parcl_st_reachable_only_if
by (simp add: parcl_st_reachable_only_if assms(1) assms(2) ffunas_term.rep_eq fvars_term.rep_eq less_eq_fset.rep_eq)
lemma gta_lang_eq_fin_to_eps:
assumes "q |∉| 𝒬 𝒜"
shows "gta_lang Q 𝒜 = gta_lang {|q|} (TA (rules 𝒜) (eps 𝒜 |∪| (λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜)))"
(is "?Ls = ?Rs")
proof -
let ?A = "TA (rules 𝒜) (eps 𝒜 |∪| (λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜) |∪| {|(q, q)|})"
let ?A' = "TA (rules 𝒜) (eps 𝒜 |∪| (λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜))"
interpret sq: derivation_split ?A "rules 𝒜" "{||}" "eps 𝒜" "{|(q, q)|}" "(λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜)"
using assms unfolding derivation_split_def
by (auto simp: 𝒬_def)
have res: "ta_der 𝒜 t |⊆| ta_der ?A t" for t by (intro ta_der_mono) auto
then have "?Ls ⊆ ?Rs" using ta_der_eps[of _ q ?A']
by (auto simp add: gta_lang_def gta_der_def)
(smt fimage_finsert finsert_iff finter_finsert_left_if1 gterm_ta_der_states
mk_disjoint_finsert sq.rule_split sup_ge1 ta.sel(1, 2) ta_der_el_mono)
moreover
{fix t assume "q |∈| ta_der ?A' (term_of_gterm t)"
then have res: "q |∈| ta_der ?A (term_of_gterm t)"
by (intro ta_der_el_mono[of ?A' ?A]) auto
have "q |∈| sq.𝒬⇩B" by (simp add: sq.eps_dest_all(6))
from sq.ta_der_split[OF res this] assms
have "∃ p. p |∈| Q ∧ p |∈| ta_der 𝒜 (term_of_gterm t)"
by (auto dest!: ta_der'_to_ta_der elim!: ta_der_rule_empty ta_der'_rule_empty)}
ultimately show ?thesis by auto fastforce
qed
lemma gta_lang_subset_mctxt_closure:
"gta_lang Q 𝒜 ⊆ {fill_gholes C ss | C ss. num_gholes C = length ss ∧ funas_gmctxt C ⊆ ℱ ∧ (∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜)}"
(is "?Ls ⊆ ?Rs")
proof
fix t assume "t ∈ ?Ls" then show "t ∈ ?Rs"
by (auto intro!: exI[of _ GMHole] exI[of _ "[t]"])
qed
lemma parallelcl_fresh_q_sequential_derivation:
assumes "q |∉| 𝒬 𝒜" and "ℱ ≠ {||}"
shows "derivation_split (gen_parallel_closure_automaton Q ℱ 𝒜 q) (rules 𝒜) (ta_relfcl_rules ℱ q) (eps 𝒜) {||} ((λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜))"
using assms unfolding derivation_split_def
by (auto simp: gen_parallel_closure_automaton_def 𝒬_def)
lemma gen_parallelcl_lang:
fixes 𝒜 :: "('q, 'f) ta"
assumes "q |∉| 𝒬 𝒜"
shows "gta_lang {|q|} (gen_parallel_closure_automaton Q ℱ 𝒜 q) =
{fill_gholes C ss | C ss. num_gholes C = length ss ∧ funas_gmctxt C ⊆ (fset ℱ) ∧ (∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜)}"
(is "?Ls = ?Rs")
proof (cases "ℱ = {||}")
case True
then have [simp]: "ta_relfcl_rules ℱ q = {||}" by (auto simp: ta_relfcl_rules_def)
have [simp]: "num_gholes C = length ss ⟹ funas_gmctxt C = {} ⟹
∀i<length ss. ss ! i ∈ gta_lang Q 𝒜 ⟹ fill_gholes C ss ∈ gta_lang Q 𝒜" for ss C
by (cases C; cases ss) auto
have "x ∈ gta_lang Q 𝒜 ⟹ fill_gholes GMHole [x] ∈ gta_lang Q 𝒜" for x by auto
then have rs2: "?Rs = gta_lang Q 𝒜" using True
by (auto intro!: exI[of _ GMHole])
(metis fill_gholes.simps(1) length_nth_simps(1, 2) less_Suc0 nth_Cons_0)
show ?thesis using gta_lang_eq_fin_to_eps[OF assms(1)] unfolding rs2
by (auto simp: gen_parallel_closure_automaton_def)
next
case False
let ?A = "gen_parallel_closure_automaton Q ℱ 𝒜 q"
interpret sq: derivation_split ?A "rules 𝒜" "ta_relfcl_rules ℱ q" "(eps 𝒜)" "{||}" "((λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜))"
using parallelcl_fresh_q_sequential_derivation[OF assms False] by simp
show ?thesis proof
{fix t assume "t ∈ ?Ls"
then have reach: "q |∈| ta_der ?A (term_of_gterm t)"
by (auto simp: gen_parallel_closure_automaton_def elim!: gta_langE)
have *: "{y. ∃a b. (a, b) ∈ fset ℱ ∧ y = (a, b)} = fset ℱ"
by auto
have qb:"q |∈| sq.𝒬⇩B" using False image_iff by (auto simp: 𝒬_def)
from sq.ta_der_to_gmcxtx[OF reach(1) this] obtain C ss qs qs' where
len : "length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss" and
reachA: "∀ i < length ss. qs ! i |∈| ta_der sq.𝒜 (term_of_gterm (ss ! i))" and
toB: "∀i<length ss. (qs ! i, qs' ! i) |∈| ((λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜))" and
reachq: "q |∈| ta_der sq.ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs'))" and
mctxt: "funas_gmctxt C ⊆ (fset ℱ) ∧ fill_gholes C ss = t"
by (auto simp: ta_sig_def image_def Bex_def * split!: prod.splits)
then have "t ∈ ?Rs" using toB reachA len mctxt
by (auto simp: intro!: exI[of _ C] exI[of _ ss])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix t assume "t ∈ ?Rs"
then obtain C ss where len: "num_gholes C = length ss" and
gr_fun: "funas_gmctxt C ⊆ fset ℱ" and
reachA: "∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜" and
const: "t = fill_gholes C ss" by auto
obtain qs where qs: "length qs = length ss" "∀ i < length ss. qs ! i |∈| Q"
"∀ i < length ss. qs ! i |∈| ta_der 𝒜 (term_of_gterm (ss ! i))" using reachA
using Ex_list_of_length_P[of "length ss" "λ q i. q |∈| ta_der 𝒜 (term_of_gterm (ss ! i)) ∧ q |∈| Q"]
by force
then have "∀ i < length qs. q |∈| ta_der ?A (Var (qs ! i))"
by (auto simp: gen_parallel_closure_automaton_def) fastforce
from mctxt_args_ta_der'[of "mctxt_of_gmctxt C" "replicate (length ss) q" "map term_of_gterm ss" ?A] this
have mid: "fill_holes (mctxt_of_gmctxt C) (map Var (replicate (length ss) q))|∈| ta_der' ?A (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss))"
using gen_parallel_closure_automaton_mono[of 𝒜 "term_of_gterm (ss ! i)" for i] qs(1, 3) len
using ta_der_trancl_eps by fastforce
then have "q |∈| ta_der ?A (fill_holes (mctxt_of_gmctxt C) (map Var (replicate (length ss) q)))"
using len gr_fun
by (intro parcl_st_reachable_only_if')
(auto simp: funas_mctxt_of_gmctxt_conv funas_term_fill_holes_iff)
then have "t ∈ ?Ls" using const ta_der'_trans[OF mid, of "Var q"]
by (simp add: fill_holes_mctxt_of_gmctxt_to_fill_gholes gta_langI len ta_der_to_ta_der')}
then show "?Rs ⊆ ?Ls" by blast
qed
qed
definition parallel_closure_reg where
"parallel_closure_reg ℱ 𝒜 = (let ℬ = fmap_states_reg Some 𝒜 in
Reg {|None|} (gen_parallel_closure_automaton (fin ℬ) ℱ (ta ℬ) None))"
lemma ta_states_gen_parallel_closure_automaton [simp]:
"𝒬 (gen_parallel_closure_automaton Q ℱ ℬ q) |⊆| 𝒬 ℬ |∪| {|q|}"
by (intro 𝒬_subseteq_I)
(auto simp: gen_parallel_closure_automaton_def rule_statesD eps_statesD in_fset_conv_nth ta_relfcl_rules_def)
lemma parallelcl_gmctxt_lang:
fixes 𝒜 :: "('q, 'f) reg"
shows "ℒ (parallel_closure_reg ℱ 𝒜) =
{fill_gholes C ss |
C ss. num_gholes C = length ss ∧ funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
proof -
have *: "gta_lang (fin (fmap_states_reg Some 𝒜)) (fmap_states_ta Some (ta 𝒜)) = gta_lang (fin 𝒜) (ta 𝒜)"
by (simp add: fmap_states_reg_def)
have " None |∉| 𝒬 (fmap_states_ta Some (ta 𝒜))" by auto
from gen_parallelcl_lang[OF this, of "fin (fmap_states_reg Some 𝒜)" ℱ] show ?thesis
unfolding ℒ_def parallel_closure_reg_def Let_def * fmap_states_reg_def
by auto
qed
lemma parallelcl_mctxt_lang:
shows "ℒ (parallel_closure_reg ℱ 𝒜) =
{(gterm_of_term :: ('f, 'q option) term ⇒ 'f gterm) (fill_holes C (map term_of_gterm ss)) |
C ss. num_holes C = length ss ∧ ground_mctxt C ∧ funas_mctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
unfolding parallelcl_gmctxt_lang
apply auto
apply (metis fill_holes_mctxt_of_gmctxt_to_fill_gholes funas_mctxt_of_gmctxt_conv ground_mctxt_of_gmctxt num_holes_mctxt_of_gmctxt term_of_gterm_inv)
apply (metis funas_gmctxt_of_mctxt ground_gmctxt_of_gterm_of_term num_gholes_gmctxt_of_mctxt)
done
abbreviation args :: "'q list ⇒ 'q ⇒ nat ⇒ 'q list" where
"args qs q i ≡ (take i qs) @ q # (drop (Suc i) qs)"
"semantic_path_rules ℱ q_c q_i q_f ≡ ">definition "semantic_path_rules ℱ q⇩c q⇩i q⇩f ≡
|⋃| ((λ (f, n). fset_of_list (map (λ i. TA_rule f (args (replicate n q⇩c) q⇩i i) q⇩f) [0..< n])) |`| ℱ) |∪|
|⋃| ((λ (f, n). fset_of_list (map (λ i. TA_rule f (args (replicate n q⇩c) q⇩f i) q⇩f) [0..< n])) |`| ℱ)"
lemma semantic_path_rules_fmember [intro]:
"TA_rule f qs q |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f ⟷ (∃ n i. (f, n) |∈| ℱ ∧ i < n ∧ q = q⇩f ∧
(qs = (args (replicate n q⇩c) q⇩i i) ∨ qs = (args (replicate n q⇩c) q⇩f i)))" (is "?Ls ⟷ ?Rs")
proof -
{fix i n assume ass: "(f, n) |∈| ℱ" "i < n" "q = q⇩f"
"qs = (args (replicate n q⇩c) q⇩i i) ∨ qs = (args (replicate n q⇩c) q⇩f i)"
then have "TA_rule f qs q |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f"
unfolding semantic_path_rules_def
by (auto simp: fimage_iff fset_of_list_elem intro!: fBexI[of _ "(f, n)"] fBexI[of _ i])}
moreover have "?Ls ⟹ ?Rs" using less_or_eq_imp_le
unfolding semantic_path_rules_def
by (auto simp: fset_of_list_elem min_def) blast+
ultimately show ?thesis by blast
qed
lemma semantic_path_rules_fmember' [intro]:
"r |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f ⟷ (∃ f qs n i. (f, n) |∈| ℱ ∧ i < n ∧
(qs = (args (replicate n q⇩c) q⇩i i) ∨ qs = (args (replicate n q⇩c) q⇩f i)) ∧
r = TA_rule f qs q⇩f)" (is "?Ls ⟷ ?Rs")
proof -
let ?P = "λ f qs .(∃ n i. (f, n) |∈| ℱ ∧ i < n ∧
(qs = (args (replicate n q⇩c) q⇩i i) ∨ qs = (args (replicate n q⇩c) q⇩f i)) ∧
r = TA_rule f qs q⇩f)"
obtain f qs q where r: "r = TA_rule f qs q" by (cases r) auto
then have "?Ls ⟹ ?P f qs" unfolding r
by (auto simp: semantic_path_rules_fmember)
then have 1: "?Ls ⟹ ?Rs" by blast
have "?P f qs ⟹ ?Ls" unfolding r semantic_path_rules_fmember
by blast
then have 2: "?Rs ⟹ ?Ls" unfolding r by blast
show ?thesis using 1 2 by blast
qed
lemma ta_der_sem_path_reflc_state:
assumes "q⇩c |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) t" and "q⇩c ≠ q⇩f"
shows "vars_term t ⊆ {q⇩c}" using assms
by (induct t) (auto simp: ta_relfcl_rules_def semantic_path_rules_def in_set_conv_nth, blast)
lemma semantic_path_rules_diff_states:
assumes "q⇩i |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) t" and "q⇩c ≠ q⇩i" "q⇩i ≠ q⇩f"
shows "t = Var q⇩i" using assms
by (cases t) (auto simp: ta_relfcl_rules_def semantic_path_rules_def nth_append_Cons)
lemma semantic_path_rules_der_if:
assumes "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) t"
and "q⇩c ≠ q⇩f" and "q⇩c ≠ q⇩i"
shows "length (filter ((=) q⇩i) (vars_term_list t)) = 1 ∨ length (filter ((=) q⇩f) (vars_term_list t)) = 1"
using assms(1)
proof (induct t)
case (Fun f ts)
let ?A = "ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||})"
from Fun(2) assms(2) obtain qs where trans: "f qs → q⇩f |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f"
"length qs = length ts" "∀ i < length ts. (qs ! i) |∈| ?A (ts ! i)"
by (auto simp: ta_relfcl_rules_def)
from trans have "∃ i < length ts. (qs ! i = q⇩f ∨ qs ! i = q⇩i) ∧ (∀ j < length ts. j ≠ i ⟶ qs ! j = q⇩c)"
by (auto simp: semantic_path_rules_fmember nth_append min_def)
then obtain i where wit: "i < length ts" "∀ j < length ts. j ≠ i ⟶ qs ! j = q⇩c" "qs ! i = q⇩f ∨ qs ! i = q⇩i"
by blast
have vars: "j < length ts ⟹ j ≠ i ⟹ vars_term (ts ! j) ⊆ {q⇩c}" for j
using wit ta_der_sem_path_reflc_state ta_der_sem_path_reflc_state[OF _ assms(2), of ℱ _ "ts ! i" for i] trans(3)
by auto
then have "length (filter ((=) q⇩i) (concat (map vars_term_list (take i ts)))) = 0"
"length (filter ((=) q⇩f) (concat (map vars_term_list (take i ts)))) = 0" using wit(1) assms(2-)
by (auto simp: in_set_conv_nth simp flip: count_mset, metis in_mono less_trans nat_less_le singletonD)+
moreover have "length (filter ((=) q⇩i) (concat (map vars_term_list (drop (Suc i) ts)))) = 0"
"length (filter ((=) q⇩f) (concat (map vars_term_list (drop (Suc i) ts)))) = 0"
using wit(1) assms(2-) vars
by (auto simp: in_set_conv_nth simp flip: count_mset)
(metis Suc_diff_Suc Suc_less_eq add_Suc_right insert_Diff insert_iff insert_not_empty
le_add_diff_inverse lessI nat_add_left_cancel_less nat_less_le not_add_less1 subset_singleton_iff)+
moreover have "length (filter ((=) q⇩i) (vars_term_list (ts ! i))) = 1 ∨
length (filter ((=) q⇩f) (vars_term_list (ts ! i))) = 1"
proof (cases "q⇩i = q⇩f")
case True
then have "q⇩f |∈| ?A (ts ! i)" using wit(1, 3) trans(3) by auto
from Fun(1)[OF nth_mem[OF wit(1)] this] show ?thesis
by auto
next
case False
from semantic_path_rules_diff_states[OF _ assms(3) False, of ℱ "ts ! i"] show ?thesis
using Fun(1)[OF nth_mem[OF wit(1)]] trans(3) wit(1, 3)
by (auto simp: vars_term_list.simps)
qed
ultimately have "sum_list (map (length ∘ (filter ((=) q⇩i) ∘ vars_term_list)) (args ts (ts ! i) i)) = 1 ∨
sum_list (map (length ∘ (filter ((=) q⇩f) ∘ vars_term_list)) (args ts (ts ! i) i)) = 1"
by (auto simp: filter_concat vars_term_list.simps length_concat)
then show ?case using id_take_nth_drop[OF wit(1)]
by (auto simp: filter_concat vars_term_list.simps length_concat)
qed (auto simp: vars_term_list.simps)
lemma length_filter_vars_term:
assumes "length (filter ((=) q) (vars_term_list t)) = 0"
shows "q ∉ vars_term t" using assms
by (auto simp flip: count_mset)
lemma semantic_path_ta_der_only_if1:
assumes "length (filter ((=) q⇩f) (vars_term_list t)) = 1"
and "vars_term t ⊆ {q⇩f, q⇩c}" and "funas_term t ⊆ fset ℱ" and "q⇩c ≠ q⇩i"
shows "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) t"
using assms
proof (induct t)
case (Fun f ts)
from Fun(3, 5) have tr: "q⇩f ≠ q⇩i ⟹ length (filter ((=) q⇩i) (vars_term_list (Fun f ts))) = 0"
by auto (metis (mono_tags, lifting) Term.term.simps(18) empty_iff filter_False insertE set_vars_term_list subset_code(1))
from Fun(2, 3) obtain i where wit: "i < length ts"
"length (filter ((=) q⇩f) (vars_term_list (ts ! i))) = 1"
"length (filter ((=) q⇩i) (vars_term_list (ts ! i))) = 0 ∨ q⇩f = q⇩i"
"∀ j < length ts. j ≠ i ⟶ q⇩f ∉ vars_term (ts ! j)"
using sum_list_length1[of "map (length ∘ filter ((=) q⇩f) ∘ vars_term_list) ts"] tr
by (cases "q⇩f = q⇩i") (auto simp: vars_term_list.simps filter_concat length_concat comp_def simp flip: count_mset)
from Fun(1)[OF nth_mem[OF wit(1)]] wit(2, 3) Fun(3-)
have qf: "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) (ts ! i)"
by (auto simp add: UN_subset_iff wit(1))
have vars [simp]: "j < length ts ⟹ j ≠ i ⟹ vars_term (ts ! j) ⊆ {q⇩c}" for j
using wit(3, 4) Fun(3, 5) by (auto simp: UN_subset_iff all_set_conv_all_nth)
{fix j assume ass: "j < length ts" "j ≠ i"
from this Fun(4) vars have "q⇩c |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c) {||}) (ts ! j)"
apply (intro reflcl_st_reachable_only_if)
apply (auto simp: fvars_term.rep_eq ffunas_term.rep_eq less_eq_fset.rep_eq)
apply fastforce
done
from ta_der_el_mono[OF _ _ this] have "q⇩c |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) (ts ! j)"
by auto}
moreover have "f (replicate i q⇩c @ q⇩f # replicate (length ts - Suc i) q⇩c) → q⇩f |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f"
using wit(1) Fun(4)
by (auto simp: le_eq_less_or_eq min_def semantic_path_rules_fmember)
(metis nat_less_le notin_fset)
ultimately show ?case using wit(1) qf
by (auto simp: nth_append_Cons intro!: exI[of _ "replicate i q⇩c @ q⇩f # replicate (length ts - Suc i) q⇩c"])
qed (auto simp: vars_term_list.simps split: if_splits)
lemma semantic_path_ta_der_only_if2:
assumes "length (filter ((=) q⇩i) (vars_term_list t)) = 1" "length (filter ((=) q⇩f) (vars_term_list t)) = 0"
and "vars_term t ⊆ {q⇩i, q⇩c}" and "funas_term t ⊆ fset ℱ"
shows "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) t ∨ t = Var q⇩i"
using assms
proof (induct t)
case (Fun f ts)
from Fun(2, 3) obtain i where wit: "i < length ts"
"length (filter ((=) q⇩i) (vars_term_list (ts ! i))) = 1"
"length (filter ((=) q⇩f) (vars_term_list (ts ! i))) = 0"
"∀ j < length ts. j ≠ i ⟶ q⇩i ∉ vars_term (ts ! j)"
using sum_list_length1[of "map (length ∘ filter ((=) q⇩i) ∘ vars_term_list) ts"]
by (auto simp: vars_term_list.simps filter_concat length_concat comp_def simp flip: count_mset)
from Fun(1)[OF nth_mem[OF wit(1)]] wit(2, 3) Fun(3-)
have qf: "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) (ts ! i) ∨ ts ! i = Var q⇩i"
by (auto simp add: UN_subset_iff wit(1))
have vars [simp]: "j < length ts ⟹ j ≠ i ⟹ vars_term (ts ! j) ⊆ {q⇩c}" for j
using wit(3, 4) Fun(3, 4) by (auto simp: vars_term_list.simps UN_subset_iff all_set_conv_all_nth)
{fix j assume ass: "j < length ts" "j ≠ i"
from this Fun(5) vars have "q⇩c |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c) {||}) (ts ! j)"
by (intro reflcl_st_reachable_only_if') (auto simp: UN_subset_iff)
from ta_der_el_mono[OF _ _ this] have "q⇩c |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) (ts ! j)"
by auto} note qc = this
have qf': "f (replicate i q⇩c @ q⇩f # replicate (length ts - Suc i) q⇩c) → q⇩f |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f"
using wit(1) Fun(5) unfolding semantic_path_rules_fmember
by (rule_tac x = "length ts" in exI, rule_tac x = i in exI)
(auto simp: le_eq_less_or_eq min_def UN_subset_iff fmember.rep_eq)
have qi: "f (replicate i q⇩c @ q⇩i # replicate (length ts - Suc i) q⇩c) → q⇩f |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f"
using wit(1) Fun(5) unfolding semantic_path_rules_fmember
by (rule_tac x = "length ts" in exI, rule_tac x = i in exI)
(auto simp: le_eq_less_or_eq min_def UN_subset_iff fmember.rep_eq)
show ?case
proof (cases "ts ! i = Var q⇩i")
case True then show ?thesis using wit(1) qc qi
by (auto simp: nth_append_Cons intro!: exI[of _ "replicate i q⇩c @ q⇩i # replicate (length ts - Suc i) q⇩c"])
next
case False
then have "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) (ts ! i)" using qf
by auto
then show ?thesis using wit(1) qc qf'
by (auto simp: nth_append_Cons intro!: exI[of _ "replicate i q⇩c @ q⇩f # replicate (length ts - Suc i) q⇩c"])
qed
qed (auto simp: vars_term_list.simps simp flip: count_mset split: if_splits)
"gen_ctxt_closure_reg ℱ 𝒜 q_c q_f =">definition "gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f =
Reg {|q⇩f|} (TA (rules (ta 𝒜) |∪| ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f)
(eps (ta 𝒜) |∪| (λ p. (p, q⇩f)) |`| (fin 𝒜)))"
"fun_sig ℱ ⟷ (∃ (f, n) |∈| ℱ. 0 < n)"">definition "fun_sig ℱ ⟷ (∃ (f, n) |∈| ℱ. 0 < n)"
lemma fun_in_sig_nt_empty [simp]:
"fun_sig ℱ ⟹ ℱ ≠ {||}"
by (auto simp: fun_sig_def)
lemma semantic_path_rules_states [simp]:
"ℱ = {||} ⟹ rule_states (semantic_path_rules ℱ q⇩c q⇩i q⇩f) = {||}"
"fun_sig ℱ ⟹ q⇩f |∈| rule_states (semantic_path_rules ℱ q⇩c q⇩i q⇩f)"
"fun_sig ℱ ⟹ q⇩i |∈| rule_states (semantic_path_rules ℱ q⇩c q⇩i q⇩f)"
by (auto simp: rule_states_def semantic_path_rules_fmember' fBex_def fimage_iff fun_sig_def min_def) force+
lemma semantic_path_rules_subs_states:
"rule_states (semantic_path_rules ℱ q⇩c q⇩i q⇩f) |⊆| {|q⇩c, q⇩i, q⇩f|}"
by (auto simp: rule_states_def semantic_path_rules_fmember' min_def fset_of_list_elem)
lemma no_fun_gr_ctxt_hole:
assumes "¬ fun_sig ℱ" and "funas_gctxt C ⊆ fset ℱ"
shows "C = GHole" using assms notin_fset unfolding fun_sig_def
by (cases C) (fastforce simp: fBall_def)+
lemma ctxt_closure_fresh_q_sequential_derivation:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜"
and "fin 𝒜 |⊆| rule_states (rules (ta 𝒜)) |∪| eps_states (eps (ta 𝒜))" and "fun_sig ℱ"
shows "derivation_split (ta (gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f)) (rules (ta 𝒜)) (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f)
(eps (ta 𝒜)) {||} ((λ p. (p, q⇩f)) |`| (fin 𝒜))"
proof -
have st: "rule_states (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f) = {|q⇩c, q⇩f|}"
using semantic_path_rules_states(2)[OF assms(4)] assms(4)
using semantic_path_rules_subs_states[of ℱ q⇩c q⇩f q⇩f]
by auto
have "(λ p. (p, q⇩f)) |`| (fin 𝒜) |⊆| (rule_states (rules (ta 𝒜)) |∪| eps_states (eps (ta 𝒜))) |×|
(rule_states (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f))"
using assms(3) unfolding st by auto
then show ?thesis using assms unfolding derivation_split_def st
by (auto simp: gen_ctxt_closure_reg_def 𝒬_def)
qed
lemma gen_gctxt_closure_sound:
fixes 𝒜 :: "('q, 'f) reg"
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜" and "q⇩c ≠ q⇩f"
and "fin 𝒜 |⊆| rule_states (rules (ta 𝒜)) |∪| eps_states (eps (ta 𝒜))" and "fun_sig ℱ"
shows "ℒ (gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f) = {C⟨s⟩⇩G | C s. funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
(is "?Ls = ?Rs")
proof -
let ?A = "gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f"
interpret sq: derivation_split "ta ?A" "rules (ta 𝒜)" "ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f"
"eps (ta 𝒜)" "{||}" "(λ p. (p, q⇩f)) |`| (fin 𝒜)"
using ctxt_closure_fresh_q_sequential_derivation[OF assms(1, 2, 4-)] .
show ?thesis proof
{fix t assume "t ∈ ?Ls"
then have reach: "q⇩f |∈| ta_der (ta ?A) (term_of_gterm t)"
by (auto simp: gen_ctxt_closure_reg_def ℒ_def elim: gta_langE)
have [simp]: "ta_sig sq.ℬ = ℱ"
by (auto simp: ta_sig_def semantic_path_rules_fmember' min_def fimage_funion)
have st: "q⇩f |∈| sq.𝒬⇩B" using assms(5)
by (auto simp: 𝒬_def fun_sig_def semantic_path_rules_fmember)
from sq.ta_der_to_gmcxtx[OF reach this] obtain C ss qs qs' where
len : "length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss" and
reachA: "∀ i < length ss. qs ! i |∈| ta_der sq.𝒜 (term_of_gterm (ss ! i))" and
toB: "∀i<length ss. (qs ! i, qs' ! i) |∈| (λ p. (p, q⇩f)) |`| (fin 𝒜)" and
reachq: "q⇩f |∈| ta_der sq.ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs'))" and
mctxt: "funas_gmctxt C ⊆ fset ℱ ∧ fill_gholes C ss = t"
by auto
then have "filter ((=) q⇩f) qs' = qs'" using toB len
by (intro filter_True) (auto simp: in_set_conv_nth)
then have [simp]: "map Var qs' = [Var q⇩f]" and size1: "length ss = Suc 0"
using toB len reachq
using semantic_path_rules_der_if[OF _ assms(3) assms(3), of ℱ "fill_holes (mctxt_of_gmctxt C) (map Var qs')"]
by auto (metis Suc_length_conv length_0_conv list.simps(8) map_eq_Cons_conv nth_Cons_0)
obtain s where [simp]: "ss = [s]" using size1 by (cases ss) auto
have "t ∈ ?Rs" using len reachA toB reachq mctxt
by (auto simp: ℒ_def fill_gholes_apply_gctxt intro!: exI[of _ "gctxt_of_gmctxt C"] exI[of _ "s"])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix t assume "t ∈ ?Rs"
then obtain C s where sp: "t = C⟨s⟩⇩G" "funas_gctxt C ⊆ fset ℱ" "s ∈ ℒ 𝒜" by auto
have [simp]: "fin (gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f) = {|q⇩f|}"
by (auto simp: gen_ctxt_closure_reg_def)
from sp(3) ta_der_el_mono[of "ta 𝒜" "ta ?A"]
obtain p where "p |∈| fin 𝒜" and "p |∈| ta_der (ta ?A) (term_of_gterm s)"
by (auto simp: gen_ctxt_closure_reg_def ℒ_def sup_assoc elim!: gta_langE)
from ta_der_eps[OF _ this(2), of q⇩f] this(1) have res: "q⇩f |∈| ta_der (ta ?A) (term_of_gterm s)"
by (auto simp: gen_ctxt_closure_reg_def)
from sp(2, 3) have mon: "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f) {||}) (ctxt_of_gctxt C)⟨Var q⇩f⟩"
using semantic_path_ta_der_only_if1[OF _ _ _ assms(3), of q⇩f "(ctxt_of_gctxt C)⟨Var q⇩f⟩" ℱ]
by (auto simp: vars_term_list.simps simp flip: set_vars_term_list)
then have "q⇩f |∈| ta_der (ta ?A) (ctxt_of_gctxt C)⟨Var q⇩f⟩"
by (intro ta_der_el_mono[OF _ _ mon]) (auto simp: gen_ctxt_closure_reg_def)
from ta_der_ctxt[OF res this] have "t ∈ ?Ls" unfolding sp(1) ℒ_def
by (auto intro!: gta_langI)
(metis ctxt_of_gctxt_inv ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply_gterm)}
then show "?Rs ⊆ ?Ls" by blast
qed
qed
lemma gen_ctxt_closure_sound:
fixes 𝒜 :: "('q, 'f) reg"
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜" and "q⇩c ≠ q⇩f"
and "fin 𝒜 |⊆| rule_states (rules (ta 𝒜)) |∪| eps_states (eps (ta 𝒜))" and "fun_sig ℱ"
shows "ℒ (gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f) =
{(gterm_of_term :: ('f, 'q) term ⇒ 'f gterm) C⟨term_of_gterm s⟩ | C s. ground_ctxt C ∧ funas_ctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
unfolding gen_gctxt_closure_sound[OF assms]
by (metis (no_types, lifting) Collect_cong ctxt_of_gctxt_apply funas_ctxt_of_gctxt_conv funas_gctxt_of_ctxt ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply_gterm term_of_gterm_inv)
"ctxt_closure_reg ℱ 𝒜 =">definition "ctxt_closure_reg ℱ 𝒜 =
(let ℬ = fmap_states_reg CInl (refin_fin_reg 𝒜) in
(if ¬ fun_sig ℱ then ℬ else gen_ctxt_closure_reg ℱ ℬ (Inr False) (Inr True)))"
lemma ℒ_sum_conv [simp]:
"ℒ (fmap_states_reg CInl 𝒜) = ℒ 𝒜"
using inj_Inl unfolding fmap_states_reg_def
by (simp add: ℒ_def finj_CInl_CInr(1) fmap_states_ta_lang2)
lemma gctxt_closure_lang:
shows "ℒ (ctxt_closure_reg ℱ 𝒜) =
{ C⟨s⟩⇩G | C s. funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
proof (cases "fun_sig ℱ")
case True
let ?B = "fmap_states_reg CInl (refin_fin_reg 𝒜)"
have ts: "Inr False |∉| 𝒬⇩r ?B" "Inr True |∉| 𝒬⇩r ?B"
by (auto simp: fmap_states_reg_def fmap_states_ta_def' 𝒬_def rule_states_def)
have "fin ?B |⊆| rule_states (rules (ta ?B)) |∪| eps_states (eps (ta ?B))"
apply (auto simp: comp_def ta_rule.map_sel(3) fmap_states_reg_def fimage_iff
refin_fin_reg_def 𝒬_def eps_states_def rule_states_def fmap_states_ta_def fBex_def)
apply (metis fset_of_list_map rev_fimage_eqI ta_rule.map_sel(2))
by blast+
from gen_gctxt_closure_sound[OF ts _ this True] show ?thesis using True
by (simp add: ctxt_closure_reg_def)
next
case False then show ?thesis
by (auto simp: ctxt_closure_reg_def dest: no_fun_gr_ctxt_hole intro!: exI[of _ GHole])
qed
lemma ctxt_closure_lang:
shows "ℒ (ctxt_closure_reg ℱ 𝒜) =
{(gterm_of_term :: ('f, 'q + bool) term ⇒ 'f gterm) C⟨term_of_gterm s⟩ |
C s. ground_ctxt C ∧ funas_ctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
unfolding gctxt_closure_lang
by (metis (mono_tags, hide_lams) ctxt_of_gctxt_inv funas_gctxt_of_ctxt ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply_gterm term_of_gterm_inv)
"gen_mctxt_closure_reg ℱ 𝒜 q_c q_f = ">definition "gen_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩f =
Reg {|q⇩f|} (TA (rules (ta 𝒜) |∪| ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f)
(eps (ta 𝒜) |∪| (λ p. (p, q⇩f)) |`| (fin 𝒜) |∪| {|(q⇩f, q⇩c)|}))"
lemma mctxt_closure_fresh_q_sequential_derivation:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜"
and "fin 𝒜 |⊆| 𝒬⇩r 𝒜" and "fun_sig ℱ"
shows "derivation_split (ta (gen_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩f)) (rules (ta 𝒜)) (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f)
(eps (ta 𝒜)) {|(q⇩f, q⇩c)|} ((λ p. (p, q⇩f)) |`| (fin 𝒜))"
proof -
have st: "rule_states (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f) = {|q⇩c, q⇩f|}"
using semantic_path_rules_states(2)[OF assms(4)] semantic_path_rules_subs_states[of ℱ q⇩c q⇩f q⇩f]
using rule_states_refl[of ℱ q⇩c]
by (cases "ℱ = {||}") (auto simp add: assms(4))
have "(λ p. (p, q⇩f)) |`| (fin 𝒜) |⊆| 𝒬⇩r 𝒜 |×| ({|q⇩c, q⇩f|} |∪| eps_states {|(q⇩f, q⇩c)|})"
using assms(3) unfolding st by auto
then show ?thesis using assms unfolding derivation_split_def st
by (auto simp: gen_mctxt_closure_reg_def 𝒬_def)
qed
lemma mctxt_fin_one_occurence:
assumes "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {|(q⇩i, q⇩c)|}) t"
and "q⇩c ≠ q⇩i" "q⇩c ≠ q⇩f"
shows "q⇩i ∈ vars_term t ∨ q⇩f ∈ vars_term t" using assms(1)
proof (induct t)
case (Fun f ts)
let ?A = "ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {|(q⇩i, q⇩c)|})"
from Fun(2) assms(2-) obtain qs where trans: "TA_rule f qs q⇩f |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f" "length qs = length ts"
"∀ i < length ts. (qs ! i) |∈| ?A (ts ! i)"
by (auto simp: ta_relfcl_rules_def)
from trans have "∃ i < length ts. (qs ! i = q⇩f ∨ qs ! i = q⇩i) ∧ (∀ j < length ts. j ≠ i ⟶ qs ! j = q⇩c)"
by (auto simp: semantic_path_rules_fmember min_def nth_append_Cons)
then obtain i where wit: "i < length ts" "∀ j < length ts. j ≠ i ⟶ qs ! j = q⇩c" "qs ! i = q⇩f ∨ qs ! i = q⇩i"
by blast
show ?case
proof (cases "qs ! i = q⇩i ∧ q⇩i ≠ q⇩f")
case [simp]: True
from trans have "q⇩i |∈| ?A (ts ! i)" using wit by auto
then have "ts ! i = Var q⇩i" using assms(2-) True
by (cases "ts ! i", auto simp: ta_relfcl_rules_def semantic_path_rules_fmember min_def nth_append_Cons)
then show ?thesis using wit(1) by (metis UN_I nth_mem term.set(4) term.set_intros(3))
next
case False
then show ?thesis using Fun(1)[OF nth_mem[OF wit(1)]] trans(3) wit by auto
qed
qed (auto simp: vars_term_list.simps)
lemma gen_gmctxt_closure_lang:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜" and "q⇩c ≠ q⇩f"
and "fin 𝒜 |⊆| 𝒬⇩r 𝒜" and "fun_sig ℱ"
shows "ℒ (gen_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩f) =
{ fill_gholes C ss |
C ss. 0 < num_gholes C ∧ num_gholes C = length ss ∧
funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
(is "?Ls = ?Rs")
proof -
let ?A = "gen_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩f"
interpret sq: derivation_split "ta (gen_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩f)" "rules (ta 𝒜)"
"ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f" "eps (ta 𝒜)" "{|(q⇩f, q⇩c)|}" "(λ p. (p, q⇩f)) |`| (fin 𝒜)"
using mctxt_closure_fresh_q_sequential_derivation[OF assms(1, 2, 4-)] .
show ?thesis proof
{fix t assume "t ∈ ?Ls"
then have reach: "q⇩f |∈| ta_der (ta ?A) (term_of_gterm t)"
by (auto simp: gen_mctxt_closure_reg_def ℒ_def elim: gta_langE)
have [simp]: "ta_sig sq.ℬ = ℱ"
by (auto simp: ta_sig_def semantic_path_rules_fmember' min_def fimage_funion)
have st: "q⇩f |∈| sq.𝒬⇩B" using assms(5)
by (auto simp: 𝒬_def fun_sig_def semantic_path_rules_def)
from sq.ta_der_to_gmcxtx[OF reach this] obtain C ss qs qs' where
len : "length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss" and
reachA: "∀ i < length ss. qs ! i |∈| ta_der sq.𝒜 (term_of_gterm (ss ! i))" and
toB: "∀i<length ss. (qs ! i, qs' ! i) |∈| (λ p. (p, q⇩f)) |`| (fin 𝒜)" and
reachq: "q⇩f |∈| ta_der sq.ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs'))" and
mctxt: "funas_gmctxt C ⊆ fset ℱ ∧ fill_gholes C ss = t"
by auto
let ?C' = "mctxt_of_gmctxt C"
have "0 < length qs'" using toB len reachq
using mctxt_fin_one_occurence[OF _ assms(3, 3), of ℱ "fill_holes ?C' (map Var qs')"]
by auto
then have "t ∈ ?Rs" using len reachA toB reachq mctxt
by (auto simp: ℒ_def intro!: exI[of _ C] exI[of _ ss])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix t assume "t ∈ ?Rs"
then obtain C ss where len: "0 < num_gholes C" "num_gholes C = length ss" and
gr_fun: "funas_gmctxt C ⊆ fset ℱ" and
reachA: "∀ i < length ss. ss ! i ∈ ℒ 𝒜" and
const: "t = fill_gholes C ss"
by auto
let ?C' = "mctxt_of_gmctxt C"
{fix i assume ass: "i < length ss"
then obtain p where p: "p |∈| fin 𝒜" "p |∈| ta_der (ta ?A) (term_of_gterm (ss ! i))"
using reachA len gta_langE unfolding ℒ_def
by (metis (no_types, lifting) fin_mono sq.ta_der_monos(1) ta.collapse)
have eps: "(p, q⇩f) |∈| (eps (ta ?A))|⇧+|" "(p, q⇩c) |∈| (eps (ta ?A))|⇧+|" using p(1)
by (auto simp: gen_mctxt_closure_reg_def)
(smt fimage_finsert finsertI1 funion_finsert_left in_ftrancl_UnI not_ftrancl_into set_finsert sq.trancl_AB)
from p(2) ta_der_trancl_eps[OF eps(1)] ta_der_trancl_eps[OF eps(2)]
have "i = 0 ⟹ q⇩f |∈| ta_der (ta ?A) (term_of_gterm (ss ! i))"
"i ≠ 0 ⟹ q⇩c |∈| ta_der (ta ?A) (term_of_gterm (ss ! i))"
by auto} note a_deriv = this
let ?S = "q⇩f # replicate (length ss - 1) q⇩c"
have l: "num_gholes C = length ?S" using len by auto
from mctxt_args_ta_der'[of ?C' ?S "map term_of_gterm ss" "ta ?A"] a_deriv
have mid: "fill_holes ?C' (map Var ?S) |∈| ta_der' (ta ?A) (fill_holes ?C' (map term_of_gterm ss))"
using len by (auto simp: nth_Cons')
have "length (filter ((=) q⇩f) (vars_term_list (fill_holes ?C' (map Var ?S)))) = 1"
"vars_term (fill_holes (mctxt_of_gmctxt C) (map Var (q⇩f # replicate (length ss - 1) q⇩c))) ⊆ {q⇩f, q⇩c}"
using l assms(3) vars_term_list_fill_holes[of ?C' ?S]
by auto
from semantic_path_ta_der_only_if1[OF this _ assms(3)] gr_fun l assms(3)
have mon: "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f) {||}) (fill_holes ?C' (map Var ?S))"
using funas_mctxt_of_gmctxt_conv
by (auto simp: funas_mctxt_fill_holes l split!: if_splits) fastforce
have "q⇩f |∈| ta_der (ta ?A) (fill_holes ?C' (map Var ?S))"
by (intro ta_der_el_mono[OF _ _ mon]) (auto simp: gen_mctxt_closure_reg_def)
then have "q⇩f |∈| ta_der (ta ?A) (term_of_gterm t)" using mid
by (auto simp: gr_fun(1) ground_fill_holes len(2) const ta_der'_ta_der
fill_holes_mctxt_of_gmctxt_to_fill_gholes)
then have "t ∈ ?Ls" by (auto simp: gen_mctxt_closure_reg_def ℒ_def intro: gta_langI)}
then show "?Rs ⊆ ?Ls" by blast
qed
qed
"mctxt_closure_reg ℱ 𝒜 =">definition "mctxt_closure_reg ℱ 𝒜 =
(let ℬ = fmap_states_reg Inl (refin_fin_reg 𝒜) in
(if ¬ fun_sig ℱ then ℬ else gen_mctxt_closure_reg ℱ ℬ (CInr False) (CInr True)))"
lemma no_fun_gr_mctxt_hole [simp]:
assumes "¬ fun_sig ℱ" and "funas_gmctxt C ⊆ fset ℱ" "0 < num_gholes C"
shows "C = GMHole" using assms unfolding fun_sig_def
by (cases C) (force simp: fBall_def fmember.rep_eq)+
lemma gmctxt_closure_lang:
"ℒ (mctxt_closure_reg ℱ 𝒜) =
{ fill_gholes C ss | C ss. num_gholes C = length ss ∧ 0 < num_gholes C ∧
funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
(is "?Ls = ?Rs")
proof (cases "fun_sig ℱ")
case True
let ?B = "fmap_states_reg Inl (refin_fin_reg 𝒜)"
have ts: "CInr False |∉| 𝒬⇩r ?B" "CInr True |∉| 𝒬⇩r ?B"
by (auto simp: fmap_states_reg_def)
have "fin ?B |⊆| 𝒬⇩r ?B"
by (intro fmap_states_reg_refin_fin_reg_fin) (simp add: finj_on.rep_eq)
from gen_gmctxt_closure_lang[OF ts _ this True] show ?thesis using True
by (simp add: mctxt_closure_reg_def) blast
next
case False
{fix t assume "t ∈ ?Ls" then have "t ∈ ?Rs" using False
by (auto simp: mctxt_closure_reg_def intro!: exI[of _ GMHole] exI[of _ "[t]"])}
moreover
{fix t assume "t ∈ ?Rs" then have "t ∈ ?Ls" using False
by (auto simp: mctxt_closure_reg_def dest!: no_fun_gr_mctxt_hole intro!: exI[of _ MHole])}
ultimately show ?thesis by blast
qed
"gen_nhole_ctxt_closure_reg ℱ 𝒜 q_c q_i q_f =">definition "gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f =
Reg {|q⇩f|} (TA (rules (ta 𝒜) |∪| ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f)
(eps (ta 𝒜) |∪| (λ p. (p, q⇩i)) |`| (fin 𝒜)))"
"gen_nhole_mctxt_closure_reg ℱ 𝒜 q_c q_i q_f =">definition "gen_nhole_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f =
Reg {|q⇩f|} (TA (rules (ta 𝒜) |∪| ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f)
(eps (ta 𝒜) |∪| (λ p. (p, q⇩i)) |`| (fin 𝒜) |∪| {|(q⇩i, q⇩c)|}))"
lemma nhole_rule_states_B [simp]:
assumes "fun_sig ℱ"
shows "rule_states (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) = {|q⇩c, q⇩i, q⇩f|}"
using assms semantic_path_rules_subs_states[of ℱ q⇩c q⇩i q⇩f]
by auto
lemma gen_nhole_ctxt_closure_automaton_sequential_derivation:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩i |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜"
and "fin 𝒜 |⊆| 𝒬⇩r 𝒜" and "fun_sig ℱ"
shows "derivation_split (ta (gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f)) (rules (ta 𝒜))
(ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f)
(eps (ta 𝒜)) {||} ((λ p. (p, q⇩i)) |`| (fin 𝒜))"
proof -
have "(λ p. (p, q⇩i)) |`| (fin 𝒜) |⊆| 𝒬⇩r 𝒜 |×| (rule_states (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f))"
using assms(4) unfolding nhole_rule_states_B[OF assms(5)] by auto
then show ?thesis using assms unfolding derivation_split_def nhole_rule_states_B[OF assms(5)]
by (auto simp: gen_nhole_ctxt_closure_reg_def 𝒬_def)
qed
lemma gen_nhole_gctxt_closure_lang:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" "q⇩i |∉| 𝒬⇩r 𝒜" "q⇩f |∉| 𝒬⇩r 𝒜"
and "q⇩c ≠ q⇩i" "q⇩c ≠ q⇩f" "q⇩i ≠ q⇩f"
and "fin 𝒜 |⊆| 𝒬⇩r 𝒜" and "fun_sig ℱ"
shows "ℒ (gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f) =
{ C⟨s⟩⇩G | C s. C ≠ GHole ∧ funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
(is "?Ls = ?Rs")
proof -
let ?A = "gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f"
interpret sq: derivation_split "ta (gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f)" "rules (ta 𝒜)"
"ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f" "eps (ta 𝒜)" "{||}" "(λ p. (p, q⇩i)) |`| (fin 𝒜)"
using gen_nhole_ctxt_closure_automaton_sequential_derivation[OF assms(1 - 3, 7-)] .
show ?thesis proof
{fix t assume "t ∈ ?Ls"
then have reach: "q⇩f |∈| ta_der (ta ?A) (term_of_gterm t)"
by (auto simp: gen_nhole_ctxt_closure_reg_def ℒ_def elim: gta_langE)
have [simp]: "ta_sig sq.ℬ = ℱ"
by (auto simp: ta_sig_def semantic_path_rules_fmember' min_def fimage_funion)
have st: "q⇩f |∈| sq.𝒬⇩B" using assms(8)
by (auto simp: 𝒬_def fun_sig_def)
from sq.ta_der_to_gmcxtx[OF reach this] obtain C ss qs qs' where
len : "length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss" and
reachA: "∀ i < length ss. qs ! i |∈| ta_der sq.𝒜 (term_of_gterm (ss ! i))" and
toB: "∀i<length ss. (qs ! i, qs' ! i) |∈| (λ p. (p, q⇩i)) |`| (fin 𝒜)" and
reachq: "q⇩f |∈| ta_der sq.ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs'))" and
mctxt: "funas_gmctxt C ⊆ fset ℱ ∧ fill_gholes C ss = t"
by auto
then have id: "filter ((=) q⇩i) qs' = qs'" using toB len
by (intro filter_True) (auto simp: in_set_conv_nth)
then have "length (filter ((=) q⇩f) qs') = 0" using assms(4 - 6)
by (auto simp flip: count_mset simp add: filter_id_conv)
then have *[simp]: "map Var qs' = [Var q⇩i]" and size1: "length ss = Suc 0" using toB len reachq
using semantic_path_rules_der_if[OF _ assms(5, 4), of ℱ "fill_holes (mctxt_of_gmctxt C) (map Var qs')"] id
by (auto simp: conjunct1[OF mctxt] vars_term_list.simps comp_def)
(metis (no_types, lifting) length_0_conv length_Suc_conv length_nth_simps(3) list.simps(8, 9))
then have nt: "C ≠ GMHole" using reachq assms(6) by auto
obtain s where [simp]: "ss = [s]" using len *
by (metis Suc_length_conv length_0_conv size1)
have "t ∈ ?Rs" using len reachA toB reachq mctxt nt
by (auto simp: fill_gholes_apply_gctxt gctxt_of_gmctxt_hole_dest ℒ_def
intro!: exI[of _ "gctxt_of_gmctxt C"] exI[of _ s])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix t assume "t ∈ ?Rs"
then obtain C s where sp: "t = C⟨s⟩⇩G" "C ≠ GHole"
"funas_gctxt C ⊆ fset ℱ" "s ∈ ℒ 𝒜" by auto
from sp(4) ta_der_el_mono[of "ta 𝒜"]
obtain p where "p |∈| fin 𝒜" and "p |∈| ta_der (ta ?A) (term_of_gterm s)"
by (auto simp: gen_nhole_ctxt_closure_reg_def ℒ_def sup_assoc)
from ta_der_eps[OF _ this(2), of q⇩i] this(1)
have res: "q⇩i |∈| ta_der (ta ?A) (term_of_gterm s)"
by (auto simp: gen_nhole_ctxt_closure_reg_def)
let ?C = "ctxt_of_gctxt C"
have *:"length (filter ((=) q⇩i) (vars_term_list (ctxt_of_gctxt C)⟨Var q⇩i⟩)) = 1"
"length (filter ((=) q⇩f) (vars_term_list (ctxt_of_gctxt C)⟨Var q⇩i⟩)) = 0"
using assms(6) by (auto simp: vars_term_list.simps)
have **: "funas_term (ctxt_of_gctxt C)⟨Var q⇩i⟩ ⊆ fset ℱ"
using sp(3) by auto
have mon: "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) ?C⟨Var q⇩i⟩"
using semantic_path_ta_der_only_if2[OF * _ **] sp(2)
by (cases C) (auto simp: vars_term_ctxt_apply)
then have "q⇩f |∈| ta_der (ta ?A) ?C⟨Var q⇩i⟩"
by (intro ta_der_el_mono[OF _ _ mon]) (auto simp: gen_nhole_ctxt_closure_reg_def)
from ta_der_ctxt[OF res this] have "t ∈ ?Ls" unfolding sp(1) ℒ_def
by (intro gta_langI[of q⇩f], simp add: gen_nhole_ctxt_closure_reg_def)
(metis ctxt_of_gctxt_inv ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply_gterm)}
then show "?Rs ⊆ ?Ls" by blast
qed
qed
lemma gen_nhole_mctxt_closure_sequential_derivation:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩i |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜"
and "fin 𝒜 |⊆| 𝒬⇩r 𝒜" and "fun_sig ℱ"
shows "derivation_split (ta (gen_nhole_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f)) (rules (ta 𝒜))
(ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f)
(eps (ta 𝒜)) {|(q⇩i, q⇩c)|} ((λ p. (p, q⇩i)) |`| (fin 𝒜))"
proof -
have "(λ p. (p, q⇩i)) |`| (fin 𝒜) |⊆| 𝒬⇩r 𝒜 |×| (rule_states (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f))"
using assms(4) unfolding nhole_rule_states_B[OF assms(5)] by auto
then show ?thesis using assms unfolding derivation_split_def nhole_rule_states_B[OF assms(5)]
by (auto simp: gen_nhole_mctxt_closure_reg_def 𝒬_def)
qed
lemma gen_nhole_gmctxt_closure_lang:
assumes "q⇩c |∉| 𝒬⇩r 𝒜" "q⇩i |∉| 𝒬⇩r 𝒜" "q⇩f |∉| 𝒬⇩r 𝒜"
and "q⇩c ≠ q⇩i" "q⇩c ≠ q⇩f" "q⇩i ≠ q⇩f"
and "fin 𝒜 |⊆| 𝒬⇩r 𝒜" and "fun_sig ℱ"
shows "ℒ (gen_nhole_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f) =
{ fill_gholes C ss | C ss. 0 < num_gholes C ∧ num_gholes C = length ss ∧ C ≠ GMHole ∧
funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
(is "?Ls = ?Rs")
proof -
let ?A = "gen_nhole_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f"
interpret sq: derivation_split "ta (gen_nhole_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f)" "rules (ta 𝒜)"
"ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f" "eps (ta 𝒜)" "{|(q⇩i, q⇩c)|}"
"(λ p. (p, q⇩i)) |`| (fin 𝒜)"
using gen_nhole_mctxt_closure_sequential_derivation[OF assms(1 - 3, 7-)] .
show ?thesis proof
{fix t assume "t ∈ ?Ls"
then have reach: "q⇩f |∈| ta_der (ta ?A) (term_of_gterm t)"
by (auto simp: gen_nhole_mctxt_closure_reg_def ℒ_def elim: gta_langE)
have [simp]: "ta_sig sq.ℬ = ℱ"
by (auto simp: ta_sig_def semantic_path_rules_fmember' min_def fimage_funion)
have st: "q⇩f |∈| sq.𝒬⇩B" using assms(8)
by (auto simp: 𝒬_def fun_sig_def)
from sq.ta_der_to_gmcxtx[OF reach this] obtain C ss qs qs' where
len : "length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss" and
reachA: "∀ i < length ss. qs ! i |∈| ta_der sq.𝒜 (term_of_gterm (ss ! i))" and
toB: "∀i<length ss. (qs ! i, qs' ! i) |∈|(λ p. (p, q⇩i)) |`| (fin 𝒜)" and
reachq: "q⇩f |∈| ta_der sq.ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs'))" and
mctxt: "funas_gmctxt C ⊆ fset ℱ ∧ fill_gholes C ss = t" by auto
then have der: "0 < length qs'" using toB len reachq assms(4)
using mctxt_fin_one_occurence[OF _ _ assms(5), of ℱ q⇩i "fill_holes (mctxt_of_gmctxt C) (map Var qs')"]
by auto
{assume ass:"C = GMHole" then obtain q where [simp]: "qs' = [q]"
using len by auto (metis length_0_conv length_Suc_conv)
have False using reachq assms(4 - 6) toB len ass
by (auto simp: fill_holes_MHole elim!: rtranclE) force}
then have "C ≠ GMHole" by blast
then have "t ∈ ?Rs" using len reachA toB reachq mctxt assms(6) der
by (auto simp: ℒ_def intro!: exI[of _ C] exI[of _ ss])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix t assume "t ∈ ?Rs"
then obtain C ss where len: "0 < num_gholes C" "num_gholes C = length ss" and
gr_fun: "funas_gmctxt C ⊆ fset ℱ" "C ≠ GMHole" and
reachA: "∀ i < length ss. ss ! i ∈ ℒ 𝒜" and
const: "t = fill_gholes C ss"
by auto
{fix i assume ass: "i < length ss"
then obtain p where p: "p |∈| fin 𝒜" "p |∈| ta_der (ta ?A) (term_of_gterm (ss ! i))"
using len sq.ta_der_monos(1) unfolding ℒ_def
using all_nth_imp_all_set[OF reachA nth_mem[OF ass]]
by (auto simp: ℒ_def elim!: gta_langE)
have eps: "(p, q⇩i) |∈| (eps (ta ?A))|⇧+|" "(p, q⇩c) |∈| (eps (ta ?A))|⇧+|" using p(1)
by (auto simp: gen_nhole_mctxt_closure_reg_def)
(smt fimage_finsert finsertI1 finsert_fsubset fr_into_trancl funion_finsert_left inf_sup_ord(4) mk_disjoint_finsert not_ftrancl_into)
from p(2) ta_der_trancl_eps[OF eps(1)] ta_der_trancl_eps[OF eps(2)]
have "i = 0 ⟹ q⇩i |∈| ta_der (ta ?A) (term_of_gterm (ss ! i))"
"i ≠ 0 ⟹ q⇩c |∈| ta_der (ta ?A) (term_of_gterm (ss ! i))"
by auto} note a_deriv = this
let ?S = "q⇩i # replicate (length ss - 1) q⇩c" let ?C = "mctxt_of_gmctxt C"
let ?T = "fill_holes ?C (map Var ?S)"
have l: "num_holes ?C = length ?S" using len by auto
from mctxt_args_ta_der'[of ?C ?S "map term_of_gterm ss" "ta ?A"] a_deriv
have mid: "?T |∈| ta_der' (ta ?A) (fill_holes ?C (map term_of_gterm ss))"
using len by (auto simp: nth_Cons')
have "length (filter ((=) q⇩i) (vars_term_list ?T)) = 1"
"length (filter ((=) q⇩f) (vars_term_list ?T)) = 0"
"vars_term ?T ⊆ {q⇩i, q⇩c}" "funas_term ?T ⊆ fset ℱ"
using gr_fun l assms(4 - 6)
unfolding vars_term_list_fill_holes[OF ground_mctxt_of_gmctxt l]
by (auto simp: funas_mctxt_fill_holes funas_mctxt_of_gmctxt_conv)
from semantic_path_ta_der_only_if2[OF this] gr_fun l assms(4 - 6) len
have mon: "q⇩f |∈| ta_der (TA (ta_relfcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f) {||}) (fill_holes ?C (map Var ?S))"
by (cases C) auto
have "q⇩f |∈| ta_der (ta ?A) (fill_holes ?C (map Var ?S))"
by (intro ta_der_el_mono[OF _ _ mon]) (auto simp: gen_nhole_mctxt_closure_reg_def)
then have "q⇩f |∈| ta_der (ta ?A) (term_of_gterm t)" using mid
by (simp add: fill_holes_mctxt_of_gmctxt_to_fill_gholes len(2) local.const ta_der'_ta_der)
then have "t ∈ ?Ls" by (auto simp: gen_nhole_mctxt_closure_reg_def ℒ_def intro: gta_langI)}
then show "?Rs ⊆ ?Ls" by blast
qed
qed
datatype cl_states = cl_state | tr_state | fin_state | fin_clstate
derive compare_order cl_states
"nhole_ctxt_closure_reg ℱ 𝒜 =">definition "nhole_ctxt_closure_reg ℱ 𝒜 =
(let ℬ = fmap_states_reg CInl (refin_fin_reg 𝒜) in
(if ¬ fun_sig ℱ then Reg {||} (TA {||} {||}) else
gen_nhole_ctxt_closure_reg ℱ ℬ (CInr cl_state) (CInr tr_state) (CInr fin_state)))"
"nhole_mctxt_closure_reg ℱ 𝒜 =">definition "nhole_mctxt_closure_reg ℱ 𝒜 =
(let ℬ = fmap_states_reg CInl (refin_fin_reg 𝒜) in
(if ¬ fun_sig ℱ then Reg {||} (TA {||} {||}) else
gen_nhole_mctxt_closure_reg ℱ ℬ (CInr cl_state) (CInr tr_state) (CInr fin_state)))"
lemma nhole_ctxtcl_lang:
"ℒ (nhole_ctxt_closure_reg ℱ 𝒜) =
{ C⟨s⟩⇩G | C s. C ≠ GHole ∧ funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
(is "?Ls = ?Rs")
proof (cases "fun_sig ℱ")
case True
let ?B = "fmap_states_reg Inl (refin_fin_reg 𝒜)"
have ts: "CInr cl_state |∉| 𝒬⇩r ?B" "CInr tr_state |∉| 𝒬⇩r ?B" "CInr fin_state |∉| 𝒬⇩r ?B"
by (auto simp: fmap_states_reg_def)
have "fin ?B |⊆| 𝒬⇩r ?B"
by (intro fmap_states_reg_refin_fin_reg_fin) (simp add: finj_on.rep_eq)
from gen_nhole_gctxt_closure_lang[OF ts _ _ _ this True] show ?thesis using True
by (auto simp add: nhole_ctxt_closure_reg_def)
next
case False then show ?thesis
by (auto simp: nhole_ctxt_closure_reg_def ℒ_def dest: no_fun_gr_ctxt_hole)
qed
lemma nhole_gmctxt_closure_lang:
"ℒ (nhole_mctxt_closure_reg ℱ 𝒜) =
{ fill_gholes C ss | C ss. num_gholes C = length ss ∧ 0 < num_gholes C ∧ C ≠ GMHole ∧
funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
(is "?Ls = ?Rs")
proof (cases "fun_sig ℱ")
case True
let ?B = "fmap_states_reg Inl (refin_fin_reg 𝒜)"
have ts: "CInr cl_state |∉| 𝒬⇩r ?B" "CInr tr_state |∉| 𝒬⇩r ?B" "CInr fin_state |∉| 𝒬⇩r ?B"
by (auto simp: fmap_states_reg_def)
have f: "fin ?B |⊆| 𝒬⇩r ?B"
by (intro fmap_states_reg_refin_fin_reg_fin) (simp add: finj_on.rep_eq)
show ?thesis
by (auto simp: nhole_mctxt_closure_reg_def True gen_nhole_gmctxt_closure_lang[OF ts _ _ _ f True])
next
case False then show ?thesis
by (auto simp: nhole_mctxt_closure_reg_def ℒ_def dest: no_fun_gr_ctxt_hole)
qed
"nhole_mctxt_reflcl_reg ℱ 𝒜 =">definition "nhole_mctxt_reflcl_reg ℱ 𝒜 =
reg_union (nhole_mctxt_closure_reg ℱ 𝒜) (Reg {|Inr fin_clstate|} (TA (ta_relfcl_rules ℱ (Inr fin_clstate)) {||}))"
lemma nhole_mctxt_reflcl_lang:
"ℒ (nhole_mctxt_reflcl_reg ℱ 𝒜) = ℒ (nhole_mctxt_closure_reg ℱ 𝒜) ∪ 𝒯⇩G (fset ℱ)"
proof -
let ?refl = "Reg {|Inr fin_clstate|} (TA (ta_relfcl_rules ℱ (Inr fin_clstate)) {||})"
{fix t assume "t ∈ ℒ ?refl" then have "t ∈ 𝒯⇩G (fset ℱ)"
using reflcl_st_reachable_if[of "Inr fin_clstate :: 'a + cl_states" ℱ "term_of_gterm t"]
by (auto simp: ℒ_def 𝒯⇩G_equivalent_def elim!: gta_langE)
(metis ffunas_gterm.rep_eq ffunas_term_of_gterm_conv less_eq_fset.rep_eq reflcl_st_reachable_if subsetD)}
moreover
{fix t assume "t ∈ 𝒯⇩G (fset ℱ)" then have "t ∈ ℒ ?refl"
using reflcl_st_reachable_only_if[of "term_of_gterm t" ℱ "Inr fin_clstate :: 'a + cl_states"]
by (auto intro!: gta_langI simp: funas_term_of_gterm_conv ℒ_def 𝒯⇩G_equivalent_def
ffunas_gterm.rep_eq ffunas_term_of_gterm_conv less_eq_fset.rep_eq reflcl_st_reachable_only_if)}
ultimately have *: "ℒ (Reg {|Inr fin_clstate|} (TA (ta_relfcl_rules ℱ (Inr fin_clstate)) {||})) = 𝒯⇩G (fset ℱ)"
by blast
show ?thesis unfolding nhole_mctxt_reflcl_reg_def ℒ_union * by simp
qed
end