theory GTT_Transitive_Closure imports GTT_Compose begin inductive_set Δ_trancl_set :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for A B where Δ_set_cong: "TA_rule f ps p |∈| rules A ⟹ TA_rule f qs q |∈| rules B ⟹ length ps = length qs ⟹ (⋀i. i < length qs ⟹ (ps ! i, qs ! i) ∈ Δ_trancl_set A B) ⟹ (p, q) ∈ Δ_trancl_set A B" | Δ_set_eps1: "(p, p') |∈| eps A ⟹ (p, q) ∈ Δ_trancl_set A B ⟹ (p', q) ∈ Δ_trancl_set A B" | Δ_set_eps2: "(q, q') |∈| eps B ⟹ (p, q) ∈ Δ_trancl_set A B ⟹ (p, q') ∈ Δ_trancl_set A B" | Δ_set_trans: "(p, q) ∈ Δ_trancl_set A B ⟹ (q, r) ∈ Δ_trancl_set A B ⟹ (p, r) ∈ Δ_trancl_set A B" lemma Δ_trancl_set_states: "Δ_trancl_set 𝒜 ℬ ⊆ fset (𝒬 𝒜 |×| 𝒬 ℬ)" proof - {fix p q assume "(p, q) ∈ Δ_trancl_set 𝒜 ℬ" then have "(p, q) ∈ fset (𝒬 𝒜 |×| 𝒬 ℬ)" by (induct) (auto dest: rule_statesD eps_statesD simp flip: fmember.rep_eq)} then show ?thesis by auto qed lemma finite_Δ_trancl_set [simp]: "finite (Δ_trancl_set 𝒜 ℬ)" using finite_subset[OF Δ_trancl_set_states] by simp context includes fset.lifting begin lift_definition Δ_trancl :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) fset" is Δ_trancl_set by simp lemmas Δ_trancl_cong = Δ_set_cong [Transfer.transferred] lemmas Δ_trancl_eps1 = Δ_set_eps1 [Transfer.transferred] lemmas Δ_trancl_eps2 = Δ_set_eps2 [Transfer.transferred] lemmas Δ_trancl_cases = Δ_trancl_set.cases[Transfer.transferred] lemmas Δ_trancl_induct [consumes 1, case_names Δ_cong Δ_eps1 Δ_eps2 Δ_trans] = Δ_trancl_set.induct[Transfer.transferred] lemmas Δ_trancl_intros = Δ_trancl_set.intros[Transfer.transferred] lemmas Δ_trancl_simps = Δ_trancl_set.simps[Transfer.transferred] end lemma Δ_trancl_states: "Δ_trancl 𝒜 ℬ |⊆| (𝒬 𝒜 |×| 𝒬 ℬ)" using Δ_trancl_set_states by (metis Δ_trancl.rep_eq fSigma_cong less_eq_fset.rep_eq) definition GTT_trancl where "GTT_trancl G = (TA (rules (fst G)) (eps (fst G) |∪| (Δ_trancl (snd G) (fst G))), TA (rules (snd G)) (eps (snd G) |∪| (Δ_trancl (fst G) (snd G))))" lemma gtt_states_GTT_trancl: "gtt_states (GTT_trancl G) |⊆| gtt_states G" unfolding GTT_trancl_def by (auto simp: gtt_states_def 𝒬_def dest!: fsubsetD[OF Δ_trancl_states] simp flip: fmember.rep_eq) lemma gtt_syms_GTT_trancl: "gtt_syms (GTT_trancl G) = gtt_syms G" by (auto simp: GTT_trancl_def ta_sig_def) lemma Δ_trancl_inv: "(Δ_trancl A B)|¯| = Δ_trancl B A" proof - have [dest]: "(p, q) |∈| Δ_trancl A B ⟹ (q, p) |∈| Δ_trancl B A" for p q A B by (induct rule: Δ_trancl_induct) (auto intro: Δ_trancl_intros) show ?thesis by auto qed lemma GTT_trancl_base: "gtt_lang G ⊆ gtt_lang (GTT_trancl G)" using gtt_accept_mono[of G "GTT_trancl G"] by (auto simp: GTT_trancl_def) lemma GTT_trancl_trans: "gtt_lang (GTT_comp (GTT_trancl G) (GTT_trancl G)) ⊆ gtt_lang (GTT_trancl G)" proof - have [dest]: "(p, q) |∈| Δ⇩ε (TA (rules A) (eps A |∪| (Δ_trancl B A))) (TA (rules B) (eps B |∪| (Δ_trancl A B))) ⟹ (p, q) |∈| Δ_trancl A B" for p q A B by (induct rule: Δ⇩ε_induct) (auto intro: Δ_trancl_intros simp: Δ_trancl_inv[of B A, symmetric]) show ?thesis by (auto intro!: gtt_accept_mono[of "GTT_comp (GTT_trancl G) (GTT_trancl G)" "GTT_trancl G"]) (auto simp: GTT_comp_def GTT_trancl_def fmember.abs_eq) qed lemma agtt_lang_base: "agtt_lang G ⊆ agtt_lang (GTT_trancl G)" by (rule agtt_lang_mono) (auto simp: GTT_trancl_def) lemma Δ⇩ε_tr_incl: "Δ⇩ε (TA (rules A) (eps A |∪| Δ_trancl B A)) (TA (rules B) (eps B |∪| Δ_trancl A B)) = Δ_trancl A B" (is "?LS = ?RS") proof - {fix p q assume "(p, q) |∈| ?LS" then have "(p, q) |∈| ?RS" by (induct rule: Δ⇩ε_induct) (auto simp: Δ_trancl_inv[of B A, symmetric] intro: Δ_trancl_intros)} moreover {fix p q assume "(p, q) |∈| ?RS" then have "(p, q) |∈| ?LS" by (induct rule: Δ_trancl_induct) (auto simp: Δ_trancl_inv[of B A, symmetric] intro: Δ⇩ε_intros)} ultimately show ?thesis by auto qed lemma agtt_lang_trans: "gcomp_rel UNIV (agtt_lang (GTT_trancl G)) (agtt_lang (GTT_trancl G)) ⊆ agtt_lang (GTT_trancl G)" proof - have [intro!, dest]: "(p, q) |∈| Δ⇩ε (TA (rules A) (eps A |∪| (Δ_trancl B A))) (TA (rules B) (eps B |∪| (Δ_trancl A B))) ⟹ (p, q) |∈| Δ_trancl A B" for p q A B by (induct rule: Δ⇩ε_induct) (auto intro: Δ_trancl_intros simp: Δ_trancl_inv[of B A, symmetric]) show ?thesis by (rule subset_trans[OF gtt_comp_acomplete agtt_lang_mono]) (auto simp: GTT_comp_def GTT_trancl_def ) qed lemma GTT_trancl_acomplete: "gtrancl_rel UNIV (agtt_lang G) ⊆ agtt_lang (GTT_trancl G)" unfolding gtrancl_rel_def using subset_trans[OF lift_root_step_incr[OF agtt_lang_base, of UNIV PAny ESingle G] relax_ext_lift_root_step] agtt_lang_trans[of G] gmctxtex_onp_rel_mono[OF agtt_lang_base[of G], of "λ C. funas_gmctxt C ⊆ UNIV"] agtt_lang_base[of G] unfolding gcomp_rel_def lift_root_step.simps by (intro kleene_trancl_induct) blast+ lemma Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang: "(gtt_lang G)⇧* = (gtt_lang G)⇧+" by (auto simp: rtrancl_trancl_reflcl simp del: reflcl_trancl dest: tranclD tranclD2) lemma GTT_trancl_complete: "(gtt_lang G)⇧+ ⊆ gtt_lang (GTT_trancl G)" using GTT_trancl_base subset_trans[OF gtt_comp_lang_complete GTT_trancl_trans] by (metis trancl_id trancl_mono_set trans_O_iff) lemma gtt_lang_ground_ctxt_closed: assumes "(s, t) ∈ gtt_lang 𝒢" shows "(C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ gtt_lang 𝒢" proof - let ?MC = "gmctxt_of_gctxt C" let ?lhs = "fill_gholes ?MC [s]" let ?rhs = "fill_gholes ?MC [t]" let ?R = "agtt_lang 𝒢" show ?thesis unfolding gmctxtex_onp_gtt_accpet[symmetric] apply_gctxt_fill_gholes apply (intro subsetD[OF gmctxtex_pred_cmp_subseteq, of "λC. True" "λC. True" "(?lhs, ?rhs)" ?R], simp) apply (intro gmctxtex_onpI[of "λC. True" ?MC "[s]" "[t]" "gmctxtex_onp (λC. True) ?R"]) apply (auto simp: assms[unfolded gmctxtex_onp_gtt_accpet[symmetric]]) done qed lemma gtt_langs_ground_ctxt_closed: assumes "(s, t) ∈ (gtt_lang 𝒢)⇧*" shows "(C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ (gtt_lang 𝒢)⇧*" using assms gtt_lang_ground_ctxt_closed[of _ _ 𝒢] by (induct rule: rtrancl_induct) (auto intro: rtrancl.intros(2)) lemma trancl_gtt_lang_arg_closed: assumes "length ss = length ts" "∀i < length ts. (ss ! i, ts ! i) ∈ (gtt_lang 𝒢)⇧+" shows "(GFun f ss, GFun f ts) ∈ (gtt_lang 𝒢)⇧+" (is "?e ∈ _") proof - have "signature_closed UNIV (gmctxtex_onp (λC. True) ((gtt_lang 𝒢)⇧+))" by (intro gmctxtex_onp_sig_closed) auto then show ?thesis using assms unfolding gmctxtex_onp_gtt_accpet[symmetric] by (intro subsetD[OF gmctxtex_onp_substep_trancl [where ?ℛ = "gmctxtex_onp (λC. True) (agtt_lang 𝒢)" and ?P = "λC. True"], of ?e] gmctxtex_pred_cmp_subseteq) (auto simp add: gmctxtex_onp_gtt_accpet gtt_accept.refl elim!: signature_closedD intro: subsetD[OF gmctxtex_closure]) qed lemma Δ_trancl_sound: assumes "(p, q) |∈| Δ_trancl A B" obtains s t where "(s, t) ∈ (gtt_lang (B, A))⇧+" "p |∈| gta_der A s" "q |∈| gta_der B t" using assms proof (induct arbitrary: thesis rule: Δ_trancl_induct) case (Δ_cong f ps p qs q) have "∃si ti. (si, ti) ∈ (gtt_lang (B, A))⇧+ ∧ ps ! i |∈| gta_der A (si) ∧ qs ! i |∈| gta_der B (ti)" if "i < length qs" for i using Δ_cong(5)[OF that] by metis then obtain ss ts where "⋀i. i < length qs ⟹ (ss i, ts i) ∈ (gtt_lang (B, A))⇧+ ∧ ps ! i |∈| gta_der A (ss i) ∧ qs ! i |∈| gta_der B (ts i)" by metis then show ?case using Δ_cong(1-5) by (intro Δ_cong(6)[of "GFun f (map ss [0..<length ps])" "GFun f (map ts [0..<length qs])"]) (auto simp: gta_der_def intro!: trancl_gtt_lang_arg_closed) next case (Δ_eps1 p p' q) then show ?case by (metis gta_der_def ta_der_eps) next case (Δ_eps2 q q' p) then show ?case by (metis gta_der_def ta_der_eps) next case (Δ_trans p q r) guess s1 t1 using Δ_trans(2) . note 1 = this guess s2 t2 using Δ_trans(4) . note 2 = this have "(t1, s2) ∈ gtt_lang (B, A)" using 1(1,3) 2(1,2) by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric]) then have "(s1, t2) ∈ (gtt_lang (B, A))⇧+" using 1(1) 2(1) by (meson trancl.trancl_into_trancl trancl_trans) then show ?case using 1(2) 2(3) by (auto intro: Δ_trans(5)[of s1 t2]) qed lemma GTT_trancl_sound_aux: assumes "p |∈| gta_der (TA (rules A) (eps A |∪| (Δ_trancl B A))) s" shows "∃t. (s, t) ∈ (gtt_lang (A, B))⇧+ ∧ p |∈| gta_der A t" using assms proof (induct s arbitrary: p) case (GFun f ss) let ?eps = "eps A |∪| Δ_trancl B A" obtain qs q where q: "TA_rule f qs q |∈| rules A" "q = p ∨ (q, p) |∈| ?eps|⇧+|" "length qs = length ss" "⋀i. i < length ss ⟹ qs ! i |∈| gta_der (TA (rules A) ?eps) (ss ! i)" using GFun(2) by (auto simp: gta_der_def) have "⋀i. i < length ss ⟹ ∃ti. (ss ! i, ti) ∈ (gtt_lang (A, B))⇧+ ∧ qs ! i |∈| gta_der A (ti)" using GFun(1)[OF nth_mem q(4)] unfolding gta_der_def by fastforce then obtain ts where ts: "⋀i. i < length ss ⟹ (ss ! i, ts i) ∈ (gtt_lang (A, B))⇧+ ∧ qs ! i |∈| gta_der A (ts i)" by metis then have q': "q |∈| gta_der A (GFun f (map ts [0..<length ss]))" "(GFun f ss, GFun f (map ts [0..<length ss])) ∈ (gtt_lang (A, B))⇧+" using q(1, 3) by (auto simp: gta_der_def intro!: exI[of _ qs] exI[of _ q] trancl_gtt_lang_arg_closed) {fix p q u assume ass: "(p, q) |∈| Δ_trancl B A" "(GFun f ss, u) ∈ (gtt_lang (A, B))⇧+ ∧ p |∈| gta_der A u" from Δ_trancl_sound[OF this(1)] guess s t . note st = this have "(u, s) ∈ gtt_lang (A, B)" using st conjunct2[OF ass(2)] by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric]) then have "(GFun f ss, t) ∈ (gtt_lang (A, B))⇧+" using ass st(1) by (meson trancl_into_trancl2 trancl_trans) then have "∃ s t. (GFun f ss, t) ∈ (gtt_lang (A, B))⇧+ ∧ q |∈| gta_der A t" using st by blast} note trancl_step = this show ?case proof (cases "q = p") case True then show ?thesis using ts q(1, 3) by (auto simp: gta_der_def intro!: exI[of _"GFun f (map ts [0..< length ss])"] trancl_gtt_lang_arg_closed) blast next case False then have "(q, p) |∈| ?eps|⇧+|" using q(2) by simp then show ?thesis using q(1) q' proof (induct rule: ftrancl_induct) case (Base q p) from Base(1) show ?case proof assume "(q, p) |∈| eps A" then show ?thesis using Base(2) ts q(3) by (auto simp: gta_der_def intro!: exI[of _"GFun f (map ts [0..< length ss])"] trancl_gtt_lang_arg_closed exI[of _ qs] exI[of _ q]) next assume "(q, p) |∈| (Δ_trancl B A)" then have "(q, p) |∈| Δ_trancl B A" by (simp add: fmember.abs_eq) from trancl_step[OF this] show ?thesis using Base(3, 4) by auto qed next case (Step p q r) from Step(2, 4-) obtain s' where s': "(GFun f ss, s') ∈ (gtt_lang (A, B))⇧+ ∧ q |∈| gta_der A s'" by auto show ?case using Step(3) proof assume "(q, r) |∈| eps A" then show ?thesis using s' by (auto simp: gta_der_def ta_der_eps intro!: exI[of _ s']) next assume "(q, r) |∈| Δ_trancl B A" then have "(q, r) |∈| Δ_trancl B A" by (simp add: fmember.abs_eq) from trancl_step[OF this] show ?thesis using s' by auto qed qed qed qed lemma GTT_trancl_asound: "agtt_lang (GTT_trancl G) ⊆ gtrancl_rel UNIV (agtt_lang G)" proof (intro subrelI, goal_cases LR) case (LR s t) then obtain s' q t' where *: "(s, s') ∈ (gtt_lang G)⇧+" "q |∈| gta_der (fst G) s'" "q |∈| gta_der (snd G) t'" "(t', t) ∈ (gtt_lang G)⇧+" by (auto simp: agtt_lang_def GTT_trancl_def trancl_converse simp flip: gtt_lang_swap[of "fst G" "snd G", unfolded prod.collapse] dest!: GTT_trancl_sound_aux) then have "(s', t') ∈ agtt_lang G" using *(2,3) by (auto simp: agtt_lang_def) then show ?case using *(1,4) unfolding gtrancl_rel_def gtt_lang_from_agtt_lang trancl_map_both[OF inj_term_of_gterm] image_comp comp_def prod.map_comp term_of_gterm_inv prod.map_ident image_ident unfolding lift_root_step_Parallels_single[of _ UNIV, simplified] by (intro relcompI[OF _ relcompI, of s s' _ t' _ t]) (auto simp add: lift_root_step.simps) qed lemma GTT_trancl_sound: "gtt_lang (GTT_trancl G) ⊆ (gtt_lang G)⇧+" proof - note [dest] = GTT_trancl_sound_aux have "gtt_accept (GTT_trancl G) s t ⟹ (s, t) ∈ (gtt_lang G)⇧+" for s t proof (induct rule: gtt_accept.induct) case (join q s t) obtain s' where "(s, s') ∈ (gtt_lang G)⇧+" "q |∈| gta_der (fst G) s'" using join by (auto simp: GTT_trancl_def) moreover obtain t' where "(t', t) ∈ (gtt_lang G)⇧+" "q |∈| gta_der (snd G) t'" using join by (auto simp: GTT_trancl_def gtt_lang_swap[of "fst G" "snd G", symmetric] trancl_converse) moreover have "(s', t') ∈ gtt_lang G" using calculation by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric]) ultimately show "(s, t) ∈ (gtt_lang G)⇧+" by (meson trancl.trancl_into_trancl trancl_trans) qed (auto intro!: trancl_gtt_lang_arg_closed) then show ?thesis by auto qed lemma GTT_trancl_alang: "agtt_lang (GTT_trancl G) = gtrancl_rel UNIV (agtt_lang G)" using GTT_trancl_asound GTT_trancl_acomplete by blast lemma GTT_trancl_lang: "gtt_lang (GTT_trancl G) = (gtt_lang G)⇧+" using GTT_trancl_sound GTT_trancl_complete by blast end