# Theory Context_RR2

```theory Context_RR2
imports Context_Extensions
Ground_MCtxt
Regular_Tree_Relations.RRn_Automata
begin

subsection ‹Auxiliary lemmas›
(* TODO Move *)
lemma gpair_gctxt:
assumes "gpair s t = u"
shows "(map_gctxt (λ f .(Some f, Some f)) C)⟨u⟩⇩G = gpair C⟨s⟩⇩G C⟨t⟩⇩G" using assms
by (induct C arbitrary: s t u) (auto simp add: gpair_context1 comp_def map_funs_term_some_gpair intro!: nth_equalityI)

lemma gpair_gctxt':
assumes "gpair C⟨v⟩⇩G C⟨w⟩⇩G = u"
shows "u = (map_gctxt (λ f .(Some f, Some f)) C)⟨gpair v w⟩⇩G"
using assms by (simp add: gpair_gctxt)

lemma gpair_gmctxt:
assumes "∀ i < length us. gpair (ss ! i) (ts ! i) = us ! i"
and "num_gholes C = length ss" "length ss = length ts" "length ts = length us"
shows "fill_gholes (map_gmctxt (λf . (Some f, Some f)) C) us = gpair (fill_gholes C ss) (fill_gholes C ts)"
using assms
proof (induct C arbitrary: ss ts us)
case GMHole
then show ?case by (cases ss; cases ts; cases us) auto
next
case (GMFun f Cs)
show ?case using GMFun(2-)
using GMFun(1)[OF nth_mem, of i "partition_gholes us Cs ! i" "partition_gholes ss Cs ! i" "partition_gholes ts Cs ! i" for i]
using length_partition_gholes_nth[of Cs] partition_by_nth_nth[of "map num_gholes Cs" us]
using partition_by_nth_nth[of "map num_gholes Cs" ss] partition_by_nth_nth[of "map num_gholes Cs" ts]
by (auto simp: partition_holes_fill_gholes_conv' gpair_context1 simp del: fill_gholes.simps intro!: nth_equalityI)
qed
(*Finished Move section*)

lemma gctxtex_onp_gpair_set_conv:
"{gpair t u |t u. (t, u) ∈ gctxtex_onp P ℛ} =
{(map_gctxt (λ f .(Some f, Some f)) C)⟨s⟩⇩G | C s. P C ∧ s ∈ {gpair t u |t u. (t, u) ∈ ℛ}}" (is "?Ls = ?Rs")
proof
show "?Ls ⊆ ?Rs" using gpair_gctxt'
by (auto elim!: gctxtex_onpE) blast
next
show "?Rs ⊆ ?Ls"
by (auto simp add: gctxtex_onpI gpair_gctxt)
qed

lemma gmctxtex_onp_gpair_set_conv:
"{gpair t u |t u. (t, u) ∈ gmctxtex_onp P ℛ} =
{fill_gholes (map_gmctxt (λ f .(Some f, Some f)) C) ss | C ss. num_gholes C = length ss ∧ P C ∧
(∀ i < length ss. ss ! i ∈ {gpair t u |t u. (t, u) ∈ ℛ})}" (is "?Ls = ?Rs")
proof
{fix u assume "u ∈ ?Ls" then obtain s t
where *: "u = gpair s t" "(s, t) ∈ gmctxtex_onp P ℛ"
by auto
from gmctxtex_onpE[OF *(2)] obtain C us vs where
**: "s = fill_gholes C us" "t = fill_gholes C vs" and
inv: "num_gholes C = length us" "length us = length vs" "P C"
"∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
by blast
define ws where "ws ≡ map2 gpair us vs"
from inv(1, 2) have "∀ i < length ws. gpair (us ! i) (vs ! i) =  ws ! i"
by(auto simp: ws_def)
from gpair_gmctxt[OF this inv(1, 2)] inv
have "u ∈ ?Rs" unfolding * **
by (auto simp: ws_def intro!: exI[of _ ws] exI[of _ C])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix u assume "u ∈ ?Rs" then obtain C ss where
*: "u = fill_gholes (map_gmctxt (λf. (Some f, Some f)) C) ss" and
inv: "P C" "num_gholes C = length ss" "∀ i < length ss. ∃ t u. ss ! i = gpair t u ∧ (t, u) ∈ ℛ"
by auto
define us where "us ≡ map gfst ss" define vs where "vs ≡ map gsnd ss"
then have len: "length ss = length us" "length us = length vs" and
rec: "∀ i < length ss. gpair (us ! i) (vs ! i) = ss ! i"
"∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
by (auto simp: us_def vs_def) (metis gfst_gpair gsnd_gpair inv(3))+
from len have l: "length vs = length ss" by auto
have "u ∈ ?Ls" unfolding * using inv(2) len
using gmctxtex_onpI[of P C us vs ℛ, OF inv(1) _ len(2) rec(2)]
using gpair_gmctxt[OF rec(1) _ len(2) l, of C]
by simp}
then show "?Rs ⊆ ?Ls" by blast
qed

(* Results about lifting signature to RR2
TODO rework, as this is not the RR2 signature more like
the context signature, so closing a RR2 term under this signature
*)

abbreviation "lift_sig_RR2 ≡ λ (f, n). ((Some f, Some f), n)"
abbreviation "lift_fun ≡ (λ f. (Some f, Some f))"
abbreviation "unlift_fst ≡ (λ f. the (fst f))"
abbreviation "unlift_snd ≡ (λ f. the (snd f))"

lemma RR2_gterm_unlift_lift_id [simp]:
"funas_gterm t ⊆ lift_sig_RR2 ` ℱ ⟹ map_gterm (lift_fun ∘ unlift_fst) t = t"
by (induct t) (auto simp add: SUP_le_iff map_idI)

