theory Ground_Closure imports Ground_Terms begin subsubsection ‹Multihole context closure› text ‹Computing the multihole context closure of a given relation› inductive_set gmctxt_cl :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" for ℱ ℛ where base [intro]: "(s, t) ∈ ℛ ⟹ (s, t) ∈ gmctxt_cl ℱ ℛ" | step [intro]: "length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ gmctxt_cl ℱ ℛ) ⟹ (f, length ss) ∈ ℱ ⟹ (GFun f ss, GFun f ts) ∈ gmctxt_cl ℱ ℛ" lemma gmctxt_cl_idemp [simp]: "gmctxt_cl ℱ (gmctxt_cl ℱ ℛ) = gmctxt_cl ℱ ℛ" proof - {fix s t assume "(s, t) ∈ gmctxt_cl ℱ (gmctxt_cl ℱ ℛ)" then have "(s, t) ∈ gmctxt_cl ℱ ℛ" by (induct) (auto intro: gmctxt_cl.step)} then show ?thesis by auto qed lemma gmctxt_cl_refl: "funas_gterm t ⊆ ℱ ⟹ (t, t) ∈ gmctxt_cl ℱ ℛ" by (induct t) (auto simp: SUP_le_iff intro!: gmctxt_cl.step) lemma gmctxt_cl_swap: "gmctxt_cl ℱ (prod.swap ` ℛ) = prod.swap ` gmctxt_cl ℱ ℛ" (is "?Ls = ?Rs") proof - {fix s t assume "(s, t) ∈ ?Ls" then have "(s, t) ∈ ?Rs" by induct auto} moreover {fix s t assume "(s, t) ∈ ?Rs" then have "(t, s) ∈ gmctxt_cl ℱ ℛ" by auto then have "(s, t) ∈ ?Ls" by induct auto} ultimately show ?thesis by auto qed lemma gmctxt_cl_mono_funas: assumes "ℱ ⊆ 𝒢" shows "gmctxt_cl ℱ ℛ ⊆ gmctxt_cl 𝒢 ℛ" proof - {fix s t assume "(s, t) ∈ gmctxt_cl ℱ ℛ" then have "(s, t) ∈ gmctxt_cl 𝒢 ℛ" by induct (auto simp: subsetD[OF assms])} then show ?thesis by auto qed lemma gmctxt_cl_mono_rel: assumes "𝒫 ⊆ ℛ" shows "gmctxt_cl ℱ 𝒫 ⊆ gmctxt_cl ℱ ℛ" proof - {fix s t assume "(s, t) ∈ gmctxt_cl ℱ 𝒫" then have "(s, t) ∈ gmctxt_cl ℱ ℛ" using assms by induct auto} then show ?thesis by auto qed definition gcomp_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel ⇒ 'f gterm rel" where "gcomp_rel ℱ R S = (R O gmctxt_cl ℱ S) ∪ (gmctxt_cl ℱ R O S)" definition gtrancl_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" where "gtrancl_rel ℱ ℛ = (gmctxt_cl ℱ ℛ)⇧^{+}O ℛ O (gmctxt_cl ℱ ℛ)⇧^{+}" lemma gcomp_rel: "gmctxt_cl ℱ (gcomp_rel ℱ ℛ 𝒮) = gmctxt_cl ℱ ℛ O gmctxt_cl ℱ 𝒮" (is "?Ls = ?Rs") proof { fix s u assume "(s, u) ∈ gmctxt_cl ℱ (ℛ O gmctxt_cl ℱ 𝒮 ∪ gmctxt_cl ℱ ℛ O 𝒮)" then have "∃t. (s, t) ∈ gmctxt_cl ℱ ℛ ∧ (t, u) ∈ gmctxt_cl ℱ 𝒮" proof (induct) case (step ss ts f) from Ex_list_of_length_P[of _ "λ u i. (ss ! i, u) ∈ gmctxt_cl ℱ ℛ ∧ (u, ts ! i) ∈ gmctxt_cl ℱ 𝒮"] obtain us where l: "length us = length ts" and inv: "∀ i < length ts. (ss ! i, us ! i) ∈ gmctxt_cl ℱ ℛ ∧ (us ! i, ts ! i) ∈ gmctxt_cl ℱ 𝒮" using step(2, 3) by blast then show ?case using step(1, 3) by (intro exI[of _ "GFun f us"]) auto qed auto} then show "?Ls ⊆ ?Rs" unfolding gcomp_rel_def by auto next {fix s t u assume "(s, t) ∈ gmctxt_cl ℱ ℛ" "(t, u) ∈ gmctxt_cl ℱ 𝒮" then have "(s, u) ∈ gmctxt_cl ℱ (ℛ O gmctxt_cl ℱ 𝒮 ∪ gmctxt_cl ℱ ℛ O 𝒮)" proof (induct arbitrary: u rule: gmctxt_cl.induct) case (step ss ts f) then show ?case proof (cases "(GFun f ts, u) ∈ 𝒮") case True then have "(GFun f ss, u) ∈ gmctxt_cl ℱ ℛ O 𝒮" using gmctxt_cl.step[OF step(1) _ step(3)] step(2) by auto then show ?thesis by auto next case False then obtain us where u[simp]: "u = GFun f us" and l: "length ts = length us" using step(4) by (cases u) (auto elim: gmctxt_cl.cases) have "i < length us ⟹ (ss ! i, us ! i) ∈ gmctxt_cl ℱ (ℛ O gmctxt_cl ℱ 𝒮 ∪ gmctxt_cl ℱ ℛ O 𝒮)" for i using step(1, 2, 4) False by (auto elim: gmctxt_cl.cases) then show ?thesis using l step(1, 3) by auto qed qed auto} then show "?Rs ⊆ ?Ls" by (auto simp: gcomp_rel_def) qed subsubsection ‹Signature closed property› definition all_ctxt_closed :: "('f × nat) set ⇒ 'f gterm rel ⇒ bool" where "all_ctxt_closed F r ⟷ (∀ f ts ss. (f, length ss) ∈ F ⟶ length ss = length ts ⟶ (∀i. i < length ts ⟶ (ss ! i, ts ! i) ∈ r) ⟶ (GFun f ss, GFun f ts) ∈ r)" lemma all_ctxt_closedI: assumes "⋀ f ss ts. (f, length ss) ∈ ℱ ⟹ length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ r) ⟹ (GFun f ss, GFun f ts) ∈ r" shows "all_ctxt_closed ℱ r" using assms unfolding all_ctxt_closed_def by auto lemma all_ctxt_closedD: "all_ctxt_closed F r ⟹ (f, length ss) ∈ F ⟹ length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ r) ⟹ (GFun f ss, GFun f ts) ∈ r" by (auto simp: all_ctxt_closed_def) lemma all_ctxt_closed_refl_on: assumes "all_ctxt_closed ℱ r" "s ∈ 𝒯⇩_{G}ℱ" shows "(s, s) ∈ r" using assms(2) by (induct) (auto simp: all_ctxt_closedD[OF assms(1)]) lemma gmctxt_cl_is_all_ctxt_closed [simp]: "all_ctxt_closed ℱ (gmctxt_cl ℱ ℛ)" unfolding all_ctxt_closed_def by auto lemma all_ctxt_closed_gmctxt_cl_idem [simp]: assumes "all_ctxt_closed ℱ ℛ" shows "gmctxt_cl ℱ ℛ = ℛ" proof - {fix s t assume "(s, t) ∈ gmctxt_cl ℱ ℛ" then have "(s, t) ∈ ℛ" proof (induct) case (step ss ts f) show ?case using step(2) all_ctxt_closedD[OF assms step(3, 1)] by auto qed auto} then show ?thesis by auto qed subsubsection ‹Transitive closure preserves @{const all_ctxt_closed}› text ‹induction scheme for transitive closures of lists› inductive_set trancl_list for ℛ where base[intro, Pure.intro] : "length xs = length ys ⟹ (∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ) ⟹ (xs, ys) ∈ trancl_list ℛ" | list_trancl [Pure.intro]: "(xs, ys) ∈ trancl_list ℛ ⟹ i < length ys ⟹ (ys ! i, z) ∈ ℛ ⟹ (xs, ys[i := z]) ∈ trancl_list ℛ" lemma trancl_list_appendI [simp, intro]: "(xs, ys) ∈ trancl_list ℛ ⟹ (x, y) ∈ ℛ ⟹ (x # xs, y # ys) ∈ trancl_list ℛ" proof (induct rule: trancl_list.induct) case (base xs ys) then show ?case using less_Suc_eq_0_disj by (intro trancl_list.base) auto next case (list_trancl xs ys i z) from list_trancl(3) have *: "y # ys[i := z] = (y # ys)[Suc i := z]" by auto show ?case using list_trancl unfolding * by (intro trancl_list.list_trancl) auto qed lemma trancl_list_append_tranclI [intro]: "(x, y) ∈ ℛ⇧^{+}⟹ (xs, ys) ∈ trancl_list ℛ ⟹ (x # xs, y # ys) ∈ trancl_list ℛ" proof (induct rule: trancl.induct) case (trancl_into_trancl a b c) then have "(a # xs, b # ys) ∈ trancl_list ℛ" by auto from trancl_list.list_trancl[OF this, of 0 c] show ?case using trancl_into_trancl(3) by auto qed auto lemma trancl_list_conv: "(xs, ys) ∈ trancl_list ℛ ⟷ length xs = length ys ∧ (∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ⇧^{+})" (is "?Ls ⟷ ?Rs") proof assume "?Ls" then show ?Rs proof (induct) case (list_trancl xs ys i z) then show ?case by auto (metis nth_list_update trancl.trancl_into_trancl) qed auto next assume ?Rs then show ?Ls proof (induct ys arbitrary: xs) case Nil then show ?case by (cases xs) auto next case (Cons y ys) from Cons(2) obtain x xs' where *: "xs = x # xs'" and inv: "(x, y) ∈ ℛ⇧^{+}" by (cases xs) auto show ?case using Cons(1)[of "tl xs"] Cons(2) unfolding * by (intro trancl_list_append_tranclI[OF inv]) force qed qed lemma trancl_list_induct [consumes 2, case_names base step]: assumes "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ⇧^{+}" and "⋀xs ys. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ ⟹ P xs ys" and "⋀xs ys i z. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ⇧^{+}⟹ P xs ys ⟹ i < length ys ⟹ (ys ! i, z) ∈ ℛ ⟹ P xs (ys[i := z])" shows "P ss ts" using assms by (intro trancl_list.induct[of ss ts ℛ P]) (auto simp: trancl_list_conv) lemma trancl_list_all_step_induct [consumes 2, case_names base step]: assumes "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ⇧^{+}" and base: "⋀xs ys. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ ⟹ P xs ys" and steps: "⋀xs ys zs. length xs = length ys ⟹ length ys = length zs ⟹ ∀ i < length zs. (xs ! i, ys ! i) ∈ ℛ⇧^{+}⟹ ∀ i < length zs. (ys ! i, zs ! i) ∈ ℛ ∨ ys ! i = zs ! i ⟹ P xs ys ⟹ P xs zs" shows "P ss ts" using assms(1, 2) proof (induct rule: trancl_list_induct) case (step xs ys i z) then show ?case by (intro steps[of xs ys "ys[i := z]"]) (auto simp: nth_list_update) qed (auto simp: base) lemma all_ctxt_closed_trancl: assumes "all_ctxt_closed ℱ ℛ" "ℛ ⊆ 𝒯⇩_{G}ℱ × 𝒯⇩_{G}ℱ" shows "all_ctxt_closed ℱ (ℛ⇧^{+})" proof - {fix f ss ts assume sig: "(f, length ss) ∈ ℱ" and steps: "length ss = length ts" "∀i<length ts. (ss ! i, ts ! i) ∈ ℛ⇧^{+}" have "(GFun f ss, GFun f ts) ∈ ℛ⇧^{+}" using steps sig proof (induct rule: trancl_list_induct) case (base ss ts) then show ?case using all_ctxt_closedD[OF assms(1) base(3, 1, 2)] by auto next case (step ss ts i t') from step(2) have "j < length ts ⟹ ts ! j ∈ 𝒯⇩_{G}ℱ" for j using assms(2) by (metis (no_types, lifting) SigmaD2 subset_iff trancl.simps) from this[THEN all_ctxt_closed_refl_on[OF assms(1)]] have "(GFun f ts, GFun f (ts[i := t'])) ∈ ℛ" using step(1, 4-) by (intro all_ctxt_closedD[OF assms(1)]) (auto simp: nth_list_update) then show ?case using step(3, 6) by auto qed} then show ?thesis by (intro all_ctxt_closedI) qed end