lemma RR2_gterm_unlift_funas [simp]:
"funas_gterm t ⊆ lift_sig_RR2 ` ℱ ⟹ funas_gterm (map_gterm unlift_fst t) ⊆ ℱ"
by (induct t) (auto simp add: SUP_le_iff map_idI)

lemma gterm_funas_lift_RR2_funas [simp]:
"funas_gterm t ⊆ ℱ ⟹ funas_gterm (map_gterm lift_fun t) ⊆ lift_sig_RR2 ` ℱ"
by (induct t) (auto simp add: SUP_le_iff map_idI)

lemma RR2_gctxt_unlift_lift_id [simp, intro]:
"funas_gctxt C ⊆ lift_sig_RR2 ` ℱ ⟹ (map_gctxt (lift_fun ∘ unlift_fst) C) = C"
by (induct C) (auto simp add: all_set_conv_all_nth SUP_le_iff map_idI intro!: nth_equalityI)

lemma RR2_gctxt_unlift_funas [simp, intro]:
"funas_gctxt C ⊆ lift_sig_RR2 ` ℱ ⟹ funas_gctxt (map_gctxt unlift_fst C) ⊆ ℱ"
by (induct C) (auto simp add: all_set_conv_all_nth SUP_le_iff map_idI intro!: nth_equalityI)

lemma gctxt_funas_lift_RR2_funas [simp, intro]:
"funas_gctxt C ⊆ ℱ ⟹ funas_gctxt (map_gctxt lift_fun C) ⊆ lift_sig_RR2 ` ℱ"
by (induct C) (auto simp add: all_set_conv_all_nth SUP_le_iff map_idI intro!: nth_equalityI)

lemma RR2_gmctxt_unlift_lift_id [simp, intro]:
"funas_gmctxt C ⊆ lift_sig_RR2 ` ℱ ⟹ (map_gmctxt (lift_fun ∘ unlift_fst) C) = C"
by (induct C) (auto simp add: all_set_conv_all_nth SUP_le_iff map_idI intro!: nth_equalityI)

lemma RR2_gmctxt_unlift_funas [simp, intro]:
"funas_gmctxt C ⊆ lift_sig_RR2 ` ℱ ⟹ funas_gmctxt (map_gmctxt unlift_fst C) ⊆ ℱ"
by (induct C) (auto simp add: all_set_conv_all_nth SUP_le_iff map_idI intro!: nth_equalityI)

lemma gmctxt_funas_lift_RR2_funas [simp, intro]:
"funas_gmctxt C ⊆ ℱ ⟹ funas_gmctxt (map_gmctxt lift_fun C) ⊆ lift_sig_RR2 ` ℱ"
by (induct C) (auto simp add: all_set_conv_all_nth SUP_le_iff map_idI intro!: nth_equalityI)

lemma RR2_gctxt_cl_to_gctxt:
assumes "⋀ C. P C ⟹ funas_gctxt C ⊆ lift_sig_RR2 ` ℱ"
and "⋀ C. P C ⟹ R (map_gctxt unlift_fst C)"
and "⋀ C. R C ⟹ P (map_gctxt lift_fun C)"
shows "{C⟨s⟩⇩G |C s. P C ∧ Q s} = {(map_gctxt lift_fun C)⟨s⟩⇩G |C s. R C ∧ Q s}" (is "?Ls = ?Rs")
proof
{fix u assume "u ∈ ?Ls" then obtain C s where
*:"u = C⟨s⟩⇩G" and inv: "P C" "Q s" by blast
then have "funas_gctxt C ⊆ lift_sig_RR2 ` ℱ" using assms by auto
from RR2_gctxt_unlift_lift_id[OF this] have "u ∈ ?Rs" using inv assms unfolding *
by (auto intro!: exI[of _ "map_gctxt unlift_fst C"] exI[of _ s])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix u assume "u ∈ ?Rs" then obtain C s where
*:"u = (map_gctxt lift_fun C)⟨s⟩⇩G" and inv: "R C" "Q s"
by blast
have "u ∈ ?Ls" unfolding * using inv assms
by (auto intro!: exI[of _ "map_gctxt lift_fun C"])}
then show "?Rs ⊆ ?Ls" by blast
qed

lemma RR2_gmctxt_cl_to_gmctxt:
assumes "⋀ C. P C ⟹ funas_gmctxt C ⊆ lift_sig_RR2 ` ℱ"
and "⋀ C. P C ⟹ R (map_gmctxt (λ f. the (fst f)) C)"
and "⋀ C. R C ⟹ P (map_gmctxt (λ f. (Some f, Some f)) C)"
shows "{fill_gholes C ss |C ss. num_gholes C = length ss ∧ P C ∧ (∀ i < length ss. Q (ss ! i))} =
{fill_gholes (map_gmctxt (λf. (Some f, Some f)) C) ss |C ss. num_gholes C = length ss ∧
R C ∧ (∀ i < length ss. Q (ss ! i))}" (is "?Ls = ?Rs")
proof
{fix u assume "u ∈ ?Ls" then obtain C ss where
*:"u = fill_gholes C ss" and inv: "num_gholes C = length ss" "P C" "∀ i < length ss. Q (ss ! i)"
by blast
then have "funas_gmctxt C ⊆ lift_sig_RR2 ` ℱ" using assms by auto
from RR2_gmctxt_unlift_lift_id[OF this] have "u ∈ ?Rs" using inv assms unfolding *
by (auto intro!: exI[of _ "map_gmctxt unlift_fst C"] exI[of _ ss])}
then show "?Ls ⊆ ?Rs" by blast
next
{fix u assume "u ∈ ?Rs" then obtain C ss where
*:"u = fill_gholes (map_gmctxt lift_fun C) ss" and inv: "num_gholes C = length ss" "R C"
"∀ i < length ss. Q (ss ! i)"
by blast
have "u ∈ ?Ls" unfolding * using inv assms
by (auto intro!: exI[of _ "map_gmctxt lift_fun C"])}
then show "?Rs ⊆ ?Ls" by blast
qed

lemma RR2_id_terms_gpair_set [simp]:
"𝒯⇩G (lift_sig_RR2 ` ℱ) = {gpair t u |t u. (t, u) ∈ Restr Id (𝒯⇩G ℱ)}"
apply (auto simp: map_funs_term_some_gpair 𝒯⇩G_equivalent_def)
apply (smt RR2_gterm_unlift_funas RR2_gterm_unlift_lift_id gterm.map_comp)
using funas_gterm_map_gterm by blast

end```